TableData
Abstract
TableData
The literal 24 mod-72 residue rows cover h=1,2 and p=4,8. The late fresh ear occurs exactly for p=4,h=1,r=56; all other rows insert at cut zero. The paired rowBounds retain the common physical interpretation used by the unbounded selectors.
Theorem 1.1 (residue_fresh_exact).
Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/TableData.residue_fresh_exact
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/TableData.residue_fresh_exact (✓ std3). ∎
Source. Repository-derived.
Commentary.
Consumed by the full HighD construction with the exact Lean telescope.