Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

Actual PBPS squared defect: positive real root and energy

Attributed ASTIS background completion supporting Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang. This real scalar-root construction is ASTIS-authored; it is not the printed joint GammaP, B.11 operator identity or a main theorem.

arXiv:2609.06905v1; Lean4.33.0/fixedMathlib · Appendix D.1 positive real square-root background; B.10-B.11 scalar defect energy precursor. ASTIS background completion, not printed joint GammaP. · faithful paraphrase

Complete source statement (Samplinglib restatement)

Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including the explicit rank-zero extension. Let V:E→ℝ be C², let 0<α≤β, and assume α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v. Assume η>0 and βη≤1. Define μ(dx) proportional to exp(−V(x))dx, J as the law of (X,X+√η Z) for independent X∼μ,Z∼N(0,I), ν=J.snd, and Λ as the law of (Y,2X−Y) under J. The laws μ,J,ν are probabilities. There exists a Markov kernel S whose every-state normalized density is S(y)=volume.tilted(x↦−V((y+x)/2)−‖y−x‖²/(8η)), with Λ.IsCondKernel S and Λ.fst=Λ.snd=ν. There exists a bounded selfadjoint T on the actual real L²(ν) such that for every u, ‖Tu‖≤‖u‖, Tu(y)=∫u(x)S(y,dx) ν-almost everywhere, and ∫Tu dν=∫u dν. Its full scalar defect D=I−T² is positive. There exists a bounded positive REAL Γ with Γ²=D and for EVERY scalar u, ‖Γu‖²=‖u‖²−‖Tu‖². Probability, kernel, T, D positivity and Γ are conclusions; no supplied CFC/root/commutation or finite-dimensional L² certificate is assumed. This is the scalar precursor to the printed joint/macro root and B.11, which remain separate.

  • Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including the explicit rank-zero extension. Let V:E→ℝ be C², let 0<α≤β, and assume α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v. Assume η>0 and βη≤1. Define μ(dx) proportional to exp(−V(x))dx, J as the law of (X,X+√η Z) for independent X∼μ,Z∼N(0,I), ν=J.snd, and Λ as the law of (Y,2X−Y) under J.
  • The normalized S, probability laws, same actual T and positive D and REAL Γ are produced conclusions. Finite E does not imply finite L²; rank-zero E and αη=1 remain permitted.
  • Pointwise conjugation is antiunitary on complex L² and differs from operator adjoint; its root-preservation and the descent are proved internally.

Actual PBPS squared defect: positive real root and energy

\[D=I-T^2\ge0,\quad\Gamma\ge0,\quad\Gamma^2=I-T^2,\quad\forall u\in L^2(\nu;\mathbb R),\ \|\Gamma u\|^2=\|u\|^2-\|Tu\|^2.\]

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

Actual PBPS squared defect: positive real root and energy

AutoSamplingTheory.ExampleCases.ProximalBPS.RealDefectRoot.actual_positive_real_defect_root · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including the explicit rank-zero extension. Let V:E→ℝ be C², let 0<α≤β, and assume α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v. Assume η>0 and βη≤1. Define μ(dx) proportional to exp(−V(x))dx, J as the law of (X,X+√η Z) for independent X∼μ,Z∼N(0,I), ν=J.snd, and Λ as the law of (Y,2X−Y) under J. The laws μ,J,ν are probabilities. There exists a Markov kernel S whose every-state normalized density is S(y)=volume.tilted(x↦−V((y+x)/2)−‖y−x‖²/(8η)), with Λ.IsCondKernel S and Λ.fst=Λ.snd=ν. There exists a bounded selfadjoint T on the actual real L²(ν) such that for every u, ‖Tu‖≤‖u‖, Tu(y)=∫u(x)S(y,dx) ν-almost everywhere, and ∫Tu dν=∫u dν. Its full scalar defect D=I−T² is positive. There exists a bounded positive REAL Γ with Γ²=D and for EVERY scalar u, ‖Γu‖²=‖u‖²−‖Tu‖². Probability, kernel, T, D positivity and Γ are conclusions; no supplied CFC/root/commutation or finite-dimensional L² certificate is assumed. This is the scalar precursor to the printed joint/macro root and B.11, which remain separate.

