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

Same actual PBPS root and centered inverse commutation

Fan Chen,Sinho Chewi,Jianfeng Lu and Matthew S. Zhang;Appendix B3 spectral commutation used by B20/B23/B21. ASTIS explicitly constructs the actual centered restriction and real-L2 adapter;this ingredient is not the full energy theorem.

arXiv:2609.06905v1;Lean4.33.0/fixedMathlib · PBPS2609.06905v1 Appendix B3: B20 corrector definition, Lemma B.3 sharp B23 estimate and B21 rotation. Same spectral square root, actual centered restriction and inverse commutation; ASTIS positive-square commutation background adapter. · 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², 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~μ and Z~N(0,I), ν=J.snd, and Λ as the law of (Y,2X−Y) under J. These are probability laws. Put mY=comap(snd), H_P=L² classes measurable with respect to mY, P=i∘E[·|Y] and the canonical M:u↦u∘snd. Then H_P=ran(P), P is identity on H_P, and there exists an onto linear isometry e:L²(ν;ℝ)≃H_P with i e=M. There is a Markov kernel S whose every-state normalized law is S(y)=volume.tilted(x↦−V((y+x)/2)−‖y−x‖²/(8η)); Λ.IsCondKernel S and both Λ marginals equal ν. The same joint reflection F(x,y)=(x,2x−y) gives the involutive selfadjoint isometry U, with Uf=f∘F J-almost everywhere for every f. There is a bounded selfadjoint T on the full real L²(ν), with ‖Tu‖≤‖u‖, Tu(y)=∫u(x)S(y,dx) ν-almost everywhere for each u, and preserved integral. On H_P put A=PUP restricted via i and orthogonal projection, and B=(I_J−P)UPi:H_P→L²(J). Then A=eTe⁻¹ is selfadjoint and contractive, PB=0. There is a bounded positive operator Γ on the real scalar-valued L² space with Γ²=I−T². For the SAME transported Γ_P=eΓe⁻¹, positivity holds and Γ_P²=I_H_P−A²=B*B. There is q∈L²(ν;ℝ) equal to one ν-almost everywhere, with Tq=q and ⟨q,u⟩=∫u dν for every u. Set q_P=e q and H_P^0=ker⟨q_P,·⟩, with its inherited Hilbert structure. Membership is exactly zero ν-mean after e⁻¹. The SAME Γ_P annihilates q_P. Put γ=2√(αη)/(1+αη)>0. There exists Γ_0:H_P^0→H_P^0 equal under inclusion to the restriction of Γ_P, positive with Γ_0−γ I positive. Γ_0 is a unit in the algebra of bounded real operators. There exists a bounded real Inv on this SAME centered space with Inv Γ_0=Γ_0 Inv=I and ‖Inv‖≤1/γ. All probability, normalization, range, root, centering, spectral-gap, unit and inverse facts are internally derived from the original inputs; none is an additional public premise. αη=1 and rank-zero E remain legal. No inverse on full H_P is asserted. Define the actual closed conditional-mean-zero space H_perp=ker P in L²(J;ℝ), with its inherited complete Hilbert structure; this is not merely the globally zero-mean joint space. There exists B_0:H_P^0→H_perp whose inclusion equals B i_0. There exists V_0:H_P^0→H_perp with V_0=B_0 Inv, B_0=V_0 Γ_0, V_0* V_0=I and ‖V_0 f‖=‖f‖ for every f∈H_P^0. All these objects and identities are conclusions from the same original inputs. There exists the canonical bounded residual map R:L²(J;ℝ)→H_perp with i_perp Rg=g−Pg for every joint g. The SAME ambient adjoint satisfies B* g=i_0 B_0* Rg for every joint g; the printed intrinsic block adjoint is recovered on H_perp. For every actual joint f∈L²(J;ℝ) with ∫f dJ=0, there exists f_P∈H_P^0 whose inclusion is E[f|Y]. Put f_perp=Rf and f_V=V_0* f_perp∈the SAME H_P^0. Then B* i_perp f_perp=i_0 Γ_0 f_V=Γ_P i_0 f_V, ‖f‖²=‖f_P‖²+‖f_perp‖² and ‖f_V‖≤‖f_perp‖. The preceding independently reviewed ambient-adjoint Test derives f=i i_0 f_P+i_perp f_perp, B* f=Γ_P i_0 f_V and ‖f_V‖²≤‖f‖²−‖f_P‖². The global zero-mean condition is a quantified input restriction to this concluded implication, not an extra assumption on the potential or an operator certificate. The SAME root commutes with T and its transport commutes with A. The SAME Inv on H_P^0 is selfadjoint. There exists an internally constructed A_0:H_P^0→H_P^0 whose inclusion equals A after inclusion; it is selfadjoint,commutes with Γ_0,satisfies A_0²+Γ_0²=I,and commutes with the SAME Inv. The genuine original-input Test proves K=A_0 Inv selfadjoint and I+K²=Inv². All old ambient-adjoint/global-centered-observable conclusions persist. These are ingredients for sharp B23 and B21;neither estimate/rotation nor full dynamics,expected costs or composition is asserted. Private literal proposition definitions store the complete original statements and add no premise or provider.

  • Finite-dimensional real Hilbert Borel base E with canonical volume, including the disclosed rank-zero extension; V is C²; 0<α≤β; both global Hessian bounds; η>0 and βη≤1.
  • Canonical normalized laws/kernel, onto pullback e, SAME U/T, full and centered roots, exact centering, gap, unit and bounded inverse are conclusions. Conditional actions are per-observable AE. L² is not assumed finite-dimensional.
  • γ=2√(αη)/(1+αη); the inverse acts only on H_P^0=ker⟨e1,·⟩ with inherited Hilbert structure; the legal endpoint αη=1 is retained.
  • H_perp is exactly ker P (conditional expectation given Y), while H_P^0 is the zero ν-mean macroscopic space. Their complete Hilbert structures, B_0 and V_0 are internally constructed; no onto-kerP or coisometry assumption is introduced.
  • The concluded global-input implication quantifies every f∈L²(J) with integral zero. R,conditional centering,constant annihilation,adjoint range and norm decomposition are derived internally. Private statement definitions expand literally to the original sealed propositions and add no premise.

