How do I prove that every hyperreal has a standard part after constructing the reals from the hyperrationals?

In texts on nonstandard analysis, I've come across references to the following construction of the real numbers: starting from the hyperrationals $^*\mathbb Q$, say that $\mathbb R$ is the quotient ring of the maximal ideal $\mathrm{mon}_{^*\mathbb Q}(0)$ in the subring $\mathrm{gal}_{^*\mathbb Q}(0)$, where:

• $\mathrm{gal}_{^*\mathbb Q}(0)$ is the galaxy in $^*\mathbb Q$ of 0, i.e. the set of the finite hyperrationals,



• $\mathrm{mon}_{^*\mathbb Q}(0)$ is the monad in $^*\mathbb Q$ of 0, i.e. the set of the infinitesimal hyperrationals.

(Note: the order is defined by $\mathrm{mon}_{^*\mathbb Q}(x) < \mathrm{mon}_{^*\mathbb Q}(y)$ iff $x < y$ and $x \approx y$, for every pair of hyperrationals $x, y$. This works because $\mathrm{mon}_{^*\mathbb Q}(x)$ is an interval: hyperrationals between infinitesimals are also infinitesimal.)

This construction seems to me to be the most natural one in a context where the tools of nonstandard analysis are being utilized. However the expositions I've read were too cursory/generalized/confusing, so I've been trying to work out the details myself. In particular I've been having some trouble with proving completeness.

I can prove, using this construction, that the reals are Dedekind and Cauchy complete, i.e. every nonempty upper-bounded set of reals has a supremum and every Cauchy sequence in $\mathbb R$ is convergent. However, there is a third formulation of the completeness of $\mathbb R$ which seems like the natural formulation given the construction described above (just as Dedekind completeness is the natural formulation given the Dedekind cut construction and Cauchy completeness is the natural formulation given the Cauchy sequence construction). Namely, the standard part principle—“every finite hyperreal number is infinitely close to a real number”.

I can prove the standard part principle from Dedekind or Cauchy completeness. But surely there is some way to prove it directly from the construction described above, without going to the trouble of proving Dedekind or Cauchy completeness. My proofs also have the issue that they are basically standard analysis proofs, rather than nonstandard analysis proofs. I'm used to standard analysis, so I find it much easier to think that way. So there may be a very simple nonstandard analytic argument I haven't thought of.

I can get this far:

Lemma 1. $\mathbb R$ is Archimedean.

Proof. Suppose $x$ is a real number. Let $r \in x$, so that $r$ is a finite hyperrational. Then there is a rational $a \ge r$. Because $\mathbb Q$ is Archimedean, there is an integer $n \ge a$. Because $r \le a \le n$, we have $\mathrm{mon}_{^*\mathbb Q}(r) \le \mathrm{mon}_{^*\mathbb Q}(n)$ (where $\le$ is the order in $\mathbb R$), and because $\mathrm{mon}_{^*\mathbb Q}(1)$ is the multiplicative identity in $\mathbb R$, the real number
\begin{equation*}
\mathrm{mon}_{^*\mathbb Q}(n) = \underbrace{\mathrm{mon}_{^*\mathbb Q}(1) + \dotsb + \mathrm{mon}_{^*\mathbb Q}(1)}_{n \text{ times}}
\end{equation*}
is an integer in $\mathbb R$.

Lemma 2. $\mathbb Q$ is dense in $\mathbb R$, i.e. every hyperreal number is infinitely close to a hyperrational number.

Proof. Suppose $x$ is a hyperreal number. Let $n$ be a large hyperinteger. Because $\mathbb R$ is Archimedean, by transfer, there is a hyperinteger $m \ge nx$. Let $m$ be the least such hyperinteger. Then $x - m/n = (nx - m)/n < 1/n$ is infinitesimal.

Theorem. $\mathbb R$ has the standard part property.

Proof. Suppose $x$ is a finite hyperreal. By Lemma 2 there is a hyperrational $r \approx x$. Because $x$ is finite, so is $r$. Let $a = \mathrm{mon}_{^*\mathbb Q}(r)$. Then $a$ is a real number…

If I could prove that $a$ in the above proof was infinitely close to $r$, I'd be done. It seems, intuitively, like every hyperrational number should be infinitely close (in $^*\mathbb R$) to the real number identified with its monad, but I don't know how to prove this or even really how to approach the problem.

(By the way, I've been working in a axiomatic nonstandard analysis framework where a $^*$-map and the transfer and saturation principles are taken as given, so ideally I'd like a solution that relies on these axioms rather than a specific ultrafilter construction. But I'd still be interested in any solution.)