# 11.3.3 The algebraic structure of Cauchy reals

We first define the additive structure $(\mathbb{R}_{\mathsf{c}},0,{+},{-})$. Clearly, the additive unit element $0$ is just $\mathsf{rat}(0)$, while the additive inverse ${-}:\mathbb{R}_{\mathsf{c}}\to\mathbb{R}_{\mathsf{c}}$ is obtained as the extension of the additive inverse ${-}:\mathbb{Q}\to\mathbb{Q}$, using \autorefRC-extend-Q-Lipschitz with Lipschitz constant $1$. We have to work a bit harder for addition.

###### Lemma 11.3.1.

Suppose $f:\mathbb{Q}\times\mathbb{Q}\to\mathbb{Q}$ satisfies, for all $q,r,s:\mathbb{Q}$,

 $|f(q,s)-f(r,s)|\leq|q-r|\qquad\text{and}\qquad|f(q,r)-f(q,s)|\leq|r-s|.$

Then there is a function $\bar{f}:\mathbb{R}_{\mathsf{c}}\times\mathbb{R}_{\mathsf{c}}\to\mathbb{R}_{% \mathsf{c}}$ such that $\bar{f}(\mathsf{rat}(q),\mathsf{rat}(r))=f(q,r)$ for all $q,r:\mathbb{Q}$. Furthermore, for all $u,v,w:\mathbb{R}_{\mathsf{c}}$ and $q:\mathbb{Q}_{+}$,

 $u\sim_{\epsilon}v\Rightarrow\bar{f}(u,w)\sim_{\epsilon}\bar{f}(v,w)\quad\text{% and}\quad v\sim_{\epsilon}w\Rightarrow\bar{f}(u,v)\sim_{\epsilon}\bar{f}(u,w).$
###### Proof.

We use $(\mathbb{R}_{\mathsf{c}},{\mathord{\sim}})$-recursion to construct the curried form of $\bar{f}$ as a map $\mathbb{R}_{\mathsf{c}}\to A$ where $A$ is the space of non-expanding real-valued functions:

 $A:\!\!\equiv\setof{h:\mathbb{R}_{\mathsf{c}}\to\mathbb{R}_{\mathsf{c}}|\forall% (\epsilon:\mathbb{Q}_{+}).\,\forall(u,v:\mathbb{R}_{\mathsf{c}}).\,u\sim_{% \epsilon}v\Rightarrow h(u)\sim_{\epsilon}h(v)}.$

We shall also need a suitable $\frown_{\epsilon}$ on $A$, which we define as

 $(h\frown_{\epsilon}k):\!\!\equiv\forall(u:\mathbb{R}_{\mathsf{c}}).\,h(u)\sim_% {\epsilon}k(u).$

Clearly, if $\forall(\epsilon:\mathbb{Q}_{+}).\,h\frown_{\epsilon}k$ then $h(u)=k(u)$ for all $u:\mathbb{R}_{\mathsf{c}}$, so $\frown$ is separated.

For the base case we define $\bar{f}(\mathsf{rat}(q)):A$, where $q:\mathbb{Q}$, as the extension of the Lipschitz map ${\lambda}r.\,f(q,r)$ from $\mathbb{Q}\to\mathbb{Q}$ to $\mathbb{R}_{\mathsf{c}}\to\mathbb{R}_{\mathsf{c}}$, as constructed in \autorefRC-extend-Q-Lipschitz with Lipschitz constant $1$. Next, for a Cauchy approximation $x$, we define $\bar{f}(\mathsf{lim}(x)):\mathbb{R}_{\mathsf{c}}\to\mathbb{R}_{\mathsf{c}}$ as

 $\bar{f}(\mathsf{lim}(x))(v):\!\!\equiv\mathsf{lim}({\lambda}\epsilon.\,\bar{f}% (x_{\epsilon})(v)).$

For this to be a valid definition, ${\lambda}\epsilon.\,\bar{f}(x_{\epsilon})(v)$ should be a Cauchy approximation, so consider any $\delta,\epsilon:\mathbb{Q}$. Then by assumption $\bar{f}(x_{\delta})\frown_{\delta+\epsilon}\bar{f}(x_{\epsilon})$, hence $\bar{f}(x_{\delta})(v)\sim_{\delta+\epsilon}\bar{f}(x_{\epsilon})(v)$. Furthermore, $\bar{f}(\mathsf{lim}(x))$ is non-expanding because $\bar{f}(x_{\epsilon})$ is such by induction hypothesis. Indeed, if $u\sim_{\epsilon}v$ then, for all $\epsilon:\mathbb{Q}$,

 $\bar{f}(x_{\epsilon/3})(u)\sim_{\epsilon/3}\bar{f}(x_{\epsilon/3})(v),$

