ResidueCertificates1

Abstract

ResidueCertificates1

The first eight residue rows satisfy every old and new head window and stock bound for every nonnegative integer R. Exact polynomial identities and binary low-bit certificates establish uniformity beyond any exponent cutoff.

Theorem 1.1 (residue_bounds_0).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates1.residue_bounds_0

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

Source. Repository-derived.

Commentary.

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

Theorem 1.2 (residue_submask_0).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates1.residue_submask_0

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

Source. Repository-derived.

Commentary.

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

Theorem 1.3 (residue_bounds_1).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates1.residue_bounds_1

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

Source. Repository-derived.

Commentary.

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

Theorem 1.4 (residue_submask_1).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates1.residue_submask_1

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

Source. Repository-derived.

Commentary.

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

Theorem 1.5 (residue_bounds_2).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates1.residue_bounds_2

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

Source. Repository-derived.

Commentary.

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

Theorem 1.6 (residue_submask_2).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates1.residue_submask_2

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

Source. Repository-derived.

Commentary.

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

Theorem 1.7 (residue_bounds_3).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates1.residue_bounds_3

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

Source. Repository-derived.

Commentary.

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

Theorem 1.8 (residue_submask_3).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates1.residue_submask_3

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

Source. Repository-derived.

Commentary.

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

Theorem 1.9 (residue_bounds_4).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates1.residue_bounds_4

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

Source. Repository-derived.

Commentary.

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

Theorem 1.10 (residue_submask_4).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates1.residue_submask_4

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

Source. Repository-derived.

Commentary.

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

Theorem 1.11 (residue_bounds_5).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates1.residue_bounds_5

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

Source. Repository-derived.

Commentary.

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

Theorem 1.12 (residue_submask_5).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates1.residue_submask_5

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

Source. Repository-derived.

Commentary.

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

Theorem 1.13 (residue_bounds_6).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates1.residue_bounds_6

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

Source. Repository-derived.

Commentary.

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

Theorem 1.14 (residue_submask_6).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates1.residue_submask_6

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

Source. Repository-derived.

Commentary.

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

Theorem 1.15 (residue_bounds_7).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates1.residue_bounds_7

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

Source. Repository-derived.

Commentary.

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

Theorem 1.16 (residue_submask_7).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates1.residue_submask_7

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

Source. Repository-derived.

Commentary.

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

References