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

ActualCorrectorChange: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. Actual PBPS corrector change under the reflected step
Samplinglib mathematical lesson

Actual PBPS corrector change under the reflected step

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualCorrectorChange.actual_corrector_change · 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. For the same U,R and inclusion of H_perp=ker P, define D=R U inclusion. Its full-domain identity V0*D=-A0 V0* is retained. For EVERY globally mean-zero f in L2(J), let fP be its actual centered conditional-expectation component, fperp=R f and fV=V0* fperp. Define the actual output g=U(P f-(f-P f)), not an abstract pair chosen to satisfy a matrix identity. The theorem proves its global mean is zero internally from invariance of the actual reflected augmentation law and preservation of the integral by conditional expectation. Let gP be the actual centered conditional-expectation component of this SAME g, gperp=R g and gV=V0* gperp. Then gP=A0 fP-Gamma0 fV, gV=Gamma0 fP+A0 fV, and ||gP||^2+||gV||^2=||fP||^2+||fV||^2. Both output components are produced by these actual conditional/polar semantics before proving the formulas; neither is defined as its right-hand side. All previous law/kernel/root/inverse/polar/full-micro and centered-observable conclusions persist with the SAME twelve witnesses and the original six analytic caller conditions. No surjectivity, sharp-energy68 bound, extra regularity or zero-output-mean premise is introduced. One private literal Prop stores the complete sealed mathematical conclusion; it supplies no proof provider or additional hypothesis. For the SAME centered A_0 and inverse Inv, define K=A_0 Inv and C(u,v)=(||u||²−||v||²)/2−⟨K u,v⟩ for u,v in H_P^0. For every globally centered actual f and the SAME actual g=U(Pf−(f−Pf)), the already produced conditional/polar components satisfy C(g_P,g_V)−C(f_P,f_V)=−||f_P||²+||f_V||². The half, signs, coefficient one and the same inverse are exact. This identity is proved internally from A_0²+Γ_0²=I, selfadjointness, commutation, the two-sided inverse and the actual projected rotation. No corrector-change certificate, sharp corrector bound, extra domain/smoothness, onto-V_0 or strict endpoint is an additional premise. Every previous clause and all twelve common witnesses persist. This closes the discrete corrector-change ingredient of (B.21) used by the first two signed terms in (B.28); it does not establish the remaining B4 dynamics or any full sampling theorem. B4/H1/B2, invariance/nonexplosion, main convergence, implementation errors/caps, expected-query costs and actual-input composition remain separate obligations.

\[C(u,v)=\frac{\|u\|^2-\|v\|^2}{2}-\langle A_0\operatorname{Inv}u,v\rangle,\qquad C(g_P,g_V)-C(f_P,f_V)=-\|f_P\|^2+\|f_V\|^2.\]
Lean statement · actual_corrector_change

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. For the same U,R and inclusion of H_perp=ker P, define D=R U inclusion. Its full-domain identity V0*D=-A0 V0* is retained. For EVERY globally mean-zero f in L2(J), let fP be its actual centered conditional-expectation component, fperp=R f and fV=V0* fperp. Define the actual output g=U(P f-(f-P f)), not an abstract pair chosen to satisfy a matrix identity. The theorem proves its global mean is zero internally from invariance of the actual reflected augmentation law and preservation of the integral by conditional expectation. Let gP be the actual centered conditional-expectation component of this SAME g, gperp=R g and gV=V0* gperp. Then gP=A0 fP-Gamma0 fV, gV=Gamma0 fP+A0 fV, and ||gP||^2+||gV||^2=||fP||^2+||fV||^2. Both output components are produced by these actual conditional/polar semantics before proving the formulas; neither is defined as its right-hand side. All previous law/kernel/root/inverse/polar/full-micro and centered-observable conclusions persist with the SAME twelve witnesses and the original six analytic caller conditions. No surjectivity, sharp-energy68 bound, extra regularity or zero-output-mean premise is introduced. One private literal Prop stores the complete sealed mathematical conclusion; it supplies no proof provider or additional hypothesis. For the SAME centered A_0 and inverse Inv, define K=A_0 Inv and C(u,v)=(||u||²−||v||²)/2−⟨K u,v⟩ for u,v in H_P^0. For every globally centered actual f and the SAME actual g=U(Pf−(f−Pf)), the already produced conditional/polar components satisfy C(g_P,g_V)−C(f_P,f_V)=−||f_P||²+||f_V||². The half, signs, coefficient one and the same inverse are exact. This identity is proved internally from A_0²+Γ_0²=I, selfadjointness, commutation, the two-sided inverse and the actual projected rotation. No corrector-change certificate, sharp corrector bound, extra domain/smoothness, onto-V_0 or strict endpoint is an additional premise. Every previous clause and all twelve common witnesses persist. This closes the discrete corrector-change ingredient of (B.21) used by the first two signed terms in (B.28); it does not establish the remaining B4 dynamics or any full sampling theorem. B4/H1/B2, invariance/nonexplosion, main convergence, implementation errors/caps, expected-query costs and actual-input composition remain separate obligations.

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

