Solution (source code)

= Solution

For clarity, each $\rho_\beta(\alpha)$ is an ordered finite sequence. Its <minimal walk along a club sequence> is finite because its nodes strictly decrease until reaching $\alpha$, and an infinite strictly decreasing sequence of <ordinals> cannot exist. At a step from $\delta>\alpha$, unboundedness of $C_\delta$ supplies $\min(C_\delta\setminus\alpha)$ in $[\alpha,\delta)$.

Compare the two <minimal walks along a club sequence> to $\xi$ and to $\alpha$. As long as their current node is the same $\delta>\alpha$, their next nodes agree exactly when $C_\delta$ has no point in $[\xi,\alpha)$. At the first such point, the walk to $\xi$ moves to
$$
\min(C_\delta\setminus\xi)\in[\xi,\alpha),
$$
whereas the walk to $\alpha$ stays at or above $\alpha$. If this does not occur before the second walk terminates, the first walk reaches $\alpha$ with it and then makes its next step below $\alpha$.

Thus there is an index $j$, possibly the terminal index of the walk to $\alpha$, with
$$
\boxed{\beta_i^\xi=\beta_i^\alpha\ (i\leq j),\qquad
\xi\leq\beta_{j+1}^\xi<\alpha.}
$$
It is unique: after this step the first walk stays below $\alpha$, so it can never again coincide with a node of the walk to $\alpha$. This is the <first-divergence lemma for minimal walks>.