Uniform cutoff plateau around a compact region

A compact subset above the negative phase gap lies in the plateau of every sufficiently wide spatial cutoff and every sufficiently short lower-time cutoff.

theorem ESS.bu_short_compact_subset_core_eventually (scale : ℝ) (S : Set CKN.Foundation.Parabolic.ParabolicPoint) (hScompact : IsCompact S) (hSne : S.Nonempty) (hSgap : ∀ z ∈ S, CKN.Foundation.Parabolic.parabolicHomeomorph z ∈ buShortAboveGap scale) : ∃ (R₀ : ℝ) (ε₀ : ℝ), 1 ≤ R₀ ∧ 0 < ε₀ ∧ ∀ (R : ℝ), R₀ ≤ R → ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∀ z ∈ S, CKN.Foundation.Parabolic.parabolicHomeomorph z ∈ buShortCoreRegion scale R ε

A compact region above the phase gap stays in the open cutoff plateau for all large radii and small lower-time widths.