Exact module and namespace context

Full Lean proposition (definition) · actual_corrector_change_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_corrector_change_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‖ ∧
                              let g : Lp ℝ 2 J := U (P f-(f-P f))
                              (∫ z, g z ∂J)=0 ∧
                              ∃ gP : HP0,
                                HP0.subtypeL gP=condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le g ∧
                                let gperp : Hperp := R g
                                let gV : HP0 := V0.adjoint gperp
                                gP=A0 fP-ΓP0 fV ∧
                                gV=ΓP0 fP+A0 fV ∧
                                ‖gP‖^2+‖gV‖^2=‖fP‖^2+‖fV‖^2 ∧
                                let C : HP0 → HP0 → ℝ := fun u v =>
                                  (‖u‖^2-‖v‖^2)/2-inner ℝ (A0 (Inv u)) v
                                C gP gV-C fP fV= -‖fP‖^2+‖fV‖^2)

Exact module and namespace context

Proof roadmap

  1. 1Retain the same actual laws, operators and original inputs

    Apply the independently accepted actual projected-rotation parent with the six original analytic caller conditions. Extract its same twelve witnesses, actual conditional components and mean preservation. Identify the inherited complete centered and conditional-mean-zero Hilbert spaces explicitly; the typed change only exposes the parent proposition and introduces no assumption.

  2. 2Test the square identity and cancel mixed terms

    Positivity gives selfadjoint Γ_0. Test A_0²+Γ_0²=I against u, moving each selfadjoint operator through the inner product, to obtain the norm identity. Move A_0 and Γ_0 through the mixed product and use their commutation to obtain the cross-term identity. These identities hold on the full centered Hilbert space, including the zero space.

  3. 3Derive the corrector operator identities from the same inverse

    Set K=A_0 Inv. Evaluate both sides of Inv Γ_0=Γ_0 Inv=I and of the two commutation identities. Consequently KΓ_0=Γ_0K=A_0 and KA_0=A_0K. The inverse remains on H_P^0; it is never extended to constants or assumed to be a new caller certificate.

  4. 4Reduce the remaining mixed inner product

    Apply A_0²+Γ_0²=I to u. Commutation and KΓ_0=A_0 give A_0 K A_0 u+Γ_0 A_0u=K(A_0²u+Γ_0²u)=Ku. Test against v and use selfadjoint A_0 and Γ_0. This is precisely the mixed term needed for the corrector expansion.

  5. 5Evaluate both diagonal terms and align the mixed terms

    Move Γ_0 across the first diagonal inner product, use Γ_0K=A_0, and move A_0 across once more. For the other diagonal use KΓ_0=A_0 directly. Real symmetry and the preceding cross-term identity align the two mixed products without any surjectivity or dimension argument.

  6. 6Expand the corrector and compute its exact change

    Write X=||A_0u||²,Y=||Γ_0u||²,Z=||A_0v||²,W=||Γ_0v||²,t=⟨A_0u,Γ_0v⟩ and r=⟨Ku,v⟩. For u′=A_0u−Γ_0v and v′=Γ_0u+A_0v, norm expansion gives ||u′||²=X+W−2t and ||v′||²=Y+Z+2t. The diagonal and mixed identities give ⟨Ku′,v′⟩=X−Z+r−2t. Hence C(u′,v′)=(−X−Y+Z+W)/2−r=−||u||²/2+||v||²/2−r. Subtract C(u,v)=(||u||²−||v||²)/2−r. All cross terms cancel and the exact half and signs remain.

  7. 7Substitute the actual conditional and polar components

    For arbitrary actual f with integral zero, use the parent to produce its actual f_P and the actual conditional g_P of the same g. Keep f_V=V_0*Rf and g_V=V_0*Rg. Apply the two-argument congruence of C to the already proved component formulas, then subtract C(f_P,f_V) and apply the preceding algebra with u=f_P,v=f_V. Thus the corrector is evaluated on actual components, rather than components defined by the rotation right-hand sides.

  8. 8Reassemble every original clause with the same witnesses

    Retain the full-micro intertwining identity, actual projected rotation, pair energy and all earlier law/kernel/root/inverse/polar conclusions, and adjoin only the new corrector identity. This supplies the discrete corrector-change ingredient for the first two signed terms of B4/B28. Time evolution, the weak H1 bridge, nonexplosion, implementation error and expected-cost composition are not inferred from this algebra.

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.
  • The global output mean, actual projected component formulas and pair-energy identity are internally proved conclusions. There is no additional zero-output-mean, onto-V0, sharp-energy or higher-smoothness hypothesis.
  • C is the exact concluded functional on the same H_P^0, with the exact half and A_0 Inv cross term. Its actual B21 change is proved; no new corrector-bound, onto, mean-preservation, strict-endpoint or smoothness caller is added.

Mathematical proof

1. Retain the same actual laws, operators and original inputs

