AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseAccuracyWork

Samplinglib mathematical lesson

Actual phase accuracy and expected work with identical witnesses

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseAccuracyWork.source_phase_accuracy_and_work · theorem · Teaching coverage

Read this first

Mathematical statement

There exist one measurable exact optimality map p, one measurable stopped output map q and one measurable N:E→Nat such that p(y)+eta*gradient V(p(y))=y, ||q(y)-p(y)||≤eps, p is nonexpansive and the actual residual-stopped interpreter from y returns some(q(y),N(y)+1) with sufficient fuel N(y)+1. The identical p,q,N define actual full-phase Markov Kp,Kq, the actual output Phi_q and the actual total returned gradient count T. For every state s and finite real rho≥1, true Euclidean W_rho(Kq(s),Kp(s))≤3hLambda eps. Under the same actual driving law mu=nu prod gamma, T is measurable, real-integrable and E_mu[T]≤J(2+L0+L1). For every driving input w the counted phase interpreter with fuel(y)=N(y)+1 returns exactly some(Phi_q(w),T(w)). All output/count/kernel/cost conjuncts share these witnesses.

\[W_\rho(K_q(s),K_p(s))\le3h\Lambda_J\varepsilon\quad(\rho\ge1),\qquad\mathbb E_{\nu\otimes\gamma}T\le J(2+L_0+L_1).\]

Lean statement · source_phase_accuracy_and_work

Exact statement includes genuine source arrays, all four Gaussian factors, actual nu prod gamma input law, full phase maps, precise returned count and Euclidean transport.

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 source_phase_accuracy_and_work {J : ℕ} (hJ : 2 ≤ J) {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 : ℝ} (hh : 0 < h) (hM : 0 ≤ M)
    (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)
