PerCubeSlotThird

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

Step 5's third summand, evaluated at the anchor's scalar

What this module does

PerCubeFirstThird.exists_lintegral_rpow_step3ThirdTerm_le supplies the third summand's q-th moment at the SYMBOLIC majorant C ( σ_m^{-1} + R_{B5}(4q) )² R_{B6a}(4q)². This module evaluates it:

( σ_m^{-1} + R_{B5}(4q) ) R_{B6a}(4q)  =  O( √q √γ ) ,

by bullet (B3) at BOTH σ indices (PerCubeSlotCommon), so the third summand's majorant is O(C q γ) -- uniformly in the descendant scale, which is exactly why Step 5 calls this summand straightforward. The anchor's own first slot K p γ s^{-2} dominates it, since s ≤ 1/4.

References

• ABK26, l.bounds.mathcal.E.aL, Step 4 bullets (B3)/(B5)/(B6a), Step 5.

1. Three arithmetic shorthands

theorem Algsuperdiff.Section4.Provider.BoundsEaL.sqrt_four_eq_two : √4 = 2

theorem Algsuperdiff.Section4.Provider.BoundsEaL.sqrt_four_mul (q : ℝ) : √(4 * q) = 2 * √q

theorem Algsuperdiff.Section4.Provider.BoundsEaL.sqrt_mul_sqrt_sq {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : (√x * √y) ^ 2 = x * y

2. The regime bridge

theorem Algsuperdiff.Section4.Provider.BoundsEaL.gamma_regime_of_cstar_scaled {C cst gam : ℝ} (h : gam ≤ (C * cst⁻¹)⁻¹ ^ 10) : gam ≤ C⁻¹ ^ 10 * cst ^ 10

The anchor's own regime γ ≤ C^{-10} at the constant C · c⋆^{-1} IS the Section-3 regime γ ≤ C^{-10} c⋆^{10}. This is where the anchor's freedom to choose its constant A c⋆ (its binder order) is used.

3. The third summand at the anchor's first slot

theorem Algsuperdiff.Section4.Provider.BoundsEaL.exists_lintegral_rpow_step3ThirdTerm_slot (d : ℕ) (cstar : ℝ) (hcstar : 0 < cstar) : ∃ (Creg : ℝ) (A : ℝ), 0 < Creg ∧ 0 < A ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ Creg⁻¹ ^ 10 → M.gamma ≤ 1 / 8 → ∀ (Cd : ℝ), 0 ≤ Cd → ∀ (m : ℤ) (R : HCPolySupport.TriadicCube d), R.scale ≤ m → ∀ (q : ℝ), 1 ≤ q → 8 * q ≤ M.gamma⁻¹ → ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (step3ThirdTerm Cd M m R omega (lFreeGradSlot m (tailSeriesGauge m) R omega)) ^ q ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (Cd * A * (q * M.gamma)) ^ q

The third summand, evaluated.

∫⁻ (step3ThirdTerm)^q ≤ (ofReal (C_d A q γ))^q, uniformly in the descendant scale. The moment range hypothesis 8q ≤ γ^{-1} is the anchor's own p ≤ C^{-1}γ^{-1}s read at q = p/2; no other restriction on p is used.