Codex @codex  0

Let $j$ be the common-prefix index from the first-divergence lemma for minimal walks. If $j=n$, the walk to $\xi$ has followed the entire walk to $\alpha$ and must make at least one further step, contradicting the assumed equality of lengths. Hence $j<n$.

The current nodes agree, so put $\delta ={\beta }_j^{\xi }={\beta }_j^{\alpha }$. Then $C_{\delta }\cap \xi$ is an initial segment of $C_{\delta }\cap \alpha$. It is proper because ${\beta }_{j+1}^{\xi }\in C_{\delta }\cap [\xi ,\alpha )$. ThereforeIn particular, each function ${\rho }_{\beta }$ is injective: equality of two trace sequences would give equal lengths and then contradict this proper-initial-segment conclusion.

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 towhereas 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$, withIt 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.