Lower Powers of the First Gap
Abstract
The constant and linear coefficients of the septic upper remainder are nonnegative.
Theorem 1.1 (Constant Coefficient).
Lean statement: D5/S3/Zeros/CoefficientBounds/SepticEnvelopeUpperLow.upper_coeff0_nonneg
Proof. Machine-checked in Lean as D5/S3/Zeros/CoefficientBounds/SepticEnvelopeUpperLow.upper_coeff0_nonneg (✓ std3). ∎
Source. Repository-derived.
Commentary.
Write twelve times the septic joint upper remainder as a polynomial in the first root gap. Its constant and linear coefficients have positive expansions with 937 and 687 monomials in the other five gaps. Exact polynomial identities and nonnegativity of the gaps prove both signs for arbitrary real inputs.