# Some representations of real numbers using integer sequences

Loïc Mazo, Marie-Andrée Jacob-da Col, Laurent Fuchs, Nicolas Magaud, Gaëlle Largeteau-Skapin

► To cite this version:

Loïc Mazo, Marie-Andrée Jacob-da Col, Laurent Fuchs, Nicolas Magaud, Gaëlle Largeteau-Skapin. Some representations of real numbers using integer sequences. Mathematical Structures in Computer Science, 2022, 32 (5), pp.648-681. 10.1017/S0960129522000342. hal-03276295v2

HAL Id: hal-03276295

https://hal.science/hal-03276295v2

Submitted on 15 Sep 2022

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Some representations of real numbers using
integer sequences

Loic Mazo¹, Marie-André Da Col-Jacob¹, Laurent Fuchs²,
Nicolas Magaud¹ and Gaëlle Skapin²

July 14, 2022

Abstract

The paper describes three models of the real field based on subsets of the integer sequences. The three models are compared to the Harthong-Reeb line. Two of the new models, contrary to the Harthong-Reeb line, provide accurate integer "views" on real numbers at a sequence of growing scales $B^n$ ($B \ge 2$).

# 1 Introduction

Modeling and computing with real numbers is a fundamental task in computer science. It remains a challenging issue and usually requires a trade-off between accuracy and efficiency. Floating-point numbers are widely used to model real numbers but they fail to form a field and though they are scattered in a wide interval, there is only finitely many of them. Proof assistants need more faithful models. The approaches used are either abstract, simply relying on some axiom systems (PVS, Coq standard library) or concrete, actually implementing the real numbers as a concrete datatype together with some operations. In the latter case, real numbers can be derived from Cauchy sequences (HOL Light, Isabelle, C-CoRN Coq library, NASA PVS Library), Dedekind cuts (Mizar, HOL4, ProofPower-HOL) and Non-Standard Analysis (ACL2(r), Isabelle non-standard library). The reader can find more information on these models in the survey [BLM16]. The main objective of our research on real number models is not to propose a new model but rather to have a model that makes it possible to switch from the discrete calculus to the continuous one, especially when dramatic changes occur. For instance, Euclidean rigid motions and their digital versions have distinct topological and set theoretical properties like homology preservation and bijectivity which are ensured in the former case and not in the latter case. Among the different kinds of models cited above, those that allow to examine how the convergence from a discrete representation to a continuous one unfolds are those using sequences (of rationals or integers) to obtain real numbers. Indeed, with convergent sequences one could get snapshots of the
convergence process by choosing some indices in the sequences. Nevertheless, to be usable, the convergence speed of the sequences has to be known. This is the case with the HOL Light model. But this model only ensures that for any sequence, there exists a parameter that controls the convergence speed. In other words, the speed depends on the real. Thus, the model will be hardly tractable in situations appealing to many reals which is generally the case. Another solution would be to use the standard positional notation. It comes down to have a Cauchy sequence with the advantage that the convergence speed is known and common to all reals. But the positional notation badly behaves with operations. Let us borrow an example from [Cia03]: deciding what is the first digit of the product $3 \times 0.333...$ is not possible, even if you postpone the decision until reading $n$ digits in the right term. If you choose 9, you are wrong if you are computing $3 \times (1/3)$ but if you choose 1 you are wrong in all the other cases. To work around this issue, one of the easiest solution is to allow negative digits in the positional notation. This is the choice made in [CDG06] with a signed-digit positional model with base 2 (the model is implemented in Coq).

The real number models presented in this paper originate in a discrete model of the continuum proposed and developed by [CWF+09, CWF+12] —see also Chollet’s PhD thesis, [Cho10]. The model of the continuum, studied by Chollet, is called the *Harthong-Reeb line*. It is based on the one hand on the works of [Har89] and Reeb [DR89] in nonstandard analysis and, in the other hand on the works of [SL58], [Lau83], in constructive mathematics. The Harthong-Reeb line is equipped with an algebraic structure in correspondence with the ordered commutative field structure of the real numbers and implemented in the Coq system [MCF15]. Thanks to this model, [CWF+12] are able to build a multiscale arithmetic representation of the plane curve $y = x(t)$ solution of the Cauchy problem $x' = F(t, x)$, $x(t_0) = x_0$. A few years later, [Maz19] proposed a multiscale representation of the affine transformations whose snapshots are the arithmetic *quasi-affine transforms* developed by M.A. Da-Col, see for instance [DCT09]. Nevertheless, these multiscale representations come up against the same pitfall: the scale in Chollet’s model is not correlated with the accuracy. Therefore, only qualitative, asymptotic results can be stated. It is impossible to give any quantitative guaranty at a given scale.

In order to connect a real number with each of its representations at the different scales in the Harthong-Reeb line, mixing the model with the sequences of rationals provided by a positional numeration system is a natural solution. Rather than the model developed by Ciaffaglione which only comes with base 2 and a few functions, we choose to incorporate inside the Harthong-Reeb line the *representations* of real numbers defined by [Mén05] —see also her PhD thesis, [Mén95]. Incorporating such efficient representations in the Harthong-Reeb line allows to bridge the gap between the abstract formal description of the Harthong-Reeb line and an actual efficient and usable concrete implementation. Given a scale $n \in \mathbb{Z}$ (also called *order*), such a representation $x_n \in \mathbb{Z}$ is linked to the represented real number $x$ by the following inequality:

$$|x_n - B^n x| < 1, \qquad (1)$$
where $B \ge 2$ is the *base* of the representations. Though the presentation is very
different, it can be seen that such representations could be expressed with a
positional encoding. This step is not done in this paper and will be accomplished
in a future work. In the work of V. Menissier-Morain, besides the fact that there
is a tight link between the real numbers and their representations, we also find
a set of operations, algebraic and transcendental functions to deal with such
representations. Hence, this paper is devoted to compare, and in a certain
way to merge, Chollet's model of the continuum with the representations of V.
Menissier-Morain together with their algebraic operations.

The paper is organized as follows.

- In Section 2, we recall the definitions of the Harthong-Reeb line and the representations of V. Menissier-Morain —let us called them tight representations in the sequel— with their operations.

- We propose in Section 3.1 a characterization of sequences that are tight representations of some real. The characterization does not appeal to real numbers (contrary to Eq. 1 which is used by V. Menissier-Morain). We also define the loose representations which are obtained by replacing the strict inequality in Eq. (1) by a (non strict) inequality. In addition to the two previous sets of integer sequences and to Chollet's sequences, regular sequences are considered. Regular sequences, introduced in [CWF+12], are integer sequences derived from rational Cauchy sequences.

- Section 3.2 is devoted to the quotient spaces defined from the sets of integer sequences using the same equivalence relation that permits to build the Harthong-Reeb line. Each quotient space comes with an ordered ring, or field, structure.

- Eventually, Section 3.3 establishes the isomorphisms between the quotient spaces (except the Harthong-Reeb line) and the ordered field of the real numbers.

2 Background

2.1 The Harthong-Reeb line

Basically, in the Harthong-Reeb line model, a real number $x$ is a sequence of
integers, each term of the sequence providing a *view* on $x$ at a growing *scale*
as we go through the sequence. The construction of the Harthong-Reeb line is
rather intuitive. For short, real numbers are modeled by sequences of rationals
which in turn are converted to integers thanks to a given sequence of increasing
scales.

In the sequel, given an equivalence relation $\sim$ on a set $X$, we denote by $[a]$ the equivalence class of $a \in X$ and by $\dot{c}$ any representative of the class $c \in X/\sim$ (all the operations defined below are well-defined, that is, they do not depend on the choice of the representatives).
Firstly, we present the classes of rational sequences and their operations. Using the Landau notations, we consider the subsets O(1) and o(1) of the rational sequences and we denote by $\mathbb{Q}_{\text{lim}}$ the quotient space O(1)/o(1) of the bounded sequences of rationals up to the sequences converging toward 0. For any $(\pi, \rho) \in \mathbb{Q}_{\text{lim}}$, we set:

$$ \pi + \rho \stackrel{\text{def}}{=} [\dot{\pi} + \dot{\rho}] , $$

$$ \pi \times \rho \stackrel{\text{def}}{=} [\dot{\pi} \times \dot{\rho}] , $$

where, on the right hand side of the equalities, + and × are the term-wise operations on the rational sequences. In a general way, throughout this article, the operations and relations on integer sequences denoted as an operation or a relation on integers are performed term-wise. The restriction of $\mathbb{Q}_{\text{lim}}$ to the classes of the Cauchy sequences is noted $\mathbb{Q}_{\text{Ca}}$. It is well-known that the limit operator provides an isomorphism from $(\mathbb{Q}_{\text{Ca}}$, $+$, $\times$) to $(\mathbb{R}$, $+$, $\times$).

Next, we have to transform rationals in integers. Let $\omega = \langle \omega_n \rangle$ be an increasing sequence of positive integers $\omega_n$, $n \in \mathbb{N}$. Such a sequence is called an *infinitely large number*. We consider the subsets O($\omega$) and o($\omega$) of $\mathbb{Z}^{\mathbb{N}}$ (Landau notations) and we define the Harthong-Reeb line, $\mathcal{HR}_{\omega}$, as the quotient space O($\omega$)/o($\omega$). We denote by $\omega_\omega$ the corresponding equivalence relation. The Harthong-Reeb line is equipped with the following operations.

$$ u + v \stackrel{\text{def}}{=} [\dot{u} + \dot{v}] , \qquad (2) $$

$$ u \times_{\omega} v \stackrel{\text{def}}{=} [(\dot{u} \times \dot{v}) \div \omega] , \qquad (3) $$

where $\div$ denotes the (term-wise) integer division: $a \div b = \lfloor a/b \rfloor$.

The set $\mathcal{HR}_{\omega}$ is also equipped with a partial order relation, $\leq_{\omega}$:

$$ [\langle x_n \rangle] \leq_{\omega} [\langle y_n \rangle] \text{ if } \forall p \in \mathbb{N}, \exists n_0 \in \mathbb{N}, n \geq n_0 \implies p(x_n - y_n) \leq \omega_n. \qquad (4) $$

The relation $\leq_{\omega}$ is well-defined (the choice of the representatives does not matter). The tuple $(\mathcal{HR}_{\omega}, +, \times_{\omega}, \leq_{\omega})$ is an ordered commutative ring [CWF$^+$09, CWF$^+$12, MCF15].

It was proved in [CWF$^+$09, CWF$^+$12] that $\mathcal{HR}_{\omega}$ and $\mathbb{Q}_{\text{lim}}$ are isomorphic via the map $\phi_{\omega}$ and its converse $\psi_{\omega}$ (both maps are well-defined):

$$ \phi_{\omega}: \mathcal{HR}_{\omega} \to \mathbb{Q}_{\text{lim}} \qquad \psi_{\omega}: \mathbb{Q}_{\text{lim}} \to \mathcal{HR}_{\omega} \\ \phi_{\omega}(u) = [\dot{u}/\omega] \qquad \psi_{\omega}(\pi) = [\lfloor \omega \times \dot{\pi} \rfloor] $$

We end this section about the Harthong-Reeb line by an example. Let $\omega$ be the sequence $\langle 10^n \rangle$. To obtain the image of $\sqrt{3}$ in $\mathcal{HR}_{\omega}$, we need a sequence of rationals converging toward $\sqrt{3}$. So, using the Babylonian algorithm, we set $b(0) = 3$ and $b(n+1) = (b(n) + 3/b(n))/2$ for any $n \in \mathbb{N}$. Then, the projection of $b$ on $\mathbb{Q}_{\text{lim}}$ represents the real $\sqrt{3}$ in $\mathbb{Q}_{\text{lim}}$. Finally, the morphism $\psi_{\omega}$ yields the Harthong-Reeb number which represents $\sqrt{3}$ in $\mathcal{HR}_{\omega}$. It is the class (for the relation $=_{\omega}$) of the sequence $\langle \lfloor 10^n b(n) \rfloor \rangle$, that is the sequence
3, 20, 175, 1732, 17320, 173205, ... up to sequences dominated by $10^n$ asymptotically.

Since one of the goals of this article is to compare the Harthong-Reeb line with sequences, defined in Sections 2.2 and 3, that are indexed by $\mathbb{Z}$, from now on we assume that the sequences in $\mathcal{HR}_\omega$ are defined on $\mathbb{Z}$. Actually, the values of the sequences for the negative indexes is not meaningful since equality between Harthong-Reeb numbers is asymptotically evaluated (toward positive infinity).

The Harthong-Reeb line is so unconstrained that it is spoiled with undesirable numbers that have no inverse and are neither zero nor positive nor negative (Appendix D gives some topological insight about this problem). Furthermore, because of the lack of constraint and contrary to a positional numeration system, the view $x_n$ of a real number $x$ at a given scale $n$ provided by the model does not necessarily give an accurate approximation of $x$. Only the whole integer sequence $(x_n)$ can give such an information. Indeed, since the model can be described using Landau notations, it only relies on convergence properties. For all these reasons, It is necessary to constrain the Harthong-Reeb model. This will be done in Section 3 by adopting the *bound property* and the algorithms presented in the following subsection.

## 2.2 Representations of real numbers

In this section we describe the work of [Mén05] about arbitrary precision approximations of real numbers.

Let $B \in \mathbb{N}$, $B \ge 2$. Notice that we assume that $B$ is set for the rest of this article.

