Good endpoints of tail-excursion prefixes

The absence of fixed jumps under the excursion measure transfers to its normalized tail.

theorem BGW.StableTrees.ExactPrefix.ae_tailPrefix_continuousAt_pos {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) : ∀ᵐ (x : Skorokhod.D ↑a ℝ) ∂↑(PathTail.tailPrefixLimit θ a), ContinuousAt ⇑x ⟨↑a, ⋯⟩ ∧ 0 < DiscreteBridge.endValue a x

The tail-excursion prefix is almost surely continuous at a with positive value (N_noFixedJump, tailExcursionLaw ≪ N, positivity before the end).