Written on the Wall II - Conjecture 7

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

theorem WrittenOnTheWallII.GraphConjecture7.conjecture7 {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) : have maxL := (Finset.image (fun (v : α) => G.indepNeighborsCard v) Finset.univ).max' ⋯; ↑↑maxL - 1 + ↑↑(Fintype.card α) - 2 * ↑↑G.indepNum ≤ G.Ls

WOWII Conjecture 7

For a simple connected graph $G$, $L_s(G) \ge \max_v \lambda(v) - 1 + n - 2 \alpha(G)$, where $L_s(G)$ is the maximum number of leaves over all spanning trees of $G$, $n = |V(G)|$, $\alpha(G) = G.\mathrm{indepNum}$ is the independence number, and $\lambda(v) = \mathrm{indepNeighborsCard}\, G\, v$ is the independence number of the neighbourhood of $v$.

Proved by DeLaVina, Fajtlowicz, Waller (2002).