Stage 8: the canonical Euclidean estimate potential

This module gives the literal finite-dimensional quadratic potential used in Phase A of the Euclidean branch. Its minimizer and exact strong lower bound are derived from the project's explicit lpNorm 2; no ambient-norm shortcut or minimizer certificate is used.

noncomputable def O3.Stage8EuclideanMinimizer.euclideanPsi (M : ℝ) {d : ℕ} (x₀ s : Point d) (c : ℝ) (x : Point d) : ℝ

The canonical representation of the recursive Euclidean estimate potential. The vector s is the accumulated weighted gradient and c contains the accumulated affine offsets.

Equations

• O3.Stage8EuclideanMinimizer.euclideanPsi M x₀ s c x = M / 2 * O3.lpNorm 2 (x - x₀) ^ 2 + c + O3.pairing s (x - x₀)

noncomputable def O3.Stage8EuclideanMinimizer.euclideanPsiMinimizer (M : ℝ) {d : ℕ} (x₀ s : Point d) : Point d

The explicit minimizer x₀ - M⁻¹ s of the canonical potential.

Equations

• O3.Stage8EuclideanMinimizer.euclideanPsiMinimizer M x₀ s = x₀ - M⁻¹ • s

theorem O3.Stage8EuclideanMinimizer.lpNorm_two_sq_sub_decomposition {d : ℕ} (x z x₀ : Point d) : lpNorm 2 (x - x₀) ^ 2 = lpNorm 2 (z - x₀) ^ 2 + 2 * pairing (z - x₀) (x - z) + lpNorm 2 (x - z) ^ 2

Polarization for the literal O3 lpNorm 2.

theorem O3.Stage8EuclideanMinimizer.pairing_sub_decomposition {d : ℕ} (s x z x₀ : Point d) : pairing s (x - x₀) = pairing s (z - x₀) + pairing s (x - z)

Affine displacement identity for the coordinate pairing.

theorem O3.Stage8EuclideanMinimizer.euclideanPsiMinimizer_firstOrder {M : ℝ} (hM : M ≠ 0) {d : ℕ} (x₀ s : Point d) : M • (euclideanPsiMinimizer M x₀ s - x₀) + s = 0

The explicit point satisfies the exact first-order cancellation equation.

theorem O3.Stage8EuclideanMinimizer.euclideanPsiMinimizer_pairing_cancel {M : ℝ} (hM : M ≠ 0) {d : ℕ} (x₀ s x : Point d) : M * pairing (euclideanPsiMinimizer M x₀ s - x₀) (x - euclideanPsiMinimizer M x₀ s) + pairing s (x - euclideanPsiMinimizer M x₀ s) = 0

Pairing form of the first-order cancellation, used by the exact square completion.

theorem O3.Stage8EuclideanMinimizer.euclideanPsi_eq_min_add_sq {M : ℝ} (hM : M ≠ 0) {d : ℕ} (x₀ s : Point d) (c : ℝ) (x : Point d) : euclideanPsi M x₀ s c x = euclideanPsi M x₀ s c (euclideanPsiMinimizer M x₀ s) + M / 2 * lpNorm 2 (x - euclideanPsiMinimizer M x₀ s) ^ 2

Exact completion-of-the-square identity. This is stronger than the needed lower bound and exposes the precise M / 2 coefficient.

theorem O3.Stage8EuclideanMinimizer.euclideanPsi_strongLower_at_minimizer {M : ℝ} (hM : 0 < M) {d : ℕ} (x₀ s : Point d) (c : ℝ) (x : Point d) : euclideanPsi M x₀ s c x ≥ euclideanPsi M x₀ s c (euclideanPsiMinimizer M x₀ s) + M / 2 * lpNorm 2 (x - euclideanPsiMinimizer M x₀ s) ^ 2

Exact M-strong lower bound at the explicit minimizer.

theorem O3.Stage8EuclideanMinimizer.euclideanPsiMinimizer_isMin {M : ℝ} (hM : 0 < M) {d : ℕ} (x₀ s : Point d) (c : ℝ) (x : Point d) : euclideanPsi M x₀ s c (euclideanPsiMinimizer M x₀ s) ≤ euclideanPsi M x₀ s c x

Genuine global minimality of the explicit point.

theorem O3.Stage8EuclideanMinimizer.euclideanPsi_add_linearization {M a fy : ℝ} {d : ℕ} (x₀ s g y : Point d) (c : ℝ) (x : Point d) : euclideanPsi M x₀ s c x + a * (fy + pairing g (x - y)) = euclideanPsi M x₀ (s + a • g) (c + a * (fy + pairing g (x₀ - y))) x

Adding one weighted oracle linearization preserves the canonical form, with the accumulated gradient and affine constant updated exactly.