3.1.1 The set ${{\left\langle {B}\right\rangle}}$ of tight representations of real numbers

The goal of V. Ménissier-Morain in her thesis and in Ménissier-Morain (Reference Ménissier-Morain2005) was to define accurate integer sequences from real numbers together with arithmetic operations on these sequences. Thus, the construction goes from reals to integer sequences. In this article, we want to do the converse: from integer sequences to reals. More precisely, our goal is to prove that the so called tight representations of real numbers provide a construction of the real field (as Cauchy sequences or Dedekind cuts do, for instance). The consequence is that we have to find a new definition of these tight representations. Indeed, in Ménissier-Morain (Reference Ménissier-Morain2005), the definition of the tight representations of real numbers relies on the bound property (5), which involves the real represented by the integer sequence. So, the bound property cannot be used in the construction of the real field. The following theorem provides a formula that makes it possible to define the tight representations of real numbers in a construction of the real field, that is, without any real variable in the formula.

Theorem 1. An integer sequence ${{\left\langle {x_n}\right\rangle}}$ is a tight representation of a real number if and only if

(9) \begin{equation}\forall\, n\in\mathbb{Z},\exists\,i\in\mathbb{Z},\forall\, k\in\mathbb{N},\ B^i\left| B^k x_n - x_{n+k}\right| \le (B^i-1)(B^k+1).\end{equation}

Furthermore, the real x of which such a sequence ${{\left\langle {x_n}\right\rangle}}$ is the tight representation is unique, the rational sequence ${{\left\langle {x_n/B^n}\right\rangle}}$ is convergent and $x=\lim {{\left\langle {x_n/B^n}\right\rangle}}$.

We prove the above theorem in two steps. The first part (the only if part) corresponds to Lemma 2, whereas the second part (the if part) corresponds to Lemma 4.

satisfies Equation (9).

Proof Let $n\in\mathbb{Z}$. From the bound property (5), we get for any $k\in\mathbb{Z}$:

(10) \begin{align}B^n x &= x_n +\varepsilon_n\end{align}

(11) \begin{align}B^{n+k} x &= x_{n+k} +\varepsilon_{n+k},\end{align}

where $\varepsilon_n$ and $\varepsilon_{n+k}$ lie in $(-1,1)$.

Then, multiplying Equation (10) by $B^k$ and subtracting Equation (11), we obtain:

\begin{equation*}\left|B^k x_n - x_{n+k}\right| < B^k|\varepsilon_n|+1.\end{equation*}

Taking i such that $B^i > 1/(1-\left|\varepsilon_n\right|)$ (thus $i\ge 1$), we derive that

(12) \begin{equation}B^i\left|B^k x_n - x_{n+k}\right| < (B^i-1)B^k+B^i.\end{equation}

Assuming now $k\in\mathbb{N}$, we observe that both sides of Equation (12) are integers. We derive that, for any $k\in\mathbb{N}$,

\[B^i\left|B^k x_n - x_{n+k}\right|\le (B^i-1)(B^k+1).\]

In order to establish the if part of Theorem 1, i.e. that Equation (9) implies the bound property (5) for some real x, we need to characterize such a real starting from the integer sequence ${{\left\langle {x_n}\right\rangle}}$. This is done by exhibiting a Cauchy sequence.

Proof. Let $m\in\mathbb{Z}$. Let us prove that, for a sufficiently large integer n and any $k\in\mathbb{N}$, $\lvert \tfrac{x_n}{B^n}-\frac{x_{n+k}}{B^{n+k}}\rvert\le \tfrac1{B^m}$:

\begin{equation*}\begin{split}\left| \frac{x_n}{B^n}-\frac{x_{n+k}}{B^{n+k}}\right|& \le \frac1{B^{n+k}} \ \left| B^k x_n-x_{n+k}\right| \\&\le \frac1{B^{n+k}}\times \frac{(B^i-1)(B^k +1)}{B^i}\quad\text{thanks to (9)}\\& \le \frac1{B^{n+k}}\times B^{k+1} \\& \le \frac1{B^{n-1}}.\end{split}\end{equation*}

Thus, it is sufficient to choose $ n\geq m+1$.

We can now complete the proof of Theorem 1.

Proof. Let x be the limit of the Cauchy sequence ${{\left\langle {x_n/B^n}\right\rangle}}$ and $m\in\mathbb{Z}$. Let $i\in\mathbb{Z}$ such that, for any $k\in\mathbb{N}$, $B^i\left|B^k x_m - x_{m+k}\right|\le (B^i-1)(B^k+1)$. Let $k_i\in\mathbb{N}$ such that, for any $k\ge k_i$, $\lvert x-\tfrac{x_{m+k}}{B^{m+k}}\rvert \le \tfrac 1{2B^{m+i}}$. Then, for any $k\ge k_i$,

\begin{equation*}\begin{split}\lvert B^m x - {x_m}\rvert& \le B^m\left| x - \frac{x_{m+k}}{B^{m+k}}\right| + \frac{1}{B^{k}} \left| x_{m+k} - {x_m}{B^k}\right| \\& \le \frac{1}{2B^{i}} + \frac{(B^i-1)(B^k+1)}{B^{k+i}}\quad\text{from (9)}\\& \le 1-\frac1{2B^i}+\frac1{B^k}(1-\frac{1}{B^{i}}).\end{split}\end{equation*}

Since the integer k can be chosen arbitrarily large, the bound property holds:

\begin{equation*}\left| {B^m} x - {x_m}\right| < 1.\end{equation*}

Thanks to Theorem 1, and because any real number has a tight representation (for instance, the sequence ${{\left\langle {\left\lfloor{x B^n}\right\rfloor}\right\rangle}}$), we can define a subset of the integer sequences that represent real numbers without using any real variable.

Definition 5 (Tight adic sequence). A tight B-adic sequence is an integer sequence ${{\left\langle {x_n}\right\rangle}}$ such that:

\[\forall\, n\in\mathbb{Z}, \exists\,i\in\mathbb{Z},\forall\, k\in\mathbb{N},\ B^i\left| B^k x_n - x_{n+k}\right| \le (B^i-1)(B^k+1).\]

The set of all tight B-adic sequences is denoted by ${{\left\langle {B}\right\rangle}}$. The real number represented by a tight B-adic sequence ${{\left\langle {x_n}\right\rangle}}$ is denoted $\lim_B\!\big({{\left\langle {x_n}\right\rangle}}\big)$, or more simply, $\lim_B{{\left\langle {x_n}\right\rangle}}$.

Ménissier-Morain (Reference Ménissier-Morain2005) for which we can just assert that they lie in the set $\{0,1\}$ or in the set $\{-1,0\}$.

Indeed, since

\[B^i\left| B^k x_n - x_{n+k}\right| \le (B^i-1)(B^k+1) \implies \left|x_{n+k}\right| \le \left(1-\frac1{B_i}\right)\left(B^k+1\right)+B^k \left|x_n\right|,\]

and

\[\lim_{k\to -\infty}\left(1-\frac1{B_i}\right)\left(B^k+1\right)+B^k \left|x_n\right| < 1,\]

the assumption $\forall k\in\mathbb{Z},\ B^i\left| B^k x_n - x_{n+k}\right| \le (B^i-1)(B^k+1)$ implies $x_{n}=0$ when n is near $-\infty$.

The next section presents a set of integer sequences whose definition is simpler than the definition of tight B-adic sequences and that are almost tight representations of real numbers.

3.1.2 The set $\widetilde{{{\left\langle { B}\right\rangle}}}$ of loose representations of real numbers

