HomSeamRepin

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

The EthmB(m) seam, re-pinned: two dominations reduced to ONE bridge

The seam, and why the printed base exponent has to move

HomSpineResiduePairing's disclosure lists three mismatches between the coarse-graining bundle's error slots and EthmB(m)'s 𝓔 factors: the coefficient field, the ORDER, and the q INDEX. the sections below settle the last two at CoarseGraining's carrier, and in doing so FIX the admissible orders:

  slot 1: 𝓔_{s/8,∞,1}(a_L)   →  𝓔_{s/16,∞,2}(a_L)   (q-index, constant 1)
  slot 2: 𝓔_{s/16,∞,2}(a_L)  →  𝓔_{s/32,∞,2}(a_L)   (order, constant √2)

The q-index step is only available at the HALVED order, so the first slot can be compared with an 𝓔 factor of order s/16 and no larger; at the printed s₁ = s/2 the comparison is FALSE, which is exactly the obstruction measured here. The move carried here changes nothing but a parameter value: EthmB(m) is instantiated at the BASE exponent

  s':= s/8      (so s₁ = s'/2 = s/16 and s₁/2 = s'/4 = s/32),

i.e. the printed formula the §4.5 parameter choices with s ↦ s/8, the shape of EthmB(m) untouched (HomStepEnvelope.ethmB is already parametrized by its base exponent, so this is an INSTANTIATION, not a new definition). The visible costs are s'^{-1} = 8 s^{-1} in the prefactor and the eightfold shrink of the anchor's admissible p-range; the 3-power of the bounds_mathcal_E_aL majorant IMPROVES (3^{(1/2)(s/16)(m-n)} in place of 3^{(1/2)(s/2)(m-n)}). Both costs are model-independent multiples and are absorbed by the root's existential constant; the re-pinned Step-1 moment bound is NOT proved here (see the disclosure).

Scope

The two domination slots at the re-pinned base are NOT proved here. They would need the COEFFICIENT half of the seam: the bundle's slots live at the cutoff field a_L (Cutoff.coefficientCutoffCoeffOn), while EthmB(m) and all four printed displays carry the flux-corrected field ã_{L,m}, and nothing in this file asserts a bridge between the two.

CORRECTION: such a bridge is NOT the standing bounds_mathcal_E_aL provider obligation — it is strictly stronger and NOT provable: it would bound the uncut-a_L error by an L-free right side, i.e. sup_L 𝓔(□_m; a_L, σ_m) < ∞, which the manuscript never asserts: the print's bounds_mathcal_E_aL lemma is stated at ã, and transports the Dirichlet datum to ã rather than bounding a_L. The print-accurate replacements live in HomSeamFluxCoefficient.lean (seamDom1Flux_of_identification / seamDom2Flux_of_identification, from the honest FluxCorrectedParentIdentification with BOTH sides at ã).

Also NOT carried here: the re-pinned Step-1 moment bound (the anchor's Step-1 factor-moment display is stated at the printed base s; its sibling at s/8 needs the anchor's s-endpoint at s/32 and its p-range at 64 d |log γ| — the machine-traced correction of this file's original 32 d |log γ|: the binding slot is homQuarterOf (homSeamBase) = s/32, so the scaling is exactly ×8, matching the gauge's 16 → 128), and the level chain's absorption of the √2 of the second slot — HomSpineResiduePairing's gap pairing takes its domination at constant one. ofReal_one_add_sq_le_of_const below is the exact arithmetic that sibling has to consume.

1. The two [0,∞] series facts

2. The two carrier comparisons

theorem Algsuperdiff.Section4.Provider.Homogenization.parentTruncatedOne_le_parentTruncatedTwo_half {d : ℕ} (Q : HCPolySupport.TriadicCube d) (n : ℤ) (hn : n ≤ Q.scale) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain Q)) (sigma0 : ℝ) (hsigma0 : 0 < sigma0) (t u : ↑HCPolySupport.FractionalOrder) (htu : ↑u = ↑t / 2) : HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityOneScalar Q n hn a sigma0 hsigma0 t ≤ HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityTwoScalar Q n hn a sigma0 hsigma0 u

THE q-INDEX STEP, AT CONSTANT EXACTLY ONE.

𝓔_{t,∞,1}(□,n; a, σ₀) ≤ 𝓔_{t/2,∞,2}(□,n; a, σ₀): CoarseGraining's q = 1 truncated parent error at order t is below its q = 2 sibling at HALF that order, on the same cube, the same truncation, the same coefficient field and the same scalar comparator.

