Tightness of all interpolated forest-height laws

Uniform modulus estimates over every scaling index and a summable allocation of exceptional probabilities give one compact path set. The paths start at zero, and Arzelà-Ascoli supplies compactness. The zero horizon is handled directly.

theorem BGW.StableTrees.HeightTightness.isTightMeasureSet_forestHeightLaw {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) (T : NNReal) : MeasureTheory.IsTightMeasureSet (Set.range fun (n : ℕ) => ↑((DiscreteForest.offspringSeqLaw μ).map (DiscreteForest.forestHeightPath B n T)))

The laws of the normalized height paths on [0,T] are tight.