Unique Main

Part of the explicit persistent quartic SOS counterexample.

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

The selected quartic's exact minimum shift is globally nonnegative.

theorem PersistentSOS.unique_persistent_failure {σ a b : ℝ} (hσ : 0 < σ) (ha : 0 < a) (hb : 0 < b) : (∀ (z : Fin 14 → ℝ), minimumValue σ a b ≤ uniqueObjective σ a b z) ∧ (∀ (z : Fin 14 → ℝ), uniqueObjective σ a b z = minimumValue σ a b ↔ z = axis (minimizingRadius σ a b)) ∧ (Matrix.PosDef fun (i j : Fin 14) => (MvPolynomial.eval (axis (minimizingRadius σ a b))) ((MvPolynomial.pderiv j) ((MvPolynomial.pderiv i) (uniqueQuarticPoly σ a b)))) ∧ ¬IsSOS (uniqueQuarticPoly σ a b - MvPolynomial.C (minimumValue σ a b))

Persistent ordinary - SOS failure with a unique global minimizer and positive - definite Hessian there, for every positive real parameter.