therefore $\bar{f}(\mathsf{lim}(x))(u)\sim_{\epsilon}\bar{f}(\mathsf{lim}(x))(v)$ by the fourth constructor of $\mathord{\sim}$.

We still have to check four more conditions, let us illustrate just one. Suppose $\epsilon:\mathbb{Q}_{+}$ and for some $\delta:\mathbb{Q}_{+}$ we have $\mathsf{rat}(q)\sim_{\epsilon-\delta}y_{\delta}$ and $\bar{f}(\mathsf{rat}(q))\frown_{\epsilon-\delta}\bar{f}(y_{\delta})$. To show $\bar{f}(\mathsf{rat}(q))\frown_{\epsilon}\bar{f}(\mathsf{lim}(y))$, consider any $v:\mathbb{R}_{\mathsf{c}}$ and observe that

 $\bar{f}(\mathsf{rat}(q))(v)\sim_{\epsilon-\delta}\bar{f}(y_{\delta})(v).$

Therefore, by the second constructor of $\mathord{\sim}$, we have $\bar{f}(\mathsf{rat}(q))(v)\sim_{\epsilon}\bar{f}(\mathsf{lim}(y))(v)$ as required. ∎

We may apply \autorefRC-binary-nonexpanding-extension to any bivariate rational function which is non-expanding separately in each variable. Addition is such a function, therefore we get ${+}:\mathbb{R}_{\mathsf{c}}\times\mathbb{R}_{\mathsf{c}}\to\mathbb{R}_{\mathsf% {c}}$. Furthermore, the extension is unique as long as we require it to be non-expanding in each variable, and just as in the univariate case, identities on rationals extend to identities on reals. Since composition of non-expanding maps is again non-expanding, we may conclude that addition satisfies the usual properties, such as commutativity and associativity. Therefore, $(\mathbb{R}_{\mathsf{c}},0,{+},{-})$ is a commutative group.

We may also apply \autorefRC-binary-nonexpanding-extension to the functions $\min:\mathbb{Q}\times\mathbb{Q}\to\mathbb{Q}$ and $\max:\mathbb{Q}\times\mathbb{Q}\to\mathbb{Q}$, which turns $\mathbb{R}_{\mathsf{c}}$ into a lattice. The partial order $\leq$ on $\mathbb{R}_{\mathsf{c}}$ is defined in terms of $\max$ as

 $(u\leq v):\!\!\equiv(\max(u,v)=v).$

The relation $\leq$ is a partial order because it is such on $\mathbb{Q}$, and the axioms of a partial order are expressible as equations in terms of $\min$ and $\max$, so they transfer to $\mathbb{R}_{\mathsf{c}}$.

Another function which extends to $\mathbb{R}_{\mathsf{c}}$ by the same method is the absolute value $|{\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}}|$. Again, it has the expected properties because they transfer from $\mathbb{Q}$ to $\mathbb{R}_{\mathsf{c}}$.

From $\leq$ we get the strict order $<$ by

 $(u

That is, $u holds when there merely exists a pair of rational numbers $q such that $x\leq\mathsf{rat}(q)$ and $\mathsf{rat}(r)\leq v$. It is not hard to check that $<$ is irreflexive and transitive, and has other properties that are expected for an ordered field. The archimedean principle follows directly from the definition of $<$.

###### Theorem 11.3.2 (Archimedean principle for $\mathbb{R}_{\mathsf{c}}$).

For every $u,v:\mathbb{R}_{\mathsf{c}}$ such that $u there merely exists $q:\mathbb{Q}$ such that $u.

###### Proof.

From $u we merely get $r,s:\mathbb{Q}$ such that $u\leq r, and we may take $q:\!\!\equiv(r+s)/2$. ∎

We now have enough structure on $\mathbb{R}_{\mathsf{c}}$ to express $u\sim_{\epsilon}v$ with standard concepts.

###### Lemma 11.3.3.

If $q:\mathbb{Q}$ and $u:\mathbb{R}_{\mathsf{c}}$ satisfy $u\leq\mathsf{rat}(q)$, then for any $v:\mathbb{R}_{\mathsf{c}}$ and $\epsilon:\mathbb{Q}_{+}$, if $u\sim_{\epsilon}v$ then $v\leq\mathsf{rat}(q+\epsilon)$.

###### Proof.

Note that the function $\max(\mathsf{rat}(q),\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}):\mathbb{R}_{% \mathsf{c}}\to\mathbb{R}_{\mathsf{c}}$ is Lipschitz with constant $1$. First consider the case when $u=\mathsf{rat}(r)$ is rational. For this we use induction on $v$. If $v$ is rational, then the statement is obvious. If $v$ is $\mathsf{lim}(y)$, we assume inductively that for any $\epsilon,\delta$, if $\mathsf{rat}(r)\sim_{\epsilon}y_{\delta}$ then $y_{\delta}\leq\mathsf{rat}(q+\epsilon)$, i.e. $\max(\mathsf{rat}(q+\epsilon),y_{\delta})=\mathsf{rat}(q+\epsilon)$.

