HomSpineResiduePairing

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

The EthmB(m) pairing: the two printed summands, against the two level slots

What this file supplies

HomSpineInstallArith reduced the §4.5 level arithmetic to three residues, of which two — hA, hB together with the budget split hsplit — are the manuscript's "comparing to the definition of EthmB(m)". This file performs that comparison at the two printed summands of EthmB(m):

  EthmB(m) = s^{-1} 3^{(1-α)X_m(α)} 𝓔_{s₁}(□_m,n) (1 + 𝓔_{1/4}(□_m))
               + C γ⁵ (1 + 𝓔²_{s₁/2}(□_m,n)).

• ofReal_firstLeg_le pairs the FIRST level slot C_cg σ⁻¹ 𝓔₁ C_en against the first summand. The Step-2 constant C_en is taken at the shape the printed energy-density bound gives it — C_en = C · (3^{(1-α)X_m} (1 + 𝓔_{1/4})) — which is what makes the pairing an inequality between the SAME two random factors.
• the gap leg pairs the SECOND level slot against the γ⁵ summand, through HomSpineInstallData.homGapAbsorbAt at any s₂ admitting the absorption, in particular the corrected pin s₂ = 49/100.
• ofReal_add_le_ethmB adds the two, and le_toReal_of_ofReal_le converts the [0,∞] domination into the REAL budget inequality A + B ≤ C_w · E_B that the bundle's hsplit conjunct is, at E_B:= (EthmB(m))(ω).toReal.

The two 𝓔-dominations are the file's inputs, stated at the own carriers; see the disclosure below.

Scope

The two hypotheses hdom1, hdom2 compare the coarse-graining bundle's error slots with EthmB(m)'s own factors. At the CURRENT pins these two are NOT the same object, in three independent respects, and no bridge between them exists in the tree:

1. the coefficient — the bundle's slots dominate parentTruncatedHomogenizationErrorInfinity{One,Two}Scalar at the CUTOFF field a_L (Cutoff.coefficientCutoffCoeffOn), while EthmB(m) and BOTH printed displays carry the FLUX-CORRECTED field ã_{L,m};
2. the order — the bundle pins the dual low order at s₁′ = s/8 (and its half s/16), while EthmB(m) carries s₁ = s/2 (and s₁/2 = s/4), the print's own choice the §4.5 parameter choices. 𝓔 is a weighted average with normalized weights and is NOT monotone in the order, so neither direction is free;
3. the q index — the first slot's carrier is the q = 1 functional, EthmB(m)'s first factor the q = 2 one (the print has the same asymmetry between the two printed displays, where it is a Jensen step).

Nothing in this file asserts those inputs; they are named, and the arithmetic above them is proved outright.

1. The two summands of EthmB(m), named

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.ethmBFirst {d : ℕ} (M : Section3.ABKModel d) (Y : Section3.Cutoff.CutoffSample d → ENNReal) (m n : ℤ) (s : { s : ℝ // 0 < s }) (omega : Section3.Cutoff.CutoffSample d) : ENNReal

The FIRST summand of EthmB(m): the minimal-scale factor times the two printed 𝓔 factors, weighted by s^{-1}.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.ethmBGap {d : ℕ} (M : Section3.ABKModel d) (Cgap : ℝ) (m n : ℤ) (s : { s : ℝ // 0 < s }) (omega : Section3.Cutoff.CutoffSample d) : ENNReal

The SECOND summand of EthmB(m): the γ⁵ gap term.

Equations

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

theorem Algsuperdiff.Section4.Provider.Homogenization.ethmB_eq_first_add_gap {d : ℕ} (M : Section3.ABKModel d) (Cgap : ℝ) (Y : Section3.Cutoff.CutoffSample d → ENNReal) (m n : ℤ) (s : { s : ℝ // 0 < s }) (omega : Section3.Cutoff.CutoffSample d) : ethmB M Cgap Y m n s omega = ethmBFirst M Y m n s omega + ethmBGap M Cgap m n s omega

EthmB(m) IS the sum of its two named summands.

2. The first leg: the level's first slot against the first summand

theorem Algsuperdiff.Section4.Provider.Homogenization.ofReal_firstLeg_le {d : ℕ} (M : Section3.ABKModel d) (Y : Section3.Cutoff.CutoffSample d → ENNReal) (m n : ℤ) (s : { s : ℝ // 0 < s }) (omega : Section3.Cutoff.CutoffSample d) {c Cen0 E1 : ℝ} (hc : 0 ≤ c) (hCen0 : 0 ≤ Cen0) (hE1 : 0 ≤ E1) (hdom : ENNReal.ofReal E1 ≤ Support.fluxCorrectedTwoScaleErrorObservableSup M m n (homHalf s) omega) : ENNReal.ofReal (c * E1 * (Cen0 * (Y omega * (1 + Support.fluxCorrectedTwoScaleErrorObservableSup M m m homQuarter omega)).toReal)) ≤ ENNReal.ofReal (c * Cen0 * ↑s) * ethmBFirst M Y m n s omega

THE FIRST PAIRING.

The level's first slot — the coarse-graining constant, the order weight, the error slot and the Step-2 constant C_en at its printed shape C · (3^{(1-α)X_m}(1 + 𝓔_{1/4})) — is below the first summand of EthmB(m) times a constant that carries no randomness.

The single input is hdom: the error slot is dominated by EthmB(m)'s own first 𝓔 factor. See the module disclosure.

3. The second leg: the level's forcing slot against the γ⁵ summand

theorem Algsuperdiff.Section4.Provider.Homogenization.homGapConstAt_nonneg {s2 : ℝ} (hs2 : 5 < 10 * s2 * Real.log 3) : 0 ≤ homGapConstAt s2

The gap-absorption constant is nonnegative exactly on the range where the absorption holds.

4. The two legs added: the budget inequality

theorem Algsuperdiff.Section4.Provider.Homogenization.ofReal_add_le_ethmB {d : ℕ} (M : Section3.ABKModel d) (Cgap : ℝ) (Y : Section3.Cutoff.CutoffSample d → ENNReal) (m n : ℤ) (s : { s : ℝ // 0 < s }) (omega : Section3.Cutoff.CutoffSample d) {A B cA cB : ℝ} (hA0 : 0 ≤ A) (hB0 : 0 ≤ B) (hcA0 : 0 ≤ cA) (hcB0 : 0 ≤ cB) (hA : ENNReal.ofReal A ≤ ENNReal.ofReal cA * ethmBFirst M Y m n s omega) (hB : ENNReal.ofReal B ≤ ENNReal.ofReal cB * ethmBGap M Cgap m n s omega) : ENNReal.ofReal (A + B) ≤ ENNReal.ofReal (cA + cB) * ethmB M Cgap Y m n s omega

THE EthmB(m) BUDGET, in [0,∞]. Both level slots together are below EthmB(m) times the sum of the two pairing constants.

5. The real budget: the bundle's hsplit, at E_B = (EthmB(m)).toReal

theorem Algsuperdiff.Section4.Provider.Homogenization.le_toReal_of_ofReal_le {X Cw : ℝ} {T : ENNReal} (hCw : 0 ≤ Cw) (hfin : T ≠ ⊤) (h : ENNReal.ofReal X ≤ ENNReal.ofReal Cw * T) : X ≤ Cw * T.toReal

THE REAL CUT. An [0,∞] domination by C_w · EthmB(m) becomes the bundle's own real budget inequality at E_B:= (EthmB(m))(ω).toReal, on the (a.e.) event where the carrier is finite.