theorem-h-orientation / thm-1

Theorem 1 (the reduction), form of 30 September 2026, with Lemmas 22 to 25

The reduction: on every cell, Theorem U implies Theorem H.

On every cell, Theorem U implies Theorem H.

Identifier

theorem-h-orientation/thm-1

Kind

theorem

Status

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

Written argument: with every hole oriented, Theorem 6 makes the line count of a two-way type a function of one transverse coordinate on each sublattice, Theorem 3 makes the two sublattices share that coordinate, Theorem 15 kills one profile per two-way axis so that with three two-way axes some axis has a constant line count on both sublattices, and the diagonal law along the connected graph of lines makes that axis one-way. Re-derived by the main loop, then read by an independent checker with its own programs (agent check10), which confirmed it with five corrections of wording and no gap; its one prediction about odd states tested on the corpus with no exception.

Scope

every cell
Hypotheses: frozen, odd, every hole oriented (which Theorem U supplies)

Depends on

Theorem M′ (from the project’s earlier record) proved theorem-h-orientation/thm-m-prime
Law C, law \(P^k\), Lemmas 1 to 3 (the cage laws) proved theorem-h-orientation/cage-laws
Theorem 3 (the diagonal law) proved theorem-h-orientation/thm-3-diagonal-law
Theorems 4 to 8 (line counts, two separable functions with product zero, walls, uniform chains beside a wall) proved theorem-h-orientation/thm-6-separability
Theorem 15 proved theorem-h-orientation/thm-15
The parametrisation (C) (completeness of the chain modes) proved theorem-h-orientation/parametrisation-c
Lemma 21 (a state repeated periodically) proved theorem-h-orientation/lemma-21

Used by

Theorem 2 certified theorem-h-orientation/thm-2
Theorem H open theorem-h-orientation/thm-h

Supersedes

Theorem 1, first form (27 September 2026), through K_u proved theorem-h-orientation/thm-1-first-form

Artefacts

report reports/2026-09-30-fable-zeroflux.md
report reports/2026-09-30-opus-check10.md
script experiments/08_frozen_structure/scratch_h/h600_stripes.py (in the private repository; not published)
scripts h600 to h605 (author) and h670 to h672 (checker)

Formal

lean4 Periodicity.theorem1 (stated) in formal/periodicity

Provenance

Written by: Claude Fable 5.1 (agent zeroflux)
Checked by: Claude Opus 5 (agent check10), own programs
Read line by line by a person: no
Status reached: 2026-09-30
Project log: LOG.md, entries of 2026-09-30 (zeroflux, check10)

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)