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ña'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 $\hat{I}{´}^{\prime }(G)$ is the second-smallest degree, counted with multiplicity, then every connected non-tree graph satisfies $t(G)\hat{I}{´}^{\prime }(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.

16 pages. Complete Lean 4 proofs of all three formal statements are included as ancillary files; see Google DeepMind Formal Conjectures pull requests #4454 and #4457