Same actual PBPS root and centered inverse commutation

\[[\Gamma,T]=[\Gamma_P,A]=[A_0,\Gamma_0]=[A_0,\mathrm{Inv}]=0,\quad\mathrm{Inv}^*=\mathrm{Inv},\quad I+(A_0\mathrm{Inv})^2=\mathrm{Inv}^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

Same actual PBPS root and centered inverse commutation

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualRootCommutation.actual_same_root_inverse_commutation · 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², 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~μ and Z~N(0,I), ν=J.snd, and Λ as the law of (Y,2X−Y) under J. These are probability laws. Put mY=comap(snd), H_P=L² classes measurable with respect to mY, P=i∘E[·|Y] and the canonical M:u↦u∘snd. Then H_P=ran(P), P is identity on H_P, and there exists an onto linear isometry e:L²(ν;ℝ)≃H_P with i e=M. There is a Markov kernel S whose every-state normalized law is S(y)=volume.tilted(x↦−V((y+x)/2)−‖y−x‖²/(8η)); Λ.IsCondKernel S and both Λ marginals equal ν. The same joint reflection F(x,y)=(x,2x−y) gives the involutive selfadjoint isometry U, with Uf=f∘F J-almost everywhere for every f. There is a bounded selfadjoint T on the full real L²(ν), with ‖Tu‖≤‖u‖, Tu(y)=∫u(x)S(y,dx) ν-almost everywhere for each u, and preserved integral. On H_P put A=PUP restricted via i and orthogonal projection, and B=(I_J−P)UPi:H_P→L²(J). Then A=eTe⁻¹ is selfadjoint and contractive, PB=0. There is a bounded positive operator Γ on the real scalar-valued L² space with Γ²=I−T². For the SAME transported Γ_P=eΓe⁻¹, positivity holds and Γ_P²=I_H_P−A²=B*B. There is q∈L²(ν;ℝ) equal to one ν-almost everywhere, with Tq=q and ⟨q,u⟩=∫u dν for every u. Set q_P=e q and H_P^0=ker⟨q_P,·⟩, with its inherited Hilbert structure. Membership is exactly zero ν-mean after e⁻¹. The SAME Γ_P annihilates q_P. Put γ=2√(αη)/(1+αη)>0. There exists Γ_0:H_P^0→H_P^0 equal under inclusion to the restriction of Γ_P, positive with Γ_0−γ I positive. Γ_0 is a unit in the algebra of bounded real operators. There exists a bounded real Inv on this SAME centered space with Inv Γ_0=Γ_0 Inv=I and ‖Inv‖≤1/γ. All probability, normalization, range, root, centering, spectral-gap, unit and inverse facts are internally derived from the original inputs; none is an additional public premise. αη=1 and rank-zero E remain legal. No inverse on full H_P is asserted. Define the actual closed conditional-mean-zero space H_perp=ker P in L²(J;ℝ), with its inherited complete Hilbert structure; this is not merely the globally zero-mean joint space. There exists B_0:H_P^0→H_perp whose inclusion equals B i_0. There exists V_0:H_P^0→H_perp with V_0=B_0 Inv, B_0=V_0 Γ_0, V_0* V_0=I and ‖V_0 f‖=‖f‖ for every f∈H_P^0. All these objects and identities are conclusions from the same original inputs. There exists the canonical bounded residual map R:L²(J;ℝ)→H_perp with i_perp Rg=g−Pg for every joint g. The SAME ambient adjoint satisfies B* g=i_0 B_0* Rg for every joint g; the printed intrinsic block adjoint is recovered on H_perp. For every actual joint f∈L²(J;ℝ) with ∫f dJ=0, there exists f_P∈H_P^0 whose inclusion is E[f|Y]. Put f_perp=Rf and f_V=V_0* f_perp∈the SAME H_P^0. Then B* i_perp f_perp=i_0 Γ_0 f_V=Γ_P i_0 f_V, ‖f‖²=‖f_P‖²+‖f_perp‖² and ‖f_V‖≤‖f_perp‖. The preceding independently reviewed ambient-adjoint Test derives f=i i_0 f_P+i_perp f_perp, B* f=Γ_P i_0 f_V and ‖f_V‖²≤‖f‖²−‖f_P‖². The global zero-mean condition is a quantified input restriction to this concluded implication, not an extra assumption on the potential or an operator certificate. The SAME root commutes with T and its transport commutes with A. The SAME Inv on H_P^0 is selfadjoint. There exists an internally constructed A_0:H_P^0→H_P^0 whose inclusion equals A after inclusion; it is selfadjoint,commutes with Γ_0,satisfies A_0²+Γ_0²=I,and commutes with the SAME Inv. The genuine original-input Test proves K=A_0 Inv selfadjoint and I+K²=Inv². All old ambient-adjoint/global-centered-observable conclusions persist. These are ingredients for sharp B23 and B21;neither estimate/rotation nor full dynamics,expected costs or composition is asserted. Private literal proposition definitions store the complete original statements and add no premise or provider.

\[[\Gamma,T]=[\Gamma_P,A]=[A_0,\Gamma_0]=[A_0,\mathrm{Inv}]=0,\quad\mathrm{Inv}^*=\mathrm{Inv},\quad I+(A_0\mathrm{Inv})^2=\mathrm{Inv}^2.\]
Lean statement · actual_same_root_inverse_commutation

Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including the explicit rank-zero extension. Let V:E→ℝ be C², 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~μ and Z~N(0,I), ν=J.snd, and Λ as the law of (Y,2X−Y) under J. These are probability laws. Put mY=comap(snd), H_P=L² classes measurable with respect to mY, P=i∘E[·|Y] and the canonical M:u↦u∘snd. Then H_P=ran(P), P is identity on H_P, and there exists an onto linear isometry e:L²(ν;ℝ)≃H_P with i e=M. There is a Markov kernel S whose every-state normalized law is S(y)=volume.tilted(x↦−V((y+x)/2)−‖y−x‖²/(8η)); Λ.IsCondKernel S and both Λ marginals equal ν. The same joint reflection F(x,y)=(x,2x−y) gives the involutive selfadjoint isometry U, with Uf=f∘F J-almost everywhere for every f. There is a bounded selfadjoint T on the full real L²(ν), with ‖Tu‖≤‖u‖, Tu(y)=∫u(x)S(y,dx) ν-almost everywhere for each u, and preserved integral. On H_P put A=PUP restricted via i and orthogonal projection, and B=(I_J−P)UPi:H_P→L²(J). Then A=eTe⁻¹ is selfadjoint and contractive, PB=0. There is a bounded positive operator Γ on the real scalar-valued L² space with Γ²=I−T². For the SAME transported Γ_P=eΓe⁻¹, positivity holds and Γ_P²=I_H_P−A²=B*B. There is q∈L²(ν;ℝ) equal to one ν-almost everywhere, with Tq=q and ⟨q,u⟩=∫u dν for every u. Set q_P=e q and H_P^0=ker⟨q_P,·⟩, with its inherited Hilbert structure. Membership is exactly zero ν-mean after e⁻¹. The SAME Γ_P annihilates q_P. Put γ=2√(αη)/(1+αη)>0. There exists Γ_0:H_P^0→H_P^0 equal under inclusion to the restriction of Γ_P, positive with Γ_0−γ I positive. Γ_0 is a unit in the algebra of bounded real operators. There exists a bounded real Inv on this SAME centered space with Inv Γ_0=Γ_0 Inv=I and ‖Inv‖≤1/γ. All probability, normalization, range, root, centering, spectral-gap, unit and inverse facts are internally derived from the original inputs; none is an additional public premise. αη=1 and rank-zero E remain legal. No inverse on full H_P is asserted. Define the actual closed conditional-mean-zero space H_perp=ker P in L²(J;ℝ), with its inherited complete Hilbert structure; this is not merely the globally zero-mean joint space. There exists B_0:H_P^0→H_perp whose inclusion equals B i_0. There exists V_0:H_P^0→H_perp with V_0=B_0 Inv, B_0=V_0 Γ_0, V_0* V_0=I and ‖V_0 f‖=‖f‖ for every f∈H_P^0. All these objects and identities are conclusions from the same original inputs. There exists the canonical bounded residual map R:L²(J;ℝ)→H_perp with i_perp Rg=g−Pg for every joint g. The SAME ambient adjoint satisfies B* g=i_0 B_0* Rg for every joint g; the printed intrinsic block adjoint is recovered on H_perp. For every actual joint f∈L²(J;ℝ) with ∫f dJ=0, there exists f_P∈H_P^0 whose inclusion is E[f|Y]. Put f_perp=Rf and f_V=V_0* f_perp∈the SAME H_P^0. Then B* i_perp f_perp=i_0 Γ_0 f_V=Γ_P i_0 f_V, ‖f‖²=‖f_P‖²+‖f_perp‖² and ‖f_V‖≤‖f_perp‖. The preceding independently reviewed ambient-adjoint Test derives f=i i_0 f_P+i_perp f_perp, B* f=Γ_P i_0 f_V and ‖f_V‖²≤‖f‖²−‖f_P‖². The global zero-mean condition is a quantified input restriction to this concluded implication, not an extra assumption on the potential or an operator certificate. The SAME root commutes with T and its transport commutes with A. The SAME Inv on H_P^0 is selfadjoint. There exists an internally constructed A_0:H_P^0→H_P^0 whose inclusion equals A after inclusion; it is selfadjoint,commutes with Γ_0,satisfies A_0²+Γ_0²=I,and commutes with the SAME Inv. The genuine original-input Test proves K=A_0 Inv selfadjoint and I+K²=Inv². All old ambient-adjoint/global-centered-observable conclusions persist. These are ingredients for sharp B23 and B21;neither estimate/rotation nor full dynamics,expected costs or composition is asserted. Private literal proposition definitions store the complete original statements and add no premise or provider.

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_same_root_inverse_commutation
    {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) : actual_same_root_inverse_commutation_statement (E := E) (V := V) (α := α) (β := β) (η := η) hα hαβ hV hH hη hβη

Exact module and namespace context

Proof roadmap

  1. 1Retain the exact actual witnesses

    Reuse the original-input parent and SAME laws,kernel,operators,roots,inverse,polar and centered geometry;fix their exact spaces.

  2. 2Produce positivity and root commutation internally

    Selfadjoint contraction and Cauchy-Schwarz give I+T positive. Γ²=I−T² commutes with I+T. The reusable leaf then yields Γ commuting with T.

  3. 3Transport and construct the exact centered restriction

    Conjugate commutation. Tq=q implies AqP=qP;symmetry preserves the exact zero-mean kernel. Construct A0 by codomain restriction and prove selfadjointness.

  4. 4Restrict the square identity and commutation

    Use exact inclusion identities and injectivity of the centered subspace inclusion.

  5. 5Cancel with the same inverse

    Taking adjoints gives Γ0 Inv*=I. Both inverse identities imply Inv selfadjoint;commutation of A0 with Γ0 passes to Inv by cancellation.

  6. 6Consume the B23 coefficient identity at original inputs

    The Test starts from the original potential and step inputs. The product of commuting selfadjoint operators is selfadjoint;multiplying the exact square identity by Inv² gives the coefficient identity.

Full assumptions and notation

All objects and hypotheses

  • Finite-dimensional real Hilbert Borel base E with canonical volume, including the disclosed rank-zero extension; V is C²; 0<α≤β; both global Hessian bounds; η>0 and βη≤1.
  • Canonical normalized laws/kernel, onto pullback e, SAME U/T, full and centered roots, exact centering, gap, unit and bounded inverse are conclusions. Conditional actions are per-observable AE. L² is not assumed finite-dimensional.
  • γ=2√(αη)/(1+αη); the inverse acts only on H_P^0=ker⟨e1,·⟩ with inherited Hilbert structure; the legal endpoint αη=1 is retained.
  • H_perp is exactly ker P (conditional expectation given Y), while H_P^0 is the zero ν-mean macroscopic space. Their complete Hilbert structures, B_0 and V_0 are internally constructed; no onto-kerP or coisometry assumption is introduced.
  • The concluded global-input implication quantifies every f∈L²(J) with integral zero. R,conditional centering,constant annihilation,adjoint range and norm decomposition are derived internally. Private statement definitions expand literally to the original sealed propositions and add no premise.

Mathematical proof

1. Retain the exact actual witnesses

Reuse the original-input parent and SAME laws,kernel,operators,roots,inverse,polar and centered geometry;fix their exact spaces.

\[\Gamma_P=e\Gamma e^{-1},\quad H_P^0=\ker\langle q_P,\cdot\rangle,\quad\Gamma_0^{-1}=\mathrm{Inv}.\]
Corresponding Lean step
  classical
  unfold actual_same_root_inverse_commutation_statement
  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
  let mY : MeasurableSpace (E × E) := MeasurableSpace.comap Prod.snd (inferInstance : MeasurableSpace E)
  letI : MeasurableSpace (E × E) := Prod.instMeasurableSpace
  letI : Fact (mY ≤ (inferInstance : MeasurableSpace (E × E))) := ⟨measurable_snd.comap_le⟩
  let HP := lpMeas ℝ ℝ mY 2 J
  letI : NormedAddCommGroup HP := HP.normedAddCommGroup
  letI : InnerProductSpace ℝ HP := HP.innerProductSpace
  let P : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J :=
    HP.subtypeL ∘L condExpL2 ℝ ℝ (μ := J) measurable_snd.comap_le
  have hBase := AutoSamplingTheory.ExampleCases.ProximalBPS.AmbientAdjointCorrector.actual_ambient_adjoint_centered_decomposition
    (E:=E) (V:=V) (α:=α) (β:=β) (η:=η) hα hαβ hV hH hη hβη
  rcases hBase with
    ⟨hμ,hJ,hν,hRange,hPf,S,hS,hSd,hSc,hSf,hSs,e,he,U,hU,hUi,hUs,
      T,hTs,hAll,hAeq,hAs,hAn,hPB,Γ,hΓ,hΓSq,hΓP,hΓPSq,hGram,
      q,hqa,hTq,hq,hCenter,hΓPq,hγ,ΓP0,hΓP0,hPos0,hOrder0,hUnit,
      Inv,hLeft,hRight,hNormInv,B0,hB0,V0,hVdef,hFactor,hVadj,hVnorm,R,hR,hAmbient,hGlobal⟩
  let A : HP →L[ℝ] HP := HP.orthogonalProjectionOnto ∘L U.toContinuousLinearMap ∘L HP.subtypeL
  let B : HP →L[ℝ] Lp ℝ 2 J :=
    (((1 : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J)-P)*U.toContinuousLinearMap*P) ∘L HP.subtypeL
  let ΓP : HP →L[ℝ] HP := e.conjStarAlgEquiv Γ
  let qP : HP := e q
  let HP0 := (innerSL ℝ qP).ker
  letI : NormedAddCommGroup HP0 := HP0.normedAddCommGroup
  letI : InnerProductSpace ℝ HP0 := HP0.innerProductSpace
  letI : CompleteSpace HP0 := (innerSL ℝ qP).isClosed_ker.completeSpace_coe
  let Hperp := P.ker
  letI : NormedAddCommGroup Hperp := Hperp.normedAddCommGroup
  letI : InnerProductSpace ℝ Hperp := Hperp.innerProductSpace
  letI : CompleteSpace Hperp := P.isClosed_ker.completeSpace_coe
  change HP0 →L[ℝ] Hperp at B0 V0
  change HP0 →L[ℝ] HP0 at ΓP0 Inv
  change Lp ℝ 2 J →L[ℝ] Hperp at R
  change (∀ g : Lp ℝ 2 J, (R g : Lp ℝ 2 J)=g-P g) at hR
  change (∀ g : Lp ℝ 2 J,
    B.adjoint g=HP0.subtypeL (B0.adjoint (R g))) at hAmbient
  change (∀ f : Lp ℝ 2 J, (∫ z, f z ∂J)=0 →
    ∃ fP : HP0,
      HP0.subtypeL fP=condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le f ∧
      let fperp : Hperp := R f
      let fV : HP0 := V0.adjoint fperp
      B.adjoint (fperp : Lp ℝ 2 J)=HP0.subtypeL (ΓP0 fV) ∧
      HP0.subtypeL (ΓP0 fV)=ΓP (HP0.subtypeL fV) ∧
      ‖f‖^2=‖fP‖^2+‖fperp‖^2 ∧ ‖fV‖≤‖fperp‖) at hGlobal

Literal compiled BODY span;exact preceding locals remain in scope.

2. Produce positivity and root commutation internally

Selfadjoint contraction and Cauchy-Schwarz give I+T positive. Γ²=I−T² commutes with I+T. The reusable leaf then yields Γ commuting with T.

\[\langle(I+T)u,u\rangle\ge\|u\|^2-\|Tu\|\|u\|\ge0,\quad[\Gamma^2,I+T]=0\Rightarrow[\Gamma,T]=0.\]
Corresponding Lean step
  have hAeqLocal : A=e.conjStarAlgEquiv T := hAeq
  have hAsLocal : IsSelfAdjoint A := hAs
  have hLeftLocal : Inv*ΓP0=(1 : HP0 →L[ℝ] HP0) := hLeft
  have hPosLocal : ΓP0.IsPositive := hPos0
  have hDpos : ((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)+T).IsPositive := by
    refine ⟨((IsSelfAdjoint.one (Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)).add hTs).isSymmetric,?_⟩
    intro u
    change 0 ≤ inner ℝ (u+T u) u
    rw [inner_add_left,real_inner_self_eq_norm_sq]
    have hn : ‖T u‖≤‖u‖ := (hAll u).1
    have hi := (abs_le.mp (abs_real_inner_le_norm (T u) u)).1
    nlinarith only [hn,hi,norm_nonneg u]
  have hCommSquare : Commute (Γ*Γ) ((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)+T) := by
    rw [hΓSq]
    show (1-T*T)*(1+T)=(1+T)*(1-T*T)
    noncomm_ring
  have hCommRootPlus := AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareCommute.positive_square_commutation
    ν Γ (1+T) hΓ hDpos hCommSquare
  have hCommRoot : Commute Γ T := by
    have h := hCommRootPlus.eq
    simp only [mul_add,add_mul,mul_one,one_mul] at h
    exact add_left_cancel h

Literal compiled BODY span;exact preceding locals remain in scope.

3. Transport and construct the exact centered restriction

Conjugate commutation. Tq=q implies AqP=qP;symmetry preserves the exact zero-mean kernel. Construct A0 by codomain restriction and prove selfadjointness.

\[[\Gamma_P,A]=0,\quad Aq_P=q_P,\quad\langle q_P,Au\rangle=\langle Aq_P,u\rangle=0\quad(u\in H_P^0).\]
Corresponding Lean step
  have hCommP : Commute ΓP A := by
    change ΓP*A=A*ΓP
    change (e.conjStarAlgEquiv Γ)*A=A*(e.conjStarAlgEquiv Γ)
    rw [hAeqLocal,← map_mul,← map_mul,hCommRoot.eq]
  have hAq : A qP=qP := by
    rw [hAeqLocal]
    change e (T (e.symm (e q)))=e q
    rw [e.symm_apply_apply,hTq]
  have hAPreserves (u : HP0) : A (u : HP) ∈ HP0 := by
    change inner ℝ qP (A (u : HP))=0
    calc
      inner ℝ qP (A (u : HP))=inner ℝ (A qP) (u : HP) :=
        (hAsLocal.isSymmetric qP (u : HP)).symm
      _ = inner ℝ qP (u : HP) := by rw [hAq]
      _ = 0 := u.property
  let A0 : HP0 →L[ℝ] HP0 := (A.comp HP0.subtypeL).codRestrict HP0 hAPreserves
  have hA0 (u : HP0) : (A0 u : HP)=A (u : HP) := rfl
  have hA0self : IsSelfAdjoint A0 := by
    apply ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric.mpr
    intro u v
    exact hAsLocal.isSymmetric (u : HP) (v : HP)

Literal compiled BODY span;exact preceding locals remain in scope.

4. Restrict the square identity and commutation

Use exact inclusion identities and injectivity of the centered subspace inclusion.

\[[A_0,\Gamma_0]=0,\qquad A_0^2+\Gamma_0^2=I_{H_P^0}.\]
Corresponding Lean step
  have hComm0 : Commute A0 ΓP0 := by
    apply ContinuousLinearMap.ext
    intro u
    apply Subtype.ext
    change (A0 (ΓP0 u) : HP)=(ΓP0 (A0 u) : HP)
    rw [hA0,hΓP0,hΓP0,hA0]
    exact congrArg (fun D : HP →L[ℝ] HP => D (u : HP)) hCommP.eq.symm
  have hSquare0 : A0*A0+ΓP0*ΓP0=(1 : HP0 →L[ℝ] HP0) := by
    apply ContinuousLinearMap.ext
    intro u
    apply Subtype.ext
    change (A0 (A0 u) : HP)+(ΓP0 (ΓP0 u) : HP)=(u : HP)
    rw [hA0,hA0,hΓP0,hΓP0]
    have h : ΓP (ΓP (u : HP))=(u : HP)-A (A (u : HP)) :=
      congrArg (fun D : HP →L[ℝ] HP => D (u : HP)) hΓPSq
    rw [h]
    abel

Literal compiled BODY span;exact preceding locals remain in scope.

5. Cancel with the same inverse

Taking adjoints gives Γ0 Inv*=I. Both inverse identities imply Inv selfadjoint;commutation of A0 with Γ0 passes to Inv by cancellation.

\[\Gamma_0\mathrm{Inv}^*=I,\quad\mathrm{Inv}^*=\mathrm{Inv},\quad A_0\mathrm{Inv}=\mathrm{Inv}A_0.\]
Corresponding Lean step
  have hStarInv : ΓP0*star Inv=(1 : HP0 →L[ℝ] HP0) := by
    have h := congrArg (fun D : HP0 →L[ℝ] HP0 => star D) hLeftLocal
    simpa only [star_mul,hPosLocal.isSelfAdjoint.star_eq,star_one] using h
  have hInvSelf : IsSelfAdjoint Inv := by
    change star Inv=Inv
    calc
      star Inv=(Inv*ΓP0)*star Inv := by rw [hLeft,one_mul]
      _ = Inv*(ΓP0*star Inv) := mul_assoc _ _ _
      _ = Inv := by rw [hStarInv,mul_one]
  have hCommInv : Commute A0 Inv := by
    change A0*Inv=Inv*A0
    calc
      A0*Inv=(Inv*ΓP0)*(A0*Inv) := by rw [hLeft,one_mul]
      _ = Inv*((ΓP0*A0)*Inv) := by noncomm_ring
      _ = Inv*((A0*ΓP0)*Inv) := by rw [hComm0.eq.symm]
      _ = Inv*A0 := by simp only [mul_assoc,hRight,mul_one]

Literal compiled BODY span;exact preceding locals remain in scope.

6. Consume the B23 coefficient identity at original inputs

The Test starts from the original potential and step inputs. The product of commuting selfadjoint operators is selfadjoint;multiplying the exact square identity by Inv² gives the coefficient identity.

\[K=A_0\mathrm{Inv}=K^*,\qquad I+K^2=(\Gamma_0^2+A_0^2)\mathrm{Inv}^2=\mathrm{Inv}^2.\]
Corresponding Lean step
  have hKself : IsSelfAdjoint (A0*Inv) := (hA0self.commute_iff hInvSelf).mp hCommInv
  have hCoefficient : (1 : HP0 →L[ℝ] HP0)+(A0*Inv)*(A0*Inv)=Inv*Inv := by
    have hFirst : (ΓP0*ΓP0)*(Inv*Inv)=(1 : HP0 →L[ℝ] HP0) := by
      calc
        (ΓP0*ΓP0)*(Inv*Inv)=ΓP0*((ΓP0*Inv)*Inv) := by noncomm_ring
        _ = (1 : HP0 →L[ℝ] HP0) := by rw [hRight,one_mul,hRight]
    have hSecond : (A0*Inv)*(A0*Inv)=(A0*A0)*(Inv*Inv) := by
      calc
        (A0*Inv)*(A0*Inv)=A0*((Inv*A0)*Inv) := by noncomm_ring
        _ = A0*((A0*Inv)*Inv) := by rw [hCommInv.eq.symm]
        _ = (A0*A0)*(Inv*Inv) := by noncomm_ring
    calc
      (1 : HP0 →L[ℝ] HP0)+(A0*Inv)*(A0*Inv)=
          (ΓP0*ΓP0)*(Inv*Inv)+(A0*A0)*(Inv*Inv) := by rw [hFirst,hSecond]
      _ = (ΓP0*ΓP0+A0*A0)*(Inv*Inv) := by rw [add_mul]
      _ = Inv*Inv := by rw [add_comm,hSquare0,one_mul]

Literal compiled BODY span;exact preceding locals remain in scope.

Lean verification

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

Lean proof · actual_same_root_inverse_commutation

Retain the exact actual witnesses; Produce positivity and root commutation internally; Transport and construct the exact centered restriction; Restrict the square identity and commutation; Cancel with the same inverse; Consume the B23 coefficient identity at original inputs

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_same_root_inverse_commutation
    {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) : actual_same_root_inverse_commutation_statement (E := E) (V := V) (α := α) (β := β) (η := η) hα hαβ hV hH hη hβη := by
  classical
  unfold actual_same_root_inverse_commutation_statement
  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
  let mY : MeasurableSpace (E × E) := MeasurableSpace.comap Prod.snd (inferInstance : MeasurableSpace E)
  letI : MeasurableSpace (E × E) := Prod.instMeasurableSpace
  letI : Fact (mY ≤ (inferInstance : MeasurableSpace (E × E))) := ⟨measurable_snd.comap_le⟩
  let HP := lpMeas ℝ ℝ mY 2 J
  letI : NormedAddCommGroup HP := HP.normedAddCommGroup
  letI : InnerProductSpace ℝ HP := HP.innerProductSpace
  let P : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J :=
    HP.subtypeL ∘L condExpL2 ℝ ℝ (μ := J) measurable_snd.comap_le
  have hBase := AutoSamplingTheory.ExampleCases.ProximalBPS.AmbientAdjointCorrector.actual_ambient_adjoint_centered_decomposition
    (E:=E) (V:=V) (α:=α) (β:=β) (η:=η) hα hαβ hV hH hη hβη
  rcases hBase with
    ⟨hμ,hJ,hν,hRange,hPf,S,hS,hSd,hSc,hSf,hSs,e,he,U,hU,hUi,hUs,
      T,hTs,hAll,hAeq,hAs,hAn,hPB,Γ,hΓ,hΓSq,hΓP,hΓPSq,hGram,
      q,hqa,hTq,hq,hCenter,hΓPq,hγ,ΓP0,hΓP0,hPos0,hOrder0,hUnit,
      Inv,hLeft,hRight,hNormInv,B0,hB0,V0,hVdef,hFactor,hVadj,hVnorm,R,hR,hAmbient,hGlobal⟩
  let A : HP →L[ℝ] HP := HP.orthogonalProjectionOnto ∘L U.toContinuousLinearMap ∘L HP.subtypeL
  let B : HP →L[ℝ] Lp ℝ 2 J :=
    (((1 : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J)-P)*U.toContinuousLinearMap*P) ∘L HP.subtypeL
  let ΓP : HP →L[ℝ] HP := e.conjStarAlgEquiv Γ
  let qP : HP := e q
  let HP0 := (innerSL ℝ qP).ker
  letI : NormedAddCommGroup HP0 := HP0.normedAddCommGroup
  letI : InnerProductSpace ℝ HP0 := HP0.innerProductSpace
  letI : CompleteSpace HP0 := (innerSL ℝ qP).isClosed_ker.completeSpace_coe
  let Hperp := P.ker
  letI : NormedAddCommGroup Hperp := Hperp.normedAddCommGroup
  letI : InnerProductSpace ℝ Hperp := Hperp.innerProductSpace
  letI : CompleteSpace Hperp := P.isClosed_ker.completeSpace_coe
  change HP0 →L[ℝ] Hperp at B0 V0
  change HP0 →L[ℝ] HP0 at ΓP0 Inv
  change Lp ℝ 2 J →L[ℝ] Hperp at R
  change (∀ g : Lp ℝ 2 J, (R g : Lp ℝ 2 J)=g-P g) at hR
  change (∀ g : Lp ℝ 2 J,
    B.adjoint g=HP0.subtypeL (B0.adjoint (R g))) at hAmbient
  change (∀ f : Lp ℝ 2 J, (∫ z, f z ∂J)=0 →
    ∃ fP : HP0,
      HP0.subtypeL fP=condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le f ∧
      let fperp : Hperp := R f
      let fV : HP0 := V0.adjoint fperp
      B.adjoint (fperp : Lp ℝ 2 J)=HP0.subtypeL (ΓP0 fV) ∧
      HP0.subtypeL (ΓP0 fV)=ΓP (HP0.subtypeL fV) ∧
      ‖f‖^2=‖fP‖^2+‖fperp‖^2 ∧ ‖fV‖≤‖fperp‖) at hGlobal
  have hAeqLocal : A=e.conjStarAlgEquiv T := hAeq
  have hAsLocal : IsSelfAdjoint A := hAs
  have hLeftLocal : Inv*ΓP0=(1 : HP0 →L[ℝ] HP0) := hLeft
  have hPosLocal : ΓP0.IsPositive := hPos0
  have hDpos : ((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)+T).IsPositive := by
    refine ⟨((IsSelfAdjoint.one (Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)).add hTs).isSymmetric,?_⟩
    intro u
    change 0 ≤ inner ℝ (u+T u) u
    rw [inner_add_left,real_inner_self_eq_norm_sq]
    have hn : ‖T u‖≤‖u‖ := (hAll u).1
    have hi := (abs_le.mp (abs_real_inner_le_norm (T u) u)).1
    nlinarith only [hn,hi,norm_nonneg u]
  have hCommSquare : Commute (Γ*Γ) ((1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)+T) := by
    rw [hΓSq]
    show (1-T*T)*(1+T)=(1+T)*(1-T*T)
    noncomm_ring
  have hCommRootPlus := AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareCommute.positive_square_commutation
    ν Γ (1+T) hΓ hDpos hCommSquare
  have hCommRoot : Commute Γ T := by
    have h := hCommRootPlus.eq
    simp only [mul_add,add_mul,mul_one,one_mul] at h
    exact add_left_cancel h
  have hCommP : Commute ΓP A := by
    change ΓP*A=A*ΓP
    change (e.conjStarAlgEquiv Γ)*A=A*(e.conjStarAlgEquiv Γ)
    rw [hAeqLocal,← map_mul,← map_mul,hCommRoot.eq]
  have hAq : A qP=qP := by
    rw [hAeqLocal]
    change e (T (e.symm (e q)))=e q
    rw [e.symm_apply_apply,hTq]
  have hAPreserves (u : HP0) : A (u : HP) ∈ HP0 := by
    change inner ℝ qP (A (u : HP))=0
    calc
      inner ℝ qP (A (u : HP))=inner ℝ (A qP) (u : HP) :=
        (hAsLocal.isSymmetric qP (u : HP)).symm
      _ = inner ℝ qP (u : HP) := by rw [hAq]
      _ = 0 := u.property
  let A0 : HP0 →L[ℝ] HP0 := (A.comp HP0.subtypeL).codRestrict HP0 hAPreserves
  have hA0 (u : HP0) : (A0 u : HP)=A (u : HP) := rfl
  have hA0self : IsSelfAdjoint A0 := by
    apply ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric.mpr
    intro u v
    exact hAsLocal.isSymmetric (u : HP) (v : HP)
  have hComm0 : Commute A0 ΓP0 := by
    apply ContinuousLinearMap.ext
    intro u
    apply Subtype.ext
    change (A0 (ΓP0 u) : HP)=(ΓP0 (A0 u) : HP)
    rw [hA0,hΓP0,hΓP0,hA0]
    exact congrArg (fun D : HP →L[ℝ] HP => D (u : HP)) hCommP.eq.symm
  have hSquare0 : A0*A0+ΓP0*ΓP0=(1 : HP0 →L[ℝ] HP0) := by
    apply ContinuousLinearMap.ext
    intro u
    apply Subtype.ext
    change (A0 (A0 u) : HP)+(ΓP0 (ΓP0 u) : HP)=(u : HP)
    rw [hA0,hA0,hΓP0,hΓP0]
    have h : ΓP (ΓP (u : HP))=(u : HP)-A (A (u : HP)) :=
      congrArg (fun D : HP →L[ℝ] HP => D (u : HP)) hΓPSq
    rw [h]
    abel
  have hStarInv : ΓP0*star Inv=(1 : HP0 →L[ℝ] HP0) := by
    have h := congrArg (fun D : HP0 →L[ℝ] HP0 => star D) hLeftLocal
    simpa only [star_mul,hPosLocal.isSelfAdjoint.star_eq,star_one] using h
  have hInvSelf : IsSelfAdjoint Inv := by
    change star Inv=Inv
    calc
      star Inv=(Inv*ΓP0)*star Inv := by rw [hLeft,one_mul]
      _ = Inv*(ΓP0*star Inv) := mul_assoc _ _ _
      _ = Inv := by rw [hStarInv,mul_one]
  have hCommInv : Commute A0 Inv := by
    change A0*Inv=Inv*A0
    calc
      A0*Inv=(Inv*ΓP0)*(A0*Inv) := by rw [hLeft,one_mul]
      _ = Inv*((ΓP0*A0)*Inv) := by noncomm_ring
      _ = Inv*((A0*ΓP0)*Inv) := by rw [hComm0.eq.symm]
      _ = Inv*A0 := by simp only [mul_assoc,hRight,mul_one]
  refine ⟨hμ, ?_⟩
  refine ⟨hJ, ?_⟩
  refine ⟨hν, ?_⟩
  refine ⟨hRange, ?_⟩
  refine ⟨hPf, ?_⟩
  refine ⟨S, ?_⟩
  refine ⟨hS, ?_⟩
  refine ⟨hSd, ?_⟩
  refine ⟨hSc, ?_⟩
  refine ⟨hSf, ?_⟩
  refine ⟨hSs, ?_⟩
  refine ⟨e, ?_⟩
  refine ⟨he, ?_⟩
  refine ⟨U, ?_⟩
  refine ⟨hU, ?_⟩
  refine ⟨hUi, ?_⟩
  refine ⟨hUs, ?_⟩
  refine ⟨T, ?_⟩
  refine ⟨hTs, ?_⟩
  refine ⟨hAll, ?_⟩
  refine ⟨hAeq, ?_⟩
  refine ⟨hAs, ?_⟩
  refine ⟨hAn, ?_⟩
  refine ⟨hPB, ?_⟩
  refine ⟨Γ, ?_⟩
  refine ⟨hΓ, ?_⟩
  refine ⟨hΓSq, ?_⟩
  refine ⟨hCommRoot, ?_⟩
  refine ⟨hΓP, ?_⟩
  refine ⟨hΓPSq, ?_⟩
  refine ⟨hCommP, ?_⟩
  refine ⟨hGram, ?_⟩
  refine ⟨q, ?_⟩
  refine ⟨hqa, ?_⟩
  refine ⟨hTq, ?_⟩
  refine ⟨hq, ?_⟩
  refine ⟨hCenter, ?_⟩
  refine ⟨hΓPq, ?_⟩
  refine ⟨hγ, ?_⟩
  refine ⟨ΓP0, ?_⟩
  refine ⟨hΓP0, ?_⟩
  refine ⟨hPos0, ?_⟩
  refine ⟨hOrder0, ?_⟩
  refine ⟨hUnit, ?_⟩
  refine ⟨Inv, ?_⟩
  refine ⟨hLeft, ?_⟩
  refine ⟨hRight, ?_⟩
  refine ⟨hNormInv, ?_⟩
  refine ⟨hInvSelf,A0,hA0,hA0self,hComm0,hSquare0,hCommInv,?_⟩
  refine ⟨B0, ?_⟩
  refine ⟨hB0, ?_⟩
  refine ⟨V0, ?_⟩
  refine ⟨hVdef, ?_⟩
  refine ⟨hFactor, ?_⟩
  refine ⟨hVadj, ?_⟩
  refine ⟨hVnorm, ?_⟩
  refine ⟨R, ?_⟩
  refine ⟨hR, ?_⟩
  refine ⟨hAmbient, ?_⟩
  exact hGlobal

end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualRootCommutation

#print axioms AutoSamplingTheory.ExampleCases.ProximalBPS.ActualRootCommutation.actual_same_root_inverse_commutation

Exact module and namespace context

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
Finite-dimensional real Hilbert Borel base E with canonical volume, including the disclosed rank-zero extension; V is C²; 0<α≤β; both global Hessian bounds; η>0 and βη≤1.Finite-dimensional real Hilbert Borel base E with canonical volume, including the disclosed rank-zero extension; V is C²; 0<α≤β; both global Hessian bounds; η>0 and βη≤1.sameExact independently reviewed header;all actual operator facts are conclusions.
Remaining sharp B23/B21/full dynamics and expected costs/composition.Same-root and actual centered inverse commutation plus B23 coefficient square identity only. Sharp B23 norm estimate/B21 rotation/full energy/H1/dynamics/errors/cost/composition not yet proved. All original finite Hilbert/Borel/C2/both Hessians/positive capped eta callers preserved. D=I+T positivity and all commutations are internally proved, never extra public paper premises.unresolvedBounded commutation/coefficient ingredient only.

Same-root and actual centered inverse commutation plus B23 coefficient square identity only. Sharp B23 norm estimate/B21 rotation/full energy/H1/dynamics/errors/cost/composition not yet proved. All original finite Hilbert/Borel/C2/both Hessians/positive capped eta callers preserved. D=I+T positivity and all commutations are internally proved, never extra public paper premises.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

  • domains: Original Euclidean conditions represented on finite real Hilbert Borel space,rank-zero disclosed;closed centered and microscopic domains and literal private propositions explicitly elaborated without new premises. — B1/B2/D1 selected primary bytes; two private Prop values retain all explicit subtypeL maps and actual domain adapters. Rank-zero extension disclosed, no full-space inverse or onto V0.

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
  • Same-root and actual centered inverse commutation plus B23 coefficient square identity only. Sharp B23 norm estimate/B21 rotation/full energy/H1/dynamics/errors/cost/composition not yet proved. All original finite Hilbert/Borel/C2/both Hessians/positive capped eta callers preserved. D=I+T positivity and all commutations are internally proved, never extra public paper premises.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • Commute.cfcₙ_nnreal
  • CFC.sqrt_unique
  • ContinuousLinearMap.ext
  • ContinuousLinearMap.codRestrict
  • ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric
  • IsSelfAdjoint.commute_iff
  • LinearIsometryEquiv.conjStarAlgEquiv
  • abs_real_inner_le_norm

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 Same actual PBPS root and centered inverse commutation
  • TODO — not closed by these contributions Remaining sharp energy,rotation,dynamics,mixing,errors and expected costs/composition