Stage 9: actual finite-data OGM-G execution

This module implements the literal deterministic recursion from TeX Lemma lem:ogmg. It contains no convergence conclusion and no algebraic certificate: its only job is to expose the actual queried data, the complete ordered-pair interpolation checks, and the final descent query.

The phase-B trace deliberately omits u₀ = U, which is reused from Phase A, and contains exactly the newly queried points u₁, …, uₙ, vₙ.

structure O3.OGMGExecutionConfig (d : ℕ) : Type

Data fixed before running the finite OGM-G phase. The coefficient function is kept explicit here so the execution algebra can also be reused by the coefficient auditor; the source run below instantiates it by the frozen backward theta sequence.

• horizon : ℕ

  The number of iterations in the OGM-G execution.

• oracle : PairOracle d

  The value-gradient oracle queried by the execution.

• M : ℝ

  The smoothness estimate used to scale the gradient steps.

• U : Vec d

  The starting point of the OGM-G execution.

• theta : ℕ → ℝ

  The momentum coefficient sequence supplied to the execution.

noncomputable def O3.stage9ExecutionConfig {d : ℕ} (n : ℕ) (oracle : PairOracle d) (M : ℝ) (U : Vec d) : OGMGExecutionConfig d

The source-exact configuration: no theta sequence is supplied by the caller; it is the frozen special-zero/backward-tail sequence for horizon n.

Equations

• O3.stage9ExecutionConfig n oracle M U = { horizon := n, oracle := oracle, M := M, U := U, theta := O3.stage9Theta n }

@[simp]

theorem O3.stage9ExecutionConfig_horizon {d : ℕ} (n : ℕ) (oracle : PairOracle d) (M : ℝ) (U : Vec d) : (stage9ExecutionConfig n oracle M U).horizon = n

@[simp]

theorem O3.stage9ExecutionConfig_theta {d : ℕ} (n i : ℕ) (oracle : PairOracle d) (M : ℝ) (U : Vec d) : (stage9ExecutionConfig n oracle M U).theta i = stage9Theta n i

structure O3.OGMGExecutionState (d : ℕ) : Type

At the beginning of iteration i, current is u_i and previousV is v_(i-1). Thus the initial previous point is literally v_(-1)=U.

• current : Vec d

  The current query point u_i at the beginning of an iteration.

• previousV : Vec d

  The previous gradient-step point v_(i-1), initialized at the starting point.

noncomputable def O3.ogmgExecutionStep {d : ℕ} (cfg : OGMGExecutionConfig d) (i : ℕ) (state : OGMGExecutionState d) : OGMGExecutionState d

One literal source step.

Equations

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

noncomputable def O3.ogmgState {d : ℕ} (cfg : OGMGExecutionConfig d) : ℕ → OGMGExecutionState d

Primitive-recursive actual execution, beginning from u_0=U, v_(-1)=U.

Equations

• O3.ogmgState cfg 0 = { current := cfg.U, previousV := cfg.U }
• O3.ogmgState cfg i.succ = O3.ogmgExecutionStep cfg i (O3.ogmgState cfg i)

noncomputable def O3.ogmgObservation {d : ℕ} (cfg : OGMGExecutionConfig d) (i : ℕ) : Observation d

The actual observation at u_i.

Equations

• O3.ogmgObservation cfg i = cfg.oracle.observe (O3.ogmgState cfg i).current

noncomputable def O3.ogmgGradient {d : ℕ} (cfg : OGMGExecutionConfig d) (i : ℕ) : Vec d

The actual queried gradient g_i.

Equations

• O3.ogmgGradient cfg i = (O3.ogmgObservation cfg i).gradient

noncomputable def O3.ogmgV {d : ℕ} (cfg : OGMGExecutionConfig d) (i : ℕ) : Vec d

The literal gradient point v_i=u_i-g_i/M.

Equations

• O3.ogmgV cfg i = (O3.ogmgState cfg i).current - cfg.M⁻¹ • O3.ogmgGradient cfg i

@[simp]

theorem O3.ogmgState_zero_current {d : ℕ} (cfg : OGMGExecutionConfig d) : (ogmgState cfg 0).current = cfg.U

@[simp]

theorem O3.ogmgState_zero_previousV {d : ℕ} (cfg : OGMGExecutionConfig d) : (ogmgState cfg 0).previousV = cfg.U

@[simp]

