HomSeamSqrtTwoChain #

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

The level pairing at the re-pinned base `s/8`, absorbing the `√2` #

What moves #

HomSpineResidueLevel's pairing chain is stated at EthmB(m)'s PRINTED base ⟨homS M, hs⟩ and takes both 𝓔-dominations at constant one. The re-pin moves the base to s' = s/8 (HomSeamRepin.homSeamBase) and delivers the SECOND domination at √2, because the order step 𝓔_{s/16,∞,2} ≤ √2 · 𝓔_{s/32,∞,2} costs exactly the ratio of the two geometric normalizations. This file carries the two consequences:

the gap pairing at a general domination constant K ≥ 1 (ofReal_gapLeg_le_of_const), the constant entering as K² — the ofReal_one_add_sq_le_of_const is the whole of it; The base re-pin is FREE on the first leg: ofReal_firstLeg_le returns the constant c · C_en0 · s', and s' = s/8 ≤ s, so the leg constant already covers it. The √2 is the only genuine cost, and it is a factor 2.

Slot-agnosticism (and why the chain stops here) #

Every theorem below takes the two error slots as BARE nonnegative reals E1, E2. It is therefore valid at the slots (the pinned slots at the uncut a_L) and equally at the print-accurate slots (HomSeamFluxCoefficient.recutPinnedE1Flux/E2Flux, at ã_{L,m}). The chain deliberately stops before the a_L lane's hlevel, which names the pinned 𝓔₁ slot and so fixes the coefficient: see HomSeamFluxCoefficient's module disclosure for why the a_L-sided domination is not available and what the print-accurate re-instantiation costs.

1. The gap pairing at a general domination constant #

source

theorem Algsuperdiff.Section4.Provider.Homogenization.ofReal_gapLeg_le_of_const {d : ℕ} (M : Section3.ABKModel d) {Cgap : ℝ} (m : ℤ) (s : { s : ℝ // 0 < s }) (omega : Section3.Cutoff.CutoffSample d) {c E2 s2 K : ℝ} (hlog : 4 ≤ |Real.log M.gamma|) (hgamma1 : M.gamma < 1) (hCgap : 0 < Cgap) (hc : 0 ≤ c) (hE2 : 0 ≤ E2) (hs2 : 5 < 10 * s2 * Real.log 3) (hK : 1 ≤ K) (hdom : ENNReal.ofReal E2 ≤ ENNReal.ofReal K * Support.fluxCorrectedTwoScaleErrorObservableSup M m (homN M m) (homQuarterOf s) omega) :

ENNReal.ofReal (c * (homS M ^ (-(9 / 2)) * 3 ^ (s2 * ↑(homN M m) - s2 * ↑m)) * (1 + E2 ^ 2)) ≤ ENNReal.ofReal (c * K ^ 2 * homGapConstAt s2 / Cgap) * ethmBGap M Cgap m (homN M m) s omega

THE SECOND PAIRING AT A GENERAL DOMINATION CONSTANT.

HomSpineResiduePairing's gap pairing with the domination weakened from constant one to constant K ≥ 1. The pairing constant picks up exactly K²; the mesoscale gap absorption homGapAbsorbAt is untouched.