ResidueCertificates3

Abstract

ResidueCertificates3

The final eight residue rows complete the mod-72 bank for h=1,2. Polynomial bounds hold for every nonnegative R and preserve the literal fresh charge.

Theorem 1.1 (residue_bounds_16).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates3.residue_bounds_16

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

Source. Repository-derived.

Commentary.

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

Theorem 1.2 (residue_submask_16).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates3.residue_submask_16

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

Source. Repository-derived.

Commentary.

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

Theorem 1.3 (residue_bounds_17).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates3.residue_bounds_17

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

Source. Repository-derived.

Commentary.

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

Theorem 1.4 (residue_submask_17).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates3.residue_submask_17

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

Source. Repository-derived.

Commentary.

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

Theorem 1.5 (residue_bounds_18).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates3.residue_bounds_18

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

Source. Repository-derived.

Commentary.

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

Theorem 1.6 (residue_submask_18).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates3.residue_submask_18

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

Source. Repository-derived.

Commentary.

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

Theorem 1.7 (residue_bounds_19).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates3.residue_bounds_19

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

Source. Repository-derived.

Commentary.

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

Theorem 1.8 (residue_submask_19).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates3.residue_submask_19

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

Source. Repository-derived.

Commentary.

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

Theorem 1.9 (residue_bounds_20).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates3.residue_bounds_20

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

Source. Repository-derived.

Commentary.

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

Theorem 1.10 (residue_submask_20).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates3.residue_submask_20

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

Source. Repository-derived.

Commentary.

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

Theorem 1.11 (residue_bounds_21).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates3.residue_bounds_21

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

Source. Repository-derived.

Commentary.

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

Theorem 1.12 (residue_submask_21).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates3.residue_submask_21

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

Source. Repository-derived.

Commentary.

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

Theorem 1.13 (residue_bounds_22).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates3.residue_bounds_22

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

Source. Repository-derived.

Commentary.

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

Theorem 1.14 (residue_submask_22).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates3.residue_submask_22

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

Source. Repository-derived.

Commentary.

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

Theorem 1.15 (residue_bounds_23).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates3.residue_bounds_23

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

Source. Repository-derived.

Commentary.

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

Theorem 1.16 (residue_submask_23).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates3.residue_submask_23

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

Source. Repository-derived.

Commentary.

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

References