The problem, in plain language
If the smallest dominating guard team can defend forever while moving only one guard per attack, must the vertices already split into that many cliques?
For a finite simple graph \(G\), let \(\gamma(G)\) be its domination number and let \(\gamma^\infty(G)\) be its eternal domination number in the standard one-guard model: attacks occur only at unoccupied vertices, and exactly one adjacent guard moves along one edge to the attacked vertex. Here \(\theta(G)\) is the clique-cover number, equivalently \(\chi(\overline G)\). It is not the Lovász theta function \(\vartheta(G)\).
The \(\gamma\)–\(\theta\) conjecture. For every finite simple graph \(G\),
A counterexample would satisfy \(\gamma(G)=\gamma^\infty(G)<\theta(G)\).
*Relative to MacGillivray–Mynhardt–Virgile's published exhaustive computation through order 11.
The certified order-12 frontier
Order-12 theorem. Assume the published exhaustive result of MacGillivray, Mynhardt, and Virgile that no counterexample has order at most 11. Then no finite simple graph of order at most 12 satisfies \(\gamma(G)=\gamma^\infty(G)<\theta(G)\). Equivalently, every counterexample, if one exists, has order at least 13.
The proof first uses the parameter chain \(\gamma\leq i\leq\alpha\leq\gamma^\infty\leq\theta\), component additivity, and a classical half-order domination theorem. A hypothetical minimum order-12 counterexample is connected and its common value can only be \(3\), \(4\), or \(5\). Those three cases are then closed by different mechanisms.
| Parameter | Method | Exact status |
|---|---|---|
| \(k=3\) | Odd-hole template coverage plus three independently replayed proof certificates | Certified finite exclusion |
| \(k=4\) | 18,381-variable graph-to-CNF theorem plus a checked 228,381,671-byte LRAT refutation | Certified connected exclusion |
| \(k=5\) | Simplicial closed-neighborhood reduction plus the McCuaig–Shepherd domination bound | Analytic exclusion |
The campaign independently reproduced the published 56-graph appendix and exhaustively checked connected unlabeled graphs through order 9. It did not rerun the original billion-graph enumeration at order 11, so that published lower-order result remains an explicit premise rather than a campaign certificate.
What is known at order 13
The complete order-13 search has not been finished, and no lower bound of 14 is claimed. The strongest current reduction concerns common parameter \(3\). In the complement of a putative counterexample, the required imperfect obstruction reduces to overlapping induced odd-hole templates \(C_5,C_7,C_9,C_{11}\).
- \(C_{11}\) branch — proved impossible. A near-spanning odd hole leaves only two outside vertices, and a direct one-guard attack argument forces \(\gamma^\infty\geq4\).
- \(C_9\) branch — certified impossible. The exact 9,802-variable, 32,108-clause formula is refuted by an addition-only RUP proof and a separate LRAT proof, both independently reconstructed and checked.
- \(C_5\) and \(C_7\) branches — still live. These are the complete remaining cover for the order-13, parameter-three slice.
- Parameters \(4\) and \(5\) — still live. The parameter-five lane has a proved ten-vertex-kernel reduction; neither slice has a complete finite exclusion.
A separately proved pair of infinite near-miss families explains why the equality conditions are delicate: for every relevant odd length, they satisfy \(\gamma=i=\alpha=3\) while \(\gamma^\infty=\theta=4\). They are not counterexamples, but they sit one eternal guard away from the target.
Reproducibility and exact scope
The release contains the paper source, theorem notes, exact formulas, compressed proofs, source-pinned proof checkers, independent reconstructions, mutation tests, acceptance records, and one-command replay wrappers. Search output is never promoted solely because a solver prints UNSAT.
| Claim | Replay | Meaning |
|---|---|---|
| Order-12 frontier, C-050 | python3 repro/c050/replay.py --full | Checks theorem bindings and replays the exact LRAT proof |
| Order-13 \(C_9\) exclusion, C-057 | python3 repro/c057/replay.py | Reconstructs the formula and replays independent RUP/LRAT checks |
| Claim ledger | CLAIMS.md | Labels every statement as proved, certified finite, observed, conjectured, or refuted |
These checks certify the exact encoded finite statements. They are not peer review, and they cannot by themselves establish literature novelty or the correctness of every imported theorem.
Current strategy: pursue a decisive proof before order 14
After a first day dominated by exact finite certification, the campaign is deliberately rebalanced toward the universal question. The next order-13 computation has been prepared and independently preflighted, but it is paused before solver launch while the proof lane receives priority.
The central proof object is a minimum counterexample. Equality collapses all four intermediate parameters:
For every independent set \(A\) smaller than this common value, deleting \(N[A]\) leaves a smaller equality graph and projects every eternal family exactly. In a minimum counterexample, the remainder must also have \(\theta=\gamma\). This supplies a recursive family of clique and common-neighborhood constraints that is now the main candidate for a universal contradiction. The order-13 templates remain a bounded fallback and a source of human-readable lemmas rather than the campaign's definition of success.
What the proof-first pivot has established
The first universal passes did not resolve the conjecture, but they produced independently checked structural results rather than only failed sketches.
- Restoration and Hall obstruction. In a candidate with \(k=\alpha\), fix a maximum independent \(k\)-guard state. If an eternal \(k\)-family exists, its legal one-guard replacement lists satisfy Hall's inequality on every independent outside set. A Hall violation is therefore a compact certificate that \(\gamma^\infty>\alpha\).
- Exact shared-response core. Private neighborhoods are already cliques. The unresolved vertices form a constrained response-list coloring problem; a compatible coloring is exactly the missing \(k\)-clique partition. Collision-transfer and minimal-core lemmas sharply restrict any obstruction, but do not yet eliminate it.
- Frozen-color induction. Starting from \(\gamma=\gamma^\infty=k\), freeze one guard and keep precisely the attacks whose response lists omit that guard. The retained family becomes a genuine one-fewer-guard eternal family on an induced graph with \(\gamma=\alpha=\gamma^\infty=k-1\). At \(k=3\), the proved parameter-two case makes every such complement projection bipartite. This rules out the previously live odd-cycle core with a common two-color list.
- Cross-state covariance. Every ordering of the target positions between two independent family states has a supported monotone one-guard path. Across states sharing two guards, the exchanged-vertex transposition transports every family-response list exactly. Closed paths preserve the response-incidence system, although the resulting permutation need not be trivial.
- Two stress-test families resolved. Complements of line graphs of triangle-free cubic class-II graphs satisfy \(i=\alpha=\gamma^\infty=3<\theta=4\) but have \(\gamma=2\). The 27-vertex Schläfli graph instead satisfies \(\gamma=i=\alpha=3<\theta=6\), but every three-guard strategy loses within two attacks. These examples show why both the static equality and the dynamic one-guard condition are essential.
The remaining parameter-three obstruction is now more precise: a mixed three-color cut or high-degree response core whose separately valid two-color projections fail to glue. The exact graph FDzro realizes the smallest mixed path inside a proper eternal three-family, but has \(\gamma=2<\alpha=\gamma^\infty=3\); this proves that the present dynamic lemmas alone cannot close the case. Under the needed equality \(\gamma=3\), the middle path pair forces an external clique of maximum-independent family states with exact response covariance. A lightweight census found no realization in the greatest family of an equality graph through order 9, but that is evidence rather than a theorem.
First 24 hours
- 25 July — model and literature gate. Built two independent one-guard evaluators, proved and adversarially reviewed the core reductions, traced the conjecture's primary-source history, and reproduced the 2022 near-miss catalog.
- 25 July — closest known objects eliminated. Exhaustively checked all one-vertex extensions of the 55 published near misses and the complete one-edge-toggle neighborhood of the deepest survivors; no counterexample appeared.
- 26 July — order 12 closed. Combined certified \(k=3\) and \(k=4\) exclusions with an analytic \(k=5\) argument to establish the order-12 theorem.
- 26 July — first order-13 branch closed. Proved the \(C_{11}\) obstruction and independently certified the \(C_9\) template exclusion, leaving \(C_5,C_7\) at parameter three.
- 26 July — universal-proof pivot. Froze the next finite input without launching it, proved the restoration/Hall and shared-response-core reductions, and converted the Schläfli graph into an exact two-attack stress test.
- 26 July — induction mechanism found. Proved the frozen-color projection and cross-state response covariance, eliminating the common-two-list odd-cycle branch and isolating the mixed three-color core that remains.
The timestamped repository log and live state file are the authoritative sources after this dated snapshot.
Current paper
A Certified Order-Twelve Extension of the \(\gamma\)–\(\theta\) Frontier in One-Guard Eternal Domination presents the complete finite theorem, the structural reductions, certificate architecture, exact hashes, and reproduction instructions.
Only this broader frontier paper is issued as the current publication. The earlier parameter-three manuscript is retained in the source archive as a superseded component draft, not a second paper.
Published context
- William F. Klostermeyer and Gary MacGillivray, “Eternal Dominating Sets in Graphs,” Journal of Combinatorial Mathematics and Combinatorial Computing 68 (2009), 97–111.
- William F. Klostermeyer and C. M. Mynhardt, “Domination, Eternal Domination, and Clique Covering,” Discussiones Mathematicae Graph Theory 35(2) (2015), 283–300.
- Gary MacGillivray, C. M. Mynhardt, and V. Virgile, “Eternal Domination and Clique Covering,” Electronic Journal of Graph Theory and Applications 10(2) (2022), 603–624; arXiv:2110.09732.
- Dmitrii Taletskii, “The Gamma-Theta Conjecture Holds for Planar Graphs,” arXiv:2412.20120 (2024), version 2.
Scope and AI-assistance disclosure
The exploratory mathematics, programs, certificate design, independent-code 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 a complete amateur and cannot independently validate the mathematics. No outside individual was contacted, and no external expert has reviewed this work. Exact verification is evidence about the encoded finite statements; it is not peer review and cannot establish worldwide priority.