Actual clipped and ideal RGO bidirectional RN moments
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedRenyiComparison.clipped_renyi_comparison · theorem · Teaching coverage
Mathematical statement
pi and qhat are probability measures and are mutually absolutely continuous. The real functions ((d pi/d qhat).toReal)^ell and ((d qhat/d pi).toReal)^ell are integrable under qhat and pi respectively. Each of their real integrals minus one is at most 2*exp(2*B-K). Each corresponding ENNReal RN ell-power lintegral is at most ofReal(1+2*exp(2*B-K)).
Lean statement · clipped_renyi_comparison
Two actual probabilities,two absolute continuities,two real RN-power L1,two real-integral-minus-one bounds and two ENNReal bounds.
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.
theorem clipped_renyi_comparison (f : E → ℝ) (hf : Differentiable ℝ f)
(eta beta B ell : ℝ) (heta : 0 < eta) (hbeta : 0 < beta) (hB : 0 < B)
(hell : 2 ≤ ell) (hd : 0 < (Module.finrank ℝ E : ℝ))
(hlip : LipschitzWith ⟨beta,hbeta.le⟩ (gradient f)) (x0 xp : E)
(hcenter : ‖(x0-eta • gradient f xp)-xp‖ ≤ Real.sqrt ((Module.finrank ℝ E : ℝ)*eta))
(hstep : 64*beta^2*(ell*(Module.finrank ℝ E : ℝ)/B+ell^2) ≤ 1/eta^2) :
let h := x0-eta • gradient f xp
let q := (stdGaussian E).map (fun z => h+Real.sqrt eta • z)
let P := (stdGaussian E).map (fun z => Real.sqrt eta • z)
let nu := (volume.restrict (Set.Ioc (0 : ℝ) 1)).prod P
let mB := fun x => ∫ a, min B (max (-B) (estimator f h xp (x,a))) ∂nu
let qhat := q.tilted mB
let pi := ((stdGaussian E).map (fun z => x0+Real.sqrt eta • z)).tilted (fun x => -f x)
let K := min (B^2/(40*beta^2*(Module.finrank ℝ E : ℝ)*eta^2)) (B/(8*beta*eta))
IsProbabilityMeasure pi ∧ IsProbabilityMeasure qhat ∧ pi ≪ qhat ∧ qhat ≪ pi ∧
Integrable (fun x => (pi.rnDeriv qhat x).toReal ^ ell) qhat ∧
Integrable (fun x => (qhat.rnDeriv pi x).toReal ^ ell) pi ∧
(∫ x, (pi.rnDeriv qhat x).toReal ^ ell ∂qhat) - 1 ≤ 2 * Real.exp (2*B-K) ∧
(∫ x, (qhat.rnDeriv pi x).toReal ^ ell ∂pi) - 1 ≤ 2 * Real.exp (2*B-K) ∧
(∫⁻ x, (pi.rnDeriv qhat x) ^ ell ∂qhat) ≤ ENNReal.ofReal (1+2*Real.exp (2*B-K)) ∧
(∫⁻ x, (qhat.rnDeriv pi x) ^ ell ∂pi) ≤ ENNReal.ofReal (1+2*Real.exp (2*B-K))Proof roadmap
- 1Identify the actual ideal law from the existing source parameters
The positive source step condition bounds 64 beta^2 ell^2 eta^2 by one; ell≥2 therefore implies beta eta<1. Invoke IdealRGOIdentification with this derived fact. Set m to the actual untruncated auxiliary mean, D=m-mB, and mu=qhat. The actual clipped exponential weight is integrable and normalizes to a probability by ClippedGradientProgram. The tilt-composition identity and mB+D=m give the actual ideal law, not an assumed target equality.
- 2Obtain genuine integrability for every exponential used later
The actual ClippedMeanExponential theorem supplies the mu-integrable exponential-minus-one error. Add the integrable constant one to obtain the full envelope. For every coefficient a with abs(a)≤2ell, pointwise domination gives integrability of exp(aD). The same envelope controls exp(c abs(D)) for 0≤c≤2ell. Since abs(D)≤abs(D)+1≤exp(abs(D)), it also proves D itself integrable. No later Jensen application or density calculation relies on a totalized integral of an unproved integrable function.
- 3Identify both actual derivatives on their correct measures
Let Z be the actual integral of exp(D) under the probability mu. Established L1 and strict pointwise positivity give Z>0. The tilted law is a probability and is mutually absolutely continuous with mu. Use the actual tilted RN formulas. The reverse formula is initially obtained mu-almost everywhere; transfer it to the tilted law using absolute continuity before integrating there.
- 4Establish weighted L1 before the normalized power identities
Raise the positive density formulas to ell. The forward power under mu is an integrable scalar multiple of exp(ell D). For the reverse power under pi, use the tilted integrability equivalence: its exponential factor has weighted integrand exp(D) exp(-ell D)=exp(-(ell-1)D), already known integrable under mu. Only then compute the integral and combine the powers of the positive Z.
- 5Control the positive normalizer power
Put a=ell-1≥1. Convexity of the a-th power and the two supplied integrability conditions give Z^a≤E exp(aD). Bound both this expectation and E exp(-aD) by E exp(a abs(D)). A second Jensen application, now for the square, bounds the product by E exp(2a abs(D)), which is at most H. The a≥1 step is why this proof uses the actual ell≥2 consumer rather than claiming the entire printed ell>1 range.
- 6Control the inverse normalizer by two exponential Jensen inequalities
Because D and exp(D) are integrable, exponential Jensen gives exp(E D)≤Z. The negative ell-th power reverses this inequality. Apply exponential Jensen again to -ell D, whose integrability and exponential integrability were already proved. This yields Z^(-ell)≤E exp(-ell D). Dominate both signed exponential moments by E exp(ell abs(D)); square Jensen gives the same H bound. This is a complete alternative to the Cauchy-Schwarz step, preserving the source constant.
- 7Transfer real powers to ENNReal and instantiate the actual consumer
Both real RN-power integrals are now finite and at most H. Subtract one and consume the parent bound H-1≤epsilon. To obtain the ENNReal lintegrals, use RN derivatives being finite almost everywhere under their denominator measures; then ofReal commutes with the nonnegative power. This excludes a false conversion through toReal(infinity). The actual ideal-law equality from the first step instantiates all generic statements with pi and qhat and returns the ten asserted conclusions.
Full assumptions and notation
All objects and hypotheses
- E is a finite-dimensional real inner-product Borel space with d=finrank(E)>0. f:E→R is differentiable everywhere and its actual gradient is globally beta-Lipschitz. eta,beta,B>0 and ell≥2. No convexity assumption is used for this selected smooth s=1 dependency.
- For x0,x_plus in E, set h=x0-eta grad f(x_plus). Assume norm(h-x_plus)≤sqrt(d*eta) and 64*beta^2*(ell*d/B+ell^2)≤1/eta^2. In particular beta*eta<1 will be proved, not added as an input.
- Let P=(z→sqrt(eta) z)_*stdGaussian(E), nu=(Lebesgue restricted to (0,1]) product P, and q=(z→h+sqrt(eta) z)_*stdGaussian(E). For theta=pi*r/2 define W(x,r,z)=< (pi/2)(cos(theta)(x-h)-sin(theta)z), grad f(x_plus)-grad f(h+sin(theta)(x-h)+cos(theta)z) >. Let mB(x)=integral min(B,max(-B,W(x,r,z))) dnu(r,z). The estimator, independent input and clipping inside the expectation are actual definitions.
- Define qhat=q.tilted(mB). First set G=(z→x0+sqrt(eta) z)_*stdGaussian(E), then pi=G.tilted(-f). Define K=min(B^2/(40*beta^2*d*eta^2),B/(8*beta*eta)). An exponential tilt uses its actual exponential integral as normalizer. Each RN power below is integrated under its denominator measure.
Mathematical proof
1. Identify the actual ideal law from the existing source parameters
The positive source step condition bounds 64 beta^2 ell^2 eta^2 by one; ell≥2 therefore implies beta eta<1. Invoke IdealRGOIdentification with this derived fact. Set m to the actual untruncated auxiliary mean, D=m-mB, and mu=qhat. The actual clipped exponential weight is integrable and normalizes to a probability by ClippedGradientProgram. The tilt-composition identity and mB+D=m give the actual ideal law, not an assumed target equality.
Corresponding Lean step
step_implies_ideal; estimator; clipped_renyi_comparison; AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.IdealRGOIdentification.ideal_rgo_identification; AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedGradientProgram.clipped_gradient_program; MeasureTheory.tilted_tilted
2. Obtain genuine integrability for every exponential used later
The actual ClippedMeanExponential theorem supplies the mu-integrable exponential-minus-one error. Add the integrable constant one to obtain the full envelope. For every coefficient a with abs(a)≤2ell, pointwise domination gives integrability of exp(aD). The same envelope controls exp(c abs(D)) for 0≤c≤2ell. Since abs(D)≤abs(D)+1≤exp(abs(D)), it also proves D itself integrable. No later Jensen application or density calculation relies on a totalized integral of an unproved integrable function.
Corresponding Lean step
exponential_domination; integrable_of_exponential_abs; integral_exp_le_abs; AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedMeanExponential.clipped_mean_exponential
3. Identify both actual derivatives on their correct measures
Let Z be the actual integral of exp(D) under the probability mu. Established L1 and strict pointwise positivity give Z>0. The tilted law is a probability and is mutually absolutely continuous with mu. Use the actual tilted RN formulas. The reverse formula is initially obtained mu-almost everywhere; transfer it to the tilted law using absolute continuity before integrating there.
Corresponding Lean step
tilt_density_pair; MeasureTheory.toReal_rnDeriv_tilted_left; MeasureTheory.toReal_rnDeriv_tilted_right; MeasureTheory.tilted_absolutelyContinuous; MeasureTheory.absolutelyContinuous_tilted; MeasureTheory.isProbabilityMeasure_tilted
4. Establish weighted L1 before the normalized power identities
Raise the positive density formulas to ell. The forward power under mu is an integrable scalar multiple of exp(ell D). For the reverse power under pi, use the tilted integrability equivalence: its exponential factor has weighted integrand exp(D) exp(-ell D)=exp(-(ell-1)D), already known integrable under mu. Only then compute the integral and combine the powers of the positive Z.
Corresponding Lean step
forward_density_power; reverse_density_power; MeasureTheory.integrable_tilted_iff; MeasureTheory.integral_exp_tilted; Real.div_rpow; Real.mul_rpow
5. Control the positive normalizer power
Put a=ell-1≥1. Convexity of the a-th power and the two supplied integrability conditions give Z^a≤E exp(aD). Bound both this expectation and E exp(-aD) by E exp(a abs(D)). A second Jensen application, now for the square, bounds the product by E exp(2a abs(D)), which is at most H. The a≥1 step is why this proof uses the actual ell≥2 consumer rather than claiming the entire printed ell>1 range.
Corresponding Lean step
power_mean_exponential; exponential_mean_square; normalized_moments; convexOn_rpow; ConvexOn.map_integral_le
6. Control the inverse normalizer by two exponential Jensen inequalities
Because D and exp(D) are integrable, exponential Jensen gives exp(E D)≤Z. The negative ell-th power reverses this inequality. Apply exponential Jensen again to -ell D, whose integrability and exponential integrability were already proved. This yields Z^(-ell)≤E exp(-ell D). Dominate both signed exponential moments by E exp(ell abs(D)); square Jensen gives the same H bound. This is a complete alternative to the Cauchy-Schwarz step, preserving the source constant.
Corresponding Lean step
exponential_mean; inverse_normalizer_power; normalized_moments; Real.rpow_le_rpow_of_nonpos; convexOn_exp
7. Transfer real powers to ENNReal and instantiate the actual consumer
Both real RN-power integrals are now finite and at most H. Subtract one and consume the parent bound H-1≤epsilon. To obtain the ENNReal lintegrals, use RN derivatives being finite almost everywhere under their denominator measures; then ofReal commutes with the nonnegative power. This excludes a false conversion through toReal(infinity). The actual ideal-law equality from the first step instantiates all generic statements with pi and qhat and returns the ten asserted conclusions.
Corresponding Lean step
rn_power_lintegral; tilt_power_bounds; clipped_renyi_comparison; MeasureTheory.Measure.rnDeriv_ne_top; MeasureTheory.ofReal_integral_eq_lintegral_ofReal; ENNReal.ofReal_rpow_of_nonneg
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · clipped_renyi_comparison
Actual ideal identification,derived normalization,exponential domination,Jensen,weighted RN algebra,a.e. measure transfer and finite RN conversion.
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.
theorem clipped_renyi_comparison (f : E → ℝ) (hf : Differentiable ℝ f)
(eta beta B ell : ℝ) (heta : 0 < eta) (hbeta : 0 < beta) (hB : 0 < B)
(hell : 2 ≤ ell) (hd : 0 < (Module.finrank ℝ E : ℝ))
(hlip : LipschitzWith ⟨beta,hbeta.le⟩ (gradient f)) (x0 xp : E)
(hcenter : ‖(x0-eta • gradient f xp)-xp‖ ≤ Real.sqrt ((Module.finrank ℝ E : ℝ)*eta))
(hstep : 64*beta^2*(ell*(Module.finrank ℝ E : ℝ)/B+ell^2) ≤ 1/eta^2) :
let h := x0-eta • gradient f xp
let q := (stdGaussian E).map (fun z => h+Real.sqrt eta • z)
let P := (stdGaussian E).map (fun z => Real.sqrt eta • z)
let nu := (volume.restrict (Set.Ioc (0 : ℝ) 1)).prod P
let mB := fun x => ∫ a, min B (max (-B) (estimator f h xp (x,a))) ∂nu
let qhat := q.tilted mB
let pi := ((stdGaussian E).map (fun z => x0+Real.sqrt eta • z)).tilted (fun x => -f x)
let K := min (B^2/(40*beta^2*(Module.finrank ℝ E : ℝ)*eta^2)) (B/(8*beta*eta))
IsProbabilityMeasure pi ∧ IsProbabilityMeasure qhat ∧ pi ≪ qhat ∧ qhat ≪ pi ∧
Integrable (fun x => (pi.rnDeriv qhat x).toReal ^ ell) qhat ∧
Integrable (fun x => (qhat.rnDeriv pi x).toReal ^ ell) pi ∧
(∫ x, (pi.rnDeriv qhat x).toReal ^ ell ∂qhat) - 1 ≤ 2 * Real.exp (2*B-K) ∧
(∫ x, (qhat.rnDeriv pi x).toReal ^ ell ∂pi) - 1 ≤ 2 * Real.exp (2*B-K) ∧
(∫⁻ x, (pi.rnDeriv qhat x) ^ ell ∂qhat) ≤ ENNReal.ofReal (1+2*Real.exp (2*B-K)) ∧
(∫⁻ x, (qhat.rnDeriv pi x) ^ ell ∂pi) ≤ ENNReal.ofReal (1+2*Real.exp (2*B-K)) := by
let h := x0-eta • gradient f xp
let q := (stdGaussian E).map (fun z => h+Real.sqrt eta • z)
let P := (stdGaussian E).map (fun z => Real.sqrt eta • z)
let nu := (volume.restrict (Set.Ioc (0 : ℝ) 1)).prod P
let m := fun x => ∫ a, estimator f h xp (x,a) ∂nu
let mB := fun x => ∫ a, min B (max (-B) (estimator f h xp (x,a))) ∂nu
let qhat := q.tilted mB
let pi := ((stdGaussian E).map (fun z => x0+Real.sqrt eta • z)).tilted (fun x => -f x)
let D := fun x => m x-mB x
let K := min (B^2/(40*beta^2*(Module.finrank ℝ E : ℝ)*eta^2)) (B/(8*beta*eta))
have hc := AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedMeanExponential.clipped_mean_exponential
f hf eta beta B ell heta hbeta hB hell hd hlip x0 xp hcenter hstep
have hp := AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedGradientProgram.clipped_gradient_program
f hf eta beta B heta hbeta.le hB hlip x0 xp
have hi := AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.IdealRGOIdentification.ideal_rgo_identification
f hf ⟨beta,hbeta.le⟩ hlip eta heta
(step_implies_ideal eta beta B ell (Module.finrank ℝ E : ℝ) heta hbeta hB hell hd hstep) x0 xp
have hmq : IsProbabilityMeasure q := hp.2.1
have hmb : Integrable (fun x => Real.exp (mB x)) q := hp.2.2.2.2.2.2.1
have hmqhat : IsProbabilityMeasure qhat := isProbabilityMeasure_tilted hmb
have hD : Measurable D := hc.1.sub hc.2.1
have hJ : Integrable (fun x => Real.exp (2*ell*|D x|)-1) qhat := hc.2.2.2.2.2.2.2.2.1
have hb : (∫ x, Real.exp (2*ell*|D x|)-1 ∂qhat) ≤ 2*Real.exp (2*B-K) :=
hc.2.2.2.2.2.2.2.2.2
have heq : qhat.tilted D = pi := by
change (q.tilted mB).tilted D = pi
rw [tilted_tilted hmb]
have hsum : mB+D=m := by funext x; dsimp [D]; ring
rw [hsum]
exact hi.2.2.2.2.2.2.1
have ht := tilt_power_bounds qhat D hD ell hell hJ
rw [heq] at ht
rcases ht with ⟨hpi,hpq,hqp,hfi,hri,hfb,hrb,hfen,hren⟩
refine ⟨hpi,hmqhat,hpq,hqp,hfi,hri,hfb.trans hb,hrb.trans hb,?_,?_⟩
· exact hfen.trans (ENNReal.ofReal_le_ofReal (by linarith))
· exact hren.trans (ENNReal.ofReal_le_ofReal (by linarith))
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedRenyiComparisonSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| The source uses positive-dimensional Euclidean space. | Finite-dimensional real inner-product Borel space with positive finrank. | generalization | Coordinate-free Gaussian and gradient interfaces preserve the dimension restriction. |
| D.1 uses Assumption3.2 with Holder gradient; the selected smooth case has s=1. | Actual beta-Lipschitz gradient, differentiability,positive beta,eta,B,d,ell>=2 and the displayed residual/64-step restriction. | same | This selects the smooth s=1 consumer, not the entire Holder theorem. D.1 itself does not assume convexity; downstream SPHMC convexity is not a missing hypothesis here. |
| B.12/D.1 proof uses denominator-measure ell-powers, whereas B.7 and section1.3 contain inconsistent measure subscripts or powers. | Both actual denominator-measure ell-power integrals are written explicitly. | source-implicit | The contract follows B.12 proof and D.1 actual use. Internal evidence suggests local printed definition errors; this is not an author-confirmed erratum or a claim of literal B.7 implementation. |
| B.12 is printed for ell>1, while D.1 uses ell>=2. | The selected actual consumer retains ell>=2. | same | The printed intermediate positive-power Jensen step can fail for1<ell<2. This is a proof-step gap, not a counterexample to its final theorem. The present packet neither claims that full range nor repairs it. |
| Auxiliary uniform time is sampled on [0,1]. | Restricted Lebesgue volume on (0,1] is independently multiplied with the actual Gaussian. | source-implicit | Endpoint differences are null; the actual estimator and independent input are retained. |
| Normalized comparison uses the actual ideal and implemented clipped laws. | beta*eta<1,positive normalizers,both probabilities,mutual absolute continuity,weighted L1 and both RN a.e. formulas are proved before use. | source-implicit | No extra ideal normalization or target equality is assumed. RN a.e. finiteness justifies the real/ENNReal conversion. |
| D.1 Eq18 feeds the terminal approximate RGO in SPHMC A.4(2). | Two real moment-minus-one bounds and two ENNReal moment bounds with factor2,constants40/8 and actual distributions. | same | This completes the selected normalized moment comparison, not logarithmic Renyi API,parameter selection,initialization,adaptivekernel,cost or fullpaper. |
The ten public conclusions are two probability statements, two absolute-continuity statements, two real RN-power L1 statements, two real-integral-minus-one bounds and two ENNReal bounds. Positive normalizers, error L1 and explicit RN formulas are proved internally, not additional returned conjuncts. ClippedGradientProgram already identifies qhat with the actual program output; its map equality is not repeated. This follows the explicit denominator-measure ell-powers in B.12/D.1. B.7 and section1.3 have inconsistent printed definitions; this is disclosed rather than silently called a literal implementation of those lines. The intermediate B.12 proof gap for 1<ell<2 is outside this ell>=2 consumer and is not repaired here. No logarithmic Renyi API, accuracy parameter selection, initialization, parameterized kernel, query-cost result or complete companion paper is asserted.
Encoder–denoiser: accepted · domain-mismatch
Detected semantic differences
- domains: Positive-dimensional coordinate-free extension disclosed. — Independent formal reviewer accepted: Positive-dimensional coordinate-free extension disclosed.
- assumptions: Selected smooth s=1 regime; D1 requires no convexity. — Independent formal reviewer accepted: Selected smooth s=1 regime; D1 requires no convexity.
- objects: Denominator-measure powers follow B12 identities; inconsistent B7 definition disclosed, not author-confirmed erratum. — Independent formal reviewer accepted: Denominator-measure powers follow B12 identities; inconsistent B7 definition disclosed, not author-confirmed erratum.
- assumptions: ell>=2 selected consumer; B12 intermediate gap below2 disclosed, not final-theorem counterexample or repair. — Independent formal reviewer accepted: ell>=2 selected consumer; B12 intermediate gap below2 disclosed, not final-theorem counterexample or repair.
- objects: Ioc/Icc uniform endpoints differ by null set; actual independent product. — Independent formal reviewer accepted: Ioc/Icc uniform endpoints differ by null set; actual independent product.
- assumptions: Normalization, AC and weighted L1 proved internally before use, not extra public conjuncts. — Independent formal reviewer accepted: Normalization, AC and weighted L1 proved internally before use, not extra public conjuncts.
- scopes: Explicit moment comparison dependency, not complete parameterized terminal routine. — Independent formal reviewer accepted: Explicit moment comparison dependency, not complete parameterized terminal routine.
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
- The ten public conclusions are two probability statements, two absolute-continuity statements, two real RN-power L1 statements, two real-integral-minus-one bounds and two ENNReal bounds. Positive normalizers, error L1 and explicit RN formulas are proved internally, not additional returned conjuncts. ClippedGradientProgram already identifies qhat with the actual program output; its map equality is not repeated. This follows the explicit denominator-measure ell-powers in B.12/D.1. B.7 and section1.3 have inconsistent printed definitions; this is disclosed rather than silently called a literal implementation of those lines. The intermediate B.12 proof gap for 1<ell<2 is outside this ell≥2 consumer and is not repaired here. No logarithmic Renyi API, accuracy parameter selection, initialization, parameterized kernel, query-cost result or complete companion paper is asserted.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedMeanExponential.clipped_mean_exponentialAutoSamplingTheory.ExampleCases.SmoothedPicardHMC.IdealRGOIdentification.ideal_rgo_identificationAutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedGradientProgram.clipped_gradient_program
Mathlib API called (external library)
- MeasureTheory.tilted_tilted
- MeasureTheory.integrable_tilted_iff
- MeasureTheory.toReal_rnDeriv_tilted_right
- ConvexOn.map_integral_le
- MeasureTheory.Measure.rnDeriv_ne_top
Mathematical sources
- D.1 Eq18 and B.12 Eq17 — Smooth actual normalized RN-power comparison; printed definition and proof-range differences disclosed.
- SPHMC Appendix A.4(2) — Terminal sampler consumer; remaining algorithmic obligations separate.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.