Main

Part of the explicit persistent quartic SOS counterexample.

theorem PersistentSOS.quantitative_sos_gap {σ a b γ : ℝ} (hσ : 0 < σ) (ha : 0 < a) (hsos : IsSOS (quarticPoly σ a b - MvPolynomial.C γ)) : γ ≤ minimumValue σ a b - b * separation * minimizingRadius σ a b ^ 3

Every ordinary polynomial SOS lower bound satisfies the displayed quantitative bound.

theorem PersistentSOS.quantitative_sos_strict {σ a b γ : ℝ} (hσ : 0 < σ) (ha : 0 < a) (hb : 0 < b) (hsos : IsSOS (quarticPoly σ a b - MvPolynomial.C γ)) : γ < minimumValue σ a b

A strict gap holds for every positive regularization parameter and every positive fixed quadratic and cubic strength.

theorem PersistentSOS.minimum_shift_not_sos {σ a b : ℝ} (hσ : 0 < σ) (ha : 0 < a) (hb : 0 < b) : ¬IsSOS (quarticPoly σ a b - MvPolynomial.C (minimumValue σ a b))

The exact minimum shift is not a finite sum of squares of real polynomials.

theorem PersistentSOS.minimum_shift_nonnegative {σ a b : ℝ} (hσ : 0 < σ) (ha : 0 < a) (hb : 0 < b) (z : Fin 14 → ℝ) : 0 ≤ (MvPolynomial.eval z) (quarticPoly σ a b - MvPolynomial.C (minimumValue σ a b))

The exact minimum shift is globally nonnegative.

theorem PersistentSOS.persistent_failure {σ a b : ℝ} (hσ : 0 < σ) (ha : 0 < a) (hb : 0 < b) : (∀ (z : Fin 14 → ℝ), minimumValue σ a b ≤ objective σ a b z) ∧ objective σ a b (axis (minimizingRadius σ a b)) = minimumValue σ a b ∧ ¬IsSOS (quarticPoly σ a b - MvPolynomial.C (minimumValue σ a b))

Explicit persistent failure, including actual global optimality and attainment.

theorem PersistentSOS.sphere_moment_gap : ∃ (L : Poly →ₗ[ℝ] ℝ), L 1 = 1 ∧ L qPoly = 1 ∧ L (qPoly ^ 2) = 1 ∧ (∀ (h : Poly), MvPolynomial.totalDegree h ≤ 2 → 0 ≤ L (h ^ 2)) ∧ (∀ (h : Poly), MvPolynomial.totalDegree h ≤ 2 → L ((qPoly - 1) * h) = 0) ∧ L cubicPoly = 500753357629 / 500000000000

The finite certificate is a functional on ordinary real polynomials, positive on every quadratic square, with normalized radial moments and a strict cubic gap.