The goal of this section is to examine what happens if we replace the strict inequalities in the bound property by large inequalities.

In doing so, we will see that we save the variable i in the intrinsic definition of a representation, going from 3 variables to 2 variables, thus obtaining a simpler statement:

\begin{align*}\forall\, n\in\mathbb{Z}, \exists\,i\in\mathbb{Z},\forall\, k\in\mathbb{N},\ B^i\left| B^k x_n - x_{n+k}\right| & \le (B^i-1)(B^k+1)\\ &\quad\quad\quad\quad\quad {\text{(Definition 5 [Tight}\, \textit{B}{\text{-adic sequence])}}},\end{align*}

versus

\[\forall\, n\in\mathbb{Z},\forall\, k\in\mathbb{N},\ \left| B^k x_n - x_{n+k}\right| \le B^k+1\quad\text{(Definition 10 [Loose}\ {B}\text{-adic sequence])}.\]

This simplification makes definitions and proofs much easier to carry out, at the very small cost of losing at most 1 unit beyond some index in the integer sequence, only for sequences converging toward reals with finite B-adic expansion (Proposition 8). For instance, the sequence ${{\left\langle {\dotsc, x_0=3, x_1=7, x_2=\underline{20}, x_3=\underline{60}, x_4=\underline{180}, \cdots}\right\rangle}}$ is a 3-adic sequence representing the rational $x=\,^{20}\!/_9$, and the underlined terms are common to all tight representations of x, whereas ${{\left\langle {\dotsc, x_0=3, x_1=7, {x_2=21}, {x_3=61}, {x_4=181}, \cdots}\right\rangle}}$ is a loose 3-adic sequence representing the rational x.

So, let us begin by naming this relaxed bound property.

Definition 7 (Loose representation). An integer sequence ${{\left\langle {x_n}\right\rangle}}_{n\in\mathbb{Z}}$ satisfies the weak bound property for the real x if, for any $n\in\mathbb{Z}$,

(13) \begin{equation} {x_n-1}\le {B^{n}} x \le {x_n+1}.\end{equation}

Such an integer sequence is called a loose representation of the real number x.

Next, for a given real x, we compare the set of its loose representations to the set of its tight representations. It is plain that any tight representation is a loose representation. We will see that the converse is almost true.

1. (1) if x has not a finite B-adic expansion, ${{\left\langle {x_n}\right\rangle}}$ is a tight representation of x.

2. (2) if x has a finite B-adic expansion, that is, $x= p/B^m$ for some $p,m\in\mathbb{Z}$, then there exists a tight representation ${{\left\langle {y_n}\right\rangle}}$ of x such that $x_n=y_n$ for any $n<m$ and $\left|x_n-y_n\right|=\left|x_n-xB^n\right|\le 1$ for any $n\ge m$.

Proof. Since ${{\left\langle {x_n}\right\rangle}}$ is a loose representation of x, we have

(14) \begin{equation}\left|x_n-xB^n\right|\le 1.\end{equation}

1. (1) If x has not a finite B-adic expansion, whatever the value of n, the left-hand side of (14) is not an integer. Then, Equation (14) is equivalent to $\left|x_n-xB^n\right| < 1$, that is, to the bound property (5) for x with order n.

2. (2) Assume that $x=p/B^m$ for some $p, m\in\mathbb{Z}$. Then, for any $n<m$ the left-hand side of (14) is not an integer and we conclude as above that $x_n$ satisfies the bound property for x at order n. In this case, we set $y_n=x_n$. Let n be an integer greater than or equal to m. Then $xB^n$ is an integer. So, setting $y_n=xB^n$, we get $\left|x_n-y_n\right|\le 1$. The sequence ${{\left\langle {y_n}\right\rangle}}$ clearly satisfies the bound property for any $n\in\mathbb{Z}$. Hence, the result holds.

Proposition 8 means that there is no difference between tight representations and loose representations for irrational numbers as $\pi$ or $\sqrt2$. Alike, both types of representations are also the same for the rational $x=\,^{20}\!/_{9}$ and the base $B=2$ for instance. If $B=3$, on the one hand, the terms of both the tight and loose 3-adic sequences representing x obey to equivalent rules until the index $n=2$. But, on the other hand, the terms beyond the index 2 are unique for tight representations of x (written in base 3, these terms are $\overline{202}, \overline{2020}, \overline{20200}, \dotsc$), whereas the subsequence ${{\left\langle {x_k}\right\rangle}}_{k\ge 2}={{\left\langle { \overline {201}, \overline{2021}, \overline{20201}, \dotsc}\right\rangle}}$ can be found in a loose representation of $^{20}\!/_{9}$.

We continue the study of the loose representations of reals by giving an “internal” definition of theses sequences, that is, a definition without reals.

Theorem 9. An integer sequence ${{\left\langle {x_n}\right\rangle}}$ is the loose representation of a real number if and only if

(15) \begin{equation}\forall\, n\in\mathbb{Z},\forall\, k\in\mathbb{N},\ \left| B^k x_n - x_{n+k}\right| \le B^k+1.\end{equation}

Furthermore, the real x of which such a sequence ${{\left\langle {x_n}\right\rangle}}$ is the representation is unique, the rational sequence ${{\left\langle {x_n/B^n}\right\rangle}}$ is convergent and $x=\lim {{\left\langle {x_n/B^n}\right\rangle}}$.

The proof of Theorem 9 is similar to the proof of Theorem 1. Therefore, to avoid a tedious repetition, we put it in Appendix A.

Alike we have defined the tight B-adic sequences as the integer sequences that are tight representations of real numbers, we can now define the loose B-adic sequences.

Definition 10 (Loose adic sequence). A loose B-adic sequence is an integer sequence ${{\left\langle {x_n}\right\rangle}}$ such that

\[\forall\, n\in\mathbb{Z},\forall\, k\in\mathbb{N},\ \left| B^k x_n - x_{n+k}\right| \le B^k+1.\]

The set of all loose B-adic sequences is denoted by $\widetilde{{{\left\langle { B}\right\rangle}}}$. The real number represented by a loose B-adic sequence ${{\left\langle {x_n}\right\rangle}}$ is denoted $\lim_B\!\big(\,{{\left\langle {x_n}\right\rangle}}\!\big)$, or more simply, $\lim_B\!{{\left\langle {x_n}\right\rangle}}$.

Note that, contrary to tight B-adic sequences (see Remark 6), replacing $\forall k\in\mathbb{N}$ by $\forall k\in\mathbb{Z}$ in the above definition has no effect.

Since it is plain that tight representations are loose representations, it follows that tight B-adic sequences are loose B-adic sequences. Nevertheless, it is interesting to have a proof of this inclusion relation that does not use real numbers:

\begin{align*}&{{\left\langle {x_n}\right\rangle}} \text{ is a tight $B$-adic sequence}&\\& \quad \quad \quad \quad \implies \forall n\in\mathbb{Z},\exists i\in\mathbb{Z},\forall k\in\mathbb{N},\ B^i\left| B^k x_n - x_{n+k}\right| \le (B^i-1)(B^k+1) \\& \quad \quad \quad \quad \implies \forall n\in\mathbb{Z},\exists i\in\mathbb{Z},\forall k\in\mathbb{N},\ B^i\left| B^k x_n - x_{n+k}\right| \le B^i(B^k+1) \\& \quad \quad \quad \quad \implies \forall n\in\mathbb{Z},\exists i\in\mathbb{Z},\forall k\in\mathbb{N},\ \left| B^k x_n - x_{n+k}\right| \le (B^k+1) \\& \quad \quad \quad \quad \implies \forall n\in\mathbb{Z},\forall k\in\mathbb{N},\ \left| B^k x_n - x_{n+k}\right| \le (B^k+1) \\& \quad \quad \quad \quad \implies {{\left\langle {x_n}\right\rangle}} {\text{is a loose}\, \textit{B}\,{\text{-adic sequence}}}.\end{align*}

