Fixed-age unit identification through the common prefix graph

The finite prefix density transfers full-filter convergence after both laws' continuous heights have been identified with the same measurable prefix functional.

theorem BGW.StableTrees.heightApprox_tendstoInMeasure_excursionHeight_unit {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) (ht0 : 0 < t) (ht1 : t < 1) : MeasureTheory.TendstoInMeasure (↑(unitExcursionLaw θ)) (fun (ε : ℝ) (e : Excursion) => heightApprox ε e.path t) (nhdsWithin 0 (Set.Ioi 0)) fun (e : Excursion) => (excursionHeight θ e) t

Identification under the unit law at ages 0 < t < 1.