First-divergence lemma for minimal walks
= First-divergence lemma for minimal walks
The walks to $\xi<\alpha$ share a unique maximal initial chain of nodes. At the next step the walk to $\xi$ moves into $[\xi,\alpha)$; the walk to $\alpha$ stays at or above $\alpha$ or has just ended.