In the following section, we compare the (tight, loose) B-adic sequences with the integer sequences used to define the set $\mathcal{H\;\!\!R}_\omega$.

3.1.3 Relations between the sets of integer sequences used to represent real numbers

In Section 2.1, we saw that the Harthong–Reeb line is defined as a quotient of the set $\text{O}({{\omega}})$ where ${{\omega}}$ is an “infinitely large number”. Taking ${{\omega}}={{\left\langle {B^n}\right\rangle}}$, $\text{O}({{\omega}})$ can be specified as the set of the integer sequences ${{\left\langle {x_n}\right\rangle}}_{n\in\mathbb{Z}}$ such that:

(16) \begin{equation}\exists n\in\mathbb{Z}, \exists i\in\mathbb{Z}, \forall k\in\mathbb{N},\; \left|x_{n+k}\right|\le B^{n+k+i}.\end{equation}

We also consider a subset of $\text{O}({{\omega}})$, introduced in Chollet et al. (Reference Chollet, Wallet, Fuchs, Andres and Largeteau-Skapin2012): the regular sequences. An integer sequence ${{\left\langle {x_n}\right\rangle}}$ is regular if the rational sequence ${{\left\langle {x_n/{{\omega}}_n}\right\rangle}}$ is a Cauchy sequence. In the thesis, the goal of this definition is to emphasize that the Harthong–Reeb line contains many non-regular elements which explain why the Harthong–Reeb line does not satisfies all the Heyting–Bridges axioms of the constructive real line. For consistency reasons, we will use the following definition.

Definition 11 (Regular sequence). An integer sequence ${{\left\langle {x_n}\right\rangle}}$ is regular if

(17) \begin{equation}\forall i\in\mathbb{Z}, \exists n\in\mathbb{Z}, \forall k\in\mathbb{N},\; B^i\left|B^k x_n - x_{n+k}\right|\le B^{n+k}.\end{equation}

The equivalence of this definition with the definition given in Chollet (Reference Chollet2010) is given in Appendix B. In particular, it is worth observing that Equation (17) is equivalent to (see Appendix B):

(18) \begin{equation}\forall i\in\mathbb{Z}, \exists n_0\in\mathbb{Z}, \forall n\ge n_0, \forall k\in\mathbb{N},\; B^i\left|B^k x_n - x_{n+k}\right|\le B^{n+k}.\end{equation}

Let ${{\left\langle {x_n}\right\rangle}}$ be a regular sequence and let $x=\lim{{\left\langle {x_n/B^n}\right\rangle}}$. We say that the sequence ${{\left\langle {x_n}\right\rangle}}$ is a free representation of x and we write $x=\lim_B{{\left\langle {x_n}\right\rangle}}$. The subset of $\text{O}({{\omega}})$ formed by the regular sequences is denoted by $\text{O}^{\text{reg}}({{\omega}})$.

These two subsets $\text{O}({{\omega}})$ and $\text{O}^{\text{reg}}({{\omega}})$ of the integer sequences are related to the (tight, loose) B-adic sequences by the following inclusion relations.

Proposition 12. For any integer $B\ge 2$,

\begin{equation*}{{\left\langle {B}\right\rangle}}\subset\widetilde{{{\left\langle { B}\right\rangle}}}\subset\text{O}^{\text{reg}}({{\omega}})\subset\text{O}({{\omega}}).\end{equation*}

• We saw in Section 3.1.2 that ${{\left\langle {B}\right\rangle}}\subset\widetilde{{{\left\langle { B}\right\rangle}}}$.

• Let ${{\left\langle {x_n}\right\rangle}}$ be a loose B-adic sequence. We have

  \[\forall n\in\mathbb{Z}, \forall k\in\mathbb{N},\ \left|B^k x_n-x_{n+k}\right|\le B^k+1.\]
  We have to prove Equation (17). So, let $i\in\mathbb{Z}$. Noting that $B^k+1\le B^{k+1}$ for any $k\ge 0$ (since $B\ge 2$), we derive that
  \[\forall n\in\mathbb{Z}, \forall k\in\mathbb{N},\ \left|B^k x_n-x_{n+k}\right|\le B^{k+1}.\]
  Then, multiplying both side of the inequality by $B^i$ and putting $n=i+1$,
  \[\exists n=i+1\in\mathbb{Z}, \forall k\in\mathbb{N},\ B^i\left|B^k x_n-x_{n+k}\right|\le B^{n+k}.\]
  Thus, ${{\left\langle {x_n}\right\rangle}}\in\text{O}^{\text{reg}}({{\omega}})$.

• Let ${{\left\langle {x_n}\right\rangle}}\in\text{O}^{\text{reg}}({{\omega}})$:

  \[\forall i\in\mathbb{Z}, \exists n\in\mathbb{Z}, \forall k\in\mathbb{N},\ B^i\left|B^k x_n - x_{n+k}\right|\le B^{n+k}.\]
  In particular, taking $i=0$,
  \[\exists n\in\mathbb{Z}, \forall k\in\mathbb{N},\ \left|B^k x_n-x_{n+k}\right|\le B^{n+k}.\]
  We derive that
  \[\exists n\in\mathbb{Z}, \forall k\in\mathbb{N},\ \left|x_{n+k}\right|\le B^{n+k}\left(1+B^{-n}\lvert x_n\rvert \right).\]
  We can now choose an integer j such that $B^j\ge 1+B^{-n}\lvert x_n\rvert$:
  \[\exists n\in\mathbb{Z}, \exists j=\left\lceil{\log_B\!\left(1+B^{-n}\lvert x_n\rvert \right)}\right\rceil\in\mathbb{Z}, \forall k\in\mathbb{N},\ \left|x_{n+k}\right|\le B^{n+k+j}.\]
  Thereby, according to Equation (16), ${{\left\langle {x_n}\right\rangle}}\in\text{O}({{\omega}})$.

Now that we have compared the four subsets of the integer sequences, the next step is to look at the four quotient spaces.

3.2.1 Canonical maps between the quotient spaces

The inclusion relations of Proposition 12 result in inclusion relations between the classes of the equivalence relation $=_{{{\omega}}}$ and the classes of its restrictions to the subsets ${{\left\langle {B}\right\rangle}}$, $\widetilde{{{\left\langle { B}\right\rangle}}}$ and $\text{O}^{\text{reg}}({{\omega}})$. Indeed, for any two sets $A\subset B$, any equivalence relation $E\subset B\times B$ and any $x\in A$, $\{y\in A\mid (x,y)\in E\}\subset\{y\in B\mid (x,y)\in E\}$, that is the class of $x\in A$ for the restriction of E to A is included in the class of x for E. These inclusions between equivalence classes result in turn in three canonical maps between the quotient spaces:

Definition 13 (Inclusions). The inclusions between the classes of the relation $=_{{{\omega}}}$ in the spaces ${\mathcal {B}_{{{\omega}}}}$, ${\widetilde{\mathcal {B}_{{{\omega}}}}}$, $\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}}({{\left\langle {B^n}\right\rangle}})$, and $\mathcal{H\;\!\!R}_\omega$ are denoted ${{\mathrm{inc_1}}}$, ${{\mathrm{inc_2}}}$, and ${{\mathrm{inc_3}}}$, respectively:

