The index-two excursion height

Brownian path continuity extends the fixed-time height formula on host paths. Excursion locality and compensation identify the marks; the shape/lifetime law transfers the identity to unit excursions with matching space and height exponents.

theorem BGW.StableTrees.ae_heightLoc_two_for_excursion : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw 2), ∀ (t : NNReal), heightLoc 2 f t = ↑f t - runningInfLoc f t

C26 (K17). At θ = 2, almost surely, the continuous height is X - I at every time.

theorem BGW.StableTrees.continuous_eq_dLoc_iff_rat (g : C(NNReal, ℝ)) (f : Skorokhod.DLoc) : (∀ (t : NNReal), g t = ↑f t) ↔ ∀ (q : ℚ), g (↑q).toNNReal = ↑f (↑q).toNNReal

A continuous function and a càdlàg path agree everywhere iff they agree at rational ages.

theorem BGW.StableTrees.measurableSet_excursionHeight_eq_path (θ : ℝ) : MeasurableSet {e : Excursion | ∀ (t : NNReal), (excursionHeight θ e) t = ↑e.path t}

The all-age equality of the continuous height with the excursion path is Borel.

theorem BGW.StableTrees.ae_excursionHeight_two : ∀ᵐ (e : Excursion) ∂excursionMeasure 2, ∀ (t : NNReal), (excursionHeight 2 e) t = ↑e.path t

At θ = 2 (variance-2 library process, H = X - I) the excursion height is the excursion path, N-a.e.

theorem BGW.StableTrees.ae_excursionHeight_two_unit : ∀ᵐ (e : Excursion) ∂↑(unitExcursionLaw 2), ∀ (t : NNReal), (excursionHeight 2 e) t = ↑e.path t

At θ = 2 the excursion height is the excursion path under the unit law (K18).