Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.Induction.InductionBoundsAssembly

InductionBoundsAssembly #

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

The self-similar coarse-graining estimate: the Section 3 root #

ABK26, p.induction.bounds (printed proof):

Main result #

The assembly #

Three inputs, all of them proved or here, each consumed exactly once:

  1. Provider.Base.base_case d (Provider/Base/BaseCaseAssembly.lean) -- its LAST clause ∃ Estart, (Estart: ℝ) = Cstart (sqrt c_star)^{-1} ∧ inductionState M (mStarStar M) Estart is the induction start S(m**, Cstart c_star^{-1/2}). Its first three clauses (the all-scale error, the m**-window and the m*-window plateaus) are NOT consumed.
  2. The draft root itself is never imported.
  3. Algsuperdiff.Frozen.Section3.diffusivity_asymptotics d (Frozen/Section3/DiffusivityAsymptotics.lean, the frozen p.propagate.diffusivity.lower.bound) -- its conclusion, the sharp defect display e.formula.for.shom on the window ∀ m ≤ m0, is the ingredient of the second root conjunct. Its 2nd and 3rd conclusions (the sigmaBar sandwich at m0) are NOT consumed here; they are consumed inside input 2.

The exported constant is chosen B the universally quantified model. Write Cstart, Cstep, Cflow for the three inputs' own constants, and set

K := max (max 6 (Cstart sqrt(3/2))) (max Cstep Cflow), C := 2 K^3.

Each of the four demands on K is met by construction and is discharged where it is used:

Per model M the terminal budget is E := K c_star^{-1}. The root's own premise gamma ≤ (C^{-1})^{10} c_star^{10} at C = 2K^3 yields both regimes actually needed, gamma ≤ (K^{-1})^{10} c_star^{10} (for the absorption) and gamma ≤ (E^{-1})^{10} (for the two gates), because K ≤ 2K^3 and (E^{-1})^{10} = (K^{-1})^{10} c_star^{10}. The iteration inductionState_of_base_of_step_of_E_le (StateCalculus.lean) then gives S(m, E) m : ℤ.

Constant reconciliation. All four C-slots of the frozen root compose at the single witness C = 2K^3: the regime is a, so the larger constant is the stronger hypothesis (and it implies the regime at K since K ≤ 2K^3 for K ≥ 6); the Gamma_2 amplitude, the Gamma_{1/2} exponent and the sigmaBar defect bound are all U bounds, so the larger constant is the weaker conclusion.

The gap in the printed proof that this module fills #

The printed proof of p.induction.bounds proves exactly S(m, C c_star^{-1}) for every m ∈ Z and then stops. The printed proof never performs that extraction: p.propagate.diffusivity.lower.bound is invoked only for e.shom.h.bounds, and its sharp first conclusion is dropped. Section 9 below, exists_sigmaBar_formula, supplies it: it re-invokes the diffusivity_asymptotics at the auxiliary top scale m0:= max m (mStar M + 1) (legal for every m ∈ Z, since the root's gate is mStar M < m0 and its defect conclusion is a ∀ m ≤ m0 window) and reads off the display at the requested m. No new mathematics is introduced: the whole content is the landmark bookkeeping the print omits.

References #

1. The single induction constant #

K is fixed before every model datum; it is the maximum of the four demands the assembly makes, and the exported constant is 2 K^3.

2. The K ↦ 2 K^3 enlargement #

The two monotonicity facts that make the single exported witness work. Both are pure arithmetic in an opaque real K ≥ 6; no transcendental and no c_star power appears, so the numeric tactics see only linear goals in the atoms K, K * K.

9. The sharp sigmaBar formula at every scale #

The step the printed proof omits (see the module header). The diffusivity_asymptotics delivers its sharp defect display as a ∀ m ≤ m0 window under the landmark gate mStar M < m0. Both are satisfied at once, for an arbitrary requested scale m, by the auxiliary top scale m0:= max m (mStar M + 1); the state at m0 - 1 comes from the all-scale iteration supplied by the caller.

10. The root #

source
theorem Algsuperdiff.Section3.Provider.Induction.induction_bounds_provided (d : ℕ) :
∃ (C : ℝ), 0 < C ∧ ∀ (M : ABKModel d), M.gamma ≤ C⁻¹ ^ 10 * Disorder.cstar M ^ 10 → (∀ (m : ℤ) (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, ⋯⟩) (C * (Disorder.cstar M)⁻¹ * s⁻¹ * √M.gamma) (Real.exp (-(C⁻¹ * Disorder.cstar M ^ 3 * M.gamma⁻¹)))) ∧ ∀ (m : ℤ), |↑(Annealed.sigmaBar M m) - √(M.nu ^ 2 + Disorder.cstar M * M.gamma⁻¹ * 3 ^ (2 * M.gamma * ↑m))| ≤ C * (Disorder.cstar M)⁻¹ ^ 2 * √M.gamma * |Real.log M.gamma| * ↑(Annealed.sigmaBar M m)

p.induction.bounds: the self-similar coarse-graining estimate.

The exported constant is C = 2 K^3 with K = max (max 6 (Cstart sqrt(3/2))) (max Cstep Cflow), chosen after the three inputs' own constants and before every model datum. Under the printed regime gamma ≤ C^{-10} c_star^{10} the induction runs at the terminal budget E = K c_star^{-1} from the base scale m** through the one-scale propagation, giving S(m, E) at every m : ℤ; the first root conjunct is then the proved s-free re-wrapping of the state's error clause, and the second is the sharp defect display of the diffusivity root, read at every scale through §9.

This is a proved local Provider helper. Its statement is the body of the draft Algsuperdiff.Frozen.Section3.induction_bounds; the draft module is deliberately NOT in this file's import closure.