\begin{align*}{\mathcal {B}_{{{\omega}}}} & \xrightarrow{{{\mathrm{inc_1}}}} && {\widetilde{\mathcal {B}_{{{\omega}}}}} && \xrightarrow{{{\mathrm{inc_2}}}} && \mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}} && \xrightarrow{{{\mathrm{inc_3}}}} && \mathcal{H\;\!\!R}_\omega\\ x & \longmapsto && y = \left[\dot{x}\right] && \longmapsto && z = \left[\dot{y}\right] && \longmapsto && t = \left[\dot{z}\right]\end{align*}

where, given a class a in the source space, $\left[\dot{a}\right]$ denotes the unique class, in the destination space, including a (formally, the denotation stands for the class – in the destination space – of a representative – in the source space – of a)

Actually, the map ${{\mathrm{inc_3}}}$ is simply the identity function.

Let $i\in\mathbb{Z}$. Since x is regular, by Formula (18), there exists $n_0\in\mathbb{Z}$, such that for $n\ge n_0$ and any $k\in\mathbb{N}$,

(21) \begin{equation}B^{i+2}\left|B^k x_{n }- x_{n+k}\right|\le B^{n+k}.\end{equation}

Moreover, since $x=_{{\omega}} y$ and thanks to Formula (19), there exists $n\ge n_0\in\mathbb{Z}$ such that, for any $k\in\mathbb{N}$,

(22) \begin{align}B^{i+2}\left|x_{n+k}-y_{n+k}\right|&\le B^{n+k}\ \text{and,}\end{align}

(23) \begin{align}B^{i+2}\left|y_{n}-x_{n}\right|&\le B^{n} .\end{align}

Then, adding Equations (21), (22), and $B^k\times$ Equation (23), we get

\begin{equation*}B^2B^i\left|B^k y_n-y_{n+k}\right|\le3B^{n+k}.\end{equation*}

Since $B^2>3$, we are done: y is regular.

The following proposition expresses the fact that a class of $=_{{{\omega}}}$ in a given set obviously contains at most one class of the restriction of $=_{{{\omega}}}$ to a subset.

We end the comparison between the four quotient spaces by showing that any class of regular sequences contains a loose B-adic sequence and any class of loose B-adic sequences contains a tight B-adic sequence. Conversely, there exist elements in the Harthong–Reeb line that do not contain any regular sequence.

• ${{\mathrm{inc_1}}}$ is onto.

Let $a={{\left\langle {a_n}\right\rangle}}$ be a loose B-adic sequence. Put $b_n=\left\lfloor{\frac{a_n+2}{B^2}}\right\rceil$ if $B=2$ and $b_n=\left\lfloor{\frac{a_n+1}{B}}\right\rceil$ otherwise.

Let $n\in\mathbb{Z}$ and $k\in\mathbb{N}$. Then, assuming $B=2$,

\begin{equation*}\begin{split}B^2\left|B^k b_n - b_{n+k}\right|&\le B^2\left|B^{k}\left\lfloor{\frac{a_{n+2}}{B^2}}\right\rceil- \left\lfloor{\frac{a_{n+k+2}}{B^2}}\right\rceil\right| \\&\le \left|B^{k}a_{n+2}- {a_{n+k+2}}\right| + \frac{B^2}2\left(B^k+1\right) \\&\le \left(1+\frac{B^2}2\right)\left(B^k+1\right)\quad\text{for $a\in\widetilde{{{\left\langle { B}\right\rangle}}}$} \\&\le \left({B^2}-1\right)\left(B^k+1\right).\end{split}\end{equation*}

Thus, $b={{\left\langle {b_n}\right\rangle}}$ is a tight B-adic sequence. The proof in the case $B\ge 3$ is similar.

Let us now verify that the sequences a and b are equivalent. We only treat the case $B=2$, the other case being similar.

So, let $i\in\mathbb{Z}$, $n\in\mathbb{Z}$.

\begin{align*}B^i\left|a_{n}-b_{n}\right|&\le B^i\left|a_n-\frac{a_{n+2}}{B^2}\right|+\frac{1}{2}B^i\\&\le B^{i-2}\left|B^2a_n-{a_{n+2}}\right|+\frac{1}{2}B^i\\&\le B^{i-2}\left(B^2+1\right)+\frac{1}{2}B^i\quad\text{for $a\in\widetilde{{{\left\langle { B}\right\rangle}}}$}\\&\le B^i\left(\frac32+\frac1{B^2}\right)\\&\le 2B^i.\end{align*}

Thus, for any $n\ge i+1$, $B^i\left|a_{n}-b_{n}\right|\le B^{n}$, that is, $a=_{{{\left\langle {B^n}\right\rangle}}}b$. Eventually, $b\in{{\mathrm{inc_1}}}^{-1}(a)$ which proves that ${{\mathrm{inc_1}}}$ is onto.

• The map ${{\mathrm{inc_2}}}$ is onto.

The idea is to build a loose B-adic sequence from a regular one by pruning the latter sequence in order to satisfy Equation (15). Since the proof is rather long, it is given in Appendix C.

• ${{\mathrm{inc_3}}}$ is not onto.

The proof is given in Appendix D. Actually, we prove a stronger result. We define a natural topology over $\text{O}({{\omega}})$, and we show that the set of regular sequences is not a dense subset of the space $\text{O}({{\omega}})$ for this topology

whereas nonregular sequences form a dense subset of $\text{O}({{\omega}})$.

3.2.2 Field structures

We saw in Section 2.2 that $\mathcal{H\;\!\!R}_\omega$ is equipped with an ordered commutative ring structure, $(\mathcal{H\;\!\!R}_\omega,+,\times_{{\omega}},\le_{{\omega}})$. This section aims at propagating this structure to the subsets ${\mathcal {B}_{{{\omega}}}}$, ${\widetilde{\mathcal {B}_{{{\omega}}}}}$, and $\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}}({{\omega}})$.

Since ${{\mathrm{inc_3}}}$ is not onto, we need to verify that $\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}}({{\omega}})$ is stable for the operators $+$ and$\times_{{{\omega}}}$.

Let $a={{\left\langle {a_n}\right\rangle}}$ and $b={{\left\langle {b_n}\right\rangle}}$ be two regular sequences. Since the addition in $\mathcal{H\;\!\!R}_\omega$ is derived from the term-wise addition, it is sufficient to prove that the sequence ${{\left\langle {a_n+b_n}\right\rangle}}$ is regular, that is, for any $i\in\mathbb{Z}$, $\left|B^k (a_n + b_n) - (a_{n+k} + b_{n+k})\right|$ is less than $B^{n+k}/B^i$ for sufficiently large n and any $k\in\mathbb{N}$.

Let $i\in\mathbb{Z}$. Because a and b are regular, $\left|B^k a_n - a_{n+k} \right|$ and $\left|B^k b_n - b_{n+k}\right|$ are less than $B^{n+k}/B^{i+1}$ for sufficiently large n and for any $k\in\mathbb{N}$.

Then, for $B\ge 2$,

(24) \begin{equation}\left|B^k (a_n + b_n) - (a_{n+k} + b_{n+k})\right|\le 2\frac{B^{n+k}}{B^{i+1}}\le \frac{B^{n+k}}{B^{i}}.\end{equation}

• Multiplication

Recall that the product $\times_{{\omega}}$ in $\mathcal{H\;\!\!R}_\omega$ is defined by $[u]\times_{{\omega}}[v]=[(u\times v)\div {{\omega}}]$ where $[\cdot]$ stands for the equivalence class and $\times$, $\div$ are the term-wise multiplication and integer division, respectively.