Now assuming $\epsilon$ and $\mathsf{rat}(r)\sim_{\epsilon}\mathsf{lim}(y)$, we have $\theta$ such that $\mathsf{rat}(r)\sim_{\epsilon-\theta}\mathsf{lim}(y)$, hence $\mathsf{rat}(r)\sim_{\epsilon}y_{\delta}$ whenever $\delta<\theta$. Thus, the inductive hypothesis gives $\max(\mathsf{rat}(q+\epsilon),y_{\delta})=\mathsf{rat}(q+\epsilon)$ for such $\delta$. But by definition,

 $\max(\mathsf{rat}(q+\epsilon),\mathsf{lim}(y))\equiv\mathsf{lim}({\lambda}% \delta.\,\max(\mathsf{rat}(q+\epsilon),y_{\delta})).$

Since the limit of an eventually constant Cauchy approximation is that constant, we have

 $\max(\mathsf{rat}(q+\epsilon),\mathsf{lim}(y))=\mathsf{rat}(q+\epsilon),$

hence $\mathsf{lim}(y)\leq\mathsf{rat}(q+\epsilon)$.

Now consider a general $u:\mathbb{R}_{\mathsf{c}}$. Since $u\leq\mathsf{rat}(q)$ means $\max(\mathsf{rat}(q),u)=\mathsf{rat}(q)$, the assumption $u\sim_{\epsilon}v$ and the Lipschitz property of $\max(\mathsf{rat}(q),-)$ imply $\max(\mathsf{rat}(q),v)\sim_{\epsilon}\mathsf{rat}(q)$. Thus, since $\mathsf{rat}(q)\leq\mathsf{rat}(q)$, the first case implies $\max(\mathsf{rat}(q),v)\leq\mathsf{rat}(q+\epsilon)$, and hence $v\leq\mathsf{rat}(q+\epsilon)$ by transitivity of $\leq$. ∎

###### Lemma 11.3.4.

Suppose $q:\mathbb{Q}$ and $u:\mathbb{R}_{\mathsf{c}}$ satisfy $u<\mathsf{rat}(q)$. Then:

1. 1.

For any $v:\mathbb{R}_{\mathsf{c}}$ and $\epsilon:\mathbb{Q}_{+}$, if $u\sim_{\epsilon}v$ then $v<\mathsf{rat}(q+\epsilon)$.

2. 2.

There exists $\epsilon:\mathbb{Q}_{+}$ such that for any $v:\mathbb{R}_{\mathsf{c}}$, if $u\sim_{\epsilon}v$ we have $v<\mathsf{rat}(q)$.

###### Proof.

By definition, $u<\mathsf{rat}(q)$ means there is $r:\mathbb{Q}$ with $r and $u\leq\mathsf{rat}(r)$. Then by \autorefthm:RC-le-grow, for any $\epsilon$, if $u\sim_{\epsilon}v$ then $v\leq\mathsf{rat}(r+\epsilon)$. Conclusion 1 follows immediately since $r+\epsilon, while for 2 we can take any $\epsilon. ∎

We are now able to show that the auxiliary relation $\mathord{\sim}$ is what we think it is.

###### Theorem 11.3.5.

$(u\sim_{\epsilon}v)\simeq(|u-v|<\mathsf{rat}(\epsilon))$ for all $u,v:\mathbb{R}_{\mathsf{c}}$ and $\epsilon:\mathbb{Q}_{+}$.

###### Proof.

The Lipschitz properties of subtraction and absolute value imply that if $u\sim_{\epsilon}v$, then $|u-v|\sim_{\epsilon}|u-u|=0$. Thus, for the left-to-right direction, it will suffice to show that if $u\sim_{\epsilon}0$, then $|u|<\mathsf{rat}(\epsilon)$. We proceed by $\mathbb{R}_{\mathsf{c}}$-induction on $u$.

