Counted phase work

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang; bounded ASTIS exact-real implementation component.

Complete source statement (Samplinglib restatement)

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

Actual successful phase work

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

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.

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

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

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

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

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

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.

Counted phase work

Complete source statement (Samplinglib restatement)

Actual successful phase work

Read the formalized proofs