StepThreeDThree #

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

Step 3 of the kicking lemma: the two channels and the `D₃` conclusion #

ABK26, §4.2, l.minimal.scale.sep, Step 3. After the rearrangement (StepThreeRearrange) the manuscript's D₃ sum over the window splits into two channels, both weighted by the lattice maxima G_i^k = 3^{(2−γ)i}max_{z ∈ 3^iℤ^d ∩ □_k}‖j_i‖_{W^{2,∞}(z+□_i)}:

in-window    (i ∈ [n,m])   :  V_i  = Σ_{k=i}^m 3^{−α(k−i)} G_i^k
below-window (i = n−1−r)   :  H_r  = Σ_{k=n}^m 3^{−α(k−n)} G_{n−1−r}^k

(the in-window channel is ABK26, the below-window channel)

with α = s/4, and the total is Σ_{i=n}^m V_i + Σ_{r≥0} 3^{−α(r+1)} H_r.

This module proves the two Γ₂ tails and closes the window average.

The two closures, at the manuscript's own constants #

Both channels are e.Gamma.sigma.triangle over a finite k-range applied to the lattice maxima, whose amplitudes carry the e.maxy.bound penalty C(k+1−i)^{1/2} (LayerBrackets.isBigOWith_hessLatticeMax). The two deterministic amplitude sums are the proved Algsuperdiff.Probability.sum_windowAmp_le (Cs^{−3/2}) and Algsuperdiff.Probability.sum_headAmp_le (per-depth, growing like √r), and the below-window recombination is the proved per-layer geometric closure Algsuperdiff.Probability.weightedTsum_isBigOWith_perLayer at Algsuperdiff.Probability.tsum_weight_step3HeadAmp_le. The resulting amplitudes are byte-identical to step3WindowAmp and step3TailAmp: the sharp Cauchy--Schwarz closure is what makes them s^{−3/2} and s^{−5/2} rather than s^{−2} and s^{−3}.

The `D₃` bound: the honest `s`-exponent #

At α = s/4 the two channel amplitudes and the depth-swap constant are (machine-checked in §6 below, 0 < s ≤ 1/2)

K₀ := 3^{α}(1−3^{−α})⁻¹        ≤ 16 s^{−1}
K  := step3WindowAmp C (s/4)   ≤ C' s^{−3/2}
b  := step3TailAmp   C (s/4)   ≤ C'' s^{−5/2}

so the window average of the prefactor-free D₃ sum obeys

avsum ≤ K₀·C_mom·K  +  𝒪_{Γ₂}( C(K₀K + K₀b)(m−n)^{−1/2} )
      ≤ C s^{−5/2}  +  𝒪_{Γ₂}( C s^{−7/2}(m−n)^{−1/2} ) .

Multiplying by the printed prefactor c⋆^{−1/2}s^{−1}γ^{1/2} of D₃ gives the deterministic level C c⋆^{−1/2}s^{−7/2}γ^{1/2} — the printed one — and the fluctuation scale C c⋆^{−1/2}s^{−9/2}γ^{1/2}(m−n)^{−1/2}, which is one power of s weaker than the printed s^{−7/2} in e.D3k.kicked. The below-window channel is the culprit: it enters the average with the factor (m−n+1)^{−1} rather than (m−n+1)^{−1/2}, and s^{−9/2}(m−n)^{−1} is not below s^{−7/2}(m−n)^{−1/2} unless m−n ≥ s^{−2}, which the lemma does not assume (it assumes only n < m). A Cesàro reconciliation therefore does not rescue the printed exponent, and the honest fluctuation exponent is s^{−9/2}.

References #

ABK26, l.minimal.scale.sep Step 3; e.D3k.kicked; e.maxy.bound.

StepThreeDThree #

Step 3 of the kicking lemma: the two channels and the D₃ conclusion #

The two closures, at the manuscript's own constants #

The D₃ bound: the honest s-exponent #

References #

1. The Step-3 weight and the per-cube amplitude #

2. The two channels #

3. The in-window Γ₂ tail #

4. The below-window Γ₂ tails #

5. The D₃ bound: the window average of the two channels #

6. The audit: the honest s-exponents at α = s/4 #

7. The two envelopes as explicit powers of s #

Step 3 of the kicking lemma: the two channels and the `D₃` conclusion #

The `D₃` bound: the honest `s`-exponent #

3. The in-window `Γ₂` tail #

4. The below-window `Γ₂` tails #

5. The `D₃` bound: the window average of the two channels #

6. The audit: the honest `s`-exponents at `α = s/4` #

7. The two envelopes as explicit powers of `s` #