theorem WrittenOnTheWallII.GraphConjecture3.conjecture3 {α : Type u} [Fintype α] [DecidableEq α] {G : SimpleGraph α} [DecidableEq α] [DecidableRel G.Adj] [Nonempty α] (h_conn : G.Connected) : ↑G.gi * G.MaxTemp ≤ G.Ls

WOWII Conjecture 3

For a connected simple graph G, the number of leaves in a maximum spanning tree satisfies Ls(G) ≥ gi(G) * MaxTemp(G), where gi(G) is the independent domination number and MaxTemp(G) is max_v deg(v)/(n(G) - deg(v)).