CountedPhaseProgram: 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.

Counted phase program
Counted phase work

Samplinglib mathematical lesson

Counted phase program

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.CountedPhaseProgram.phaseQuery · def · Teaching coverage

Read this first

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.

\[T=2m+\sum_{i=0}^{m-1}\bigl[N(Y_i^0)+1+N(Y_i^1)+1\bigr],\quad \mathbb E_\mu T\le m(2+L_0+L_1).\]

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.

Download module (.lean)

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) × ℕ)

Exact module and namespace context

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.

\[\operatorname{collect}(r_i)=(x_i,\sum_i c_i)\quad\text{if }r_i=\operatorname{some}(x_i,c_i).\]

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.

\[T=2m+\sum_{i=0}^{m-1}\bigl[N(Y_i^0)+1+N(Y_i^1)+1\bigr],\quad \mathbb E_\mu T\le m(2+L_0+L_1).\]

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.

Download module (.lean)

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)

Exact module and namespace context

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

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ApproximateProximalExecution.proximalQuery

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.

Samplinglib mathematical lesson

Counted phase work

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.CountedPhaseProgram.implemented_phase_expected_query_work · theorem · Teaching coverage

Read this first

Mathematical statement

Under mu=nu product ((Gaussian product Gaussian) product (Gaussian Fin-m array product Gaussian Fin-m array)), set d=finrank(E), a=exp(-h/2), sigma=sqrt(1-exp(-h)), MR=M+(1-exp(-h))*d, B=6MR+3eps^2+3eta*d, C=2+(1+log((1-c)^(-1)))/(-log c), L0=C[1+log(1+sqrt(2MR)/eps)], L1=C[1+log(1+sqrt(4MR+2S^2B)/eps)]. There exist measurable p,q,N with exact proximal equation, ||q(y)-p(y)||≤eps and successful proximalQuery from y with fuel N(y)+1 returning (q(y),N(y)+1) for every y. P0=aP+sigma zeta0, Y0_i=X+t_i P0, Z0_j=grad V(q(Y0_j)+sqrt(eta)G0_j), Y1_i=Y0_i-sum_j omega_ij Z0_j, Z1_j=grad V(q(Y1_j)+sqrt(eta)G1_j), Phi=(X+hP0-sum_j positionWeight_j Z1_j, a(P0-sum_j momentumWeight_j Z1_j)+sigma zeta1). The same Phi is measurable and defines the Gaussian pushforward Markov kernel. The count T=2*m+sum_i[(N(Y0_i)+1)+(N(Y1_i)+1)] is measurable. For every driving input w, phaseQuery with fuel(y)=N(y)+1 returns exactly some(Phi(w),T(w)); the real cast of T is integrable under mu and E_mu T≤m*(2+L0+L1).

\[T=2m+\sum_{i=0}^{m-1}\bigl[N(Y_i^0)+1+N(Y_i^1)+1\bigr],\quad \mathbb E_\mu T\le m(2+L_0+L_1).\]

Lean statement · implemented_phase_expected_query_work

Exact finite arrays, full input/return types, parameters and counting boundary are retained in Lean.

Download module (.lean)

