HomSeamEnergyFinitenessCuts

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

The three finiteness cuts of the enlarged-Y top-scale item

What this file supplies

HomSeamEnergySlotAssembly.htop_seamEnlargedY carries three a.e. cuts — the 𝓔-suprema at the honest Step-2 indices t/2 = 1/8, t = 1/4 and at the printed 1/4 are not ⊤. They are DISCHARGED here off branches 2, 4 and 5 of HomStepOneSeamAnchor.exists_ethmB_seam_factor_moments, read at the boosted exponent q = 64 d |log γ|, under the same γ-gate the seam display uses.

Nothing analytic is added: a finite q-moment of a [0,∞]-valued observable makes the observable finite almost surely.

1. A finite moment kills the value ⊤

theorem Algsuperdiff.Section4.Provider.Homogenization.ae_ne_top_of_rpow_moment {d : ℕ} (M : Section3.ABKModel d) {F : Section3.Cutoff.CutoffSample d → ENNReal} (hF : Measurable F) {q c : ℝ} (hq : 0 < q) (hmom : ∫⁻ (omega : Section3.Cutoff.CutoffSample d), F omega ^ q ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal c ^ q) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), F omega ≠ ⊤

A finite q-moment at a positive exponent makes a [0,∞]-valued observable almost surely finite.

2. THE THREE CUTS

theorem Algsuperdiff.Section4.Provider.Homogenization.ae_seam_quarter_errors_ne_top (d : ℕ) [NeZero d] (cstar : ℝ) (hcstar : 0 < cstar) : ∃ (gamma0 : ℝ), 0 < gamma0 ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → 0 < homS M → ∀ (m : ℤ), ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), Support.fluxCorrectedTwoScaleErrorObservableSup M m m ⟨1 / 4 / 2, ⋯⟩ omega ≠ ⊤ ∧ Support.fluxCorrectedTwoScaleErrorObservableSup M m m ⟨1 / 4, seamQuarterPos⟩ omega ≠ ⊤ ∧ Support.fluxCorrectedTwoScaleErrorObservableSup M m m homQuarter omega ≠ ⊤

THE THREE 𝓔-FINITENESS CUTS OF THE ENLARGED Y, DISCHARGED.

At every model below one explicit threshold and at every scale, the two honest Step-2 error indices 1/8, 1/4 and the printed index 1/4 have almost surely finite sup_{L ≥ m} observables. These are exactly the three ≠ ⊤ hypotheses of HomSeamEnergySlotAssembly.htop_seamEnlargedY.