ProximalPhaseStability actual source component

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang; explicitly bounded source component or shared prerequisite, not main-theorem completion.

Complete source statement (Samplinglib restatement)

Construct measurable exact p, actual stopped q and natural N for full0<eta<1, with p+eta gradientV(p)=id, ||q-p||<=eps and proximalQuery(g,eta,eps,y,N(y)+1,y)=some(q(y),N(y)+1). The exact p is nonexpansive. Construct Markov Kp and Kq as the full two-layer source Gaussian pushforwards. For every deterministic phase state s and finite real rho>=1, the Euclidean Wasserstein cost W_rho(Kq(s),Kp(s))<=3h Lambda eps. Moreover every measurable delta-accurate r has its true pushforward Markov Kr with W_rho(Kr(s),Kp(s))<=3h Lambda delta for all s and rho>=1, includingdelta0. Here W_rho is the 1/rho power of the infimum coupling integral of [sqrt(||DX||²+||DP||²)]^rho. It is not the default max-norm product metric.

Exact bounded formula

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

ProximalPhaseStability actual source component

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalPhaseStability.source_phase_proximal_stability · theorem · Teaching coverage

Read this first

Mathematical statement

Construct measurable exact p, actual stopped q and natural N for full0<eta<1, with p+eta gradientV(p)=id, ||q-p||≤eps and proximalQuery(g,eta,eps,y,N(y)+1,y)=some(q(y),N(y)+1). The exact p is nonexpansive. Construct Markov Kp and Kq as the full two-layer source Gaussian pushforwards. For every deterministic phase state s and finite real rho≥1, the Euclidean Wasserstein cost W_rho(Kq(s),Kp(s))≤3h Lambda eps. Moreover every measurable delta-accurate r has its true pushforward Markov Kr with W_rho(Kr(s),Kp(s))≤3h Lambda delta for all s and rho≥1, includingdelta0. Here W_rho is the 1/rho power of the infimum coupling integral of [sqrt(||DX||²+||DP||²)]^rho. It is not the default max-norm product metric.

\[W_\rho(\delta_sK_r,\delta_sK_p)\le3h\Lambda_J\delta,\qquad \rho\ge1,\quad\delta\ge0,\quad h^2\Lambda_J\le1.\]

Lean statement · source_phase_proximal_stability

Complete exact statement with all constructed source arrays, probability laws, terminal-query identities and Euclidean cost as applicable.

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_proximal_stability {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 eps : ℝ} (heta : 0 < eta) (heta1 : eta < 1) (heps : 0 < eps)
    {J : ℕ} (hJ : 2 ≤ J) {h : ℝ} (hh : 0 < h) :
    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 pw := omega ⟨J-1,by omega⟩
    let bw := fun j : Fin J => ∫ s in 0..h, (ell j).eval s
    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 γ := ((stdGaussian E).prod (stdGaussian E)).prod
        ((Measure.pi (fun _ : Fin J => stdGaussian E)).prod
          (Measure.pi (fun _ : Fin J => stdGaussian E)))
      let Φ := fun (f : E → E)
          (w : (E × E) × ((E × E) × ((Fin J → E) × (Fin J → E)))) =>
        let a := Real.exp (-h/2)
        let sigma := Real.sqrt (1-Real.exp (-h))
        let P0 := a • w.1.2 + sigma • w.2.1.1
        let Y0 := fun i => w.1.1+t i • P0
        let Z0 := fun j => gradient V (f (Y0 j)+Real.sqrt eta • w.2.2.1 j)
        let Y1 := fun i => Y0 i-∑ j, omega i j • Z0 j
        let Z1 := fun j => gradient V (f (Y1 j)+Real.sqrt eta • w.2.2.2 j)
        (w.1.1+h • P0-∑ j, pw j • Z1 j,
          a • (P0-∑ j, bw j • Z1 j)+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⁻¹)
      ∃ 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 => Φ q (s,z))) ∧
        (∀ s rho, 1 ≤ rho → W rho (Kq s) (Kp s) ≤ ENNReal.ofReal (3*h*Lambda*eps)) ∧
        (∀ (r : E → E), Measurable r → ∀ delta : ℝ, 0 ≤ delta →
          (∀ y, ‖r y-p y‖ ≤ delta) →
          ∃ Kr : Kernel (E × E) (E × E), IsMarkovKernel Kr ∧
            (∀ s, Kr s = γ.map (fun z => Φ r (s,z))) ∧
            ∀ s rho, 1 ≤ rho → W rho (Kr s) (Kp s) ≤
              ENNReal.ofReal (3*h*Lambda*delta))