Let $a={{\left\langle {a_n}\right\rangle}}$ and $b={{\left\langle {b_n}\right\rangle}}$ be two regular sequences. By abuse of notation, we write $a \times_{{\omega}} b$ for the sequence ${{\left\langle {(a_n b_n)\div {{\omega}}}\right\rangle}}$ (with ${{\omega}}=B^n$). In order to prove that ${{\mathrm{inc_3}}}\!(\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}})$ is stable for $\times_{{\omega}}$, it is sufficient to prove that $a\times_{{\omega}} b$ is regular.

So, let $i\in\mathbb{Z}$. We shall prove that

\[\left|B^k (a_n\times_{{\omega}} b_n) - (a_{n+k}\times_{{\omega}} b_{n+k})\right| \le B^{n+k}/B^i\]

for sufficiently large n and any $k\in\mathbb{N}$.

First, we split $\left|B^k (a_n\times_{{\omega}} b_n) - (a_{n+k}\times_{{\omega}} b_{n+k})\right|$ in three terms.

\begin{equation*}\begin{split}& \left|B^k (a_n\times_{{\omega}} b_n) - (a_{n+k}\times_{{\omega}} b_{n+k})\right|\\ &= \left|B^k \left((a_n b_n)\div B^n\right) - (a_{n+k} b_{n+k})\div B^{n+k}\right|\\&=\left|B^k \left(\frac{a_n b_n}{B^n}+\varepsilon_1\right)-\frac{a_{n+k} b_{n+k}}{B^{n+k}}+\varepsilon_2\right|\ \text{where $\varepsilon_1, \varepsilon_2\in(-1,1)$}\\&\le\left|\frac{b_n}{B^n}\left(B^{k}a_n-a_{n+k}\right)+\frac{a_{n+k}}{B^{n+k}}\left(B^{k}b_n-b_{n+k}\right)\right| +2B^{k} \\&\le M_b \left|B^ka_n-a_{n+k}\right|+M_a \left|B^kb_n-b_{n+k}\right| +2B^{k} ,\end{split}\end{equation*}

where $M_a=\sup_m\frac{a_m}{B^m}$ and $M_b=\sup_m\frac{b_m}{B^m}$.

Since the sequences a and b are regular, and thus in $\text{O}(B^n)$, $M_a<\infty$, and $M_b<\infty$. Hence, there exists $i_0\in\mathbb{N}$ such that $B^{i_0}>3\max\!(M_a, M_b)$. Furthermore, by Formula (18), for any i and for sufficiently large n,

\[B^{i_0+i}\left|B^ka_n-a_{n+k}\right|\le B^{n+k} \text{ and } B^{i_0+i}\left|B^kb_n-b_{n+k}\right|\le B^{n+k}.\]

Taking $n\ge \log_B6+i$, we also have $6B^{k+i}\le B^{n+k}$. Therefore, the three terms $M_b \left|B^ka_n-a_{n+k}\right|$, $M_a \left|B^kb_n-b_{n+k}\right|$ and $2B^k$ are less than, or equal to $B^{n+k}/{3B^i}$ which proves the result.

We can now extend the operators $+$, $\times_{{\omega}}$ and the binary relation $\le_{{\omega}}$ to the sets $\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}}$, $\widetilde{{{\left\langle { B}\right\rangle}}}$ and ${{\left\langle {B}\right\rangle}}$ (denoting by ${{\mathrm{inc_1}}}^{-1}$, resp. ${{\mathrm{inc_2}}}^{-1}$, the inverse function of ${{\mathrm{inc_1}}}$, resp. ${{\mathrm{inc_2}}}$, and by ${{\mathrm{inc_3}}}^{-1}$ the partial inverse function of ${{\mathrm{inc_3}}}$ defined on the set ${{\mathrm{inc_3}}}\!(\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}})$).

1. (1) $\forall x,y\in\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}}$

   \begin{align*}x+y & \ \overset{\mathrm{def}}{=} \ {{\mathrm{inc_3}}}^{-1}\!( {{\mathrm{inc_3}}}\!(x)+{{\mathrm{inc_3}}}\!(y))\\x\times_{{\omega}} y & \ \overset{\mathrm{def}}{=} \ {{\mathrm{inc_3}}}^{-1}\!( {{\mathrm{inc_3}}}\!(x)\times_{{\omega}}{{\mathrm{inc_3}}}\!(y))\\x\le_{{\omega}} y & \overset{\mathrm{def}}{\leftrightarrow} {{\mathrm{inc_3}}}\!(x)\le_{{\omega}}{{\mathrm{inc_3}}}\!(y).\end{align*}

2. (2) $\forall x,y\in{\widetilde{\mathcal {B}_{{{\omega}}}}}$,

   \begin{align*}x+y & \ \overset{\mathrm{def}}{=} \ {{\mathrm{inc_2}}}^{-1}\!( {{\mathrm{inc_2}}}\!(x)+{{\mathrm{inc_2}}}\!(y))\\x\times_{{\omega}} y & \ \overset{\mathrm{def}}{=} \ {{\mathrm{inc_2}}}^{-1}\!( {{\mathrm{inc_2}}}\!(x)\times_{{\omega}}{{\mathrm{inc_2}}}\!(y))\\x\le_{{\omega}} y & \overset{\mathrm{def}}{\leftrightarrow} {{\mathrm{inc_2}}}\!(x)\le_{{\omega}}{{\mathrm{inc_2}}}\!(y).\end{align*}

3. (3) $\forall x,y\in{\mathcal {B}_{{{\omega}}}}$,

   \begin{align*}x+y & \ \overset{\mathrm{def}}{=} \ {{\mathrm{inc_1}}}^{-1}\!( {{\mathrm{inc_1}}}\!(x)+{{\mathrm{inc_1}}}\!(y))\\x\times_{{\omega}} y & \ \overset{\mathrm{def}}{=} \ {{\mathrm{inc_1}}}^{-1}\!( {{\mathrm{inc_1}}}\!(x)\times_{{\omega}}{{\mathrm{inc_1}}}\!(y))\\x\le_{{\omega}} y & \overset{\mathrm{def}}{\leftrightarrow} {{\mathrm{inc_1}}}\!(x)\le_{{\omega}}{{\mathrm{inc_1}}}\!(y).\end{align*}

By Definition 18, we directly have the following properties.

The three morphisms ${{\mathrm{inc_3}}}$, ${{\mathrm{inc_2}}}$, and ${{\mathrm{inc_1}}}$ transfer the properties of $\mathcal{H\;\!\!R}_\omega$ to the other structures. Actually, ${\mathcal {B}_{{{\omega}}}}$, ${\widetilde{\mathcal {B}_{{{\omega}}}}}$, and $\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}}$ have a richer structure than $\mathcal{H\;\!\!R}_\omega$: their order relation is total and they are fields, not only rings.

Proof. Since ${{\mathrm{inc_1}}}$ and ${{\mathrm{inc_2}}}$ are bijective, it suffices to prove the result for the set $\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}}$. Moreover, because $\mathcal{H\;\!\!R}_\omega$ is an ordered ring, the order $\le_{{\omega}}$ is a total order of the subset $\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}}$ if and only if any nonzero element in $\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}}$ is positive or negative. So, let us consider a regular sequence $x={{\left\langle {x_n}\right\rangle}}$ that is not equivalent to the null sequence. From the definition of $=_{{{\left\langle {B^n}\right\rangle}}}$ (Equation (19)), we derive that there exists $i\in\mathbb{Z}$ and a sequence of indices ${{\left\langle {u_n}\right\rangle}}$ such that, for any $n\in\mathbb{Z}$,

