Written on the Wall II - Conjecture 200

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

theorem WrittenOnTheWallII.GraphConjecture200.conjecture200 {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) (h : G.Connected) (htree : ↑G.largestInducedTreeSize = ↑⌈1 + G.l⌉) : ∃ (a : α) (b : α) (p : G.Walk a b), p.IsHamiltonian

WOWII Conjecture 200

For a simple connected graph G, if tree(G) = ⌈1 + l_avg(G)⌉, then G has a Hamiltonian path. Here tree(G) is the number of vertices of a largest induced tree subgraph, 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.