One common continuous stable height process

Moment bounds construct a continuous modification. Rational agreement identifies it with heightLoc, reconstructed from heightUniv. Literal prefix locality and uniqueness imply one graph event for all horizons. The compact walk/height law is its graph pushforward.

theorem BGW.StableTrees.ae_heightPrefix_restrict_all {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (T : NNReal) (t : ↑(Set.Icc 0 ↑T)), (heightPrefix θ T (Skorokhod.DLoc.restrict T f)) t = heightLoc θ f ⟨↑t, ⋯⟩

Graph identity on one event for all horizons (CT8 blueprint §2 item 3).

theorem BGW.StableTrees.ae_heightPrefix_restrict {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (T : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (t : ↑(Set.Icc 0 ↑T)), (heightPrefix θ T (Skorokhod.DLoc.restrict T f)) t = heightLoc θ f ⟨↑t, ⋯⟩

Graph identity: almost surely, on every time of [0,T], the prefix map applied to the restriction of the path is the continuous height.

theorem BGW.StableTrees.ae_heightPrefix_eval {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (T : NNReal) (t : ↑(Set.Icc 0 ↑T)) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), (heightPrefix θ T (Skorokhod.DLoc.restrict T f)) t = height θ f ⟨↑t, ⋯⟩

Fixed-time evaluation of the prefix map is H02's height a.s.

theorem BGW.StableTrees.map_heightPrefix_pair {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (T : NNReal) : MeasureTheory.Measure.map (fun (f : Skorokhod.DLoc) => (Skorokhod.DLoc.restrict T f, heightPrefix θ T (Skorokhod.DLoc.restrict T f))) ↑(stableLocalLaw θ) = MeasureTheory.Measure.map (fun (g : Skorokhod.D ↑T ℝ) => (g, heightPrefix θ T g)) ↑(stableProcessLaw θ ↑T)

Pair law: the walk/height pair on [0,T] is the graph pushforward of the stable process law on [0,T] (all T, including T = 0).