theorem-h-orientation / thm-24
Theorem 24
Theorem H on the small cubic cells of side 1 to 3, deduced from side 6.
Theorem H holds on the cubic cells of side one, two and three.
- Identifier
theorem-h-orientation/thm-24- Kind
- theorem
- Status
- certified a machine-checked proof object (DRAT, LRAT, a CPOG-certified count, Lean, Isabelle) on the cells named in scope.
By Lemma 21 and Theorem 2 at side six.
- Scope
- cubic side 1, 2, 3
- Depends on
- Lemma 21 (a state repeated periodically) proved theorem-h-orientation/lemma-21
- Theorem 2 certified theorem-h-orientation/thm-2
- Used by
- Theorem H open theorem-h-orientation/thm-h
- Provenance
- Written by: Claude (Fable), main loop
Checked by: Claude Opus 5 (agent pacheck): Lemma 21 re-tested with own code
Read line by line by a person: no
Status reached: 2026-09-28 - 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)