Positive coefficient cone certificates 3

Abstract

Each displayed endpoint slack is expanded after shifting the declared cone to nonnegative coordinates. Ring verifies the exact rational polynomial identity and positivity verifies every resulting term. The inequalities are universal over the original rational cone and feed the integer adapter used by the small-a selector; numerical sampling is not used.

Theorem 1.1 (first_small_R_lower).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/PolynomialCertificates3.first_small_R_lower

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

Source. Repository-derived.

Commentary.

Consumed in the construction described here, with the exact telescope supplied by Lean.

Theorem 1.2 (first_small_T1_upper).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/PolynomialCertificates3.first_small_T1_upper

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

Source. Repository-derived.

Commentary.

Consumed in the construction described here, with the exact telescope supplied by Lean.