Real algebraic numbers are countably infinite, without choice

The decoding is total and assigns to every $n$ a finite list of integers. For $n$, [F2] gives $d,s\in \mathbb{N}$ with $J^{-1}(n)=(d,s)$ and the sequences $T,U$; then $a_k=z(U(k))$ is an integer for each $k\le d$, so $(a_0,\dots ,a_d)$ is a finite integer list. Define $P_n(x):={\sum }_{k=0}^d{a}_k^{\ast }{x}^k$ when $a_d\mathrm{\ne }0$, and $P_n(x):=1$ when $a_d=0$; in both cases $P_n:\mathbb{R}\to \mathbb{R}$ is given by a finite sum of real powers, and $R_n:=\{x\in \mathbb{R}:P_n(x)=0\}$ is a set by Separation. Finally $A:=\{x\in \mathbb{R}:P_n(x)=0\text{ for some }n\in \mathbb{N}\}$ is a set by Separation; every element of this set is real algebraic, since a fallback code has no roots. The converse follows from the coefficient coding below.

Unique increasing listings. For every finite $S\subseteq \mathbb{R}$ and its unique $m\in \mathbb{N}$ with $S\approx m$, there is exactly one increasing bijection $\mathrm{\ell }:m\to S$. Prove this by induction on $m$. At $m=0$, $S=\mathrm{\varnothing }$ and the empty function is the unique listing. At $m=\sigma (m^{\mathrm{\prime }})$, let $s=\min S$, which exists by [F4]. Transport $T=S\setminus \{s\}$ into a subset of $m$ using a bijection $S\to m$; [F4] makes $T$ finite, say $T\approx m^{\mathrm{\prime }\mathrm{\prime }}$. Extending a bijection $T\to m^{\mathrm{\prime }\mathrm{\prime }}$ by $s\mapsto m^{\mathrm{\prime }\mathrm{\prime }}$ gives $S\approx \sigma (m^{\mathrm{\prime }\mathrm{\prime }})$, because $m^{\mathrm{\prime }\mathrm{\prime }}\mathrm{\notin }{m}^{\mathrm{\prime }\mathrm{\prime }}$. Uniqueness of finite cardinality and successor injectivity give $m^{\mathrm{\prime }\mathrm{\prime }}=m^{\mathrm{\prime }}$ by [F5]. The induction hypothesis, including the empty case, gives an increasing bijection ${\mathrm{\ell }}^{\mathrm{\prime }}:m^{\mathrm{\prime }}\to T$. Define $\mathrm{\ell }(0)=s$ and $\mathrm{\ell }(\sigma (i))={\mathrm{\ell }}^{\mathrm{\prime }}(i)$ for $i\in m^{\mathrm{\prime }}$. By [F8] these clauses cover $\sigma (m^{\mathrm{\prime }})$; they give a bijection and preserve order because $s$ is strictly below every member of $T$ and successor preserves the index order. For uniqueness, any increasing bijection sends $0$ to $\min S$; deleting this value gives an increasing bijection $m^{\mathrm{\prime }}\to T$, unique by the induction hypothesis.

Every valid list is coded. Given integers $a_0,\dots ,a_d$ with $a_d\mathrm{\ne }0$, define $u_k:=\min \{u\in \mathbb{N}:z(u)=a_k\}$ for each $k\le d$. These sets are nonempty by [F1], and [F8] supplies unique least values, so the finite function $k\mapsto u_k$ is defined without choice. Form $t_{d+1}=0$ and $t_k=J(u_k,t_{k+1})$ backwards for $k=d,\dots ,0$. To justify this finite recursion with a total self-map, carry a counter $j$ and an accumulator $v$, start at $(0,0)$, and send $(j,v)$ to $(\sigma (j),J(u_{d-j},v))$ when $j\le d$, leaving the state fixed when $j>d$. Recursion on $\mathbb{N}\times \mathbb{N}$ yields $(d+1,t_0)$ after $d+1$ steps. Put $n=J(d,t_0)$. Induction on $k\le d$ gives $T(k)=t_k$ and $U(k)=u_k$, so code $n$ has exactly the coefficients $a_k=z(u_k)$ and does not use the fallback. Thus every valid integer list occurs. Together with step 1.1 this identifies $A$ with the set of real algebraic numbers. The encoding is generally many-to-one, since different tails or integer representatives can decode to the same list.

For every $n\in \mathbb{N}$ the root set $R_n$ is finite, and if the decoded list has $a_d\mathrm{\ne }0$ then $R_n$ is equinumerous with some $m\le d$. In the fallback case $a_d=0$ we have $P_n=1$ and $R_n=\mathrm{\varnothing }$. Otherwise $a_d^{\ast }\mathrm{\ne }0$, since the composite embedding $\mathbb{Z}\to \mathbb{Q}\to \mathbb{R}$ is injective and $a_d\mathrm{\ne }0$; the polynomial $P_n$ is exactly the evaluation of the real coefficient list $a_0^{\ast },\dots ,a_d^{\ast }$ with nonzero top coefficient, so [F3] applies and $R_n$ is finite of cardinality at most $d$.

