Abstract
No finite simple graph on 13 vertices satisfies \(\gamma(G)=\gamma^\infty(G)=3<\theta(G)\).
The proof fixes a maximum independent triple in an optimal one-guard eternal family and separates the search into full-response and no-full-response branches. Human response-list lemmas reduce the no-full branch to a bounded signature census. Three exact formulas are then discharged by independently reconstructed, RUP-only proof certificates.
Main theorem
Theorem. There is no finite simple graph \(G\) on 13 vertices such that
This theorem is unconditional on lower-order enumeration. Combined with the separately certified order-12 frontier and standard structural bounds, it says only that any order-13 counterexample has common parameter four or five. It does not establish a lower bound of 14.
Here \(\theta(G)=\chi(\overline G)\) is the clique-cover number. The paper uses the standard one-guard-moves eternal domination game: attacks occur only at unoccupied vertices, and exactly one adjacent guard moves to the attacked vertex. It does not concern the all-guards-move model or the Lovász theta function \(\vartheta\).
Proof and certificate architecture
| Branch | Evidence |
|---|---|
| Full response | 9,802 variables, 85,409 clauses, RUP-only DRAT refutation, independent reduced replay, exact orbit coverage, and a positive equality control after removing the clique-cover gap |
| Four-neutral obstruction | 1,222 variables, 24,694 clauses, 78,697 addition-only RUP steps, fresh LRAT conversion, and a sharp three-neutral equality control |
| Residual no-full branch | 9,802 variables, 84,614 clauses, 156,205 addition-only RUP steps, all six anchor normalizations, all 1,716 sorted residual signature multisets, and a satisfiable theta-gap ablation |
| Independent replay | Clean-room generators reconstruct decisive formulas byte for byte; separate checkers validate one-guard semantics, graph/complement direction, proof streams, controls, and theorem coverage |
The compact aggregate replay is python3 -I -B -W error repro/c097/replay.py, run from the campaign directory. No SAT solver is needed to verify the retained deletion-free proofs.
Attribution, scope, and limitations
William F. Klostermeyer and Gary MacGillivray asserted the implication in 2009. Klostermeyer and C. M. Mynhardt identified a gap in that proof and reopened the implication as an explicit question in 2015; subsequent literature refers to their conjectural formulation as the \(\gamma\)–\(\theta\) conjecture. The published exhaustive computation through order 11 is due to Gary MacGillivray, C. M. Mynhardt, and Virgélot Virgile.
The candidate contribution here is the order-13, parameter-three exclusion and its exact proof package. A current literature audit found no prior matching result, but a negative search is not proof of worldwide priority and no priority claim is made. No external expert was contacted, and no external review has occurred.
AI-assistance and verification disclosure
The exploratory mathematics, programs, certificate design, adversarial audits, literature review, manuscript, and publication materials were developed with heavy assistance from ChatGPT 5.6 Sol under Alec Kriebel's direction. Alec Kriebel is the human author and project lead. No finite or mathematical claim was accepted on model output alone. Passing the supplied checks is evidence about the encoded theorem; it is not peer review.
Suggested citation
Alec Kriebel, “Excluding Parameter Three at Order Thirteen in the \(\gamma\)–\(\theta\) Conjecture for One-Guard Eternal Domination,” provisional research paper, 28 July 2026.