StepOneAssembly

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

The D₁ half of e.kick.Dees.Dees

ABK26, §4.2, the end of Step 1 of l.minimal.scale.sep. Summing the Step-1 pointwise estimate over the window and rearranging (e.D1k.Larry) gives

avsum_{k=n}^m D₁(k)
  ≤ C s^{1/2} · [ 𝔠 · avsum_{j=n}^m X_j  +  (min{N, 𝔠}/N) · ∑_{p ≥ 0} 3^{−¼sp} X_{n−1−p} ]

with N = m − n + 1 and 𝔠 = (1 − 3^{−¼s})^{−1} ≤ 8/s. The window average is closed by the r-dependent Cesàro engine (p.concentration) and the head by the countable Γ₂ triangle inequality; adding the two gives the D₁ half of e.kick.Dees.Dees:

avsum_{k=n}^m D₁(k) ≤ C c⋆^{−1}s^{−7/2}√γ + 𝒪_{Γ₂}(C c⋆^{−1}s^{−7/2}√γ N^{−1/2}) .

Where the printed s^{−7/2} comes from

The two legs land at different s-powers:

• the window leg gives s^{1/2}·𝔠·A₁ ≍ s^{1/2}·s^{−1}·s^{−5/2} = s^{−3};
• the head leg gives s^{1/2}·√𝔠·(𝔠 A₁) ≍ s^{1/2}·s^{−1/2}·s^{−1}·s^{−5/2} = s^{−7/2}.

So the printed s^{−7/2} of e.kick.Dees.Dees is attained only at the head, and only if the head's window coefficient is read at the sharp min{N,𝔠}/N ≤ √𝔠·N^{−1/2} (Probability.min_div_le_sqrt_mul_rpow).

The one-shot engine Probability.cesaroAvg_isBigO_of_rDependent_with_tail cannot deliver this: it absorbs the boundary term through 1/N ≤ N^{−1/2}, which loses exactly the √N that the sharp min-coefficient provides, and the head then costs s^{−4} (with the N^{−1/2} decay) or s^{−7/2} (without it). The assembly below therefore uses the plain engine cesaroAvg_isBigO_of_rDependent for the window leg and applies the sharp min-coefficient to the head leg by hand before adding the two Γ₂ bounds — which is exactly what the manuscript does ("adding the previous two displays").

The r-dependence is read at r = d + 2

This module instantiates r = d + 2, which clears the count for every d (three_pow_dim_clears) and keeps the output constant a function of d alone. It is not the minimal admissible r (the minimal one is logarithmic in d); the cost of the non-minimal choice is the factor √(r+1) inside rDepEngineConst, i.e. a d-only constant.

Main results

• three_pow_dim_clears — the separation count at r = d + 2.
• exists_stepOne_d1_bound — the D₁ half of e.kick.Dees.Dees.

References

• ABK26, l.minimal.scale.sep, Step 1; e.D1k.Larry; p.concentration.

1. The separation count at r = d + 2

theorem Algsuperdiff.Section4.Provider.MinimalScale.three_pow_dim_clears (d : ℕ) : 3 + 2 * 3 ^ (1 - 2) * √↑d ≤ 3 ^ (d + 2)

The r-dependence count is cleared at r = d + 2, for every d. The proved bridge asks for 3 + 2·3^{1−2}·√d ≤ 3^r; at r = d+2 this follows from √d ≤ 1 + d and 1 + 2d ≤ 3^d. No dimension restriction is introduced.

2. The endpoint

theorem Algsuperdiff.Section4.Provider.MinimalScale.exists_stepOne_d1_bound (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10 → ∀ (s : { s : ℝ // 0 < s }), 8 * M.gamma ≤ ↑s → ↑s ≤ 1 / 4 → ∀ (Ccg : ℝ) (n m : ℤ), n ≤ m → ∃ (Xdet : Section3.Cutoff.CutoffSample d → ℝ) (Xfluc : Section3.Cutoff.CutoffSample d → ℝ), (∀ (omega : Section3.Cutoff.CutoffSample d), Probability.cesaroAvg (fun (k : ℤ) => (dOne M Ccg s k omega).toReal) n m ≤ Xdet omega + Xfluc omega) ∧ (∀ (omega : Section3.Cutoff.CutoffSample d), Xdet omega ≤ C * ((Section3.Disorder.cstar M)⁻¹ * (√↑s ^ 7)⁻¹ * √M.gamma)) ∧ HCPolySupport.IndependentSums.IsBigO (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) Xfluc (C * ((Section3.Disorder.cstar M)⁻¹ * (√↑s ^ 7)⁻¹ * √M.gamma) * ↑(m - n + 1) ^ (-1 / 2))