Are the multi-valued Eudoxus reals constructively equivalent to the Dedekind reals?

Question

Without LEM or the axiom of choice, we can prove that the Eudoxus reals are equivalent to the Cauchy reals but can't prove either of those equivalent to the Dedekind reals.

However, we can prove that the multi-valued Cauchy reals are equivalent to the Dedekind reals. My question is if we can say the same about a kind of multi-valued Eudoxus real?

In particular, a multi-valued Eudoxus real will be represented by a set $R \subseteq \mathbb Z \times \mathbb Z$ (thought of as a relation) such that $\forall x \in \mathbb Z. \exists a \in \mathbb Z. xRa$ and the set $\{a + b - c: \exists x, y \in \mathbb Z. xRa \land yRb \land (x+y)Rc\}$ is bounded. Relations $R_1$ and $R_2$ represent the same multi-valued Eudoxus real when the set $\{a - b : \exists x \in \mathbb Z. xR_1a \land xR_2b\}$ is bounded.

We turn this into an ordered field in the same way as we do the (single-valued) Eudoxus reals. The Eudoxus reals are subfield of the multi-valued Eudoxus reals, and they are equal if we assume the axiom of countable choice.

We can embed a multi-valued Eudoxus real $e$ into the Dedekind reals via the Dedekind cut $(\{p \in \mathbb Q: p < e\}, \{q \in \mathbb Q: e < q\})$, as usual. My question: is this embedding surjective?

Answer 1

Yes

In particular, for any real number $r$, we can construct a total relation $R$ representing it such that $B = \{a + b - c: \exists x, y \in \mathbb Z. xRa \land yRb \land (x+y)Rc\} \subseteq \{-1, 0,1\}$.

In classical mathematics, we usually define $xRa$ as $a = \lfloor xr \rfloor$, which is equivalent to $a \in [xr, xr+1)$. The floor function can't be constructively shown total. So instead we define $xRa$ as $$a \in (xr - \frac 23, xr + \frac 23)$$

This is total because we can find a rational $p \in (xr - \frac 16, xr + \frac 16)$ (because $\mathbb Q$ is dense) and then an integer $a \in [p - \frac 12, p + \frac 12]$. Thus $|a - xr| < \frac 23$ by the triangle inequality.

Note that $xRa$ is equivalent to $\exists \delta \in (-\frac 23, \frac 23). a = xr + \delta$. Now we find a bound on $B$.

$$a + b - c = (xr + \delta_1) + (yr + \delta_2) - ((x+y)r + \delta_3) \text{ for some $x, y \in \mathbb Z$ and $\delta_1, \delta_2, \delta_3 \in (-\frac 23, \frac 23)$}$$ $$a + b - c = \delta_1 + \delta_2 + (-\delta_3)$$ $$|a + b - c| = |\delta_1 + \delta_2 + (-\delta_3)|$$ $$\le |\delta_1| + |\delta_2| + |\delta_3|$$ $$< \frac 23 + \frac 23 + \frac 23$$ $$= 2$$

Thus $a + b - c \in (-2,2)$. We already know that $a + b - c \in \mathbb Z$, and thus $$a + b -c \in \mathbb Z \cap (-2,2) = \{-1, 0, 1\}$$ $\square$