Written on the Wall II - Conjecture 217

Per the WOWII definitions popup linked from this conjecture:

• $L(G)$ is the maximum number of leaves of a spanning tree of $G$ — i.e. Ls G in our invariant library.
• $\chi_{\mathrm{residue}=2}(G)$ is the characteristic function for the predicate $\mathrm{residue}\, G = 2$, i.e. $1$ when $\mathrm{residue}\, G = 2$ and $0$ otherwise. It is not a connected-component count of any 2-core.

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

noncomputable def WrittenOnTheWallII.GraphConjecture217.residueEqTwoIndicator {α : Type u_1} [Fintype α] (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ

The characteristic function for the predicate $\mathrm{residue}\, G = 2$: returns $1$ when $G.\mathrm{residue} = 2$ and $0$ otherwise. This is the WOWII $\chi_{\mathrm{residue}=2}(G)$ indicator appearing in Conjecture 217.

Equations

• WrittenOnTheWallII.GraphConjecture217.residueEqTwoIndicator G = if G.residue = 2 then 1 else 0

theorem WrittenOnTheWallII.GraphConjecture217.conjecture217 {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) (hL : G.Ls ≤ 4 * ↑(residueEqTwoIndicator G) + 2) : ∃ (a : α) (b : α) (p : G.Walk a b), p.IsHamiltonian

WOWII Conjecture 217:

If $G$ is a finite simple connected graph on $n > 1$ vertices and $L_s(G) \le 4 \cdot \chi_{\mathrm{residue}=2}(G) + 2$, then $G$ has a Hamiltonian path. Here $L_s(G)$ is the maximum number of leaves over all spanning trees and $\chi_{\mathrm{residue}=2}(G)$ is the indicator of $\mathrm{residue}(G) = 2$.