ResidueCertificates2

Abstract

ResidueCertificates2

The middle eight residue rows satisfy the paired physical windows and natural binary submask condition for every nonnegative R. The same physical parameters feed the old and the charged new source.

Theorem 1.1 (residue_bounds_8).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates2.residue_bounds_8

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

Source. Repository-derived.

Commentary.

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

Theorem 1.2 (residue_submask_8).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates2.residue_submask_8

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

Source. Repository-derived.

Commentary.

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

Theorem 1.3 (residue_bounds_9).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates2.residue_bounds_9

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

Source. Repository-derived.

Commentary.

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

Theorem 1.4 (residue_submask_9).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates2.residue_submask_9

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

Source. Repository-derived.

Commentary.

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

Theorem 1.5 (residue_bounds_10).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates2.residue_bounds_10

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

Source. Repository-derived.

Commentary.

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

Theorem 1.6 (residue_submask_10).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates2.residue_submask_10

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

Source. Repository-derived.

Commentary.

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

Theorem 1.7 (residue_bounds_11).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates2.residue_bounds_11

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

Source. Repository-derived.

Commentary.

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

Theorem 1.8 (residue_submask_11).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates2.residue_submask_11

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

Source. Repository-derived.

Commentary.

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

Theorem 1.9 (residue_bounds_12).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates2.residue_bounds_12

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

Source. Repository-derived.

Commentary.

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

Theorem 1.10 (residue_submask_12).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates2.residue_submask_12

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

Source. Repository-derived.

Commentary.

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

Theorem 1.11 (residue_bounds_13).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates2.residue_bounds_13

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

Source. Repository-derived.

Commentary.

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

Theorem 1.12 (residue_submask_13).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates2.residue_submask_13

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

Source. Repository-derived.

Commentary.

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

Theorem 1.13 (residue_bounds_14).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates2.residue_bounds_14

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

Source. Repository-derived.

Commentary.

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

Theorem 1.14 (residue_submask_14).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates2.residue_submask_14

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

Source. Repository-derived.

Commentary.

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

Theorem 1.15 (residue_bounds_15).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates2.residue_bounds_15

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

Source. Repository-derived.

Commentary.

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

Theorem 1.16 (residue_submask_15).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/ResidueCertificates2.residue_submask_15

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

Source. Repository-derived.

Commentary.

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

References