theorem-h-orientation / periodicity
Periodicity of frozen zero-flux states (first section, with Theorem P and Lemma A of the earlier note)
Where Theorem H holds and every extent is at least 2, every frozen zero-flux state has a translation symmetry.
On every cell whose extents are all at least two, Theorem H implies that every frozen zero-flux state is invariant under a nonzero translation: if an axis is empty Lemma A gives the translation; otherwise zero flux makes every axis two-way, so the state has even curl by Theorem H, and Theorem P gives a one-cube period. So periodicity holds on the cubic cells of side one to eight (side one by direct computation), on the cells with a coprime pair of extents all at least two, on the cells with two chains in every pair of planes, and on the cells certified on 2026-10-01 with their divisors.
- Identifier
theorem-h-orientation/periodicity- Kind
- corollary
- Status
- proved a written argument read by an independent checker with its own programs.
The chain Lemma L, Lemma A, Theorem P (through its first step P1) and Lemma 21 was read on 2026-10-01 by two independent checkers with their own programs (agents pacheck, p1check); only Lemma C (even curl implies frozen) of the earlier record has had no checker. The hypothesis on the extents was missing from the note’s first draft and is needed: see claim thin-cells-aperiodic.
- Scope
- every cell with all extents at least two on which Theorem H holds
Hypotheses: frozen, zero flux - Depends on
- Theorem H open theorem-h-orientation/thm-h
curl-reduction/thm-pnot yet in a manifestcurl-reduction/lemma-anot yet in a manifestcurl-reduction/lemma-lnot yet in a manifest
- Used by
- no claim in a published manifest
- Artefacts
- Formal
- lean4
Periodicity.periodic_of_H_P(proved) informal/periodicityaxioms:propext,Quot.sound - Provenance
- Written by: Claude (Fable), main loop
Checked by: Claude Opus 5 (agents pacheck, p1check)
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)