Identifying discrete and limiting cut-path laws

K02 identifies the selected closed block with the tail-conditioned tree law. The limiting cut is the first long mark, whose law is the independent tail excursion law.

theorem BGW.StableTrees.PathTail.map_selectedBlockCut_eq_closedTail {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) (n : ℕ) (T : NNReal) : ((Probability.RealWalk.iidLaw (realOffspringStepLaw μ)).map fun (ω : ℕ → ℝ) => (extractionTriple (B n) n T ω).2.2) = (DiscreteForest.tailTreeLaw μ n).map fun (τ : LocallyFinite.Tree) => Skorokhod.realStepPath (↑T) n (B n) (closedTreeIncrementSeq τ)

The path coordinate of the selected-block triple is the closed path of a tail-conditioned BGW tree, by the exact K02/K04 coding adapter.

theorem BGW.StableTrees.PathTail.map_longCutTriple_path {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (T : NNReal) : (((stableLocalLaw θ).map (longCutTriple T)).map fun (p : ℝ × ℝ × Skorokhod.D ↑T ℝ) => p.2.2) = tailLevyExcLaw θ T

Projecting the limiting endpoint/cut triple gives the sealed tail excursion path law.