Simulate the regularized first-order oracle with no extra queries

The compiled first-order regularization theorem computes the genuine gradient of W. Its value is W by definition. Therefore adding the known quadratic value and gradient correction to one O_f reply produces exactly O_W(x). Convexity and gradient Lipschitzness are inherited source-class premises of the reused parent; no Hessian or second derivative is needed. Induct on query allowance, for every state. Both runs inspect the same next(s). A halt or zero-fuel exhaustion returns the same result without querying. In the positive-fuel query branch, corrected and true replies update to exactly the same state. Apply the induction hypothesis there; this handles reply-dependent future queries and stopping. In the only querying branch both interpreters make one interaction and add one to the equal recursive counters. The inductive bound c≤n gives c+1≤n+1. Halt/exhaustion branches have zero cost. No externally supplied cost label or objective minimizer enters the execution.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem simulate_regularized
    {E S X : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
    (next : S → Sum X E) (update : S → E → (ℝ × E) → S)
    {f : E → ℝ} (hd : Differentiable ℝ f) (hc : ConvexOn ℝ univ f)
    {β δ : ℝ≥0} (hL : LipschitzWith β (gradient f)) (u : E) (fuel : ℕ) (s : S) :
    let W := fun x => f x + (δ : ℝ)/2*‖x-u‖^2
    let corrected := fun s x (a : ℝ × E) =>
      update s x (a.1 + (δ : ℝ)/2*‖x-u‖^2, a.2 + (δ : ℝ) • (x-u))
    let base := run next corrected (fun x => (f x, gradient f x)) fuel s
    let target := run next update (fun x => (W x, gradient W x)) fuel s
    base = target ∧ base.2 ≤ fuel := by
  dsimp only
  have hg := (QuadraticRegularizationFirstOrder.curvature_gradient_and_smoothness
    hd hc hL (δ := δ) u).2.2.1
  induction fuel generalizing s with
  | zero => cases h : next s <;> simp [run, h]
  | succ n ih =>
    cases h : next s with
    | inl x => simp [run, h]
    | inr x =>
      have step (upd : S → E → (ℝ × E) → S) (O : E → ℝ × E) :
          run next upd O (n+1) s =
            let tail := run next upd O n (upd s x (O x))
            (tail.1, tail.2+1) := by rw [run, h]
      simp only [step, hg]
      obtain ⟨he, hn⟩ := ih (update s x
        (f x + (δ : ℝ)/2*‖x-u‖^2, gradient f x + (δ : ℝ) • (x-u)))
      refine ⟨?_, Nat.succ_le_succ hn⟩
      simpa only [hg] using congrArg (fun r => (r.1, r.2+1)) he
end AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularizationOracle

Exact module and namespace context