Exact module and namespace context

Proof roadmap

1Construct and identify the actual proximal maps
Use the compiled full-range stopped execution kernel with contraction c=eta. It constructs one exact optimality solution p and its actual finite residual-stopped q,N. Derive gradient monotonicity and 1-Lipschitz gradient from the genuine C2 Hessian through the shared quadratic/first-order APIs, then apply the shared monotone-optimality implication. Strong convexity identifies this unique optimality solution with the source proximal minimizer; no p-nonexpansiveness premise or hidden eta≤1/2 restriction.
2Use the actual coefficients and preserve the same noise
Use the independent coefficient construction for Lambda≥1 and every omega row sum≤S=h²Lambda/2. Position weights are the final row. The new absolute momentum-integral prerequisite yields sum|b|≤hLambda. Set a=exp(-h/2), sigma=sqrt(1-exp(-h)); P0=aP+sigma*zeta0; both phases use the same P0 and independent G0,G1 arrays, and the same terminal zeta1.
3Propagate the two actual Picard layers
At Y0_i=X+t_iP0, common G0 cancels; gradient Lipschitz and ||r-p||≤delta give first gradient difference≤delta. Therefore ||Y1_r-Y1_p||≤S delta. In the second layer add and subtract p(Y1_r), use r accuracy and exact p nonexpansiveness, then cancel common G1 and use gradient Lipschitz. This works for delta=0 and does not assume r Lipschitz.
4Bound true Euclidean phase displacement
The full actual position difference is≤S(1+S)delta and momentum difference≤aB(1+S)delta. From Lambda≥1 and h²Lambda≤1 obtain h≤1, S≤1/2 and S≤B/2; also a≤1. The sum of these norms is≤9Bdelta/4≤3Bdelta. The Euclidean square-root norm is at most that sum by nonnegative cross product. Source prose uses momentum-weight positivity to give a sharper intermediate bound; this proof uses the independently derived absolute sum and keeps the same universal D2 scaling with explicit3, without adding an assumption.
5Construct actual kernels and a coupling for every finite rho
The product Gaussian law gamma contains both refreshes and both Fin J Gaussian arrays. Each full phase map is measurable by finite sums and composition. Map the product id/kernel-constant to construct each Markov kernel, retaining the existing actual Kq. For fixed s, gamma.map(z↦(Phi_r(s,z),Phi_p(s,z))) has exactly Kr(s) and Kp(s) marginals. The pointwise Euclidean displacement bounds its rho-cost integral by A^rho with A=3hLambda delta; probability normalization supplies the constant integral, so no incoming-state moment assumption is needed. Taking the monotone1/rho root gives the bound, for delta=0 as well.

Full assumptions and notation

All objects and hypotheses

E is a complete finite-dimensional real inner-product space with its Borel sigma algebra; dimension zero is allowed. V:E→R is genuinely C2, kappa≥1 and kappa^-1||v||²≤D²V(x)[v,v]≤||v||² for every x,v (normalized beta=1).
0<eta<1, eps>0 for the actual stopped approximate program. J≥2, h>0; the actual nodes, cardinal polynomials, Lambda, omega and b are defined as in the coefficient prerequisite. Position weights are the last omega row, whose node equals h. The sole step condition is h² Lambda≤1.
The abstract comparison oracle r is Borel measurable and uniformly satisfies ||r(y)-p(y)||≤delta for every y, with delta≥0 including0. No Lipschitz assumption on r, no state moment or integrability budget, no b positivity, no target-law approximation premise.

