Height zeros at fixed passage levels

Strong Markov at strict passage gives a fresh stable path. Regularity below zero empties the old occupation, and continuous restart identifies the height at passage with the fresh zero.

theorem BGW.StableTrees.map_shiftAt_firstPassageBelow {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x : NNReal) : MeasureTheory.Measure.map (Skorokhod.DLoc.shiftAt (firstPassageBelow x)) ↑(stableLocalLaw θ) = ↑(stableLocalLaw θ)

The post-passage centered path has the full local stable law at each fixed level.

theorem BGW.StableTrees.futureInf_neg_of_regularBelowAtZero {g : Skorokhod.DLoc} (hg : g.RegularBelowAtZero) {u : NNReal} (hu : 0 < u) : futureInf g u 0 < 0

Regularity below zero implies a negative future infimum at every positive age.

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

At every fixed passage level the continuous host height is zero almost surely.