CarrierIdentification

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

The two ã_{L,m} carriers of Section 4.1 carry the same response functional

ABK26, Section 4.1, (ã_{L,m} := a_L − (k_L − k_m)_{□_m}), (e.mathcalE.annular.decomp.pre).

Section 4.1 reads the response functional J(z+□_n, …; ã_{L,m}) through two different Chapter 2 triadic coefficient families:

• subConstCutoffTriadicCoeffFamily M L C hC ω at C := (k_L − k_m)_{□_m} — the hand-built family of SubConstFamily, the object the ugly chain and hence the annulus maximum of FinalStitch is built on.

Their fields are literally the same function of x (Support.fluxCorrectedField_apply and subConstCutoffField_apply both read a_L(x) − C), but the two TriadicCoeffFamily wrappers are constructed differently, so no responseJ identification was available. This module supplies it.

The route

The missing input is the Ch02.CoeffOn.AEEq between the two coeffOn values. Both sides have a definitional coeffOn-characterization:

• subConstCutoffTriadicCoeffFamily_coeffOn_toCoeffField (this repository) gives ((… C hC ω).coeffOn Q).toCoeffField = subConstCutoffField M L C ω by rfl.

So the A is Filter.Eventually.of_forallapplied to a pointwise field identity, andCh02.responseJ_eq_ofA transports every response value; the supremum over the unit sphere follows. No new device and no new mathematics: this is a definitional unfolding on both sides.

Ownership note

annularResponseMaxPref is the canonical annulus response family. FinalStitch.annularResponseMax reuses it through an abbreviation, so both names reduce to the same lattice maximum.

References

• ABK26.

Part A -- the scalar response maximum respects a.e. equality

Part B -- the two ã_{L,m} families agree on every lattice cube

theorem Algsuperdiff.Section4.Provider.Annular.fluxCorrectedCoeffFamily_coeffOn_aeeq_subConstCutoff {d : ℕ} (M : Section3.ABKModel d) (L m : ℤ) (omega : Section3.Cutoff.CutoffSample d) (n : ℤ) (v : Fin d → ℤ) : ((Support.fluxCorrectedCoeffFamily M L m (HCPolySupport.originCube d m) omega).coeffOn (latticeCube n v)).AEEq ((subConstCutoffTriadicCoeffFamily M L (Support.fluxIncrementAverage M L m (HCPolySupport.originCube d m) omega) ⋯ omega).coeffOn { scale := n, index := v })

A6c finding (f), closed. The Chapter 4 dependent family of the flux-corrected carrier field and the hand-built family of a_L − C at C = (k_L − k_m)_{□_m} have a.e. equal coefficient objects on every scale-n lattice cube.

The proof is a pointwise field identity: both toCoeffField values reduce definitionally, one through Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField_coeffOn_toCoeffField and Support.fluxCorrectedRegField_toFun, the other through subConstCutoffTriadicCoeffFamily_coeffOn_toCoeffField, to x ↦ a_L(x) − (k_L − k_m)_{□_m}.

theorem Algsuperdiff.Section4.Provider.Annular.scalarResponseMax_fluxCorrected_eq_subConstCutoff {d : ℕ} (M : Section3.ABKModel d) (L m : ℤ) (omega : Section3.Cutoff.CutoffSample d) (n : ℤ) (v : Fin d → ℤ) (sigma : Section3.Observable.PositiveScalar) : scalarResponseMax ((Support.fluxCorrectedCoeffFamily M L m (HCPolySupport.originCube d m) omega).coeffOn (latticeCube n v)) sigma = scalarResponseMax ((subConstCutoffTriadicCoeffFamily M L (Support.fluxIncrementAverage M L m (HCPolySupport.originCube d m) omega) ⋯ omega).coeffOn { scale := n, index := v }) sigma

The response-level carrier identification. The scalar response maximum of the jLegField carrier at the lattice cube 3^n v + □_n equals the scalar response maximum of the annulus carrier at the same cube.

Part C -- the annulus response family

noncomputable def Algsuperdiff.Section4.Provider.Annular.annularResponseMaxPref {d : ℕ} (M : Section3.ABKModel d) (L m : ℤ) (omega : Section3.Cutoff.CutoffSample d) (j n : ℤ) : ℝ

The Jann family of e.mathcalE.annular.decomp.pre: the maximum, over the scale-n lattice cubes of the annulus □_j ∖ □_{j−1}, of the scalar response maximum of ã_{L,m}.

FinalStitch.annularResponseMax is a compatibility name for this family.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.Annular.annularResponseMaxPref_nonneg {d : ℕ} (M : Section3.ABKModel d) (L m : ℤ) (omega : Section3.Cutoff.CutoffSample d) (j n : ℤ) : 0 ≤ annularResponseMaxPref M L m omega j n

theorem Algsuperdiff.Section4.Provider.Annular.scalarResponseMax_le_annularResponseMaxPref {d : ℕ} (M : Section3.ABKModel d) (L m : ℤ) (omega : Section3.Cutoff.CutoffSample d) {j n : ℤ} (hnj : n ≤ j) {v : Fin d → ℤ} (hv : v ∈ Support.latticeAnnulusSet d n j (j - 1)) : scalarResponseMax ((Support.fluxCorrectedCoeffFamily M L m (HCPolySupport.originCube d m) omega).coeffOn (latticeCube n v)) (Section3.Annealed.sigmaBar M m) ≤ annularResponseMaxPref M L m omega j n

The annulus family dominates each of its jLegField-carrier entries. For a lattice index in the annulus □_j ∖ □_{j−1}, the flux-corrected scalar response maximum at that cube is at most the annulus maximum.

theorem Algsuperdiff.Section4.Provider.Annular.annularResponseMaxPref_le_jLegField {d : ℕ} (M : Section3.ABKModel d) (L m : ℤ) (omega : Section3.Cutoff.CutoffSample d) {j n : ℤ} (hjm : j ≤ m) (hnj : n ≤ j - 1) : annularResponseMaxPref M L m omega j n ≤ jLegField M L m omega n

The annulus family is dominated by the full-grid J-leg. Every annulus index of □_j ∖ □_{j−1} with j ≤ m is a lattice index of □_m, so the annulus maximum is at most AssemblyFeed.jLegField at the same scale.

theorem Algsuperdiff.Section4.Provider.Annular.annularResponseMaxPref_le_uniform {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L m : ℤ) (omega : Section3.Cutoff.CutoffSample d) {j n : ℤ} (hjm : j ≤ m) (hnj : n ≤ j - 1) : annularResponseMaxPref M L m omega j n ≤ HCPolySupport.Book.Ch02.normalizedBlockResponseUniformBound (HCPolySupport.originCube d m) (Support.fluxCorrectedCoeffFamily M L m (HCPolySupport.originCube d m) omega) (Section3.Observable.isotropicComparatorMatrix (Section3.Annealed.sigmaBar M m))

The annulus family is uniformly bounded, by the single cube-□_m ellipticity constant of AssemblyFeed.jLegField_le_uniform. Unconditional: no event, no probability, no regime.