Simultaneous ancestral height identification

A countable intersection over rational horizons identifies every ancestral time. The Stieltjes source is carried by strict ancestors and upward-jump endpoints, so this event also gives the simultaneous measure-level bridge without Lebesgue disintegration.

theorem BGW.StableTrees.exists_rat_horizon_of_ancestor (f : Skorokhod.DLoc) {t s : NNReal} (ha : s < t ∧ Function.leftLim (↑f) s ≤ futureInf f t s ∨ s = t ∧ Function.leftLim (↑f) t < ↑f t) : ∃ (q : ℚ), 0 < ↑q ∧ s ≤ (↑q).toNNReal ∧ Function.leftLim (↑f) s ≤ futureInf f (↑q).toNNReal s

Each ancestor is ancestral to a strictly positive rational horizon.

theorem BGW.StableTrees.ae_heightApprox_ancestral {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (t s : NNReal), s < t ∧ Function.leftLim (↑f) s ≤ futureInf f t s ∨ s = t ∧ Function.leftLim (↑f) t < ↑f t → Filter.Tendsto (fun (k : ℕ) => heightApprox (supEps θ k) f s) Filter.atTop (nhds (height θ f s)) ∧ 0 ≤ height θ f s ∧ heightRaw θ f s = ENNReal.ofReal (height θ f s)

Ancestral convergence (one null set; all t and all ancestral s ≤ t at once): at an ancestral time s (X_{s-} ≤ I^s_t with s < t, or an upward jump of X at s = t) the approximations along supEps θ converge to the finite nonnegative H_s, and the raw height is the genuine finite ofReal.

theorem BGW.StableTrees.ae_exploration_strict_or_jump (f : Skorokhod.DLoc) (hf : ∀ (r : NNReal), Function.leftLim (↑f) r ≤ ↑f r) (t : NNReal) : ∀ᵐ (s : ℝ) ∂(explorationStieltjes f t).measure.restrict (Set.Ioc 0 ↑t), s.toNNReal < t ∧ Function.leftLim (↑f) s.toNNReal ≤ futureInf f t s.toNNReal ∨ s.toNNReal = t ∧ Function.leftLim (↑f) t < ↑f t

The Stieltjes source measure is carried by strict ancestors and upward-jump endpoints.

theorem BGW.StableTrees.ae_heightRaw_eq_stieltjes {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (t : NNReal), ∀ᵐ (s : ℝ) ∂(explorationStieltjes f t).measure.restrict (Set.Ioc 0 ↑t), 0 ≤ height θ f s.toNNReal ∧ heightRaw θ f s.toNNReal = ENNReal.ofReal (height θ f s.toNNReal)

Measure-level bridge (endpoint atoms retained): a.s., for every t, the random Stieltjes measure of x ↦ I^x_t on (0,t] is carried by times where H is finite, nonnegative and equal to the raw height. Must be proved by Stieltjes ancestral concentration, NOT by Fubini against Lebesgue measure from ae_heightRaw_eq.