Step1Assembly

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

The two interchanges and the centre closure of Step 1

ABK26, Section 4.1, e.mathcalE.annular.decomp.pre, Step 1. Step1.annularDecompPre_of reduces the Step-1 shape to three caller obligations: hgrid (the cover split), hcov (the cover interchange) and hcen (the resummed centre term). This module proves the last two abstractly, in the weight the manuscript uses, so that the concrete producer only has to supply the geometry.

What is proved

• tsum_annFam_row -- the n-row of the guarded annular family is a finite sum over j ∈ [n+1, m]. This is the manuscript's interchange Σ_{n ≤ m} Σ_{j=n+1}^m = Σ_{j ≤ m} Σ_{n ≤ j-1}, and it is an identity, so the cover leg costs C_cov = 1 with no loss.
• annDouble_eq_tsum_rows, summable_annFam_rows -- the transposed iterated form of the annular double sum, and the summability of its rows.
• tsum_centre_le -- the centre closure. Given only the one-step subadditivity recursion Jcen n ≤ A n + ρ^{-1} Jcen (n-1) and a uniform bound on both families, the weighted centre sum is at most 3 times the diagonal slice of the annular double sum. C_cen = 3 is an absolute numeral on the printed window s ≤ 1/4, ρ ≥ 9.

The centre closure, and why it does not iterate

The manuscript iterates the one-step recursion into an infinite series and then computes Σ_{n=k+1}^m 3^{-2s(m-n) - d(n-1-k)} ≤^{-2s(m-k)}. The same constant is obtained here without any iteration: the weighted centre sum S is (the uniform bound plus the geometric weight), the weight satisfies w(n) = 3^{2s} w(n-1) exactly, and the ℤ-shift is a tsum bijection, so summing the one-step recursion gives

S ≤ T + 3^{2s} ρ^{-1} S ,

with T the weighted diagonal sum. On s ≤ 1/4 and ρ ≥ 9 the contraction factor is at most 7/36, whence S ≤ (36/29) T, and T = 3^{2s} times the diagonal slice in the spelling Step1.annularDecompPre_of expects. Since (36/29)·(7/4) = 63/29 < 3, C_cen = 3 closes it. This is exactly the geometric factor 3^{2s}(1 - 3^{2s-d})^{-1} of the centre interchange, evaluated with slack on the printed window; the honest convergence condition 2s < d is what s ≤ 1/4 < 1 ≤ d/2 supplies.

The tolerance

The printed W(p) = 3^{-dp} at C₀ = 1 -- which is what the one-step recursion at ρ = 3^d produces -- sits far inside that condition; the numerals 7/4, 1/9, 7/36, 36/29, 3 above are the explicit margin.

References

• ABK26, (Step 1); (the cover interchange); (the centre resummation).

Part A -- the lower-half reindexing n = m − u

theorem Algsuperdiff.Section4.Provider.Annular.summable_guarded_iff {m : ℤ} {f : ℤ → ℝ} (h0 : ∀ (n : ℤ), ¬n ≤ m → f n = 0) : (Summable fun (u : ℕ) => f (m - ↑u)) ↔ Summable f

A family on ℤ supported on {n ≤ m} is summable iff its n = m − u reindexing is.

theorem Algsuperdiff.Section4.Provider.Annular.tsum_guarded_eq {m : ℤ} {f : ℤ → ℝ} (h0 : ∀ (n : ℤ), ¬n ≤ m → f n = 0) : ∑' (u : ℕ), f (m - ↑u) = ∑' (n : ℤ), f n

The corresponding sum identity.

theorem Algsuperdiff.Section4.Provider.Annular.summable_guarded_geom {s B : ℝ} {m : ℤ} {F : ℤ → ℝ} (hs0 : 0 < s) (hF0 : ∀ (n : ℤ), 0 ≤ F n) (hFB : ∀ n ≤ m, F n ≤ B) : Summable fun (n : ℤ) => if n ≤ m then 3 ^ (-(2 * s * ↑(m - n))) * F n else 0

The guarded geometric criterion. A nonnegative family that is uniformly bounded on {n ≤ m} is summable against the Step-1 weight 3^{−2s(m−n)}.

Part B -- the cover interchange

theorem Algsuperdiff.Section4.Provider.Annular.tsum_annFam_row (m : ℤ) (h : ℤ → ℤ → ℝ) (n : ℤ) : ∑' (j : ℤ), annFam m h (j, n) = if n ≤ m then ∑ j ∈ Finset.Icc (n + 1) m, h j n else 0

The n-row of the guarded annular family. For n ≤ m the row is the finite sum over the annulus indices j ∈ [n+1, m]; for n > m it vanishes. The manuscript's interchange of the order of summation is exactly this identity together with annDouble_eq_tsum_rows.

theorem Algsuperdiff.Section4.Provider.Annular.annDouble_eq_tsum_rows {m : ℤ} {h : ℤ → ℤ → ℝ} (hsum : Summable (annFam m h)) : annDouble m h = ∑' (n : ℤ) (j : ℤ), annFam m h (j, n)

The annular double sum, summed over scales first.

theorem Algsuperdiff.Section4.Provider.Annular.summable_annFam_rows {m : ℤ} {h : ℤ → ℤ → ℝ} (hsum : Summable (annFam m h)) : Summable fun (n : ℤ) => ∑' (j : ℤ), annFam m h (j, n)

The rows of a summable guarded annular family are summable in the scale.

Part C -- the two numerals of the centre closure

theorem Algsuperdiff.Section4.Provider.Annular.threeRpow_two_mul_le {s : ℝ} (hs14 : s ≤ 1 / 4) : 3 ^ (2 * s) ≤ 7 / 4

3^{2s} ≤ 7/4 on the printed window s ≤ 1/4.

Part D -- the centre closure

theorem Algsuperdiff.Section4.Provider.Annular.tsum_centre_le {s rho B : ℝ} {m : ℤ} {Jcen A : ℤ → ℝ} (hs0 : 0 < s) (hs14 : s ≤ 1 / 4) (hrho : 9 ≤ rho) (hJcen0 : ∀ (n : ℤ), 0 ≤ Jcen n) (hA0 : ∀ (n : ℤ), 0 ≤ A n) (hJcenB : ∀ n ≤ m, Jcen n ≤ B) (hAB : ∀ n ≤ m, A n ≤ B) (hstep : ∀ (n : ℤ), Jcen n ≤ A n + rho⁻¹ * Jcen (n - 1)) : (∑' (n : ℤ), if n ≤ m then 3 ^ (-(2 * s * ↑(m - n))) * Jcen n else 0) ≤ 3 * ∑' (u : ℕ), 3 ^ (-(2 * s * ↑(m - (m - ↑u - 1)))) * A (m - ↑u)

The Step-1 centre closure, at the absolute constant 3.

Jcen is the centre leg J(□_n) and A n the annulus maximum at step n (the manuscript's max_{z' ∈ 3^{n-1}ℤ^d ∩ (□_n ∖ □_{n-1})} J(z' + □_{n-1})). The only structural input is the one-step subadditivity recursion hstep; the uniform bounds make the weighted sums finite, which is what lets the recursion be summed instead of iterated.

The conclusion is exactly the hcen slot of Step1.annularDecompPre_of at Ccen = 3, once A is instantiated at fun n ↦ Jann n (n-1).