(25) \begin{equation}u_n\ge n\quad\text{and}\quad B^i |x_{u_n}| > B^{u_n}.\end{equation}

A consequence of the existence of such a pair $(i,{{\left\langle {u_n}\right\rangle}})$ is that for large enough index n, the sign of $x_n$ is not null and constant. Indeed, from Equation (25), we get $x_{u_n}\neq 0$ for any n and from Formula (18), we derive that for large enough n, $B^i\left|B^kx_{u_n}-x_{u_n+k}\right|\le B^{u_n+k}$ for any $k\ge 0$. If, for some $k\ge 1$, $x_{u_n+k}$ has not the same sign as $x_{u_n}$, then it comes that $B^i\left|B^kx_{u_n}\right|\le B^{u_n+k}$, that is $B^i\left|x_{u_n}\right|\le B^{u_n}$ which contradicts Equation (25). Since there exists $n_0\in\mathbb{Z}$ such that $\forall n\ge n_0,\ x_n\ge 0$ or $\forall n\ge n_0,\ x_n\le 0$, we easily get from the definition of $\le_{{\omega}}$, Equation (4), that either $\left[x\right]\ge0$ or $\left[x\right]\le 0$ and, because $\left[x\right] \neq 0$, $\left[x\right]>0$ or $\left[x\right] < 0$.

• First, we prove that the tuple $({{\mathrm{inc_3}}}\!(\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}}),+,\times_{{\omega}}, \le_{{\omega}})$ is a subring of $\mathcal{H\;\!\!R}_\omega$. We already have proved that ${{\mathrm{inc_3}}}\!(\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}})$ is stable for the operators $+$ and $\times_{{\omega}}$. It remains to prove that the opposite of an element in ${{\mathrm{inc_3}}}\!(\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}})$ is still in ${{\mathrm{inc_3}}}\!(\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}})$. Since, obviously, $[\!{{\left\langle {-x_n}\right\rangle}}\!]$ is the opposite class of $[\!{{\left\langle {x_n}\right\rangle}}\!]$ in $\mathcal{H\;\!\!R}_\omega$, it suffices to prove that for any regular sequence $x={{\left\langle {x_n}\right\rangle}}$, the sequence ${{\left\langle {-x_n}\right\rangle}}$ is regular. The proof is straightforward.

• Second, we show that ${{\mathrm{inc_3}}}\!(\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}})$ is a field. At this aim, we define a map $\mathrm{inv}\colon {{\mathrm{inc_3}}}\!(\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}})\setminus\left[{{\left\langle {0}\right\rangle}}\right]\to{{\mathrm{inc_3}}}\!(\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}})$ by putting

  \[\mathrm{inv}\!( \left[{{\left\langle {x_n}\right\rangle}}\right] )=\left[{{\left\langle {\left\lfloor{\frac{B^{2n}}{x_n}}\right\rceil}\right\rangle}}\right],\]
  where the representative ${{\left\langle {x_n}\right\rangle}}$ is chosen such as $x_n\neq 0$ for any $n\in\mathbb{Z}$ (this can be achieved for instance by replacing the zero terms by ones).

Let $x\in{{\mathrm{inc_3}}}\!(\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}})\setminus\left[{{\left\langle {0}\right\rangle}}\right]$. Let us prove that inv is well-defined, that is, $\mathrm{inv}(x)\in{{\mathrm{inc_3}}}\!(\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}})$ and $\mathrm{inv}(x)$ does not depend on the choice of the representative of x.

• Let ${{\left\langle {x_n}\right\rangle}}\in x$. We claim that

  (26) \begin{equation} \exists i_0\in\mathbb{Z}, \exists n_0\in\mathbb{Z}, \forall n\ge n_0, \ \left|x_n\right|\ge B^{n-i_0}. \end{equation}
  Indeed, by hypothesis, ${{\left\langle {0}\right\rangle}}\notin x$. Then, the negation of Equation (19) yields an integer $i_1$ such that for any $n\in\mathbb{Z}$, there exists $k_n\in\mathbb{N}$ such that
  (27) \begin{equation} B^{i_1}\left|x_{n+k_n}\right|>B^{n+k_n}. \end{equation}
  Moreover, thanks to the regularity of ${{\left\langle {x_n}\right\rangle}}$ and Equation (18), there exists $n_0\in\mathbb{Z}$ such that, for any $n\ge n_0$,
  \[B^{i_1+1}\left|B^{k_n} x_n-x_{n+k_n}\right|\le B^{n+k_n}.\]
  Then, splitting the absolute value,
  \[B^{i_1+1}\left(\left|x_{n+k_n}\right|-B^{k_n}\left|x_n\right|\right)\le B^{n+k_n}.\]
  Using Equation (27),
  \[B B^{n+k_n}-B^{i_1+1+k_n}\left|x_n\right|\le B^{n+k_n}.\]
  We derive that
  \[B^{n-i_1}\frac{B-1}{B} < \left|x_n\right|.\]
  Since $B\ge2$, we have $(B-1)/B\ge 1/B$. Hence, choosing $i_0=i_1+1$, the claim is established.

• Let ${{\left\langle {x_n}\right\rangle}}\in x$ with $x_n\neq 0$ for any $n\in\mathbb{Z}$. We now prove that the sequence ${{\left\langle {B^{2n}/x_n}\right\rangle}}$ is regular. The integers $i_0$ and $n_0$ are those defined in the previous item. Let $i\in\mathbb{Z}$ and $n\ge n_0$. We have

  \begin{equation*} \begin{split} B^i\left|B^k\frac{B^{2n}}{x_{n}}-\frac{B^{2(n+k)}}{x_{n+k}}\right| &= B^{i+2n+k}\frac{\left|x_{n+k}-B^kx_{n}\right|}{{\left|x_{n}\right|}{\left|x_{n+k}\right|}} \\ &\le B^{i+2n+k}\frac{\left|B^k x_{n}-x_{n+k}\right|}{B^{n-i_0}B^{n+k-i_0}}\\ &\le B^{i+2q_0}\left|B^k x_{n}-x_{n+k}\right|. \end{split} \end{equation*}
  Since x is regular, for sufficiently large n and any $k\in\mathbb{N}$, we have $B^{i+2q_0}\left|B^k x_{n}-x_{n+k}\right|\le B^{k+n}$, so we are done: the sequence ${{\left\langle {B^{2n}/x_n}\right\rangle}}$ is regular.

• We prove that the function inv is independent of the choice of the representative. Let ${{\left\langle {x_n}\right\rangle}}$ and ${{\left\langle {y_n}\right\rangle}}$ be two representatives of x with $x_n\neq 0$ and $y_n\neq 0$ for any $n\in\mathbb{Z}$. Let $i_0^x$, $i_0^y$, $n_0^x$, and $n_0^y$ be integers provided by Equation (26) for the sequences ${{\left\langle {x_n}\right\rangle}}$ and ${{\left\langle {y_n}\right\rangle}}$.

Let $i\in\mathbb{Z}$ and $n\ge\max\!(n_0^x, n_0^y)$. We have

\begin{equation*} \begin{split} B^i\left|\frac{B^{2(n+k)}}{x_{n+k}}-\frac{B^{2(n+k)}}{y_{n+k}}\right| &= B^{i+2(n+k)}\frac{\left|x_{n+k}-y_{n+k}\right|}{\left|x_{n+k}y_{n+k}\right|} \\ &\le B^{i+i_0^x+i_0^y}\left|x_{n+k}-y_{n+k}\right|. \end{split} \end{equation*}

