theorem-h-orientation / u-prime-certificates-2026-09-27
Theorem U′ certified at the cubic sides four, five and six
DRAT proofs that an unoriented hole forces even curl, on the cubic cells of side 4, 5 and 6.
Theorem U′: a state of the type model with a hole whose rods are both of type \(k\), one bridgehead of type \(a\) on its lower side and one of type \(b\) on its upper side, has even curl on every hexagon. Certified on the cubic cells of side 4, 5 and 6 by DRAT proofs checked by drat-trim: 16, 16 and 4 formulas (at side six the sixteen hypotheses form one orbit of the formula’s symmetries), each with a satisfiable control whose witness was decoded and checked.
- Identifier
theorem-h-orientation/u-prime-certificates-2026-09-27- 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.
114 formulas in all with the diagonal and line laws; longest solve 22 s; proofs 36 to 385 MB; hashes and verdicts kept, files regenerable.
- Scope
- cubic side 4, 5, 6
- 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/h28x_results.jsonlRegenerate:cd experiments/08_frozen_structure/scratch_h && h282_certify.py - ledger
certificates/h28x_sha256_2026-09-27.txt - report
reports/2026-09-27-opus-cert.md
- ledger
- Provenance
- Written by: Claude Opus 5 (agent cert)
Checked by: Claude Opus 5 (agent check3): symmetry orbit and encoding
Read line by line by a person: no
Status reached: 2026-09-27 - 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)