Counted phase program
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.CountedPhaseProgram.phaseQuery · def · Teaching coverage
Mathematical statement
For arbitrary real normed E, gradient oracle g, eta,eps,h, Fin m nodes and weights, input w and fuel:E→Nat, phaseQuery returns Option((E*E)*Nat). It first refreshes P0 and builds Y0. It sequentially executes every proximalQuery at Y0_i from Y0_i using fuel(Y0_i), and if successful evaluates g at returned point plus sqrt(eta)G0_i and adds one query to that returned count. It builds Y1 from these actual returned gradients, sequentially executes every second proximal/noisy-gradient call similarly using G1, then returns the complete phase output and the sum of both arrays actual counts. Any failed call returns none, with no successful cost certificate.
Lean statement · phaseQuery
Exact finite arrays, full input/return types, parameters and counting boundary are retained in 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.
def phaseQuery {m : ℕ} (g : E → E) (eta eps h : ℝ)
(t : Fin m → ℝ) (omega : Fin m → Fin m → ℝ)
(positionWeight momentumWeight : Fin m → ℝ) (fuel : E → ℕ)
(w : (E × E) × ((E × E) × ((Fin m → E) × (Fin m → E)))) :
Option ((E × E) × ℕ)Proof roadmap
- 1Execute a finite successful query array
Induct on the finite array size. The empty array returns count zero. For a nonempty array, execute index zero, then the tail, returning the actual vector of outputs and the sum of their returned counts. Fin.cons reconstruction and Fin.sum_univ_succ identify the complete returned vector and count. This helper has no probabilistic or termination premise beyond the individual successful calls.
- 2Run the actual two-layer program
For each first center, run the residual-stopped proximal interpreter and evaluate the Gaussian-shifted gradient of its returned point, adding one direct query. Construct the second centers using these actual first returned gradients; run the second array in the same manner. Form the full updated state including both half-refreshes from the second returned gradients. In both layers each proximal count N(Y)+1 already includes its terminal successful residual test. Thus the returned count is the sum of both arrays plus exactly 2*m direct gradient evaluations. Failed insufficient-fuel calls return none.
Full assumptions and notation
All objects and hypotheses
- E is an arbitrary real normed vector space; g, parameters, supplied finite nodes/weights and fuel are arbitrary. The input contains one state pair, two refresh noises and two Fin-m noise arrays; no probability or success assumption.
Construction and meaning
1. Execute a finite successful query array
Induct on the finite array size. The empty array returns count zero. For a nonempty array, execute index zero, then the tail, returning the actual vector of outputs and the sum of their returned counts. Fin.cons reconstruction and Fin.sum_univ_succ identify the complete returned vector and count. This helper has no probabilistic or termination premise beyond the individual successful calls.
Corresponding Lean step
collectQueries; collectQueries_some
2. Run the actual two-layer program
For each first center, run the residual-stopped proximal interpreter and evaluate the Gaussian-shifted gradient of its returned point, adding one direct query. Construct the second centers using these actual first returned gradients; run the second array in the same manner. Form the full updated state including both half-refreshes from the second returned gradients. In both layers each proximal count N(Y)+1 already includes its terminal successful residual test. Thus the returned count is the sum of both arrays plus exactly 2*m direct gradient evaluations. Failed insufficient-fuel calls return none.
Corresponding Lean step
phaseQuery; phaseQuery_success; Finset.sum_add_distrib
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean construction · phaseQuery
The proof steps cover both private execution helpers and the public actual-law total-cost theorem. The definition itself is an execution prerequisite, not a proof edge.
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.
def phaseQuery {m : ℕ} (g : E → E) (eta eps h : ℝ)
(t : Fin m → ℝ) (omega : Fin m → Fin m → ℝ)
(positionWeight momentumWeight : Fin m → ℝ) (fuel : E → ℕ)
(w : (E × E) × ((E × E) × ((Fin m → E) × (Fin m → E)))) :
Option ((E × E) × ℕ) := do
let P0 := Real.exp (-h/2) • w.1.2 + Real.sqrt (1-Real.exp (-h)) • w.2.1.1
let Y0 := fun i => w.1.1 + t i • P0
let r0 ← collectQueries m (fun i =>
(ApproximateProximalExecution.proximalQuery g eta eps (Y0 i) (fuel (Y0 i)) (Y0 i)).map
(fun r => (g (r.1+Real.sqrt eta • w.2.2.1 i),r.2+1)))
let Y1 := fun i => Y0 i - ∑ j, omega i j • r0.1 j
let r1 ← collectQueries m (fun i =>
(ApproximateProximalExecution.proximalQuery g eta eps (Y1 i) (fuel (Y1 i)) (Y1 i)).map
(fun r => (g (r.1+Real.sqrt eta • w.2.2.2 i),r.2+1)))
pure ((w.1.1+h • P0-∑ j, positionWeight j • r1.1 j,
Real.exp (-h/2) • (P0-∑ j, momentumWeight j • r1.1 j) +
Real.sqrt (1-Real.exp (-h)) • w.2.1.2),r0.2+r1.2)Source assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Source Algorithm3.1 fixes quadrature; D4 uses run-wide D7 and substitutes selected parameters. | Actual interpreter definition only. Single full Gaussian phase with supplied incoming integrable state L2 budget, finite bounded nodes and row l1 bounds; actual successful exact-real interpreter output and total gradient count. Sufficient finite fuel certifies execution and is not a runtime precomputation or a count/cost hypothesis. No cost claim for failed insufficient-fuel executions. Gaussian sampling and arithmetic are not gradient queries. Source quadrature/J adapter, run-wide D7 induction, D8 parameter/iteration substitution, Wp, proxy-warmness, initialization, PBPS and composition/main results remain open. No TV-to-unbounded-cost transfer. | generalization | Actual arbitrary finite-array single-phase work component; source adapter and repeated-history theorem remain explicit obligations. |
| Stopped AlgorithmD2 repeats until the residual criterion succeeds. | Finite fuel returns Option; success is certified by the proved global proximal execution with N(y)+1. Failure returns none without a successful count. | source-implicit | Execution certificate avoids introducing unproved termination or nominal counts; no fuel precomputation is charged as source runtime. |
Actual interpreter definition only. Single full Gaussian phase with supplied incoming integrable state L2 budget, finite bounded nodes and row l1 bounds; actual successful exact-real interpreter output and total gradient count. Sufficient finite fuel certifies execution and is not a runtime precomputation or a count/cost hypothesis. No cost claim for failed insufficient-fuel executions. Gaussian sampling and arithmetic are not gradient queries. Source quadrature/J adapter, run-wide D7 induction, D8 parameter/iteration substitution, Wp, proxy-warmness, initialization, PBPS and composition/main results remain open. No TV-to-unbounded-cost transfer.
Encoder–denoiser: source-reviewed · equivalent-after-elaboration
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
- Actual interpreter definition only. Single full Gaussian phase with supplied incoming integrable state L2 budget, finite bounded nodes and row l1 bounds; actual successful exact-real interpreter output and total gradient count. Sufficient finite fuel certifies execution and is not a runtime precomputation or a count/cost hypothesis. No cost claim for failed insufficient-fuel executions. Gaussian sampling and arithmetic are not gradient queries. Source quadrature/J adapter, run-wide D7 induction, D8 parameter/iteration substitution, Wp, proxy-warmness, initialization, PBPS and composition/main results remain open. No TV-to-unbounded-cost transfer.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- Fin.sum_univ_succ
- MeasureTheory.integrable_finsetSum
- MeasureTheory.integral_finsetSum
- MeasureTheory.probReal_univ
Mathematical sources
- SPHMC actual two-layer phase queries — Actual interpreter definition only. Single full Gaussian phase with supplied incoming integrable state L2 budget, finite bounded nodes and row l1 bounds; actual successful exact-real interpreter output and total gradient count. Sufficient finite fuel certifies execution and is not a runtime precomputation or a count/cost hypothesis. No cost claim for failed insufficient-fuel executions. Gaussian sampling and arithmetic are not gradient queries. Source quadrature/J adapter, run-wide D7 induction, D8 parameter/iteration substitution, Wp, proxy-warmness, initialization, PBPS and composition/main results remain open. No TV-to-unbounded-cost transfer.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.