Club sequence ($⟨C_{\delta }⟩$)

A sequence $⟨C_{\delta }⟩$ in which $C_{\delta }$ is closed and unbounded in $\delta$. At a successor ordinal its predecessor is a club singleton. Such sequences define minimal walks along a club sequence.

To walk from $\beta$ to $\alpha <\beta$, start at $\beta$ and repeatedly move from $\delta$ to $\min (C_{\delta }\setminus \alpha )$ until reaching $\alpha$. The strict decrease in ordinals makes the walk finite. Its trace records the successive $C_{\delta }\cap \alpha$.

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.

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.

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.