Let $x \in \mathbb{R}$. A sequence $\langle x_n \rangle_{n \in \mathbb{Z}}$ of integers is a *tight representation*<fnref n="1" /> of $x$ if, for any $n$, the *bound property of $x$ by $x_n$ for order $n$* is satisfied:

$$x_n - 1 < B^n x < x_n + 1. \qquad (5)$$

In other words, $\langle x_n \rangle$ is a tight representation of $x$ if, for any $n$, $x_n = \lfloor xB^n \rfloor$ or $x_n = \lceil xB^n \rceil$. In particular,

* $\lim x_n/B^n = x$;

* if $\langle x_n \rangle$ is a tight representation of $x$, then, for any $n < -\log_B(|x|)$, either $x_n = 0$ or $x_n = \varepsilon$ where $\varepsilon = 1$ if $x$ is positive and $\varepsilon = -1$ if $x$ is negative;

* the tight representations of a given integer coincide for the positive indices;

* the rational $q$ admits for tight representation the sequence $\langle q_n \rangle_{n \in \mathbb{N}}$ where

$$q_n = \lfloor B^n q \rfloor;$$

<footnote n="1">¹The qualifying adjective “tight” is not used in the original paper of [Mén05]. Here, we use it to distinguish these representations from another kind of representations—the *loose* representations—that will be introduced in the following section.</footnote>
• given $x, y \in \mathbb{R}$ with tight representations $\langle x_n \rangle$ and $\langle y_n \rangle$, the real $x + y$ admits for tight representation the sequence $\langle z_n \rangle_{n \in \mathbb{N}}$ where

$$z_n = \left\lfloor \frac{x_{n+w} + y_{n+w}}{B^w} \right\rfloor \quad \text{with } w = \begin{cases} 1 & \text{if } B \ge 4, \\ 2 & \text{if } B = 2 \text{ or } 3. \end{cases}$$

The binary operator over integer sequences

$$(\langle x_n \rangle, \langle y_n \rangle) \mapsto \langle z_n = \lfloor (x_{n+w} + y_{n+w})/B^w \rfloor \rangle$$

is denoted by $+_B$.

• The computation of the product tight representation needs the definition of the *most significant digit* (msd):

$$\text{msd}(\langle x_n \rangle_{n \in \mathbb{Z}}) = \min\{n \in \mathbb{Z}, |x_n| > 1\}.$$

For any tight representation $\langle x_n \rangle$ of a non-zero number, $\text{msd}(\langle x_n \rangle)$ is finite whereas $\text{msd}(\langle 0 \rangle) = +\infty$. Given two tight representations $\langle x_n \rangle$ and $\langle x'_n \rangle$ of $x$, $\text{msd}(\langle x_n \rangle)$ and $\text{msd}(\langle x'_n \rangle)$ may differ from one unit<fnref n="2" />. Moreover, for any $n \ge \text{msd}(\langle x_n \rangle)$ one has

$$B^{n-\text{msd}(\langle x_n \rangle)} \le |x_n| \le 2B^{n-\text{msd}(\langle x_n \rangle)+1}. \quad (6)$$

Actually, the computation of the product of two tight representations only needs the following bounded version of the function $\text{msd}$:

$$\text{msd}^*(\langle x_n \rangle, n) \stackrel{\text{def}}{=} \begin{cases} \text{msd}(\langle x_n \rangle) & \text{if } |x_0| > 1, \\ \inf(\text{msd}(\langle x_n \rangle), \sup(0, n)) & \text{otherwise.} \end{cases} \quad (7)$$

Observe that the condition $|x_0| > 1$ is equivalent to $\text{msd}(x) \le 0$, in which case $\langle x_n \rangle$ is the tight representation of a non-zero number and $\text{msd}(x)$ is finite. If $|x_0| \le 1$, that is $\text{msd}(\langle x_n \rangle) > 0$, and if $n > 0$, the computation of $\text{msd}^*(x, n)$ is done by an incremental search starting from 1 with at most $n$ steps. That way, contrary to the function $\text{msd}$, the value of $\text{msd}^*(\langle 0 \rangle, n)$ is finite, equal to 0 if $n \le 0$ and equal to $n$ otherwise.

Given $x, y \in \mathbb{R}$ with tight representations $\langle x_n \rangle$ and $\langle y_n \rangle$, the real $x \times y$

<footnote n="2">²For instance, with $B = 10$ and $x = \sqrt{2}$, we have $\text{msd}(\langle \lfloor \sqrt{2B^n} \rfloor \rangle) = 1$ and $\text{msd}(\langle \lceil \sqrt{2B^n} \rceil \rangle) = 0$.</footnote>
admits for tight representation the sequence $\langle z_n \rangle_{n \in \mathbb{N}}$ where<fnref n="3" />

$$ 
\begin{align*}
z_n &= \operatorname{sign}(x_{p_x}) \times \operatorname{sign}(y_{p_y}) \times \left\lfloor \frac{1 + |x_{p_x} y_{p_y}|}{B^{p_x + p_y - n}} \right\rfloor \\
\text{with } p_x &= \max \left( n - \operatorname{msd}^* \left( \langle y_n \rangle, \frac{n-w}{2} + v \right) + v, \left\lfloor \frac{n+w}{2} \right\rfloor \right) \\
\text{and } p_y &= \max \left( n - \operatorname{msd}^* \left( \langle x_n \rangle, \frac{n-w}{2} + v \right) + v, \left\lfloor \frac{n+w}{2} \right\rfloor \right) \\
\text{and } (v, w) &= \begin{cases} (3, 2) & \text{if } B \ge 4, \\ (3, 3) & \text{if } B = 3, \\ (4, 3) & \text{if } B = 2. \end{cases}
\end{align*}
$$

The binary operator over integer sequences

$$ (\langle x_n \rangle, \langle y_n \rangle) \mapsto \langle z_n = \operatorname{sign}(x_{p_x} y_{p_y}) \times \lfloor (1 + |x_{p_x} y_{p_y}|) / B^{p_x + p_y - n} \rfloor \rangle \quad (8) $$

is denoted by $\cdot_B$.

* Given $x \in \mathbb{R}$, the reader will find in [Mén95], algorithms to compute tight representations of $1/x$, $\sqrt[k]{x}$, $\exp(x)$, $\log_b(x)$, arctan($x$), $\sin(x)$, $\cos(x)$, etc.

* To get a tight representation of the quotient of two reals, one can combine a product and an inverse operation. Nevertheless, it can be useful to compute the division directly. In Appendix E, we give the formula yielding the quotient of two numbers from their respective tight representations.

Taking the same example as in Sec. 2.1 and according to [Mén95], a tight representation of $\sqrt{3}$ for $B = 10$ is given by the sequence $\langle \sqrt{x}(2n) \rangle$ where $\langle x_n \rangle = \langle 3, 30, 300, \dots \rangle$ is a tight representation of 3 and $\sqrt{x} = \lfloor \sqrt{x} \rfloor$ is returned by the algorithm $\{ \text{int } z = x; \text{int } y = z+1; \text{while } (z < y) \{ y = z; z = (y+x \div y) \div 2; \} \text{ return } y; \}$.

The obtained tight representation is the sequence 1, 17, 173, 17320, 173205, ...

# 3 From integer sequences to real numbers

## 3.1 Four sets of integer sequences

In this section, we define a subset of the integer sequences $\langle B \rangle$ that corresponds to the tight representations of the real numbers as defined in [Mén05] (see Section 2.2) but without using any real number. We will also introduce another

<footnote n="3">³In [Mén05], the author gives a definition of $z_n$ using msd instead of msd* but she explains just below the definition that, actually, the algorithm works with the msd* function.</footnote>
subset $\langle \tilde{B} \rangle$, slightly bigger than the first one, that has the advantage to have a simpler characterization. In the following, we set

$$ \omega = \langle B^n \rangle_{n \in \mathbb{Z}} $$

and we will compare these two sets $\langle B \rangle$ and $\langle \tilde{B} \rangle$ with $O(\omega)$ which is used to define $\mathcal{HR}_\omega$ (see Section 2.1), and with the Cauchy sequences of $O(\omega)$.

### 3.1.1 The set $\langle B \rangle$ of tight representations of real numbers

The goal of V. Ménissier-Morain in her thesis and in [Mén05] 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én05], 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 $\langle x_n \rangle$ is a tight representation of a real number if and only if

$$ \forall n \in \mathbb{Z}, \exists i \in \mathbb{Z}, \forall k \in \mathbb{N}, B^i |B^k x_n - x_{n+k}| \le (B^i - 1)(B^k + 1). \quad (9) $$

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

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

**Lemma 1.** If the sequence $\langle x_n \rangle$ is a tight representation of a real number, then $\langle x_n \rangle$ satisfies Equation (9).

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

$$ B^k x = x_n + \epsilon_n \quad (10) $$

$$ B^{n+k} x = x_{n+k} + \epsilon_{n+k}, \quad (11) $$

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

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

$$ |B^k x_n - x_{n+k}| < B^k |\epsilon_n| + 1. $$
Taking $i$ such that $B^i > 1/(1 - |\epsilon_n|)$ (thus $i \ge 1$), we derive that

$$B^i |B^k x_n - x_{n+k}| < (B^i - 1)B^k + B^i. \quad (12)$$

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 |B^k x_n - x_{n+k}| \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 $\langle x_n \rangle$. This is done by exhibiting a Cauchy sequence.

**Proposition 1.** Let $\langle x_n \rangle$ be an integer sequence satisfying Equation (9). Then, the sequence $\langle x_n/B^n \rangle$ is 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}$, $|\frac{x_n}{B^n} - \frac{x_{n+k}}{B^{n+k}}| \le \frac{1}{B^m}$:

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

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

□

We can now complete the proof of Theorem 1.

**Lemma 2.** Let $\langle x_n \rangle$ be an integer sequence satisfying Equation (9). Then, $\langle x_n \rangle$ satisfies the bound property (5) for the real $x$ that is the limit of the Cauchy sequence $\langle x_n/B^n \rangle$.

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

$$\begin{aligned}
|B^m x - x_m| &\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 - \frac{1}{2B^i} + \frac{1}{B^k} \left( 1 - \frac{1}{B^i} \right).
\end{aligned}$$
Since the integer $k$ can be chosen arbitrarily large, the bound property holds:

$$|B^m x - x_m| < 1.$$

□

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

**Definition 1 (Tight B-adic sequence).** A tight B-adic sequence is an integer sequence $\langle x_n \rangle$ such that:

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

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

**Remark 1.** If we strengthen Equation (9) by putting "$\forall k \in \mathbb{Z}$" instead of "$\forall k \in \mathbb{N}$", Lemma 1 is no more valid while Lemma 2 remains true. That way, we have the possibility of defining a subset of tight B-adic sequences that are zero below some threshold unlike the tight representations defined in [Mén05] for which we can just assert that they lie in the set $\{0, 1\}$ or in the set $\{-1, 0\}$. Indeed, since

$$B^i |B^k x_n - x_{n+k}| \le (B^i - 1)(B^k + 1) \implies |x_{n+k}| \le (1 - \frac{1}{B_i})(B^k + 1) + B^k |x_n|$$

and

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

the assumption $\forall k \in \mathbb{Z}, B^i |B^k x_n - x_{n+k}| \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 $\langle B \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:

$$\forall n \in \mathbb{Z}, \exists i \in \mathbb{Z}, \forall k \in \mathbb{N}, B^i |B^k x_n - x_{n+k}| \le (B^i - 1)(B^k + 1) \qquad (\text{Definition 1 [Tight B-adic sequence]}),$$
versus

$$ \begin{array}{l} \forall n \in \mathbb{Z}, \forall k \in \mathbb{N}, |B^k x_n - x_{n+k}| \le B^k + 1 \\ \text{(Definition 3 [Loose B-adic sequence])}. \end{array} $$

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 2). For instance, the sequence ..., $x_0 = 3$, $x_1 = 7$, $x_2 = 20$, $x_3 = 60$, $x_4 = 180$, ... is a 3-adic sequence representing the rational $x = 20/9$ and the underlined terms are common to all tight representations of $x$ whereas ..., $x_0 = 3$, $x_1 = 7$, $x_2 = 21$, $x_3 = 61$, $x_4 = 181$, ... is a loose 3-adic sequence representing the rational $x$.

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

**Definition 2** (Loose representation). An integer sequence $\langle x_n \rangle_{n \in \mathbb{Z}}$ satisfies the weak bound property for the real $x$ if, for any $n \in \mathbb{Z}$,

$$ x_n - 1 \le B^n x \le x_n + 1. \qquad (13) $$

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.

**Proposition 2.** Let $x$ be a real number and $\langle x_n \rangle$ be a loose representation of $x$. Then,

1. if $x$ has not a finite B-adic expansion, $\langle x_n \rangle$ is a tight representation of $x$.

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 $\langle y_n \rangle$ of $x$ such that $x_n = y_n$ for any $n < m$ and $|x_n - y_n| = |x_n - xB^n| \le 1$ for any $n \ge m$.

*Proof.* Since $\langle x_n \rangle$ is a loose representation of $x$, we have

$$ |x_n - xB^n| \le 1. \qquad (14) $$

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 $|x_n - xB^n| < 1$, that is to the bound property (5) for $x$ with order $n$.

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 $|x_n - y_n| \le 1$. The sequence $\langle y_n \rangle$ clearly satisfies the bound property for any $n \in \mathbb{Z}$. Hence, the result holds. $\square$
Proposition 2 means that there is no difference between tight representations and loose representations for irrational numbers as $\pi$ or $\sqrt{2}$. 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 202, 2020, 20200, ... ) whereas the subsequence $\langle x_k \rangle_{k \ge 2} = \langle 201, 202, 2021, 20201, ... \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 these sequences, that is a definition without reals.

