Documentation

FormalConjectures.WrittenOnTheWallII.GraphConjecture194

Written on the Wall II - Conjecture 194 #

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

theorem WrittenOnTheWallII.GraphConjecture194.conjecture194 {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) (h : G.Connected) ( : G.indepNum 1 + G.l) :
∃ (a : α) (b : α) (p : G.Walk a b), p.IsHamiltonian

WOWII Conjecture 194

For a simple connected graph G, if α(G) ≤ 1 + l_avg(G), then G has a Hamiltonian path. Here α(G) = G.indepNum is the independence number, and l_avg(G) = averageIndepNeighbors G is the average over all vertices of the independence number of the neighbourhood. A Hamiltonian path is a walk visiting every vertex exactly once.