Foundational aspects of multiscale digitization

In this article, we describe the theoretical foundations of the @W-arithmetization. This method provides a multi-scale discretization of a continuous function that is a solution of a differential equation. This discretization process is based on the Harthong-Reeb line HR"@w. The Harthong-Reeb line is a linear space that is both discrete and continuous. This strange line HR"@w stems from a nonstandard point of view on arithmetic based, in this paper, on the concept of @W-numbers introduced by Laugwitz and Schmieden. After a full description of this nonstandard background and of the first properties of HR@w, we introduce the @W-arithmetization and we apply it to some significant examples. An important point is that the constructive properties of our approach leads to algorithms which can be exactly translated into functional computer programs without uncontrolled numerical error. Afterwards, we investigate to what extent HR"@w fits Bridges's axioms of the constructive continuum. Finally, we give an overview of a formalization of the Harthong-Reeb line with the Coq proof assistant.