InductionState

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

The all-scales induction state 𝒮(m, C c⋆⁻¹)

Section 4 consumes the Section 3 induction state 𝒮(m₀, E) as a premise at half a dozen call sites: p.cg.ellipticity.bounds and e.shom.m.vs.shom.n both carry 𝒮(m₀−1, E) together with a budget gate E ≥ C c⋆⁻¹ and a regime γ ≤ E⁻¹¹⁰, and §4.1 applies them at arbitrary scales without ever exhibiting the state. The manuscript's discharge is the last two lines of the proof of p.induction.bounds:

According to Proposition p.base.case, there exists C(d) < ∞ such that 𝒮(m**, C c⋆^{−1/2}) is valid. By induction, we deduce the existence of C(d) < ∞ such that 𝒮(m, C c⋆⁻¹) is valid for every m ∈ ℤ.

This module renders those two lines over the Section 3 surface.

The c⋆^{−1/2} to c⋆⁻¹ reconciliation

Both halves are proved in this repository, so the gap is closed here, not assumed:

• Algsuperdiff.Section3.Provider.Induction.inductionState_mono_E — the frozen state is monotone in E (both E-occurrences of the frozen definition are increasing in E); and

Together they give Cstart c⋆^{−1/2} ≤ C c⋆⁻¹ as soon as C ≥ Cstart √(3/2) — the proved Algsuperdiff.Section3.Provider.Induction.startBudget_le_of_sqrt.

What is consumed

• the proved state calculus of Section3/Provider/Induction/StateCalculus.lean (inductionState_mono_E, inductionState_of_base_of_step_of_E_le, startBudget_le_of_sqrt) and cstar_le_three_halves.

Algsuperdiff.Frozen.Section3.induction_bounds is not consumed: its proof builds exactly this state internally (InductionBoundsAssembly.lean) but does not export it, and its own conclusion does not carry the state. The assembly here therefore repeats the constant bookkeeping rather than importing a private helper or editing Section 3.

References

• ABK26, d.mathcalS.def; p.base.case; p.induction.bounds proof, the terminal budget.

1. The constant bookkeeping

K is fixed before every model datum: above 6, above the caller's threshold, above the base case's Cstart √(3/2), and above the induction step's own constant.

2. The all-scales state

theorem Algsuperdiff.Section4.Provider.GoodEvents.exists_allScalesInductionState_ge (d : ℕ) (C₀ : ℝ) : ∃ (C : ℝ), 6 ≤ C ∧ C₀ ≤ C ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10 → ∃ (E : { E : ℝ // 1 ≤ E }), ↑E = C * (Section3.Disorder.cstar M)⁻¹ ∧ M.gamma ≤ (↑E)⁻¹ ^ 10 ∧ ∀ (m : ℤ), Frozen.Section3.inductionState M m E

The all-scales induction state, with a caller-prescribed constant floor.

For every requested threshold C₀ there is a C ≥ max 6 C₀, depending only on the dimension and on C₀, such that every model in the printed regime γ ≤ C⁻¹¹⁰ c⋆¹⁰ admits the budget E = C c⋆⁻¹, and 𝒮(m, E) holds at every integer scale. The returned bundle also carries the three E-side facts the Section 4 call sites need (see §3).

The C₀ slot is what makes the result usable: a downstream node with its own constant C' gets C' c⋆⁻¹ ≤ E from mul_cstarInv_le_of_budget by requesting C₀ := C'.

theorem Algsuperdiff.Section4.Provider.GoodEvents.exists_allScalesInductionState (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10 → ∃ (E : { E : ℝ // 1 ≤ E }), ↑E = C * (Section3.Disorder.cstar M)⁻¹ ∧ ∀ (m : ℤ), Frozen.Section3.inductionState M m E

The all-scales induction state in the shape printed: there is a C(d) such that 𝒮(m, C c⋆⁻¹) is valid for every m ∈ ℤ.

3. The E-window consumption A

The Section 4 call sites do not consume 𝒮 alone: p.cg.ellipticity.bounds (as Algsuperdiff.Frozen.Section3.coarse_ellipticity_bounds) asks for max (exp (Ccg/σ)) c⋆⁻¹ ≤ E and E ≤ γ^{−1/5} on top of the state, and e.shom.m.vs.shom.n asks for C' c⋆⁻¹ ≤ E and γ ≤ E⁻¹¹⁰. Each of the budget-side facts is discharged from the budget identity (E : ℝ) = C c⋆⁻¹.

theorem Algsuperdiff.Section4.Provider.GoodEvents.mul_cstarInv_le_of_budget {d : ℕ} (M : Section3.ABKModel d) {C C' : ℝ} {E : { E : ℝ // 1 ≤ E }} (hEval : ↑E = C * (Section3.Disorder.cstar M)⁻¹) (h : C' ≤ C) : C' * (Section3.Disorder.cstar M)⁻¹ ≤ ↑E

Any constant below the budget constant clears the budget gate. This is the premise E ≥ C' c⋆⁻¹ of e.shom.m.vs.shom.n and of the induction_step, at a downstream node's own constant C'.

theorem Algsuperdiff.Section4.Provider.GoodEvents.cstarInv_le_of_budget {d : ℕ} (M : Section3.ABKModel d) {C : ℝ} {E : { E : ℝ // 1 ≤ E }} (hEval : ↑E = C * (Section3.Disorder.cstar M)⁻¹) (hC : 1 ≤ C) : (Section3.Disorder.cstar M)⁻¹ ≤ ↑E

c⋆⁻¹ ≤ E — the second entry of the max in the coarse_ellipticity_bounds.

theorem Algsuperdiff.Section4.Provider.GoodEvents.le_rpow_neg_fifth_of_regime {d : ℕ} (M : Section3.ABKModel d) {E : { E : ℝ // 1 ≤ E }} (hreg : M.gamma ≤ (↑E)⁻¹ ^ 10) : ↑E ≤ M.gamma ^ (-(1 / 5))

E ≤ γ^{−1/5} — the upper E-window of the coarse_ellipticity_bounds, from the regime γ ≤ E⁻¹¹⁰ alone.

The regime gives γ^{1/5} ≤ E⁻², hence γ^{−1/5} ≥ E² ≥ E.

theorem Algsuperdiff.Section4.Provider.GoodEvents.coarseEllipticityBudget {d : ℕ} (M : Section3.ABKModel d) {C Ccg sigma : ℝ} {E : { E : ℝ // 1 ≤ E }} (hEval : ↑E = C * (Section3.Disorder.cstar M)⁻¹) (hC : 1 ≤ C) (hreg : M.gamma ≤ (↑E)⁻¹ ^ 10) (hall : ∀ (m : ℤ), Frozen.Section3.inductionState M m E) (hexp : Real.exp (Ccg / sigma) ≤ ↑E) (m : ℤ) : Frozen.Section3.inductionState M (m - 1) E ∧ max (Real.exp (Ccg / sigma)) (Section3.Disorder.cstar M)⁻¹ ≤ ↑E ∧ ↑E ≤ M.gamma ^ (-(1 / 5))

The E-side hypotheses of the coarse_ellipticity_bounds.

Given the budget identity, the regime, and the caller's own choice of σ and Ccg (through hexp, which is genuinely a caller obligation: exp (Ccg/σ) is unbounded as σ ↓ 0 while the budget is fixed), the two E-window premises and the state premise are all available at every scale m.