BadEventMultiscaleConsumption

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

Bad-event estimate at the multiscale parameters

This module applies the frozen bad-event theorem to the event at scales (l, l - h). Its private arithmetic derives the theorem's admissibility, fifth-root, nonlinear-time, and entropy/exponential gates from the scale separation hypotheses used by the multiscale argument.

theorem Algsuperdiff.Section3.Provider.BadEvents.exists_measureReal_compl_goodLocalEventAt_le_of_multiscaleParameters (d : ℕ) : ∃ (Ccg : ℝ) (c : ℝ), 1 ≤ Ccg ∧ 0 < c ∧ ∀ (H : ℝ), 0 ≤ H → ∃ (C : ℝ), 1 ≤ C ∧ ∀ (M : ABKModel d) (m0 : ℤ) (E : { E : ℝ // 1 ≤ E }) (epsilon : ℝ) (h : ℕ) (l : ℤ), Frozen.Section3.inductionState M (m0 - 1) E → epsilon ∈ Set.Ioc 0 (1 / 2) → ↑h ≤ H * |Real.log epsilon| + 1 → (Disorder.cstar M)⁻¹ * epsilon ^ (-C) ≤ ↑E → M.gamma ≤ (↑E)⁻¹ ^ 10 → l - ↑h ≤ m0 - 1 → ∀ (z : HCPolySupport.Vec d), (↑(Cutoff.cutoffSampleLaw M)).real (Frozen.Section3.goodLocalEventAt M (2 * Ccg) l (l - ↑h) z)ᶜ ≤ Real.exp (-(c * Disorder.cstar M * M.gamma⁻¹ * 3 ^ (-5 * scaleGapPos (l - ↑h) l) * 3 ^ scaleGapPos l (l - ↑h))) + Real.exp (-Real.exp (c * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))

Direct use of the frozen bad-event estimate at the multiscale event goodLocalEventAt M _ l (l - h) z. The two branch-guard estimates are consequences of the paper's scale separation, not caller-supplied proof obligations. The bad-event constants Ccg and c are selected before H; only the scale exponent C depends on H.