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

Actual PBPS reflection intertwining on the full conditional-complement space

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang, arXiv:2609.06905v1 Appendix B.1 and B.3 (B.21), Lemma B.4. ASTIS expands the same actual conditional-complement compression and all-domain polar-adjoint intertwining.

arXiv:2609.06905v1;Lean4.33.0/fixedMathlib · PBPS2609.06905v1 Appendix B1/B3, source graph P11 actual micro intertwining, B21 rotation A2.Ex15.m2 and B4 A2.SS3.p8.m10; exact source graph independently reconstructed over419 math items. · 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 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. Define D=R U i_perp:H_perp→H_perp using the SAME produced U,R and the inclusion i_perp. For every h∈H_perp, i_perp D h=U i_perp h−P(U i_perp h). On ALL of H_perp the SAME actual polar adjoint satisfies V_0* D=−A_0 V_0*. This identity is not restricted to the range of V_0; no surjectivity or coisometry is assumed. Every preceding actual law/kernel/root/inverse/polar/ambient-adjoint and globally centered-observable conclusion persists with the same witnesses. The reflection is fixed by its almost-everywhere pullback formula; the already compiled actual reflection block identity is transported only after proving equality of that reflection with the current U. This is the full micro-space intertwining ingredient used in Appendix B.3 (B.21) and Lemma B.4. The actual projected rotation and corrector change, weak H1/B2, B4 dynamics, invariance/nonexplosion, main convergence, implementation errors/caps, expected query costs and actual-input composition remain separate. One private literal Prop stores the complete sealed proposition and supplies no mathematical proof provider or additional premise.

  • 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.
  • D=R U inclusion and V0*D=-A0V0* on all ker P are internally proved conclusions, not source hypotheses. No onto-V0, sharp-energy estimate or additional smoothness is required.

Actual PBPS reflection intertwining on the full conditional-complement space

\[D=RUi_\perp,\quad i_\perp Dh=Ui_\perp h-PUi_\perp h,\quad V_0^*D=-A_0V_0^*\quad(h\in\ker P).\]

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 reflection intertwining on the full conditional-complement space

AutoSamplingTheory.ExampleCases.ProximalBPS.ReflectionIntertwining.actual_reflection_intertwining · 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 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. Define D=R U i_perp:H_perp→H_perp using the SAME produced U,R and the inclusion i_perp. For every h∈H_perp, i_perp D h=U i_perp h−P(U i_perp h). On ALL of H_perp the SAME actual polar adjoint satisfies V_0* D=−A_0 V_0*. This identity is not restricted to the range of V_0; no surjectivity or coisometry is assumed. Every preceding actual law/kernel/root/inverse/polar/ambient-adjoint and globally centered-observable conclusion persists with the same witnesses. The reflection is fixed by its almost-everywhere pullback formula; the already compiled actual reflection block identity is transported only after proving equality of that reflection with the current U. This is the full micro-space intertwining ingredient used in Appendix B.3 (B.21) and Lemma B.4. The actual projected rotation and corrector change, weak H1/B2, B4 dynamics, invariance/nonexplosion, main convergence, implementation errors/caps, expected query costs and actual-input composition remain separate. One private literal Prop stores the complete sealed proposition and supplies no mathematical proof provider or additional premise.

\[D=RUi_\perp,\quad i_\perp Dh=Ui_\perp h-PUi_\perp h,\quad V_0^*D=-A_0V_0^*\quad(h\in\ker P).\]
Lean statement · actual_reflection_intertwining

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 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. Define D=R U i_perp:H_perp→H_perp using the SAME produced U,R and the inclusion i_perp. For every h∈H_perp, i_perp D h=U i_perp h−P(U i_perp h). On ALL of H_perp the SAME actual polar adjoint satisfies V_0* D=−A_0 V_0*. This identity is not restricted to the range of V_0; no surjectivity or coisometry is assumed. Every preceding actual law/kernel/root/inverse/polar/ambient-adjoint and globally centered-observable conclusion persists with the same witnesses. The reflection is fixed by its almost-everywhere pullback formula; the already compiled actual reflection block identity is transported only after proving equality of that reflection with the current U. This is the full micro-space intertwining ingredient used in Appendix B.3 (B.21) and Lemma B.4. The actual projected rotation and corrector change, weak H1/B2, B4 dynamics, invariance/nonexplosion, main convergence, implementation errors/caps, expected query costs and actual-input composition remain separate. One private literal Prop stores the complete sealed proposition and supplies no mathematical proof provider or additional premise.

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

Exact module and namespace context

Full Lean proposition (definition) · actual_reflection_intertwining_statement