If $u$ is rational, the statement follows immediately since absolute value and order extend the standard ones on $\mathbb{Q}_{+}$. If $u$ is $\mathsf{lim}(x)$, then by roundedness we have $\theta:\mathbb{Q}_{+}$ with $\mathsf{lim}(x)\sim_{\epsilon-\theta}0$. By the triangle inequality, therefore, we have $x_{\theta/3}\sim_{\epsilon-2\theta/3}0$, so the inductive hypothesis yields $|x_{\theta/3}|<\mathsf{rat}(\epsilon-2\theta/3)$. But $x_{\theta/3}\sim_{2\theta/3}\mathsf{lim}(x)$, hence $|x_{\theta/3}|\sim_{2\theta/3}|\mathsf{lim}(x)|$ by the Lipschitz property, so \autorefthm:RC-lt-open1 implies $|\mathsf{lim}(x)|<\mathsf{rat}(\epsilon)$.

In the other direction, we use $\mathbb{R}_{\mathsf{c}}$-induction on $u$ and $v$. If both are rational, this is the first constructor of $\mathord{\sim}$.

If $u$ is $\mathsf{rat}(q)$ and $v$ is $\mathsf{lim}(y)$, we assume inductively that for any $\epsilon,\delta$, if $|\mathsf{rat}(q)-y_{\delta}|<\mathsf{rat}(\epsilon)$ then $\mathsf{rat}(q)\sim_{\epsilon}y_{\delta}$. Fix an $\epsilon$ such that $|\mathsf{rat}(q)-\mathsf{lim}(y)|<\mathsf{rat}(\epsilon)$. Since $\mathbb{Q}$ is order-dense in $\mathbb{R}_{\mathsf{c}}$, there exists $\theta<\epsilon$ with $|\mathsf{rat}(q)-\mathsf{lim}(y)|<\mathsf{rat}(\theta)$. Now for any $\delta,\eta$ we have $\mathsf{lim}(y)\sim_{2\delta}y_{\delta}$, hence by the Lipschitz property

 $|\mathsf{rat}(q)-\mathsf{lim}(y)|\sim_{\delta+\eta}|\mathsf{rat}(q)-y_{\delta}|.$

Thus, by \autorefthm:RC-lt-open1, we have $|\mathsf{rat}(q)-y_{\delta}|<\mathsf{rat}(\theta+2\delta)$. So by the inductive hypothesis, $\mathsf{rat}(q)\sim_{\theta+2\delta}y_{\delta}$, and thus $\mathsf{rat}(q)\sim_{\theta+4\delta}\mathsf{lim}(y)$ by the triangle inequality. Thus, it suffices to choose $\delta:\!\!\equiv(\epsilon-\theta)/4$.

The remaining two cases are entirely analogous. ∎

Next, we would like to equip $\mathbb{R}_{\mathsf{c}}$ with multiplicative structure. For each $q:\mathbb{Q}$ the map $r\mapsto q\cdot r$ is Lipschitz with constant11We defined Lipschitz constants as positive rational numbers. $|q|+1$, and so we can extend it to multiplication by $q$ on the real numbers. Therefore $\mathbb{R}_{\mathsf{c}}$ is a vector space over $\mathbb{Q}$. In general, we can define multiplication of real numbers as

 $u\cdot v:\!\!\equiv{\textstyle\frac{1}{2}}\cdot((u+v)^{2}-u^{2}-v^{2}),$ (11.3.6)

so we just need squaring $u\mapsto u^{2}$ as a map $\mathbb{R}_{\mathsf{c}}\to\mathbb{R}_{\mathsf{c}}$. Squaring is not a Lipschitz map, but it is Lipschitz on every bounded domain, which allows us to patch it together. Define the open and closed intervals

 $[u,v]:\!\!\equiv\setof{x:\mathbb{R}_{\mathsf{c}}|u\leq x\leq v}\qquad\text{and% }\qquad(u,v):\!\!\equiv\setof{x:\mathbb{R}_{\mathsf{c}}|u

Although technically an element of $[u,v]$ or $(u,v)$ is a Cauchy real number together with a proof, since the latter inhabits a mere proposition it is uninteresting. Thus, as is common with subset types, we generally write simply $x:[u,v]$ whenever $x:\mathbb{R}_{\mathsf{c}}$ is such that $u\leq x\leq v$, and similarly.

###### Theorem 11.3.7.

There exists a unique function ${(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})}^{2}:\mathbb{R}_{\mathsf{c}}\to% \mathbb{R}_{\mathsf{c}}$ which extends squaring $q\mapsto q^{2}$ of rational numbers and satisfies

 $\forall(n:\mathbb{N}).\,\forall(u,v:[-n,n]).\,|u^{2}-v^{2}|\leq 2\cdot n\cdot|% u-v|.$
###### Proof.

