ConclusionArithmetic

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

The arithmetic cores of p.bfA.multiscalebound, Step 3

ABK26, proof of Proposition p.bfA.multiscalebound, Step 3. Having decomposed the block matrix over the Whitney simplices (Step 1) and bounded the wave influence (Step 2), the manuscript sums the per-layer contributions over the layer index k, selects k_0 := c E^{-2} gamma^{-1}, and collapses the two small factors coming from l.bad.cubes.density into a single improved exponential.

This module isolates the pure real-arithmetic content of that step, over abstract reals with no ABK carrier in sight. Two development rules force the split: nlinarith/linarith must never see rpow or exp applied to a compound carrier expression, and the k_0 collapse is an exp/rpow computation. The carrier-level layer series that consumes these cores is Provider.Multiscale.ConclusionAssembly.

The square-root layer-density correction

With only the mass form available the k-sum of the exp(-cE^{-2}gamma^{-1}) leg diverges.

The consequence is proved locally here:

• the layer series runs at ratio 3^{-1/4} (tsum_geometric_three_rpow_neg_quarter, with its summability twin summable_geometric_three_rpow_neg_quarter) rather than at the printed 3^{-3/4}.

The cost is an absolute inflation of the Step-3 constant by (1 - 3^{-1/4})^{-1} / (1 - 3^{-3/4})^{-1}, exactly 1 + 3^{-1/4} + 3^{-1/2}, a number between 2.33 and 2.34. It is a constant of the carrier-level assembly, not of this module.

The deterministic half used here is three_rpow_le_two_add_indicator, `3^x <= 2

• 3^x 1_{x > 3^{-4}}forx >= 0`, which is's own display.

References

• ABK26, p.bfA.multiscalebound, Step 3.

log 3

Percolation.Numerics supplies 1 <= log 3 <= 2. The k_0 collapse uses the sharper upper bound log 3 <= 3/2 for comfort (: log 3 <= 2 would in fact suffice — 2b·log 3 <= 4/9 <= 17/36; convenience, not necessity).

theorem Algsuperdiff.Section3.Provider.Multiscale.log_three_le_three_halves : Real.log 3 ≤ 3 / 2

log 3 <= 3/2, sharper than Percolation.log_three_le_two.

The Cauchy-Schwarz step

min{a, b} <= sqrt(a b): the interpolation that lets the capped layer bad mass be spent half against the layer's own mass and half against the density bound.

theorem Algsuperdiff.Section3.Provider.Multiscale.min_le_sqrt_mul {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) : min a b ≤ √(a * b)

The min/Cauchy-Schwarz step. For nonnegative a, b, min a b <= sqrt (a * b).

Square roots of the two elementary profiles

theorem Algsuperdiff.Section3.Provider.Multiscale.sqrt_three_rpow (t : ℝ) : √(3 ^ t) = 3 ^ (t / 2)

sqrt (3^t) = 3^{t/2}.

theorem Algsuperdiff.Section3.Provider.Multiscale.sqrt_exp (x : ℝ) : √(Real.exp x) = Real.exp (x / 2)

sqrt (exp x) = exp (x/2).

theorem Algsuperdiff.Section3.Provider.Multiscale.sqrt_add_le_sqrt_add_sqrt {a c : ℝ} (ha : 0 ≤ a) (hc : 0 ≤ c) : √(a + c) ≤ √a + √c

Subadditivity of the square root: sqrt (a + c) <= sqrt a + sqrt c.

Core 1a: the k_0 collapse at the corrected (square-root) density

theorem Algsuperdiff.Section3.Provider.Multiscale.k0_sqrt_collapse {b t : ℝ} (hb0 : 0 ≤ b) (hb9 : 9 * b ≤ 1) (ht : 0 ≤ t) : 3 ^ (2 * b * t) * √(Real.exp (-t) + 3 ^ (-(t / 2))) ≤ 2 * Real.exp (-(t / 36))

The k_0 collapse (p.bfA.multiscalebound Step 3, at the min-capped layer density).

3^{2 b t} (exp(-t) + 3^{-t/2})^{1/2}  <=  2 exp(-t/36) ,

valid whenever 9 b <= 1 (true for the manuscript's b = 2^{-20}).

The exponent 1/36, in place of the 1/4 of the printed k0_exponent_collapse, is the entire quantitative cost; it is absorbed by the manuscript's own "selecting k_0 := c E^{-2} gamma^{-1} for a sufficiently small c > 0", i.e. by relabelling c |-> c/36.

Core 1b: the printed k_0 collapse

Core 2: the layer geometric series

theorem Algsuperdiff.Section3.Provider.Multiscale.three_rpow_neg_quarter_nonneg : 0 ≤ 3 ^ (-(1 / 4))

theorem Algsuperdiff.Section3.Provider.Multiscale.three_rpow_neg_quarter_lt_one : 3 ^ (-(1 / 4)) < 1

theorem Algsuperdiff.Section3.Provider.Multiscale.three_rpow_neg_three_quarters_nonneg : 0 ≤ 3 ^ (-(3 / 4))

theorem Algsuperdiff.Section3.Provider.Multiscale.tsum_geometric_three_rpow_neg_quarter : ∑' (k : ℕ), (3 ^ (-(1 / 4))) ^ k = (1 - 3 ^ (-(1 / 4)))⁻¹

The layer-summation geometric series at the corrected ratio. After the min/Cauchy-Schwarz step the collar leg of layer k carries the extra factor 3^{k/2}, so the printed ratio 3^{-3/4} degrades to 3^{-1/4}; the sum still converges.

theorem Algsuperdiff.Section3.Provider.Multiscale.summable_geometric_three_rpow_neg_quarter : Summable fun (k : ℕ) => (3 ^ (-(1 / 4))) ^ k

The exact constant inflation

The deterministic split

theorem Algsuperdiff.Section3.Provider.Multiscale.three_rpow_le_two_add_indicator {x : ℝ} (hx : 0 ≤ x) : 3 ^ x ≤ 2 + if 81⁻¹ < x then 3 ^ x else 0

The deterministic half's 3^{gamma hsep} reduction (p.bfA.multiscalebound Step 3).

3^x  <=  1 + 3 x 1_{x <= 3^{-4}} + 3^x 1_{x > 3^{-4}}  <=  2 + 3^x 1_{x > 3^{-4}}

for x >= 0, using 3 * 3^{-4} < 1 for the deterministic step. This is that display, at the sharper deterministic estimate 3^x <= exp(1/2) <= 2 on 0 <= x <= 3^{-4}.