**Theorem 2.** An integer sequence $\langle x_n \rangle$ is the loose representation of a real number if and only if

$$ \forall n \in \mathbb{Z}, \forall k \in \mathbb{N}, \quad |B^k x_n - x_{n+k}| \le B^k + 1. \qquad (15) $$

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

The proof of Theorem 2 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 3 (Loose B-adic sequence).** A loose B-adic sequence is an integer sequence $\langle x_n \rangle$ such that

$$ \forall n \in \mathbb{Z}, \forall k \in \mathbb{N}, \quad |B^k x_n - x_{n+k}| \le B^k + 1. $$

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

Note that, contrary to tight B-adic sequences (see Remark 1), 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:

$\langle x_n \rangle$ is a tight B-adic sequence

$$ \Rightarrow \forall n \in \mathbb{Z}, \exists i \in \mathbb{Z}, \forall k \in \mathbb{N}, B^i |B^k x_n - x_{n+k}| \le (B^i - 1)(B^k + 1) $$

$$ \Rightarrow \forall n \in \mathbb{Z}, \exists i \in \mathbb{Z}, \forall k \in \mathbb{N}, B^i |B^k x_n - x_{n+k}| \le B^i(B^k + 1) $$

$$ \Rightarrow \forall n \in \mathbb{Z}, \exists i \in \mathbb{Z}, \forall k \in \mathbb{N}, |B^k x_n - x_{n+k}| \le (B^k + 1) $$

$$ \Rightarrow \forall n \in \mathbb{Z}, \forall k \in \mathbb{N}, |B^k x_n - x_{n+k}| \le (B^k + 1) $$

$$ \Rightarrow \langle x_n \rangle \text{ is a loose B-adic sequence.} $$
In the following section, we compare the (tight, loose) B-adic sequences with the integer sequences used to define the set $\mathcal{H}\mathbb{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 $O(\omega)$ where $\omega$ is an “infinitely large number”. Taking $\omega = \langle B^n \rangle$, $O(\omega)$ can be specified as the set of the integer sequences $\langle x_n \rangle_{n \in \mathbb{Z}}$ such that:

$$ \exists n \in \mathbb{Z}, \exists i \in \mathbb{Z}, \forall k \in \mathbb{N}, |x_{n+k}| \le B^{n+k+i}. \quad (16) $$

We also consider a subset of $O(\omega)$, introduced in [CWF+12]: the regular sequences. An integer sequence $\langle x_n \rangle$ is regular if the rational sequence $\langle x_n/\omega_n \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 4 (Regular sequence).** An integer sequence $\langle x_n \rangle$ is regular if

$$ \forall i \in \mathbb{Z}, \exists n \in \mathbb{Z}, \forall k \in \mathbb{N}, B^i |B^k x_n - x_{n+k}| \le B^{n+k}. \quad (17) $$

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

$$ \forall i \in \mathbb{Z}, \exists n_0 \in \mathbb{Z}, \forall n \ge n_0, \forall k \in \mathbb{N}, B^i |B^k x_n - x_{n+k}| \le B^{n+k}. \quad (18) $$

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

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

**Proposition 3.** For any integer $B \ge 2$,

$$ \langle B \rangle \subset \widetilde{\langle B \rangle} \subset O^{\text{reg}}(\omega) \subset O(\omega). $$

*Proof.* We show the inclusions from left to right.

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

* Let $\langle x_n \rangle$ be a loose B-adic sequence. We have

$$ \forall n \in \mathbb{Z}, \forall k \in \mathbb{N}, |B^k x_n - x_{n+k}| \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}, |B^k x_n - x_{n+k}| \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 |B^k x_n - x_{n+k}| \le B^{n+k}. $$

Thus, $\langle x_n \rangle \in \mathbb{O}^{\text{reg}}(\omega)$.

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

$$ \forall i \in \mathbb{Z}, \exists n \in \mathbb{Z}, \forall k \in \mathbb{N}, B^i |B^k x_n - x_{n+k}| \le B^{n+k}. $$

In particular, taking $i = 0$,

$$ \exists n \in \mathbb{Z}, \forall k \in \mathbb{N}, |B^k x_n - x_{n+k}| \le B^{n+k}. $$

We derive that

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

We can now choose an integer $j$ such that $B^j \ge 1 + B^{-n}|x_n|$:

$$ \exists n \in \mathbb{Z}, \exists j = [\log_B (1 + B^{-n} |x_n|)] \in \mathbb{Z}, \forall k \in \mathbb{N}, |x_{n+k}| \le B^{n+k+j}. $$

Thereby, according to Equation (16), $\langle x_n \rangle \in \mathbb{O}(\omega)$. $\square$

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 Quotient spaces

We saw in Section 2.1, that the Harthong-Reeb line $\mathcal{HR}_\omega$ is the quotient space $\mathbb{O}(\omega)/\mathbb{O}(\omega)$ (recall that we write $=_{\omega}$ for the corresponding equivalence relation). Alike, we define the quotient spaces $\mathcal{HR}_{\omega}^{\text{reg}} = \mathbb{O}^{\text{reg}}(\omega)/\mathbb{O}(\omega)$, $\mathcal{B}_{\omega} = \langle B \rangle /\mathbb{O}(\omega)$ and $\tilde{\mathcal{B}}_{\omega} = \langle \tilde{B} \rangle /\mathbb{O}(\omega)$. In this section, we aim at propagating the algebraic structure of $\mathcal{HR}_{\omega}$ to the three other quotient spaces. But before that, we have to rewrite the definition of the equivalence relation $=_{\omega}$ in a form compatible with B-adic numbers:

$$ \langle x_n \rangle =_{\omega} \langle y_n \rangle \overset{\text{def}}{\iff} \forall i \in \mathbb{Z}, \exists n \in \mathbb{Z}, \forall k \in \mathbb{N}, B^i |x_{n+k} - y_{n+k}| \le B^{n+k}. \quad (19) $$

Alike, we rewrite the order relation $\le_{\omega}$ (by abuse of notation, we confuse the order on the sequences and the order on the classes).

$$ \langle x_n \rangle \le_{\omega} \langle y_n \rangle \overset{\text{def}}{\iff} \forall i \in \mathbb{Z}, \exists n \in \mathbb{Z}, \forall k \in \mathbb{N}, B^i (x_{n+k} - y_{n+k}) \le B^{n+k}. \quad (20) $$

### 3.2.1 Canonical maps between the quotient spaces

The inclusion relations of Proposition 3 result in inclusion relations between the classes of the equivalence relation $=_{\omega}$ and the classes of its restrictions to the subsets $\langle B \rangle$, $\langle \tilde{B} \rangle$ and $\mathbb{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 5 (Inclusions).** The inclusions between the classes of the relation $=_{\omega}$ in the spaces $B_{\omega}$, $\tilde{B}_{\omega}$, $\mathcal{HR}_{\omega}^{reg}(\langle B^n \rangle)$ and $\mathcal{HR}_{\omega}$ are denoted $\text{inc}_1$, $\text{inc}_2$ and $\text{inc}_3$ respectively:

$$ \begin{array}{ccccccc} B_{\omega} & \xrightarrow{\text{inc}_1} & \tilde{B}_{\omega} & & \xrightarrow{\text{inc}_2} & \mathcal{HR}_{\omega}^{reg} & \xrightarrow{\text{inc}_3} & \mathcal{HR}_{\omega} \\ x & \mapsto & y = [\dot{x}] & & \mapsto & z = [\dot{y}] & & t = [\dot{z}] \end{array} $$

where, given a class a in the source space, $[\dot{a}]$ 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 $\text{inc}_3$ is simply the identity function.

**Proposition 4.** For any $x, y \in O(\omega)$, $(x =_{\omega} y \land x \in O^{reg}(\omega)) \implies y \in O^{reg}(\omega)$. In other words, putting $z = [x]$, for any class $z \in \mathcal{HR}_{\omega}^{reg}$, $\text{inc}_3(z) = z$.

*Proof.* Let $x = \langle x_n \rangle$, $y = \langle y_n \rangle$ be two sequences in $O(\omega)$ such that $x =_{\omega} y$ and $x$ is regular.

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}$,

$$ B^{i+2} |B^k x_n - x_{n+k}| \le B^{n+k}. \qquad (21) $$

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}$,

$$ B^{i+2} |x_{n+k} - y_{n+k}| \le B^{n+k} \quad \text{and,} \qquad (22) $$

$$ B^{i+2} |y_n - x_n| \le B^n. \qquad (23) $$

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

$$ B^2 B^i |B^k y_n - y_{n+k}| \le 3 B^{n+k}. $$

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

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.

**Proposition 5.** The three maps $\text{inc}_1$, $\text{inc}_2$ and $\text{inc}_3$ are one-to-one.

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.

**Proposition 6.** The two maps $\text{inc}_1$, $\text{inc}_2$ are onto. The map $\text{inc}_3$ is not onto.
*Proof.* Using reals, the proof is easy: given a regular sequence *a*, let $x = \lim_B a$. The real *x* has a tight representation $\langle x_n \rangle$ (which is also a loose representation). Then, *a* is equivalent to $\langle x_n \rangle$ since $\lim_B a = \lim_B \langle x_n \rangle$. So, $\text{inc}_1$ is onto. Alike, $\text{inc}_1$ is onto. Conversely, the integer sequence $\langle (-B)^n \rangle$ belongs to $O(B^n)$. But it has no limit. Thus, it is not equivalent to a regular sequence. Nevertheless, writing a proof without using reals is much longer. For instance, in order to prove that $\text{inc}_2$ is onto, we have to exhibit a process to build a loose B-adic sequence from a regular one, both sequences being equivalent, but without appealing to the limits.

• $\text{inc}_1$ is onto.

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

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

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

Thus, $b = \langle b_n \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{aligned}
B^i |a_n - b_n| &\le B^i \left| a_n - \frac{a_{n+2}}{B^2} \right| + \frac{1}{2} B^i \\
&\le B^{i-2} \left| B^2 a_n - a_{n+2} \right| + \frac{1}{2} B^i \\
&\le B^{i-2} (B^2 + 1) + \frac{1}{2} B^i \quad \text{for } a \in \langle \widetilde{B} \rangle \\
&\le B^i \left( \frac{3}{2} + \frac{1}{B^2} \right) \\
&\le 2B^i.
\end{aligned}
$$

Thus, for any $n \ge i+1$, $B^i |a_n - b_n| \le B^n$, that is $a = \langle B^n \rangle b$. Eventually, $b \in \text{inc}_1^{-1}(a)$ which proves that $\text{inc}_1$ is onto.

