BaseCaseAssembly

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

Final assembly of the Section 3 base case

This module combines the three proved base-error regimes with the annealed plateau estimates and constructs the induction state at m**. A single positive constant depending only on d is chosen before the model and every scale parameter. It is the sum of the constants used by the m** and m* error regimes, so each of the three error conclusions follows by monotonicity of its tail scale.

The terminal endpoint in the induction-state error window is proved directly. For s in [8 gamma, 1], the open-interval base estimate is applied at min s (1/2), transported to s by antitonicity of the cutoff error, and bounded using sqrt (baseLoss d u) <= K u^-1. The factor two from (min s (1/2))^-1 <= 2 s^-1 is absorbed into the chosen start constant.

noncomputable def Algsuperdiff.Section3.Provider.Base.baseCaseErrorConst (d : ℕ) : ℝ

The common dimension-only error constant for all three base regimes.

Equations

• Algsuperdiff.Section3.Provider.Base.baseCaseErrorConst d = Algsuperdiff.Section3.Provider.Base.baseCaseMStarStarErrorConst d + Algsuperdiff.Section3.Provider.Base.cutoffMassSqrtConst d

theorem Algsuperdiff.Section3.Provider.Base.baseCaseErrorConst_pos (d : ℕ) : 0 < baseCaseErrorConst d

The common base-error constant is strictly positive.

theorem Algsuperdiff.Section3.Provider.Base.base_case (d : ℕ) : ∃ (C0 : ℝ) (Cstart : ℝ), 0 < C0 ∧ 0 < Cstart ∧ ∀ (M : ABKModel d), (∀ (m : ℤ), M.nu ≤ ↑(Annealed.sigmaBar M m) ∧ ↑(Annealed.sigmaBar M m) ≤ M.nu * (1 + Disorder.cstarPlus M * (2 * M.nu ^ 2)⁻¹ * M.gamma⁻¹ * (1 + 4 * M.gamma) * 3 ^ (2 * M.gamma * ↑m)) ∧ ∀ (s : { s : ℝ // s ∈ Set.Ioo 0 1 }), Probability.IsTwoTermBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma 4) (Observable.cutoffHomogenizationError M m ⟨↑s, ⋯⟩) (C0 * M.nu⁻¹ * (√M.gamma)⁻¹ * 3 ^ (M.gamma * ↑m) * √(baseLoss d s)) (C0 * (√M.nu)⁻¹ * (√√M.gamma)⁻¹ * 3 ^ (M.gamma * ↑m / 2) * √√(baseLoss d s))) ∧ (∀ m ≤ mStarStar M, M.nu ≤ ↑(Annealed.sigmaBar M m) ∧ ↑(Annealed.sigmaBar M m) ≤ (1 + M.gamma ^ 2) * M.nu ∧ ∀ (s : { s : ℝ // s ∈ Set.Ioo 0 1 }), Probability.IsOneSidedOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (Observable.cutoffHomogenizationError M m ⟨↑s, ⋯⟩) (C0 * (√(Disorder.cstarPlus M))⁻¹ * √M.gamma * √(baseLoss d s))) ∧ (∀ m ≤ mStar M, M.nu ≤ ↑(Annealed.sigmaBar M m) ∧ ↑(Annealed.sigmaBar M m) ≤ 2 * M.nu ∧ ∀ (s : { s : ℝ // s ∈ Set.Ioo 0 1 }), Probability.IsDeterministicShiftOneSidedOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (Observable.cutoffHomogenizationError M m ⟨↑s, ⋯⟩) 2 (C0 * (√(Disorder.cstarPlus M))⁻¹ * √(baseLoss d s))) ∧ ∃ (Estart : { E : ℝ // 1 ≤ E }), ↑Estart = Cstart * (√(Disorder.cstar M))⁻¹ ∧ Frozen.Section3.inductionState M (mStarStar M) Estart

A proved local corrected base-case assembly, with one common dimension-only error constant and a directly assembled induction start.