HomProviderBAssembly

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

Theorem B, §4.5: the Theorem-B assembly off Theorem C

What this file supplies

exists_regularity_minimalScale — the Theorem-C export re-shaped at the §4.5 parameter web: at α:= homAlpha M = 1 - s/2 the minimal scale X_m(α) exists with a tail at ONE model-independent constant C⋆ ≥ 1, together with the per-ω energy-density display. This produces exactly the htail hypothesis of the §4.5 spine's close step (the Cst slot) plus the display the residual step consumes. It is UNCONDITIONAL.

Two arithmetic facts carry it: the printed observation in the paper that α ∈ (0, 1 - C₀ γ^{1/2}] for small γ (homAlpha_le_one_sub here, off absLog_mul_sqrt_le), and the monotonicity of the printed tail profile in its own constant (regTail_mono_const).

1. The Theorem-C display, transcribed

def Algsuperdiff.Section4.Provider.Homogenization.RegularityDisplayAt {d : ℕ} (M : Section3.ABKModel d) (Creg alpha : ℝ) (m : ℤ) (X : Section3.Cutoff.CutoffSample d → ℕ∞) (omega : Section3.Cutoff.CutoffSample d) : Prop

The per-ω conclusion of anomalous_regularity, byte for byte from the frozen statement's ∀ᵐ ω body, with the root's C and alpha and its minimal scale X as parameters.

This is the ONLY thing the §4.5 Step-2 energy slot consumes from Theorem C.

Equations

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

2. The two arithmetic facts of the re-shaping

theorem Algsuperdiff.Section4.Provider.Homogenization.homAlpha_le_one_sub {d : ℕ} {M : Section3.ABKModel d} {Creg : ℝ} (hCreg : 0 < Creg) (hg1 : M.gamma < 1) (hgle : M.gamma ≤ (8 * Creg)⁻¹ ^ 4) : homAlpha M ≤ 1 - Creg * √M.gamma

The printed observation, formalized: at the §4.5 web α = 1 - s/2 sits inside Theorem C's admissible range α ≤ 1 - C₀ √γ once γ ≤ (8C₀)⁻⁴.

The only ingredient is |log γ|√γ ≤ 4 γ^{1/4} (absLog_mul_sqrt_le): the printed "if γ is sufficiently small" made explicit.

theorem Algsuperdiff.Section4.Provider.Homogenization.regTail_mono_const {K K' a gamma : ℝ} (N : ℕ) (hK : 0 < K) (hKK' : K ≤ K') (ha : 0 ≤ a) (hgamma : 0 < gamma) : K * Real.exp (-(a * (↑N - K)) / (K * gamma)) ≤ K' * Real.exp (-(a * (↑N - K')) / (K' * gamma))

The printed tail profile is monotone in its own constant.

K ↦ K exp(-(a(N-K))/(Kγ)) = K exp((a/γ)(1 - N/K)) increases in K > 0 for every N ≥ 0, so Theorem C's tail at its own C implies the spine's tail at any C⋆ ≥ C. This is what lets the spine's Cst slot be filled by max 1 C.

3. Theorem C, re-shaped at the §4.5 web

theorem Algsuperdiff.Section4.Provider.Homogenization.exists_regularity_minimalScale (d : ℕ) (cstar : ℝ) (hcstar : 0 < cstar) : ∃ (Cst : ℝ) (Creg : ℝ) (gamma0 : ℝ), 1 ≤ Cst ∧ 0 < Creg ∧ 0 < gamma0 ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (m : ℤ), ∃ (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)))) ∧ ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), RegularityDisplayAt M Creg (homAlpha M) m X omega

THE MINIMAL SCALE, AT THE §4.5 PARAMETER WEB.

The anomalous_regularity read at α:= homAlpha M = 1 - s/2: one model-independent C⋆ ≥ 1 and one threshold γ₀ > 0 such that for every model and every scale m the minimal scale X exists, is measurable, has the spine's own tail profile at C⋆, and carries the per-ω energy-density display.

htail of the §4.5 spine's close step is exactly the second conjunct.