Finite-fuel meaning of a gradient-only proximal query

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang; Samplinglib supplies finite-fuel semantics for the stated recurrence.

Complete source statement (Samplinglib restatement)

Represent one gradient evaluation and residual test per positive-fuel step. With no fuel return none. Otherwise set z=y−eta g(x); on a successful test return the current x with count one, and on failure recurse from z with one less fuel, adding one to a successful count. This is a definition, not a correctness or termination theorem.

Current-point return

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

A gradient-query interpreter that counts the successful test

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ApproximateProximalExecution.proximalQuery · def · Teaching coverage

Read this first

Mathematical statement

With no fuel return none. Otherwise evaluate g at x, form z=y−eta g(x), and test the residual. Success returns the current x and count one. Failure recurses at z with one less fuel and adds one to a successful returned count; unsuccessful recursion returns none.

\[Q_0(x)=\mathrm{none},\qquad Q_{m+1}(x)=\begin{cases}\mathrm{some}(x,1),&\|y-\eta g(x)-x\|\le(1-\eta)\varepsilon,\\\mathrm{map}((u,k)\mapsto(u,k+1),Q_m(y-\eta g(x))),&\text{otherwise}.\end{cases}\]

Lean statement · proximalQuery

The adjacent disclosure extracts the exact oracle, real parameters, natural fuel, and Option-valued return type from Lean.

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)

noncomputable def proximalQuery (g : E → E) (eta eps : ℝ) (y : E) :
    ℕ → E → Option (E × ℕ)
  | 0, _ => none
  | n+1, x => by
    classical
    let z := y-eta • g x
    exact if ‖z-x‖ ≤ (1-eta)*eps then some (x,1)
      else (proximalQuery g eta eps y n z).map (fun r => (r.1,r.2+1))

Exact module and namespace context

Proof roadmap

1Spend one query before testing
Even an immediately successful residual test needs the gradient at the current point. The let-bound z represents that single oracle evaluation. Mathematical arithmetic and comparison are exact; this is not a numerical-roundoff model.
2Return the tested point, not the next point
The certificate in the companion theorem controls the error at x through the residual between x and z. Therefore the successful branch returns x. Each unsuccessful level contributes exactly one additional query to the recursively returned count.

Full assumptions and notation

All objects and hypotheses

E is a real normed vector space. g:E→E is an arbitrary oracle, eta and eps are real parameters, y is the fixed center, x is the current point, and fuel is a natural number. No regularity or positivity is required just to define the interpreter.

Construction and meaning

1. Spend one query before testing

Even an immediately successful residual test needs the gradient at the current point. The let-bound z represents that single oracle evaluation. Mathematical arithmetic and comparison are exact; this is not a numerical-roundoff model.

\[z=y-\eta g(x),\qquad r=\|z-x\|.\]

Corresponding Lean step

The positive-fuel branch binds z before the if; success is some (x,1).

2. Return the tested point, not the next point

The certificate in the companion theorem controls the error at x through the residual between x and z. Therefore the successful branch returns x. Each unsuccessful level contributes exactly one additional query to the recursively returned count.

\[\mathrm{returned\ point}=x,\qquad\mathrm{count}=1+\mathrm{recursive\ count}.\]

Corresponding Lean step

Option.map preserves failure and increments only the count in a successful pair; run_first_stop proves the recurrence's execution equation.

Lean verification

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

Lean construction · proximalQuery

This is a recursive definition, not an independently proved accuracy theorem. Its execution is certified by approximate_proximal_execution.

Download module (.lean)

noncomputable def proximalQuery (g : E → E) (eta eps : ℝ) (y : E) :
    ℕ → E → Option (E × ℕ)
  | 0, _ => none
  | n+1, x => by
    classical
    let z := y-eta • g x
    exact if ‖z-x‖ ≤ (1-eta)*eps then some (x,1)
      else (proximalQuery g eta eps y n z).map (fun r => (r.1,r.2+1))

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
The algorithm is applied to gradient V under curvature and positive-parameter assumptions.	The recurrence is defined for arbitrary g, eta and eps in a real normed space.	generalization	Only the construction is generalized. Its correctness theorem reinstates the source assumptions; the definition supplies no correctness conclusion.
Iterate until the first successful residual and return the current iterate.	A natural-number fuel bounds the recursion; failure returns none and success records current point plus query count.	API-limitation	Finite fuel gives a total Lean definition. The execution theorem supplies sufficient fuel; it does not turn this into a floating-point executable or an unbounded recursive program.

Construction only. No termination, minimizer, accuracy, expected cost or floating-point implementation claim; no query-list trace. The separate execution theorem proves successful fuel and its returned count.

Encoder–denoiser: source-reviewed · exact

Detected semantic differences

domains: Relative to Algorithm D.2 itself, the attributed construction abstracts the gradient to arbitrary g and permits arbitrary current states and real parameters. — The packet expressly separates the broadly defined recurrence from the assumptions needed for its proximal interpretation.
scopes: Natural fuel, Option failure and returned query counts are explicitly attributed representation structure, not syntax printed in Algorithm D.2. — The primary algorithm supplies the update, residual test and current-iterate return; the packet discloses Samplinglib's finite-fuel representation.

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

Exact-real noncomputable finite-fuel semantics, not floating-point software. This definition alone proves neither termination nor accuracy. It records output and count, not a query-list trace.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Option.map

Mathematical sources

Chen–Chewi–Lu–Zhang, SPHMC Algorithm D.2 — Attributed paraphrase; Samplinglib's finite-fuel representation is explicit implementation structure.

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