StateCalculus

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

The state calculus of the Section 3.6 induction

Support layer for the two induction roots p.induction.step and p.induction.bounds. The roots themselves are NOT declared here: they wait on Algsuperdiff.Frozen.Section3.multiscale_estimate. This module delivers the surrounding calculus of Algsuperdiff.Frozen.Section3.inductionState:

• monotonicity in the budget E;
• the integer-iteration scaffold from a base scale to every scale;
• the s^{-2} to s-free absorption of the rare lane at the terminal display;
• the epsilon-fixing arithmetic of the multiscale conclusion; and
• the base-bridge arithmetic Cstart c_star^{-1/2} <= C c_star^{-1}.

The frozen definition's E-occurrences

inductionState M m0 E is a conjunction of two forall m <= m0 clauses. The first (the sigmaBar sandwich) does not mention E at all. The second is a Probability.IsTwoTermBigOWith display whose two amplitudes are

• (E : R) * s^{-1} * sqrt gamma -- increasing in E; and
• (s^{-1})^2 * exp (-((E : R)^{-1})^3 * gamma^{-1}) -- also increasing in E, because E >= 1 > 0 makes E^{-1} decreasing, hence (E^{-1})^3 decreasing, hence the negated exponent increasing (gamma > 0 is the standing M.shellPrefix.gamma_pos).

So every occurrence of E in the real definition is monotone and inductionState_mono_E is unconditional. No non-monotone occurrence exists.

Sources

• ABK26, d.mathcalS.def, p.induction.bounds, p.induction.step, the induction proof, the epsilon-fixing, the terminal budget E = C c_star^{-1}.
• The gate does NOT fail at C = 6; it clears with margin (64 * 6 = 384 >= 324).

1. Amplitude monotonicity of the two-term display

2. Monotonicity of the induction state in the budget E

theorem Algsuperdiff.Section3.Provider.Induction.inductionState_mono_E {d : ℕ} {M : ABKModel d} {m0 : ℤ} {E E' : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 E) (hEE : ↑E ≤ ↑E') : Frozen.Section3.inductionState M m0 E'

The induction state is monotone in its budget.