:
    let t := fun i : Fin J => h/2*(1-Real.cos ((i : ℝ)/(J-1 : ℝ)*Real.pi))
    let ell := fun j : Fin J => Lagrange.basis Finset.univ t j
    let Lambda := sSup ((fun s : ℝ => ∑ j : Fin J, |(ell j).eval s|) '' Set.Icc 0 h)
    let omega := fun i j : Fin J => ∫ s in 0..t i, (t i-s)*(ell j).eval s
    let positionWeight := omega ⟨J-1,by omega⟩
    let momentumWeight := fun j : Fin J => ∫ s in 0..h, (ell j).eval s
    let S := h^2/2*Lambda
    let a := Real.exp (-h/2)
    let sigma := Real.sqrt (1-Real.exp (-h))
    let gi := Measure.pi (fun _ : Fin J => 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))
    h^2*Lambda ≤ 1 →
    ∃ 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)) ∧ LipschitzWith 1 p ∧
      let P0 := fun w : (E × E) × ((E × E) × ((Fin J → E) × (Fin J → 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*J+∑ i, ((N (Y0 i w)+1)+(N (Y1 i w)+1))
      let Z0p := fun j w => gradient V (p (Y0 j w) + Real.sqrt eta • w.2.2.1 j)
      let Y1p := fun i w => Y0 i w - ∑ j, omega i j • Z0p j w
      let Z1p := fun j w => gradient V (p (Y1p j w) + Real.sqrt eta • w.2.2.2 j)
      let Φp := fun w => (w.1.1 + h • P0 w - ∑ j, positionWeight j • Z1p j w,
        a • (P0 w - ∑ j, momentumWeight j • Z1p j w) + sigma • w.2.1.2)
      let W := fun (rho : ℝ) (μ ν : Measure (E × E)) =>
        (TechnicalLemmas.Measure.Transport.transportCost
          (fun z : (E × E) × (E × E) =>
            (ENNReal.ofReal (Real.sqrt (‖z.1.1-z.2.1‖^2+‖z.1.2-z.2.2‖^2)))^rho)
          μ ν)^(rho⁻¹)
      Measurable Φ ∧ Measurable T ∧
      ∃ Kp Kq : Kernel (E × E) (E × E), IsMarkovKernel Kp ∧ IsMarkovKernel Kq ∧
      (∀ s, Kp s = γ.map (fun z => Φp (s,z))) ∧
      (∀ s, Kq s = γ.map (fun z => Φ (s,z))) ∧
      (∀ w, CountedPhaseProgram.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 : ℝ) ∂μ) ≤ (J : ℝ)*(2+L0+L1) ∧
      ∀ s rho, 1 ≤ rho → W rho (Kq s) (Kp s) ≤ ENNReal.ofReal (3*h*Lambda*eps)

Exact module and namespace context

Proof roadmap

1Discharge the genuine step adapter
The compiled actual source coefficient certificate proves Lambda≥1. Combined with h>0 and h²Lambda≤1 it yields h²≤1 and h≤1. Thus the actual-work producer is callable with no new small-step premise.
2Obtain both genuine producers
Use the actual source quadrature expected-work theorem for p_c,q_c,N_c and the precision theorem for p_a,q_a,N_a,Kp,Kq. Their gradient, eta, eps, starting state and all source arrays are identical; c may affect the certificate but never the interpreter. Both exact maps satisfy the genuine optimality equation.
3Identify the exact optimality map
Derive 1-Lipschitz gradient from the actual C2 Hessian via the shared zero-quadratic specialization. Subtract the exact equations: the displacement equals eta times the reversed gradient displacement. Its norm is ≤eta times itself; eta<1 forces zero. This proves p_c=p_a without assuming witness identity.
4Identify stopped points and returned counts
Both successful calls use exactly the same residual branch norm(y-eta*g(x)-x)≤(1-eta)*eps, anchor y and starting x=y. Deterministic successful_query_unique identifies their returned point/count pairs independently of the supplied sufficient fuel. Take each projection and cancel +1 on natural counts; obtain q_c=q_a and N_c=N_a.
5Retain the real phase and driving measure
For a=exp(-h/2), sigma=sqrt(1-exp(-h)), P0=aP+sigma*zeta0, let Y0_i=X+t_iP0, Z0_f,j=g(f(Y0_j)+sqrt(eta)G0_j), Y1_f,i=Y0_i-sum_j omega_ij Z0_f,j and Z1_f,j=g(f(Y1_f,j)+sqrt(eta)G1_j). Phi_f=(X+hP0-sum pw_j Z1_f,j, a(P0-sum b_j Z1_f,j)+sigma*zeta1). gamma is the independent product law of zeta0,zeta1,G0,G1; K_f(s)=gamma.map(z↦Phi_f(s,z)). Substituting the proven function identities makes the actual interpreter output, count and precision kernel exactly the same phase.
6Join the two guarantees with explicit constants
Let d=finrank_R E, MR=M+(1-exp(-h))*d, S=h²Lambda/2, B=6MR+3eps²+3eta*d, C=2+(1+log((1-c)^(-1)))/(-log c), L0=C[1+log(1+sqrt(2MR)/eps)] and L1=C[1+log(1+sqrt(4MR+2S²B)/eps)]. Carry integrability and the actual mu-expectation from the cost producer, and all-state/all-finite-rho Euclidean precision from the now-identical accuracy kernel. The cost is evaluated on the actual incoming law nu prod gamma; no discrepancy bound is used to transfer an unbounded expectation.

Full assumptions and notation

All objects and hypotheses

E is a complete finite-dimensional real inner-product space with its Borel sigma algebra, including dimension zero. V:E→R is C2; kappa≥1 and kappa^-1||v||²≤D²V(x)[v,v]≤||v||² for every x,v (normalized beta=1).
J≥2; h>0; actual t_i=h/2(1-cos(i*pi/(J-1))), i=0,...,J-1; ell_j=Lagrange.basis(univ,t,j); Lambda=sup_{s∈[0,h]}sum_j|ell_j(s)|; omega_ij=integral_0^{t_i}(t_i-s)ell_j(s) ds; pw is the final omega row and b_j=integral_0^h ell_j(s) ds. Assume only h²Lambda≤1; h≤1 is derived.
0<eta≤c<1 and eps>0. c is a contraction upper-bound parameter in the cost certificate, not an algorithm parameter or additional gradient query.
nu is the actual incoming phase-state probability measure. xstar∈E satisfies gradient V(xstar)=0; M≥0. The real function ||X-xstar||²+||P||² is nu-integrable and its nu-expectation is ≤M. These actual-state moment hypotheses are explicit; no TV approximation or independently sampled proxy law is substituted.
gamma=((stdGaussian(E) prod stdGaussian(E)) prod (gi prod gi)), where gi=Measure.pi_{Fin J}(stdGaussian(E)); all four factors and each array coordinate are independent. mu=nu prod gamma. Write w=((X,P),((zeta0,zeta1),(G0,G1))), a=exp(-h/2), sigma=sqrt(1-exp(-h)) and P0=aP+sigma*zeta0.
For any f:E→E define Y0_i=X+t_iP0, Z0_f,j=gradient V(f(Y0_j)+sqrt(eta)G0_j), Y1_f,i=Y0_i-sum_j omega_ij Z0_f,j, Z1_f,j=gradient V(f(Y1_f,j)+sqrt(eta)G1_j) and Phi_f(w)=(X+hP0-sum_j pw_j Z1_f,j, a(P0-sum_j b_j Z1_f,j)+sigma*zeta1). The exact and approximate branches have their own Y1_f. For the constructed q,N set T(w)=2J+sum_i[(N(Y0_i(w))+1)+(N(Y1_q,i(w))+1)].
Set d=finrank_R E, S=h²Lambda/2, MR=M+(1-exp(-h))*d, B=6MR+3eps²+3eta*d, C=2+(1+log((1-c)^(-1)))/(-log c), L0=C*(1+log(1+sqrt(2MR)/eps)) and L1=C*(1+log(1+sqrt(4MR+2S²B)/eps)). W_rho(mu1,mu2) is [inf_{pi coupling(mu1,mu2)} integral (sqrt(||DX||²+||DP||²))^rho dpi]^(1/rho), expressed in extended nonnegative reals, for every finite real rho≥1.

Mathematical proof

1. Discharge the genuine step adapter

The compiled actual source coefficient certificate proves Lambda≥1. Combined with h>0 and h²Lambda≤1 it yields h²≤1 and h≤1. Thus the actual-work producer is callable with no new small-step premise.

\[1\le\Lambda_J,\quad h^2\Lambda_J\le1,\quad h>0\Longrightarrow h\le1.\]

Corresponding Lean step

chebyshev_lobatto_coefficients; hLambda; hh1

2. Obtain both genuine producers

Use the actual source quadrature expected-work theorem for p_c,q_c,N_c and the precision theorem for p_a,q_a,N_a,Kp,Kq. Their gradient, eta, eps, starting state and all source arrays are identical; c may affect the certificate but never the interpreter. Both exact maps satisfy the genuine optimality equation.

\[p_c(y)+\eta g(p_c(y))=y=p_a(y)+\eta g(p_a(y)),\qquad g=\nabla V.\]

Corresponding Lean step

SourceQuadratureWork.source_quadrature_phase_work; ProximalPhaseStability.source_phase_proximal_stability

3. Identify the exact optimality map

Derive 1-Lipschitz gradient from the actual C2 Hessian via the shared zero-quadratic specialization. Subtract the exact equations: the displacement equals eta times the reversed gradient displacement. Its norm is ≤eta times itself; eta<1 forces zero. This proves p_c=p_a without assuming witness identity.

\[\|p_c(y)-p_a(y)\|\le\eta\|p_c(y)-p_a(y)\|,\quad\eta<1\Longrightarrow p_c=p_a.\]

Corresponding Lean step

QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadratic; hg; hpEq; norm_smul; norm_sub_le

4. Identify stopped points and returned counts

Both successful calls use exactly the same residual branch norm(y-eta*g(x)-x)≤(1-eta)*eps, anchor y and starting x=y. Deterministic successful_query_unique identifies their returned point/count pairs independently of the supplied sufficient fuel. Take each projection and cancel +1 on natural counts; obtain q_c=q_a and N_c=N_a.

\[(q_c(y),N_c(y)+1)=(q_a(y),N_a(y)+1)\Longrightarrow q_c=q_a,\ N_c=N_a.\]

Corresponding Lean step

ProximalExecutionIdentity.successful_query_unique; hpair; hqEq; hNEq; Prod.fst; Prod.snd; Nat.add_right_cancel

5. Retain the real phase and driving measure

For a=exp(-h/2), sigma=sqrt(1-exp(-h)), P0=aP+sigma*zeta0, let Y0_i=X+t_iP0, Z0_f,j=g(f(Y0_j)+sqrt(eta)G0_j), Y1_f,i=Y0_i-sum_j omega_ij Z0_f,j and Z1_f,j=g(f(Y1_f,j)+sqrt(eta)G1_j). Phi_f=(X+hP0-sum pw_j Z1_f,j, a(P0-sum b_j Z1_f,j)+sigma*zeta1). gamma is the independent product law of zeta0,zeta1,G0,G1; K_f(s)=gamma.map(z↦Phi_f(s,z)). Substituting the proven function identities makes the actual interpreter output, count and precision kernel exactly the same phase.

\[T(w)=2J+\sum_i[(N(Y_i^0(w))+1)+(N(Y_{q,i}^1(w))+1)],\qquad K_q(s)=(\Phi_q(s,\cdot))_\#\gamma.\]

Corresponding Lean step

subst p2; subst q2; subst N2; hKppush; hKqpush; hrun1

6. Join the two guarantees with explicit constants

Let d=finrank_R E, MR=M+(1-exp(-h))*d, S=h²Lambda/2, B=6MR+3eps²+3eta*d, C=2+(1+log((1-c)^(-1)))/(-log c), L0=C[1+log(1+sqrt(2MR)/eps)] and L1=C[1+log(1+sqrt(4MR+2S²B)/eps)]. Carry integrability and the actual mu-expectation from the cost producer, and all-state/all-finite-rho Euclidean precision from the now-identical accuracy kernel. The cost is evaluated on the actual incoming law nu prod gamma; no discrepancy bound is used to transfer an unbounded expectation.

\[M_R=M+(1-e^{-h})d,\ S=\tfrac12h^2\Lambda_J,\ B=6M_R+3\varepsilon^2+3\eta d,\quad \mathbb E_{\nu\otimes\gamma}T\le J(2+L_0+L_1).\]

Corresponding Lean step

hPhi1; hT1; hTI1; hcost1; hW; final same-witness tuple

Lean verification

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

Lean proof · source_phase_accuracy_and_work

The whole current module has one public theorem. Both existential producer witnesses are identified by genuine optimality contraction and actual successful-run identity before returning the combined guarantees.

Download module (.lean)

theorem source_phase_accuracy_and_work {J : ℕ} (hJ : 2 ≤ J) {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 : ℝ} (hh : 0 < h) (hM : 0 ≤ M)
    (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)
:
    let t := fun i : Fin J => h/2*(1-Real.cos ((i : ℝ)/(J-1 : ℝ)*Real.pi))
    let ell := fun j : Fin J => Lagrange.basis Finset.univ t j
    let Lambda := sSup ((fun s : ℝ => ∑ j : Fin J, |(ell j).eval s|) '' Set.Icc 0 h)
    let omega := fun i j : Fin J => ∫ s in 0..t i, (t i-s)*(ell j).eval s
    let positionWeight := omega ⟨J-1,by omega⟩
    let momentumWeight := fun j : Fin J => ∫ s in 0..h, (ell j).eval s
    let S := h^2/2*Lambda
    let a := Real.exp (-h/2)
    let sigma := Real.sqrt (1-Real.exp (-h))
    let gi := Measure.pi (fun _ : Fin J => 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))
    h^2*Lambda ≤ 1 →
    ∃ 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)) ∧ LipschitzWith 1 p ∧
      let P0 := fun w : (E × E) × ((E × E) × ((Fin J → E) × (Fin J → 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*J+∑ i, ((N (Y0 i w)+1)+(N (Y1 i w)+1))
      let Z0p := fun j w => gradient V (p (Y0 j w) + Real.sqrt eta • w.2.2.1 j)
      let Y1p := fun i w => Y0 i w - ∑ j, omega i j • Z0p j w
      let Z1p := fun j w => gradient V (p (Y1p j w) + Real.sqrt eta • w.2.2.2 j)
      let Φp := fun w => (w.1.1 + h • P0 w - ∑ j, positionWeight j • Z1p j w,
        a • (P0 w - ∑ j, momentumWeight j • Z1p j w) + sigma • w.2.1.2)
      let W := fun (rho : ℝ) (μ ν : Measure (E × E)) =>
        (TechnicalLemmas.Measure.Transport.transportCost
          (fun z : (E × E) × (E × E) =>
            (ENNReal.ofReal (Real.sqrt (‖z.1.1-z.2.1‖^2+‖z.1.2-z.2.2‖^2)))^rho)
          μ ν)^(rho⁻¹)
      Measurable Φ ∧ Measurable T ∧
      ∃ Kp Kq : Kernel (E × E) (E × E), IsMarkovKernel Kp ∧ IsMarkovKernel Kq ∧
      (∀ s, Kp s = γ.map (fun z => Φp (s,z))) ∧
      (∀ s, Kq s = γ.map (fun z => Φ (s,z))) ∧
      (∀ w, CountedPhaseProgram.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 : ℝ) ∂μ) ≤ (J : ℝ)*(2+L0+L1) ∧
      ∀ s rho, 1 ≤ rho → W rho (Kq s) (Kp s) ≤ ENNReal.ofReal (3*h*Lambda*eps) := by
  classical
  dsimp only
  intro hstep
  obtain ⟨_,_,_,_,_,hLambda,_,_⟩ :=
    TechnicalLemmas.Analysis.ChebyshevLobattoQuadrature.chebyshev_lobatto_coefficients hJ hh
  have hh1 : h ≤ 1 := by
    have hsq : h^2 ≤ 1 := (le_mul_of_one_le_right (sq_nonneg h) hLambda).trans hstep
    nlinarith only [hsq,hh]
  have heta1 : eta < 1 := hec.trans_lt hc
  obtain ⟨p1,q1,N1,hp1,hq1,hN1,hall1,hPhi1,hT1,_,hrun1,hTI1,hcost1⟩ :=
    SourceQuadratureWork.source_quadrature_phase_work hJ hκ hV hH heta hec hc heps
      ν xstar hstar hh hh1 hM hstateI hstate
  obtain ⟨p2,q2,N2,hp2,hq2,hN2,hall2,hLip2,Kp,Kq,hKp,hKq,hKppush,hKqpush,hW,_⟩ :=
    ProximalPhaseStability.source_phase_proximal_stability hκ hV hH heta heta1 heps hJ hh hstep
  have hH' : ∀ x v : E, ((κ⁻¹ : ℝ≥0) : ℝ)*‖v‖^2 ≤
      (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (1 : ℝ≥0)*‖v‖^2 := by
    simpa only [NNReal.coe_inv,NNReal.coe_one,one_mul] using hH
  have hreg := TechnicalLemmas.Analysis.QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadratic
    (r := 0) hV hH' (0 : E)
  have hg : LipschitzWith 1 (gradient V) := by simpa using hreg.2
  have hpEq : p1 = p2 := by
    funext y
    have hop1 := (hall1 y).1
    have hop2 := (hall2 y).1
    have hd : p1 y-p2 y = eta • (gradient V (p2 y)-gradient V (p1 y)) := by
      calc
        p1 y-p2 y = (p1 y+eta • gradient V (p1 y)) -
            (p2 y+eta • gradient V (p2 y)) +
            eta • (gradient V (p2 y)-gradient V (p1 y)) := by module
        _ = eta • (gradient V (p2 y)-gradient V (p1 y)) := by rw [hop1,hop2]; simp
    have hn : ‖p1 y-p2 y‖ ≤ eta*‖p1 y-p2 y‖ := by
      calc
        ‖p1 y-p2 y‖ = eta*‖gradient V (p2 y)-gradient V (p1 y)‖ := by
          rw [hd,norm_smul,Real.norm_eq_abs,abs_of_pos heta]
        _ ≤ eta*‖p1 y-p2 y‖ := by
          have hb := hg.norm_sub_le (p2 y) (p1 y)
          simpa only [NNReal.coe_one,one_mul,norm_sub_rev] using
            mul_le_mul_of_nonneg_left hb heta.le
    have hz : ‖p1 y-p2 y‖ = 0 := by
      nlinarith only [hn,norm_nonneg (p1 y-p2 y),heta1]
    exact sub_eq_zero.mp (norm_eq_zero.mp hz)
  have hpair (y : E) : (q1 y,N1 y+1) = (q2 y,N2 y+1) :=
    ProximalExecutionIdentity.successful_query_unique (gradient V) eta eps y
      (hall1 y).2.2 (hall2 y).2.2
  have hqEq : q1 = q2 := by funext y; exact congrArg Prod.fst (hpair y)
  have hNEq : N1 = N2 := by
    funext y
    exact Nat.add_right_cancel (congrArg Prod.snd (hpair y))
  subst p2
  subst q2
  subst N2
  exact ⟨p1,q1,N1,hp1,hq1,hN1,hall1,hLip2,hPhi1,hT1,Kp,Kq,hKp,hKq,
    hKppush,hKqpush,hrun1,hTI1,hcost1,hW⟩

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseAccuracyWork

Exact module and namespace context

Scope and omitted-condition boundaries

One successful exact-real source two-layer phase with actual integral coefficients and all four Gaussian factors, joining real accuracy and expected returned query cost. The exact comparison phase uses exact proximal stochastic gradients, not deterministic gradient V_eta. N(y)+1 is a sufficient execution certificate, not a free runtime computation of N. Counts include terminal residual tests and 2J shifted noisy-gradient calls; arithmetic, random draws and failed-run cost are separate. No TV-to-unbounded-cost transfer. Run-wideD3 contraction/history/D7/D8, B2/depth-K/logarithmic Lambda/weight positivity/source parameter choices/smoothing/Wp/proxy-warmness/initialization/PBPS/main results and actual-input composition remain open.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

LipschitzWith.norm_sub_le
norm_smul
Real.norm_eq_abs
norm_sub_rev
norm_eq_zero
Nat.add_right_cancel
funext
Prod.fst
Prod.snd

Mathematical sources

SPHMC actual proximal implementation precision and expected work — One successful exact-real source two-layer phase with actual integral coefficients and all four Gaussian factors, joining real accuracy and expected returned query cost. The exact comparison phase uses exact proximal stochastic gradients, not deterministic gradient V_eta. N(y)+1 is a sufficient execution certificate, not a free runtime computation of N. Counts include terminal residual tests and 2J shifted noisy-gradient calls; arithmetic, random draws and failed-run cost are separate. No TV-to-unbounded-cost transfer. Run-wideD3 contraction/history/D7/D8, B2/depth-K/logarithmic Lambda/weight positivity/source parameter choices/smoothing/Wp/proxy-warmness/initialization/PBPS/main results and actual-input composition remain open.

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

PhaseAccuracyWork: mathematical reading route

Actual phase accuracy and expected work with identical witnesses

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Discharge the genuine step adapter

2. Obtain both genuine producers

3. Identify the exact optimality map

4. Identify stopped points and returned counts

5. Retain the real phase and driving measure

6. Join the two guarantees with explicit constants

Lean verification

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources