MinimalScaleFinal

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

The outer constant is 2 · max (zTwoConst d) (zOneConst d): the Z^{(2)} leg's d-only floor and the Z^{(1)} leg's, doubled so that each leg's tail carries half the prefactor.

It does NOT import the anchor.

theorem Algsuperdiff.Section4.Provider.MinimalScale.minimal_scale_separation_provider (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d) (s delta : ℝ), s ∈ Set.Ioc 0 (1 / 4) → delta ∈ Set.Ioc 0 (1 / 2) → M.gamma ≤ C⁻¹ ^ 10 * min (Section3.Disorder.cstar M ^ 10) (delta ^ 2 * Section3.Disorder.cstar M ^ 2 * s ^ 9) → 8 * M.gamma ≤ s → ∀ (m : ℤ) (hs : 0 < s), ∃ (Z : Section3.Cutoff.CutoffSample d → ℕ∞), Measurable Z ∧ (∀ (N : ℕ), ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | ↑N ≤ Z omega} ≤ ENNReal.ofReal (C * Real.exp (-((↑N - 1) * s ^ 9 * Section3.Disorder.cstar M ^ 2 * delta ^ 2) / (C * M.gamma)))) ∧ ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ n ≤ m, Z omega ≤ ↑(m - n).toNat → ⨆ (z : ↑(Support.latticeCubeSet d (n - 1) m)), (↑(m - n).toNat + 1)⁻¹ * ∑ k ∈ Finset.Icc n m, (Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) k (Support.triadicLatticePoint (n - 1) ↑z) ⟨s, hs⟩ (s * √delta)).indicator (fun (omega' : Section3.Cutoff.CutoffSample d) => Support.fluxCorrectedErrorObservableSup M k ⟨s, hs⟩ (Section3.Cutoff.translateCutoffSample (Support.triadicLatticePoint (n - 1) ↑z) omega')) omega ≤ ENNReal.ofReal delta ∧ ⨆ (z : ↑(Support.latticeCubeSet d (n - 1) m)), (↑(m - n).toNat + 1)⁻¹ * ∑ k ∈ Finset.Icc n m, (Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) k (Support.triadicLatticePoint (n - 1) ↑z) ⟨s, hs⟩ (s * √delta))ᶜ.indicator (fun (x : Section3.Cutoff.CutoffSample d) => 1) omega ≤ ENNReal.ofReal delta

The frozen minimal-scale-separation statement, proved.