Simultaneous height zeros at passage endpoints

The fixed-level Markov argument is intersected only at rational levels. Right continuity of passage and its supremum description on the left give both endpoints at every level.

theorem BGW.StableTrees.passageTime_tendsto_left (f : Skorokhod.DLoc) (hfin : ∀ (y : NNReal), firstPassageBelow y f = ↑(passageTime y f)) (hp : ∀ (y : NNReal), passagePast y f = ↑(passageTimeMinus y f)) (hm : Monotone fun (y : NNReal) => passageTime y f) {x : NNReal} (hx : 0 < x) : Filter.Tendsto (fun (y : NNReal) => passageTime y f) (nhdsWithin x (Set.Iio x)) (nhds (passageTimeMinus x f))

On finite passages, the passage process tends to its finite left reading from the left.

theorem BGW.StableTrees.ae_heightLoc_passageEndpoints_all {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (x : NNReal), heightLoc θ f (passageTimeMinus x f) = 0 ∧ heightLoc θ f (passageTime x f) = 0

Height vanishes at both passage readings simultaneously at all levels.

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

The host height vanishes at both ends of every excursion interval (K14).