Apply the independently accepted actual projected-rotation parent with the six original analytic caller conditions. Extract its same twelve witnesses, actual conditional components and mean preservation. Identify the inherited complete centered and conditional-mean-zero Hilbert spaces explicitly; the typed change only exposes the parent proposition and introduces no assumption.

\[g=U(Pf-(f-Pf)),\quad g_P=A_0f_P-\Gamma_0f_V,\quad g_V=\Gamma_0f_P+A_0f_V.\]
Corresponding Lean step
  unfold actual_corrector_change_statement
  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.ActualProjectedRotation.actual_projected_rotation
    (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 hDparent := parentSlice65.1
  have parentSlice66 := parentSlice65.2
  have hIntertwineParent := parentSlice66.1
  have hGlobal := parentSlice66.2
  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‖ ∧
                              let g : Lp ℝ 2 J := U (P f-(f-P f))
                              (∫ z, g z ∂J)=0 ∧
                              ∃ gP : HP0,
                                HP0.subtypeL gP=condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le g ∧
                                let gperp : Hperp := R g
                                let gV : HP0 := V0.adjoint gperp
                                gP=A0 fP-ΓP0 fV ∧
                                gV=ΓP0 fP+A0 fV ∧
                                ‖gP‖^2+‖gV‖^2=‖fP‖^2+‖fV‖^2) 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)) := hDparent h
  have hIntertwine : V0.adjoint ∘L D= -(A0 ∘L V0.adjoint) := hIntertwineParent

Exact compiled BODY span, with preceding local definitions and inherited Hilbert structures in scope.

2. Test the square identity and cancel mixed terms

Positivity gives selfadjoint Γ_0. Test A_0²+Γ_0²=I against u, moving each selfadjoint operator through the inner product, to obtain the norm identity. Move A_0 and Γ_0 through the mixed product and use their commutation to obtain the cross-term identity. These identities hold on the full centered Hilbert space, including the zero space.

\[\|A_0u\|^2+\|\Gamma_0u\|^2=\|u\|^2,\qquad\langle A_0u,\Gamma_0v\rangle=\langle\Gamma_0u,A_0v\rangle.\]
Corresponding Lean step
  have hΓself : IsSelfAdjoint ΓP0 := (show ΓP0.IsPositive from hPos0).isSelfAdjoint
  have hEnergy (u : HP0) : ‖A0 u‖^2+‖ΓP0 u‖^2=‖u‖^2 := by
    have h := congrArg (fun L : HP0 →L[ℝ] HP0 => inner ℝ (L u) u) hSquare0
    simp only [ContinuousLinearMap.add_apply,ContinuousLinearMap.mul_apply,
      ContinuousLinearMap.one_apply,inner_add_left] at h
    have ha : inner ℝ (A0 (A0 u)) u=‖A0 u‖^2 :=
      (hA0self.isSymmetric (A0 u) u).trans (real_inner_self_eq_norm_sq _)
    have hg : inner ℝ (ΓP0 (ΓP0 u)) u=‖ΓP0 u‖^2 :=
      (hΓself.isSymmetric (ΓP0 u) u).trans (real_inner_self_eq_norm_sq _)
    rw [ha,hg,real_inner_self_eq_norm_sq] at h
    exact h
  have hCross (u v : HP0) : inner ℝ (A0 u) (ΓP0 v)=inner ℝ (ΓP0 u) (A0 v) := by
    calc
      inner ℝ (A0 u) (ΓP0 v)=inner ℝ u (A0 (ΓP0 v)) := hA0self.isSymmetric _ _
      _ = inner ℝ u (ΓP0 (A0 v)) := congrArg (fun z : HP0 => inner ℝ u z) (DFunLike.congr_fun hComm0.eq v)
      _ = inner ℝ (ΓP0 u) (A0 v) := (hΓself.isSymmetric _ _).symm

Exact compiled BODY span, with preceding local definitions and inherited Hilbert structures in scope.

3. Derive the corrector operator identities from the same inverse

Set K=A_0 Inv. Evaluate both sides of Inv Γ_0=Γ_0 Inv=I and of the two commutation identities. Consequently KΓ_0=Γ_0K=A_0 and KA_0=A_0K. The inverse remains on H_P^0; it is never extended to constants or assumed to be a new caller certificate.

