NormalizedStructuralLaw

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

Structural law of the normalized coefficient cutoff

This file packages the structural properties of the canonically normalized coefficient-cutoff law. Stationarity, isotropy, and adjoint invariance are transported separately through CoarseGraining's triadic normalization. Unit-range dependence comes from the direct restriction-sigma-algebra proof for the normalized cutoff law; no unit-range property of the unnormalized law is assumed.

Main results

• cutoffNormalization_structuralLaw: the normalized cutoff law satisfies the four Chapter 4 structural assumptions.

theorem Algsuperdiff.Section3.Cutoff.cutoffNormalization_structuralLaw {d : ℕ} (M : ABKModel d) (m : ℤ) : HCPolySupport.Book.Ch04.RestrictionStructuralLaw (HCPolySupport.Book.Ch04.restrictionScaleNormalizedLaw (cutoffNormalizationDepth d m) (coefficientCutoffLaw M m))

The canonically normalized genuine cutoff law has exactly the Chapter 4 structural package. The three symmetry fields are transported independently; the unit-range field is the direct normalized-law theorem.