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 the long-block extraction convergence on the first-long-mark good event, with no subsequence change of the mesh index.

theorem BGW.StableTrees.TailPair.exists_localized_pair_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 ℝ × C(↑(Set.Icc 0 ↑M), ℝ)), (∀ (n : ℕ), Measurable (Y n)) ∧ (∀ (n : ℕ), MeasureTheory.Measure.map (Y n) ↑η = ↑((DiscreteForest.offspringSeqLaw μ).map (DiscreteForest.forestPairPath B n M))) ∧ MeasureTheory.Measure.map Prod.snd ↑η = ↑(stableLocalLaw θ) ∧ ∀ᵐ (p : ↑unitInterval × Skorokhod.DLoc) ∂↑η, Filter.Tendsto (fun (n : ℕ) => Y n p) Filter.atTop (nhds (Skorokhod.DLoc.restrict M p.2, heightPrefix θ M (Skorokhod.DLoc.restrict M p.2))) ∧ (∀ (n i : ℕ), IsSkipFreeIncrement (PathTail.reconstructIncrements M n (B n) (Y n p).1 i)) ∧ (passageTime (firstLongLabel p.2) p.2 < M → Filter.Tendsto (fun (n : ℕ) => extractionTriple (B n) n T (PathTail.reconstructIncrements M n (B n) (Y n p).1)) Filter.atTop (nhds (longCutTriple T p.2)) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, firstLongIndex n (PathTail.reconstructIncrements M n (B n) (Y n p).1) ∈ longBlockSet n (PathTail.reconstructIncrements M n (B n) (Y n p).1) ∧ ladderTime (PathTail.reconstructIncrements M n (B n) (Y n p).1) (firstLongIndex n (PathTail.reconstructIncrements M n (B n) (Y n p).1) + 1) ≤ ⌊↑n * ↑M⌋₊)

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