ScaleSumOrdering

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

Step 5's scale sum: the two orderings of the same per-scale data

Nothing here imports that file, and nothing here claims the anchor. Everything below is abstract-real arithmetic: no model, no measure, no carrier occurs.

What is here

The manuscript's Step 5 combines the per-scale data

G_l  =  B · min{1, (γ(D+l))^{1/2}} · 3^{γ(D+l)} ,   D = m − n ,  l = n − j ≥ 0 ,

(B carries the Γ₂-moment constant (K p)^{1/2}, D = m − n) against the geometric scale weight 3^{−s l}. There are two possible orderings, and they are NOT equivalent:

• the ℓ^p (Jensen) ordering ( c_s ∑_l 3^{−s l} G_l^p )^{1/p}, which is what the printed display literally writes -- the weight sits INSIDE the p-th power, so after the p-th root it acts at the rate s/p; and
• the ℓ¹ (Minkowski) ordering ( c_{2s} ∑_l 3^{−s l} G_l^2 )^{1/2}, which is what d.mathcal.E's q = 2 branch offers directly (the scale sum is already outside the p-th power there, so the p/2-th moments may be combined by the triangle inequality in L^{p/2} instead of by Jensen).

This module proves the exact arithmetic of both.

1. minkowskiOrder_scaleSum_le / sqrt_minkowskiOrder_bound_le: in the ℓ¹ ordering the sum is at most γ(36 D + 144/s), i.e. its square root is at most 12 √γ (√D + s^{−1/2}) -- exactly the value the manuscript's Step 5 asserts for its display, with an explicit absolute constant.
2. anchorScalar_rpow_lt_jensenOrder_weighted_term (with jensenOrder_term_le_printed_summand for faithfulness to the printed summand): in the ℓ^p ordering ONE term of the same sum already exceeds the p-th power of the anchor's own scalar C √γ s^{−1} at D = 0 and at the top p = C^{-1} γ^{-1} s of the anchor's p-range, for C > 72. Since the anchor's statement at a constant C₀ implies it at every C ≥ C₀ (all three parameter ranges shrink and the right-hand side grows with C), this settles the ℓ^p ordering for every constant.

The two together locate the discrepancy exactly: it is the placement of the p-th root relative to the scale sum, and nothing else. The maximising scale in 2 is l ≈ p/s, where 3^{−s l/p} ≈ 1/3 while (γ l)^{1/2} ≈ (γ p/s)^{1/2}; the ℓ¹ ordering instead sees the geometric weight at full strength and is maximised at l ≈ 1/s, which is the source of the printed s^{−1/2}.

References

• ABK26, l.bounds.mathcal.E.aL, Step 5; d.mathcal.E; e.mathcalE.infty.to.q.

1. Two elementary transcendental estimates

theorem Algsuperdiff.Section4.Provider.BoundsEaL.half_le_one_sub_rpow_three_neg {u : ℝ} (hu : 0 < u) (hu1 : u ≤ 1) : u / 2 ≤ 1 - 3 ^ (-u)

The geometric discount is at least u/2 on 0 < u ≤ 1: u/2 ≤ 1 − 3^{−u}. This is the only place a logarithm enters the ℓ¹ ordering.

2. The ℓ¹ (Minkowski) ordering: the manuscript's own value

theorem Algsuperdiff.Section4.Provider.BoundsEaL.minkowskiOrder_scaleSum_le {s gam D : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (hgam : 0 ≤ gam) (h4gam : 4 * gam ≤ s) (hD : 0 ≤ D) (hgamD : gam * D ≤ 1) : (1 - 3 ^ (-(2 * s))) * ∑' (l : ℕ), 3 ^ (-(s * ↑l)) * (gam * (D + ↑l) * 3 ^ (2 * gam * (D + ↑l))) ≤ gam * (36 * D + 144 / s)

The scale sum in the ℓ¹ ordering.

For 0 < s ≤ 1, 4γ ≤ s, D ≥ 0 and γ D ≤ 1 (the anchor's own binder m ≤ n + γ^{-1}),

(1 − 3^{−2s}) · ∑_{l ≥ 0} 3^{−s l} · γ(D+l) · 3^{2γ(D+l)}  ≤  γ (36 D + 144/s) .

The summand is the square of the second summand's per-scale majorant min{1,(γ(D+l))^{1/2}} 3^{γ(D+l)} with the min discarded (min ≤ its second argument), and the prefactor is the q = 2 geometric discount 𝔠_{2s}.

3. The ℓ^p (Jensen) ordering: one term already overshoots