Unique Geometry

Part of the explicit persistent quartic SOS counterexample.

theorem PersistentSOS.unique_cubic_eq (z : Fin 14 → ℝ) : uniqueCubic z = (1000 * C z + z 0 * Q z) / 1001

The selected cubic is the explicit convex combination of the original cubic and the first coordinate times the squared Euclidean norm.

theorem PersistentSOS.unique_objective_eq (σ a b : ℝ) (z : Fin 14 → ℝ) : uniqueObjective σ a b z = σ / 4 * Q z ^ 2 - a / 2 * Q z - b * uniqueCubic z

The selected quartic is evaluated on ordinary real vectors.

theorem PersistentSOS.coordinate_abs_le_radius (z : Fin 14 → ℝ) (i : Fin 14) : |z i| ≤ radius z

Every coordinate has absolute value bounded by the Euclidean radius.

theorem PersistentSOS.Q_sub_axis (z : Fin 14 → ℝ) (r : ℝ) : (Q fun (i : Fin 14) => z i - axis r i) = Q z - 2 * r * z 0 + r ^ 2

Squared distance to a point on the distinguished axis.

theorem PersistentSOS.eq_axis_of_first_eq_radius (z : Fin 14 → ℝ) (h : z 0 = radius z) : z = axis (radius z)

Equality of the first coordinate with the radius forces all transverse coordinates to vanish.

theorem PersistentSOS.unique_cubic_deficit (z : Fin 14 → ℝ) : radius z ^ 3 - uniqueCubic z = (1000 * (radius z ^ 3 - C z) + radius z ^ 2 * (radius z - z 0)) / 1001

The deficit separates into two nonnegative terms.

theorem PersistentSOS.unique_cubic_le (z : Fin 14 → ℝ) : uniqueCubic z ≤ radius z ^ 3

The original sharp bound and a coordinate bound give the same upper bound for the selected cubic.

theorem PersistentSOS.unique_cubic_scale (z : Fin 14 → ℝ) (r : ℝ) : (uniqueCubic fun (i : Fin 14) => r * z i) = r ^ 3 * uniqueCubic z

The selected cubic remains homogeneous of degree three.

theorem PersistentSOS.unique_cubic_neg (z : Fin 14 → ℝ) : (uniqueCubic fun (i : Fin 14) => -z i) = -uniqueCubic z

theorem PersistentSOS.radius_neg (z : Fin 14 → ℝ) : (radius fun (i : Fin 14) => -z i) = radius z

theorem PersistentSOS.unique_cubic_abs_le (z : Fin 14 → ℝ) : |uniqueCubic z| ≤ radius z ^ 3

The selected cubic has the sharp global homogeneous bound.

@[simp]

theorem PersistentSOS.unique_cubic_axis (r : ℝ) : uniqueCubic (axis r) = r ^ 3

theorem PersistentSOS.unique_cubic_upper_equality (z : Fin 14 → ℝ) : uniqueCubic z = radius z ^ 3 ↔ z = axis (radius z)

Equality in the upper cubic bound occurs exactly on the nonnegative part of the distinguished coordinate axis, including the origin.

theorem PersistentSOS.unique_cubic_unit_maximizer (z : Fin 14 → ℝ) (hQ : Q z = 1) : uniqueCubic z = 1 ↔ z = axis 1

The selected cubic attains its unit - sphere maximum only at the first coordinate unit vector.

theorem PersistentSOS.unique_objective_radial_decomposition (σ a b : ℝ) (z : Fin 14 → ℝ) : uniqueObjective σ a b z = radialValue σ a b (radius z) + b * (radius z ^ 3 - uniqueCubic z)

Decomposition into the radial envelope and the selected cubic deficit.

theorem PersistentSOS.unique_objective_global_lower_bound {σ a b : ℝ} (hσ : 0 < σ) (ha : 0 < a) (hb : 0 < b) (z : Fin 14 → ℝ) : minimumValue σ a b ≤ uniqueObjective σ a b z

Global optimality for every positive real regularization, quadratic strength and cubic strength.

theorem PersistentSOS.unique_objective_axis_attainment {σ a b : ℝ} (hσ : 0 < σ) (ha : 0 < a) : uniqueObjective σ a b (axis (minimizingRadius σ a b)) = minimumValue σ a b

The distinguished point attains the explicit minimum.

theorem PersistentSOS.unique_objective_minimizer {σ a b : ℝ} (hσ : 0 < σ) (ha : 0 < a) (hb : 0 < b) (z : Fin 14 → ℝ) : uniqueObjective σ a b z = minimumValue σ a b ↔ z = axis (minimizingRadius σ a b)

The global minimizer is unique for every positive choice of all three real parameters.