11.3.3 The algebraic structure of Cauchy reals

We first define the additive structure $({ℝ}_{𝖼},0,+,-)$. Clearly, the additive unit element $0$ is just $\mathrm{𝗋𝖺𝗍}(0)$, while the additive inverse $-:{ℝ}_{𝖼}\to {ℝ}_{𝖼}$ is obtained as the extension of the additive inverse $-:\mathbb{Q}\to \mathbb{Q}$, using RC-extend-Q-Lipschitz with Lipschitz constant $1$. We have to work a bit harder for addition.

Lemma 11.3.1.

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

$$|f(q,s)-f(r,s)|\le |q-r|\mathit{\hspace{1em}\hspace{1em}}\text{𝑎𝑛𝑑}\mathit{\hspace{1em}\hspace{1em}}|f(q,r)-f(q,s)|\le |r-s|.$$

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

$$u{\sim }_{ϵ}v\Rightarrow \overline{f}(u,w){\sim }_{ϵ}\overline{f}(v,w)\mathit{\hspace{1em}}\text{𝑎𝑛𝑑}\mathit{\hspace{1em}}v{\sim }_{ϵ}w\Rightarrow \overline{f}(u,v){\sim }_{ϵ}\overline{f}(u,w).$$

Proof.

We use $({ℝ}_{𝖼},\mathrm{\sim })$-recursion to construct the curried form of $\overline{f}$ as a map ${ℝ}_{𝖼}\to A$ where $A$ is the space of non-expanding real-valued functions:

$$A:\equiv h:{ℝ}_{𝖼}\to {ℝ}_{𝖼}|\forall (ϵ:{\mathbb{Q}}_{+}).\forall (u,v:{ℝ}_{𝖼}).u{\sim }_{ϵ}v\Rightarrow h(u){\sim }_{ϵ}h(v).$$

We shall also need a suitable ${⌢}_{ϵ}$ on $A$, which we define as

$$(h{⌢}_{ϵ}k):\equiv \forall (u:{ℝ}_{𝖼}).h(u){\sim }_{ϵ}k(u).$$

Clearly, if $\forall (ϵ:{\mathbb{Q}}_{+}).h{⌢}_{ϵ}k$ then $h(u)=k(u)$ for all $u:{ℝ}_{𝖼}$, so $⌢$ is separated.

