Absence of an exploration atom at the root

Strict growth after upward passages transfers through bounded prefix laws. At a fixed horizon, zero-height ancestors lie at the initial future-infimum level. Rational horizons extend this statement simultaneously; upward jumps and continuous endpoints handle atoms.

theorem BGW.StableTrees.measurable_supLocalTime_prefix_eval (θ : ℝ) (T : NNReal) : Measurable fun (p : Skorokhod.DLoc × ↑(Set.Iic T)) => supLocalTime θ p.1 ↑p.2

Joint prefix measurability of the clock and its bounded evaluation time.

theorem BGW.StableTrees.ae_reversed_passage_clock_growth {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {T : NNReal} (hT : 0 < T) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (q : ℚ), have g := reversedAt T f; have τ := Skorokhod.DLoc.strictPassageAbove (↑(↑q).toNNReal) g; τ < ↑T → ∀ (r : NNReal), τ.toNNReal < r → r ≤ T → supLocalTime θ g τ.toNNReal < supLocalTime θ g r

Upward-passage clock growth is available inside a reversed prefix.

theorem BGW.StableTrees.leftLim_supRunning_reversedAt (f : Skorokhod.DLoc) {t s : NNReal} (hst : s < t) (hf : ∀ (r : NNReal), Function.leftLim (↑f) r ≤ ↑f r) : Function.leftLim (supRunning (reversedAt t f)) (t - s) = ↑f t - futureInf f t s

Left limits of the reversed supremum are terminal value minus the future infimum.

theorem BGW.StableTrees.ae_zero_height_ancestor_inf {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (s : NNReal), 0 < s → s ≤ t → Function.leftLim (↑f) s ≤ futureInf f t s → height θ f s = 0 → futureInf f t s = futureInf f t 0

A zero-height ancestor of a fixed horizon lies at the initial future-infimum level.

theorem BGW.StableTrees.futureInf_split (f : Skorokhod.DLoc) {s q t : NNReal} (hsq : s ≤ q) (hqt : q ≤ t) : futureInf f t s = min (futureInf f q s) (futureInf f t q)

Splitting a future-infimum window at an intermediate horizon.

theorem BGW.StableTrees.exists_rat_ancestor_of_jump (f : Skorokhod.DLoc) {s : NNReal} (hs : Function.leftLim (↑f) s < ↑f s) : ∃ (q : ℚ), ↑s < ↑q ∧ Function.leftLim (↑f) s < futureInf f (↑q).toNNReal s

Upward jumps remain ancestral to some rational later horizon.

theorem BGW.StableTrees.futureInf_zero_le_leftLim (f : Skorokhod.DLoc) {s t : NNReal} (hs : 0 < s) (hst : s ≤ t) : futureInf f t 0 ≤ Function.leftLim (↑f) s

A positive-time left limit bounds the future infimum from the root.

theorem BGW.StableTrees.ae_zero_height_ancestor_inf_all {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (t s : NNReal), 0 < s → s < t → Function.leftLim (↑f) s ≤ futureInf f t s → height θ f s = 0 → futureInf f t s = futureInf f t 0

One null set controls zero-height ancestors at all strict later horizons.

theorem BGW.StableTrees.ae_height_pos_at_jumps {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (s : NNReal), Function.leftLim (↑f) s < ↑f s → 0 < height θ f s

Every upward jump has positive height, on a single full-measure set.

theorem BGW.StableTrees.explorationStieltjes_no_atom_of_leftLim_eq (f : Skorokhod.DLoc) {t : NNReal} (ht : 0 < t) (he : Function.leftLim (↑f) t = ↑f t) : (explorationStieltjes f t).measure {↑t} = 0

At a terminal continuity point, the future-infimum Stieltjes measure has no atom.

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

No root atom: a.s., simultaneously for all t, ρ_t has no atom at height 0.