theorem implemented_phase_expected_query_work {m : ℕ} {V : E → ℝ} {κ : ℝ≥0}
    (hκ : 1 ≤ κ) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E, (κ : ℝ)⁻¹ * ‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ ‖v‖^2)
    {eta c eps : ℝ} (heta : 0 < eta) (hec : eta ≤ c) (hc : c < 1) (heps : 0 < eps)
    (ν : Measure (E × E)) [IsProbabilityMeasure ν]
    (xstar : E) (hstar : gradient V xstar = 0)
    {h M S : ℝ} (hh : 0 ≤ h) (hM : 0 ≤ M) (hS : 0 ≤ S)
    (hstateI : Integrable (fun s : E × E => ‖s.1-xstar‖^2 + ‖s.2‖^2) ν)
    (hstate : (∫ s : E × E, ‖s.1-xstar‖^2 + ‖s.2‖^2 ∂ν) ≤ M)
    (t : Fin m → ℝ) (ht : ∀ i, |t i| ≤ 1) (omega : Fin m → Fin m → ℝ)
    (hrow : ∀ i, (∑ j, |omega i j|) ≤ S)
    (positionWeight momentumWeight : Fin m → ℝ) :
    let a := Real.exp (-h/2)
    let sigma := Real.sqrt (1-Real.exp (-h))
    let gi := Measure.pi (fun _ : Fin m => stdGaussian E)
    let γ := ((stdGaussian E).prod (stdGaussian E)).prod (gi.prod gi)
    let μ := ν.prod γ
    let MR := M + (1-Real.exp (-h)) * (Module.finrank ℝ E : ℝ)
    let B := 6*MR + 3*eps^2 + 3*eta*(Module.finrank ℝ E : ℝ)
    let C := 2 + (1+Real.log ((1-c)⁻¹))/(-Real.log c)
    let L0 := C*(1+Real.log (1+Real.sqrt (2*MR)/eps))
    let L1 := C*(1+Real.log (1+Real.sqrt (4*MR+2*S^2*B)/eps))
    ∃ p q : E → E, ∃ N : E → ℕ,
      Measurable p ∧ Measurable q ∧ Measurable N ∧
      (∀ y, p y + eta • gradient V (p y) = y ∧ ‖q y-p y‖ ≤ eps ∧
        ApproximateProximalExecution.proximalQuery (gradient V) eta eps y (N y+1) y =
          some (q y,N y+1)) ∧
      let P0 := fun w : (E × E) × ((E × E) × ((Fin m → E) × (Fin m → E))) =>
        a • w.1.2 + sigma • w.2.1.1
      let Y0 := fun i w => w.1.1 + t i • P0 w
      let Z0 := fun j w => gradient V (q (Y0 j w) + Real.sqrt eta • w.2.2.1 j)
      let Y1 := fun i w => Y0 i w - ∑ j, omega i j • Z0 j w
      let Z1 := fun j w => gradient V (q (Y1 j w) + Real.sqrt eta • w.2.2.2 j)
      let Φ := fun w => (w.1.1 + h • P0 w - ∑ j, positionWeight j • Z1 j w,
        a • (P0 w - ∑ j, momentumWeight j • Z1 j w) + sigma • w.2.1.2)
      let T := fun w => 2*m+∑ i, ((N (Y0 i w)+1)+(N (Y1 i w)+1))
      Measurable Φ ∧ Measurable T ∧
      (∃ K : Kernel (E × E) (E × E), IsMarkovKernel K ∧
        ∀ s, K s = γ.map (fun z => Φ (s,z))) ∧
      (∀ w, phaseQuery (gradient V) eta eps h t omega positionWeight momentumWeight
        (fun y => N y+1) w = some (Φ w,T w)) ∧
      Integrable (fun w => (T w : ℝ)) μ ∧
      (∫ w, (T w : ℝ) ∂μ) ≤ (m : ℝ)*(2+L0+L1)

Exact module and namespace context

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.
3Use one actual full-law witness
The existing full-phase moments/work theorem supplies the same measurable p,q,N, full phase map and kernel, with both count integrabilities and the bounds L0,L1 under mu. No center moment, count-integrability or expected-query bound is introduced as a new premise. The execution identity applies its global successful proximal runs directly, with certified fuel N(y)+1.
4Prove measurable and integrable total actual cost
The C2 gradient is measurable, as are the stopped q/N and finite center maps. Therefore the natural count T is measurable. Cast the finite natural sum to the reals. Its constant part is integrable under the full probability law; each first- and second-layer count has L1 integrability supplied by the actual-law parent, so finite addition proves L1 integrability of the actual program count.
5Integrate and sum the actual query bounds
Use integral_add and integral_finsetSum only after establishing their integrability hypotheses. For each index the two count expectations add to at most L0+L1. Summing over Fin m gives m*(L0+L1); probability normalization makes the constant contribution exactly 2*m. Ring arithmetic yields m*(2+L0+L1). All inputs and costs use the same full Gaussian law.

