Measurability of the selected long block

Discrete first hits, selection, endpoints and closed increments are measurable even on sequences with infinite ladder times, with the sealed totalization conventions.

theorem BGW.StableTrees.PathTail.measurable_extractionTriple (b : ℝ) (n : ℕ) (T : NNReal) : Measurable (extractionTriple b n T)

The selected endpoint/cut triple is measurable for every scale, including junk branches.

theorem BGW.StableTrees.PathTail.measurableSet_extractionLocalEvent (N n : ℕ) : MeasurableSet {ω : ℕ → ℝ | firstLongIndex n ω ∈ longBlockSet n ω ∧ ladderTime ω (firstLongIndex n ω + 1) ≤ N}

The event that the selected block exists, is long, and ends within a fixed prefix is measurable, with the sealed finite-hit guard.