theorem-h-orientation / thm-2
Theorem 2
Theorem H by machine-checked certificate on the cubic cells of side 4 to 8, four cells that are not cubic, and their divisors.
Theorem H holds on the cubic cells of side four to eight, and on the cells (3,3,9), (4,4,8), (3,3,12) and (6,6,9), and by Lemma 21 on every cell whose extents divide one of these up to a permutation of the axes.
- Identifier
theorem-h-orientation/thm-2- Kind
- theorem
- Status
- certified a machine-checked proof object (DRAT, LRAT, a CPOG-certified count, Lean, Isabelle) on the cells named in scope.
Theorem 1 applied to the DRAT certificates of Theorem U′ (claims u-prime-certificates-2026-09-27 and u-prime-certificates-2026-10-01).
- Scope
- cubic side 4 to 8; (3,3,9), (4,4,8), (3,3,12), (6,6,9); their divisors
- Depends on
- Theorem 1 (the reduction), form of 30 September 2026, with Lemmas 22 to 25 proved theorem-h-orientation/thm-1
- Theorem U′ certified at the cubic sides four, five and six certified theorem-h-orientation/u-prime-certificates-2026-09-27
- Theorem U′ certified at sides seven and eight and on four cells that are not cubic; the counterexample search certified theorem-h-orientation/u-prime-certificates-2026-10-01
- Lemma 21 (a state repeated periodically) proved theorem-h-orientation/lemma-21
- Used by
- Theorem 24 certified theorem-h-orientation/thm-24
- Theorem H open theorem-h-orientation/thm-h
- Provenance
- Written by: Claude (Fable), main loop
Checked by: no independent checker
Read line by line by a person: no
Status reached: 2026-10-01 - 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)