HomStepOneDisplay

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

Theorem B, §4.5, Step 1: the printed display the 𝓔 estimate

The target

The Step-1 conclusion, in the ADOPTED form of (fix 2):

𝔼[ EthmB(m)^p ]^{1/p}  ≤  C ( √p + √|log γ| ) √γ (log γ)²

for p ∈ [1, C⁻¹ γ⁻¹ |log γ|⁻¹], in the lintegral normal form ∫⁻ EthmB^p ≤ (ofReal R)^p.

The √|log γ| summand is NOT cosmetic: it is exactly the anchor's own lower moment endpoint q ≥ 2 d s'⁻¹, which at the §4.5 exponents reads q ≥ 8 d |log γ|. The assembly below evaluates the anchor at q = max(4p, 8d|log γ|) and √q ≤ 2√p + √(8d)√|log γ| is where the second summand comes from. The printed √p alone is unreachable below p ≈ d|log γ|; this module states the reachable bound.

The Cgap-explicit constant

The produced constant is C₀ (1 + C_gap), LINEAR in the Step-3 gap constant C_gap of EthmB's second summand, with C₀ = C₀(d, c⋆) independent of it. Keeping C_gap a free parameter rather than fixing it here is the honest reading: the source's C in C γ⁵ is pinned by Step 3, not by Step 1, and (the Step-3 rescaling of the witness) then costs exactly one more factor, absorbed by lintegral_rpow_const_mul_le.

The conditional set (exactly one edge)

hY — the Markov/Γ₁ moment 𝔼[(3^{(1-α)X_m(α)})^{2p}] ≤ 2^{2p} of the Theorem-C minimal-scale factor, transcribed as a named hypothesis at the single exponent it is consumed at. Theorem C is a declared dependency of the Step 1 (the moment bound). NOTHING else is assumed.

1. Elementary square-root facts

theorem Algsuperdiff.Section4.Provider.Homogenization.sqrt_max_le {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) : √(max a b) ≤ √a + √b

theorem Algsuperdiff.Section4.Provider.Homogenization.sqrt_four : √4 = 2

theorem Algsuperdiff.Section4.Provider.Homogenization.sqrt_le_one_of_le_one {x : ℝ} (h : x ≤ 1) : √x ≤ 1

2. The purely algebraic collapse

theorem Algsuperdiff.Section4.Provider.Homogenization.display_collapse {A D L S G W gam Cgap C0 : ℝ} (hA : 0 ≤ A) (hD : 0 ≤ D) (hL : 4 ≤ L) (hS : 3 ≤ S) (hG : 0 ≤ G) (hW : 0 ≤ W) (hCgap : 0 ≤ Cgap) (hWDS : W ≤ D * S) (hSG : S * G ≤ 2) (hgam5 : gam ^ 5 ≤ G) (h1 : 2 * A * D * (1 + 2 * A * D) ≤ C0) (h2 : 1 + 4 * A ^ 2 * D ^ 2 ≤ C0) : L * (2 * (A * L * W * G * (1 + A * W * G))) + Cgap * gam ^ 5 * (1 + (A * L * W * G) ^ 2) ≤ C0 * (1 + Cgap) * S * G * L ^ 2

The Step-1 numeric collapse, over abstract reals.

W is √q, S is √p + √|log γ|, G is √γ, L is |log γ|, A the anchor's factor constant and D = 2 + √(8d) the √max loss. Nothing γ-dependent is hidden: every hypothesis is displayed.