Mathematical proof

1. Construct and identify the actual proximal maps

Use the compiled full-range stopped execution kernel with contraction c=eta. It constructs one exact optimality solution p and its actual finite residual-stopped q,N. Derive gradient monotonicity and 1-Lipschitz gradient from the genuine C2 Hessian through the shared quadratic/first-order APIs, then apply the shared monotone-optimality implication. Strong convexity identifies this unique optimality solution with the source proximal minimizer; no p-nonexpansiveness premise or hidden eta≤1/2 restriction.

\[p(y)+\eta\nabla V(p(y))=y,\quad\|q(y)-p(y)\|\le\varepsilon,\quad\operatorname{Lip}(p),\operatorname{Lip}(\nabla V)\le1.\]

Corresponding Lean step

ImplementedPhaseKernel.implemented_phase_kernel; QuadraticRegularization; StrongConvexFirstOrder; MonotoneProximalMap

2. Use the actual coefficients and preserve the same noise

Use the independent coefficient construction for Lambda≥1 and every omega row sum≤S=h²Lambda/2. Position weights are the final row. The new absolute momentum-integral prerequisite yields sum|b|≤hLambda. Set a=exp(-h/2), sigma=sqrt(1-exp(-h)); P0=aP+sigma*zeta0; both phases use the same P0 and independent G0,G1 arrays, and the same terminal zeta1.

\[S=\tfrac12h^2\Lambda_J,\quad B=h\Lambda_J,\quad\sum_j|\omega_{ij}|\le S,\quad\sum_j|b_j|\le B.\]

Corresponding Lean step

ChebyshevLobattoQuadrature.chebyshev_lobatto_coefficients; ChebyshevLobattoMomentum.momentum_absolute_sum_le; phaseMap

3. Propagate the two actual Picard layers

At Y0_i=X+t_iP0, common G0 cancels; gradient Lipschitz and ||r-p||≤delta give first gradient difference≤delta. Therefore ||Y1_r-Y1_p||≤S delta. In the second layer add and subtract p(Y1_r), use r accuracy and exact p nonexpansiveness, then cancel common G1 and use gradient Lipschitz. This works for delta=0 and does not assume r Lipschitz.

\[\|Z^0_{r,j}-Z^0_{p,j}\|\le\delta,\quad\|Y^1_{r,i}-Y^1_{p,i}\|\le S\delta,\quad\|Z^1_{r,j}-Z^1_{p,j}\|\le(1+S)\delta.\]

Corresponding Lean step

weighted_difference_le; phase_displacement_le hz0,hy1,hz1

4. Bound true Euclidean phase displacement

The full actual position difference is≤S(1+S)delta and momentum difference≤aB(1+S)delta. From Lambda≥1 and h²Lambda≤1 obtain h≤1, S≤1/2 and S≤B/2; also a≤1. The sum of these norms is≤9Bdelta/4≤3Bdelta. The Euclidean square-root norm is at most that sum by nonnegative cross product. Source prose uses momentum-weight positivity to give a sharper intermediate bound; this proof uses the independently derived absolute sum and keeps the same universal D2 scaling with explicit3, without adding an assumption.

\[\sqrt{\|\Delta X\|^2+\|\Delta P\|^2}\le(S+aB)(1+S)\delta\le\tfrac94B\delta\le3h\Lambda_J\delta.\]

Corresponding Lean step

phase_displacement_le hx,hm,hShalf,hSB,htotal; Real.sqrt_le_iff

5. Construct actual kernels and a coupling for every finite rho

