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 $δ'(G)$ is the second-smallest degree, counted with multiplicity, then every connected non-tree graph satisfies $t(G) δ'(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.

Disclosure

“etric estimate. Conjecture 143 reduces to a two-leaf induced-tree lemma. The associated Lean developments are recorded in Formal Conjectures pull requests #4454 and #4457 [15, 16] and are included as ancillary files. Use of generative AI. OpenAI GPT Pro and Codex were used for proof exploration, literature- search assistance, computational checks, Lean development, and manuscript preparation. They are not authors. Responsibility for verifying the work and for the submitted version”

PDF page 2

Classification

Proof ideas or individual proof-step assistance

Multiplier

8

Verified

2026-08-23T21:13:22.439528Z

Structural counts