Finite-prefix localization of the selected block

A selected long block ending within an observed prefix is unchanged by any modification of the subsequent increments. This includes its endpoints and closed cut on every output horizon.

theorem BGW.StableTrees.PathTail.extractionTriple_eq_of_prefix {ω ξ : ℕ → ℝ} {N n : ℕ} (h : ∀ i < N, ω i = ξ i) (hmem : firstLongIndex n ω ∈ longBlockSet n ω) (hend : ladderTime ω (firstLongIndex n ω + 1) ≤ N) (b : ℝ) (T : NNReal) : extractionTriple b n T ξ = extractionTriple b n T ω

If a selected long block ends in an observed prefix, modifying later increments does not change its extracted endpoints or cut path.