KickArith

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

Arithmetic for the Step-1 annular kick family

ABK26, §4.2, Step 1 of l.minimal.scale.sep. Two of the manuscript's Step-1 moves are pure real arithmetic that the printed text performs silently, and both are load-bearing for the amplitudes:

• the geometric closures. The union-bound penalties of the lattice annulus are (j−i+1)^{1/σ}, i.e. √(j−i+1) on the Γ₂ lane and (j−i+1)² on the Γ_{1/2} lane. Summed against the §4.2 weight 3^{−½s(j−i)} these give s^{−3/2} and s^{−3}. The √ closure is the sharp one — the crude √(r+1) ≤ r+1 gives s^{−2} and does not reproduce the printed s^{−5/2} — and is the proved Probability.tsum_threePow_neg_sqrt_le; its (r+1)² companion is proved here, and geomTailConst_le converts both closure constants into explicit powers of s.

• the absorptions. The s-powers picked up on the Γ_{1/2} lane must disappear into the exponential, because prints the amplitude C exp(−C^{−1}c⋆³γ^{−1}) with no power of s in front. The manuscript says only "for C chosen sufficiently large". inv_cube_mul_exp_le performs the s^{−3} absorption on the window s ≥ 8γ, and exp_neg_eighth_le_sqrt performs the absorption the Step-1 collapse needs, namely that the fourth root of the exponentially small amplitude is below the Γ₂ amplitude C c⋆^{−1}s^{−5/2}√γ. Both consume the regime γ ≤ C^{−10}c⋆^{10} through the single lemma pow_le_expArg_mul, which reads the regime as a lower bound on the exponent C^{−1}c⋆³γ^{−1}. Without such a lower bound the absorbed prefactor would carry c⋆^{−9}, which is not a dimensional constant: this is exactly where the regime is used.

The regime, honestly

The absorptions are proved from γ ≤ C^{−10}c⋆^{10}, which is the enclosing lemma's own printed hypothesis and is also what the proved producer of the per-cube two-term display carries.

Why there is no nlinarith

Every statement here involves Real.exp, Real.log, Real.sqrt or Real.rpow. All transcendental content is concentrated in pow_mul_exp_neg_half_le (xⁿe^{−x/2} ≤ (2n)ⁿ, itself only x ≤ eˣ raised to the n-th power); after that every step is polynomial and closed by linarith only, field_simp or ring. The collapse absorption squares both sides, which removes every root before any arithmetic happens.

References

