The reals are complete

For a fixed $k\ge 1$, call a triple $(h,b,j)$ of naturals admissible when $h\ge 1$, $1\le b\le h$, $0\le j\le 2h$, and $\mathrm{\mid }{x}_k-\widehat{(j-h)\mathrm{/}b}\mathrm{\mid }<\widehat{1\mathrm{/}k}$. Here $j-h$ is an integer. Such a triple exists: [L1] supplies one approximating rational $a\mathrm{/}b$; [L6] makes $b$ a positive natural, and either $a$ or $-a$ is a nonnegative integer. Thus some natural $h$ satisfies $h\ge b$ and $-h\le a\le h$. Then $j=a+h$ is a natural with $j\le 2h$ and $(j-h)\mathrm{/}b=a\mathrm{/}b$. This proves nonemptiness separately for each $k$; it does not choose a family of witnesses.

To prove the least-upper-bound property, fix any nonempty $S\subseteq \mathbb{R}$ and any upper bound $U$. Fix one $t_0\in S$, and set $u_0=t_0-1$, $v_0=U$. Then $u_0$ is not an upper bound, $v_0$ is an upper bound, and $u_0<v_0$. For any pair $(u,v)\in {\mathbb{R}}^2$, put $m=(u+v)\mathrm{/}2$ and send $(u,v)$ to $(u,m)$ if $m$ is an upper bound of $S$, and to $(m,v)$ otherwise. This specifies a single self-map; [L9] gives its unique iterated sequence $(u_k,v_k{)}_{k\ge 0}$. Only one element $t_0$ and one upper bound are fixed; each later value is uniquely determined, so no choice axiom is used.

Let $h_k$ be the least first coordinate of an admissible triple; with $h_k$ fixed, let $b_k$ be the least admissible second coordinate; with both fixed, let $j_k$ be the least admissible third coordinate. Each minimum exists and is unique by [L7]. Define $q_k=(j_k-h_k)\mathrm{/}{b}_k$. This unique rule defines the graph of $(q_k)$ as a subset of ${\mathbb{N}}_{\ge 1}\times \mathbb{Q}$ by Separation. Consequently $\mathrm{\mid }{x}_k-{\widehat{q}}_k\mathrm{\mid }<\widehat{1\mathrm{/}k}$ for every $k$, without choosing representatives of all the $x_k$ or invoking any choice axiom.

Induction gives that $u_k$ is not an upper bound, $v_k$ is an upper bound, $u_k\le u_{k+1}\le v_{k+1}\le v_k$, and $v_k-u_k=(v_0-u_0)\mathrm{/}{2}^k$. Here $2^0=1$ and $2^{k+1}=2\cdot 2^k$, defined by recursion. Also $2^k\ge k+1$: the base case is equality, and $2(k+1)\ge k+2$ propagates the bound. Put $w=v_0-u_0>0$. By [L1] choose a rational $q$ with $\mathrm{\mid }w-\widehat{q}\mathrm{\mid }<1$, and set $B=q+1$, so $0<w<\widehat{B}$. Given rational $\epsilon >0$, [L2] supplies $N\ge 1$ with $1\mathrm{/}N<\epsilon \mathrm{/}B$. For every $k\ge N$, $0<v_k-u_k=w\mathrm{/}{2}^k<\widehat{B\mathrm{/}(k+1)}\le \widehat{B\mathrm{/}N}<\widehat{\epsilon }$. Thus the interval widths tend to zero, proved using only rational Archimedeanity.

$(q_k)$ is Cauchy in $\mathbb{Q}$: given rational $\epsilon >0$, pick $k_0$ with $1\mathrm{/}{k}_0<\epsilon \mathrm{/}3$ and $K$ with $\mathrm{\mid }{x}_k-x_l\mathrm{\mid }<\widehat{\epsilon \mathrm{/}3}$ for $k,l\ge K$; then for $k,l\ge \max (k_0,K)$, $\widehat{\mathrm{\mid }{q}_k-q_l\mathrm{\mid }}\le \mathrm{\mid }{\widehat{q}}_k-x_k\mathrm{\mid }+\mathrm{\mid }{x}_k-x_l\mathrm{\mid }+\mathrm{\mid }{x}_l-{\widehat{q}}_l\mathrm{\mid }<\widehat{1\mathrm{/}k}+\widehat{\epsilon \mathrm{/}3}+\widehat{1\mathrm{/}l}\le 3\widehat{\epsilon \mathrm{/}3}=\widehat{\epsilon }$, and the embedding reflects order, so $\mathrm{\mid }{q}_k-q_l\mathrm{\mid }<\epsilon$.

