Full-sequence coupling for localized long-block extraction

The compact-horizon FCLT is represented along the entire sequence. Graph disintegration lifts the limit to the local stable law. Reconstructed mesh increments then satisfy K04 on the K05 good event, with no subsequence change of the mesh index.

theorem BGW.StableTrees.PathTail.exists_localized_extraction_coupling {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) (M T : NNReal) (hM : 0 < M) (hT : 0 < T) : ∃ (η : MeasureTheory.ProbabilityMeasure (↑unitInterval × Skorokhod.DLoc)) (Y : ℕ → ↑unitInterval × Skorokhod.DLoc → Skorokhod.D ↑M ℝ), (∀ (n : ℕ), Measurable (Y n)) ∧ (∀ (n : ℕ), MeasureTheory.Measure.map (Y n) ↑η = ↑(stepPathLaw (realOffspringStepLaw μ) (↑M) B n)) ∧ MeasureTheory.Measure.map Prod.snd ↑η = ↑(stableLocalLaw θ) ∧ ∀ᵐ (p : ↑unitInterval × Skorokhod.DLoc) ∂↑η, (∀ (n i : ℕ), IsSkipFreeIncrement (reconstructIncrements M n (B n) (Y n p) i)) ∧ (passageTime (firstLongLabel p.2) p.2 < M → Filter.Tendsto (fun (n : ℕ) => extractionTriple (B n) n T (reconstructIncrements M n (B n) (Y n p))) Filter.atTop (nhds (longCutTriple T p.2)) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, firstLongIndex n (reconstructIncrements M n (B n) (Y n p)) ∈ longBlockSet n (reconstructIncrements M n (B n) (Y n p)) ∧ ladderTime (reconstructIncrements M n (B n) (Y n p)) (firstLongIndex n (reconstructIncrements M n (B n) (Y n p)) + 1) ≤ ⌊↑n * ↑M⌋₊)

A full-sequence compact-path coupling with a local stable limit, reconstructed skip-free increments, and K04 extraction convergence on the event that the limiting end precedes M.