• The map $\text{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.
• inc$_{3}$ is not onto.

The proof is given in Appendix D. Actually, we prove a stronger result. We define a natural topology over O(ω) and we show that the set of regular sequences is not a dense subset of the space O(ω) for this topology whereas non regular sequences form a dense subset of O(ω). □

### 3.2.2 Field structures

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

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

**Lemma 3.** The subset inc$_{3}$(H$\mathcal{R}_{\omega}^{\text{reg}}$) of H$\mathcal{R}_{\omega}$ is stable for the operators $+ \text{ and } \times_{\omega}$.

*Proof.*

• Addition

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

Then, for $B \geq 2$,

$$|B^k(a_n + b_n) - (a_{n+k} + b_{n+k})| \leq 2 \frac{B^{n+k}}{B^{i+1}} \leq \frac{B^{n+k}}{B^i}. \quad (24)$$

• Multiplication

Recall that the product $\times_{\omega}$ in $\mathcal{H}\mathcal{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 = \langle a_n \rangle$ and $b = \langle b_n \rangle$ be two regular sequences. By abuse of notation, we write $a \times_{\omega} b$ for the sequence $\langle (a_n b_n) \div \omega \rangle$ (with $\omega = B^n$). In order to prove that inc$_{3}$(H$\mathcal{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

$$|B^k(a_n \times_{\omega} b_n) - (a_{n+k} \times_{\omega} b_{n+k})| \leq B^{n+k}/B^i$$

for sufficiently large $n$ and any $k \in \mathbb{N}$.
Firstly we split $|B^k(a_n \times_\omega b_n) - (a_{n+k} \times_\omega b_{n+k})|$ in three terms.

$$
\begin{align*}
|B^k(a_n \times_\omega b_n) - (a_{n+k} \times_\omega b_{n+k})| \\
&= |B^k((a_n b_n) \div B^n) - (a_{n+k} b_{n+k}) \div B^{n+k}| \\
&= \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| \quad \text{where } \varepsilon_1, \varepsilon_2 \in (-1, 1) \\
&\le \left| \frac{b_n}{B^n} (B^k a_n - a_{n+k}) + \frac{a_{n+k}}{B^{n+k}} (B^k b_n - b_{n+k}) \right| + 2B^k \\
&\le M_b |B^k a_n - a_{n+k}| + M_a |B^k b_n - b_{n+k}| + 2B^k,
\end{align*}
$$

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 $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} |B^k a_n - a_{n+k}| \le B^{n+k} \text{ and } B^{i_0+i} |B^k b_n - b_{n+k}| \le B^{n+k}.$$

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

We can now extend the operators $+$, $\times_\omega$ and the binary relation $\le_\omega$ to the sets $\mathcal{H}\mathcal{R}_\omega^{\text{reg}}$, $\langle B \rangle$ and $\langle B \rangle$ (denoting by $\text{inc}_1^{-1}$, resp. $\text{inc}_2^{-1}$, the inverse function of $\text{inc}_1$, resp. $\text{inc}_2$, and by $\text{inc}_3^{-1}$ the partial inverse function of $\text{inc}_3$ defined on the set $\text{inc}_3(\mathcal{H}\mathcal{R}_\omega^{\text{reg}})$).

**Definition 6 (Operations).**

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

$$
\begin{align*}
x + y &\stackrel{\text{def}}{=} \text{inc}_3^{-1}(\text{inc}_3(x) + \text{inc}_3(y)) \\
x \times_\omega y &\stackrel{\text{def}}{=} \text{inc}_3^{-1}(\text{inc}_3(x) \times_\omega \text{inc}_3(y)) \\
x \le_\omega y &\stackrel{\text{def}}{\Longleftrightarrow} \text{inc}_3(x) \le_\omega \text{inc}_3(y).
\end{align*}
$$

$$2. \forall x, y \in \tilde{\mathcal{B}}_{\omega},$$

$$
\begin{align*}
x + y &\stackrel{\text{def}}{=} \text{inc}_2^{-1}(\text{inc}_2(x) + \text{inc}_2(y)) \\
x \times_\omega y &\stackrel{\text{def}}{=} \text{inc}_2^{-1}(\text{inc}_2(x) \times_\omega \text{inc}_2(y)) \\
x \le_\omega y &\stackrel{\text{def}}{\Longleftrightarrow} \text{inc}_2(x) \le_\omega \text{inc}_2(y).
\end{align*}
$$

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

$$
\begin{align*}
x + y &\stackrel{\text{def}}{=} \text{inc}_1^{-1}(\text{inc}_1(x) + \text{inc}_1(y)) \\
x \times_\omega y &\stackrel{\text{def}}{=} \text{inc}_1^{-1}(\text{inc}_1(x) \times_\omega \text{inc}_1(y)) \\
x \le_\omega y &\stackrel{\text{def}}{\Longleftrightarrow} \text{inc}_1(x) \le_\omega \text{inc}_1(y).
\end{align*}
$$
By Definition 6, we directly have the following properties.

**Proposition 7.**

* The map $\text{inc}_1: (\mathcal{B}_\omega, +, \times_\omega, \le_\omega) \to (\widetilde{\mathcal{B}}_\omega, +, \times_\omega, \le_\omega)$ is an isomorphism.

* The map $\text{inc}_2: (\widetilde{\mathcal{B}}_\omega, +, \times_\omega, \le_\omega) \to (\mathcal{HR}_\omega^{\text{reg}}, +, \times_\omega, \le_\omega)$ is an isomorphism.

* The map $\text{inc}_3: (\mathcal{HR}_\omega^{\text{reg}}, +, \times_\omega, \le_\omega) \to (\mathcal{HR}_\omega, +, \times_\omega, \le_\omega)$ is a one-to-one morphism.

The three morphisms $\text{inc}_3$, $\text{inc}_2$ and $\text{inc}_1$ transfer the properties of $\mathcal{HR}_\omega$ to the other structures. Actually, $\mathcal{B}_\omega$, $\widetilde{\mathcal{B}}_\omega$ and $\mathcal{HR}_\omega^{\text{reg}}$ have a richer structure than $\mathcal{HR}_\omega$: their order relation is total and they are fields, not only rings.

**Proposition 8.** The order $\le_\omega$ is total in $\mathcal{B}_\omega$, $\widetilde{\mathcal{B}}_\omega$ and $\mathcal{HR}_\omega^{\text{reg}}$.

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

$$u_n \ge n \quad \text{and} \quad B^i|x_{u_n}| > B^{u_n}. \qquad (25)$$

A consequence of the existence of such a pair $(i, \langle u_n \rangle)$ is that for large enough index $n$, the sign of $x_n$ is not null and constant. Indeed, from Eq. (25), we get $x_{u_n} \ne 0$ for any $n$ and from Formula (18), we derive that for large enough $n$, $B^i|B^k x_{u_n} - x_{u_n+k}| \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|B^k x_{u_n}| \le B^{u_n+k}$, that is $B^i|x_{u_n}| \le B^{u_n}$ which contradicts Eq. (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$, Eq. (4), that either $[x] \ge 0$ or $[x] \le 0$ and, because $[x] \ne 0$, $[x] > 0$ or $[x] < 0$. $\square$

**Proposition 9.** $\mathcal{B}_\omega$, $\widetilde{\mathcal{B}}_\omega$ and $\mathcal{HR}_\omega^{\text{reg}}$ are ordered commutative fields.

*Proof.* The proof is split in three parts.

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

* Secondly, we show that $\text{inc}_3(\mathcal{HR}_\omega^{\text{reg}})$ is a field. At this aim, we define a map $\text{inv}: \text{inc}_3(\mathcal{HR}_\omega^{\text{reg}}) \setminus [\langle 0 \rangle] \to \text{inc}_3(\mathcal{HR}_\omega^{\text{reg}})$ by putting

$$\text{inv}([\langle x_n \rangle]) = \left[ \left\langle \left\lfloor \frac{B^{2n}}{x_n} \right\rfloor \right\rangle \right],$$
where the representative $\langle x_n \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 \text{inc}_3(\mathcal{HR}_\omega^{\text{reg}}) \setminus [\langle 0 \rangle]$. Let us prove that $\text{inv}$ is well-defined, that is, $\text{inv}(x) \in \text{inc}_3(\mathcal{HR}_\omega^{\text{reg}})$ and $\text{inv}(x)$ does not depend on the choice of the representative of $x$.

Let $\langle x_n \rangle \in x$. We claim that

$$ \exists i_0 \in \mathbb{Z}, \exists n_0 \in \mathbb{Z}, \forall n \ge n_0, |x_n| \ge B^{n-i_0}. \quad (26) $$

Indeed, by hypothesis, $\langle 0 \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

$$ B^{i_1} |x_{n+k_n}| > B^{n+k_n}. \quad (27) $$

Moreover, thanks to the regularity of $\langle x_n \rangle$ and Equation (18), there exists $n_0 \in \mathbb{Z}$ such that, for any $n \ge n_0$,

$$ B^{i_1+1} |B^{k_n} x_n - x_{n+k_n}| \le B^{n+k_n}. $$

Then, splitting the absolute value,

$$ B^{i_1+1} (|x_{n+k_n}| - B^{k_n} |x_n|) \le B^{n+k_n}. $$

Using Equation (27),

$$ BB^{n+k_n} - B^{i_1+1+k_n} |x_n| \le B^{n+k_n}. $$

We derive that

$$ B^{n-i_1} \frac{B-1}{B} < |x_n|. $$

Since $B \ge 2$, we have $(B-1)/B \ge 1/B$. Hence, choosing $i_0 = i_1+1$, the claim is established.

Let $\langle x_n \rangle \in x$ with $x_n \neq 0$ for any $n \in \mathbb{Z}$. We now prove that the sequence $\langle B^{2n}/x_n \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{aligned} B^i \left| B^k \frac{B^{2n}}{x_n} - \frac{B^{2(n+k)}}{x_{n+k}} \right| &= B^{i+2n+k} \frac{|x_{n+k} - B^k x_n|}{|x_n||x_{n+k}|} \\ &\le B^{i+2n+k} \frac{|B^k x_n - x_{n+k}|}{B^{n-i_0} B^{n+k-i_0}} \\ &\le B^{i+2q_0} |B^k x_n - x_{n+k}|. \end{aligned} $$

Since $x$ is regular, for sufficiently large $n$ and any $k \in \mathbb{N}$, we have $B^{i+2q_0} |B^k x_n - x_{n+k}| \le B^{k+n}$. Thereby, we are done: the sequence $\langle B^{2n}/x_n \rangle$ is regular.
- We prove that the function inv is independent of the choice of the representative. Let $\langle x_n \rangle$ and $\langle y_n \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 $\langle x_n \rangle$ and $\langle y_n \rangle$.

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

$$ 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{|x_{n+k} - y_{n+k}|}{|x_{n+k}y_{n+k}|} \\ \le B^{i+i_0^x+i_0^y} |x_{n+k} - y_{n+k}|. $$

Because $\langle x_n \rangle = \omega \langle y_n \rangle$, $B^{i+i_0^x+i_0^y} |x_{n+k} - y_{n+k}| \le B^{n+k}$ for sufficiently large $n$ and any $k \in \mathbb{N}$, which proves that $\langle B^{2n}/x_n \rangle$ and $\langle B^{2n}/y_n \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) = [\omega]$.

Given $\langle x_n \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 $\mathcal{O}(\omega)$ which is the sequence $\omega = \langle B^n \rangle$ itself:

$$ \left| \frac{x_n \times \left| \frac{B^{2n}}{x_n} \right|}{B^n} \right| = \varepsilon_1 + \frac{x_n}{B^n} \varepsilon_2 + B^n \\ \text{where } \varepsilon_1 \in (-1, 0] \text{ and } \varepsilon_2 \in (-\frac{1}{2}, \frac{1}{2}] \\ = \varepsilon + B^n \quad \text{where } |\varepsilon| \le 1 + \sup_n \frac{|x_n|}{B^n}. $$

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

* Finally, thanks to the isomorphisms $\mathrm{inc}_3$ (whose codomain is restricted to $\mathrm{inc}_3(\mathcal{HR}^\mathrm{reg}_\omega)$), $\mathrm{inc}_2$ and $\mathrm{inc}_1$, we derive that $\mathcal{HR}^\mathrm{reg}_\omega$, $\mathcal{B}_\omega$ and $\tilde{\mathcal{B}}_\omega$ are also ordered commutative fields. $\square$

The following proposition shows that the operations $+_B$ and $\cdot_B$ defined in [Mén05] (see Section 2.2) directly perform the operations of both fields $(\mathcal{B}_\omega, +, \times_\omega)$ and $(\tilde{\mathcal{B}}_\omega, +, \times_\omega)$, avoiding the cost of the computation of the function $\mathrm{inc}_2^{-1}$ (see the proof of Proposition 6).

**Proposition 10.** Let $x, y \in \mathcal{B}_\omega$, or $x, y \in \tilde{\mathcal{B}}_\omega$. Then,

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

We split the proof of Proposition 10 by stating Lemma 4 (addition of integer sequences) and Lemma 5 (multiplication of integer sequences). The last part of the proof is devoted to formally switching to quotient spaces.
**Lemma 4.** Let $x$ and $y$ be two regular sequences. Then,

$$x+B y =_{\omega} x+y.$$

*Proof.* Let $x = \langle x_n \rangle$ and $y = \langle y_n \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}| \le B^{n+k}.$$

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

Thereby, we have:

$$\begin{aligned} 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| \\ &\le \frac{1}{2} B^i + B^{-r} \left( B^i |B^r x_{n+k} - x_{n+k+r}| + B^i |B^r y_{n+k} - y_{n+k+r}| \right). \end{aligned}$$

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 |B^r x_{n+k} - x_{n+k+r}| \le B^r$ and $B^i |B^r x_{n+k} - x_{n+k+r}| \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. $\square$

**Lemma 5.** Let $x = \langle x_n \rangle$ and $y = \langle y_n \rangle$ be two loose B-adic sequences. Then,

$$x \cdot_B y =_{\omega} x \times_{\omega} y.$$

*Proof.* Let $x = \langle x_n \rangle$ and $y = \langle y_n \rangle$ be two loose B-adic sequences. We set $z = x \cdot_B y$ and $z' = x \times_{\omega} y$ (where $\omega = \langle B^n \rangle$). If either $x$ or $y$ is zero, the result is obvious (taking the sequence $\langle 0 \rangle_{n \in \mathbb{Z}}$ as a representative of zero). So, until the end of the proof, we assume that $x$ and $y$ are not zero. Then, msd($x$) and msd($y$) are finite.

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

$$z_n = \frac{a + x_{p_x} y_{p_y}}{B^{p_x + p_y - n}} + \varepsilon,$$

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

It follows that

$$\begin{aligned} |z'_{n} - z_{n}| &= \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^{n} y_{p_{y}}}{B^{n + p_{x} + p_{y}}} \right| + 2 + B^{n - p_{x} - p_{y}}. \end{aligned}$$
Provided we enforce $n - p_x - p_y \le 0$, that is, $n \ge \text{msd}(x) + \text{msd}(y) - 2v$, we get

$$|z'_n - z_n| \le \left| \frac{B^{p_x} x_n B^{p_y} y_n - B^n x_{p_x} B^n y_{p_y}}{B^{n+p_x+p_y}} \right| + 3. \quad (28)$$

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

$$\frac{B^{p_x} x_n B^{p_y} y_n - B^n x_{p_x} B^n y_{p_y}}{B^{n+p_x+p_y}} = \frac{x_n}{B^n} \times \frac{B^{p_y} y_n - B^n y_{p_y}}{B^{p_y}} + \frac{y_{p_y}}{B^{p_y}} \times \frac{B^{p_x} x_n - B^n x_{p_x}}{B^{p_x}}. \quad (29)$$

Since $x$ and $y$ belong to $\mathcal{HR}_\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$,

$$\frac{|B^{p_y} y_n - B^n y_{p_y}|}{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}}, \quad (30)$$

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

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

$$\frac{|B^{p_x} x_n - B^n x_{p_x}|}{B^{p_x}} \le \frac{B^n B^{c_y}}{B^{i_0}}, \quad (31)$$

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

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

$$B^i |z'_n - z_n| \le MB^{i-i_0} B^n + 3B^i,$$

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

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 |z'_n - z_n| \le B^n$ for any $i \in \mathbb{Z}$ and sufficiently large $n \in \mathbb{Z}$. Thereby, we have proved that $\langle z_n \rangle =_\omega \langle z'_n \rangle$. $\square$

**Proof of Proposition 10.** We develop the case $x, y \in \tilde{B}_\omega$ for the addition. The case $x, y \in B_\omega$ and the proof for the multiplication are similar.

So, let $x, y \in \tilde{B}_\omega$. Then, $\dot{x}$ and $\dot{y}$ are regular sequences. Therefore, we derive from Lemma 4 that $\dot{x} +_B \dot{y} =_\omega \dot{x} + \dot{y}$. We set $\phi = \text{inc}_3 \circ \text{inc}_2$. Observe that, from Proposition 14, we get $\dot{x} +_B \dot{y} \in \langle \tilde{B} \rangle$. Hence, $\phi([\dot{x} +_B \dot{y}])$ is well defined and belongs to $\mathcal{HR}_\omega$. We have

$$\begin{align*}
\dot{x} +_B \dot{y} =_\omega \dot{x} + \dot{y} &\implies \dot{x} +_B \dot{y} \in [\dot{x} + \dot{y}] \text{ where } [\dot{x} + \dot{y}] \in \mathcal{HR}_\omega \\
&\implies \dot{x} +_B \dot{y} \in [\dot{x}] + [\dot{y}] \text{ by Equation (2)} \\
&\implies \dot{x} +_B \dot{y} \in \phi(x) + \phi(y) \text{ by Definition 5} \\
&\implies \dot{x} +_B \dot{y} \in \phi(x + y) \text{ by Proposition 7} \\
&\implies \phi([\dot{x} +_B \dot{y}]) = \phi(x + y) \text{ where } [\dot{x} +_B \dot{y}] \in \tilde{B}_\omega \\
&\implies [\dot{x} +_B \dot{y}] = x + y \text{ by Proposition 5,}
\end{align*}$$

which is the stated result. $\square$
### 3.3 Back to real numbers

Until now, we have extended the structure of the Harthong-Reeb line to the (free, loose, tight) representations of real numbers. To end this study, it remains to verify that the obtained fields are isomorphic to the real numbers field.

Firstly, let us show that the equivalence relation $\cong_{\omega}$ inherited from the construction of $\mathcal{H}\mathcal{R}_{\omega}$ actually corresponds to the identification of representations of the same real number.

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

On the one hand, the Harthong-Reeb line $\mathcal{H}\mathcal{R}_{\omega}$ was defined in [CWF+12] as the quotient set $O(\omega)/o(\omega)$. On the other hand, it is natural to identify (free, loose, tight) representations of real numbers that represents the same real number. Actually, these two equivalence relations are identical for the free representations and thus for the other kinds of representation.

**Proposition 11.** Let $\langle x_n \rangle$, $\langle y_n \rangle$ be two free representations of some real numbers $x$ and $y$. Then $\langle x_n \rangle =_{\omega} \langle y_n \rangle$ if and only if $x = y$.

*Proof.* Let $\langle x_n \rangle$, $\langle y_n \rangle \in O^{\text{reg}}(\omega)$. Put $x = \lim \langle x_n/B^n \rangle$ and $y = \lim \langle y_n/B^n \rangle$ (recall that by definition of $O^{\text{reg}}(\omega)$, $\langle x_n/B^n \rangle$ and $\langle y_n/B^n \rangle$ are Cauchy sequences). The proof is straightforward:

$$ 
\begin{align*}
\langle x_n \rangle =_{\omega} \langle y_n \rangle &\iff \forall i \in \mathbb{Z}, \exists n_0 \in \mathbb{Z}, n \ge n_0 \implies B^i |x_n - y_n| \le B^n \\
&\iff \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 \frac{1}{B^i} \\
&\iff \lim \left\langle \frac{x_n}{B^n} \right\rangle = \lim \left\langle \frac{y_n}{B^n} \right\rangle \\
&\iff x = y.
\end{align*}
$$

□

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

$$ 
\lim_B: \quad \mathcal{H}\mathcal{R}_{\omega}^{\text{reg}} \text{ (resp. } \tilde{\mathcal{B}}_{\omega}, \mathcal{B}_{\omega}) \quad \rightarrow \quad \mathbb{R} \\
x = [\langle x_n \rangle] \quad \longmapsto \quad \lim \left\langle \frac{x_n}{B^n} \right\rangle
$$

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

<footnote n="4">⁴This fact is stated without proof in [Cho10].</footnote>
### 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{HR}_\omega^{\text{reg}}$, $\tilde{\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{HR}_\omega^{\text{reg}}, +, \times_\omega, \le_\omega)$, $(\tilde{\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: \mathcal{B}_\omega \to \mathbb{R}$.

**Theorem 3.** The function $\lim_B: (\mathcal{B}_\omega, +, \times_\omega, \le_\omega) \to (\mathbb{R}, +, \times, \le)$ is a order-preserving isomorphism.

*Proof.*

* $\lim_B$ is onto: for any $x \in \mathbb{R}$, $[xB^n]$ is a preimage of $x$.

* $\lim_B$ is one-to-one. This is just the if part of Proposition 11.

* $\lim_B$ is a morphism. We have seen in Proposition 10, that the operations $+$ and $\times_\omega$ of the field $\mathcal{B}_\omega$ are identical to the operations $+_B$ and $\cdot_B$ described in [Mén05]. Hence, the results obtained in [Mén05] and recalled in Section 2.2, show that, for any classes $x$, $y$ in $\mathcal{B}_\omega$, we have $\lim_B(x+y) = \lim_B(x) + \lim_B(y)$ and $\lim_B(x \times_\omega y) = \lim_B(x) \times \lim_B(y)$.

* $\lim_B$ is increasing. Let $x, y \in \mathcal{B}_\omega$. Let $\langle x_n \rangle \in x$ and $\langle y_n \rangle \in y$. Then,

$$ 
\begin{align*}
x \leq_{\omega} y &\implies \forall i \in \mathbb{Z}, \exists n \in \mathbb{Z}, \forall k \in \mathbb{N}, B^i (x_{n+k} - y_{n+k}) \leq B^{n+k} \\
&\implies \forall i \in \mathbb{Z}, \exists n \in \mathbb{Z}, \forall k \in \mathbb{N}, \frac{x_{n+k}}{B^{n+k}} - \frac{y_{n+k}}{B^{n+k}} \leq \frac{1}{B^i} \\
&\implies \forall i \in \mathbb{Z}, \lim_{B} (x) - \lim_{B} (y) \leq \frac{1}{B^i} \\
&\implies \lim_{B} (x) - \lim_{B} (y) \leq 0 \\
&\implies \lim_{B} (x) \leq \lim_{B} (y).
\end{align*}
$$

□

## 4 Conclusion

In this article we built an isomorphism between the B-adic sequences and the real field. This new isomorphism is in line with a rather long series of efforts in nonstandard and constructive mathematics to represent real numbers with sequences of integers. The advantage of the representations proposed in this article over a model like the Harthong-Reeb line is that, at each scale provided by the choice of the base $B$, the term of the B-adic sequence is almost the best one in terms of precision.

In the near future, we wish to make the link between our model and the one developed by [Cia03] for the base 2 and founded on the positional numeral system.
Moreover, now that the theoretical foundations are laid properly, we plan to extend the already-existing Coq formalization of the Harthong-Reeb line, to integrate B-adic sequences as a new implementation for elements of the Harthong-Reeb line and to formally check that all properties of the Harthong-Reeb line are verified by this implementation. In parallel, we want to take advantage of the determinism and the accuracy of the B-adic sequences over the too much unconstrained elements of the Harthong-Reeb line to resume the study of the digitalization of the affine transforms, especially rigid motions. One of the goals of such a study will be to understand how the periodic structures highlighted by the works on quasi-affine transforms evolve when the resolution under which the Euclidean world is seen in the digital space grows.

## A Proof of Theorem 2

Theorem 2 binds the integer sequences $\langle x_n \rangle$ satisfying the weak bound property (13) for some real $x$ with a predicat on integer sequences, Equation (15). It makes it possible to construct the field $\mathbb{R}$ from loose B-adic sequences. The proof of Theorem 2 is similar to the proof of Theorem 1.

**Lemma 6.** Let $(x_n)$ be the loose representation of a real number. Then,

$$ \forall n \in \mathbb{Z}, k \in \mathbb{Z}, |B^k x_n - x_{n+k}| \le B^k + 1. \qquad (15) $$

*Proof.* Assuming $(x_n)$ is a loose representation of a real number $x$, the weak bound property (13) is satisfied. Hence, for any $n \in \mathbb{Z}$ and any $k \in \mathbb{Z}$,

$$ x_n - 1 \le xB^n \le x_n + 1, $$

and

$$ x_{n+k} - 1 \le xB^{n+k} \le x_{n+k} + 1. $$

These two equations lead to

$$ (B^k x_n - x_{n+k}) - (B^k + 1) \le 0 \le (B^k x_n - x_{n+k}) + (B^k + 1), $$

which can be rewritten as

$$ |B^k x_n - x_{n+k}| \le B^k + 1. $$

□

**Proposition 12.** Let $(x_n)$ be an integer sequence satisfying Equation (15). Then, the sequence $(x_n/B^n)$ is a Cauchy sequence.
*Proof.* Let $m \in \mathbb{N}$. Let us prove that, for sufficiently large $n$ and any $k \ge 0$, $|\frac{x_n}{B^n} - \frac{x_{n+k}}{B^{n+k}}| \le \frac{1}{B^m}$.

$$ 
\begin{aligned}
\left| \frac{x_n}{B^n} - \frac{x_{n+k}}{B^{n+k}} \right| &\le \frac{1}{B^{n+k}} \left| B^k x_n - x_{n+k} \right| \\
&\le \frac{1}{B^{n+k}} \times (B^k + 1) \quad \text{thanks to (15)} \\
&\le \frac{1}{B^{n+k}} \times B^{k+1} \\
&\le \frac{1}{B^{n-1}}.
\end{aligned}
$$

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

<figure><img src="image_2.png" /></figure>

**Lemma 7.** Let $(x_n)$ be an integer sequence satisfying Equation (15). Then, $(x_n)$ satisfies the weak bound property

$$ |x - \frac{x_m}{B^m}| \le \frac{1}{B^m}, $$

where $x$ is the limit of the Cauchy sequence $\langle x_n/B^n \rangle$.

*Proof.* Let $x$ be the limit of the Cauchy sequence $\langle x_n/B^n \rangle$ and $m \in \mathbb{Z}$. For any positive real $a$, there exists an integer $k_a \ge 1$ such that, for any $k \ge k_a$, $|x - \frac{x_{m+k}}{B^{m+k}}| \le \frac{a}{B^m}$. Then,

$$ 
\begin{aligned}
|x - \frac{x_m}{B^m}| &\le \left| x - \frac{x_{m+k}}{B^{m+k}} \right| + \frac{1}{B^{m+k}} \left| x_{m+k} - x_m B^k \right| \\
&\le \frac{a}{B^m} + \frac{B^k + 1}{B^{m+k}} \quad \text{from (15)} \\
&\le \frac{1 + a + \frac{1}{B^k}}{B^m}.
\end{aligned}
\quad (32) $$

Since Inequality (32) is satisfied for any $a > 0$ and any $k \ge k_a$, we derive that

$$ |x - \frac{x_m}{B^m}| \le \frac{1}{B^m}. $$

<figure><img src="image_3.png" /></figure>

# B Equivalence of the definitions of regular sequences

We compare the definition of a regular sequence given in [Cho10] with the definition given in this article (Definition 4). Firstly, let us recall Chollet’s definition of regular sequences:

$$ \forall p \in \mathbb{N} \setminus \{0\}, \exists n_0 \in \mathbb{N}, \forall \ell \ge n_0, \forall m \ge n_0, \left| \frac{x_\ell}{\omega_\ell} - \frac{x_m}{\omega_m} \right| \le \frac{1}{p}. \quad (33) $$

We give below a stronger formulation of our definition of regular sequences.
**Lemma 8.** An integer sequence $\langle x_n \rangle$ is regular (in the sense of Definition 4) if and only if

$$ \forall i \in \mathbb{Z}, \exists n_0 \in \mathbb{Z}, \forall n \ge n_0, \forall k \in \mathbb{N}, B^i |B^k x_n - x_{n+k}| \le B^{n+k}. \quad (34) $$

*Proof.* The “if” part is obvious (taking $n = n_0$ in Equation (34)). Conversely, let $i \in \mathbb{Z}$. From Equation (17), we get an integer $n_0$ such that, for any $k \in \mathbb{Z}$,

$$ B^{i+1} |B^k x_{n_0} - x_{n_0+k}| \le B^{n_0+k}. $$

Thus, for any $n \ge n_0$ and any $k \ge 0$, we have

$$ \begin{aligned} B^{i+1} |B^{n-n_0} x_{n_0} - x_n| &\le B^n \\ B^{i+1} |B^{n+k-n_0} x_{n_0} - x_{n+k}| &\le B^{n+k}. \end{aligned} $$

By combining the two equations above in order to eliminate $x_{n_0}$, we get

$$ B^{i+1} |B^k x_n - x_{n+k}| \le 2B^{n+k}. $$

Since we assume $B \ge 2$, the result holds. $\square$

We can now establish the equivalence of both definitions of regular sequences.

**Proposition 13.** Let $B$ be an integer greater than or equal to 2. Then, the following statements are equivalent:

$$ (1) \quad \forall p \in \mathbb{N} \setminus \{0\}, \exists n_0 \in \mathbb{N}, \forall \ell \ge n_0, \forall m \ge n_0, \left| \frac{x_\ell}{B^\ell} - \frac{x_m}{B^m} \right| \le \frac{1}{p}. $$

$$ (2) \quad \forall i \in \mathbb{Z}, \exists n_0 \in \mathbb{Z}, \forall n \ge n_0, \forall k \in \mathbb{N}, B^i |B^k x_n - x_{n+k}| \le B^{n+k}. $$

*Proof.*

$$ \bullet \quad (1) \implies (2) $$

Let $i \in \mathbb{Z}$. Taking $p = B^i$, $\ell = n$ and $m = n + k$, we directly obtain the second statement from the first one.

$$ \bullet \quad (2) \implies (1) $$

Let $p \ge 1$ and take $i$ such that $B^i \ge p$. From (2), there exists $n_0 \in \mathbb{Z}$ such that, for any $n \ge n_0$ and any $k \ge 0$,

$$ \left| \frac{x_n}{B^n} - \frac{x_{n+k}}{B^{n+k}} \right| \le \frac{1}{B^i} \le \frac{1}{p}. $$

In particular, taking $n = \min(\ell, m)$ and $k = |\ell - m|$, we get the first statement. $\square$
### C Building a loose B-adic sequence from a regular sequence

Let $x = \langle x_n \rangle$ be a regular sequence. Making the change $i \leftarrow i + 1$, and dividing by $B^n$ in Formula (18), we get

$$ \forall i \in \mathbb{Z}, \exists n_0 \in \mathbb{Z}, \forall n \ge n_0, \forall k \in \mathbb{N}, \left| B^k \frac{x_n}{B^{n-i}} - \frac{x_{n+k}}{B^{n-i}} \right| \le B^{k-1}. \quad (35) $$

Observing that, for any integers $i, j, m, n$,

$$ \left| B^{j-i} \frac{x_n}{B^{n-i}} - \frac{x_m}{B^{m-j}} \right| = B^{(j-i)-(m-n)} \left| B^{m-n} \frac{x_n}{B^{n-i}} - \frac{x_m}{B^{n-i}} \right|, $$

we derive from Eq. (35), that, for any $i \in \mathbb{Z}$, there exists $n_0 \in \mathbb{Z}$ such that for any $m \ge n \ge n_0$ and any $j \in \mathbb{Z}$,

$$ \left| B^{j-i} \frac{x_n}{B^{n-i}} - \frac{x_m}{B^{m-j}} \right| \le B^{j-i-1}. $$

Consequently,

$$ \left| B^{j-i} \left\lfloor \frac{x_n}{B^{n-i}} \right\rfloor - \left\lfloor \frac{x_m}{B^{m-j}} \right\rfloor \right| \le B^{j-i-1} + \frac{1}{2} B^{j-i} + \frac{1}{2}. $$

Finally, since $B \ge 2$ and the left hand side of the previous inequality is an integer, we get

$$ \forall i \in \mathbb{Z}, \exists n_0 \in \mathbb{Z}, \forall n, m \ge n_0, \forall j \in \mathbb{Z}, \left| B^{j-i} \left\lfloor \frac{x_n}{B^{n-i}} \right\rfloor - \left\lfloor \frac{x_m}{B^{m-j}} \right\rfloor \right| \le B^{j-i}. $$

Then, for any $i \in \mathbb{Z}$, we define $\gamma(i)$ as the smallest integer $n \ge i$ such that

$$ \forall j \in \mathbb{Z}, \forall m \ge n, \left| B^{j-i} \left\lfloor \frac{x_n}{B^{n-i}} \right\rfloor - \left\lfloor \frac{x_m}{B^{m-j}} \right\rfloor \right| \le B^{j-i}. \quad (36) $$

This mapping $\gamma$ is monotonically increasing. Indeed, let $i < k$. Let us show that Formula (36) is satisfied putting $n = \gamma(k)$, which, by definition of $\gamma$, implies that $\gamma(k) \ge \gamma(i)$.

We start by splitting the inequality of Formula (36) in two parts:

$$ \left| B^{j-i} \left\lfloor \frac{x_{\gamma(k)}}{B^{\gamma(k)-i}} \right\rfloor - \left\lfloor \frac{x_m}{B^{m-j}} \right\rfloor \right| \le B^{j-k} \left| B^{k-i} \left\lfloor \frac{x_{\gamma(k)}}{B^{\gamma(k)-i}} \right\rfloor - \left\lfloor \frac{x_{\gamma(k)}}{B^{\gamma(k)-k}} \right\rfloor \right| + \\ \left| B^{j-k} \left\lfloor \frac{x_{\gamma(k)}}{B^{\gamma(k)-k}} \right\rfloor - \left\lfloor \frac{x_m}{B^{m-j}} \right\rfloor \right|. \quad (37) $$

Observe that the second part of the right hand side of the previous inequality is upper-bounded by $B^{j-k}$ by definition of $\gamma$. We now look at the first part of the expression putting $\frac{x_{\gamma(k)}}{B^{\gamma(k)-i}} = \left\lfloor \frac{x_{\gamma(k)}}{B^{\gamma(k)-i}} \right\rfloor + \epsilon_1$ and $\frac{x_{\gamma(k)}}{B^{\gamma(k)-k}} = \left\lfloor \frac{x_{\gamma(k)}}{B^{\gamma(k)-k}} \right\rfloor + \epsilon_2$ where $|\epsilon_1|, |\epsilon_2| \le \frac{1}{2}$. Then,

$$ \left| B^{k-i} \left\lfloor \frac{x_{\gamma(k)}}{B^{\gamma(k)-i}} \right\rfloor - \left\lfloor \frac{x_{\gamma(k)}}{B^{\gamma(k)-k}} \right\rfloor \right| \le B^{k-i} \epsilon_1 + \epsilon_2 \le \frac{1}{2} B^{k-i} + \frac{1}{2}. \quad (38) $$

Now, we have to examine two cases.
1. If $B > 2$ or $k - i > 1$, using Eq (38) and the definition of $\gamma(k)$, we derive from Eq (37) that

$$ \begin{aligned} \left| B^{j-i} \left[ \frac{x_{\gamma(k)}}{B^{\gamma(k)-i}} \right] - \left[ \frac{x_m}{B^{m-j}} \right] \right| & \le B^{j-k} \left( \frac{1}{2} B^{k-i} + \frac{1}{2} \right) + B^{j-k} \\ & \le \left( \frac{1}{2} \frac{3}{B^{k-i}} + \frac{1}{2} \right) B^{j-i}. \end{aligned} $$

Because at this point we assume $B > 2$ or $k - i > 1$, we get $\frac{3}{B^{k-i}} \le 1$. Hence, $|B^{j-i} \left[ \frac{x_{\gamma(k)}}{B^{\gamma(k)-i}} \right] - \left[ \frac{x_m}{B^{m-j}} \right]| \le B^{j-i}$ and we are done.

2. If $B = 2$ and $k = i + 1$, Eq. 38 can be rewritten as

$$ \left| B^{k-i} \left[ \frac{x_{\gamma(k)}}{B^{\gamma(k)-i}} \right] - \left[ \frac{x_{\gamma(k)}}{B^{\gamma(k)-k}} \right] \right| \le \frac{3}{2}. $$

Since the left hand side of the above equation is an integer, we derive that

$$ \left| B^{k-i} \left[ \frac{x_{\gamma(k)}}{B^{\gamma(k)-i}} \right] - \left[ \frac{x_{\gamma(k)}}{B^{\gamma(k)-k}} \right] \right| \le 1. $$

Then, from Eq (37), we get

$$ \begin{aligned} \left| B^{j-i} \left[ \frac{x_{\gamma(k)}}{B^{\gamma(k)-i}} \right] - \left[ \frac{x_m}{B^{m-j}} \right] \right| & \le B^{j-k} \times 1 + B^{j-k} \\ & \le 2B^{j-k} \\ & \le B^{j-i}, \end{aligned} $$

for $B = 2$ and $j - i = j - k + 1$.

So, we have proved that $\gamma$ is increasing. Eventually, we define the sequence $y = \langle y_i \rangle_{i \in \mathbb{Z}}$ by

$$ y_i = \left\lfloor \frac{x_{\gamma(i)}}{B^{\gamma(i)-i}} \right\rfloor, \qquad (39) $$

for any $i \in \mathbb{Z}$.

From the definition of $\gamma$ and because it is increasing, we derive that

$$ \forall i \in \mathbb{Z}, \forall j \ge i, |B^{j-i} y_i - y_j| \le B^{j-i}. $$

Hence, the sequence $\langle y_i \rangle_{i \in \mathbb{Z}}$ is a loose B-adic sequence. It remains to prove that $\langle y_i \rangle$ is equivalent to $\langle x_i \rangle$. That is,

$$ \forall i \in \mathbb{Z}, \exists n \in \mathbb{Z}, \forall m \ge n, B^i |x_m - y_m| \le B^m. $$

We have

$$ \begin{aligned} B^i |x_m - y_m| & \le B^i \left| x_m - \frac{x_{\gamma(m)}}{B^{\gamma(m)-m}} \right| + \frac{1}{2} B^i & \qquad (40) \\ & \le B^{m-\gamma(m)} \times B^i \left| B^{\gamma(m)-m} x_m - x_{\gamma(m)} \right| + \frac{1}{2} B^i. \end{aligned} $$
Since the sequence $x$ is regular, for large enough $m$,

$$B^i |B^{\gamma(m)-m} x_m - x_{\gamma(m)}| \le B^{\gamma(m)}.$$

Thus, Eq. 40 can be rewritten as

$$B^i |x_m - y_m| \le B^m + \frac{1}{2},$$

which is equivalent to

$$B^i |x_m - y_m| \le B^m,$$

because the left hand side of the inequality is an integer. We conclude that the sequences $x$ and $y$ are equivalent. In other words, we obtain $\text{inc}_2(y) = x$ which establishes that $\text{inc}_2$ is onto.

# D The Harthong-Reeb line is fat

We define a topology over the sequences bounded by $\omega = \langle B^n \rangle_{n \in \mathbb{Z}}$ up to a constant factor and we show that

1. there exists a sequence in $O(\omega)$ that is far (for this topology) from any regular sequence. In other words, the regular sequences are not dense in $O(\omega)$;

2. any regular sequence is close to non regular sequences. In other words, non regular sequences are dense in $O(\omega)$.

Let $a = \langle a_n \rangle \in O(\omega)$ and $i \in \mathbb{Z}$. We set

$$\mathcal{B}(a, i) = \{ \langle b_n \rangle \mid \exists n_0 \in \mathbb{Z}, \forall n \ge n_0, B^i |a_n - b_n| < B^n \}.$$

Then, a sequence $b = \langle b_n \rangle$ is equivalent to a sequence $a = \langle a_n \rangle$, that is $b =_\omega a$, if and only if $b \in \mathcal{B}(a, i)$ for any $i \in \mathbb{Z}$. We consider the topology $\mathcal{T}$ over $O(\omega)$ generated by the set of all the balls $\mathcal{B}(a, i)$.

In $O(\omega)$, we choose a prototypical undesirable sequence, $o = \langle (-B)^n \rangle$, and we show that there is no regular sequence in its neighborhood.

**Lemma 9.** *The ball $\mathcal{B}(o, 1)$ does not contain any regular sequence.*

*Proof.* By contradiction, we consider a regular sequence $b = \langle b_n \rangle$ in the ball $\mathcal{B}(o, 1)$.

On the one hand, since $b$ is regular, there exists an integer $n_1$ such that for any $n \ge n_1$ (taking $i = 1$ and $k = 1$ in Eq. (18)),

$$B |Bb_n - b_{n+1}| \le B^{n+1}. \qquad (41)$$

On the other hand, since $b \in \mathcal{B}(o, 1)$, there exists $n_2 \ge n_1$ such that for any $n \ge n_2$,

$$B |(-1)^n B^n - b_n| \le B^n, \qquad (42)$$
and also,

$$B|b_{n+1} - (-1)^{n+1}B^{n+1}| < B^{n+1}. \quad (43)$$

Then, adding Equations (41), (42), multiplied by $B$, and (43), we get

$$B|(-1)^n - (-1)^{n+1}| \le 3.$$

That is $B \le 3/2$ which contradicts the assumption on $B$. $\square$

Let us now prove that non regular sequences are dense in $O(\omega)$.

**Lemma 10.** Let $a = \langle a_n \rangle$ be a regular sequence and $r$ be a positive integer. Then, the ball $B(a, r)$ contains a non regular sequence.

*Proof.* We will prove that $b = a + \frac{1}{2}B^{-r}o$ belongs to $B(a, r)$ and is non regular.

1. The sequence $b$ belongs to $B(a, r)$. Indeed,

$$B^r |a_n - b_n| = B^r \left| a_n - \left( a_n + \frac{1}{2} B^{-r} (-B)^n \right) \right| = \frac{1}{2} B^n < B^n.$$

2. In order to prove that $b$ is non regular, we show the negation of Equation (18), that is:

$$\exists i \in \mathbb{Z}, \forall n_0 \in \mathbb{Z}, \exists n \ge n_0, \exists k \in \mathbb{N}, B^i |B^k b_n - b_{n+k}| > B^{n+k}.$$

Let $i = \lceil \log_B 2 \rceil + r$ and $n_0 \in \mathbb{Z}$. Since $a$ is regular, we can use Equation (18) to get an integer $n \ge n_0$ such that $B^i |Ba_n - a_{n+1}| \le B^{n+1}$. Then, we have

$$\begin{aligned} B^i |Bb_n - b_{n+1}| & \ge B^i \left| B \left( a_n + \frac{1}{2} B^{-r} (-B)^n \right) - \left( a_{n+1} + \frac{1}{2} B^{-r} (-B)^{n+1} \right) \right| \\ & \ge B^i \times B^{-r} B^{n+1} - B^i \times |Ba_n - a_{n+1}| \\ & \ge 2B^{n+1} - B^{n+1} \text{ by definition of } i \text{ and } n \\ & > B^{n+1}. \end{aligned}$$

We are done (using $k = 1$ in the negation of Equation (18)). $\square$
E Division

**Theorem 4.** Let $x \in \mathbb{R}$, $y \in \mathbb{R} \setminus \{0\}$ with tight representations $\langle x_n \rangle$ and $\langle y_n \rangle$. Define $\langle z_n \rangle$ by:

$$z_n = \begin{cases} \operatorname{sign}(x_{p_x}) \times \operatorname{sign}(y_{p_y}) & \text{if } n \le \operatorname{msd}(\langle x_n \rangle) - \operatorname{msd}(\langle y_n \rangle) - 1 \\ \operatorname{sign}(x_{p_x}) \times \operatorname{sign}(y_{p_y}) \times \left\lfloor \frac{|x_{p_x}|+1}{|y_{p_y}|-1} B^{p_y-p_x-n} \right\rfloor & \text{otherwise,} \end{cases}$$
where

$$p_x = \mathrm{msd}(\langle x_n \rangle) + \left( n + \mathrm{msd}(\langle y_n \rangle) - \mathrm{msd}(\langle x_n \rangle) \right) \quad \text{and,} \quad (44)$$

$$p_y = \mathrm{msd}(\langle y_n \rangle) + \left( n + \mathrm{msd}(\langle y_n \rangle) - \mathrm{msd}(\langle x_n \rangle) \right) + k,$$

$$\text{with } k = \begin{cases} 2 & \text{if } B > 2 \\ 3 & \text{if } B = 2. \end{cases}$$

Then $\langle z_n \rangle$ is well defined and satisfies the bound property for $x/y$:

$$z_n - 1 < \frac{x}{y} B^n < z_n + 1.$$

*Proof.* When $x = 0$, the definition of $\langle z_n \rangle$ gives $z_n = 0$ for any $n \in \mathbb{Z}$. Thus, the result holds in this case. We now assume $x \ne 0$ and we set $m_x = \mathrm{msd}(\langle x_n \rangle)$, $m_y = \mathrm{msd}(\langle y_n \rangle)$.

The bound property of $|x|$, resp. $|y|$, for order $m_x - 1$, resp. $m_y$, and the definitions of $m_x$, $m_y$ give

$$|x_{m_x-1}| - 1 < B^{m_x-1}|x| < |x_{m_x-1}| + 1 \le 2, \text{ and} \\ 1 \le |y_{m_y}| - 1 < B^{m_y}|y| < |y_{m_y}| + 1.$$

So, we have

$$1 \le B^{m_x - m_y - 1} \frac{|x|}{|y|} < \frac{|x_{m_x - 1}| + 1}{|y_{m_y}| - 1} \le 2.$$

We derive that, for any $n \le m_x - m_y - 1$, the integer $\operatorname{sign}(x) \times \operatorname{sign}(y)$ satisfies the bound property for $x/y$ at order $n$:

$$\operatorname{sign}(x) \times \operatorname{sign}(y) - 1 < B^n \frac{x}{y} < \operatorname{sign}(x) \times \operatorname{sign}(y) + 1.$$

If $n \ge m_x - m_y$, then $p_x \ge m_x$ and $p_y \ge m_y + 1$. Thus, according to Eq. (6),

$$\begin{aligned} 1 &\le B^{p_x - m_x} \le |x_{p_x}| < 2B^{1+p_x - m_x}, \text{ and} \\ 2 &\le B^{p_y - m_y} \le |y_{p_y}| < 2B^{1+p_y - m_y}. \end{aligned} \quad (45)$$

So,

$$|x_{p_x}| \le 2B^{1+p_x-m_x} \le \frac{2}{B^{k-1}} B^{p_y-m_y} < B^{p_y-m_y} \le |y_{p_y}|.$$
Hence,

$$|x_{p_x}| < |y_{p_y}|.$$

Moreover, from Equation (45), we derive that $|y_{p_y}| - 1 \neq 0$. Then, using the bound property of $x$, resp. $y$, of order $p_x$, resp. $p_y$, we obtain:

$$\frac{|x_{p_x}| - 1}{|y_{p_y}| + 1} < B^{p_x - p_y} \left| \frac{x}{y} \right| < \frac{|x_{p_x}| + 1}{|y_{p_y}| - 1}. \qquad (46)$$

Let us put $\alpha = \frac{|x_{p_x}|-1}{|y_{p_y}|+1} B^{p_y-p_x+n}$ and $\beta = \frac{|x_{p_x}|+1}{|y_{p_y}|-1} B^{p_y-p_x+n}$. Then, Eq. (46) can be rewritten as

$$\alpha < B^n \left| \frac{x}{y} \right| < \beta.$$

Besides, we have

$$\begin{aligned} 0 < \beta - \alpha &= 2 \frac{|x_{p_x}| + |y_{p_y}|}{|y_{p_y}|^2 - 1} B^{p_y - p_x + n} \\ &< 2 \frac{|x_{p_x}| + |y_{p_y}|}{|y_{p_y}|^2 - |x_{p_x}|^2} B^{p_y - p_x + n} \\ &\le 2 \frac{1}{|y_{p_y}| - |x_{p_x}|} B^{p_y - p_x + n} \\ &< \frac{2 B^{p_y - p_x + n}}{B^{p_y - m_y} - 2B^{1+p_x-m_x}} \\ &\le \frac{2}{B^k - 2B}. \end{aligned}$$

Hence, in both cases $B = 2$ and $k = 3$ or $B > 2$ and $k = 2$, we get $0 < \beta - \alpha < 1$. It follows that $\lfloor \beta \rfloor$ verifies the bound property for $|x|/|y|$ and $\text{sign}(x_{p_x}) \times \text{sign}(y_{p_y}) \times \lfloor \beta \rfloor$ verifies the bound property for $x/y$. $\square$

# F Binary operations on loose B-adic sequences

The goal of this section of the appendix is to study whether the relaxation of the bound property into a weak bound property has consequences on some propositions proved in [Mén95] or in [Mén05] which are of prime importance for our work. For each proposition, we use a red font when a modification was done compare to the initial version in [Mén95] or in [Mén05].

Firstly, let us recall the definitions of the bound property and of the weak bound property.

**Definition 7 (Bound property).** Let $x \in \mathbb{R}$. A sequence $\langle x_n \rangle$ of integers is a tight representation of $x$ if, for any $n$, the bound property of $x$ by $x_n$ for order $n$ is satisfied:

$$\frac{(x_n - 1)}{B^n} < x < \frac{(x_n + 1)}{B^n}. \qquad (5)$$
**Definition 8 (Weak bound property).** Let $x \in \mathbb{R}$. A sequence $\langle x_n \rangle$ of integers is a loose representation of $x$ if, for any $n$, the weak bound property of $x$ by $x_n$ for order $n$ is satisfied:

$$ \frac{(x_n - 1)}{B^n} \le x \le \frac{(x_n + 1)}{B^n}. \qquad (13) $$

A sequence $\langle x_n \rangle$ of integers is a loose representation of $x \in \mathbb{R}$ without being a tight representation of $x$ only if, for some $n \in \mathbb{Z}$, $x_n = B^n x \pm 1$, which implies that $B^n x$ is an integer. Taking this scenario into account requires to check each algorithm and property in the work of Ménissier-Morain. First of all, we check the addition algorithm. The result is that no change is needed.

**Proposition 14 (addition).** Let $\langle x_n \rangle$ and $\langle y_n \rangle$ be loose representations of $x, y \in \mathbb{R}$. Then, the real $x + y$ admits for loose representation the sequence $\langle z_n \rangle_{n \in \mathbb{N}}$ where

$$ z_n = \left\lfloor \frac{x_{n+w} + y_{n+w}}{B^w} \right\rfloor \quad \text{with } w = \begin{cases} 1 & \text{if } B \ge 4, \\ 2 & \text{if } B = 2 \text{ or } 3. \end{cases} $$

*Proof.* We show that the sequence $\langle z_n \rangle$ satisfies the weak bound property for any $n$.

By definition of $\lfloor \cdot \rfloor$, we have

$$ \frac{x_{n+w} + y_{n+w}}{B^w} - \frac{1}{2} < z_n \le \frac{x_{n+w} + y_{n+w}}{B^w} + \frac{1}{2}. $$

Thanks to the weak bound property satisfied by $\langle x_n \rangle$ and $\langle y_n \rangle$, we derive

$$ \frac{B^{n+w}(x+y)-2}{B^w} - \frac{1}{2} < z_n \le \frac{B^{n+w}(x+y)+2}{B^w} + \frac{1}{2}. $$

Equivalently,

$$ B^n(x + y) - \frac{2}{B^w} - \frac{1}{2} < z_n \le B^n(x + y) + \frac{2}{B^w} + \frac{1}{2}. $$

Since $B^w \ge 4$, we get

$$ B^n(x + y) - 1 < z_n \le B^n(x + y) + 1. $$

We conclude that $\langle z_n \rangle$ satisfies the weak bound property. $\square$

<figure><img src="image_4.png" /></figure>

Before dealing with multiplication, we need to extend the definition of the *most significant digit* to loose representations. Unfortunately, doing so, we break some properties of the msd function described by [Mén95, Property 7]$^5$. Indeed, it is no more true that $|\text{msd}(\langle x_n \rangle)| + \lfloor \log_B |x| \rfloor \le 1$ and it is no more true that, for any $n \ge \text{msd}(\langle x_n \rangle)$, $|x_n|/B^{n-\text{msd}(\langle x_n \rangle)} \in [1, 2B]$ as shown by the following counterexamples.

<footnote>$^5$In [Mén05], the statement of the algorithm contains a typo but the proof is exactly the same as in [Mén95].</footnote>
Let $B=2$ and $x=1/2$. Then, $B^nx = B^{n-1}$. So, putting $x_n = [B^{n-1}-1]$ if $n \le 2$ and $x_n = B^{n-1}+1$ otherwise, we obtain a loose representation of $x$. In this case, $\text{msd}(x_n) = 3$ whereas $\log_B(x) = -1$. Hence, $\text{msd}(x_n) + \log_B(x) > 1$. Moreover, $x_3 = 5$. Hence, for $n = \text{msd}(x_n) = 3$, $|x_n|/B^{n-\text{msd}(x_n)} > 2B$. Now, we can change the sequence $\langle x_n \rangle$ by setting $x_n = [B^{n-1}] + 1$ if $n \le 1$ and $x_n = B^{n-1} - 1$ otherwise. We still have a loose representation of $x$ where $\text{msd}(x_n) = 1$ and $|x_n|/B^{n-\text{msd}(x_n)} < 1$ for any $n > \text{msd}(x_n)$.

In view of these counterexamples, we have to adapt the results of Ménissier-Morain to encompass the loose representations of real numbers.

**Proposition 15.** [Mén95, Property 7], [Mén05, Property 15] Let $x \in \mathbb{R} \setminus \{0\}$ and $\langle x_n \rangle$ be a loose representation of $x$. Then,

1. $\text{msd}(\langle x_n \rangle)$ exists;

2. $\text{msd}(\langle x_n \rangle) = -[\log_B|x|] + \epsilon$ where $\epsilon \in \{0, 1, 2\}$;

3. for any $n \ge \text{msd}(\langle x_n \rangle)$,

$$B^{n-\text{msd}(\langle x_n \rangle)} - \zeta_1 \le |x_n| \le \zeta_2 + (2B)B^{n-\text{msd}(\langle x_n \rangle)}, \quad (47)$$

where

$\zeta_1 = 1 \text{ if } \log_B|x| \in \mathbb{Z} \wedge |x_n| = |x|B^n - 1 \text{ and } \zeta_1 = 0 \text{ otherwise; }$

$\zeta_2 = 1 \text{ if } |x| = 2B^{1-\text{msd}(\langle x_n \rangle)} \wedge |x_n| = |x|B^n + 1 \text{ and } \zeta_2 = 0 \text{ otherwise.}$

*Proof.* Let $x \in \mathbb{R} \setminus \{0\}$ and $m = \lfloor \log_B |x| \rfloor$. Let $\langle x_n \rangle$ be a loose representation of $x$.

By definition of $\lfloor \cdot \rfloor$,

$$B^m \le |x| < B^{m+1}. \quad (48)$$

Besides, $x_{-m+k}$ satisfies the weak bound property for order $-m+k$ of $x$:

$$x_{-m+k} - 1 \le B^{-m+k}x \le x_{-m+k} + 1.$$

Thus, we also have

$$|x_{-m+k}| - 1 \le B^{-m+k}|x| \le |x_{-m+k}| + 1. \quad (49)$$

Observe that in the previous equation, an equality can occur only if $B^{-m+k}x$ is an integer.

From Eq. (48) and (49), we derive that

$$|x_{-m+k}| - 1 < B^{k+1} \quad (50)$$

and

$$\begin{cases} B^k \le |x_{-m+k}| + 1 & \text{if } |x| = B^m \text{ and } k \ge 0 \\ B^k < |x_{-m+k}| + 1 & \text{otherwise.} \end{cases} \quad (51)$$
In particular, for any $k < 0$, $|x_{-m+k}| < B^{k+1} + 1 \le 2$. That is, $|x_{-m+k}| \in \{0, 1\}$. Therefore, $\text{msd} \ge -m$ (to lighten the notation, we write $\text{msd}$ instead of $\text{msd}(\langle x_n \rangle)$).

In the other hand, if $k \ge 0$, Equations (50) and (51) concern integers. Thus, they can be rewritten as

$$|x_{-m+k}| \le B^{k+1},$$

and

$$B^k - \zeta_1 \le |x_{-m+k}|, \qquad (52)$$

where $\zeta_1 = 1$ if $|x| = B^m \wedge |x_{-m+k}| = |x|B^{-m+k} - 1$ and $\zeta_1 = 0$ otherwise. Then, because $B^k - 1 \ge 2$ for any $B \ge 2$ and $k \ge 2$, one has $\text{msd} \le -m + 2$, that is, $\text{msd} = -m + \varepsilon$ where $\varepsilon \in \{0, 1, 2\}$.

By definition of the most significant digit, we have $|x_{\text{msd}-1}| \le 1$. Thus, the right part of Equation (49), taking $-m + k = \text{msd} - 1$, gives $|x| \le 2B \times B^{-\text{msd}}$. Then, the left part of Equation (49), where $-m + k = n \ge \text{msd}$, yields

$$\begin{cases} |x_n| \le 1 + 2B \times B^{n-\text{msd}} & \text{if } |x| = 2B \times B^{-\text{msd}}, \\ |x_n| < 1 + 2B \times B^{n-\text{msd}} & \text{otherwise.} \end{cases}$$

Since the last equation only involves integers, it is equivalent to

$$|x_n| \le \zeta_2 + 2B \times B^{n-\text{msd}},$$

where $\zeta_2 = 1$ if $|x| = 2B^{1-\text{msd}} \wedge |x_n| = B^n + 1$ and $\zeta_2 = 0$ otherwise.

Moreover, for any $n \ge \text{msd}$, Equation (52) can be rewritten as

$$B^{n-\text{msd}+(\text{msd}+m)} - \zeta_1 \le |x_n|.$$

Thereby, for $\text{msd} + m \ge 0$,

$$B^{n-\text{msd}} - \zeta_1 \le |x_n|.$$

□

We saw that the extension of the most significant digit to loose representations slightly change its properties. Surprisingly, these changes do not propagate to the multiplication algorithm [Mén95, Algorithm 4 and Theorem 14], [Mén05, Algorithm 4 and Theorem 16]).

