Minimal-walk tree
= Minimal-walk tree
The tree of restrictions $\rho_\beta\upharpoonright\alpha$, ordered by extension. For a <club sequence> on $\omega_2$ with club order types at most $\omega_1$, the <Continuum hypothesis> bounds each level by $\aleph_1$. Trace injectivity and <Fodor lemma> exclude a <cofinal branch>.