InductionStart

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

The induction state at the base landmark m**

ABK26 packages the base case from the m <= m** consequences of the plateau estimate as the induction state d.mathcalS.def at m0 = m**. This file supplies the diffusivity half of that packaging, and the scale-transport glue the base-case assembly consumes.

Main results

• inductionState_diffusivity: the diffusivity conjunct of Algsuperdiff.Frozen.Section3.inductionState M (mStarStar M) E — proved unconditionally, with no residual input and no dependence on E.

Supporting glue:

• isOneSidedOrlicz_cutoffHomogenizationError_of_le: the non-strict scale transport of the Appendix-literal one-sided relation, obtained from the proved Provider.ErrorComparison.isBigOWith_cutoffHomogenizationError_of_lt.
• sqrt_cstar_le_sqrt_cstarPlus: the numeric comparison the base-case assembly needs.

The model-free two-term promotion isTwoTermBigOWith_of_isOneSidedOrlicz — a one-sided Gamma_sigma bound promotes for free to the two-term shape, with the second witness identically zero and the second amplitude an arbitrary positive number — lives in Provider/Orlicz/TwoTermPromotion.lean, and the base-loss square-root comparison in Provider/Scales/BaseLoss.lean.

The diffusivity conjunct

Since m** <= m*, the conjunct is the proved Provider.Induction.inductionState_diffusivity_le_mStar composed with transitivity: for m <= m* the landmark threshold forces cstar gamma^{-1} 3^{2 gamma m} <= nu^2, so the max in the induction state collapses to nu^2, and the plateau specialization gives nu <= sigmaBar_m <= 2 nu, which is inside the printed window [nu^2 / 4, 4 nu^2].

The scale endpoint

inductionState quantifies its error clause over the closed window s in [8 gamma, 1], while every recorded base estimate carries the literal open interval 0 < s < 1. The endpoint s = 1 is reached by the consumer without ever evaluating baseLoss at 1: the interior scale min s (1/2) is used, and the error at the larger scale s is dominated a.e. by the error at the smaller scale via e.mathcalE.monotone.ordered, proved as Provider.ErrorComparison.cutoffHomogenizationError_ae_antitone and exposed here as isOneSidedOrlicz_cutoffHomogenizationError_of_le. That costs only the factor (min s (1/2))^{-1} <= 2 s^{-1}.

References

• ABK26, p.base.case.
• ABK26, d.mathcalS.def, the induction state.
• ABK26, e.mstarstar.
• ABK26, e.mathcalE.monotone.ordered.

The diffusivity conjunct of the induction state

theorem Algsuperdiff.Section3.Provider.Base.inductionState_diffusivity {d : ℕ} (M : ABKModel d) (m : ℤ) : m ≤ mStarStar 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)

The diffusivity conjunct of Algsuperdiff.Frozen.Section3.inductionState at m0 = m**, unconditionally.

This statement is the first conjunct of Algsuperdiff.Frozen.Section3.inductionState M (mStarStar M) E, which does not mention E. No residual input is used.

m** <= m* (Provider.Scales.mStarStar_le_mStar), so this is the proved Provider.Induction.inductionState_diffusivity_le_mStar, which proves the same window on the whole base range m <= m*, composed with transitivity. There the landmark characterization collapses the max to nu^2 and the plateau specialization gives nu <= sigmaBar_m <= 2 nu, hence nu^2 / 4 <= nu^2 <= sigmaBar_m^2 <= 4 nu^2.

Scale transport of the one-sided relation

theorem Algsuperdiff.Section3.Provider.Base.isOneSidedOrlicz_cutoffHomogenizationError_of_le {d : ℕ} (M : ABKModel d) (m : ℤ) {Psi : ℝ → ℝ} {t s A : ℝ} (ht : 0 < t) (hts : t ≤ s) (h : Probability.IsOneSidedOrlicz (↑(Cutoff.cutoffSampleLaw M)) Psi (Observable.cutoffHomogenizationError M m ⟨t, ht⟩) A) : Probability.IsOneSidedOrlicz (↑(Cutoff.cutoffSampleLaw M)) Psi (Observable.cutoffHomogenizationError M m ⟨s, ⋯⟩) A

The non-strict scale transport of X <= O_Psi(A) for the Section 3 error observable.

The proved Provider.ErrorComparison.isBigOWith_cutoffHomogenizationError_of_lt covers t < s; the base case also needs t = s, where the two observables are literally the same function. Neither Psi nor A changes.

The two numeric comparisons

theorem Algsuperdiff.Section3.Provider.Base.sqrt_cstar_le_sqrt_cstarPlus {d : ℕ} (M : ABKModel d) : √(Disorder.cstar M) ≤ √(Disorder.cstarPlus M)

The directional constant never exceeds the Frobenius one: cstar <= c+ because d cstar <= c+ and d >= 2.