BaseWindowDiffusivity

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

The diffusivity conjunct of the induction state on the whole base window m ≤ m*

ABK26, the induction hypothesis d.mathcalS.def and its first clause e.shom.h.bounds:

¼ max{c⋆ γ⁻¹ 3^(2γm), ν²} ≤ σ_m² ≤ 4 max{c⋆ γ⁻¹ 3^(2γm), ν²}.

Main results

• inductionState_diffusivity_le_mStar: the clause at every m ≤ mStar M.

Route

The window characterization Provider.Scales.le_mStar_iff (Provider/Scales/Landmarks.lean) turns m ≤ mStar M into

2 (log 3) c⁺ γ⁻¹ 3^(2γm) ≤ ν².

The standing dimension bound 2 ≤ d (M.shellPrefix.dimension) and the proved Disorder.dim_mul_cstar_le_cstarPlus (Section3/Disorder/Cstar.lean) give 2 c⋆ ≤ d c⋆ ≤ c⁺, so with log 3 > 1

c⋆ γ⁻¹ 3^(2γm) ≤ ½ c⁺ γ⁻¹ 3^(2γm) ≤ ν² / (4 log 3) ≤ ν²,

and the max collapses to ν². The proved plateau specialization Provider.Base.annealedPlateau_le_mStar (Provider/Base/PlateauLandmarks.lean), which is the diffusivity conjunct of e.basecase.diffusivity, then gives ν ≤ σ_m ≤ 2 ν; squaring proves inside the printed window [ν²/4, 4 ν²], the constants ¼ and 4 being exactly the squares of 1 and 2.

No hypothesis beyond m ≤ mStar M is used: 2 ≤ d is not a binder here, it is read off the standing model through M.shellPrefix.dimension, exactly as the near-twin does.

References

• ABK26, (d.mathcalS.def), (e.shom.h.bounds).
• ABK26, (e.basecase.diffusivity), proof reference.
• ABK26, (e.mstar).
• ABK26, (the printed split at m*).

The numeric input

The abstract collapse

Stated on bare reals so that the geometric factor never appears in a linear arithmetic goal: Y below is instantiated at γ⁻¹ 3^(2γm), which is an rpow and stays an opaque nonnegative atom throughout.

The window collapse of the comparison quantity

The diffusivity conjunct on the base window

theorem Algsuperdiff.Section3.Provider.Induction.inductionState_diffusivity_le_mStar {d : ℕ} (M : ABKModel d) (m : ℤ) : m ≤ mStar M → 1 / 4 * max (Disorder.cstar M * M.gamma⁻¹ * 3 ^ (2 * M.gamma * ↑m)) (M.nu ^ 2) ≤ ↑(Annealed.sigmaBar M m) ^ 2 ∧ ↑(Annealed.sigmaBar M m) ^ 2 ≤ 4 * max (Disorder.cstar M * M.gamma⁻¹ * 3 ^ (2 * M.gamma * ↑m)) (M.nu ^ 2)

e.shom.h.bounds on the whole base window m ≤ m*.

This is the first conjunct of Algsuperdiff.Frozen.Section3.inductionState, which does not mention E, on the printed range of e.basecase.diffusivity. Unconditional: no residual input, no caller-supplied proposition.

For m ≤ m* the landmark e.mstar collapses the max to ν² (cstar_mul_rpow_le_nu_sq), and the proved plateau specialization Provider.Base.annealedPlateau_le_mStar gives ν ≤ σ_m ≤ 2 ν, hence ν²/4 ≤ ν² ≤ σ_m² ≤ 4 ν².

theorem Algsuperdiff.Section3.Provider.Induction.inductionState_diffusivity_of_le_mStar {d : ℕ} (M : ABKModel d) {m0 : ℤ} (hm0 : m0 ≤ mStar M) (m : ℤ) : m ≤ m0 → 1 / 4 * max (Disorder.cstar M * M.gamma⁻¹ * 3 ^ (2 * M.gamma * ↑m)) (M.nu ^ 2) ≤ ↑(Annealed.sigmaBar M m) ^ 2 ∧ ↑(Annealed.sigmaBar M m) ^ 2 ≤ 4 * max (Disorder.cstar M * M.gamma⁻¹ * 3 ^ (2 * M.gamma * ↑m)) (M.nu ^ 2)

The window form: the first conjunct of the induction state at every top scale m0 ≤ m*.

Algsuperdiff.Frozen.Section3.inductionState M m0 E opens with ∀ m : ℤ, m ≤ m0 → e.shom.h.bounds at m. For m0 ≤ mStar M that clause is exactly the previous theorem composed with transitivity, so it is available unconditionally and for every budget E.