ShellSumLayerZeroEnergy

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The layer-zero term of the shell decomposition is the (J4) constant

ABK26, a.j.nondeg and e.perturb.assumption.

ShellSumLayerFlip.lean reduces the shell-sum corrector energy to the diagonal sum Σ_{k ∈ (n,m]} ‖P 𝐟_k‖² on the layer carrier. This module evaluates the k = 0 term:

‖P 𝐟_0‖² = c⋆ (log 3) at a unit direction,

by transporting to the single-shell path carrier along the equivariant coordinate map F ↦ F 0 and reading FreshShellCorrectorEnergy.integral_normSq_valuePathCorrectorRepr_eq.

theorem Algsuperdiff.Section3.Provider.Corrector.measurePreserving_seqPathCoord_zero {d : ℕ} (M : ABKModel d) : MeasureTheory.MeasurePreserving (fun (F : ℤ → C(HCPolySupport.Vec d, HCPolySupport.Mat d)) => F 0) ↑(seqPathLaw M.P) ↑(zeroShellValuePathLaw M.P)

Reading layer zero pushes the layer law onto the fresh-shell path law.

theorem Algsuperdiff.Section3.Provider.Corrector.carrierTransport_valuePathForcingL2 {d : ℕ} (M : ABKModel d) {e : HCPolySupport.Vec d} (he : HCPolySupport.Book.Ch02.vecNorm e = 1) : (carrierTransport (HCPolySupport.HilbertVec d) ⋯) (valuePathForcingL2 M he) = layerForcingL2 M e 0

The transported fresh-shell forcing is the layer-zero forcing.

theorem Algsuperdiff.Section3.Provider.Corrector.norm_sq_stationaryPotentialProjection_layerForcingL2_zero {d : ℕ} (M : ABKModel d) {e : HCPolySupport.Vec d} (he : HCPolySupport.Book.Ch02.vecNorm e = 1) : ‖Probability.Stationary.stationaryPotentialProjection (layerForcingL2 M e 0)‖ ^ 2 = Disorder.cstar M * Real.log 3

The layer-zero corrector energy is the (J4) constant.

The k = 0 term of the layer decomposition of e.perturb.assumption equals c⋆ (log 3) at a unit direction, c⋆ the constant selected by a.j.nondeg.