**Proposition 16** (multiplication). Let $\langle x_n \rangle$ and $\langle y_n \rangle$ be the loose representations of $x, y \in \mathbb{R} \setminus \{0\}$. Then, the real $x \times y$ admits for loose representation the sequence
$\langle z_n \rangle_{n \in \mathbb{N}}$ where

$$
\begin{align*}
z_n &= \operatorname{sign}(x_{p_x}) \times \operatorname{sign}(y_{p_y}) \times \left\lfloor \frac{1 + |x_{p_x} y_{p_y}|}{B^{p_x + p_y - n}} \right\rfloor \\
\text{with } p_x &= \max(n - \operatorname{msd}(\langle y_n \rangle) + v, \left\lfloor \frac{n+w}{2} \right\rfloor) \\
\text{and } p_y &= \max(n - \operatorname{msd}(\langle x_n \rangle) + v, \left\lfloor \frac{n+w}{2} \right\rfloor) \\
\text{and } (v, w) &= \begin{cases} (3, 2) & \text{if } B \ge 4, \\ (3, 3) & \text{if } B = 3, \\ (4, 3) & \text{if } B = 2. \end{cases}
\end{align*}
$$

Proof. Since, given a sequence $\langle z_n \rangle$ that is a loose representation of the real $z$,
the sequences $\langle |z_n| \rangle$ and $\langle -|z_n| \rangle$ are loose representations of $|z|$ and $-|z|$,
we can assume without loss of generality that $x > 0$ and $y > 0$.

