HomProviderBSeamClose

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

Theorem B, §4.5: the seam base and the enlarged Y, prepared

What this file supplies

The print-accurate ã chain runs at

  sb = homSeamBase M hs = s/8      (the authorized re-pin),
  Y  = seamEnlargedY M m C_top Y₀  (the authorized index enlargement),

and this file supplies the three facts that base needs: the measurability of the enlarged Y slot, the reciprocal-range arithmetic, and the a.e. finiteness of the seam carrier ethmB there. The Theorem-C edge is read at 2p exactly as homY_moment_bound_of_gamma_le states it, the 4p boost being paid inside the seam display.

1. Measurability of the enlarged Y

theorem Algsuperdiff.Section4.Provider.Homogenization.measurable_seamEnlargedY {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (Ctop : ℝ) {Y0 : Section3.Cutoff.CutoffSample d → ENNReal} (hY0 : Measurable Y0) : Measurable (seamEnlargedY M m Ctop Y0)

The enlarged Y slot is measurable: a constant times the Theorem-C minimal-scale factor times two of the own measurable observables.

3. The a.e. finiteness of the carrier at the seam base

theorem Algsuperdiff.Section4.Provider.Homogenization.one_le_reciprocal_range {C gam : ℝ} (hC : 0 < C) (hg : 0 < gam) (hg1 : gam < 1) (hL : 0 < |Real.log gam|) (hgC : gam ≤ (4 * C)⁻¹ ^ 2) : 1 ≤ C⁻¹ * gam⁻¹ * |Real.log gam|⁻¹

p = 1 lies inside a reciprocal p-range once γ ≤ (4C)⁻². This is HomSpineFinalWitness's own step, isolated.

theorem Algsuperdiff.Section4.Provider.Homogenization.ae_ethmB_seam_ne_top (d : ℕ) (cstar : ℝ) (hcstar : 0 < cstar) {Cst Cgap Ctop : ℝ} (hCst : 1 ≤ Cst) (hCgap : 0 ≤ Cgap) (hCtop : 0 ≤ Ctop) : ∃ (gamma0 : ℝ), 0 < gamma0 ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (X : Section3.Cutoff.CutoffSample d → ℕ∞), Measurable X → (∀ (N : ℕ), ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | ↑N ≤ X omega} ≤ ENNReal.ofReal (Cst * Real.exp (-((1 - homAlpha M) ^ 2 * (↑N - Cst)) / (Cst * M.gamma)))) → ∀ (hs : 0 < homS M) (m : ℤ), ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ethmB M Cgap (seamEnlargedY M m Ctop (homMinimalScaleFactor (1 - homAlpha M) X)) m (homN M m) (homSeamBase M hs) omega ≠ ⊤

THE EthmB(m) CARRIER IS a.e. FINITE AT THE SEAM BASE AND THE ENLARGED Y.

The p = 1 instance of the seam display. This is the input of the ã bundle's hfin slot that the residue cannot see (it needs the Theorem-C tail), so it is produced here and threaded to the residue by the assembly.