theorem-h-orientation / statement-r-box-lemma
Statement R and its box lemma (Conjecture \(R_b\); Theorem U section, item 8)
A weaker relative of (V): two aligned rods extend to a whole line of their type; its first step certified for \(b\) from 3 to 6.
Two rods of type \(k\) four apart, a lower bridgehead of type \(a\) and the upper bridgehead on the other side not of type \(a\) make the whole line of the rods of type \(k\). Its first step is forced inside a box over one closed transverse circle, \(x \in [-3, 2b + 1]\), \(|z| \leq 2b - 1\), with the \(y\)-circle of the cell whole, whatever \(a\), \(c\) and \(\gcd(b, c)\).
- Identifier
theorem-h-orientation/statement-r-box-lemma- Kind
- conjecture
- Status
- certified a machine-checked proof object (DRAT, LRAT, a CPOG-certified count, Lean, Isabelle) on the cells named in scope.
The box lemma certified by DRAT proofs for \(b = 3, 4, 5, 6\) (hashes in the report); conjectured for every \(b\). R follows from (V) in two lines and is strictly weaker than (V). On 2026-10-01 shown not to be a first step towards (V): it adds exactly one literal to (V) and supplies neither transverse circle (claim closed-r-then-monodromy).
- Scope
- certified for b = 3 to 6 on every cell meeting the box’s bounds; conjectured for all b
- Depends on
- The model (first section; Holes, cages and rods) proved theorem-h-orientation/model
- Used by
- Statement R, a monodromy in the weights, and the heights are not a route to (V) (Theorem U section, item 9) closed-route theorem-h-orientation/closed-r-then-monodromy
- Artefacts
- Provenance
- Written by: Claude Fable 5.1 (agent rodline)
Checked by: no independent checker
Read line by line by a person: no
Status reached: 2026-09-30 - 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)