RelativeLimitLoadBridge

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

Limiting scalar for the same-cutoff relative normalization

The relative normalization is an arbitrary integer triadic dilation of the genuine cutoff law. This file transports the deterministic coarse block matrix through that dilation, lifts the identity to annealed block matrices, and identifies the relative law's limiting scalar with the already characterized source-facing sigmaBar.

The proof keeps the cutoff index fixed. It uses only a finite shift of the natural-scale limit and does not assume covariance between cutoff indices.

theorem Algsuperdiff.Section3.Provider.Homogenization.coarseBlockMatrix_cubeSet_dilateReg_of_aelocallyUniformlyElliptic {d : ℕ} [NeZero d] {a : HCPolySupport.RegCoeffField d} (ha : HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField a) (k : ℤ) (Q : HCPolySupport.TriadicCube d) : HCPolySupport.coarseBlockMatrix (HCPolySupport.cubeSet Q) (HCPolySupport.dilateReg k a).toFun = HCPolySupport.coarseBlockMatrix (HCPolySupport.cubeSet (HCPolySupport.Book.Ch02.dilateCube (-k) Q)) a.toFun

The deterministic coarse block matrix shifts on an arbitrary triadic cube under an arbitrary integer dilation of the coefficient field.

theorem Algsuperdiff.Section3.Provider.Homogenization.annealedBlockMatrix_map_dilateReg_cube {d : ℕ} [NeZero d] {P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d} (hP : HCPolySupport.Book.Ch04.RestrictionLawCarrier P) (k : ℤ) (hPk : HCPolySupport.Book.Ch04.RestrictionLawCarrier (MeasureTheory.Measure.map (HCPolySupport.dilateReg k) P)) (Q : HCPolySupport.TriadicCube d) : HCPolySupport.Book.Ch04.annealedBlockMatrix (MeasureTheory.Measure.map (HCPolySupport.dilateReg k) P) (HCPolySupport.cubeSet Q) = HCPolySupport.Book.Ch04.annealedBlockMatrix P (HCPolySupport.cubeSet (HCPolySupport.Book.Ch02.dilateCube (-k) Q))

Annealed coarse block matrices shift under an arbitrary integer dilation pushforward.

theorem Algsuperdiff.Section3.Provider.Homogenization.annealedBlockMatrixAtScale_relativeNormalizedCutoffLaw {d : ℕ} [NeZero d] (M : ABKModel d) (cutoff : ℤ) (r : ℕ) : HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.relativeNormalizedCutoffLaw M cutoff) ↑r = HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M cutoff) (cutoff + ↑(Cutoff.cutoffRelativeNormalizationShift d) + ↑r)

The relative law's annealed matrix at natural scale r is the genuine same-index cutoff law's matrix at physical integer scale cutoff + c + r.

theorem Algsuperdiff.Section3.Provider.Homogenization.relativeNormalizedCutoff_barSigmaLimit_eq_sigmaBar {d : ℕ} [NeZero d] (M : ABKModel d) (cutoff : ℤ) : HCPolySupport.Book.Ch05.Section57.barSigmaLimit ⋯ ⋯ = ↑(Annealed.sigmaBar M cutoff)

The limiting scalar of the same-cutoff relative law is exactly the source-facing running diffusivity.