The full truncated sphere relation

The sphere relation annihilates every polynomial of degree at most two. This follows from positivity and its zero square, without enumerating individual localizer equations.

theorem PersistentSOS.mul_eq_zero_of_square_eq_zero (L : Poly →ₗ[ℝ] ℝ) (hL : ∀ (p : Poly), MvPolynomial.totalDegree p ≤ 2 → 0 ≤ L (p ^ 2)) (h k : Poly) (hh : MvPolynomial.totalDegree h ≤ 2) (hk : MvPolynomial.totalDegree k ≤ 2) (hk0 : L (k ^ 2) = 0) : L (k * h) = 0

A null square of a positive truncated functional is orthogonal to every other polynomial in its domain of quadratic - square positivity.

theorem PersistentSOS.moment_sphere_relation_square : sphereFunctional ((qPoly - 1) ^ 2) = 0

The sphere relation has zero square under the exact moment functional.

theorem PersistentSOS.moment_sphere_localizer (h : Poly) (hh : MvPolynomial.totalDegree h ≤ 2) : sphereFunctional ((qPoly - 1) * h) = 0

All sphere localizer identities through degree four, for arbitrary quadratic multipliers.