Rational bounds at countable limit levels

Fix enumerations of $T$ and $\delta$. From an enumeration $d:\omega \to \delta$, define ${\gamma }_0=d(0)$ and ${\gamma }_{k+1}=\max \{{\gamma }_k+1,d(k+1)\}$. All terms lie below the limit $\delta$ and ${\gamma }_k\ge d(k)$, so the sequence is cofinal. By F1 and F2, $T\times \mathbb{Q}$ has an enumeration. Keep precisely the entries $(x,r)$ with $\mathrm{\ell }(x)<r$ to enumerate all requests as $(x_n,r_n)$. There are infinitely many entries to keep, since for one fixed $x$ the distinct rationals $\mathrm{\ell }(x)+m+1$ give requests for all natural $m$. Retaining successive least valid indices is recursion, not countable choice.

Suppose branches $b_0,\dots ,b_{n-1}$ for the earlier requests have been defined. Set $q_n=(\mathrm{\ell }(x_n)+r_n)\mathrm{/}2$, so $\mathrm{\ell }(x_n)<q_n<r_n$. Infinitely many immediate successors of $x_n$ have labels below $q_n$. Each earlier branch contains at most one of them, since distinct immediate successors are incomparable by F5. Thus finitely many earlier branches exclude at most finitely many candidates. Choose the least enumerated remaining successor $z_0$; it has label below $q_n$ and belongs to none of the earlier branches.

Recursively, with $z_k$ already defined, put ${\eta }_k=\max \{{\gamma }_k,\mathrm{ht}(z_k)+1\}<\delta$. The first invariant gives an extension $z_{k+1}$ of height ${\eta }_k$ and label below $q_n$, since $\mathrm{\ell }(z_k)<q_n$. Take the least enumerated such extension. This defines a strictly increasing chain whose heights are cofinal and whose labels are all less than $q_n$. Recursion uses the state $(k,z_k)$, and the successor bound stays below $\delta$ because it is limit.

Let $b_n=\{s:\mathrm{\exists }ks{\le }_T{z}_k\}$. Common-predecessor comparability makes this a chain; its cofinality and unique predecessors give exactly one node of each height below $\delta$. A node comparable with all of $b_n$ lies below some $z_k$ of greater height and hence belongs to $b_n$, so it is a maximal chain. Every label on $b_n$ is less than $q_n$: for $s{\le }_T{z}_k$, strict increase gives $\mathrm{\ell }(s)\le \mathrm{\ell }(z_k)<q_n$. It contains $x_n$ and $z_0$, and $z_0$ belongs to no earlier branch, so $b_n$ differs from all of them. This construction determines $b_n$ uniquely from the finite list of previous branches; recursion on finite lists therefore produces all $b_n$ simultaneously.

Adjoin a distinct top $v_n$ above precisely $b_n$, with label $q_n$. Formally use the disjoint union of a tagged copy of $T$ and a tagged copy of $\omega$, ordered by the old order and $s<v_n$ iff $s\in b_n$. A branch is downward closed, so this order is transitive. The predecessor set of $v_n$ is ordered like $\delta$ by height, proving that these are exactly a new level at $\delta$. Their predecessor sets are distinct by step 4.1. The new tree is countable by interleaving its old enumeration with $n\mapsto v_n$. Strict increase holds on new comparisons because $\mathrm{\ell }(s)<q_n=\mathrm{\ell }(v_n)$ for $s\in b_n$; there are no comparisons between new tops.

For any old $x$ and rational $r>\mathrm{\ell }(x)$, its request occurs at some $n$. Then $x{<}_T{v}_n$ and $\mathrm{\ell }(v_n)=q_n<r$, proving the invariant at the new level. Earlier instances are unchanged and new tops have no higher level to check. If the old tree is normal, its root and old limit-level uniqueness persist, the request argument supplies extensions to the new level, and step 5.1 supplies new limit-level uniqueness. No immediate successors of old nodes are lost or changed, since their successor heights are strictly below $\delta$; new tops have no successor requirement. Every selection used least indices after finitely many fixed enumerations.