Written on the Wall II - Conjecture 1

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

theorem WrittenOnTheWallII.GraphConjecture1.conjecture1 {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) [DecidableRel G.Adj] (h_conn : G.Connected) : ↑(Fintype.card α) + 1 - 2 * G.matchingNumber ≤ G.Ls

WOWII Conjecture 1

For a simple connected graph G the maximum number of leaves of a spanning tree satisfies Ls(G) ≥ n(G) + 1 - 2·m(G) where n(G) counts vertices and m(G) is the size of a maximum matching.