Documentation

FormalConjectures.WrittenOnTheWallII.GraphConjecture65

Written on the Wall II - Conjecture 65 #

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

theorem WrittenOnTheWallII.GraphConjecture65.conjecture65 {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) :
have A := {v : α | G.degree v = G.minDegree}; have M := {v : α | G.degree v = G.maxDegree}; (G.distMin A) + (G.distMin M) / 3 G.largestInducedForestSize

WOWII Conjecture 65:

For a simple connected graph $G$, the size $f(G)$ of a largest induced forest satisfies $f(G) \ge \operatorname{dist\_min}(A) + \lceil \operatorname{dist\_min}(M) / 3 \rceil$, where $A$ is the set of minimum-degree vertices, $M$ is the set of maximum-degree vertices, and $\operatorname{dist\_min}(S) = \min_{v \notin S} \operatorname{dist}(v, S)$ (see distMin).