Because ${{\left\langle {x_n}\right\rangle}}=_{{\omega}}{{\left\langle {y_n}\right\rangle}}$, $B^{i+i_0^x+i_0^y}\left|x_{n+k}-y_{n+k}\right|\le B^{n+k}$ for sufficiently large n and any $k\in\mathbb{N}$, which proves that ${{\left\langle {B^{2n}/x_n}\right\rangle}}$ and ${{\left\langle {B^{2n}/y_n}\right\rangle}}$ are equivalent: $\mathrm{inv}(x)$ is independent of the choice of the representative for x.

It remains to prove that $\mathrm{inv}(x)$ is actually the inverse of x, that is, $x\times_{{\omega}}\mathrm{inv}\!(x)=\left[{{\omega}}\right]$.

Given ${{\left\langle {x_n}\right\rangle}}\in x$, we compute a representative of $x\times_{{\omega}} \mathrm{inv}(x)$ and show that this representative is equivalent to the unity element of the ring $\text{O}({{\omega}})$ which is the sequence ${{\omega}}={{\left\langle {B^n}\right\rangle}}$ itself:

\begin{align*}\left\lfloor{\frac{{x_n} \times \left\lfloor{\frac{B^{2n}}{x_n}}\right\rceil}{B^n}}\right\rfloor &= \varepsilon_1+\frac{x_n}{B^n}\varepsilon_2+B^n \\ &\quad\text{where $\varepsilon_1\in( -\!1,0]$ and $\varepsilon_2\in\Big( -\!\frac{1}{2},\frac{1}{2}\Big]$}\\ & = \varepsilon+B^n\quad\text{where $|\varepsilon|\le 1+{\text{sup}_n}{\frac{\left|x_n\right|}{B^n}}$}. \end{align*}

The latter inequality clearly establishes that $x\times_{{\omega}}\mathrm{inv}\!(x)=\left[{{\omega}}\right]$.

• Finally, thanks to the isomorphisms ${{\mathrm{inc_3}}}$ (whose codomain is restricted to ${{\mathrm{inc_3}}}\!(\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}})$), ${{\mathrm{inc_2}}}$, and ${{\mathrm{inc_1}}}$, we derive that $\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}}$, ${\mathcal {B}_{{{\omega}}}}$, and ${\widetilde{\mathcal {B}_{{{\omega}}}}}$ are also ordered commutative fields.

The following proposition shows that the operations $+_B$ and $\cdot_B$ defined in Ménissier-Morain (Reference Ménissier-Morain2005) (see Section 2.2) directly perform the operations of the fields $({\mathcal {B}_{{{\omega}}}},+,\times_{{\omega}})$ and $({\widetilde{\mathcal {B}_{{{\omega}}}}}, +, \times_{{\omega}})$, avoiding the cost of the computation of the function ${{\mathrm{inc_2}}}^{-1}$ (see the proof of Proposition 16).

Then,

\[x+y=\left[\dot{x} +_B \dot{y}\right]\quad\text{and}\quad x\times_{{\omega}} y=\left[\dot{x} \cdot_B \dot{y}\right].\]

We split the proof of Proposition 22 by stating Lemma 23 (addition of integer sequences) and Lemma 24 (multiplication of integer sequences).

The last part of the proof is devoted to formally switching to quotient spaces.

Lemma 23. Let x and y be two regular sequences. Then,

\[x+_B y\ =_{{\omega}}\ x + y.\]

Proof. Let $x={{\left\langle {x_n}\right\rangle}}$ and $y={{\left\langle {y_n}\right\rangle}}$ be two integer sequences. Put $z = x +_B y$ and $z' = x + y$. In order to prove the proposition, we have to show that

\[\forall i\in\mathbb{Z}, \exists n\in\mathbb{Z},\forall k\in\mathbb{N},\ B^i|z'_{n+k}-z_{n+k}|\leq B^{n+k}.\]

So, let $i\in\mathbb{Z}$. By definition, $z'_n=x_n+y_n$ and $z_n = \left\lfloor{ ({x_{n+r} + y_{n+r}})/{B^r}}\right\rceil = ({x_{n+r} + y_{n+r}})/{B^r} + \varepsilon $ with $r\in\{1,2\}$ (depending on the value of B) and $|\varepsilon| \leq \frac{1}{2}$.

Thereby, we have

\begin{equation*}\begin{split}B^i&|z'_{n+k}-z_{n+k}| \\& =B^i\left| x_{n+k} + y_{n+k} - \frac{x_{n+k+r} + y_{n+k+r}}{B^r} - \varepsilon\right|\\& = B^i\left| \frac{B^r x_{n+k} - x_{n+k+r}}{B^r} + \frac{B^r y_{n+k} - y_{n+k+r}}{B^r}- \varepsilon \right|\\&\leq \frac{1}{2}B^i + B^{-r}\big(B^i\left| {B^r x_{n+k} - x_{n+k+r}}\right| + B^i\left|{B^r y_{n+k} - y_{n+k+r}}\right|\big).\end{split}\end{equation*}

The sequences x and y are regular. Thus, according to Equation (18), for sufficiently large n and for any $k\in\mathbb{N}$, we have $B^i\left|B^r x_{n+k} - x_{n+k+r}\right|\le B^r$ and $B^i \left|B^r x_{n+k} - x_{n+k+r}\right|\le B^r$. Therefore, for sufficiently large $n\in\mathbb{Z}$ and any $k\in\mathbb{N}$,

\[B^i|z'_{n+k}-z_{n+k}| \le 2 + \frac{1}{2} B^i.\]

As $2 + \frac{1}{2} B^i\le B^{n+k}$ for large enough n, we are done.

Lemma 24. Let $x={{\left\langle {x_n}\right\rangle}}$ and $y={{\left\langle {y_n}\right\rangle}}$ be two loose B-adic sequences. Then,

\[x\cdot_B y\ =_{{\omega}}\ x \times_{{{\omega}}} y.\]

From the definition of the product $\cdot_B$ (Equation (8)), we derive that, for large enough n,

\begin{equation*} z_n=\frac{a+ x_{p_x} y_{p_y}}{B^{p_x+p_y-n}}+\varepsilon , \end{equation*}

where $|a|=1$, $p_x=n+v-\mathrm{msd} (y)$, $p_y=n+v-\mathrm{msd} (x)$, $v \in\{3, 4, 5\}$ and $|\varepsilon|\le\frac{1}{2}$.

It follows that

\begin{equation*} \begin{split} \left|z'_n - z_n\right| & = \left|\frac{x_n \ y_n}{B^n} - \varepsilon' - \frac{a+ x_{p_x} y_{p_y}}{B^{p_x+p_y-n}} - \varepsilon\right|\quad \text{where $|\varepsilon'| < 1$}\\&\le\left|\frac{B^{p_x} x_n B^{p_y} y_n - B^n x_{p_x}B^ny_{p_y}}{B^{n+p_x+p_y}}\right|+2+B^{n-p_x-p_y} .\end{split}\end{equation*}

Provided we enforce $n-p_x-p_y\le 0$, that is, $n\ge \mathrm{msd} (x)+\mathrm{msd} (y)-2v$, we get

(28) \begin{equation}\left|z'_n - z_n\right| \le \left|\frac{B^{p_x} x_n B^{p_y} y_n - B^n x_{p_x}B^ny_{p_y}}{B^{n+p_x+p_y}}\right|+3.\end{equation}

We rewrite the first term of the right-hand side of the previous inequality as follows:

(29) \begin{equation}\frac{B^{p_x} x_n B^{p_y} y_n - B^n x_{p_x}B^ny_{p_y}}{B^{n+p_x+p_y}}=\frac{x_n}{B^n}\times\frac{B^{p_y}y_n-B^ny_{p_y}}{B^{p_y}}+\frac{y_{p_y}}{B^{p_y}}\times\frac{B^{p_x}x_n-B^nx_{p_x}}{B^{p_x}}.\end{equation}

Since x and y belong to $\mathcal{H\;\!\!R}_\omega$, we have $\frac{x_n}{B^n}\le\sup_p\frac{x_p}{B^p}<\infty$ and $\frac{y_n}{B^n}\le\sup_p\frac{y_p}{B^p}<\infty$. Moreover, since x and y are regular and thanks to Equation (18), for any $i_0\in\mathbb{Z}$ and for sufficiently large n,

(30) \begin{equation} \frac{\left|B^{p_y}y_n-B^ny_{p_y}\right|}{B^{p_y}}\le \frac{B^{\min\!(p_y,n)}B^{\max\!(p_y,n)}}{B^{p_y}B^{i_0}}\le \frac{B^{\max\!(P_y,n)}}{B^{i_0}}\le \frac{B^{n}B^{c_x}}{B^{i_0}}, \end{equation}

where $c_x$ is the constant $\left|n-p_y\right|=\left|\mathrm{msd} (x)-v\right|$.

Alike, for any $i_0\in\mathbb{Z}$ and for sufficiently large n,

(31) \begin{equation} \frac{\left|B^{p_x}x_n-B^nx_{p_x}\right|}{B^{p_x}}\le \frac{B^{n}B^{c_y}}{B^{i_0}}, \end{equation}

where $c_y$ is the constant $\left|n-p_x\right|=\left|\mathrm{msd} (y)-v\right|$.

From Formulae (28), (29), (30), and (31), we derive that, for any $i_0$, i and for some large enough n,

\begin{equation*}B^i\left|z'_n - z_n\right| \le M B^{i-i_0}B^n + 3B^i,\end{equation*}

where M is a constant $\left(M=c_x\sup_p\frac{x_p}{B^p}+c_y\sup_p\frac{y_p}{B^p}\right)$.

Finally, taking $i_0$ such that $MB^{i-i_0}<1$ and enforcing n to satisfy $MB^{i-i_0}+3B^{i-n}\le 1$, we get $B^i\left|z'_n - z_n\right| \le B^n$ for any $i\in\mathbb{Z}$ and sufficiently large $n\in\mathbb{Z}$. Thereby, we have proved that ${{\left\langle {z_n}\right\rangle}}=_{{\omega}} {{\left\langle {z'_n}\right\rangle}}$.

