Trace coherence lemma for minimal walks
= Trace coherence lemma for minimal walks
{title2=$\rho_\beta\upharpoonright\alpha=\rho_\gamma\upharpoonright\alpha$}
If $\rho_\beta(\alpha)=\rho_\gamma(\alpha)$, then the trace functions agree below $\alpha$. Each shorter trace is reconstructed by locating the first recorded club initial segment that meets $[\xi,\alpha)$ and continuing the walk from its least such point.