Positive coefficient cone certificates 4

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 (tail_R16).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/PolynomialCertificates4.tail_R16

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

Source. Repository-derived.

Commentary.

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

Theorem 1.2 (tail_R16q4).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/PolynomialCertificates4.tail_R16q4

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

Source. Repository-derived.

Commentary.

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