Full assumptions and notation

All objects and hypotheses

E is a complete finite-dimensional real inner-product space with Borel sigma-algebra; the actual array index is Fin m for supplied natural m, not silently the source J.
V is C2, kappa≥1, and kappa^(-1)||v||^2 ≤ D2V(x)[v,v] ≤ ||v||^2 for all x,v. Its actual gradient vanishes at the supplied xstar.
0<eta≤c<1, eps>0, h≥0, M≥0, S≥0. The incoming probability law nu on (X,P) has integrable ||X-xstar||^2+||P||^2, with integral at most M.
The supplied deterministic nodes satisfy |t_i|≤1 and each supplied omega row satisfies sum_j |omega_ij|≤S. Position and momentum weights are arbitrary supplied real arrays; source Chebyshev quadrature is not instantiated.

Mathematical proof

1. Execute a finite successful query array

\[\operatorname{collect}(r_i)=(x_i,\sum_i c_i)\quad\text{if }r_i=\operatorname{some}(x_i,c_i).\]

Corresponding Lean step

collectQueries; collectQueries_some

2. Run the actual two-layer program

\[T=2m+\sum_{i=0}^{m-1}\bigl[N(Y_i^0)+1+N(Y_i^1)+1\bigr],\quad \mathbb E_\mu T\le m(2+L_0+L_1).\]

Corresponding Lean step

phaseQuery; phaseQuery_success; Finset.sum_add_distrib

3. Use one actual full-law witness

The existing full-phase moments/work theorem supplies the same measurable p,q,N, full phase map and kernel, with both count integrabilities and the bounds L0,L1 under mu. No center moment, count-integrability or expected-query bound is introduced as a new premise. The execution identity applies its global successful proximal runs directly, with certified fuel N(y)+1.

\[\operatorname{phaseQuery}(w)=\operatorname{some}(\Phi(w),T(w)).\]

Corresponding Lean step

ImplementedPhaseWork.implemented_phase_query_moments_and_work; phaseQuery_success

4. Prove measurable and integrable total actual cost

The C2 gradient is measurable, as are the stopped q/N and finite center maps. Therefore the natural count T is measurable. Cast the finite natural sum to the reals. Its constant part is integrable under the full probability law; each first- and second-layer count has L1 integrability supplied by the actual-law parent, so finite addition proves L1 integrability of the actual program count.

\[T\in L^1(\mu),\qquad \mu(\Omega)=1.\]

Corresponding Lean step

fun_prop; Nat.cast_sum; integrable_finsetSum; Integrable.add

5. Integrate and sum the actual query bounds

Use integral_add and integral_finsetSum only after establishing their integrability hypotheses. For each index the two count expectations add to at most L0+L1. Summing over Fin m gives m*(L0+L1); probability normalization makes the constant contribution exactly 2*m. Ring arithmetic yields m*(2+L0+L1). All inputs and costs use the same full Gaussian law.

\[T=2m+\sum_{i=0}^{m-1}\bigl[N(Y_i^0)+1+N(Y_i^1)+1\bigr],\quad \mathbb E_\mu T\le m(2+L_0+L_1).\]

Corresponding Lean step

integral_add; integral_finsetSum; Finset.sum_le_sum; probReal_univ; ring

Lean verification

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

Lean proof · implemented_phase_expected_query_work

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.

Download module (.lean)