theorem O3.ogmgObservation_point {d : ℕ} (cfg : OGMGExecutionConfig d) (i : ℕ) : (ogmgObservation cfg i).point = (ogmgState cfg i).current

@[simp]

theorem O3.ogmgObservation_value {d : ℕ} (cfg : OGMGExecutionConfig d) (i : ℕ) : (ogmgObservation cfg i).value = cfg.oracle.value (ogmgState cfg i).current

@[simp]

theorem O3.ogmgObservation_gradient {d : ℕ} (cfg : OGMGExecutionConfig d) (i : ℕ) : (ogmgObservation cfg i).gradient = cfg.oracle.gradient (ogmgState cfg i).current

@[simp]

theorem O3.ogmgGradient_eq {d : ℕ} (cfg : OGMGExecutionConfig d) (i : ℕ) : ogmgGradient cfg i = cfg.oracle.gradient (ogmgState cfg i).current

theorem O3.ogmgV_eq {d : ℕ} (cfg : OGMGExecutionConfig d) (i : ℕ) : ogmgV cfg i = (ogmgState cfg i).current - cfg.M⁻¹ • ogmgGradient cfg i

@[simp]

theorem O3.ogmgState_succ_previousV {d : ℕ} (cfg : OGMGExecutionConfig d) (i : ℕ) : (ogmgState cfg (i + 1)).previousV = ogmgV cfg i

theorem O3.ogmgState_succ_current {d : ℕ} (cfg : OGMGExecutionConfig d) (i : ℕ) : (ogmgState cfg (i + 1)).current = ogmgV cfg i + ((cfg.theta i - 1) * (2 * cfg.theta (i + 1) - 1) / (cfg.theta i * (2 * cfg.theta i - 1))) • (ogmgV cfg i - (ogmgState cfg i).previousV) + ((2 * cfg.theta (i + 1) - 1) / (2 * cfg.theta i - 1)) • (ogmgV cfg i - (ogmgState cfg i).current)

The actual source recurrence with its coefficients unchanged.

theorem O3.stage9Execution_succ_current {d : ℕ} (n : ℕ) (oracle : PairOracle d) (M : ℝ) (U : Vec d) (i : ℕ) : (ogmgState (stage9ExecutionConfig n oracle M U) (i + 1)).current = ogmgV (stage9ExecutionConfig n oracle M U) i + ((stage9Theta n i - 1) * (2 * stage9Theta n (i + 1) - 1) / (stage9Theta n i * (2 * stage9Theta n i - 1))) • (ogmgV (stage9ExecutionConfig n oracle M U) i - (ogmgState (stage9ExecutionConfig n oracle M U) i).previousV) + ((2 * stage9Theta n (i + 1) - 1) / (2 * stage9Theta n i - 1)) • (ogmgV (stage9ExecutionConfig n oracle M U) i - (ogmgState (stage9ExecutionConfig n oracle M U) i).current)

The recurrence specialized to the non-user-supplied, source-exact theta coefficients.

theorem O3.stage9Execution_theta_denominators_pos {d : ℕ} (n i : ℕ) (oracle : PairOracle d) (M : ℝ) (U : Vec d) : 0 < (stage9ExecutionConfig n oracle M U).theta i ∧ 0 < 2 * (stage9ExecutionConfig n oracle M U).theta i - 1

theorem O3.ogmg_velocity_p_relation {d : ℕ} (cfg : OGMGExecutionConfig d) (hM : cfg.M ≠ 0) (hθ : ∀ (i : ℕ), cfg.theta i ≠ 0) (hden : ∀ (i : ℕ), 2 * cfg.theta i - 1 ≠ 0) (i : ℕ) : cfg.M • (ogmgV cfg i - (ogmgState cfg i).previousV) = -cfg.theta i • (stage9P cfg.theta (ogmgGradient cfg) i + stage9P cfg.theta (ogmgGradient cfg) (i + 1))

The actual iterate recursion produces the precise velocity identity used by the frozen quadratic telescoping proof. This is proved for every natural index, hence in particular at the terminal endpoint i=n; no extrapolated iterate hypothesis is introduced.

theorem O3.stage9Execution_velocity_p_relation {d : ℕ} (n : ℕ) (oracle : PairOracle d) (M : ℝ) (U : Vec d) (hM : M ≠ 0) (i : ℕ) : have cfg := stage9ExecutionConfig n oracle M U; M • (ogmgV cfg i - (ogmgState cfg i).previousV) = -stage9Theta n i • (stage9P (stage9Theta n) (ogmgGradient cfg) i + stage9P (stage9Theta n) (ogmgGradient cfg) (i + 1))