So, let $x, y\in{\widetilde{\mathcal {B}_{{{\omega}}}}}$. Then, $\dot{x}$ and $\dot{y}$ are regular sequences. Therefore, we derive from Lemma 23 that $\dot{x}+_B \dot{y}\ =_{{\omega}}\ \dot{x} + \dot{y}$. We set $\phi={{\mathrm{inc_3}}}\circ{{\mathrm{inc_2}}}$. Observe that, from Proposition 37, we get $\dot{x}+_B \dot{y}\in\widetilde{{{\left\langle { B}\right\rangle}}}$. Hence, $\phi\left(\left[\dot{x}+_B\dot{y}\right]\right)$ is well defined and belongs to $\mathcal{H\;\!\!R}_\omega$. We have

\begin{equation*}\begin{split}\dot{x}+_B \dot{y}=_{{\omega}}\ \dot{x} + \dot{y}&\implies \dot{x}+_B \dot{y}\in\left[\dot{x}+\dot{y}\right] \text{ where } \left[\dot{x}+\dot{y}\right]\in\mathcal{H\;\!\!R}_\omega\\&\implies \dot{x}+_B \dot{y}\in\left[\dot{x}\right]+\left[\dot{y}\right] \text{ by Equation (2)}\\&\implies \dot{x}+_B \dot{y}\in \phi(x)+\phi(y)\text{ by Definition 13}\\&\implies \dot{x}+_B \dot{y}\in \phi(x+y)\text{ by Proposition 19}\\&\implies \phi\left(\left[\dot{x}+_B \dot{y}\right]\right) = \phi(x+y) \text{ where } \left[\dot{x}+_B\dot{y}\right]\in{\widetilde{\mathcal {B}_{{{\omega}}}}}\\&\implies \left[\dot{x}+_B\dot{y}\right] =x+y\text{ by Proposition 15},\end{split}\end{equation*}

which is the stated result.

3.3.1 A natural equivalence relation for (free, loose, tight) representations

On the one hand, the Harthong–Reeb line $\mathcal{H\;\!\!R}_\omega$ was defined in Chollet et al. (Reference Chollet, Wallet, Fuchs, Andres and Largeteau-Skapin2012) as the quotient set $\text{O}({{\omega}})/\text{o}({{\omega}})$. On the other hand, it is natural to identify (free, loose, tight) representations of reals numbers that represents the same real number. Actually, these two equivalence relations are identical for the free representations^{Footnote 4} and thus for the other kinds of representation.

The proof is straightforward:

\begin{align*}{{\left\langle {x_n}\right\rangle}}=_{{\omega}} {{\left\langle {y_n}\right\rangle}}&\Longleftrightarrow\forall i\in\mathbb{Z}, \exists n_0\in\mathbb{Z}, n\ge n_0\implies B^i\left|x_n-y_n\right|\le B^n\\&\Longleftrightarrow\forall i\in\mathbb{Z}, \exists n_0\in\mathbb{Z}, n\ge n_0\implies \left|\frac{x_n}{B^n}-\frac{y_n}{B^n}\right|\le \frac1{B^i}\\&\Longleftrightarrow \lim\!{{\left\langle {\frac{x_n}{B^n}}\right\rangle}}=\lim\!{{\left\langle {\frac{y_n}{B^n}}\right\rangle}}\\&\Longleftrightarrow x=y.\end{align*}

As a consequence of Proposition 25, we can define a new map, $\lim_B$, from the field $\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}}$, resp. ${\widetilde{\mathcal {B}_{{{\omega}}}}}$, ${\mathcal {B}_{{{\omega}}}}$, to the field of real numbers:

\begin{align*}\lim{\!}_B\colon\qquad &\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}}\ (\text{resp. } {\widetilde{\mathcal {B}_{{{\omega}}}}}, {\mathcal {B}_{{{\omega}}}})&\longrightarrow\qquad &\mathbb R\\&\qquad x=\left[{{\left\langle {x_n}\right\rangle}}\right] &\longmapsto\qquad &\lim\!{{\left\langle {\frac{x_n}{B^n}}\right\rangle}}\end{align*}

In the next section, we show that the functions $\lim_B$ are isomorphisms.

3.3.2 Isomorphisms between the real number field and the representation fields

Our last result asserts that the addition, the multiplication, and the order relation of the three fields $\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}}$, ${\widetilde{\mathcal {B}_{{{\omega}}}}}$, ${\mathcal {B}_{{{\omega}}}}$ correspond, via the map $\lim_B$ to the addition, the multiplication, and the order of the real field $\mathbb R$. Since we have already shown that $(\mathcal{H\;\!\!R}_{{{\omega}}}^{\text{reg}},+,\times_{{\omega}},\le_{{\omega}})$, $({\widetilde{\mathcal {B}_{{{\omega}}}}},+,\times_{{\omega}},\le_{{\omega}})$, and $({\mathcal {B}_{{{\omega}}}},+,\times_{{\omega}},\le_{{\omega}})$ are isomorphic, we just now examine the map $\lim_B\colon{\mathcal {B}_{{{\omega}}}}\to\mathbb R$.