Firstly, observe that

$$
p_x + p_y - n \geq w - 1. \tag{53}
$$

and, if $p_x \ge \mathrm{msd}(\langle x_n \rangle)$ or $p_y \ge \mathrm{msd}(\langle y_n \rangle)$,

$$
p_x + p_y - n \geq v. \tag{54}
$$

Indeed, by definition of $p_x$ and $p_y$,

$$
\bullet p_x + p_y - n \geq 2 \times \lfloor (n+w)/2 \rfloor - n \geq w - 1;
$$

$$
\bullet \text{ if, for instance, } p_x \ge \text{msd}(\langle x_n \rangle), \text{ then } p_x + p_y - n \ge \text{msd}(\langle x_n \rangle) + p_y - n \ge v.
$$

We separate the rest of the proof in two cases, depending on the value of $\zeta_2$
in Equation (47).

1. Let us assume that $x_n < xB^n + 1$ and $y_n < yB^n + 1$. Then, $\zeta_2 = 0$ in Equation (47) for both terms $x_n$ and $y_n$. In this case, we follow the proof in [Mén05].

From the weak bound property for $x$ and $y$ at respective orders $p_x$ and $p_y$, we derive that

$$
\frac{x_{p_x} - 1}{B^{p_x}} \times \frac{y_{p_y} - 1}{B^{p_y}} \le x \times y \le \frac{x_{p_x} + 1}{B^{p_x}} \times \frac{x_{p_y} + 1}{B^{p_y}}.
$$

