FluxCorrectedTwoScaleCarrier

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

The two-argument carrier identity for the flux-corrected (∞,2) error

FluxCorrectedTwoScale.lean builds the measurable two-argument observable fluxCorrectedTwoScaleErrorObservableSup and records its a.e. identification with CoarseGraining's literal object as a named obligation. This file discharges that obligation in the exact form the §4.5 chain consumes it: for a.e. sample, at every admissible L and every fractional order, CoarseGraining's literal q = 2 truncated parent error of the flux-corrected coefficient on □_m is the extended-real encoding of the proved measurable two-argument representative.

The three ingredients

1. Summability of the real series is internal to that theorem (it comes from the uniform response bound of the parent CoeffOn's own ellipticity constants), so no summability side condition enters here and the real square root does not junk to 0.

2. The family swap is a.e.-invariance of the response. The response value set is built from Ch02.doubledResponseJ, which depends on the coefficient only through its a.e. class (Ch02.doubledResponseJ_eq_ofAEEq). Hence Ch02.normalizedBlockResponseMax is unchanged when the root pointwise family of fluxCorrectedCoeffOn is replaced by the proved canonical family fluxCorrectedCoeffFamily: both are a.e. the same field on every descendant cube (fluxCorrectedRegField_toFun).

3. The representative swap is the proved probability-one event ae_forall_normalizedBlockResponseMax_fluxCorrected_eq_representative, which is indexed by L alone — it does not depend on the order t — so a single countable intersection over L ≥ m carries every order at once.

Units

Carrier bookkeeping only. σ_m occurs solely as the comparator of the two error functionals, and it is the SAME comparator on both sides (isotropicComparatorMatrix (σ_m) = scalarMatrix (σ_m) definitionally). No ν-division, no ν ↔ σ conversion, no flat elliptic estimate.

1. The comparator is literally CoarseGraining's scalar matrix

2. The response maximum sees the coefficient only through its a.e. class

theorem Algsuperdiff.Section4.Support.normalizedBlockResponseMax_congr_of_aeeq {d : ℕ} (R : HCPolySupport.TriadicCube d) {F G : HCPolySupport.Book.Ch02.TriadicCoeffFamily d} (a0 : HCPolySupport.Mat d) (h : (F.coeffOn R).AEEq (G.coeffOn R)) : HCPolySupport.Book.Ch02.normalizedBlockResponseMax R F a0 = HCPolySupport.Book.Ch02.normalizedBlockResponseMax R G a0

A.e. invariance of the one-cube response maximum. If two triadic families have a.e. equal representatives on R, their normalized block-response maxima on R agree. The whole content is Ch02.doubledResponseJ_eq_ofAEEq: the response is an infimum/supremum of integrals of the coefficient, so it factors through the a.e. class.

theorem Algsuperdiff.Section4.Support.fluxCorrectedCoeffFamily_coeffOn_aeeq_rootPointwise {d : ℕ} (M : Section3.ABKModel d) (L m : ℤ) (Q : HCPolySupport.TriadicCube d) (omega : Section3.Cutoff.CutoffSample d) {R : HCPolySupport.TriadicCube d} {k : ℤ} (hk : k ≤ Q.scale) (hR : R ∈ HCPolySupport.descendantsAtScale Q k) : ((fluxCorrectedCoeffFamily M L m Q omega).coeffOn R).AEEq ((HCPolySupport.Book.Ch03.ABK26.rootPointwiseCoeffFamily Q (fluxCorrectedCoeffOn M L m Q omega)).coeffOn R)

The proved canonical family of the flux-corrected field and CoarseGraining's root pointwise family of the flux-corrected CoeffOn are a.e. equal on every descendant cube: both representatives are literally the flux-corrected field.

theorem Algsuperdiff.Section4.Support.maxDescendant_rootPointwise_eq_fluxCorrectedCoeffFamily {d : ℕ} (M : Section3.ABKModel d) (L m : ℤ) (Q : HCPolySupport.TriadicCube d) (omega : Section3.Cutoff.CutoffSample d) {k : ℤ} (hk : k ≤ Q.scale) (a0 : HCPolySupport.Mat d) : HCPolySupport.Book.Ch02.maxDescendantNormalizedBlockResponseAtScale Q k (HCPolySupport.Book.Ch03.ABK26.rootPointwiseCoeffFamily Q (fluxCorrectedCoeffOn M L m Q omega)) a0 = HCPolySupport.Book.Ch02.maxDescendantNormalizedBlockResponseAtScale Q k (fluxCorrectedCoeffFamily M L m Q omega) a0

The descendant maximum at one physical scale is the same for CoarseGraining's root pointwise family and for the proved canonical flux-corrected family.

3. The carrier identity at one sample of the proved event

theorem Algsuperdiff.Section4.Support.parentTruncatedTwo_fluxCorrected_eq_ofReal_representative {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L m n : ℤ) (hn : n ≤ (HCPolySupport.originCube d m).scale) (t : ↑HCPolySupport.FractionalOrder) (omega : Section3.Cutoff.CutoffSample d) (hall : ∀ (R : HCPolySupport.TriadicCube d), HCPolySupport.Book.Ch02.normalizedBlockResponseMax R (fluxCorrectedCoeffFamily M L m (HCPolySupport.originCube d m) omega) (Section3.Observable.isotropicComparatorMatrix (Section3.Annealed.sigmaBar M m)) = fluxCorrectedNormalizedBlockResponseRepresentative M L m (HCPolySupport.originCube d m) R (Section3.Observable.isotropicComparatorMatrix (Section3.Annealed.sigmaBar M m)) omega) : HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityTwoScalar (HCPolySupport.originCube d m) n hn (fluxCorrectedCoeffOn M L m (HCPolySupport.originCube d m) omega) ↑(Section3.Annealed.sigmaBar M m) ⋯ t = ENNReal.ofReal (fluxCorrectedTwoScaleErrorFunctional M L m n (↑t) omega)

The two-argument carrier identity, at one sample.

On the proved probability-one event of ae_forall_normalizedBlockResponseMax_fluxCorrected_eq_representative, CoarseGraining's literal q = 2 truncated parent error of the flux-corrected coefficient ã_{L,m} on □_m, truncated at any n ≤ m, is exactly the extended-real encoding of the proved measurable two-argument representative at the same order. This is an, not a domination.

4. The public carrier, at the {s // 0 < s} order and a.e.

theorem Algsuperdiff.Section4.Support.ae_forall_parentTruncatedTwo_fluxCorrected_eq_representative {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (m n : ℤ) (hn : n ≤ (HCPolySupport.originCube d m).scale) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (L : ℤ), m ≤ L → ∀ (t : ↑HCPolySupport.FractionalOrder), HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityTwoScalar (HCPolySupport.originCube d m) n hn (fluxCorrectedCoeffOn M L m (HCPolySupport.originCube d m) omega) ↑(Section3.Annealed.sigmaBar M m) ⋯ t = ENNReal.ofReal (fluxCorrectedTwoScaleErrorRepresentative M L m n ⟨↑t, ⋯⟩ omega)

The a.e. two-argument carrier identification.

One probability-one event, one measure: on it, at every L ≥ m and every fractional order, CoarseGraining's literal q = 2 truncated parent error of ã_{L,m} at the truncation index n equals the encoding of the proved measurable two-argument representative. The event is the countable intersection over L ≥ m of the proved per-L events; the order plays no role in it.