\(K_u\) (a uniform chain forces a direction to be absent)

A chain with a single moment forces some direction to be absent; no longer used by any proof.

A chain of one moment forces a direction to be absent. Certified within its recorded scope (chains of an axis whose two transverse extents have greatest common divisor at most two); its first step on the whole slab certified on the cubic cells of side four to eight; its later steps hold on every cell.

Identifier

theorem-h-orientation/ku

Kind

fact

Status

certified a machine-checked proof object (DRAT, LRAT, a CPOG-certified count, Lean, Isabelle) on the cells named in scope.

No longer a step of any proof in the note since 30 September 2026. A checker found a gap in its original form on cubic cells (27 September), closed by the whole-slab certificates. Given orientation, its first step has a hand proof uniform in the side (claim ku-first-step-hand).

Scope

as stated

Depends on

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

Used by

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

Artefacts

ledger certificates/h28x_results.jsonl
the first-step certificates are in the same ledger

Provenance

Written by: Claude (Fable and Opus 5), 11 to 27 September 2026
Checked by: Claude Opus 5 (agents check5, check6)
Read line by line by a person: no
Status reached: 2026-09-27

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)