\[K=A_0\operatorname{Inv},\quad K\Gamma_0=\Gamma_0K=A_0,\quad KA_0=A_0K.\]
Corresponding Lean step
  let K : HP0 →L[ℝ] HP0 := A0 ∘L Inv
  have hInvΓ (u : HP0) : Inv (ΓP0 u)=u := by
    have h := DFunLike.congr_fun hLeft u
    simpa only [ContinuousLinearMap.mul_apply,ContinuousLinearMap.one_apply] using h
  have hΓInv (u : HP0) : ΓP0 (Inv u)=u := by
    have h := DFunLike.congr_fun hRight u
    simpa only [ContinuousLinearMap.mul_apply,ContinuousLinearMap.one_apply] using h
  have hCommEval (u : HP0) : A0 (ΓP0 u)=ΓP0 (A0 u) :=
    DFunLike.congr_fun hComm0.eq u
  have hCommInvEval (u : HP0) : A0 (Inv u)=Inv (A0 u) :=
    DFunLike.congr_fun hCommInv.eq u
  have hKΓ (u : HP0) : K (ΓP0 u)=A0 u := congrArg A0 (hInvΓ u)
  have hΓK (u : HP0) : ΓP0 (K u)=A0 u := by
    change ΓP0 (A0 (Inv u))=A0 u
    calc
      ΓP0 (A0 (Inv u))=A0 (ΓP0 (Inv u)) := (hCommEval (Inv u)).symm
      _ = A0 u := congrArg A0 (hΓInv u)
  have hKA (u : HP0) : K (A0 u)=A0 (K u) := by
    change A0 (Inv (A0 u))=A0 (A0 (Inv u))
    exact congrArg A0 (hCommInvEval u).symm

Exact compiled BODY span, with preceding local definitions and inherited Hilbert structures in scope.

4. Reduce the remaining mixed inner product

Apply A_0²+Γ_0²=I to u. Commutation and KΓ_0=A_0 give A_0 K A_0 u+Γ_0 A_0u=K(A_0²u+Γ_0²u)=Ku. Test against v and use selfadjoint A_0 and Γ_0. This is precisely the mixed term needed for the corrector expansion.

\[A_0KA_0u+\Gamma_0A_0u=Ku,\qquad\langle KA_0u,A_0v\rangle+\langle A_0u,\Gamma_0v\rangle=\langle Ku,v\rangle.\]
Corresponding Lean step
  have hSquareApply (u : HP0) : A0 (A0 u)+ΓP0 (ΓP0 u)=u := by
    have h := DFunLike.congr_fun hSquare0 u
    simpa only [ContinuousLinearMap.add_apply,ContinuousLinearMap.mul_apply,
      ContinuousLinearMap.one_apply] using h
  have hKMixedVector (u : HP0) : A0 (K (A0 u))+ΓP0 (A0 u)=K u := by
    calc
      A0 (K (A0 u))+ΓP0 (A0 u)=K (A0 (A0 u))+K (ΓP0 (ΓP0 u)) :=
        congrArg₂ (fun x y : HP0 => x+y) (hKA (A0 u)).symm
          ((hCommEval u).symm.trans (hKΓ (ΓP0 u)).symm)
      _ = K (A0 (A0 u)+ΓP0 (ΓP0 u)) := (K.map_add _ _).symm
      _ = K u := congrArg K (hSquareApply u)
  have hMixed (u v : HP0) :
      inner ℝ (K (A0 u)) (A0 v)+inner ℝ (A0 u) (ΓP0 v)=inner ℝ (K u) v := by
    calc
      inner ℝ (K (A0 u)) (A0 v)+inner ℝ (A0 u) (ΓP0 v)=
          inner ℝ (A0 (K (A0 u))) v+inner ℝ (ΓP0 (A0 u)) v :=
        congrArg₂ (fun x y : ℝ => x+y)
          (hA0self.isSymmetric (K (A0 u)) v).symm
          (hΓself.isSymmetric (A0 u) v).symm
      _ = inner ℝ (A0 (K (A0 u))+ΓP0 (A0 u)) v := (inner_add_left _ _ _).symm
      _ = inner ℝ (K u) v := by rw [hKMixedVector]

Exact compiled BODY span, with preceding local definitions and inherited Hilbert structures in scope.

5. Evaluate both diagonal terms and align the mixed terms

Move Γ_0 across the first diagonal inner product, use Γ_0K=A_0, and move A_0 across once more. For the other diagonal use KΓ_0=A_0 directly. Real symmetry and the preceding cross-term identity align the two mixed products without any surjectivity or dimension argument.

\[\langle KA_0u,\Gamma_0u\rangle=\|A_0u\|^2,\quad\langle K\Gamma_0v,A_0v\rangle=\|A_0v\|^2,\quad\langle A_0v,\Gamma_0u\rangle=\langle A_0u,\Gamma_0v\rangle.\]
Corresponding Lean step
  have hDiagL (u : HP0) : inner ℝ (K (A0 u)) (ΓP0 u)=‖A0 u‖^2 := by
    calc
      inner ℝ (K (A0 u)) (ΓP0 u)=inner ℝ (ΓP0 (K (A0 u))) u :=
        (hΓself.isSymmetric _ _).symm
      _ = inner ℝ (A0 (A0 u)) u := by rw [hΓK]
      _ = inner ℝ (A0 u) (A0 u) := hA0self.isSymmetric _ _
      _ = ‖A0 u‖^2 := real_inner_self_eq_norm_sq _
  have hDiagR (v : HP0) : inner ℝ (K (ΓP0 v)) (A0 v)=‖A0 v‖^2 := by
    rw [hKΓ,real_inner_self_eq_norm_sq]
  have hSwap (u v : HP0) : inner ℝ (ΓP0 u) (A0 v)=inner ℝ (A0 u) (ΓP0 v) :=
    (hCross u v).symm
  have hSwap2 (u v : HP0) : inner ℝ (A0 v) (ΓP0 u)=inner ℝ (A0 u) (ΓP0 v) :=
    (real_inner_comm _ _).trans (hSwap u v)

