Finite Euclidean phase data, guard schedules, and the two-phase local trial contract.

structure V7.EuclideanGapData (d m : ℕ) : Type

Instance, coefficients, iterates, and observations of the Euclidean gap-reduction phase.

• x0 : Point d

  The starting point of the Euclidean phase.

• inst : PositiveInstance 2 d self.x0

  The positive secant instance governing the objective and oracle.

• M : ℝ

  The smoothness estimate used by the phase.

• D : ℝ

  The radius estimate used to bound the initial distance to a minimizer.

• A : ℕ → ℝ

  The cumulative estimate-sequence weights.

• a : ℕ → ℝ

  The increments of the estimate-sequence weights.

• x : ℕ → Point d

  The accelerated primal iterates.

• w : ℕ → Point d

  The minimizers of the accumulated quadratic estimate potentials.

• y : ℕ → Point d

  The interpolated oracle query points.

• trace : List (Observation d)

  The chronological oracle observations of the Euclidean phase.

def V7.EuclideanGapDynamics {d m : ℕ} (data : EuclideanGapData d m) : Prop

The initial state, coefficient equations, and accelerated Euclidean update recurrences.

Equations

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

def V7.EuclideanGapAssumptions {d m : ℕ} (data : EuclideanGapData d m) : Prop

The Euclidean dynamics, radius bound, accepted models, and exact observation trace.

Equations

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

noncomputable def V7.EuclideanGapStatement : Prop

Source carrier for lem:euclideangap (E01).

Equations

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

structure V7.OGMGData (d n : ℕ) : Type

Oracle, coefficients, iterates, and observations of a finite OGM-G execution.

• oracle : PairOracle d

  The value-gradient oracle queried by OGM-G.

• M : ℝ

  The smoothness estimate scaling the OGM-G gradient steps.

• fstar : ℝ

  The proposed minimum objective value.

• U : Point d

  The starting point of the OGM-G phase.

• theta : ℕ → ℝ

  The backward momentum coefficient sequence.

• u : ℕ → Point d

  The OGM-G query iterates.

• v : ℕ → Point d

  The gradient-step points computed from the query iterates.

• vMinusOne : Point d

  The previous gradient-step point before iteration zero.

• trace : List (Observation d)

  The chronological oracle observations of the OGM-G phase.

def V7.OGMGDynamics {d n : ℕ} (data : OGMGData d n) : Prop

The backward coefficient equations, initial state, and literal OGM-G update recurrences.

Equations

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

def V7.OGMGAssumptions {d n : ℕ} (data : OGMGData d n) : Prop

The OGM-G dynamics, convex gradient oracle, attained minimum, guards, and exact trace.

Equations

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

noncomputable def V7.FiniteDataOGMGStatement : Prop

Source carrier for lem:ogmg (E02).

Equations

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

def V7.euclideanPlannedTrace {d : ℕ} {x0 : Point d} {m n : ℕ} (inst : PositiveInstance 2 d x0) (phaseA : EuclideanGapData d m) (phaseB : OGMGData d n) : List (Observation d)

The prescribed observation list for the Euclidean gap and OGM-G phases.

Equations

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

def V7.exactGuardCheck {d : ℕ} (kind : ObservableGuardKind) (oracle : PairOracle d) (x y : Point d) : ObservableGuardCheck d

A guard check formed from the exact oracle observations at its two points.

Equations

• V7.exactGuardCheck kind oracle x y = { kind := kind, xPair := O3.PairOracle.observe oracle x, yPair := O3.PairOracle.observe oracle y }

def V7.euclideanGuardSchedule {d : ℕ} {x0 : Point d} {m n : ℕ} (inst : PositiveInstance 2 d x0) (phaseA : EuclideanGapData d m) (phaseB : OGMGData d n) : List (ObservableGuardCheck d)

The upper-model, interpolation, and terminal-descent checks of a Euclidean trial.

Equations

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

def V7.EuclideanScaleTraceStopsAtFailure {d : ℕ} {x0 : Point d} {m n : ℕ} (inst : PositiveInstance 2 d x0) (report : TrialReport d) (phaseA : EuclideanGapData d m) (phaseB : OGMGData d n) : Prop

The Euclidean trial stops at the query that makes its first failed guard checkable. Phase-A upper-model checks are made after each two-query step; the ordered interpolation ledger is checked after u_n and before the separate terminal-descent query at v_n.

Equations

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

def V7.EuclideanTrialOperationalContract {d m n : ℕ} (x0 : Point d) (M D : ℝ) (inst : PositiveInstance 2 d x0) (report : TrialReport d) (phaseA : EuclideanGapData d m) (phaseB : OGMGData d n) : Prop

The linked Euclidean phases, guard schedule, and chronological trial report contract.

Equations

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

noncomputable def V7.EuclideanTrialStatement : Prop

Source carrier for prop:euclideantrial (E03), retaining the exact 2m+n+1 accounting and the distinct terminal descent query.

Equations

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