Both E-occurrences of the frozen definition are increasing in E: the Gamma_2 amplitude E s^{-1} sqrt gamma visibly, and the Gamma_{1/2} amplitude (s^{-1})^2 exp (-(E^{-1})^3 gamma^{-1}) because 1 <= E makes (E^{-1})^3 decreasing. Enlarging both amplitudes weakens the display, so no hypothesis beyond (E : R) <= (E' : R) is needed.

3. The integer-iteration scaffold

theorem Algsuperdiff.Section3.Provider.Induction.inductionState_of_base_of_step {d : ℕ} {M : ABKModel d} {mb : ℤ} {E : { E : ℝ // 1 ≤ E }} (base : Frozen.Section3.inductionState M mb E) (step : ∀ (n : ℤ), Frozen.Section3.inductionState M (n - 1) E → Frozen.Section3.inductionState M n E) (m : ℤ) : Frozen.Section3.inductionState M m E

From a base scale and a one-scale step to every integer scale.

Above the base scale this is Int.leInduction; below it the conclusion is already contained in the base case, because both clauses of the frozen definition are forall m <= m0 (the proved ...ApproximateRecurrence.Closure.inductionState_mono).

theorem Algsuperdiff.Section3.Provider.Induction.inductionState_of_base_of_step_of_E_le {d : ℕ} {M : ABKModel d} {mb : ℤ} {E0 E : { E : ℝ // 1 ≤ E }} (base : Frozen.Section3.inductionState M mb E0) (hE : ↑E0 ≤ ↑E) (step : ∀ (n : ℤ), Frozen.Section3.inductionState M (n - 1) E → Frozen.Section3.inductionState M n E) (m : ℤ) : Frozen.Section3.inductionState M m E

The E-enlarging iteration. The base case holds at the smaller budget and the one-scale step at the larger budget E; the bridge is inductionState_mono_E. This is the manuscript's C c_star^{-1/2} |-> C c_star^{-1} bump.

4. The s^{-2} to s-free absorption of the rare lane

The transcendental step is confined to pow_three_le_const_mul_exp; the arithmetic core inv_sq_le_of_regime sees exp only as an opaque positive real X.

theorem Algsuperdiff.Section3.Provider.Induction.inv_sq_mul_exp_le_exp_of_regime {gamma cst C s : ℝ} (hgamma : 0 < gamma) (hcs0 : 0 < cst) (hcs : cst ≤ 3 / 2) (hC : 6 ≤ C) (hreg : gamma ≤ C⁻¹ ^ 10 * cst ^ 10) (hs8 : 8 * gamma ≤ s) : s⁻¹ ^ 2 * Real.exp (-((C ^ 3)⁻¹ * cst ^ 3 * gamma⁻¹)) ≤ Real.exp (-((2 * C ^ 3)⁻¹ * cst ^ 3 * gamma⁻¹))

The s^{-2} of the induction state's Gamma_{1/2} clause is absorbable at the terminal display, uniformly over the printed window s >= 8 gamma, at the cost of one enlargement C |-> 2 C^3 of the exponent constant.

theorem Algsuperdiff.Section3.Provider.Induction.inductionState_isTwoTermBigOWith_sFree {d : ℕ} (M : ABKModel d) {C : ℝ} {E : { E : ℝ // 1 ≤ E }} (hC : 6 ≤ C) (hEval : ↑E = C * (Disorder.cstar M)⁻¹) (hreg : M.gamma ≤ C⁻¹ ^ 10 * Disorder.cstar M ^ 10) {m0 : ℤ} (hS : Frozen.Section3.inductionState M m0 E) (m : ℤ) (hm : m ≤ m0) (s : ℝ) (hsWindow : s ∈ Set.Icc (8 * M.gamma) 1) : Probability.IsTwoTermBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Observable.cutoffHomogenizationError M m ⟨s, ⋯⟩) (2 * C ^ 3 * (Disorder.cstar M)⁻¹ * s⁻¹ * √M.gamma) (Real.exp (-((2 * C ^ 3)⁻¹ * Disorder.cstar M ^ 3 * M.gamma⁻¹)))

The consumer-facing s-free display.

At the terminal budget E = C c_star^{-1} the induction state's Gamma_2 amplitude is already the printed C c_star^{-1} s^{-1} sqrt gamma and its Gamma_{1/2} amplitude is (s^{-1})^2 exp (-C^{-3} c_star^3 gamma^{-1}). Re-wrapping both at the single enlarged constant Cp = 2 C^3 produces exactly the first conclusion of Algsuperdiff.Frozen.Section3.induction_bounds (with C there instantiated at Cp): amplitude Cp c_star^{-1} s^{-1} sqrt gamma and the s-free exp (-(Cp^{-1} c_star^3 gamma^{-1})).

No multiscale input is used: the whole content is the E-instantiation, the absorption above, and amplitude monotonicity.

5. The epsilon-fixing of the multiscale conclusion

The frozen multiscale_estimate conclusion carries Cms * E * s^{-1} * sqrt (epsilon * gamma) and Cms * epsilon * (s^{-1})^2 * exp (...). Fixing epsilon := (2 Cms)^{-2} makes Cms * sqrt epsilon = 1/2 and Cms * epsilon = (4 Cms)^{-1} <= 1, so both amplitudes drop to the inductionState shape at the same E.

The enlargement is admissible because every Cms-occurrence in the frozen conclusion is weakened by a larger constant, except the guard s <= Cms * epsilon of the Y-refinement clause -- and at the fixed epsilon = ((2 Cms)^2)^{-1} that guard's threshold (4 Cms)^{-1} tightens with Cms.

theorem Algsuperdiff.Section3.Provider.Induction.epsilonFix_mem_Ioc {Cms : ℝ} (hCms : 1 ≤ Cms) : ((2 * Cms) ^ 2)⁻¹ ∈ Set.Ioc 0 (1 / 2)

The fixed epsilon = (2 Cms)^{-2} lies in the admissible window Ioc 0 (1/2) of multiscale_estimate, for every Cms >= 1.

theorem Algsuperdiff.Section3.Provider.Induction.mul_sqrt_epsilonFix {Cms : ℝ} (hCms : 0 < Cms) : Cms * √((2 * Cms) ^ 2)⁻¹ = 2⁻¹

The epsilon-fixing makes the multiscale Gamma_2 loss coefficient exactly 1/2.

theorem Algsuperdiff.Section3.Provider.Induction.multiscaleAmplitude_le_of_epsilonFix {Cms E s gamma : ℝ} (hCms : 0 < Cms) (hE : 0 ≤ E) (hs : 0 ≤ s⁻¹) : Cms * E * s⁻¹ * √(((2 * Cms) ^ 2)⁻¹ * gamma) ≤ E * s⁻¹ * √gamma

The fixed multiscale Gamma_2 amplitude is at most the induction state's, at the same budget E.

theorem Algsuperdiff.Section3.Provider.Induction.multiscaleRareAmplitude_le_of_epsilonFix {Cms u v : ℝ} (hCms : 1 ≤ Cms) (hu : 0 ≤ u) (hv : 0 ≤ v) : Cms * ((2 * Cms) ^ 2)⁻¹ * u * v ≤ u * v

The fixed multiscale Gamma_{1/2} amplitude is at most the induction state's: Cms * (2 Cms)^{-2} = (4 Cms)^{-1} <= 1.

6. The base bridge Cstart c_star^{-1/2} <= C c_star^{-1}

theorem Algsuperdiff.Section3.Provider.Induction.startBudget_le_of_sqrt {cst Cstart C : ℝ} (hcs0 : 0 < cst) (hcs : cst ≤ 3 / 2) (hCstart : 0 ≤ Cstart) (hC : Cstart * √(3 / 2) ≤ C) : Cstart * (√cst)⁻¹ ≤ C * cst⁻¹

The base bridge. Under the proved c_star <= 3/2 the base case's budget Cstart c_star^{-1/2} is below the induction budget C c_star^{-1} as soon as C >= Cstart sqrt (3/2). The equivalence is Cstart c_star^{-1/2} <= C c_star^{-1} iff Cstart sqrt c_star <= C.

theorem Algsuperdiff.Section3.Provider.Induction.one_le_terminalBudget {K cst : ℝ} (hK : 6 ≤ K) (hcs0 : 0 < cst) (hcs : cst ≤ 3 / 2) : 1 ≤ K * cst⁻¹

The terminal budget is at least one in the induction parameter regime.