Universal positive polynomial windows
Abstract
Universal positive polynomial windows
For each of twelve residue families, R and U range over all nonnegative integers; for each of eight boundary families, U ranges over all nonnegative integers. Ring proves 340 exact identities. Nonnegative coefficients prove the twelve old/new window inequalities, the v and M stocks, and strict mask separation. These identities use the actual HighD rowBounds, including the fresh charge, and contain no exponent cutoff or finite-grid inference.
Theorem 1.1 (residue_bounds).
Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/SmallAAllHCertificates.residue_bounds
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/SmallAAllHCertificates.residue_bounds (✓ std3). ∎
Source. Repository-derived.
Commentary.
Consumed in the construction described here, with the exact telescope supplied by Lean.
Theorem 1.2 (fixed_bounds).
Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/SmallAAllHCertificates.fixed_bounds
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/SmallAAllHCertificates.fixed_bounds (✓ std3). ∎
Source. Repository-derived.
Commentary.
Consumed in the construction described here, with the exact telescope supplied by Lean.