$A$ is at most countable. Every $x\in A$ lies in $R_n$ for some $n$, so the least such $n$ exists by [F8]; write $n(x):=\min \{n:P_n(x)=0\}$. Then $R_{n(x)}$ is finite by step 2.2 and nonempty, say $R_{n(x)}\approx m$ with $m\in \mathbb{N}$, and by step 1.2 it has a unique increasing listing ${\mathrm{\ell }}_{n(x)}:m\to R_{n(x)}$; define $j(x):={\mathrm{\ell }}_{n(x)}^{-1}(x)\in m\subseteq \mathbb{N}$, the position of $x$ in that listing. Define $\phi (x):=J(n(x),j(x))\in \mathbb{N}$. Then $\phi$ is injective: if $\phi (x)=\phi (x^{\mathrm{\prime }})$, injectivity of $J$ gives $n(x)=n(x^{\mathrm{\prime }})=:n$ and $j(x)=j(x^{\mathrm{\prime }})=:i$, and both $x$ and $x^{\mathrm{\prime }}$ are the value ${\mathrm{\ell }}_n(i)$ of the same unique listing. Hence $\phi$ is a bijection of $A$ onto the subset $\phi [A]\subseteq \mathbb{N}$, and every subset of $\mathbb{N}$ is at most countable by [F4], so $A$ is at most countable.

Every embedded rational lies in $A$. Let $q\in \mathbb{Q}$ and fix a representative $(p,v)$ with $v\mathrm{\ne }0$. Applying the construction of step 2.1 to the integer list $(a_0,a_1):=(-p,v)$, of degree $d=1$ with $a_1=v\mathrm{\ne }0$, produces a code $n$ whose decoded polynomial is $P(x)=(-p{)}^{\ast }+v^{\ast }x$. By [F7], $P(\epsilon (q))=\epsilon (j(-p))+\epsilon (j(v))\epsilon (q)=\epsilon (j(-p)+j(v)q)=\epsilon (0)=0$, because $j(-p)+j(v)q=0$ in $\mathbb{Q}$, that is $v\cdot q=p$. Hence $\epsilon (q)\in A$.

$\mathbb{N}⪯A$. The composite embedding $g:\mathbb{N}\to \mathbb{R}$, $g(m):=\epsilon (j(\bar{m}))$, is injective, as a composite of injective maps; and $g(m)\in A$ for every $m$, since $g(m)=\epsilon (q)$ for the rational $q=j(\bar{m})$ by step 3.2. So $g$ is an injection $\mathbb{N}\to A$.

By step 3.1 there is an injection $A\to \mathbb{N}$, and by step 4.1 there is an injection $\mathbb{N}\to A$; Schröder-Bernstein gives $A\approx \mathbb{N}$, so $A$ is countably infinite.

$\mathbb{R}\setminus A$ is uncountable. Suppose it were at most countable. If $\mathbb{R}\setminus A=\mathrm{\varnothing }$ then $\mathbb{R}=A\approx \mathbb{N}$ by step 5.1, contradicting [F6]. Otherwise $\mathbb{R}\setminus A$ is nonempty, so by [F6] fix a surjection $s:\mathbb{N}\to \mathbb{R}\setminus A$; by step 5.1 fix a bijection $f:\mathbb{N}\to A$. Define $t:\mathbb{N}\times \mathbb{N}\to \mathbb{R}$ by $t(0,k):=f(k)$ and $t(\sigma (i),k):=s(k)$; every real is in $A$ or in $\mathbb{R}\setminus A$, elements of $A$ are values $f(k)$, and elements of $\mathbb{R}\setminus A$ are values $s(k)=t(\sigma (0),k)$, so $t$ is onto. Composing $t$ with the bijection $\beta :\mathbb{N}\to \mathbb{N}\times \mathbb{N}$ inverse to $J$ gives a surjection $\mathbb{N}\to \mathbb{R}$, contradicting [F6]. Hence $\mathbb{R}\setminus A$ is uncountable.

Collecting the results: $A$ is countably infinite by step 5.1, every embedded rational lies in $A$ by step 3.2, and $\mathbb{R}\setminus A$ is uncountable by step 6.1. The injection of step 3.1 is the least-code-and-root-rank map $x\mapsto J(n(x),j(x))$, and the only selections made anywhere are least elements of nonempty sets of naturals and the unique increasing listings of finite root sets, so the argument is a theorem of ZF.