Universal height sequence by predicates on subsequences

The six countable families retain their own laws. The common extraction diagonalizes their convergence predicates, including the finite survival-restricted excursion age windows.

theorem BGW.StableTrees.exists_isUniversalHeightSeq {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∃ (ε : ℕ → ℝ), IsUniversalHeightSeq θ ε

A universal sequence exists (diagonal extraction from the in-measure statements). The excursion age windows use the finite survival restriction of volume ⊗ N. Joint limits are obtained by the Cauchy criterion, without choosing a family of fixed-age limits.

theorem BGW.StableTrees.isUniversalHeightSeq_heightEps {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : IsUniversalHeightSeq θ (heightEps θ)

The chosen universal cutoffs satisfy the full sequence specification.