Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

ProximalExecutionIdentity: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. Successful stopped executions have one output and count
Samplinglib mathematical lesson

Successful stopped executions have one output and count

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalExecutionIdentity.successful_query_unique · theorem · Teaching coverage

Read this first

Mathematical statement

For the deterministic stopped gradient interpreter of Algorithm D.2, any two successful finite-fuel executions from the same y and initial x, using the same g,eta,eps, return exactly the same pair (output point, actual gradient-test count), independently of the sufficient fuels.

\[\operatorname{run}(g,\eta,\varepsilon,y,n,x)=\operatorname{some}(r),\quad\operatorname{run}(g,\eta,\varepsilon,y,m,x)=\operatorname{some}(s)\quad\Longrightarrow\quad r=s.\]
Lean statement · successful_query_unique

Arbitrary real normed E, g, eta, eps, y, x and finite fuels n,m; successful interpreter equations for both returned pairs imply exact equality r=s. No measure or probability law occurs.

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.

Download module (.lean)
theorem successful_query_unique {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] (g : E → E) (eta eps : ℝ) (y : E)
    {n m : ℕ} {x : E} {r s : E × ℕ}
    (hr : ApproximateProximalExecution.proximalQuery g eta eps y n x = some r)
    (hs : ApproximateProximalExecution.proximalQuery g eta eps y m x = some s) : r = s

Exact module and namespace context

Proof roadmap

  1. 1Exclude zero fuel

    Zero fuel returns none, so a supplied successful run cannot have zero fuel. Induct on the first fuel and eliminate zero fuel for the second.

  2. 2Compare identical stopping branches

    Both positive-fuel runs evaluate the same gradient at the same current x and the same residual test. If that test succeeds, both return the current x with count one. This counts the final gradient evaluation.

  3. 3Compare identical continuing branches

    If the common residual test fails, both recurse at the same next point y-eta*g(x). Successful Option.map outputs imply successful recursive returned pairs. The induction hypothesis identifies those pairs; applying the same count increment gives equality of the outer returned pairs. No mathematical contraction or termination claim is needed.

Full assumptions and notation

All objects and hypotheses

  • E is a real normed vector space; g:E→E, eta,eps,y and initial state x are arbitrary. Two supplied finite fuels n,m yield successful returned pairs r,s under the same deterministic interpreter. No positivity, contractivity or termination hypothesis.

Mathematical proof

1. Exclude zero fuel

Zero fuel returns none, so a supplied successful run cannot have zero fuel. Induct on the first fuel and eliminate zero fuel for the second.

\[\operatorname{run}(\cdot,0,x)=\operatorname{none}.\]
Corresponding Lean step

induction n; cases m; simp [proximalQuery] at hr hs

2. Compare identical stopping branches

Both positive-fuel runs evaluate the same gradient at the same current x and the same residual test. If that test succeeds, both return the current x with count one. This counts the final gradient evaluation.

\[\|y-\eta g(x)-x\|\le(1-\eta)\varepsilon\ \Longrightarrow\ r=s=(x,1).\]
Corresponding Lean step

split_ifs; Option.some.inj

3. Compare identical continuing branches

If the common residual test fails, both recurse at the same next point y-eta*g(x). Successful Option.map outputs imply successful recursive returned pairs. The induction hypothesis identifies those pairs; applying the same count increment gives equality of the outer returned pairs. No mathematical contraction or termination claim is needed.

\[r\prime=s\prime\ \Longrightarrow\ (r\prime_1,r\prime_2+1)=(s\prime_1,s\prime_2+1).\]
Corresponding Lean step

Option.map_eq_some_iff; induction hypothesis; congrArg

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · successful_query_unique

Induct on the first fuel, eliminate zero successful fuel for either run, then compare the identical residual test. A stopping branch returns the same pair; a continuing branch uses recursive pair equality and the same count increment.

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.

Download module (.lean)
theorem successful_query_unique {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] (g : E → E) (eta eps : ℝ) (y : E)
    {n m : ℕ} {x : E} {r s : E × ℕ}
    (hr : ApproximateProximalExecution.proximalQuery g eta eps y n x = some r)
    (hs : ApproximateProximalExecution.proximalQuery g eta eps y m x = some s) : r = s := by
  classical
  induction n generalizing m x r s with
  | zero => simp [ApproximateProximalExecution.proximalQuery] at hr
  | succ n ih =>
    cases m with
    | zero => simp [ApproximateProximalExecution.proximalQuery] at hs
    | succ m =>
      rw [ApproximateProximalExecution.proximalQuery] at hr hs
      split_ifs at hr hs with hstop
      · exact Option.some.inj (hr.symm.trans hs)
      · obtain ⟨r', hr', hrr⟩ := Option.map_eq_some_iff.mp hr
        obtain ⟨s', hs', hss⟩ := Option.map_eq_some_iff.mp hs
        have heq := ih hr' hs'
        simpa [← hrr, ← hss] using congrArg (fun z : E × ℕ => (z.1, z.2 + 1)) heq

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalExecutionIdentity

Exact module and namespace context

Scope and omitted-condition boundaries
  • Conditional deterministic identity for successful runs only. No existence of a successful run, proximal accuracy, count bound, Gaussian law or main theorem. Reusable interface extracted for the same-witness full-phase consumer; no independent paper-progress credit for extraction.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

    Mathlib API called (external library)

    • Option.map_eq_some_iff

    Mathematical sources

    Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.