The same moment certificate separates a cubic with a unique maximizer

No new moment data are required. The existing sphere localizer identifies L(tQ) with L(t), giving a positive exact gap for the selected cubic. The ordinary SOS degree bridge then transfers that gap at every positive regularization parameter.

theorem PersistentSOS.moment_first_coordinate : sphereFunctional (MvPolynomial.X 0) = 423308963 / 1000000000

The exact first - coordinate moment from the retained rational certificate.

theorem PersistentSOS.moment_first_coordinate_q : sphereFunctional (MvPolynomial.X 0 * qPoly) = 423308963 / 1000000000

Multiplication by the sphere equation preserves the first - coordinate moment.

theorem PersistentSOS.unique_moment_C_mul (c : ℝ) (p : Poly) : sphereFunctional (MvPolynomial.C c * p) = c * sphereFunctional p

Constants act by ordinary scalar multiplication under the moment functional.

theorem PersistentSOS.uniqueSeparation_pos : 0 < uniqueSeparation

The separation for the selected cubic is strictly positive.

theorem PersistentSOS.moment_unique_cubic : sphereFunctional uniqueCubicPoly = 1 + uniqueSeparation

The exact gap for the selected cubic, using the unchanged functional.

theorem PersistentSOS.moment_unique_cubic_exact : sphereFunctional uniqueCubicPoly = 143132860603 / 143000000000

The selected cubic's exact rational moment value.

theorem PersistentSOS.moment_unique_cubic_gt_one : 1 < sphereFunctional uniqueCubicPoly

The selected cubic still exceeds its unit - sphere bound under the functional.

@[simp]

theorem PersistentSOS.scalePoly_uniqueCubicPoly (r : ℝ) : (scalePoly r) uniqueCubicPoly = MvPolynomial.C (r ^ 3) * uniqueCubicPoly

Common scaling respects the degree - three homogeneity of the selected cubic.

theorem PersistentSOS.scalePoly_uniqueQuarticPoly (r σ a b : ℝ) : (scalePoly r) (uniqueQuarticPoly σ a b) = MvPolynomial.C (σ / 4 * r ^ 4) * qPoly ^ 2 - MvPolynomial.C (a / 2 * r ^ 2) * qPoly - MvPolynomial.C (b * r ^ 3) * uniqueCubicPoly

Exact scaling identity for the selected quartic.

theorem PersistentSOS.totalDegree_uniqueCubicPoly_le : MvPolynomial.totalDegree uniqueCubicPoly ≤ 3

The selected polynomial remains a cubic.

theorem PersistentSOS.totalDegree_uniqueQuarticPoly_le (σ a b : ℝ) : MvPolynomial.totalDegree (uniqueQuarticPoly σ a b) ≤ 4

The selected objective has degree at most four.

theorem PersistentSOS.totalDegree_shiftedUniqueQuartic_le (σ a b γ : ℝ) : MvPolynomial.totalDegree (uniqueQuarticPoly σ a b - MvPolynomial.C γ) ≤ 4

Subtracting a real lower bound preserves the selected quartic degree bound.

theorem PersistentSOS.unique_functional_separation (σ a b r γ : ℝ) : sphereFunctional (MvPolynomial.C (σ / 4 * r ^ 4) * qPoly ^ 2 - MvPolynomial.C (a / 2 * r ^ 2) * qPoly - MvPolynomial.C (b * r ^ 3) * uniqueCubicPoly - MvPolynomial.C γ) = radialValue σ a b r - b * uniqueSeparation * r ^ 3 - γ

The scaled functional evaluates the selected quartic shift exactly.

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

Every ordinary SOS lower bound for the selected quartic has the exact gap.

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

The selected cubic gives a strict SOS gap for every positive parameter.

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

The selected quartic's exact minimum shift is not an ordinary polynomial SOS.

theorem PersistentSOS.unique_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 ∧ L (MvPolynomial.X 0) = 423308963 / 1000000000 ∧ L uniqueCubicPoly = 143132860603 / 143000000000

A common ordinary - polynomial functional certifies both exact cubic values, all truncated sphere relations, and positivity on every quadratic square.