Written on the Wall II - Conjecture 61

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

theorem WrittenOnTheWallII.GraphConjecture61.conjecture61 {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) : ↑G.residue + ↑⌈↑G.diam / 3⌉ ≤ ↑G.largestInducedForestSize

WOWII Conjecture 61

For a simple connected graph $G$, the size $f(G)$ of a largest induced forest satisfies $f(G) \ge \mathrm{residue}(G) + \lceil \mathrm{diam}(G) / 3 \rceil$, where $\mathrm{residue}(G)$ is the Havel-Hakimi residue and $\mathrm{diam}(G)$ is the diameter of $G$.

See: Favaron, Mahéo, Saclé (1991) for the residue; DeLaVina's Graffiti.pc for the conjecture.