This literal definition stores the complete proposition asserted above. It supplies no mathematical proof or additional hypothesis; the theorem proof must establish its value.

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)
private def actual_reflection_intertwining_statement
    {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) : Prop :=
    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))
    let F := fun p : E × E => (p.1,(2 : ℝ) • p.1-p.2)
    let mY := 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
    let P : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J :=
      HP.subtypeL ∘L condExpL2 ℝ ℝ (μ := J) measurable_snd.comap_le
    let hp : MeasurePreserving (Prod.snd : E × E → E) J ν := ⟨measurable_snd,rfl⟩
    let M : Lp ℝ 2 ν →ₗᵢ[ℝ] Lp ℝ 2 J := Lp.compMeasurePreservingₗᵢ ℝ Prod.snd hp
    IsProbabilityMeasure μ ∧ IsProbabilityMeasure J ∧ IsProbabilityMeasure ν ∧
    HP = P.toLinearMap.range ∧
    (∀ f : HP, P (f : Lp ℝ 2 J) = f) ∧
    ∃ 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 = ν ∧
      ∃ e : Lp ℝ 2 ν ≃ₗᵢ[ℝ] HP,
        (∀ u : Lp ℝ 2 ν, (e u : Lp ℝ 2 J) = M u) ∧
        ∃ U : Lp ℝ 2 J →ₗᵢ[ℝ] Lp ℝ 2 J,
          (∀ g : Lp ℝ 2 J, (U g : E × E → ℝ) =ᵐ[J] g ∘ F) ∧
          Function.Involutive U ∧ IsSelfAdjoint U.toContinuousLinearMap ∧
          ∃ 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 ∂ν) ∧
            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
            A = e.conjStarAlgEquiv T ∧ IsSelfAdjoint A ∧
            (∀ f : HP, ‖A f‖ ≤ ‖f‖) ∧
            (∀ f : HP, P (B f) = 0) ∧
            ∃ Γ : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν,
              Γ.IsPositive ∧ Γ*Γ=(1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T ∧
              Commute Γ T ∧
              let ΓP : HP →L[ℝ] HP := e.conjStarAlgEquiv Γ
              ΓP.IsPositive ∧ ΓP*ΓP=(1 : HP →L[ℝ] HP)-A*A ∧
              Commute ΓP A ∧
              B.adjoint ∘L B = ΓP*ΓP ∧
              ∃ q : Lp ℝ 2 ν,
                (q : E → ℝ) =ᵐ[ν] (fun _ => (1 : ℝ)) ∧ T q = q ∧
                (∀ u : Lp ℝ 2 ν, inner ℝ q u = ∫ y, u y ∂ν) ∧
                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 γ : ℝ := 2*Real.sqrt ((α : ℝ)*η)/(1+(α : ℝ)*η)
                (∀ f : HP, f ∈ HP0 ↔ (∫ y, (e.symm f) y ∂ν) = 0) ∧
                ΓP qP = 0 ∧ 0 < γ ∧
                ∃ ΓP0 : HP0 →L[ℝ] HP0,
                  (∀ f : HP0, (ΓP0 f : HP) = ΓP (f : HP)) ∧
                  ΓP0.IsPositive ∧ (ΓP0-γ • (1 : HP0 →L[ℝ] HP0)).IsPositive ∧
                  IsUnit ΓP0 ∧
                  ∃ Inv : HP0 →L[ℝ] HP0,
                    Inv*ΓP0=(1 : HP0 →L[ℝ] HP0) ∧
                    ΓP0*Inv=(1 : HP0 →L[ℝ] HP0) ∧ ‖Inv‖ ≤ 1/γ ∧
                    IsSelfAdjoint Inv ∧
                    ∃ A0 : HP0 →L[ℝ] HP0,
                      (∀ u : HP0, (A0 u : HP)=A (u : HP)) ∧
                      IsSelfAdjoint A0 ∧ Commute A0 ΓP0 ∧
                      A0*A0+ΓP0*ΓP0=(1 : HP0 →L[ℝ] HP0) ∧
                      Commute A0 Inv ∧
                    let Hperp := P.ker
                    letI : NormedAddCommGroup Hperp := Hperp.normedAddCommGroup
                    letI : InnerProductSpace ℝ Hperp := Hperp.innerProductSpace
                    letI : CompleteSpace Hperp := P.isClosed_ker.completeSpace_coe
                    ∃ B0 : HP0 →L[ℝ] Hperp,
                      (∀ f : HP0, (B0 f : Lp ℝ 2 J) = B (f : HP)) ∧
                      ∃ V0 : HP0 →L[ℝ] Hperp,
                        V0 = B0 ∘L Inv ∧ B0 = V0 ∘L ΓP0 ∧
                        V0.adjoint ∘L V0 = (1 : HP0 →L[ℝ] HP0) ∧
                        (∀ f : HP0, ‖V0 f‖ = ‖f‖) ∧
                        ∃ R : Lp ℝ 2 J →L[ℝ] Hperp,
                          (∀ g : Lp ℝ 2 J, (R g : Lp ℝ 2 J)=g-P g) ∧
                          (∀ g : Lp ℝ 2 J,
                            B.adjoint g=HP0.subtypeL (B0.adjoint (R g))) ∧
                          let D : Hperp →L[ℝ] Hperp :=
                            R ∘L U.toContinuousLinearMap ∘L Hperp.subtypeL
                          (∀ h : Hperp, (D h : Lp ℝ 2 J)=
                            U (h : Lp ℝ 2 J)-P (U (h : Lp ℝ 2 J))) ∧
                          V0.adjoint ∘L D = -(A0 ∘L V0.adjoint) ∧
                          (∀ 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‖)

Exact module and namespace context

Proof roadmap

  1. 1Fix the original probability geometry and the same witnesses

    Apply the original-input production parent and retain every probability, kernel, centered-root, inverse, polar and globally centered-observable conclusion. Both complete subspaces have their inherited Hilbert structures.

  2. 2Use the actual compression and identify the reflection

    Define D by the residual map and current reflection. The existing actual block theorem produces a reflection with the same AE pullback action; L2 extensionality proves it equals the current U before its block identity is used. Put A_J=PUP, B_J=(I-P)UP and D_J=(I-P)U(I-P).

  3. 3Match the actual inclusions

    Let iota=i i_0 include the centered macro space in the joint space. The defining B0/A0 inclusions and P h=0 for every micro h identify the actual compressed maps exactly.

  4. 4Transport the block adjoint identity on every micro input

    Test against an arbitrary centered macro vector u. Move the adjoints across the inner products, apply the actual ambient block identity, then use selfadjoint A_J and A0. The inclusion identities give the displayed equality for every h in ker P; inner-product separation yields the operator identity.

  5. 5Pass from B0 to the same polar adjoint

    The exact produced equation V0=B0 Inv and selfadjointness of the same Inv give V0*=Inv B0*. Its previously proved commutation with A0 then transports B0*D=-A0B0* without any range or surjectivity restriction.

  6. 6Preserve the complete original conclusion

    Prove the exact new tail with D semantics, full micro intertwining and the old globally centered-f conclusion, then reassemble the original witnesses. The new identity is an internal conclusion from the same six caller conditions.

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.
  • D=R U inclusion and V0*D=-A0V0* on all ker P are internally proved conclusions, not source hypotheses. No onto-V0, sharp-energy estimate or additional smoothness is required.

Mathematical proof

1. Fix the original probability geometry and the same witnesses

Apply the original-input production parent and retain every probability, kernel, centered-root, inverse, polar and globally centered-observable conclusion. Both complete subspaces have their inherited Hilbert structures.

\[H_P^0=\ker\langle q_P,\cdot\rangle,\qquad H_\perp=\ker P.\]
Corresponding Lean step
  classical
  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.ActualRootCommutation.actual_same_root_inverse_commutation
    (E:=E) (V:=V) (α:=α) (β:=β) (η:=η) hα hαβ hV hH hη hβη
  have parentSlice0 := hBase
  have hμ := parentSlice0.1
  have parentSlice1 := parentSlice0.2
  have hJ := parentSlice1.1
  have parentSlice2 := parentSlice1.2
  have hν := parentSlice2.1
  have parentSlice3 := parentSlice2.2
  have hRange := parentSlice3.1
  have parentSlice4 := parentSlice3.2
  have hPf := parentSlice4.1
  have parentSlice5 := parentSlice4.2
  obtain ⟨S, parentSlice6⟩ := parentSlice5
  have hS := parentSlice6.1
  have parentSlice7 := parentSlice6.2
  have hSd := parentSlice7.1
  have parentSlice8 := parentSlice7.2
  have hSc := parentSlice8.1
  have parentSlice9 := parentSlice8.2
  have hSf := parentSlice9.1
  have parentSlice10 := parentSlice9.2
  have hSs := parentSlice10.1
  have parentSlice11 := parentSlice10.2
  obtain ⟨e, parentSlice12⟩ := parentSlice11
  have he := parentSlice12.1
  have parentSlice13 := parentSlice12.2
  obtain ⟨U, parentSlice14⟩ := parentSlice13
  have hU := parentSlice14.1
  have parentSlice15 := parentSlice14.2
  have hUi := parentSlice15.1
  have parentSlice16 := parentSlice15.2
  have hUs := parentSlice16.1
  have parentSlice17 := parentSlice16.2
  obtain ⟨T, parentSlice18⟩ := parentSlice17
  have hTs := parentSlice18.1
  have parentSlice19 := parentSlice18.2
  have hAll := parentSlice19.1
  have parentSlice20 := parentSlice19.2
  have hAeq := parentSlice20.1
  have parentSlice21 := parentSlice20.2
  have hAs := parentSlice21.1
  have parentSlice22 := parentSlice21.2
  have hAn := parentSlice22.1
  have parentSlice23 := parentSlice22.2
  have hPB := parentSlice23.1
  have parentSlice24 := parentSlice23.2
  obtain ⟨Γ, parentSlice25⟩ := parentSlice24
  have hΓ := parentSlice25.1
  have parentSlice26 := parentSlice25.2
  have hΓSq := parentSlice26.1
  have parentSlice27 := parentSlice26.2
  have hCommRoot := parentSlice27.1
  have parentSlice28 := parentSlice27.2
  have hΓP := parentSlice28.1
  have parentSlice29 := parentSlice28.2
  have hΓPSq := parentSlice29.1
  have parentSlice30 := parentSlice29.2
  have hCommP := parentSlice30.1
  have parentSlice31 := parentSlice30.2
  have hGram := parentSlice31.1
  have parentSlice32 := parentSlice31.2
  obtain ⟨q, parentSlice33⟩ := parentSlice32
  have hqa := parentSlice33.1
  have parentSlice34 := parentSlice33.2
  have hTq := parentSlice34.1
  have parentSlice35 := parentSlice34.2
  have hq := parentSlice35.1
  have parentSlice36 := parentSlice35.2
  have hCenter := parentSlice36.1
  have parentSlice37 := parentSlice36.2
  have hΓPq := parentSlice37.1
  have parentSlice38 := parentSlice37.2
  have hγ := parentSlice38.1
  have parentSlice39 := parentSlice38.2
  obtain ⟨ΓP0, parentSlice40⟩ := parentSlice39
  have hΓP0 := parentSlice40.1
  have parentSlice41 := parentSlice40.2
  have hPos0 := parentSlice41.1
  have parentSlice42 := parentSlice41.2
  have hOrder0 := parentSlice42.1
  have parentSlice43 := parentSlice42.2
  have hUnit := parentSlice43.1
  have parentSlice44 := parentSlice43.2
  obtain ⟨Inv, parentSlice45⟩ := parentSlice44
  have hLeft := parentSlice45.1
  have parentSlice46 := parentSlice45.2
  have hRight := parentSlice46.1
  have parentSlice47 := parentSlice46.2
  have hNormInv := parentSlice47.1
  have parentSlice48 := parentSlice47.2
  have hInvSelf := parentSlice48.1
  have parentSlice49 := parentSlice48.2
  obtain ⟨A0, parentSlice50⟩ := parentSlice49
  have hA0 := parentSlice50.1
  have parentSlice51 := parentSlice50.2
  have hA0self := parentSlice51.1
  have parentSlice52 := parentSlice51.2
  have hComm0 := parentSlice52.1
  have parentSlice53 := parentSlice52.2
  have hSquare0 := parentSlice53.1
  have parentSlice54 := parentSlice53.2
  have hCommInv := parentSlice54.1
  have parentSlice55 := parentSlice54.2
  obtain ⟨B0, parentSlice56⟩ := parentSlice55
  have hB0 := parentSlice56.1
  have parentSlice57 := parentSlice56.2
  obtain ⟨V0, parentSlice58⟩ := parentSlice57
  have hVdef := parentSlice58.1
  have parentSlice59 := parentSlice58.2
  have hFactor := parentSlice59.1
  have parentSlice60 := parentSlice59.2
  have hVadj := parentSlice60.1
  have parentSlice61 := parentSlice60.2
  have hVnorm := parentSlice61.1
  have parentSlice62 := parentSlice61.2
  obtain ⟨R, parentSlice63⟩ := parentSlice62
  have hR := parentSlice63.1
  have parentSlice64 := parentSlice63.2
  have hAmbient := parentSlice64.1
  have parentSlice65 := parentSlice64.2
  have hGlobal := parentSlice65
  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 A0
  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 module locals remain in scope.

2. Use the actual compression and identify the reflection

Define D by the residual map and current reflection. The existing actual block theorem produces a reflection with the same AE pullback action; L2 extensionality proves it equals the current U before its block identity is used. Put A_J=PUP, B_J=(I-P)UP and D_J=(I-P)U(I-P).

\[i_\perp Dh=Ui_\perp h-PUi_\perp h,\quad U_2=U,\quad B_J^*D_J=-A_JB_J^*.\]
Corresponding Lean step
  let D : Hperp →L[ℝ] Hperp := R ∘L U.toContinuousLinearMap ∘L Hperp.subtypeL
  have hD (h : Hperp) : (D h : Lp ℝ 2 J)=
      U (h : Lp ℝ 2 J)-P (U (h : Lp ℝ 2 J)) := hR (U (h : Lp ℝ 2 J))
  letI : IsProbabilityMeasure μ := hμ
  obtain ⟨ρ,hρ,hρf,U2,hU2,hU2i,hU2s,hρp,hBB,hBD,hBE⟩ :=
    AutoSamplingTheory.ExampleCases.ProximalBPS.ReflectionL2.actual_reflection_block_identities μ hη
  have hU2eq : U2=U := by
    apply LinearIsometry.ext
    intro f
    apply Lp.ext
    exact (hU2 f).trans (hU f).symm
  subst U2
  let AJ : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J := P*U.toContinuousLinearMap*P
  let BA : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J := (1-P)*U.toContinuousLinearMap*P
  let DA : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J := (1-P)*U.toContinuousLinearMap*(1-P)
  have hBDtyped : BA.adjoint ∘L DA= -(AJ ∘L BA.adjoint) := hBD
  have hPself : IsSelfAdjoint P := isSelfAdjoint_starProjection HP
  have hAJself : IsSelfAdjoint AJ := by
    change star (P*U.toContinuousLinearMap*P)=P*U.toContinuousLinearMap*P
    simp only [star_mul,hPself.star_eq,hUs.star_eq,mul_assoc]

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

3. Match the actual inclusions

Let iota=i i_0 include the centered macro space in the joint space. The defining B0/A0 inclusions and P h=0 for every micro h identify the actual compressed maps exactly.

\[B_J\iota=i_\perp B_0,\quad A_J\iota=\iota A_0,\quad D_Ji_\perp=i_\perp D.\]
Corresponding Lean step
  let ι : HP0 →L[ℝ] Lp ℝ 2 J := HP.subtypeL ∘L HP0.subtypeL
  have hBambient (u : HP0) : BA (ι u)=(B0 u : Lp ℝ 2 J) := (hB0 u).symm
  have hAambient (u : HP0) : AJ (ι u)=ι (A0 u) := by
    change P (U (P ((u : HP) : Lp ℝ 2 J)))=((A0 u : HP) : Lp ℝ 2 J)
    rw [hPf]
    change (A (u : HP) : Lp ℝ 2 J)=((A0 u : HP) : Lp ℝ 2 J)
    exact congrArg (fun x : HP => (x : Lp ℝ 2 J)) (hA0 u).symm
  have hDambient (h : Hperp) : DA (h : Lp ℝ 2 J)=(D h : Lp ℝ 2 J) := by
    change U ((h : Lp ℝ 2 J)-P (h : Lp ℝ 2 J))-
      P (U ((h : Lp ℝ 2 J)-P (h : Lp ℝ 2 J)))=(D h : Lp ℝ 2 J)
    rw [show P (h : Lp ℝ 2 J)=0 from h.property,sub_zero]
    exact (hD h).symm

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

4. Transport the block adjoint identity on every micro input

Test against an arbitrary centered macro vector u. Move the adjoints across the inner products, apply the actual ambient block identity, then use selfadjoint A_J and A0. The inclusion identities give the displayed equality for every h in ker P; inner-product separation yields the operator identity.

\[\langle u,B_0^*Dh\rangle=\langle B_J\iota u,D_Ji_\perp h\rangle=-\langle B_0A_0u,h\rangle=-\langle u,A_0B_0^*h\rangle.\]
Corresponding Lean step
  have hB0intertwine : B0.adjoint ∘L D= -(A0 ∘L B0.adjoint) := by
    apply ContinuousLinearMap.ext
    intro h
    apply ext_inner_left ℝ
    intro u
    change inner ℝ u (B0.adjoint (D h))=inner ℝ u (-(A0 (B0.adjoint h)))
    calc
      inner ℝ u (B0.adjoint (D h))=inner ℝ (B0 u) (D h) := B0.adjoint_inner_right u (D h)
      _ = inner ℝ (BA (ι u)) (DA (h : Lp ℝ 2 J)) := by rw [hBambient,hDambient]; rfl
      _ = inner ℝ (ι u) (BA.adjoint (DA (h : Lp ℝ 2 J))) := (BA.adjoint_inner_right _ _).symm
      _ = inner ℝ (ι u) (-(AJ (BA.adjoint (h : Lp ℝ 2 J)))) := by
        have hb := DFunLike.congr_fun hBDtyped (h : Lp ℝ 2 J)
        change BA.adjoint (DA (h : Lp ℝ 2 J))= -(AJ (BA.adjoint (h : Lp ℝ 2 J))) at hb
        rw [hb]
      _ = -inner ℝ (AJ (ι u)) (BA.adjoint (h : Lp ℝ 2 J)) := by
        simpa only [inner_neg_right,hAJself.adjoint_eq] using
          congrArg Neg.neg (AJ.adjoint_inner_right (ι u) (BA.adjoint (h : Lp ℝ 2 J)))
      _ = -inner ℝ (BA (AJ (ι u))) (h : Lp ℝ 2 J) := by rw [BA.adjoint_inner_right]
      _ = -inner ℝ (B0 (A0 u)) h := by rw [hAambient,hBambient]; rfl
      _ = -inner ℝ (A0 u) (B0.adjoint h) := by rw [B0.adjoint_inner_right]
      _ = inner ℝ u (-(A0 (B0.adjoint h))) := by
        simpa only [inner_neg_right,hA0self.adjoint_eq] using
          (congrArg Neg.neg (A0.adjoint_inner_right u (B0.adjoint h))).symm

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

5. Pass from B0 to the same polar adjoint

The exact produced equation V0=B0 Inv and selfadjointness of the same Inv give V0*=Inv B0*. Its previously proved commutation with A0 then transports B0*D=-A0B0* without any range or surjectivity restriction.

\[V_0^*=\mathrm{Inv}\,B_0^*,\quad V_0^*D=-\mathrm{Inv}A_0B_0^*=-A_0\mathrm{Inv}B_0^*=-A_0V_0^*.\]
Corresponding Lean step
  have hVdefTyped : V0=B0 ∘L Inv := hVdef
  have hInvSelfTyped : IsSelfAdjoint Inv := hInvSelf
  have hVadjEq : V0.adjoint=Inv ∘L B0.adjoint := by
    calc
      V0.adjoint=(B0 ∘L Inv).adjoint :=
        congrArg (fun L : HP0 →L[ℝ] Hperp => L.adjoint) hVdefTyped
      _ = Inv.adjoint ∘L B0.adjoint := ContinuousLinearMap.adjoint_comp B0 Inv
      _ = Inv ∘L B0.adjoint := by rw [hInvSelfTyped.adjoint_eq]
  have hIntertwine : V0.adjoint ∘L D= -(A0 ∘L V0.adjoint) := by
    calc
      V0.adjoint ∘L D=Inv ∘L (B0.adjoint ∘L D) := by rw [hVadjEq,ContinuousLinearMap.comp_assoc]
      _ = Inv ∘L (-(A0 ∘L B0.adjoint)) := by rw [hB0intertwine]
      _ = -(A0 ∘L V0.adjoint) := by
        apply ContinuousLinearMap.ext
        intro h
        change Inv (-(A0 (B0.adjoint h)))= -(A0 (V0.adjoint h))
        rw [map_neg,hVadjEq]
        change -(Inv (A0 (B0.adjoint h)))= -(A0 (Inv (B0.adjoint h)))
        exact congrArg Neg.neg (DFunLike.congr_fun hCommInv.eq (B0.adjoint h)).symm

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

6. Preserve the complete original conclusion

Prove the exact new tail with D semantics, full micro intertwining and the old globally centered-f conclusion, then reassemble the original witnesses. The new identity is an internal conclusion from the same six caller conditions.

\[\text{same }\mu,J,\nu,S,e,U,T,\Gamma,\Gamma_0,\mathrm{Inv},A_0,B_0,V_0,R;\quad\forall h\in\ker P.\]
Corresponding Lean step
  have hFinal :
      (∀ h : Hperp, (D h : Lp ℝ 2 J)=U (h : Lp ℝ 2 J)-P (U (h : Lp ℝ 2 J))) ∧
      V0.adjoint ∘L D= -(A0 ∘L V0.adjoint) ∧
      (∀ 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‖) := ⟨hD,hIntertwine,hGlobal⟩
  unfold actual_reflection_intertwining_statement
  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 hFinal

Literal compiled BODY span; exact preceding module 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_reflection_intertwining

Fix the original probability geometry and the same witnesses; Use the actual compression and identify the reflection; Match the actual inclusions; Transport the block adjoint identity on every micro input; Pass from B0 to the same polar adjoint; Preserve the complete original conclusion

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_reflection_intertwining
    {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_reflection_intertwining_statement (E := E) (V := V) (α := α) (β := β) (η := η) hα hαβ hV hH hη hβη := by
  classical
  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.ActualRootCommutation.actual_same_root_inverse_commutation
    (E:=E) (V:=V) (α:=α) (β:=β) (η:=η) hα hαβ hV hH hη hβη
  have parentSlice0 := hBase
  have hμ := parentSlice0.1
  have parentSlice1 := parentSlice0.2
  have hJ := parentSlice1.1
  have parentSlice2 := parentSlice1.2
  have hν := parentSlice2.1
  have parentSlice3 := parentSlice2.2
  have hRange := parentSlice3.1
  have parentSlice4 := parentSlice3.2
  have hPf := parentSlice4.1
  have parentSlice5 := parentSlice4.2
  obtain ⟨S, parentSlice6⟩ := parentSlice5
  have hS := parentSlice6.1
  have parentSlice7 := parentSlice6.2
  have hSd := parentSlice7.1
  have parentSlice8 := parentSlice7.2
  have hSc := parentSlice8.1
  have parentSlice9 := parentSlice8.2
  have hSf := parentSlice9.1
  have parentSlice10 := parentSlice9.2
  have hSs := parentSlice10.1
  have parentSlice11 := parentSlice10.2
  obtain ⟨e, parentSlice12⟩ := parentSlice11
  have he := parentSlice12.1
  have parentSlice13 := parentSlice12.2
  obtain ⟨U, parentSlice14⟩ := parentSlice13
  have hU := parentSlice14.1
  have parentSlice15 := parentSlice14.2
  have hUi := parentSlice15.1
  have parentSlice16 := parentSlice15.2
  have hUs := parentSlice16.1
  have parentSlice17 := parentSlice16.2
  obtain ⟨T, parentSlice18⟩ := parentSlice17
  have hTs := parentSlice18.1
  have parentSlice19 := parentSlice18.2
  have hAll := parentSlice19.1
  have parentSlice20 := parentSlice19.2
  have hAeq := parentSlice20.1
  have parentSlice21 := parentSlice20.2
  have hAs := parentSlice21.1
  have parentSlice22 := parentSlice21.2
  have hAn := parentSlice22.1
  have parentSlice23 := parentSlice22.2
  have hPB := parentSlice23.1
  have parentSlice24 := parentSlice23.2
  obtain ⟨Γ, parentSlice25⟩ := parentSlice24
  have hΓ := parentSlice25.1
  have parentSlice26 := parentSlice25.2
  have hΓSq := parentSlice26.1
  have parentSlice27 := parentSlice26.2
  have hCommRoot := parentSlice27.1
  have parentSlice28 := parentSlice27.2
  have hΓP := parentSlice28.1
  have parentSlice29 := parentSlice28.2
  have hΓPSq := parentSlice29.1
  have parentSlice30 := parentSlice29.2
  have hCommP := parentSlice30.1
  have parentSlice31 := parentSlice30.2
  have hGram := parentSlice31.1
  have parentSlice32 := parentSlice31.2
  obtain ⟨q, parentSlice33⟩ := parentSlice32
  have hqa := parentSlice33.1
  have parentSlice34 := parentSlice33.2
  have hTq := parentSlice34.1
  have parentSlice35 := parentSlice34.2
  have hq := parentSlice35.1
  have parentSlice36 := parentSlice35.2
  have hCenter := parentSlice36.1
  have parentSlice37 := parentSlice36.2
  have hΓPq := parentSlice37.1
  have parentSlice38 := parentSlice37.2
  have hγ := parentSlice38.1
  have parentSlice39 := parentSlice38.2
  obtain ⟨ΓP0, parentSlice40⟩ := parentSlice39
  have hΓP0 := parentSlice40.1
  have parentSlice41 := parentSlice40.2
  have hPos0 := parentSlice41.1
  have parentSlice42 := parentSlice41.2
  have hOrder0 := parentSlice42.1
  have parentSlice43 := parentSlice42.2
  have hUnit := parentSlice43.1
  have parentSlice44 := parentSlice43.2
  obtain ⟨Inv, parentSlice45⟩ := parentSlice44
  have hLeft := parentSlice45.1
  have parentSlice46 := parentSlice45.2
  have hRight := parentSlice46.1
  have parentSlice47 := parentSlice46.2
  have hNormInv := parentSlice47.1
  have parentSlice48 := parentSlice47.2
  have hInvSelf := parentSlice48.1
  have parentSlice49 := parentSlice48.2
  obtain ⟨A0, parentSlice50⟩ := parentSlice49
  have hA0 := parentSlice50.1
  have parentSlice51 := parentSlice50.2
  have hA0self := parentSlice51.1
  have parentSlice52 := parentSlice51.2
  have hComm0 := parentSlice52.1
  have parentSlice53 := parentSlice52.2
  have hSquare0 := parentSlice53.1
  have parentSlice54 := parentSlice53.2
  have hCommInv := parentSlice54.1
  have parentSlice55 := parentSlice54.2
  obtain ⟨B0, parentSlice56⟩ := parentSlice55
  have hB0 := parentSlice56.1
  have parentSlice57 := parentSlice56.2
  obtain ⟨V0, parentSlice58⟩ := parentSlice57
  have hVdef := parentSlice58.1
  have parentSlice59 := parentSlice58.2
  have hFactor := parentSlice59.1
  have parentSlice60 := parentSlice59.2
  have hVadj := parentSlice60.1
  have parentSlice61 := parentSlice60.2
  have hVnorm := parentSlice61.1
  have parentSlice62 := parentSlice61.2
  obtain ⟨R, parentSlice63⟩ := parentSlice62
  have hR := parentSlice63.1
  have parentSlice64 := parentSlice63.2
  have hAmbient := parentSlice64.1
  have parentSlice65 := parentSlice64.2
  have hGlobal := parentSlice65
  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 A0
  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
  let D : Hperp →L[ℝ] Hperp := R ∘L U.toContinuousLinearMap ∘L Hperp.subtypeL
  have hD (h : Hperp) : (D h : Lp ℝ 2 J)=
      U (h : Lp ℝ 2 J)-P (U (h : Lp ℝ 2 J)) := hR (U (h : Lp ℝ 2 J))
  letI : IsProbabilityMeasure μ := hμ
  obtain ⟨ρ,hρ,hρf,U2,hU2,hU2i,hU2s,hρp,hBB,hBD,hBE⟩ :=
    AutoSamplingTheory.ExampleCases.ProximalBPS.ReflectionL2.actual_reflection_block_identities μ hη
  have hU2eq : U2=U := by
    apply LinearIsometry.ext
    intro f
    apply Lp.ext
    exact (hU2 f).trans (hU f).symm
  subst U2
  let AJ : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J := P*U.toContinuousLinearMap*P
  let BA : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J := (1-P)*U.toContinuousLinearMap*P
  let DA : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J := (1-P)*U.toContinuousLinearMap*(1-P)
  have hBDtyped : BA.adjoint ∘L DA= -(AJ ∘L BA.adjoint) := hBD
  have hPself : IsSelfAdjoint P := isSelfAdjoint_starProjection HP
  have hAJself : IsSelfAdjoint AJ := by
    change star (P*U.toContinuousLinearMap*P)=P*U.toContinuousLinearMap*P
    simp only [star_mul,hPself.star_eq,hUs.star_eq,mul_assoc]
  let ι : HP0 →L[ℝ] Lp ℝ 2 J := HP.subtypeL ∘L HP0.subtypeL
  have hBambient (u : HP0) : BA (ι u)=(B0 u : Lp ℝ 2 J) := (hB0 u).symm
  have hAambient (u : HP0) : AJ (ι u)=ι (A0 u) := by
    change P (U (P ((u : HP) : Lp ℝ 2 J)))=((A0 u : HP) : Lp ℝ 2 J)
    rw [hPf]
    change (A (u : HP) : Lp ℝ 2 J)=((A0 u : HP) : Lp ℝ 2 J)
    exact congrArg (fun x : HP => (x : Lp ℝ 2 J)) (hA0 u).symm
  have hDambient (h : Hperp) : DA (h : Lp ℝ 2 J)=(D h : Lp ℝ 2 J) := by
    change U ((h : Lp ℝ 2 J)-P (h : Lp ℝ 2 J))-
      P (U ((h : Lp ℝ 2 J)-P (h : Lp ℝ 2 J)))=(D h : Lp ℝ 2 J)
    rw [show P (h : Lp ℝ 2 J)=0 from h.property,sub_zero]
    exact (hD h).symm
  have hB0intertwine : B0.adjoint ∘L D= -(A0 ∘L B0.adjoint) := by
    apply ContinuousLinearMap.ext
    intro h
    apply ext_inner_left ℝ
    intro u
    change inner ℝ u (B0.adjoint (D h))=inner ℝ u (-(A0 (B0.adjoint h)))
    calc
      inner ℝ u (B0.adjoint (D h))=inner ℝ (B0 u) (D h) := B0.adjoint_inner_right u (D h)
      _ = inner ℝ (BA (ι u)) (DA (h : Lp ℝ 2 J)) := by rw [hBambient,hDambient]; rfl
      _ = inner ℝ (ι u) (BA.adjoint (DA (h : Lp ℝ 2 J))) := (BA.adjoint_inner_right _ _).symm
      _ = inner ℝ (ι u) (-(AJ (BA.adjoint (h : Lp ℝ 2 J)))) := by
        have hb := DFunLike.congr_fun hBDtyped (h : Lp ℝ 2 J)
        change BA.adjoint (DA (h : Lp ℝ 2 J))= -(AJ (BA.adjoint (h : Lp ℝ 2 J))) at hb
        rw [hb]
      _ = -inner ℝ (AJ (ι u)) (BA.adjoint (h : Lp ℝ 2 J)) := by
        simpa only [inner_neg_right,hAJself.adjoint_eq] using
          congrArg Neg.neg (AJ.adjoint_inner_right (ι u) (BA.adjoint (h : Lp ℝ 2 J)))
      _ = -inner ℝ (BA (AJ (ι u))) (h : Lp ℝ 2 J) := by rw [BA.adjoint_inner_right]
      _ = -inner ℝ (B0 (A0 u)) h := by rw [hAambient,hBambient]; rfl
      _ = -inner ℝ (A0 u) (B0.adjoint h) := by rw [B0.adjoint_inner_right]
      _ = inner ℝ u (-(A0 (B0.adjoint h))) := by
        simpa only [inner_neg_right,hA0self.adjoint_eq] using
          (congrArg Neg.neg (A0.adjoint_inner_right u (B0.adjoint h))).symm
  have hVdefTyped : V0=B0 ∘L Inv := hVdef
  have hInvSelfTyped : IsSelfAdjoint Inv := hInvSelf
  have hVadjEq : V0.adjoint=Inv ∘L B0.adjoint := by
    calc
      V0.adjoint=(B0 ∘L Inv).adjoint :=
        congrArg (fun L : HP0 →L[ℝ] Hperp => L.adjoint) hVdefTyped
      _ = Inv.adjoint ∘L B0.adjoint := ContinuousLinearMap.adjoint_comp B0 Inv
      _ = Inv ∘L B0.adjoint := by rw [hInvSelfTyped.adjoint_eq]
  have hIntertwine : V0.adjoint ∘L D= -(A0 ∘L V0.adjoint) := by
    calc
      V0.adjoint ∘L D=Inv ∘L (B0.adjoint ∘L D) := by rw [hVadjEq,ContinuousLinearMap.comp_assoc]
      _ = Inv ∘L (-(A0 ∘L B0.adjoint)) := by rw [hB0intertwine]
      _ = -(A0 ∘L V0.adjoint) := by
        apply ContinuousLinearMap.ext
        intro h
        change Inv (-(A0 (B0.adjoint h)))= -(A0 (V0.adjoint h))
        rw [map_neg,hVadjEq]
        change -(Inv (A0 (B0.adjoint h)))= -(A0 (Inv (B0.adjoint h)))
        exact congrArg Neg.neg (DFunLike.congr_fun hCommInv.eq (B0.adjoint h)).symm
  have hFinal :
      (∀ h : Hperp, (D h : Lp ℝ 2 J)=U (h : Lp ℝ 2 J)-P (U (h : Lp ℝ 2 J))) ∧
      V0.adjoint ∘L D= -(A0 ∘L V0.adjoint) ∧
      (∀ 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‖) := ⟨hD,hIntertwine,hGlobal⟩
  unfold actual_reflection_intertwining_statement
  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 hFinal

end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ReflectionIntertwining

#print axioms AutoSamplingTheory.ExampleCases.ProximalBPS.ReflectionIntertwining.actual_reflection_intertwining

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 original input seal independently admitted before proof search.
B21 actual rotation/corrector change, B4 dynamics and whole-paper conclusions.Intertwining only; actual centered g=U(P-Pperp)f rotation, B21 corrector change and B4 dynamics are subsequent independent obligations. No sharp-energy68 parent is invented. No main/errors/cost/composition/Exposition/PURIFIED/Goal claim.unresolvedThe full-micro intertwining is one substantive prerequisite; no subsequent conclusion is inferred.

Intertwining only; actual centered g=U(P-Pperp)f rotation, B21 corrector change and B4 dynamics are subsequent independent obligations. No sharp-energy68 parent is invented. No main/errors/cost/composition/Exposition/PURIFIED/Goal claim.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

  • domains: Explicit elaboration: finite-dimensional real Hilbert Borel E presents source Euclidean R^d; rank-zero/trivial centered spaces are retained as the disclosed extension, with no positive-rank premise. — Source P0 and endpoint freeze; Lean18-20/77-100; native domains/scopes. Finite-dimensionality is on E only, not L2.
  • domains: Explicit elaboration: real L2 denotes AE classes; HP0 is a closed centered macro kernel while Hperp is the full conditional kernel of P. — Source P3/P6/P10; Lean36-40,77-100; native domains/scopes. This is not replacing Hperp by all globally centered H.
  • objects: Explicit elaboration: intrinsic source blocks are represented by ambient bounded maps plus distinct inclusions and exact restriction equalities. — Source P3/P4/P9; Lean59-65,101-110,316-350. The ambient B* all-g adapter is retained; no extra public binder.
  • quantifiers: Equivalent elaboration: the source operator equality is expanded as a bounded-map equality on every h:kerP; it is not rangeV-only or dependent on a chosen globalf. — Source P11 A2.SS3.p5.m19; Lean111-116; native quantifiers and scopes; BODY h.property at326 uses only Ph=0.
  • objects: Explicit elaboration: root positivity/square, centered gap, two-sided bounded inverse, same-polar factor and all commutations are named output witnesses or internal conclusions. — Source P5-P9; Lean66-110 and BODY134-295; public125-133 has only original six analytic assumptions.
  • scopes: Equivalent representative adapter: the independently produced reflection in the block theorem is identified with SAME U by L2 AE extensionality before transporting the block identity. — Source P2/P4; BODY301-307 proves U2=U and substitutes U2. No arbitrary involution substitution or pointwise-for-all-observables exceptional-set claim.
  • scopes: Equivalent internal algebra route: first prove B0*D=-A0B0* by inner transport, then use V0*=Inv B0* and SAME inverse commutation; source instead cancels the centered positive root. — Source P4/P7-P11, A2.E5.m1,A2.Ex14.m1,A2.SS3.p5.m19; BODY328-369; both routes use same actual blocks,root,inverse and all kerP. This changes no source hypothesis.
  • quantifiers: Same dependent-output contract: all12 original witnesses precede every globally centered f; only fP is chosen after that quantifier, and the entire original globalf conclusion persists. — Exact parent HEADER-ONLY fragment comparison in literal-statement-and-whole-module-audit.json; Lean44-123 and reassembly370-441; native quantifiers/conclusion.
  • assumptions: No strengthening: six original analytic conditions are unchanged; internally necessary proof ingredients are not public caller binders. — Primary P0; public125-133; full BODY134-441; native assumptions. No source repair proposed.
  • constant_dependencies: Same signs and endpoints: V0*D=-A0V0*, gamma=2sqrt(alphaeta)/(1+alphaeta), normInv<=1/gamma, betaeta<=1; rank0 and alphaeta1 remain legal. — Source P0/P6/P11 and frozen endpoints; literal81,90,115; BODY351-369; native constants/scopes.
  • conclusion: Bounded source ingredient, with explicit retained context:69 proves P11 and preserves its actual-input witness contract; it does not claim actual B21 rotation/corrector change, B4 dynamics or the main result. — Source graph P11,P14,P17,P19-P21; publication supports only reflection-intertwining; unclaimed remaining-paper obligation remains open. This is a disclosed theorem-DAG slice, not weakening a whole-B21 claim.
  • scopes: Reader/API metadata only: the independently approved two fields expose the complete literal Prop in the existing adjacent proof fold and correct the root Mathlib name; neither supplies a mathematical provider. — reader-api-metadata-overlay.proposal.json SHA85cfec574019132c82244c1536a6ffb1b018e7932aefd825d3e05530be5f815d; applied lesson SHA6242d60d05c88045f0beffda0a62eff912d0794d2c0ca98bde3f8574e7e2d43a; all other lesson fields and6BODY unchanged.

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
  • Intertwining only; actual centered g=U(P-Pperp)f rotation, B21 corrector change and B4 dynamics are subsequent independent obligations. No sharp-energy68 parent is invented. No main/errors/cost/composition/Exposition/PURIFIED/Goal claim.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • Lp.ext
  • LinearIsometry.ext
  • ContinuousLinearMap.adjoint_inner_right
  • ContinuousLinearMap.adjoint_comp
  • IsSelfAdjoint.adjoint_eq
  • Commute.eq
  • isSelfAdjoint_starProjection

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 reflection intertwining on the full conditional-complement space
  • TODO — not closed by these contributions Actual B21 rotation/corrector change,B4 dynamics,H1,main,errors,costs/composition