Take and choose a club sequence on , each of order type at most . For a successor use its predecessor as a singleton; at a limit use a cofinal sequence of minimal length. Form the minimal-walk tree
ordered by proper extension. Its height is .
For , the initial segment has order type strictly below , and is countable. The strict inequality follows because a point of at or above occurs later in its enumeration. Hence every entry of every trace is countable. Under the Continuum hypothesis, for ,
There are at most finite sequences of such sets. The trace coherence lemma for minimal walks says that, for , the value determines . The case adds at most one node. Thus for every level.
Suppose that had a cofinal branch, and take the union of its functions, , with domain . Every is injective by the proper-initial-segment argument, so is injective too. On the stationary set
this set is stationary because the supremum of a strictly increasing -sequence from any club set has cofinality and lies in that club. The union of the finitely many countable entries of is bounded below . Assign a strict upper bound below to obtain a regressive function. By Fodor lemma, there is a stationary and a single such that every entry of lies inside for . There are at most such finite sequences by the same cardinal arithmetic, but , contradicting injectivity.
Therefore is an aleph-two Aronszajn tree: