Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

TableCertificates

Abstract

TableCertificates

The 24 residue families supply exact paired windows, stock limits and actual natural submasks. These rows are consumed by the unrestricted HighD selector.

Theorem 1.1 (residue_bounds).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/TableCertificates.residue_bounds

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/TableCertificates.residue_bounds (✓ std3). ∎

Source. Repository-derived.

Commentary.

Consumed by the full HighD construction with the exact Lean telescope.

Theorem 1.2 (residue_submask).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/TableCertificates.residue_submask

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/TableCertificates.residue_submask (✓ std3). ∎

Source. Repository-derived.

Commentary.

Consumed by the full HighD construction with the exact Lean telescope.

References