theorem-h-orientation / u-prime-certificates-2026-10-01
Theorem U′ certified at sides seven and eight and on four cells that are not cubic; the counterexample search
The same proofs at cubic sides 7 and 8 and on four cells that are not cubic; run as a search for a counterexample, which found none.
Theorem U′ holds on the cubic cells of side 7 and 8 and on (3,3,9), (4,4,8), (3,3,12) and (6,6,9): 224 whole-torus queries (16 per rod axis: two sublattices, two orders of the transverse types, two positions of each bridgehead; all three axes on the cells that are not cubic, where the forty-eight hypotheses fall into three orbits of the formula’s symmetries), every one unsatisfiable with a satisfiable control; 155 DRAT proofs checked by drat-trim (every query on the three small cells, one per orbit on (6,6,9), one per sublattice and order at sides seven and eight, the cyclic permutation of the axes being a checked automorphism).
- Identifier
theorem-h-orientation/u-prime-certificates-2026-10-01- Kind
- certificate-campaign a family of machine-checked proofs on named cells.
- Status
- certified a machine-checked proof object (DRAT, LRAT, a CPOG-certified count, Lean, Isabelle) on the cells named in scope.
Run as a search for a counterexample to Theorem U; none found and no near miss (controls satisfiable in under 0.5 s, refutations in at most 124 s, solve time growing smoothly with the side). The encoding is clause-for-clause identical to the 27 September encoding on the cubic cells of side four and five, and was tested on odd corpus states repeated onto the new cells. Proofs over 50 MB (to 2.9 GB) deleted after checking and recorded by hash and size. The main loop re-ran sixteen queries and one certificate.
- Scope
- cubic side 7, 8; (3,3,9), (4,4,8), (3,3,12), (6,6,9)
- Depends on
- The model (first section; Holes, cages and rods) proved theorem-h-orientation/model
- Used by
- Theorem 2 certified theorem-h-orientation/thm-2
- Artefacts
- ledger
certificates/h74x_results.jsonlRegenerate:cd experiments/08_frozen_structure/scratch_h && h741_uprime.py 7 7 7 x 0,0,0,0 0,1,0,0 1,0,0,0 1,1,0,0 --drat --cap 1200 --dcap 2400 (and likewise per cell; see the report) - ledger
certificates/h74x_sha256_2026-10-01.txt - report
reports/2026-10-01-opus-falsify.md
- ledger
- Provenance
- Written by: Claude Opus 5 (agent falsify)
Checked by: no independent checker
Read line by line by a person: no
Status reached: 2026-10-01
Project log: LOG.md, entry of 2026-10-01 (falsify) - Source
- Theorem H for frozen pyrochlore ice: proofs on the cells with a coprime pair of extents and on the cells with two chains in every pair of planes, a reduction to Theorem U alone on every cell, and the cubic cells of side one to eight, version 2026-10-01; manifest (JSON)