The product Gaussian law gamma contains both refreshes and both Fin J Gaussian arrays. Each full phase map is measurable by finite sums and composition. Map the product id/kernel-constant to construct each Markov kernel, retaining the existing actual Kq. For fixed s, gamma.map(z↦(Phi_r(s,z),Phi_p(s,z))) has exactly Kr(s) and Kp(s) marginals. The pointwise Euclidean displacement bounds its rho-cost integral by A^rho with A=3hLambda delta; probability normalization supplies the constant integral, so no incoming-state moment assumption is needed. Taking the monotone1/rho root gives the bound, for delta=0 as well.

\[\pi_s=(\Phi_r(s,\cdot),\Phi_p(s,\cdot))_\#\gamma,\quad\int d_{\rm Eucl}^{\rho}\,d\pi_s\le A^\rho\Longrightarrow W_\rho\le A.\]

Corresponding Lean step

measurable_phase; kernel_from_phase; euclidean_transport_bound; Measure.fst_map_prodMk; Measure.snd_map_prodMk; Transport.transportCost_le_lintegral_of_isCoupling; lintegral_map; ENNReal.rpow_mul

Lean verification

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

Lean proof · source_phase_proximal_stability

Entire current module is covered, including private phase, finite weighted difference, measurability, actual kernel and transport helpers. Extraction carries no new mathematical credit.

Download module (.lean)

theorem source_phase_proximal_stability {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 eps : ℝ} (heta : 0 < eta) (heta1 : eta < 1) (heps : 0 < eps)
    {J : ℕ} (hJ : 2 ≤ J) {h : ℝ} (hh : 0 < h) :
    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 pw := omega ⟨J-1,by omega⟩
    let bw := fun j : Fin J => ∫ s in 0..h, (ell j).eval s
    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 γ := ((stdGaussian E).prod (stdGaussian E)).prod
        ((Measure.pi (fun _ : Fin J => stdGaussian E)).prod
          (Measure.pi (fun _ : Fin J => stdGaussian E)))
      let Φ := fun (f : E → E)
          (w : (E × E) × ((E × E) × ((Fin J → E) × (Fin J → E)))) =>
        let a := Real.exp (-h/2)
        let sigma := Real.sqrt (1-Real.exp (-h))
        let P0 := a • w.1.2 + sigma • w.2.1.1
        let Y0 := fun i => w.1.1+t i • P0
        let Z0 := fun j => gradient V (f (Y0 j)+Real.sqrt eta • w.2.2.1 j)
        let Y1 := fun i => Y0 i-∑ j, omega i j • Z0 j
        let Z1 := fun j => gradient V (f (Y1 j)+Real.sqrt eta • w.2.2.2 j)
        (w.1.1+h • P0-∑ j, pw j • Z1 j,
          a • (P0-∑ j, bw j • Z1 j)+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⁻¹)
      ∃ 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 => Φ q (s,z))) ∧
        (∀ s rho, 1 ≤ rho → W rho (Kq s) (Kp s) ≤ ENNReal.ofReal (3*h*Lambda*eps)) ∧
        (∀ (r : E → E), Measurable r → ∀ delta : ℝ, 0 ≤ delta →
          (∀ y, ‖r y-p y‖ ≤ delta) →
          ∃ Kr : Kernel (E × E) (E × E), IsMarkovKernel Kr ∧
            (∀ s, Kr s = γ.map (fun z => Φ r (s,z))) ∧
            ∀ s rho, 1 ≤ rho → W rho (Kr s) (Kp s) ≤
              ENNReal.ofReal (3*h*Lambda*delta)) := by
  classical
  dsimp only
  intro hstep
  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 pw := omega ⟨J-1,by omega⟩
  let bw := fun j : Fin J => ∫ s in 0..h, (ell j).eval s
  obtain ⟨p,q,N,hp,hq,hN,hall,_,hΦq,Kq,hKq,hKqpush⟩ :=
    ImplementedPhaseKernel.implemented_phase_kernel hκ hV hH heta
      (le_refl eta) heta1 heps h hh.le t omega pw bw
  have hg : Measurable (gradient V) := by
    unfold gradient
    exact ((InnerProductSpace.toDual ℝ E).symm.continuous.comp
      (hV.continuous_fderiv (by norm_num))).measurable
  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 hLip : LipschitzWith 1 (gradient V) := by simpa using hreg.2
  have hsc : StrongConvexOn Set.univ ((κ : ℝ)⁻¹) V := by simpa using hreg.1
  have hmono (x y : E) : 0 ≤ inner ℝ (gradient V x-gradient V y) (x-y) := by
    have hb :=
      TechnicalLemmas.Analysis.StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn hsc
        (fun z _ => (hV.differentiable (by norm_num) z).hasGradientAt)
        (x := y) (y := x) (Set.mem_univ _) (Set.mem_univ _)
    exact (mul_nonneg (inv_nonneg.mpr (NNReal.coe_nonneg κ)) (sq_nonneg _)).trans hb
  have hpLip := TechnicalLemmas.Analysis.MonotoneProximalMap.nonexpansive_of_monotone_optimality
    heta.le hmono (fun y => (hall y).1)
  have hcoeff := TechnicalLemmas.Analysis.ChebyshevLobattoQuadrature.chebyshev_lobatto_coefficients hJ hh
  have hL : 1 ≤ Lambda := hcoeff.2.2.2.2.2.1
  have hrow : ∀ i, (∑ j, |omega i j|) ≤ h^2/2*Lambda := fun i =>
    (hcoeff.2.2.2.2.2.2.1 i).2
  have hpw : (∑ j, |pw j|) ≤ h^2/2*Lambda := hrow _
  have hbw : (∑ j, |bw j|) ≤ h*Lambda :=
    TechnicalLemmas.Analysis.ChebyshevLobattoMomentum.momentum_absolute_sum_le hJ hh
  let γ := ((stdGaussian E).prod (stdGaussian E)).prod
    ((Measure.pi (fun _ : Fin J => stdGaussian E)).prod
      (Measure.pi (fun _ : Fin J => stdGaussian E)))
  let Φ := fun f => phaseMap (gradient V) f eta h t omega pw bw
  have hΦ (f : E → E) (hf : Measurable f) : Measurable (Φ f) :=
    measurable_phase hg hf eta h t omega pw bw
  obtain ⟨Kp,hKp,hKppush⟩ := kernel_from_phase γ (hΦ p hp)
  refine ⟨p,q,N,hp,hq,hN,hall,hpLip,Kp,Kq,hKp,hKq,hKppush,hKqpush,?_,?_⟩
  · intro state rho hrho
    rw [hKqpush state,hKppush state]
    apply euclidean_transport_bound γ ((hΦ q hq).comp (by fun_prop))
      ((hΦ p hp).comp (by fun_prop)) _ hrho
    intro z
    exact phase_displacement_le hLip hpLip heps.le hh hL hstep
      (fun y => (hall y).2.1) eta t omega pw bw hrow hpw hbw (state,z)
  · intro r hr delta hd herr
    obtain ⟨Kr,hKr,hKrpush⟩ := kernel_from_phase γ (hΦ r hr)
    refine ⟨Kr,hKr,hKrpush,fun state rho hrho => ?_⟩
    rw [hKrpush state,hKppush state]
    apply euclidean_transport_bound γ ((hΦ r hr).comp (by fun_prop))
      ((hΦ p hp).comp (by fun_prop)) _ hrho
    intro z
    exact phase_displacement_le hLip hpLip hd hh hL hstep herr
      eta t omega pw bw hrow hpw hbw (state,z)

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalPhaseStability

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Source uses normalized Euclidean strongly convex C2 potential and true Euclidean phase distance.	E is a complete finite-dimensional real inner-product space with its Borel sigma algebra; dimension zero is allowed. V:E→R is genuinely C2, kappa>=1 and kappa^-1\|\|v\|\|²<=D²V(x)[v,v]<=\|\|v\|\|² for every x,v (normalized beta=1).	generalization	The abstract shared implication is an explicit prerequisite; paper consumer supplies its exact Hessian hypotheses. Main uses finite real inner-product coordinates and explicitly sqrt(sum squares), never default product max norm.
D2 gives universal C Lambda h delta under h²Lambda<=1 for arbitrary measurable delta-accurate oracle delta>=0; B1 includes further positivity/logarithmic claims.	Appendix D1/D2 one-phase proximal implementation stability only, explicit universal constant3. Both compared phases use the exact same two stochastic-gradient Gaussian arrays and two half-refresh Gaussian vectors; the exact phase uses exact proximal p, not a deterministic smoothed force. N(y)+1 is a noncomputable successful execution certificate, not free runtime fuel determination or expected-work evidence. Repeated-phase D3, weighted contraction, numerical D7/D8, invariant law, bias/concentration, Wp/proxy-warmness/init/PBPS/composition and both main results remain separate. No TV-to-unbounded-cost transfer.	unresolved	Only D1/D2 one-phase comparison or a named prerequisite is asserted. Absolute-b proof is a faithful universal-constant route adapter, not a source assumption repair or completed B1.

