Lean-Certified Infinite Counterexamples to Written on the Wall II Conjecture 194
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 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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2609.19195
curl -X POST /api/v1/records/arxiv/2609.19195/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2609.19195/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'