Identification and convergence of the localized selected pair

The limit height is the common continuous host height cut at the first long excursion.

theorem BGW.StableTrees.TailPair.ae_cutHeightPath_firstLongMark {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (M T : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), (firstLongEnds f).2 ≤ ↑M → cutHeightPath M T (heightPrefix θ M (Skorokhod.DLoc.restrict M f)) (firstLongEnds f).1 (firstLongEnds f).2 = (excursionPair θ T (firstLongMark f)).2

At the first long mark the centered host-height cut is the excursion height.