Notice that in the case where $x$, resp. $y$, is the $B$-adic number $B^{-p_x}$, resp. $B^{-p_y}$, it is possible to have $x_{p_x} = 0$, resp. $y_{p_y} = 0$. Nevertheless, the reader can check that the above left inequality remains true.

The previous inequalities can be equivalently stated as follows:

$$
\frac{1 + x_{p_x} y_{p_y} - (x_{p_x} + y_{p_y})}{B^{p_x + p_y - n}} \le B^n x \times y \le \frac{1 + x_{p_x} y_{p_y} + (x_{p_x} + y_{p_y})}{B^{p_x + p_y - n}},
$$
or

$$ \left| B^n x \times y - \frac{1 + x_{p_x} y_{p_y}}{B^{p_x + p_y - n}} \right| \le \frac{x_{p_x} + y_{p_y}}{B^{p_x + p_y - n}}. $$

Therefore, from the definition of $\lfloor \cdot \rfloor$, we get

$$ \left| B^n x \times y - \left| \frac{1 + x_{p_x} y_{p_y}}{B^{p_x + p_y - n}} \right| \right| \le \frac{1}{2} + \frac{x_{p_x} + y_{p_y}}{B^{p_x + p_y - n}}. $$

It remains to show that

$$ \frac{x_{p_x} + y_{p_y}}{B^{p_x + p_y - n}} \le \frac{1}{2}. \qquad (55) $$