Exact compiled BODY span, with preceding local definitions and inherited Hilbert structures in scope.

6. Expand the corrector and compute its exact change

Write X=||A_0u||²,Y=||Γ_0u||²,Z=||A_0v||²,W=||Γ_0v||²,t=⟨A_0u,Γ_0v⟩ and r=⟨Ku,v⟩. For u′=A_0u−Γ_0v and v′=Γ_0u+A_0v, norm expansion gives ||u′||²=X+W−2t and ||v′||²=Y+Z+2t. The diagonal and mixed identities give ⟨Ku′,v′⟩=X−Z+r−2t. Hence C(u′,v′)=(−X−Y+Z+W)/2−r=−||u||²/2+||v||²/2−r. Subtract C(u,v)=(||u||²−||v||²)/2−r. All cross terms cancel and the exact half and signs remain.

\[C(A_0u-\Gamma_0v,\Gamma_0u+A_0v)-C(u,v)=-\|u\|^2+\|v\|^2.\]
Corresponding Lean step
  have hCorrector (u v : HP0) :
      ((‖A0 u-ΓP0 v‖^2-‖ΓP0 u+A0 v‖^2)/2-
        inner ℝ (K (A0 u-ΓP0 v)) (ΓP0 u+A0 v))-
      ((‖u‖^2-‖v‖^2)/2-inner ℝ (K u) v)= -‖u‖^2+‖v‖^2 := by
    rw [norm_sub_sq_real,norm_add_sq_real,map_sub,inner_sub_left,
      inner_add_right,inner_add_right,hDiagL,hDiagR,hKΓ,hSwap2,hSwap]
    nlinarith only [hEnergy u,hEnergy v,hMixed u v]

Exact compiled BODY span, with preceding local definitions and inherited Hilbert structures in scope.

7. Substitute the actual conditional and polar components

For arbitrary actual f with integral zero, use the parent to produce its actual f_P and the actual conditional g_P of the same g. Keep f_V=V_0*Rf and g_V=V_0*Rg. Apply the two-argument congruence of C to the already proved component formulas, then subtract C(f_P,f_V) and apply the preceding algebra with u=f_P,v=f_V. Thus the corrector is evaluated on actual components, rather than components defined by the rotation right-hand sides.

\[f_V=V_0^*Rf,\quad g_V=V_0^*Rg,\quad C(g_P,g_V)-C(f_P,f_V)=-\|f_P\|^2+\|f_V\|^2.\]
Corresponding Lean step
  have hGlobal71 :
      (∀ 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‖ ∧
                              let g : Lp ℝ 2 J := U (P f-(f-P f))
                              (∫ z, g z ∂J)=0 ∧
                              ∃ gP : HP0,
                                HP0.subtypeL gP=condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le g ∧
                                let gperp : Hperp := R g
                                let gV : HP0 := V0.adjoint gperp
                                gP=A0 fP-ΓP0 fV ∧
                                gV=ΓP0 fP+A0 fV ∧
                                ‖gP‖^2+‖gV‖^2=‖fP‖^2+‖fV‖^2 ∧
                                let C : HP0 → HP0 → ℝ := fun u v =>
                                  (‖u‖^2-‖v‖^2)/2-inner ℝ (A0 (Inv u)) v
                                C gP gV-C fP fV= -‖fP‖^2+‖fV‖^2) := by
    intro f hf
    obtain ⟨fP,hfP,hBf,hΓf,hBudget,hVBudget,hgMean,gP,hgP,hgPformula,hgVformula,hgEnergy⟩ :=
      hGlobal f hf
    refine ⟨fP,hfP,hBf,hΓf,hBudget,hVBudget,hgMean,gP,hgP,hgPformula,hgVformula,hgEnergy,?_⟩
    change ((‖gP‖^2-‖V0.adjoint (R (U (P f-(f-P f))))‖^2)/2-
        inner ℝ (K gP) (V0.adjoint (R (U (P f-(f-P f))))))-
      ((‖fP‖^2-‖V0.adjoint (R f)‖^2)/2-inner ℝ (K fP) (V0.adjoint (R f)))=
      -‖fP‖^2+‖V0.adjoint (R f)‖^2
    let fV : HP0 := V0.adjoint (R f)
    let gV : HP0 := V0.adjoint (R (U (P f-(f-P f))))
    have hgp : gP=A0 fP-ΓP0 fV := hgPformula
    have hgv : gV=ΓP0 fP+A0 fV := hgVformula
    let C : HP0 → HP0 → ℝ := fun u v => (‖u‖^2-‖v‖^2)/2-inner ℝ (K u) v
    change C gP gV-C fP fV= -‖fP‖^2+‖fV‖^2
    have hPair : C gP gV=C (A0 fP-ΓP0 fV) (ΓP0 fP+A0 fV) :=
      congrArg₂ C hgp hgv
    exact (congrArg (fun a : ℝ => a-C fP fV) hPair).trans (hCorrector fP fV)