theorem implemented_phase_expected_query_work {m : ℕ} {V : E → ℝ} {κ : ℝ≥0}
    (hκ : 1 ≤ κ) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E, (κ : ℝ)⁻¹ * ‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ ‖v‖^2)
    {eta c eps : ℝ} (heta : 0 < eta) (hec : eta ≤ c) (hc : c < 1) (heps : 0 < eps)
    (ν : Measure (E × E)) [IsProbabilityMeasure ν]
    (xstar : E) (hstar : gradient V xstar = 0)
    {h M S : ℝ} (hh : 0 ≤ h) (hM : 0 ≤ M) (hS : 0 ≤ S)
    (hstateI : Integrable (fun s : E × E => ‖s.1-xstar‖^2 + ‖s.2‖^2) ν)
    (hstate : (∫ s : E × E, ‖s.1-xstar‖^2 + ‖s.2‖^2 ∂ν) ≤ M)
    (t : Fin m → ℝ) (ht : ∀ i, |t i| ≤ 1) (omega : Fin m → Fin m → ℝ)
    (hrow : ∀ i, (∑ j, |omega i j|) ≤ S)
    (positionWeight momentumWeight : Fin m → ℝ) :
    let a := Real.exp (-h/2)
    let sigma := Real.sqrt (1-Real.exp (-h))
    let gi := Measure.pi (fun _ : Fin m => stdGaussian E)
    let γ := ((stdGaussian E).prod (stdGaussian E)).prod (gi.prod gi)
    let μ := ν.prod γ
    let MR := M + (1-Real.exp (-h)) * (Module.finrank ℝ E : ℝ)
    let B := 6*MR + 3*eps^2 + 3*eta*(Module.finrank ℝ E : ℝ)
    let C := 2 + (1+Real.log ((1-c)⁻¹))/(-Real.log c)
    let L0 := C*(1+Real.log (1+Real.sqrt (2*MR)/eps))
    let L1 := C*(1+Real.log (1+Real.sqrt (4*MR+2*S^2*B)/eps))
    ∃ p q : E → E, ∃ N : E → ℕ,
      Measurable p ∧ Measurable q ∧ Measurable N ∧
      (∀ y, p y + eta • gradient V (p y) = y ∧ ‖q y-p y‖ ≤ eps ∧
        ApproximateProximalExecution.proximalQuery (gradient V) eta eps y (N y+1) y =
          some (q y,N y+1)) ∧
      let P0 := fun w : (E × E) × ((E × E) × ((Fin m → E) × (Fin m → E))) =>
        a • w.1.2 + sigma • w.2.1.1
      let Y0 := fun i w => w.1.1 + t i • P0 w
      let Z0 := fun j w => gradient V (q (Y0 j w) + Real.sqrt eta • w.2.2.1 j)
      let Y1 := fun i w => Y0 i w - ∑ j, omega i j • Z0 j w
      let Z1 := fun j w => gradient V (q (Y1 j w) + Real.sqrt eta • w.2.2.2 j)
      let Φ := fun w => (w.1.1 + h • P0 w - ∑ j, positionWeight j • Z1 j w,
        a • (P0 w - ∑ j, momentumWeight j • Z1 j w) + sigma • w.2.1.2)
      let T := fun w => 2*m+∑ i, ((N (Y0 i w)+1)+(N (Y1 i w)+1))
      Measurable Φ ∧ Measurable T ∧
      (∃ K : Kernel (E × E) (E × E), IsMarkovKernel K ∧
        ∀ s, K s = γ.map (fun z => Φ (s,z))) ∧
      (∀ w, phaseQuery (gradient V) eta eps h t omega positionWeight momentumWeight
        (fun y => N y+1) w = some (Φ w,T w)) ∧
      Integrable (fun w => (T w : ℝ)) μ ∧
      (∫ w, (T w : ℝ) ∂μ) ≤ (m : ℝ)*(2+L0+L1) := by
  classical
  dsimp only
  let gi := Measure.pi (fun _ : Fin m => stdGaussian E)
  let γ := ((stdGaussian E).prod (stdGaussian E)).prod (gi.prod gi)
  let μ := ν.prod γ
  let MR := M+(1-Real.exp (-h))*(Module.finrank ℝ E : ℝ)
  let B := 6*MR+3*eps^2+3*eta*(Module.finrank ℝ E : ℝ)
  let C := 2+(1+Real.log ((1-c)⁻¹))/(-Real.log c)
  let L0 := C*(1+Real.log (1+Real.sqrt (2*MR)/eps))
  let L1 := C*(1+Real.log (1+Real.sqrt (4*MR+2*S^2*B)/eps))
  obtain ⟨p,q,N,hp,hq,hN,hall,hΦ,K,hK,hKlaw,hw0,hw1⟩ :=
    ImplementedPhaseWork.implemented_phase_query_moments_and_work hκ hV hH heta hec hc heps
      ν xstar hstar hh hM hS hstateI hstate t ht omega hrow positionWeight momentumWeight
  let P0 := fun w : (E × E) × ((E × E) × ((Fin m → E) × (Fin m → E))) =>
    Real.exp (-h/2) • w.1.2+Real.sqrt (1-Real.exp (-h)) • w.2.1.1
  let Y0 := fun i w => w.1.1+t i • P0 w
  let Z0 := fun j w => gradient V (q (Y0 j w)+Real.sqrt eta • w.2.2.1 j)
  let Y1 := fun i w => Y0 i w-∑ j, omega i j • Z0 j w
  let T := fun w => 2*m+∑ i, ((N (Y0 i w)+1)+(N (Y1 i w)+1))
  have hg : Measurable (gradient V) := by
    unfold gradient
    exact ((InnerProductSpace.toDual ℝ E).symm.continuous.comp
      (hV.continuous_fderiv (by norm_num))).measurable
  have hTm : Measurable T := by fun_prop
  have hi0 (i : Fin m) : Integrable (fun w => (N (Y0 i w) : ℝ)+1) μ :=
    (hw0 i).2.2.1
  have hi1 (i : Fin m) : Integrable (fun w => (N (Y1 i w) : ℝ)+1) μ :=
    (hw1 i).2.2.1
  have hsum : Integrable (fun w => ∑ i, (((N (Y0 i w) : ℝ)+1)+
      ((N (Y1 i w) : ℝ)+1))) μ :=
    integrable_finsetSum Finset.univ (fun i _ => (hi0 i).add (hi1 i))
  have hTex : (fun w => (T w : ℝ)) = fun w => 2*(m : ℝ)+
      ∑ i, (((N (Y0 i w) : ℝ)+1)+((N (Y1 i w) : ℝ)+1)) := by
    funext w
    simp only [T, Nat.cast_add, Nat.cast_mul, Nat.cast_ofNat, Nat.cast_sum, Nat.cast_one]
  have hTi : Integrable (fun w => (T w : ℝ)) μ := by
    rw [hTex]
    exact (integrable_const (2*(m : ℝ))).add hsum
  refine ⟨p,q,N,hp,hq,hN,hall,hΦ,hTm,⟨K,hK,hKlaw⟩,?_,hTi,?_⟩
  · intro w
    exact phaseQuery_success (gradient V) q N (fun y => N y+1) eta eps h t omega
      positionWeight momentumWeight (fun y => (hall y).2.2) w
  · change (∫ w, (T w : ℝ) ∂μ) ≤ (m : ℝ)*(2+L0+L1)
    rw [hTex, integral_add (integrable_const _) hsum]
    rw [integral_finsetSum (f := fun i w => ((N (Y0 i w) : ℝ)+1)+
      ((N (Y1 i w) : ℝ)+1)) Finset.univ (fun i _ => (hi0 i).add (hi1 i))]
    have hb : (∑ i : Fin m, ∫ w, (((N (Y0 i w) : ℝ)+1)+
        ((N (Y1 i w) : ℝ)+1)) ∂μ) ≤ ∑ _i : Fin m, (L0+L1) := by
      apply Finset.sum_le_sum
      intro i _
      rw [integral_add (hi0 i) (hi1 i)]
      exact add_le_add (hw0 i).2.2.2 (hw1 i).2.2.2
    calc
      _ ≤ (∫ _w, 2*(m : ℝ) ∂μ)+∑ _i : Fin m, (L0+L1) := add_le_add_right hb _
      _ = (m : ℝ)*(2+L0+L1) := by
        simp [integral_const, Finset.sum_const, nsmul_eq_mul]
        ring

end ExpectedWork

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.CountedPhaseProgram

Exact module and namespace context

Scope and omitted-condition boundaries

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 — 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.