Successful stopped executions have one output and count
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalExecutionIdentity.successful_query_unique · theorem · Teaching coverage
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.
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.
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 = sProof roadmap
- 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.
- 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.
- 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.
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.
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.
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.
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.ProximalExecutionIdentitySource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Euclidean source algorithm and its normalized C2 potential. | 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. | generalization | The scope and typeclasses are explicit; no full source theorem is asserted. |
| D.4 uses run-wide D.7 before Jensen and phase/run query aggregation. | 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. | source-implicit | This isolates the actual implementation component and states all remaining 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.
Encoder–denoiser: source-reviewed · equivalent-after-elaboration
Detected semantic differences
- scopes: The formal result is an explicitly scoped deterministic implementation identity, generalized to arbitrary normed real E and arbitrary g/parameters. It does not separately reproduce a named source theorem or receive additional paper-progress credit. — The proof uses only exact successful-run equations; current lesson scope retains all termination, accuracy, Gaussian and cost obligations separately.
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
- 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
- Chen–Chewi–Lu–Zhang, stopped routine and actual Picard query centers — 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.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.