Stage 8: the guarded Euclidean gap

This module proves the vector estimate-sequence invariant for the actual recursive Phase-A execution and evaluates it at the internally constructed closest optimizer.

theorem O3.euclideanEstimateFunction_le_model {d : ℕ} (P : AdmissibleInstance d 2) {M : ℝ} (_hM : 0 < M) (k : ℕ) (x : Vec d) : euclideanEstimateFunction P M k x ≤ M / 2 * lpNorm 2 (x - P.x0) ^ 2 + euclideanA k * P.f x

The literal recursive potential is bounded by the quadratic prox plus A_k f(x), using convexity at every actual query.

theorem O3.euclideanEstimate_oneStep {d : ℕ} (P : AdmissibleInstance d 2) {M : ℝ} (hM : 0 < M) (k : ℕ) (hprev : euclideanA k * P.f (euclideanEstimateState P M k).accelerated ≤ euclideanEstimateMinimum P M k) (hguard : (euclideanEstimateGuard P M k).Holds) : euclideanA (k + 1) * P.f (euclideanEstimateState P M (k + 1)).accelerated ≤ euclideanEstimateMinimum P M (k + 1)

One accepted actual step closes with exact cancellation a_(k+1)^2=A_(k+1).

theorem O3.euclideanEstimate_potential {d : ℕ} (P : AdmissibleInstance d 2) {M : ℝ} (hM : 0 < M) (m : ℕ) : EuclideanEstimateAccepted P M m → euclideanA m * P.f (euclideanEstimateState P M m).accelerated ≤ euclideanEstimateMinimum P M m

The source vector estimate-sequence invariant on the actual accepted prefix.

def O3.EuclideanGapStatement : Prop

Exact frozen carrier for TeX Lemma lem:euclideangap. The optimizer is proof-side and universally quantified in the conclusion; it is not supplied to the algorithm or used by its recursion.

Equations

• One or more equations did not get rendered due to their size.

theorem O3.euclideanGap : EuclideanGapStatement

Native closure of the guarded Euclidean gap.