%
\label{prop:ordered-field-axioms}
$(\mathbb{R}_\tau, +, \cdot, <)$ is a \textbf{totally ordered field}:
\begin{enumerate}
    \item \textbf{Commutativity.}
          $x + y = y + x$ and $x \cdot y = y \cdot x$.
    \item \textbf{Associativity.}
          $(x + y) + z = x + (y + z)$
          and $(x \cdot y) \cdot z = x \cdot (y \cdot z)$.
    \item \textbf{Distributivity.}
          $x \cdot (y + z) = x \cdot y + x \cdot z$.
    \item \textbf{Identities and inverses.}
          $x + 0 = x$, $x \cdot 1 = x$,
          $x + (-x) = 0$, $x \cdot x^{-1} = 1$ for $x \neq 0$.
    \item \textbf{Order compatibility.}
          $x < y \implies x + z < y + z$;
          $x < y,\, z > 0 \implies xz < yz$.
    \item \textbf{Trichotomy} (apartness form).
          For $x \neq y$, either $x < y$ or $y < x$.
\end{enumerate}

[Proof sketch]
Items (1)--(4) follow from the corresponding properties
on $\mathbb{Q}_\tau$ (Proposition~\ref{prop:q-tau-field}),
transported through term-by-term operations.
The main subtlety is the multiplicative inverse:
if $[q_n] \neq 0$, the explicit modulus guarantees
$|q_n|$ is eventually bounded away from zero.
Items (5)--(6) are direct calculations on representatives.
The verification is standard
(cf.\ Bishop \& Bridges, \emph{Constructive Analysis}, Ch.~2).