Excluding early long discrete blocks

A hypothetical sequence of early long blocks has compact endpoint limits. Their running infima agree, contradicting the least-long-label property.

theorem BGW.StableTrees.eventually_no_early_longBlock {B : ℕ → ℝ} (hB : Filter.Tendsto B Filter.atTop Filter.atTop) {M : NNReal} (ω : ℕ → ℕ → ℝ) (hω : ∀ (n i : ℕ), IsSkipFreeIncrement (ω n i)) {f : Skorokhod.DLoc} (hf : GoodLongExtractionPath M f) (hu : Filter.Tendsto (fun (n : ℕ) => Skorokhod.realStepPath (↑M) n (B n) (ω n)) Filter.atTop (nhds (Skorokhod.DLoc.restrict M f))) {H : NNReal} (hHM : H ≤ M) (hH : H < passageTimeMinus (firstLongLabel f) f + 1) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ r ∈ longBlockSet n (ω n), ↑H < ↑(ladderTime (ω n) (r + 1)) / ↑n

Long blocks cannot end before a fixed time strictly below the first start plus one. Reference: Billingsley (1999), Chapter 3.