Written on the Wall II - Conjecture 142

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

theorem WrittenOnTheWallII.GraphConjecture142.conjecture142 {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) : have B := G.maxEccentricityVertices; 2 / 3 * ↑G.girth + ↑(G.eccSet B) ≤ ↑G.largestInducedTreeSize

WOWII Conjecture 142:

For a simple connected graph $G$, $\mathrm{tree}(G) \ge (2/3) \cdot \mathrm{girth}(G) + \mathrm{ecc}(B)$ where $\mathrm{tree}(G)$ is the largest induced tree size, $\mathrm{girth}(G)$ is the length of the shortest cycle ($0$ if acyclic), $B$ is the set of boundary vertices (those of maximum eccentricity), and $\mathrm{ecc}(B)$ is the eccentricity of the set $B$.