We distinguish three sub-cases

(a) If $p_x < \text{msd}(\langle x_n \rangle)$ and $p_y < \text{msd}(\langle y_n \rangle)$, then, by definition of the most significant digit (Eq. 53) and by definition of $w$,

$$ \frac{x_{p_x} + y_{p_y}}{B^{p_x + p_y - n}} \le \frac{2}{B^{w-1}} \le \frac{1}{2}. $$

(b) If, for instance, $p_x \ge \text{msd}(\langle x_n \rangle)$ and $p_y < \text{msd}(\langle y_n \rangle)$, then, according to Equation (47) (taking into account the hypothesis $\zeta_2 = 0$) and according to the definition of the most significant digit,

$$ \frac{x_{p_x} + y_{p_y}}{B^{p_x + p_y - n}} \le \frac{2B^{p_x - \text{msd}(\langle x_n \rangle) + 1} + 1}{B^{p_x + p_y - n}} \le \frac{2B^{n - \text{msd}(\langle x_n \rangle) + 1}}{B^{p_y}} + \frac{1}{B^{p_x + p_y - n}}. $$

Hence, by definition of $p_y$ and by Equation (54),

$$ \frac{x_{p_x} + y_{p_y}}{B^{p_x + p_y - n}} \le \frac{2B + 1}{B^v} \le \frac{1}{2}. $$

The last inequality comes from the definition of $v$.

(c) If both $p_x \ge \text{msd}(\langle x_n \rangle)$ and $p_y \ge \text{msd}(\langle y_n \rangle)$,

$$ \frac{x_{p_x} + y_{p_y}}{B^{p_x + p_y - n}} \le \frac{2B \times B^{n - \text{msd}(\langle x_n \rangle)}}{B^{p_y}} + \frac{2B \times B^{n - \text{msd}(\langle y_n \rangle)}}{B^{p_x}}. $$

Thus, by definition of $p_x$, $p_y$ and Equation (54),

$$ \frac{x_{p_x} + y_{p_y}}{B^{p_x + p_y - n}} \le \frac{4B}{B^v} \le \frac{1}{2}. $$

We have shown that, in the three sub-cases, Equation (55) is satisfied so we are done for the first case.

2. We now assume that $x_n \ge xB^n + 1$ or $y_n \ge yB^n + 1$: for instance, $x_n \ge xB^n + 1$ (the other case is perfectly similar). Then the weak bound property for $y$ at order $p_y$ gives

$$ \frac{x_{p_x} - 1}{B^{p_x}} \times \frac{y_{p_y} - 1}{B^{p_y}} \le x \times y \le \frac{x_{p_x} - 1}{B^{p_x}} \times \frac{y_{p_y} + 1}{B^{p_y}}, $$
which can be rewritten as

$$ \frac{(x_{p_x} + y_{p_y})}{B^{p_x+p_y-n}} \le B^n x \times y - \frac{1 + x_{p_x} y_{p_y}}{B^{p_x+p_y-n}} \le \frac{x_{p_x} - y_{p_y} - 2}{B^{p_x+p_y-n}}. \quad (56) $$

We observe that, in Equation (56), the difference between both bounds is less than or equal to 1/2:

$$ \frac{2x_{p_x} - 2}{B^{p_x+p_y-n}} \le \frac{4B^{p_x-\text{msd}(\langle x_n \rangle)+1}}{B^{p_x+p_y-n}} \le 4B^{1-v} \le 1/2. $$

Thereby,

$$ A \le B^n x \times y - \left| \frac{1 + x_{p_x} y_{p_y}}{B^{p_x + p_y - n}} \right| \le B, $$

where $B - A \le 1$. We derive that

$$ \left| B^n x \times y - \left| \frac{1 + x_{p_x} y_{p_y}}{B^{p_x + p_y - n}} \right| \right| \le 1. $$

which establishes the result in the second case. □

## References

[BLM16] Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Formalization of real analysis: a survey of proof assistants and libraries. *Mathematical Structures in Computer Science*, 26(7):1196–1233, 2016.

[CDG06] Alberto Ciaffaglione and Pietro Di Gianantonio. A certified, corecursive implementation of exact real numbers. *Theor. Comput. Sci.*, 351(1):39–51, 2006.

[Cho10] A. Chollet. *Non classical formalisms for the computing treatment of the topology and the discrete geometry*. PhD thesis, Université de La Rochelle, 2010.

[Cia03] Alberto Ciaffaglione. *Certified reasoning on real numbers and objects in co-inductive type theory*. Theses, Institut National Polytechnique de Lorraine, May 2003.

[CWF+09] A. Chollet, G. Wallet, L. Fuchs, G. Largeteau-Skapin, and E. Andres. Insight in discrete geometry and computational content of a discrete model of the continuum. *Pattern Recognition*, 42(10):2220–2228, 2009.

[CWF+12] A. Chollet, G. Wallet, L. Fuchs, E. Andres, and G. Largeteau-Skapin. Foundational aspects of multiscale digitization. *Theor. Comput. Sci.*, 466:2–19, 2012.
[DCT09] M-A. Da Col and P. Tellier. Quasi-linear transformations and discrete tilings. *Theoretical Computer Science*, 410:2126–2134, May 2009.

[DR89] F. Diener and G. Reeb. *Analyse non standard*. Hermann, 1989.

[Har89] J. Harthong. Une théorie du continu. In *Les mathématiques non standard*, pages 307–329, 1989.

[Lau83] D. Laugwitz. $\Omega$-calculus as a generalization of field extension: An alternative approach to nonstandard analysis. In *Nonstandard Analysis - Recent developments*, LNM, pages 120–133. Springer, 1983.

[Maz19] L. Mazo. Multi-scale arithmetization of linear transformations. *Journal of Mathematical Imaging and Vision*, 61(4):432–442, May 2019.

[MCF15] N. Magaud, A. Chollet, and L. Fuchs. Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective. *Annals of Mathematics and Artificial Intelligence*, 74(3-4):309–332, 2015.

[Mén95] V. Ménissier-Morain. *Arithmétique exacte: conception, algorith-mique et performances d'une implémentation informatique en pré-cision arbitraire*. PhD thesis, Université Paris 7, Nov 1995.

[Mén05] Valérie Ménissier-Morain. Arbitrary precision real arithmetic: design and algorithms. *J. Log. Algebr. Program.*, 64(1):13–39, 2005.

[SL58] C. Schmieden and D. Laugwitz. Eine erweiterung der infinitesimalrechnung. *Mathematische Zeitschrift*, 69:1–39, 1958.