The weak ascending ladder-height law

A last-step decomposition combines exact pre-return occupations with an independent offspring coordinate. The resulting height law is the offspring tail, including its atom at zero.

theorem BGW.StableTrees.DiscreteHeightApprox.weakEpochHeight_one_law (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (j : ℕ) : ↑(DiscreteForest.offspringSeqLaw μ) {ω : ℕ → ℕ | weakEpochHeight ω 1 = j} = μ.toMeasure (Set.Ici (j + 1))

The first weak ascending ladder height has the offspring-tail law, with its zero atom.