Almost sure finiteness of ladder times

Extinction normalizes the law of first passage to level -1, so the walk reaches -1 almost surely. Shift invariance then gives such a passage below every starting value, simultaneously at every integer time. This avoids a separate general random-walk oscillation theorem.

theorem BGW.StableTrees.DiscreteForest.ae_ladderFinite (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) : ∀ᵐ (ω : ℕ → ℕ) ∂↑(offspringSeqLaw μ), LadderFinite ω

Critical nondegenerate walks reach every level downward a.s.