Appendix D1/D2 one-phase proximal implementation stability only, explicit universal constant3. Both compared phases use the exact same two stochastic-gradient Gaussian arrays and two half-refresh Gaussian vectors; the exact phase uses exact proximal p, not a deterministic smoothed force. N(y)+1 is a noncomputable successful execution certificate, not free runtime fuel determination or expected-work evidence. Repeated-phase D3, weighted contraction, numerical D7/D8, invariant law, bias/concentration, Wp/proxy-warmness/init/PBPS/composition and both main results remain separate. No TV-to-unbounded-cost transfer.

Encoder–denoiser: accepted · 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

Appendix D1/D2 one-phase proximal implementation stability only, explicit universal constant3. Both compared phases use the exact same two stochastic-gradient Gaussian arrays and two half-refresh Gaussian vectors; the exact phase uses exact proximal p, not a deterministic smoothed force. N(y)+1 is a noncomputable successful execution certificate, not free runtime fuel determination or expected-work evidence. Repeated-phase D3, weighted contraction, numerical D7/D8, invariant law, bias/concentration, Wp/proxy-warmness/init/PBPS/composition and both main results remain separate. No TV-to-unbounded-cost transfer.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Measure.fst_map_prodMk
Measure.snd_map_prodMk
Kernel.IsMarkovKernel.map
Measure.map_map
lintegral_map
ENNReal.rpow_le_rpow
ENNReal.rpow_mul
Real.sqrt_le_iff

Mathematical sources

SPHMC proximal phase and coefficient prerequisites — Appendix D1/D2 one-phase proximal implementation stability only, explicit universal constant3. Both compared phases use the exact same two stochastic-gradient Gaussian arrays and two half-refresh Gaussian vectors; the exact phase uses exact proximal p, not a deterministic smoothed force. N(y)+1 is a noncomputable successful execution certificate, not free runtime fuel determination or expected-work evidence. Repeated-phase D3, weighted contraction, numerical D7/D8, invariant law, bias/concentration, Wp/proxy-warmness/init/PBPS/composition and both main results remain separate. 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.

ProximalPhaseStability actual source component

Complete source statement (Samplinglib restatement)

Exact bounded formula

Read the formalized proofs

ProximalPhaseStability actual source component

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Construct and identify the actual proximal maps

2. Use the actual coefficients and preserve the same noise

3. Propagate the two actual Picard layers

4. Bound true Euclidean phase displacement

5. Construct actual kernels and a coupling for every finite rho

Lean verification

Source assumptions versus formal assumptions

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?