• ABK26, l.minimal.scale.sep, (the lemma's own hypotheses), Step 1.

1. Two numerical facts

theorem Algsuperdiff.Section4.Provider.MinimalScale.one_lt_log_three : 1 < Real.log 3

theorem Algsuperdiff.Section4.Provider.MinimalScale.sqrt_three_le_two : √3 ≤ 2

2. The geometric closure constant is at most 2/α

theorem Algsuperdiff.Section4.Provider.MinimalScale.half_le_three_rpow_neg {alpha : ℝ} (halpha : alpha ≤ 1 / 2) : 1 / 2 ≤ 3 ^ (-alpha)

3^{−α} ≥ ½ for α ≤ ½: the elementary bound that turns the exact closure constant (1 − 3^{−α})⁻¹ into the explicit 2/α.

theorem Algsuperdiff.Section4.Provider.MinimalScale.geomTailConst_le {alpha : ℝ} (h0 : 0 < alpha) (h1 : alpha ≤ 1 / 2) : Probability.geomTailConst alpha ≤ 2 / alpha

(1 − 3^{−α})⁻¹ ≤ 2/α for 0 < α ≤ ½. The conversion of the proved closure constants into explicit powers of the window parameter: at α = ½s it reads geomTailConst (½s) ≤ 4/s.

3. The (r+1)² geometric closure

theorem Algsuperdiff.Section4.Provider.MinimalScale.summable_threePow_neg_sq_succ {alpha : ℝ} (halpha : 0 < alpha) : Summable fun (r : ℕ) => 3 ^ (-(alpha * ↑r)) * (↑r + 1) ^ 2

The (r+1)²-weighted geometric series is summable.

theorem Algsuperdiff.Section4.Provider.MinimalScale.tsum_threePow_neg_sq_succ_le {alpha : ℝ} (halpha : 0 < alpha) : ∑' (r : ℕ), 3 ^ (-(alpha * ↑r)) * (↑r + 1) ^ 2 ≤ 2 * Probability.geomTailConst alpha ^ 3

∑_r (r+1)² 3^{−αr} ≤ 2(1 − 3^{−α})^{−3}. The Γ_{1/2} companion of the proved sharp √ closure: the union-bound penalty at σ = ½ is the square (j−i+1)², whose weighted sum is a cubic closure.

4. The one transcendental inequality

theorem Algsuperdiff.Section4.Provider.MinimalScale.pow_mul_exp_neg_half_le (n : ℕ) {x : ℝ} (hx : 0 ≤ x) : x ^ n * Real.exp (-(x / 2)) ≤ (2 * ↑n) ^ n

xⁿ e^{−x/2} ≤ (2n)ⁿ for x ≥ 0. The single transcendental estimate behind both absorptions: e^{x/(2n)} ≥ x/(2n) raised to the n-th power. No numeric tactic ever sees Real.exp.

5. The regime, read as a lower bound on the exponent

theorem Algsuperdiff.Section4.Provider.MinimalScale.pow_le_expArg_mul {C cstar gam : ℝ} (hC : 0 < C) (hcs : 0 < cstar) (hgam : 0 < gam) (hreg : gam ≤ C⁻¹ ^ 10 * cstar ^ 10) : C ^ 9 ≤ C⁻¹ * cstar ^ 3 * gam⁻¹ * cstar ^ 7

The printed regime γ ≤ C^{−10}c⋆^{10}, in exponent form. It says exactly that the exponent b = C^{−1}c⋆³γ^{−1} of the Γ_{1/2} amplitude obeys b·c⋆⁷ ≥ C⁹. Both absorptions consume the regime only through this.

6. The two absorption cores, over abstract reals

7. The two absorptions, at the printed exponent

theorem Algsuperdiff.Section4.Provider.MinimalScale.inv_cube_mul_exp_le {C cstar gam s : ℝ} (hC : 0 < C) (hcs : 0 < cstar) (hgam : 0 < gam) (hreg : gam ≤ C⁻¹ ^ 10 * cstar ^ 10) (hs : 8 * gam ≤ s) : s⁻¹ ^ 3 * Real.exp (-(C⁻¹ * cstar ^ 3 * gam⁻¹)) ≤ (216 * C ^ 3 + 100000 * C⁻¹ ^ 15) * Real.exp (-(C⁻¹ * cstar ^ 3 * gam⁻¹ / 2))

The s^{−3} absorption. On the window s ≥ 8γ and in the regime γ ≤ C^{−10}c⋆^{10},

s^{−3} exp(−C^{−1}c⋆³γ^{−1}) ≤ (216C³ + 10⁵C^{−15}) exp(−½C^{−1}c⋆³γ^{−1}),

so the s^{−3} of the (j−i+1)² union-bound penalty leaves no trace in the printed Γ_{1/2} amplitude, at the cost of halving the exponent (equivalently, of doubling the dimensional constant).

theorem Algsuperdiff.Section4.Provider.MinimalScale.exp_neg_eighth_le_sqrt {C cstar gam : ℝ} (hC : 0 < C) (hcs : 0 < cstar) (hgam : 0 < gam) (hreg : gam ≤ C⁻¹ ^ 10 * cstar ^ 10) : Real.exp (-(C⁻¹ * cstar ^ 3 * gam⁻¹ / 8)) ≤ √(4 * C + 64 * C⁻¹ ^ 8) * (cstar⁻¹ * √gam)

The collapse absorption. In the regime γ ≤ C^{−10}c⋆^{10},

exp(−⅛C^{−1}c⋆³γ^{−1}) ≤ √(4C + 64C^{−8}) · c⋆^{−1}√γ,

i.e. the fourth root of the exponentially small Γ_{1/2} amplitude is below the printed Γ₂ amplitude C c⋆^{−1}s^{−5/2}√γ. This is the numerical content's "by e.powerofGammasigma, s ≥ 8γ and γ ≤ C^{−1}c⋆⁵". Squaring both sides removes every root, after which exp_quarter_core closes it.

8. Small utilities used by the tail split and the closed forms

theorem Algsuperdiff.Section4.Provider.MinimalScale.le_of_sq_le_sq' {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (h : a ^ 2 ≤ b ^ 2) : a ≤ b

Comparison of nonnegative reals through their squares. Used wherever a Real.sqrt has to be removed before any arithmetic happens.

theorem Algsuperdiff.Section4.Provider.MinimalScale.log_two_le_one : Real.log 2 ≤ 1

theorem Algsuperdiff.Section4.Provider.MinimalScale.exp_neg_le_half_exp_neg {a c : ℝ} (h : c + Real.log 2 ≤ a) : Real.exp (-a) ≤ Real.exp (-c) / 2

The halving step of every union bound below: an exponential whose argument is log 2 further out is at most half of the target exponential.

9. The two closure constants at the §4.2 rate ½s

theorem Algsuperdiff.Section4.Provider.MinimalScale.geomTailConst_cube_le {s : ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) : Probability.geomTailConst (s / 2) ^ 3 ≤ 64 * s⁻¹ ^ 3

geomTailConst (½s)³ ≤ 64 s^{−3}, the Γ_{1/2} closed form.

theorem Algsuperdiff.Section4.Provider.MinimalScale.geomSqrtConst_le {s : ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) : Probability.geomSqrtConst (s / 2) ≤ 8 * (√s ^ 3)⁻¹

geomSqrtConst (½s) ≤ 8 s^{−3/2}, the sharp Γ₂ closed form, written with (√s)³ so that no rpow enters.