We first observe that for every $u:\mathbb{R}_{\mathsf{c}}$ there merely exists $n:\mathbb{N}$ such that $-n\leq u\leq n$, see \autorefex:traditional-archimedean, so the map

 $e:\Bigl{(}\mathchoice{\sum_{n:\mathbb{N}}\,}{\mathchoice{{\textstyle\sum_{(n:% \mathbb{N})}}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{% N})}}}{\mathchoice{{\textstyle\sum_{(n:\mathbb{N})}}}{\sum_{(n:\mathbb{N})}}{% \sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}}{\mathchoice{{\textstyle\sum_{(n% :\mathbb{N})}}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb% {N})}}}[-n,n]\Bigr{)}\to\mathbb{R}_{\mathsf{c}}\qquad\text{defined by}\qquad e% (n,x):\!\!\equiv x$

is surjective. Next, for each $n:\mathbb{N}$, the squaring map

 $s_{n}:\setof{q:\mathbb{Q}|-n\leq q\leq n}\to\mathbb{Q}\qquad\text{defined by}% \qquad s_{n}(q):\!\!\equiv q^{2}$

is Lipschitz with constant $2n$, so we can use \autorefRC-extend-Q-Lipschitz to extend it to a map $\bar{s}_{n}:[-n,n]\to\mathbb{R}_{\mathsf{c}}$ with Lipschitz constant $2n$, see \autorefRC-Lipschitz-on-interval for details. The maps $\bar{s}_{n}$ are compatible: if $m for some $m,n:\mathbb{N}$ then $s_{n}$ restricted to $[-m,m]$ must agree with $s_{m}$ because both are Lipschitz, and therefore continuous in the sense of \autorefRC-continuous-eq. Therefore, by \autoreflem:images_are_coequalizers the map

 $\Bigl{(}\mathchoice{\sum_{n:\mathbb{N}}\,}{\mathchoice{{\textstyle\sum_{(n:% \mathbb{N})}}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{% N})}}}{\mathchoice{{\textstyle\sum_{(n:\mathbb{N})}}}{\sum_{(n:\mathbb{N})}}{% \sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}}{\mathchoice{{\textstyle\sum_{(n% :\mathbb{N})}}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb% {N})}}}[-n,n]\Bigr{)}\to\mathbb{R}_{\mathsf{c}},\qquad\text{given by}\qquad(n,% x)\mapsto s_{n}(x)$

factors uniquely through $\mathbb{R}_{\mathsf{c}}$ to give us the desired function. ∎

At this point we have the ring structure of the reals and the archimedean order. To establish $\mathbb{R}_{\mathsf{c}}$ as an archimedean ordered field, we still need inverses.

###### Theorem 11.3.8.

A Cauchy real is invertible if, and only if, it is apart from zero.

###### Proof.

First, suppose $u:\mathbb{R}_{\mathsf{c}}$ has an inverse $v:\mathbb{R}_{\mathsf{c}}$ By the archimedean principle there is $q:\mathbb{Q}$ such that $|v|. Then $1=|uv|<|u|\cdot v<|u|\cdot q$ and hence $|u|>1/q$, which is to say that $u\mathrel{\#}0$.

For the converse we construct the inverse map

 $({\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}})^{-1}:\setof{u:\mathbb{R}_{% \mathsf{c}}|u\mathrel{\#}0}\to\mathbb{R}_{\mathsf{c}}$

by patching together functions, similarly to the construction of squaring in \autorefRC-squaring. We only outline the main steps. For every $q:\mathbb{Q}$ let

 $[q,\infty):\!\!\equiv\setof{u:\mathbb{R}_{\mathsf{c}}|q\leq u}\qquad\text{and}% \qquad(-\infty,q]:\!\!\equiv\setof{u:\mathbb{R}_{\mathsf{c}}|u\leq-q}.$

Then, as $q$ ranges over $\mathbb{Q}_{+}$, the types $(-\infty,q]$ and $[q,\infty)$ jointly cover $\setof{u:\mathbb{R}_{\mathsf{c}}|u\mathrel{\#}0}$. On each such $[q,\infty)$ and $(-\infty,q]$ the inverse function is obtained by an application of \autorefRC-extend-Q-Lipschitz with Lipschitz constant $1/q^{2}$. Finally, \autoreflem:images_are_coequalizers guarantees that the inverse function factors uniquely through $\setof{u:\mathbb{R}_{\mathsf{c}}|u\mathrel{\#}0}$. ∎

We summarize the algebraic structure of $\mathbb{R}_{\mathsf{c}}$ with a theorem.

###### Theorem 11.3.9.

The Cauchy reals form an archimedean ordered field.

 Title 11.3.3 The algebraic structure of Cauchy reals \metatable