Exact compiled BODY span, with preceding local definitions and inherited Hilbert structures in scope.

8. Reassemble every original clause with the same witnesses

Retain the full-micro intertwining identity, actual projected rotation, pair energy and all earlier law/kernel/root/inverse/polar conclusions, and adjoin only the new corrector identity. This supplies the discrete corrector-change ingredient for the first two signed terms of B4/B28. Time evolution, the weak H1 bridge, nonexplosion, implementation error and expected-cost composition are not inferred from this algebra.

\[C(u,v)=\frac{\|u\|^2-\|v\|^2}{2}-\langle A_0\operatorname{Inv}u,v\rangle,\qquad C(g_P,g_V)-C(f_P,f_V)=-\|f_P\|^2+\|f_V\|^2.\]
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‖ ∧
                              let g : Lp ℝ 2 J := U (P f-(f-P f))
                              (∫ z, g z ∂J)=0 ∧
                              ∃ gP : HP0,
                                HP0.subtypeL gP=condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le g ∧
                                let gperp : Hperp := R g
                                let gV : HP0 := V0.adjoint gperp
                                gP=A0 fP-ΓP0 fV ∧
                                gV=ΓP0 fP+A0 fV ∧
                                ‖gP‖^2+‖gV‖^2=‖fP‖^2+‖fV‖^2 ∧
                                let C : HP0 → HP0 → ℝ := fun u v =>
                                  (‖u‖^2-‖v‖^2)/2-inner ℝ (A0 (Inv u)) v
                                C gP gV-C fP fV= -‖fP‖^2+‖fV‖^2) := ⟨hD,hIntertwine,hGlobal71⟩
  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

Exact compiled BODY span, with preceding local definitions and inherited Hilbert structures 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_corrector_change