Set $x:=[(q_k)]\in \mathbb{R}$, the class of this rational Cauchy sequence.

$x_k\to x$: given rational $\epsilon >0$, pick $k_1$ with $1\mathrm{/}{k}_1<\epsilon \mathrm{/}3$ and $K_2$ with $\mathrm{\mid }{q}_k-q_l\mathrm{\mid }<\epsilon \mathrm{/}3$ for $k,l\ge K_2$; for $k\ge \max (k_1,K_2)$, the difference ${\widehat{q}}_k-x$ has representative $(q_k-q_l{)}_l$, whose absolute values $\mathrm{\mid }{q}_k-q_l\mathrm{\mid }$ are eventually below $\epsilon \mathrm{/}3$, so $\mathrm{\mid }{\widehat{q}}_k-x\mathrm{\mid }\le \widehat{\epsilon \mathrm{/}3}$, and $\mathrm{\mid }{x}_k-x\mathrm{\mid }\le \mathrm{\mid }{x}_k-{\widehat{q}}_k\mathrm{\mid }+\mathrm{\mid }{\widehat{q}}_k-x\mathrm{\mid }<\widehat{1\mathrm{/}k}+\widehat{\epsilon \mathrm{/}3}\le 2\widehat{\epsilon \mathrm{/}3}<\widehat{\epsilon }$.

Since the initial Cauchy sequence was arbitrary, every Cauchy sequence of reals converges in $\mathbb{R}$.

For $j,l\ge k$, nestedness puts $u_j,u_l$ in $[u_k,v_k]$, so $\mathrm{\mid }{u}_j-u_l\mathrm{\mid }\le v_k-u_k$. Step 2.2 makes this less than any prescribed positive rational tolerance for all sufficiently large $k$; hence $(u_k)$ is Cauchy. By step 6.1 (reindexing by $k+1$), it converges to a real $s$. For every fixed $k$, nestedness gives $u_k\le u_j\le v_k$ for all $j\ge k$. If $s<u_k$, density supplies a rational $\eta >0$ with $\widehat{\eta }<u_k-s$, and eventually $\mathrm{\mid }{u}_j-s\mathrm{\mid }<\widehat{\eta }$ contradicts $u_j\ge u_k$. If $s>v_k$, use $0<\widehat{\eta }<s-v_k$ instead. Thus $u_k\le s\le v_k$ for every $k$. In particular $0\le v_k-s\le v_k-u_k$, so step 2.2 also proves $v_k\to s$.

For every $t\in S$, $t\le v_k$ for all $k$. If $s<t$, choose a positive rational $\eta$ with $\widehat{\eta }<t-s$; convergence $v_k\to s$ gives eventually $v_k<s+\widehat{\eta }<t$, a contradiction. Hence $s$ is an upper bound of $S$. If $v$ is any upper bound, $u_k<v$ for every $k$: since $u_k$ is not an upper bound, some $t\in S$ satisfies $u_k<t\le v$. This is a separate existential implication for each $k$, with no sequence of witnesses chosen. If $v<s$, take $0<\widehat{\eta }<s-v$ and use $u_k\to s$ to obtain eventually $u_k>s-\widehat{\eta }>v$, a contradiction. Thus $s\le v$ for every upper bound $v$: $s$ is the least upper bound.

Every Cauchy sequence of reals converges, and every nonempty bounded-above subset of $\mathbb{R}$ has a least upper bound. Together with its totally ordered field structure, $\mathbb{R}$ is a complete totally ordered field; neither construction uses any form of the axiom of choice.