Lean-Certified Infinite Counterexamples to Written on the Wall II Conjecture 194

Abstract

For a finite simple graph G, let alpha(G) denote its independence number and let l_avg(G) = (1 / |V(G)|) sum_{v in V(G)} alpha(G[N_G(v)]) be the average independence number of its open neighbourhoods. Written on the Wall II Conjecture 194 asserts that every simple connected graph on n > 1 vertices satisfying alpha(G) <= 1 + l_avg(G) has a Hamiltonian path. We give a four-parameter family of counterexamples. Its principal two-parameter subfamily satisfies the proposed inequality with equality: for every pair of integers s >= 1 and t >= 3 it has (s + 1)t^2 vertices, independence number t + 1, l_avg(G) = t, and minimum degree s, but has no Hamiltonian path. This entire infinite subfamily is machine-checked in Lean 4: one universally quantified theorem certifies its order, connectivity, independence number, average neighbourhood independence, minimum degree, conjecture hypothesis, and failure of traceability. Thus no fixed lower bound on the minimum degree repairs the conjecture. The case (s,t) = (1,3) has 18 vertices, but the formal certificate is parametric rather than a verification of that one graph alone.