Retain the same actual laws, operators and original inputs; Test the square identity and cancel mixed terms; Derive the corrector operator identities from the same inverse; Reduce the remaining mixed inner product; Evaluate both diagonal terms and align the mixed terms; Expand the corrector and compute its exact change; Substitute the actual conditional and polar components; Reassemble every original clause with the same witnesses

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_corrector_change
    {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_corrector_change_statement (E:=E) (V:=V) (α:=α) (β:=β) (η:=η) hα hαβ hV hH hη hβη := by
  unfold actual_corrector_change_statement
  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.ActualProjectedRotation.actual_projected_rotation
    (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 hDparent := parentSlice65.1
  have parentSlice66 := parentSlice65.2
  have hIntertwineParent := parentSlice66.1
  have hGlobal := parentSlice66.2
  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‖ ∧
                              let g : Lp ℝ 2 J := U (P f-(f-P f))
                              (∫ z, g z ∂J)=0 ∧
                              ∃ gP : HP0,
                                HP0.subtypeL gP=condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le g ∧
                                let gperp : Hperp := R g
                                let gV : HP0 := V0.adjoint gperp
                                gP=A0 fP-ΓP0 fV ∧
                                gV=ΓP0 fP+A0 fV ∧
                                ‖gP‖^2+‖gV‖^2=‖fP‖^2+‖fV‖^2) 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)) := hDparent h
  have hIntertwine : V0.adjoint ∘L D= -(A0 ∘L V0.adjoint) := hIntertwineParent
  have hΓself : IsSelfAdjoint ΓP0 := (show ΓP0.IsPositive from hPos0).isSelfAdjoint
  have hEnergy (u : HP0) : ‖A0 u‖^2+‖ΓP0 u‖^2=‖u‖^2 := by
    have h := congrArg (fun L : HP0 →L[ℝ] HP0 => inner ℝ (L u) u) hSquare0
    simp only [ContinuousLinearMap.add_apply,ContinuousLinearMap.mul_apply,
      ContinuousLinearMap.one_apply,inner_add_left] at h
    have ha : inner ℝ (A0 (A0 u)) u=‖A0 u‖^2 :=
      (hA0self.isSymmetric (A0 u) u).trans (real_inner_self_eq_norm_sq _)
    have hg : inner ℝ (ΓP0 (ΓP0 u)) u=‖ΓP0 u‖^2 :=
      (hΓself.isSymmetric (ΓP0 u) u).trans (real_inner_self_eq_norm_sq _)
    rw [ha,hg,real_inner_self_eq_norm_sq] at h
    exact h
  have hCross (u v : HP0) : inner ℝ (A0 u) (ΓP0 v)=inner ℝ (ΓP0 u) (A0 v) := by
    calc
      inner ℝ (A0 u) (ΓP0 v)=inner ℝ u (A0 (ΓP0 v)) := hA0self.isSymmetric _ _
      _ = inner ℝ u (ΓP0 (A0 v)) := congrArg (fun z : HP0 => inner ℝ u z) (DFunLike.congr_fun hComm0.eq v)
      _ = inner ℝ (ΓP0 u) (A0 v) := (hΓself.isSymmetric _ _).symm
  let K : HP0 →L[ℝ] HP0 := A0 ∘L Inv
  have hInvΓ (u : HP0) : Inv (ΓP0 u)=u := by
    have h := DFunLike.congr_fun hLeft u
    simpa only [ContinuousLinearMap.mul_apply,ContinuousLinearMap.one_apply] using h
  have hΓInv (u : HP0) : ΓP0 (Inv u)=u := by
    have h := DFunLike.congr_fun hRight u
    simpa only [ContinuousLinearMap.mul_apply,ContinuousLinearMap.one_apply] using h
  have hCommEval (u : HP0) : A0 (ΓP0 u)=ΓP0 (A0 u) :=
    DFunLike.congr_fun hComm0.eq u
  have hCommInvEval (u : HP0) : A0 (Inv u)=Inv (A0 u) :=
    DFunLike.congr_fun hCommInv.eq u
  have hKΓ (u : HP0) : K (ΓP0 u)=A0 u := congrArg A0 (hInvΓ u)
  have hΓK (u : HP0) : ΓP0 (K u)=A0 u := by
    change ΓP0 (A0 (Inv u))=A0 u
    calc
      ΓP0 (A0 (Inv u))=A0 (ΓP0 (Inv u)) := (hCommEval (Inv u)).symm
      _ = A0 u := congrArg A0 (hΓInv u)
  have hKA (u : HP0) : K (A0 u)=A0 (K u) := by
    change A0 (Inv (A0 u))=A0 (A0 (Inv u))
    exact congrArg A0 (hCommInvEval u).symm
  have hSquareApply (u : HP0) : A0 (A0 u)+ΓP0 (ΓP0 u)=u := by
    have h := DFunLike.congr_fun hSquare0 u
    simpa only [ContinuousLinearMap.add_apply,ContinuousLinearMap.mul_apply,
      ContinuousLinearMap.one_apply] using h
  have hKMixedVector (u : HP0) : A0 (K (A0 u))+ΓP0 (A0 u)=K u := by
    calc
      A0 (K (A0 u))+ΓP0 (A0 u)=K (A0 (A0 u))+K (ΓP0 (ΓP0 u)) :=
        congrArg₂ (fun x y : HP0 => x+y) (hKA (A0 u)).symm
          ((hCommEval u).symm.trans (hKΓ (ΓP0 u)).symm)
      _ = K (A0 (A0 u)+ΓP0 (ΓP0 u)) := (K.map_add _ _).symm
      _ = K u := congrArg K (hSquareApply u)
  have hMixed (u v : HP0) :
      inner ℝ (K (A0 u)) (A0 v)+inner ℝ (A0 u) (ΓP0 v)=inner ℝ (K u) v := by
    calc
      inner ℝ (K (A0 u)) (A0 v)+inner ℝ (A0 u) (ΓP0 v)=
          inner ℝ (A0 (K (A0 u))) v+inner ℝ (ΓP0 (A0 u)) v :=
        congrArg₂ (fun x y : ℝ => x+y)
          (hA0self.isSymmetric (K (A0 u)) v).symm
          (hΓself.isSymmetric (A0 u) v).symm
      _ = inner ℝ (A0 (K (A0 u))+ΓP0 (A0 u)) v := (inner_add_left _ _ _).symm
      _ = inner ℝ (K u) v := by rw [hKMixedVector]
  have hDiagL (u : HP0) : inner ℝ (K (A0 u)) (ΓP0 u)=‖A0 u‖^2 := by
    calc
      inner ℝ (K (A0 u)) (ΓP0 u)=inner ℝ (ΓP0 (K (A0 u))) u :=
        (hΓself.isSymmetric _ _).symm
      _ = inner ℝ (A0 (A0 u)) u := by rw [hΓK]
      _ = inner ℝ (A0 u) (A0 u) := hA0self.isSymmetric _ _
      _ = ‖A0 u‖^2 := real_inner_self_eq_norm_sq _
  have hDiagR (v : HP0) : inner ℝ (K (ΓP0 v)) (A0 v)=‖A0 v‖^2 := by
    rw [hKΓ,real_inner_self_eq_norm_sq]
  have hSwap (u v : HP0) : inner ℝ (ΓP0 u) (A0 v)=inner ℝ (A0 u) (ΓP0 v) :=
    (hCross u v).symm
  have hSwap2 (u v : HP0) : inner ℝ (A0 v) (ΓP0 u)=inner ℝ (A0 u) (ΓP0 v) :=
    (real_inner_comm _ _).trans (hSwap u v)
  have hCorrector (u v : HP0) :
      ((‖A0 u-ΓP0 v‖^2-‖ΓP0 u+A0 v‖^2)/2-
        inner ℝ (K (A0 u-ΓP0 v)) (ΓP0 u+A0 v))-
      ((‖u‖^2-‖v‖^2)/2-inner ℝ (K u) v)= -‖u‖^2+‖v‖^2 := by
    rw [norm_sub_sq_real,norm_add_sq_real,map_sub,inner_sub_left,
      inner_add_right,inner_add_right,hDiagL,hDiagR,hKΓ,hSwap2,hSwap]
    nlinarith only [hEnergy u,hEnergy v,hMixed u v]
  have hGlobal71 :
      (∀ 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‖ ∧
                              let g : Lp ℝ 2 J := U (P f-(f-P f))
                              (∫ z, g z ∂J)=0 ∧
                              ∃ gP : HP0,
                                HP0.subtypeL gP=condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le g ∧
                                let gperp : Hperp := R g
                                let gV : HP0 := V0.adjoint gperp
                                gP=A0 fP-ΓP0 fV ∧
                                gV=ΓP0 fP+A0 fV ∧
                                ‖gP‖^2+‖gV‖^2=‖fP‖^2+‖fV‖^2 ∧
                                let C : HP0 → HP0 → ℝ := fun u v =>
                                  (‖u‖^2-‖v‖^2)/2-inner ℝ (A0 (Inv u)) v
                                C gP gV-C fP fV= -‖fP‖^2+‖fV‖^2) := by
    intro f hf
    obtain ⟨fP,hfP,hBf,hΓf,hBudget,hVBudget,hgMean,gP,hgP,hgPformula,hgVformula,hgEnergy⟩ :=
      hGlobal f hf
    refine ⟨fP,hfP,hBf,hΓf,hBudget,hVBudget,hgMean,gP,hgP,hgPformula,hgVformula,hgEnergy,?_⟩
    change ((‖gP‖^2-‖V0.adjoint (R (U (P f-(f-P f))))‖^2)/2-
        inner ℝ (K gP) (V0.adjoint (R (U (P f-(f-P f))))))-
      ((‖fP‖^2-‖V0.adjoint (R f)‖^2)/2-inner ℝ (K fP) (V0.adjoint (R f)))=
      -‖fP‖^2+‖V0.adjoint (R f)‖^2
    let fV : HP0 := V0.adjoint (R f)
    let gV : HP0 := V0.adjoint (R (U (P f-(f-P f))))
    have hgp : gP=A0 fP-ΓP0 fV := hgPformula
    have hgv : gV=ΓP0 fP+A0 fV := hgVformula
    let C : HP0 → HP0 → ℝ := fun u v => (‖u‖^2-‖v‖^2)/2-inner ℝ (K u) v
    change C gP gV-C fP fV= -‖fP‖^2+‖fV‖^2
    have hPair : C gP gV=C (A0 fP-ΓP0 fV) (ΓP0 fP+A0 fV) :=
      congrArg₂ C hgp hgv
    exact (congrArg (fun a : ℝ => a-C fP fV) hPair).trans (hCorrector fP fV)
  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‖ ∧
                              let g : Lp ℝ 2 J := U (P f-(f-P f))
                              (∫ z, g z ∂J)=0 ∧
                              ∃ gP : HP0,
                                HP0.subtypeL gP=condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le g ∧
                                let gperp : Hperp := R g
                                let gV : HP0 := V0.adjoint gperp
                                gP=A0 fP-ΓP0 fV ∧
                                gV=ΓP0 fP+A0 fV ∧
                                ‖gP‖^2+‖gV‖^2=‖fP‖^2+‖fV‖^2 ∧
                                let C : HP0 → HP0 → ℝ := fun u v =>
                                  (‖u‖^2-‖v‖^2)/2-inner ℝ (A0 (Inv u)) v
                                C gP gV-C fP fV= -‖fP‖^2+‖fV‖^2) := ⟨hD,hIntertwine,hGlobal71⟩
  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.ActualCorrectorChange