\[D=I-T^2\ge0,\quad\Gamma\ge0,\quad\Gamma^2=I-T^2,\quad\forall u\in L^2(\nu;\mathbb R),\ \|\Gamma u\|^2=\|u\|^2-\|Tu\|^2.\]
Lean statement · actual_positive_real_defect_root

Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including the explicit rank-zero extension. Let V:E→ℝ be C², let 0<α≤β, and assume α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v. Assume η>0 and βη≤1. Define μ(dx) proportional to exp(−V(x))dx, J as the law of (X,X+√η Z) for independent X∼μ,Z∼N(0,I), ν=J.snd, and Λ as the law of (Y,2X−Y) under J. The laws μ,J,ν are probabilities. There exists a Markov kernel S whose every-state normalized density is S(y)=volume.tilted(x↦−V((y+x)/2)−‖y−x‖²/(8η)), with Λ.IsCondKernel S and Λ.fst=Λ.snd=ν. There exists a bounded selfadjoint T on the actual real L²(ν) such that for every u, ‖Tu‖≤‖u‖, Tu(y)=∫u(x)S(y,dx) ν-almost everywhere, and ∫Tu dν=∫u dν. Its full scalar defect D=I−T² is positive. There exists a bounded positive REAL Γ with Γ²=D and for EVERY scalar u, ‖Γu‖²=‖u‖²−‖Tu‖². Probability, kernel, T, D positivity and Γ are conclusions; no supplied CFC/root/commutation or finite-dimensional L² certificate is assumed. This is the scalar precursor to the printed joint/macro root and B.11, which remain separate.

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 actual_positive_real_defect_root
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ)*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ)*‖v‖^2)
    (hη : 0 < η) (hβη : (β : ℝ)*η ≤ 1) :
    let μ := (volume : Measure E).tilted (fun x => -V x)
    let J := (μ.prod (stdGaussian E)).map
      (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
    let ν := J.snd
    let Λ := J.map (fun p : E × E => (p.2,(2 : ℝ) • p.1-p.2))
    IsProbabilityMeasure μ ∧ IsProbabilityMeasure J ∧ IsProbabilityMeasure ν ∧
    ∃ S : Kernel E E, IsMarkovKernel S ∧
      (∀ y, S y = (volume : Measure E).tilted
        (fun x => -V ((1/2 : ℝ) • (y+x)) - ‖y-x‖^2/(8*η))) ∧
      Λ.IsCondKernel S ∧ Λ.fst = ν ∧ Λ.snd = ν ∧
      ∃ T : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν,
        IsSelfAdjoint T ∧
        (∀ u : Lp ℝ 2 ν, ‖T u‖ ≤ ‖u‖ ∧
          (T u : E → ℝ) =ᵐ[ν] (fun y => ∫ x, u x ∂S y) ∧
          (∫ y, T u y ∂ν) = ∫ y, u y ∂ν) ∧
        ((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T).IsPositive ∧
        ∃ Γ : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν,
          Γ.IsPositive ∧ Γ*Γ = ((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T) ∧
          ∀ u : Lp ℝ 2 ν, ‖Γ u‖^2 = ‖u‖^2-‖T u‖^2

Exact module and namespace context

Proof roadmap

  1. 1Produce the genuine reflected kernel and scalar defect

    The independently verified centered-defect producer under the displayed original potential and step assumptions supplies probability μ,J,ν, the every-state normalized Markov S, genuine disintegration with both stationary marginals, and the same selfadjoint contractive mean-preserving T with AE conditional action. It proves D=I−T² positive internally, including the nontrivial constant mode; no caller operator or positivity certificate is used.

  2. 2Apply the shared real-root theorem to that same defect

    Apply the generic theorem to the actual marginal ν and the produced D. Its internally constructed positive real Γ satisfies Γ²=I−T². This supplies the real scalar root even when L² is infinite-dimensional and includes rank-zero base geometry and the legal αη=1 endpoint.

  3. 3Identify the scalar norm defect

    For every scalar observable u, root energy equals ⟨(I−T²)u,u⟩. Selfadjointness of the same T gives ⟨T²u,u⟩=‖Tu‖²; thus ‖Γu‖²=‖u‖²−‖Tu‖². The anonymous actual-input Test also checks ‖Γu‖≤‖u‖. This is a scalar B.11 precursor. Printed joint ΓP still requires the same onto M, restriction to ran(P) and the typed B*B identity; no full-space inverse is claimed.

Full assumptions and notation

All objects and hypotheses

  • Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including the explicit rank-zero extension. Let V:E→ℝ be C², let 0<α≤β, and assume α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v. Assume η>0 and βη≤1. Define μ(dx) proportional to exp(−V(x))dx, J as the law of (X,X+√η Z) for independent X∼μ,Z∼N(0,I), ν=J.snd, and Λ as the law of (Y,2X−Y) under J.
  • The normalized S, probability laws, same actual T and positive D and REAL Γ are produced conclusions. Finite E does not imply finite L²; rank-zero E and αη=1 remain permitted.
  • Pointwise conjugation is antiunitary on complex L² and differs from operator adjoint; its root-preservation and the descent are proved internally.

Mathematical proof

1. Produce the genuine reflected kernel and scalar defect

The independently verified centered-defect producer under the displayed original potential and step assumptions supplies probability μ,J,ν, the every-state normalized Markov S, genuine disintegration with both stationary marginals, and the same selfadjoint contractive mean-preserving T with AE conditional action. It proves D=I−T² positive internally, including the nontrivial constant mode; no caller operator or positivity certificate is used.

\[S(y,dx)\propto\exp\!\left[-V\!\left(\frac{y+x}{2}\right)-\frac{\|y-x\|^2}{8\eta}\right]dx,\quad Tu(y)=\int u(x)S(y,dx),\quad D=I-T^2\ge0.\]
Corresponding Lean step

CenteredDefectOperator.actual_centered_selfadjoint_defect; hBase; hAll; hD

2. Apply the shared real-root theorem to that same defect

Apply the generic theorem to the actual marginal ν and the produced D. Its internally constructed positive real Γ satisfies Γ²=I−T². This supplies the real scalar root even when L² is infinite-dimensional and includes rank-zero base geometry and the legal αη=1 endpoint.

\[\Gamma\ge0,\quad\Gamma^2=I-T^2\quad\text{on actual }L^2(\nu;\mathbb R).\]
Corresponding Lean step

L2RealSquareRoot.exists_positive_real_square_root; hΓ; hΓSq

3. Identify the scalar norm defect

For every scalar observable u, root energy equals ⟨(I−T²)u,u⟩. Selfadjointness of the same T gives ⟨T²u,u⟩=‖Tu‖²; thus ‖Γu‖²=‖u‖²−‖Tu‖². The anonymous actual-input Test also checks ‖Γu‖≤‖u‖. This is a scalar B.11 precursor. Printed joint ΓP still requires the same onto M, restriction to ran(P) and the typed B*B identity; no full-space inverse is claimed.

\[\|\Gamma u\|^2=\|u\|^2-\|Tu\|^2,\quad\|\Gamma u\|\le\|u\|.\]
Corresponding Lean step

hEnergy; hTs.isSymmetric; hs; real_inner_self_eq_norm_sq

Lean verification

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

Lean proof · actual_positive_real_defect_root

Produce the genuine reflected kernel and scalar defect; Apply the shared real-root theorem to that same defect; Identify the scalar norm defect

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 actual_positive_real_defect_root
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ)*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ)*‖v‖^2)
    (hη : 0 < η) (hβη : (β : ℝ)*η ≤ 1) :
    let μ := (volume : Measure E).tilted (fun x => -V x)
    let J := (μ.prod (stdGaussian E)).map
      (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
    let ν := J.snd
    let Λ := J.map (fun p : E × E => (p.2,(2 : ℝ) • p.1-p.2))
    IsProbabilityMeasure μ ∧ IsProbabilityMeasure J ∧ IsProbabilityMeasure ν ∧
    ∃ S : Kernel E E, IsMarkovKernel S ∧
      (∀ y, S y = (volume : Measure E).tilted
        (fun x => -V ((1/2 : ℝ) • (y+x)) - ‖y-x‖^2/(8*η))) ∧
      Λ.IsCondKernel S ∧ Λ.fst = ν ∧ Λ.snd = ν ∧
      ∃ T : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν,
        IsSelfAdjoint T ∧
        (∀ u : Lp ℝ 2 ν, ‖T u‖ ≤ ‖u‖ ∧
          (T u : E → ℝ) =ᵐ[ν] (fun y => ∫ x, u x ∂S y) ∧
          (∫ y, T u y ∂ν) = ∫ y, u y ∂ν) ∧
        ((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T).IsPositive ∧
        ∃ Γ : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν,
          Γ.IsPositive ∧ Γ*Γ = ((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T) ∧
          ∀ u : Lp ℝ 2 ν, ‖Γ u‖^2 = ‖u‖^2-‖T u‖^2 := by
  classical
  dsimp only
  let μ := (volume : Measure E).tilted (fun x => -V x)
  let J := (μ.prod (stdGaussian E)).map
    (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
  let ν := J.snd
  have hBase := CenteredDefectOperator.actual_centered_selfadjoint_defect
    hα hαβ hV hH hη hβη
  rcases hBase with ⟨hμ,hJ,hν,S,hS,hSd,hSc,hSf,hSs,U,hU,hUi,hUs,M,hM,T,hTs,hAll,
    q,hq,hTq,hqi,hzero,hD,hRest⟩
  obtain ⟨Γ,hΓ,hΓSq,hEnergy⟩ :=
    AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareRoot.exists_positive_real_square_root
      ν ((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T) hD
  refine ⟨hμ,hJ,hν,S,hS,hSd,hSc,hSf,hSs,T,hTs,?_,hD,Γ,hΓ,hΓSq,?_⟩
  · intro u
    exact (hAll u).2.2
  · intro u
    rw [hEnergy]
    simp only [ContinuousLinearMap.sub_apply, ContinuousLinearMap.one_apply,
      ContinuousLinearMap.mul_apply, inner_sub_left]
    have hs : inner ℝ (T (T u)) u = inner ℝ (T u) (T u) := hTs.isSymmetric (T u) u
    rw [hs,real_inner_self_eq_norm_sq,real_inner_self_eq_norm_sq]

end
end AutoSamplingTheory.ExampleCases.ProximalBPS.RealDefectRoot

#print axioms AutoSamplingTheory.ExampleCases.ProximalBPS.RealDefectRoot.actual_positive_real_defect_root

Exact module and namespace context

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
D.1 positive square-root background on a complete real Hilbert space.Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including the explicit rank-zero extension. Let V:E→ℝ be C², let 0<α≤β, and assume α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v. Assume η>0 and βη≤1. Define μ(dx) proportional to exp(−V(x))dx, J as the law of (X,X+√η Z) for independent X∼μ,Z∼N(0,I), ν=J.snd, and Λ as the law of (Y,2X−Y) under J.sameASTIS background completion is attributed. Generic D positivity is its exact mathematical input; actual paper D positivity is proved inside original-binder consumer.
Actual normalized Gaussian-reflection kernel and conditional scalar observable.Actual normalized S at every y; true disintegration/stationary marginals and AE scalar T action with mean preservation; sameD root.sameNo fallback objects, supplied representatives, finite L² assumption or extra root/extension certificate.
Euclidean finite base geometry convention.Finite real Hilbert/Borel extension, including rank-zero geometry and αη=1.generalizationOriginal curvature and step restrictions retained; zero dimension is explicit extension.
Unique printed joint/macro GammaP, B.11 identity, centered root order/inverse/polar and full algorithms/costs.REAL scalar positive root and scalar energy only. Generic real uniqueness, canonical joint GammaP / P U blocks / onto transport / typed B*B, centered root order/inverse/polar, weakH1,dynamics,hypocoercivity,main,error,cost,composition remain separate; paper/Goal open.unresolvedThis proves only positive scalar REAL root existence and energy. Real uniqueness, SAME ontoM transport and joint typed B*B still separate; no main theorem, functor or cost claim.

REAL scalar positive root and scalar energy only. Generic real uniqueness, canonical joint GammaP / P U blocks / onto transport / typed B*B, centered root order/inverse/polar, weakH1,dynamics,hypocoercivity,main,error,cost,composition remain separate; paper/Goal open.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

  • domains: Real AE quotient/completeness and scalar-field typing made explicit; finite L2 not assumed. — Independent native explicit-elaboration nonblocking classification retained in runs/20261007-companion-priority/pbps-real-defect-root61/source-review61/source.1.review.json
  • assumptions: Complex CFC, conjugation preservation and full real descent are internal proof edges, no public extra premise. — Independent native dependency-not-source-binder nonblocking classification retained in runs/20261007-companion-priority/pbps-real-defect-root61/source-review61/source.1.review.json
  • scopes: Only bounded positive REAL scalar root existence and all-observable energy. Exported generic real uniqueness, same canonical ontoM/joint ΓP/typed B*B transport, centered root order/inverse/polar, weakH1/dynamics/main/error/cost/composition remain separate; no full-paper or Goal completion. — Independent native unresolved-source-boundary nonblocking classification retained in runs/20261007-companion-priority/pbps-real-defect-root61/source-review61/source.1.review.json
  • domains: Finite real Hilbert/Borel coordinates and rank-zero base extend Euclidean source; original potential/step hypotheses retained. — Independent native disclosed-domain-extension nonblocking classification retained in runs/20261007-companion-priority/pbps-real-defect-root61/source-review61/source.1.review.json
  • quantifiers: Every-y normalized S distinguished from per-observable ν-AE T action, with nested fixed S/T/Γ serving all quantifiers. — Independent native explicit-elaboration nonblocking classification retained in runs/20261007-companion-priority/pbps-real-defect-root61/source-review61/source.1.review.json
  • conclusion: Same actual59 D yields scalar root/energy only. Full source ΓP/B11 still requires ontoM and typed microscopic square transport. — Independent native scalar-precursor-not-joint-theorem nonblocking classification retained in runs/20261007-companion-priority/pbps-real-defect-root61/source-review61/source.1.review.json

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
  • REAL scalar positive root and scalar energy only. Generic real uniqueness, canonical joint GammaP / P U blocks / onto transport / typed B*B, centered root order/inverse/polar, weakH1,dynamics,hypocoercivity,main,error,cost,composition remain separate; paper/Goal open.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • ContinuousLinearMap.sub_apply
  • ContinuousLinearMap.mul_apply
  • IsSelfAdjoint.isSymmetric
  • real_inner_self_eq_norm_sq

Mathematical sources

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

Which proof obligations and prerequisites are covered?

  • Formalized proof edge; source adapter/review separate Actual PBPS squared defect: positive real root and energy
  • TODO — not closed by these contributions Printed GammaP/B11, uniqueness, centered root/polar/H1/dynamics/main/error/cost/composition remain open