Three Graffiti.pc Conjectures on Largest Induced Trees: Proofs of Conjectures 141, 142, and 143

Abstract

For a finite simple graph $G$, let $t(G)$ be the largest order of an induced tree and let $g(G)$ be the girth. We prove three consecutive conjectures of DeLaVi\~na's Graffiti.pc program. First, writing $\ell(v)$ for the independence number of the subgraph induced by the neighbourhood of $v$, we prove $t(G) \ge \lfloor g(G)/2 \rfloor - 1 + \max_{v \in V(G)} \ell(v)$. Second, if $\mathrm{Per}(G)$ is the periphery and $f(G) = \max_x d(x, \mathrm{Per}(G))$, we prove $t(G) \ge \frac{2}{3} g(G) + f(G)$, and establish the stronger integral bound $t(G) \ge f(G) + \lceil 2g(G)/3 \rceil$ when $G$ contains a cycle. Third, if $\delta'(G)$ is the second-smallest degree, counted with multiplicity, then every connected non-tree graph satisfies $t(G) \delta'(G) \ge g(G) + 1$. These are Conjectures 141, 142, and 143 of Written on the Wall II. Complete, machine-checked Lean 4 proofs of all three formal statements accompany the manuscript.