Lemma 21 (a state repeated periodically)

Repeating a state onto a larger cell keeps it frozen and odd, so Theorem H passes from a cell to its divisors.

A frozen state of the cell \((a, b, c)\), repeated periodically, is a frozen state of the cell \((k_1 a, k_2 b, k_3 c)\) for any positive integers \(k_1, k_2, k_3\); it has an odd hexagon exactly when the original has, and the same set of moments. So Theorem H on the larger cell implies Theorem H on the smaller.

Identifier

theorem-h-orientation/lemma-21

Kind

lemma

Status

proved a written argument read by an independent checker with its own programs.

Written by the main session and tested exactly on 765 repeated states; on 2026-10-01 read by an independent checker (agent pacheck) with its own code on eight pairs of cells with unequal multipliers, 0 violations; the direction Theorem 24 uses confirmed sound.

Scope

every cell

Depends on

The model (first section; Holes, cages and rods) proved theorem-h-orientation/model

Used by

Theorem 1 (the reduction), form of 30 September 2026, with Lemmas 22 to 25 proved theorem-h-orientation/thm-1
Theorem 2 certified theorem-h-orientation/thm-2
Theorem 24 certified theorem-h-orientation/thm-24

Artefacts

report reports/2026-10-01-opus-pacheck.md
lean formal/periodicity/Periodicity/Lift.lean
Regenerate: cd formal/periodicity && lake build && lake env lean Axioms.lean
script experiments/08_frozen_structure/scratch_h/h736_lift.py (in the private repository; not published)

Formal

lean4 Periodicity.lemma21 (proved) in formal/periodicity axioms: propext, Quot.sound

Provenance

Written by: Claude (Fable), main loop
Checked by: Claude Opus 5 (agent pacheck)
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)