ShomContinuityCore

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

Two-sided diffusivity comparator: a model-free arithmetic core

This file is model-free deterministic arithmetic. Everything below is stated for an abstract sequence s : ℤ → ℝ and an abstract two-sided comparator diffMax; no renormalization, probabilistic, or geometric object occurs, and every hypothesis is an explicit input supplied by the caller rather than a source premise of any frozen theorem.

The genuine long-range step additionally requires the asymptotic diffusivity profile of p.propagate.diffusivity.lower.bound (ABK26), which is neither used nor asserted here. What this file provides is the arithmetic that the manuscript performs after that profile has been consumed, i.e. the two steps that use only the two-sided envelope e.shom.h.bounds.

Source

e.shom.h.bounds (ABK26) reads ¼ max{c⋆ γ⁻¹ 3^{2γm}, ν²} ≤ σ_m² ≤ 4 max{c⋆ γ⁻¹ 3^{2γm}, ν²},

and diffMax below is exactly the bracketed maximum.

• The quarter comparison is ABK26: σ_m² ≥ ¼ max{c⋆γ⁻¹3^{2γm},ν²} ≥ ¼ max{c⋆γ⁻¹3^{2γn},ν²} ≥ 1/16 σ_n², "Taking square roots gives σ_m ≥ ¼ σ_n".
• The far branch is ABK26: for m − n ≥ γ⁻¹, |σ_m σ_n⁻¹ − 1| + |σ_n σ_m⁻¹ − 1| ≤^{γ(m−n)}. The manuscript leaves C unnamed; the explicit witness proved here is 8. The argument in fact delivers 4·3^{γ(m−n)} + 2, hence also the sharper 6·3^{γ(m−n)}; 8 is retained as the stated constant.

Both statements below are proved under n ≤ m although the source range is m > n; the extra equality case costs nothing and is not used to weaken any conclusion. Neither statement uses the source's regime split, the constraint γ ≤ E^{-10}, or the endpoint m₀: they hold whenever the caller exhibits the two-sided envelope at the two scales.

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ShomContinuityCore.diffMax (nu gamma cstar : ℝ) (k : ℤ) : ℝ

The two-sided comparator max{c⋆ γ⁻¹ 3^{2γk}, ν²} bracketing σ_k² in e.shom.h.bounds (ABK26).

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ShomContinuityCore.diffMax nu gamma cstar k = max (cstar * gamma⁻¹ * 3 ^ (2 * gamma * ↑k)) (nu ^ 2)

Auxiliary pure-algebra facts

These two lemmas are over abstract reals; they contain no Real.rpow, so the arithmetic tactics below never meet a transcendental atom.

Elementary properties of the comparator

theorem Algsuperdiff.Section3.Provider.Diffusivity.ShomContinuityCore.diffMax_mono {nu gamma cstar : ℝ} (hgamma : 0 < gamma) (hcstar : 0 < cstar) {n m : ℤ} (hnm : n ≤ m) : diffMax nu gamma cstar n ≤ diffMax nu gamma cstar m

The comparator is nondecreasing in the scale: c⋆γ⁻¹3^{2γk} increases and ν² is constant. This is the second inequality of ABK26.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ShomContinuityCore.diffMax_le_rpow_mul {nu gamma cstar : ℝ} (hgamma : 0 < gamma) {n m : ℤ} (hnm : n ≤ m) : diffMax nu gamma cstar m ≤ 3 ^ (2 * gamma * (↑m - ↑n)) * diffMax nu gamma cstar n

Geometric growth of the comparator: max{c⋆γ⁻¹3^{2γm},ν²} ≤ 3^{2γ(m−n)} max{c⋆γ⁻¹3^{2γn},ν²} for n ≤ m. The first summand scales exactly by 3^{2γ(m−n)}, and the constant summand ν² only grows when multiplied by a factor ≥ 1.

The two regime-free consequences of the two-sided envelope

theorem Algsuperdiff.Section3.Provider.Diffusivity.ShomContinuityCore.quarter_le_of_twoSided {nu gamma cstar : ℝ} {s : ℤ → ℝ} {n m : ℤ} (hgamma : 0 < gamma) (hcstar : 0 < cstar) (hnm : n ≤ m) (hsm : 0 < s m) (hlo_m : 1 / 4 * diffMax nu gamma cstar m ≤ s m ^ 2) (hhi_n : s n ^ 2 ≤ 4 * diffMax nu gamma cstar n) : 1 / 4 * s n ≤ s m

Quarter comparison (ABK26). From the lower envelope at m, the upper envelope at n, and monotonicity of the comparator, σ_m² ≥ ¼ diffMax_m ≥ ¼ diffMax_n ≥ 1/16 σ_n², and taking square roots gives ¼ σ_n ≤ σ_m. Only two of the four envelope inequalities are needed.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ShomContinuityCore.ratioSum_le_of_twoSided {nu gamma cstar : ℝ} {s : ℤ → ℝ} {n m : ℤ} (hgamma : 0 < gamma) (hcstar : 0 < cstar) (hnm : n ≤ m) (hsm : 0 < s m) (hsn : 0 < s n) (hlo_m : 1 / 4 * diffMax nu gamma cstar m ≤ s m ^ 2) (hhi_m : s m ^ 2 ≤ 4 * diffMax nu gamma cstar m) (hlo_n : 1 / 4 * diffMax nu gamma cstar n ≤ s n ^ 2) (hhi_n : s n ^ 2 ≤ 4 * diffMax nu gamma cstar n) : |s m / s n - 1| + |s n / s m - 1| ≤ 8 * 3 ^ (gamma * (↑m - ↑n))

Far branch (ABK26). From the two-sided envelope at both scales, σ_n ≤ 4σ_m and σ_m ≤ 4·3^{γ(m−n)}σ_n, whence |σ_m σ_n⁻¹ − 1| + |σ_n σ_m⁻¹ − 1| ≤ 8·3^{γ(m−n)}.

The manuscript states this with an unnamed C; 8 is an explicit witness (the proof actually yields 4·3^{γ(m−n)} + 2). No regime constraint on m − n is used: the bound holds for every n ≤ m at which the envelope is available.