This is the machine-checked form of the Cauchy--Schwarz step the manuscript performs between the two printed displays. The halving is not a slack: at equal orders the inequality fails.

theorem Algsuperdiff.Section4.Provider.Homogenization.parentTruncatedTwo_le_of_order_le {d : ℕ} (Q : HCPolySupport.TriadicCube d) (n : ℤ) (hn : n ≤ Q.scale) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain Q)) (sigma0 : ℝ) (hsigma0 : 0 < sigma0) (s1 s2 : ↑HCPolySupport.FractionalOrder) {K : ℝ} (hle : ↑s2 ≤ ↑s1) (hK0 : 0 ≤ K) (hK : 1 - 3 ^ (-↑s1 * 2) ≤ K * (1 - 3 ^ (-↑s2 * 2))) : HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityTwoScalar Q n hn a sigma0 hsigma0 s1 ≤ ENNReal.ofReal √K * HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityTwoScalar Q n hn a sigma0 hsigma0 s2

THE ORDER STEP AT q = 2.

𝓔_{s₁,∞,2} ≤ √K · 𝓔_{s₂,∞,2} whenever s₂ ≤ s₁ and the normalization ratio is below K. The scale sum is monotone in the right direction; the constant is purely the ratio c_{s₁,2}/c_{s₂,2} of the two normalizations.

theorem Algsuperdiff.Section4.Provider.Homogenization.parentTruncatedTwo_le_sqrtTwo_half {d : ℕ} (Q : HCPolySupport.TriadicCube d) (n : ℤ) (hn : n ≤ Q.scale) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain Q)) (sigma0 : ℝ) (hsigma0 : 0 < sigma0) (s1 s2 : ↑HCPolySupport.FractionalOrder) (hhalf : ↑s2 = ↑s1 / 2) : HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityTwoScalar Q n hn a sigma0 hsigma0 s1 ≤ ENNReal.ofReal √2 * HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityTwoScalar Q n hn a sigma0 hsigma0 s2

The halving instance of the previous theorem: K = 2 always works, because c_{2s,2} = c_{s,2}(1 + 3^{-2s}) and 3^{-2s} ≤ 1.

3. The re-pinned base exponent

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.homSeamBase {d : ℕ} (M : Section3.ABKModel d) (hs : 0 < homS M) : { s : ℝ // 0 < s }

THE RE-PINNED BASE s' = s/8. EthmB(m) is the printed object at this base exponent: its first 𝓔 factor is then at s'/2 = s/16 and its γ⁵ factor at s'/4 = s/32, which are exactly the two orders the q-index and order steps of sections 1--2 deliver.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.homSeamBase M hs = ⟨Algsuperdiff.Section4.Provider.Homogenization.homS M / 8, ⋯⟩

@[simp]

theorem Algsuperdiff.Section4.Provider.Homogenization.homSeamBase_val {d : ℕ} (M : Section3.ABKModel d) (hs : 0 < homS M) : ↑(homSeamBase M hs) = homS M / 8

theorem Algsuperdiff.Section4.Provider.Homogenization.fluxCorrectedTwoScaleErrorObservableSup_congr_order {d : ℕ} (M : Section3.ABKModel d) (m n : ℤ) {s1 s2 : { s : ℝ // 0 < s }} (h : ↑s1 = ↑s2) : Support.fluxCorrectedTwoScaleErrorObservableSup M m n s1 = Support.fluxCorrectedTwoScaleErrorObservableSup M m n s2

The observable depends on its order slot only through the underlying real.

6. The absorption the level chain still owes

theorem Algsuperdiff.Section4.Provider.Homogenization.ofReal_one_add_sq_le_of_const {E K : ℝ} {Ecar : ENNReal} (hE : 0 ≤ E) (hK : 1 ≤ K) (hdom : ENNReal.ofReal E ≤ ENNReal.ofReal K * Ecar) : ENNReal.ofReal (1 + E ^ 2) ≤ ENNReal.ofReal (K ^ 2) * (1 + Ecar ^ 2)

THE √2 IS FREE. A domination with a constant K ≥ 1 enters the gap leg only through 1 + E², where it costs exactly K². This is the arithmetic a sibling of HomSpineResiduePairing's gap pairing has to consume in order to accept the second domination at √2; nothing else in the level chain sees the constant.