Geometry

Part of the explicit persistent quartic SOS counterexample.

theorem PersistentSOS.objective_radial_decomposition (σ a b : ℝ) (z : Fin 14 → ℝ) : objective σ a b z = radialValue σ a b (radius z) + b * (radius z ^ 3 - C z)

The objective separates into its radial envelope and a nonnegative cubic deficit.

theorem PersistentSOS.objective_minimizer_radius_iff {σ a b : ℝ} (hσ : 0 < σ) (ha : 0 < a) (hb : 0 < b) (z : Fin 14 → ℝ) : objective σ a b z = minimumValue σ a b ↔ radius z = minimizingRadius σ a b ∧ C z = radius z ^ 3

Equality in the global lower bound requires the unique radial minimum and equality in the sharp cubic bound.

theorem PersistentSOS.objective_all_minimizers {σ a b : ℝ} (hσ : 0 < σ) (ha : 0 < a) (hb : 0 < b) (z : Fin 14 → ℝ) : objective σ a b z = minimumValue σ a b ↔ Q z = minimizingRadius σ a b ^ 2 ∧ (z 1 = 0 ∧ z 2 = 0 ∧ z 3 = 0 ∧ z 4 = 0) ∧ (z 0 = minimizingRadius σ a b ∨ z 0 = -minimizingRadius σ a b / 2)

Complete coordinate description of all global minimizers. Besides the distinguished axis point, they form a sphere in the nine y coordinates at first coordinate -r / 2, with squared radius 3 * r² / 4.