Bootstrap

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

Deterministic recurrence integration: squared bootstrap

This file assembles Steps 3--4 of ABK26 l.integrate.approx.recurrence into the squared-deviation estimate. The all-scale envelope uses cstarPlus; the comparator and recurrence remain directional in cstar. The additional cstar⁻² * cstarPlus term pays for that exact two-constant interface.

References

• ABK26.

def Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.recurrenceDescentConstant : ℝ

The fixed universal descent constant: any value ≥ 6400·18/log 3 ≈ 1.05·10⁵ works; 120000 gives margin. It is public because the explicit integration constant is built from it.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.recurrenceDescentConstant = 120000

Pure-real algebra cores

The three lemmas below are the Chunk.lean (chunk_algebra) device: every genuinely nonlinear step of this file is discharged here, over abstract reals in a minimal context, so that no numeric tactic is ever run inside the Real.sqrt / Real.log / geometricTerm / recurrenceComparator-laden contexts of base_bound, smallness_B and sq_deviation_core_explicit. At the call sites only linarith only [...] (or a direct application) remains.

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.sq_deviation_core_explicit {ν cstar cplus γ E F : ℝ} {m₀ : ℤ} {s : ℤ → ℝ} (hν : 0 < ν) (hcstar : 0 < cstar) (hcc : cstar ≤ cplus) (hγ : 0 < γ) (hE : 1 ≤ E) (hF : 1 ≤ F) (hpos : ∀ (m : ℤ), 0 < s m) (hsmall : ∀ (m : ℤ), ν ≤ s m ∧ s m ≤ (1 + (ν ^ 2)⁻¹ * cplus * γ⁻¹ * geometricTerm γ m) * ν) (hupper : ∀ (n m : ℤ), m ≤ m₀ → n ≤ m → ↑m ≤ ↑n + cstar * γ⁻¹ → s m ≤ (1 + E * γ) * s n + recurrenceIncrement cstar γ n m * (s n)⁻¹) (hlower : ∀ (n m : ℤ), m ≤ m₀ → n ≤ m → ↑m ≤ ↑n + cstar * γ⁻¹ → (1 - E * γ) * s n + recurrenceIncrement cstar γ n m * (s n)⁻¹ ^ 2 * s m - F * (↑m - ↑n) ^ 2 * (s n)⁻¹ ^ 4 * s m * geometricTerm (2 * γ) m ≤ s m) : γ * (4 * recurrenceDescentConstant ^ 2 * (E * (1 + (cstar ^ 2)⁻¹ * F + (cstar * min cstar 1)⁻¹ * cplus))) ≤ 1 → ∀ m ≤ m₀, recurrenceComparator ν cstar γ m ≤ 2 * s m ^ 2 ∧ |s m ^ 2 - recurrenceComparator ν cstar γ m| ≤ 4 * recurrenceDescentConstant ^ 2 * √(E * (1 + (cstar ^ 2)⁻¹ * F + (cstar * min cstar 1)⁻¹ * cplus) * γ) * recurrenceComparator ν cstar γ m

Squared-deviation core (ABK26 Steps 3–4), two-constant capped form. Produces the constant C₀ and, under the quadratic smallness γ·C₀·(E(1+c⋆⁻²F+(c⋆·min{c⋆,1})⁻¹c⁺)) ≤ 1, the bootstrap sandwich T_m ≤ 2s_m² and the squared-deviation bound |s_m² − T_m| ≤ C₀√(E(1+c⋆⁻²F+(c⋆·min{c⋆,1})⁻¹c⁺)γ)·T_m for every m ≤ m₀.

The a-priori envelope hsmall (e.small.scale.bound) is read at the constant c⁺ ≥ c⋆, while the comparator T_m and the recurrence hypotheses keep the directional c⋆; the gap is paid for by the extra (c⋆·min{c⋆,1})⁻¹c⁺ summand in the γ-threshold.

Both are recovered here from the cap c = min{c⋆,1} (adaptStep_le_cap), whose only price is that the c⁺-summand of the composite constant is denominated in c⋆c rather than c⋆².