For the base case we define $\overline{f}(\mathrm{𝗋𝖺𝗍}(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 ${ℝ}_{𝖼}\to {ℝ}_{𝖼}$, as constructed in RC-extend-Q-Lipschitz with Lipschitz constant $1$. Next, for a Cauchy approximation $x$, we define $\overline{f}(\mathrm{𝗅𝗂𝗆}(x)):{ℝ}_{𝖼}\to {ℝ}_{𝖼}$ as

$$\overline{f}(\mathrm{𝗅𝗂𝗆}(x))(v):\equiv \mathrm{𝗅𝗂𝗆}(\lambda ϵ.\overline{f}(x_{ϵ})(v)).$$

For this to be a valid definition, $\lambda ϵ.\overline{f}(x_{ϵ})(v)$ should be a Cauchy approximation, so consider any $\delta ,ϵ:\mathbb{Q}$. Then by assumption $\overline{f}(x_{\delta }){⌢}_{\delta +ϵ}\overline{f}(x_{ϵ})$, hence $\overline{f}(x_{\delta })(v){\sim }_{\delta +ϵ}\overline{f}(x_{ϵ})(v)$. Furthermore, $\overline{f}(\mathrm{𝗅𝗂𝗆}(x))$ is non-expanding because $\overline{f}(x_{ϵ})$ is such by induction hypothesis. Indeed, if $u{\sim }_{ϵ}v$ then, for all $ϵ:\mathbb{Q}$,

$$\overline{f}(x_{ϵ/3})(u){\sim }_{ϵ/3}\overline{f}(x_{ϵ/3})(v),$$

therefore $\overline{f}(\mathrm{𝗅𝗂𝗆}(x))(u){\sim }_{ϵ}\overline{f}(\mathrm{𝗅𝗂𝗆}(x))(v)$ by the fourth constructor of $\mathrm{\sim }$.

We still have to check four more conditions, let us illustrate just one. Suppose $ϵ:{\mathbb{Q}}_{+}$ and for some $\delta :{\mathbb{Q}}_{+}$ we have $\mathrm{𝗋𝖺𝗍}(q){\sim }_{ϵ-\delta }{y}_{\delta }$ and $\overline{f}(\mathrm{𝗋𝖺𝗍}(q)){⌢}_{ϵ-\delta }\overline{f}(y_{\delta })$. To show $\overline{f}(\mathrm{𝗋𝖺𝗍}(q)){⌢}_{ϵ}\overline{f}(\mathrm{𝗅𝗂𝗆}(y))$, consider any $v:{ℝ}_{𝖼}$ and observe that

$$\overline{f}(\mathrm{𝗋𝖺𝗍}(q))(v){\sim }_{ϵ-\delta }\overline{f}(y_{\delta })(v).$$

Therefore, by the second constructor of $\mathrm{\sim }$, we have $\overline{f}(\mathrm{𝗋𝖺𝗍}(q))(v){\sim }_{ϵ}\overline{f}(\mathrm{𝗅𝗂𝗆}(y))(v)$ as required. ∎

We may apply RC-binary-nonexpanding-extension to any bivariate rational function which is non-expanding separately in each variable. Addition is such a function, therefore we get $+:{ℝ}_{𝖼}\times {ℝ}_{𝖼}\to {ℝ}_{𝖼}$. 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, $({ℝ}_{𝖼},0,+,-)$ is a commutative group.

We may also apply RC-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 ${ℝ}_{𝖼}$ into a lattice. The partial order $\le$ on ${ℝ}_{𝖼}$ is defined in terms of $\max$ as

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

The relation $\le$ 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 ${ℝ}_{𝖼}$.

Another function which extends to ${ℝ}_{𝖼}$ by the same method is the absolute value $|\text{–}|$. Again, it has the expected properties because they transfer from $\mathbb{Q}$ to ${ℝ}_{𝖼}$.

From $\le$ we get the strict order by

That is, holds when there merely exists a pair of rational numbers such that $x\le \mathrm{𝗋𝖺𝗍}(q)$ and $\mathrm{𝗋𝖺𝗍}(r)\le 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 ${\mathrm{R}}_{\mathrm{c}}$).

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

Proof.

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

We now have enough structure on ${ℝ}_{𝖼}$ to express $u{\sim }_{ϵ}v$ with standard concepts.

Lemma 11.3.3.

If $q\mathrm{:}\mathrm{Q}$ and $u\mathrm{:}{\mathrm{R}}_{\mathrm{c}}$ satisfy $u\mathrm{\le }\mathrm{rat}\mathit{}\mathrm{(}q\mathrm{)}$, then for any $v\mathrm{:}{\mathrm{R}}_{\mathrm{c}}$ and $ϵ\mathrm{:}{\mathrm{Q}}_{\mathrm{+}}$, if $u{\mathrm{\sim }}_{ϵ}v$ then $v\mathrm{\le }\mathrm{rat}\mathit{}\mathrm{(}q\mathrm{+}ϵ\mathrm{)}$.

Proof.

Note that the function $\max (\mathrm{𝗋𝖺𝗍}(q),\text{–}):{ℝ}_{𝖼}\to {ℝ}_{𝖼}$ is Lipschitz with constant $1$. First consider the case when $u=\mathrm{𝗋𝖺𝗍}(r)$ is rational. For this we use induction on $v$. If $v$ is rational, then the statement is obvious. If $v$ is $\mathrm{𝗅𝗂𝗆}(y)$, we assume inductively that for any $ϵ,\delta$, if $\mathrm{𝗋𝖺𝗍}(r){\sim }_{ϵ}{y}_{\delta }$ then $y_{\delta }\le \mathrm{𝗋𝖺𝗍}(q+ϵ)$, i.e. $\max (\mathrm{𝗋𝖺𝗍}(q+ϵ),y_{\delta })=\mathrm{𝗋𝖺𝗍}(q+ϵ)$.

Now assuming $ϵ$ and $\mathrm{𝗋𝖺𝗍}(r){\sim }_{ϵ}\mathrm{𝗅𝗂𝗆}(y)$, we have $\theta$ such that $\mathrm{𝗋𝖺𝗍}(r){\sim }_{ϵ-\theta }\mathrm{𝗅𝗂𝗆}(y)$, hence $\mathrm{𝗋𝖺𝗍}(r){\sim }_{ϵ}{y}_{\delta }$ whenever . Thus, the inductive hypothesis gives $\max (\mathrm{𝗋𝖺𝗍}(q+ϵ),y_{\delta })=\mathrm{𝗋𝖺𝗍}(q+ϵ)$ for such $\delta$. But by definition,

$$\max (\mathrm{𝗋𝖺𝗍}(q+ϵ),\mathrm{𝗅𝗂𝗆}(y))\equiv \mathrm{𝗅𝗂𝗆}(\lambda \delta .\max (\mathrm{𝗋𝖺𝗍}(q+ϵ),y_{\delta })).$$

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

$$\max (\mathrm{𝗋𝖺𝗍}(q+ϵ),\mathrm{𝗅𝗂𝗆}(y))=\mathrm{𝗋𝖺𝗍}(q+ϵ),$$

hence $\mathrm{𝗅𝗂𝗆}(y)\le \mathrm{𝗋𝖺𝗍}(q+ϵ)$.

Now consider a general $u:{ℝ}_{𝖼}$. Since $u\le \mathrm{𝗋𝖺𝗍}(q)$ means $\max (\mathrm{𝗋𝖺𝗍}(q),u)=\mathrm{𝗋𝖺𝗍}(q)$, the assumption $u{\sim }_{ϵ}v$ and the Lipschitz property of $\max (\mathrm{𝗋𝖺𝗍}(q),-)$ imply $\max (\mathrm{𝗋𝖺𝗍}(q),v){\sim }_{ϵ}\mathrm{𝗋𝖺𝗍}(q)$. Thus, since $\mathrm{𝗋𝖺𝗍}(q)\le \mathrm{𝗋𝖺𝗍}(q)$, the first case implies $\max (\mathrm{𝗋𝖺𝗍}(q),v)\le \mathrm{𝗋𝖺𝗍}(q+ϵ)$, and hence $v\le \mathrm{𝗋𝖺𝗍}(q+ϵ)$ by transitivity of $\le$. ∎

Lemma 11.3.4.

Suppose $q\mathrm{:}\mathrm{Q}$ and $u\mathrm{:}{\mathrm{R}}_{\mathrm{c}}$ satisfy . Then:

1. For any $v:{ℝ}_{𝖼}$ and $ϵ:{\mathbb{Q}}_{+}$, if $u{\sim }_{ϵ}v$ then .

2. There exists $ϵ:{\mathbb{Q}}_{+}$ such that for any $v:{ℝ}_{𝖼}$, if $u{\sim }_{ϵ}v$ we have .

Proof.

By definition, means there is $r:\mathbb{Q}$ with and $u\le \mathrm{𝗋𝖺𝗍}(r)$. Then by thm:RC-le-grow, for any $ϵ$, if $u{\sim }_{ϵ}v$ then $v\le \mathrm{𝗋𝖺𝗍}(r+ϵ)$. Conclusion 1 follows immediately since , while for 2 we can take any . ∎

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

Theorem 11.3.5.

for all $u\mathrm{,}v\mathrm{:}{\mathrm{R}}_{\mathrm{c}}$ and $ϵ\mathrm{:}{\mathrm{Q}}_{\mathrm{+}}$.

Proof.

The Lipschitz properties of subtraction and absolute value imply that if $u{\sim }_{ϵ}v$, then $|u-v|{\sim }_{ϵ}|u-u|=0$. Thus, for the left-to-right direction, it will suffice to show that if $u{\sim }_{ϵ}0$, then . We proceed by ${ℝ}_{𝖼}$-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 $\mathrm{𝗅𝗂𝗆}(x)$, then by roundedness we have $\theta :{\mathbb{Q}}_{+}$ with $\mathrm{𝗅𝗂𝗆}(x){\sim }_{ϵ-\theta }0$. By the triangle inequality, therefore, we have $x_{\theta /3}{\sim }_{ϵ-2\theta /3}0$, so the inductive hypothesis yields . But $x_{\theta /3}{\sim }_{2\theta /3}\mathrm{𝗅𝗂𝗆}(x)$, hence $|x_{\theta /3}|{\sim }_{2\theta /3}|\mathrm{𝗅𝗂𝗆}(x)|$ by the Lipschitz property, so thm:RC-lt-open1 implies .

In the other direction, we use ${ℝ}_{𝖼}$-induction on $u$ and $v$. If both are rational, this is the first constructor of $\mathrm{\sim }$.

If $u$ is $\mathrm{𝗋𝖺𝗍}(q)$ and $v$ is $\mathrm{𝗅𝗂𝗆}(y)$, we assume inductively that for any $ϵ,\delta$, if then $\mathrm{𝗋𝖺𝗍}(q){\sim }_{ϵ}{y}_{\delta }$. Fix an $ϵ$ such that . Since $\mathbb{Q}$ is order-dense in ${ℝ}_{𝖼}$, there exists with . Now for any $\delta ,\eta$ we have $\mathrm{𝗅𝗂𝗆}(y){\sim }_{2\delta }{y}_{\delta }$, hence by the Lipschitz property

$$|\mathrm{𝗋𝖺𝗍}(q)-\mathrm{𝗅𝗂𝗆}(y)|{\sim }_{\delta +\eta }|\mathrm{𝗋𝖺𝗍}(q)-y_{\delta }|.$$

Thus, by thm:RC-lt-open1, we have . So by the inductive hypothesis, $\mathrm{𝗋𝖺𝗍}(q){\sim }_{\theta +2\delta }{y}_{\delta }$, and thus $\mathrm{𝗋𝖺𝗍}(q){\sim }_{\theta +4\delta }\mathrm{𝗅𝗂𝗆}(y)$ by the triangle inequality. Thus, it suffices to choose $\delta :\equiv (ϵ-\theta )/4$.

The remaining two cases are entirely analogous. ∎

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

$$u\cdot v:\equiv \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 ${ℝ}_{𝖼}\to {ℝ}_{𝖼}$. 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

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:{ℝ}_{𝖼}$ is such that $u\le x\le v$, and similarly.

Theorem 11.3.7.

There exists a unique function ${\mathrm{(}\mathit{\text{–}}\mathrm{)}}^{\mathrm{2}}\mathrm{:}{\mathrm{R}}_{\mathrm{c}}\mathrm{\to }{\mathrm{R}}_{\mathrm{c}}$ which extends squaring $q\mathrm{\mapsto }{q}^{\mathrm{2}}$ of rational numbers and satisfies

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

Proof.

We first observe that for every $u:{ℝ}_{𝖼}$ there merely exists $n:\mathbb{N}$ such that $-n\le u\le n$, see ex:traditional-archimedean, so the map

$$e:\left(\sum _{n:\mathbb{N}}[-n,n]\right)\to {ℝ}_{𝖼}\mathit{\hspace{1em}\hspace{1em}}\text{defined by}\mathit{\hspace{1em}\hspace{1em}}e(n,x):\equiv x$$

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

$$s_n:q:\mathbb{Q}|-n\le q\le n\to \mathbb{Q}\mathit{\hspace{1em}\hspace{1em}}\text{defined by}\mathit{\hspace{1em}\hspace{1em}}{s}_n(q):\equiv q^2$$

is Lipschitz with constant $2n$, so we can use RC-extend-Q-Lipschitz to extend it to a map ${\overline{s}}_n:[-n,n]\to {ℝ}_{𝖼}$ with Lipschitz constant $2n$, see RC-Lipschitz-on-interval for details. The maps ${\overline{s}}_n$ are compatible: if 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 RC-continuous-eq. Therefore, by lem:images_are_coequalizers the map

$$\left(\sum _{n:\mathbb{N}}[-n,n]\right)\to {ℝ}_{𝖼},\text{given by}\mathit{\hspace{1em}\hspace{1em}}(n,x)\mapsto s_n(x)$$

factors uniquely through ${ℝ}_{𝖼}$ to give us the desired function. ∎

At this point we have the ring structure of the reals and the archimedean order. To establish ${ℝ}_{𝖼}$ 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:{ℝ}_{𝖼}$ has an inverse $v:{ℝ}_{𝖼}$ By the archimedean principle there is $q:\mathbb{Q}$ such that . Then and hence $|u|>1/q$, which is to say that $u\#0$.

For the converse we construct the inverse map

$${(\text{–})}^{-1}:u:{ℝ}_{𝖼}|u\#0\to {ℝ}_{𝖼}$$

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

$$[q,\mathrm{\infty }):\equiv u:{ℝ}_{𝖼}|q\le u\mathit{\hspace{1em}\hspace{1em}}\text{and}\mathit{\hspace{1em}\hspace{1em}}(-\mathrm{\infty },q]:\equiv u:{ℝ}_{𝖼}|u\le -q.$$

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

We summarize the algebraic structure of ${ℝ}_{𝖼}$ 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