Source-exact specialization of the velocity identity.

theorem O3.ogmgState_previousV {d : ℕ} (cfg : OGMGExecutionConfig d) (i : ℕ) : (ogmgState cfg (i + 1)).previousV = ogmgV cfg i

For every positive index the stored predecessor is the actual preceding gradient point.

noncomputable def O3.ogmgNewIterates {d : ℕ} (cfg : OGMGExecutionConfig d) : Fin cfg.horizon → Vec d

The n new iterate queries u_1,…,u_n, indexed without a phantom query.

Equations

• O3.ogmgNewIterates cfg i = (O3.ogmgState cfg (↑i + 1)).current

noncomputable def O3.ogmgTerminalObservation {d : ℕ} (cfg : OGMGExecutionConfig d) : Observation d

The final extra query is at exactly v_n.

Equations

• O3.ogmgTerminalObservation cfg = cfg.oracle.observe (O3.ogmgV cfg cfg.horizon)

noncomputable def O3.ogmgExecutionTrace {d : ℕ} (cfg : OGMGExecutionConfig d) : OracleTrace d

Phase-B calls only: u_1,…,u_n,v_n.

Equations

• O3.ogmgExecutionTrace cfg = O3.finiteDataOGMGTrace cfg.oracle (O3.ogmgNewIterates cfg) (O3.ogmgV cfg cfg.horizon)

theorem O3.ogmgExecutionTrace_exact {d : ℕ} (cfg : OGMGExecutionConfig d) : TraceExact cfg.oracle (ogmgExecutionTrace cfg)

@[simp]

theorem O3.ogmgExecutionTrace_length {d : ℕ} (cfg : OGMGExecutionConfig d) : List.length (ogmgExecutionTrace cfg) = cfg.horizon + 1

theorem O3.ogmgExecutionTrace_terminal_queried {d : ℕ} (cfg : OGMGExecutionConfig d) : WasQueried (ogmgExecutionTrace cfg) (ogmgV cfg cfg.horizon)

The additional terminal point v_n is genuinely queried.

theorem O3.ogmgExecutionTrace_final_iterate_queried {d : ℕ} (cfg : OGMGExecutionConfig d) (hn : 1 ≤ cfg.horizon) : WasQueried (ogmgExecutionTrace cfg) (ogmgState cfg cfg.horizon).current

For a nonzero horizon, u_n is one of the newly queried iterates.

noncomputable def O3.ogmgDataObservation {d : ℕ} (cfg : OGMGExecutionConfig d) (i : Fin (cfg.horizon + 1)) : Observation d

The reused point u₀=U and every subsequently queried u_i, including u_n, as an actual oracle observation.

Equations

• O3.ogmgDataObservation cfg i = O3.ogmgObservation cfg ↑i

noncomputable def O3.ogmgFunctionValue {d : ℕ} (cfg : OGMGExecutionConfig d) (i : ℕ) : ℝ

Scalar/vector projections of the actual finite data, ready for the algebraic certificate. These are definitions, not freely supplied arrays.

Equations

• O3.ogmgFunctionValue cfg i = (O3.ogmgObservation cfg i).value

noncomputable def O3.ogmgGradientSq {d : ℕ} (cfg : OGMGExecutionConfig d) (i : ℕ) : ℝ

The squared Euclidean norm of the gradient at an execution query.

Equations

• O3.ogmgGradientSq cfg i = O3.lpNorm 2 (O3.ogmgGradient cfg i) ^ 2

noncomputable def O3.ogmgPairTerm {d : ℕ} (cfg : OGMGExecutionConfig d) (i j : ℕ) : ℝ

The gradient at query j paired with the difference of gradient-step points i and j.

Equations

• O3.ogmgPairTerm cfg i j = O3.pairing (O3.ogmgGradient cfg j) (O3.ogmgV cfg i - O3.ogmgV cfg j)

@[simp]

theorem O3.ogmgFunctionValue_zero {d : ℕ} (cfg : OGMGExecutionConfig d) : ogmgFunctionValue cfg 0 = cfg.oracle.value cfg.U

@[simp]

theorem O3.ogmgPairTerm_self {d : ℕ} (cfg : OGMGExecutionConfig d) (i : ℕ) : ogmgPairTerm cfg i i = 0

