Positive coefficient cone certificates 1
Abstract
Positive coefficient cone certificates 1
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 (base_K_gt_B).
Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/PolynomialCertificates1.base_K_gt_B
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/PolynomialCertificates1.base_K_gt_B (✓ std3). ∎
Source. Repository-derived.
Commentary.
Consumed in the construction described here, with the exact telescope supplied by Lean.
Theorem 1.2 (base_C_positive).
Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/PolynomialCertificates1.base_C_positive
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/PolynomialCertificates1.base_C_positive (✓ std3). ∎
Source. Repository-derived.
Commentary.
Consumed in the construction described here, with the exact telescope supplied by Lean.
Theorem 1.3 (base_second_slack).
Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/PolynomialCertificates1.base_second_slack
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/PolynomialCertificates1.base_second_slack (✓ std3). ∎
Source. Repository-derived.
Commentary.
Consumed in the construction described here, with the exact telescope supplied by Lean.
Theorem 1.4 (base_M_stock).
Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/PolynomialCertificates1.base_M_stock
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/PolynomialCertificates1.base_M_stock (✓ std3). ∎
Source. Repository-derived.
Commentary.
Consumed in the construction described here, with the exact telescope supplied by Lean.
Theorem 1.5 (base_S3_lower).
Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/PolynomialCertificates1.base_S3_lower
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/PolynomialCertificates1.base_S3_lower (✓ std3). ∎
Source. Repository-derived.
Commentary.
Consumed in the construction described here, with the exact telescope supplied by Lean.
References
- Truth anchor:
D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/PolynomialCertificates1.base_C_positive - Truth anchor:
D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/PolynomialCertificates1.base_K_gt_B - Truth anchor:
D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/PolynomialCertificates1.base_M_stock - Truth anchor:
D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/PolynomialCertificates1.base_S3_lower - Truth anchor:
D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/PolynomialCertificates1.base_second_slack - Dependency: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/Algebra