#print axioms AutoSamplingTheory.ExampleCases.ProximalBPS.ActualCorrectorChange.actual_corrector_change

Exact module and namespace context

Scope and omitted-condition boundaries
  • Actual B21 corrector change is the present bounded theorem. Lemma B4/B28 dynamics, weak H1/B2, invariance/nonexplosion, full PBPS/SPHMC results, implementation errors/caps, actual-input expected-query costs and composition remain separate obligations. B21 alone establishes no full Exposition, PURIFIED, main/live, whole-paper or Goal completion.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • IsSelfAdjoint.isSymmetric
  • ContinuousLinearMap.IsPositive.isSelfAdjoint
  • ContinuousLinearMap.mul_apply
  • Commute.eq
  • real_inner_self_eq_norm_sq
  • real_inner_comm
  • norm_add_sq_real
  • norm_sub_sq_real
  • congrArg₂

Mathematical sources

  • PBPS Appendix B3 B20/B21; P16/P17 exact actual corrector-change and B4/B28 consumer — Actual B21 corrector change is the present bounded theorem. Lemma B4/B28 dynamics, weak H1/B2, invariance/nonexplosion, full PBPS/SPHMC results, implementation errors/caps, actual-input expected-query costs and composition remain separate obligations. Independent review, integration, full Exposition and PURIFIED remain pending.

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