noncomputable def O3.ogmgInterpolationCheck {d : ℕ} (cfg : OGMGExecutionConfig d) (i j : Fin (cfg.horizon + 1)) : GuardCheck

The observable ordered interpolation check for (i,j).

Equations

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

noncomputable def O3.ogmgAllInterpolationChecks {d : ℕ} (cfg : OGMGExecutionConfig d) : List GuardCheck

A concrete list containing all (n+1)^2 ordered interpolation checks.

Equations

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

@[simp]

theorem O3.ogmgAllInterpolationChecks_length {d : ℕ} (cfg : OGMGExecutionConfig d) : (ogmgAllInterpolationChecks cfg).length = (cfg.horizon + 1) * (cfg.horizon + 1)

@[simp]

theorem O3.ogmgInterpolationCheck_kind {d : ℕ} (cfg : OGMGExecutionConfig d) (i j : Fin (cfg.horizon + 1)) : (ogmgInterpolationCheck cfg i j).kind = GuardKind.interpolation

def O3.OGMGAllInterpolationGuardsHold {d : ℕ} (cfg : OGMGExecutionConfig d) : Prop

All ordered-pair finite-data interpolation guards pass.

Equations

• O3.OGMGAllInterpolationGuardsHold cfg = O3.allGuardsPass (O3.ogmgAllInterpolationChecks cfg)

theorem O3.ogmgAllInterpolationGuardsHold_iff {d : ℕ} (cfg : OGMGExecutionConfig d) : OGMGAllInterpolationGuardsHold cfg ↔ ∀ (i j : Fin (cfg.horizon + 1)), (ogmgInterpolationCheck cfg i j).Holds

noncomputable def O3.ogmgTerminalDescentCheck {d : ℕ} (cfg : OGMGExecutionConfig d) : GuardCheck

The source terminal guard is the actual upper-model check at the extra query v_n.

Equations

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

theorem O3.ogmgTerminalDescentCheck_holds_iff {d : ℕ} (cfg : OGMGExecutionConfig d) : (ogmgTerminalDescentCheck cfg).Holds ↔ (ogmgTerminalObservation cfg).value ≤ (ogmgObservation cfg cfg.horizon).value + pairing (ogmgGradient cfg cfg.horizon) (ogmgV cfg cfg.horizon - (ogmgState cfg cfg.horizon).current) + cfg.M / 2 * lpNorm 2 (ogmgV cfg cfg.horizon - (ogmgState cfg cfg.horizon).current) ^ 2

theorem O3.ogmgTerminal_displacement {d : ℕ} (cfg : OGMGExecutionConfig d) : ogmgV cfg cfg.horizon - (ogmgState cfg cfg.horizon).current = -cfg.M⁻¹ • ogmgGradient cfg cfg.horizon

Exact displacement of the queried terminal gradient point.

theorem O3.pairing_self_eq_lpNorm_two_sq {d : ℕ} (g : Vec d) : pairing g g = lpNorm 2 g ^ 2

theorem O3.ogmgTerminalDescentCheck_source_iff {d : ℕ} (cfg : OGMGExecutionConfig d) (hM : 0 < cfg.M) : (ogmgTerminalDescentCheck cfg).Holds ↔ (ogmgTerminalObservation cfg).value ≤ (ogmgObservation cfg cfg.horizon).value - lpNorm 2 (ogmgGradient cfg cfg.horizon) ^ 2 / (2 * cfg.M)

With M>0, the actual queried upper-model check at v_n=u_n-g_n/M is exactly the terminal descent inequality printed in the source.

noncomputable def O3.ogmgExecutionGuards {d : ℕ} (cfg : OGMGExecutionConfig d) : List GuardCheck

All Stage-9 observable guards, without any algebraic certificate field.

Equations

• O3.ogmgExecutionGuards cfg = O3.ogmgAllInterpolationChecks cfg ++ [O3.ogmgTerminalDescentCheck cfg]

theorem O3.ogmgExecutionGuards_interpolation {d : ℕ} (cfg : OGMGExecutionConfig d) (h : allGuardsPass (ogmgExecutionGuards cfg)) (i j : Fin (cfg.horizon + 1)) : (ogmgInterpolationCheck cfg i j).Holds

theorem O3.ogmgExecutionGuards_terminal {d : ℕ} (cfg : OGMGExecutionConfig d) (h : allGuardsPass (ogmgExecutionGuards cfg)) : (ogmgTerminalDescentCheck cfg).Holds