Excursion locality and existence of the continuous version

The continuous host height stopped at the excursion endpoint is a version of each mark. Translation preserves the host's exceptional time set, and exact cancellation identifies the interior raw heights. Uniqueness proves locality and the non-junk assertion together.

theorem BGW.StableTrees.ae_jumpExcursion_heightVersion {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ x ∈ passageJumpSet f, (∃ (g : C(NNReal, ℝ)), IsExcursionHeightVersion θ (jumpExcursion x f) g) ∧ ∀ (t : NNReal), (excursionHeight θ (jumpExcursion x f)) t = if t ≤ passageTime x f - passageTimeMinus x f then heightLoc θ f (passageTimeMinus x f + t) else 0

Locality and non-junk on one event: almost surely, for every passage jump level x, the attached excursion has an a.e.-age height version, and its height is the continuous host height t ↦ heightLoc θ f (T(x-) + t) on [0, T(x) - T(x-)], zero after.

theorem BGW.StableTrees.ae_heightLoc_jumpExcursion {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ x ∈ passageJumpSet f, ∀ t ≤ passageTime x f - passageTimeMinus x f, heightLoc θ f (passageTimeMinus x f + t) = (excursionHeight θ (jumpExcursion x f)) t

Simultaneous excursion locality: almost surely, for every passage jump level x and every 0 ≤ t ≤ T(x) - T(x-), the continuous height of the stable process at T(x-) + t is the height of the excursion attached to x at time t.