@ARTICLE{SURREALN.MIZ,
  AUTHOR = {P\k{a}k, Karol},
  TITLE = {Surreal Dyadic and Real Numbers: A Formal Construction},
  SECTION1 = {Mappings between Integers and Surreal Integers},
  SECTION2 = {Dyadic Numbers},
  SECTION3 = {Mappings between Dyadic Numbers and Surreal Dyadic Numbers},
  SECTION4 = {Mappings between Real Numbers and Surreal Real Numbers},
  SECTION5 = {*Real Surreal Numbers},
  SECTION6 = {Surreal Ordinals}
  DAY = {10},
  MONTH = {April},
  YEAR = {2025},
  ADDRESS1 = {Faculty of Computer Science\\University of Bia{\l}ystok\\ Konstantego Cio{\l}kowskiego 1M, 15-245 Bia{\l}ystok\\Poland},
  SUMMARY = {
The concept of surreal numbers, as postulated by John Conway, represents a
complex and multifaceted structure that encompasses a multitude of familiar
number systems, including the real numbers, as integral components.
In this study, we undertake the construction of the real numbers, commencing
with the integers and dyadic rationals as preliminary steps.
We proceed to contrast the resulting set of real numbers derived from our
construction with the axiomatically defined set of real numbers
based on Conway's axiom. Our findings reveal that both approaches
culminate in the same set.
},
INTRODUCTION = {
In his seminal book, John Conway introduces an axiomatic definition of real numbers.
Conway call a number $x$ {\it real} number if $-n < x < n$ for some integer $n$ and
\begin{equation}\label{ConwayReal}
x \approx \{x - 1, x-\frac{1}{2}, x-\frac{1}{3},\ldots | x + 1, x+\frac{1}{2}, x+\frac{1}{3},\ldots\}.
\end{equation}
This property is self-contained within the context of the surreal number system, which is expressed using only the explicitly outlined conditions of the system itself, and it does not rely on the standard real numbers used in mathematical analysis.
Note that all these real numbers appear in the Day $\omega$ which contains other numbers like infinitesimals and $\omega$
 and the days formed previously contain only dyadic rationals surreal numbers.
 Conway indicates these dyadic numbers as exemplars of the {\it reals},
 yet does not formally establish a connection between the concepts of the reals or
 dyadic numbers and their counterparts in mathematical analysis.
 The map that converts dyadic rationals into their surreal counterparts, called as {\it Dali} function by T{\o}ndering \cite{Tondering}, has been analyzed in \cite{Tondering, ROUGHAN2019, NietoParityofdyadic}.
\par
In our formalization, we introduce the {\it Dali} function in two steps.
First, we define the recursive integer function $\mathrm{s}_{\mathbb{Z}}$, as follows: the base step is given as $\mathrm{s}_{\mathbb{Z}}(0)=0$, while $\mathrm{s}_{\mathbb{Z}}(n+1)=\{\mathrm{s}_{\mathbb{Z}}(n)\mid\;\} $,
$\mathrm{s}_{\mathbb{Z}}(-n-1)=\{\;\mid\mathrm{s}_{\mathbb{Z}}(-n)\}$ for all $n > 0$ (see~Def1).
Then, $\mathrm{s}_{\mathbb{Z}}$ is used to define the base step of $\mathrm{s}_{\mathbb{D}}$ as follows:
 $\mathrm{s}_{\mathbb{D}}(d)=\mathrm{s}_{\mathbb{Z}}(d)$ for all $d \in \mathbb{Z}$ and
$\{\mathrm{s}_\mathbb{D}(\frac{j}{2^p})\mid \mathrm{s}_\mathbb{D}(\frac{j+1}{2^p})\}$
if $d=\frac{2j+1}{2^{p+1}}$ for some $j\in \mathbb{Z}$, $p \in \mathbb{N}$ (see~Def5).
We prove that the values of the function $\mathrm{s}_{\mathbb{D}}$ have \texttt{uniq-surreal}, i.e.
$\mathrm{s}_{\mathbb{D}}(d) = \textrm{Unique}_{\bf No} \mathrm{s}_{\mathbb{D}}(d)$ for every dyadic rational $d$,
or more formally, $\mathrm{s}_{\mathbb{D}}(d)$ is equal to our construction of the $\approx$ equivalence
class representative of $\mathrm{s}_{\mathbb{D}}(d)$. This property is important for the next stage of our construction.
\par
We subsequently employ the function $\mathrm{s}_{\mathbb{S}}$ to establish a homeomorphism between the real numbers and their Conway representations.
The fundamental premise of this construction is that the sequences of dyadic rational numbers
$\{\frac{\lceil r\cdot2^n-1 \rceil}{2^n}\}_{n>0}$ and
 $\{\frac{\lfloor r\cdot2^n+1 \rfloor}{2^n}\}_{n>0}$ represent successive approximations of a given real number $r$. Moreover, these sequences are non-decreasing and non-increasing, respectively, and the relation
 the inequality $\frac{\lceil r\cdot 2^n-1 \rceil}{2^n} < r < \frac{\lfloor r\cdot 2^n +1 \rfloor}{2^n}$ is satisfied
 for all values of $n > 0$.
This allows us to associate any real number $r$ with the Conway number $\mathrm{s}_\mathbb{R}(r)$ (see~Def6, Def7), which is equal to:
\begin{equation}
\textrm{Unique}_{\bf No} \left\{ \left\{\mathrm{s}_\mathbb{D}\left(\frac{\lceil r\cdot2^n-1 \rceil}{2^n}\right)\mid n \in\mathbb{N}\right\}\mid
\left\{\mathrm{s}_\mathbb{D}\left(\frac{\lfloor r\cdot 2^n+1 \rfloor}{2^n}\right)\mid n \in\mathbb{N}\right\}\right\}
\end{equation}
Note that we apply additionally $\textrm{Unique}_{\bf No}$ to obtain $\mathrm{s}_\mathbb{R}(d) = \mathrm{s}_\mathbb{D}(r)$ for each dyadic number $d$.
\par
We prove that that the function $\mathrm{s}_\mathbb{R}$ preserves the identity elements for both addition (see~Th47) and multiplication (see~Th48). Furthermore, it is shown that it respects the operations of addition (see~Th55) and multiplication (see~Th57).
We conduct also a comparison between the set of values of function $\mathrm{s}_\mathbb{R}$,
and the set of {\it real} numbers that fulfils the Conway property.
We prove that $\mathrm{s}_\mathbb{R}(r)$ satisfies Conway's property for all $r\in\mathbb{R}$
and that for each {\it real} number $x$, there exists a real number $r$ such that $x \approx \mathrm{s}_\mathbb{R}(r)$.
}
}

@article{ROUGHAN2019,
title = {Practically surreal: Surreal arithmetic in Julia},
journal = {SoftwareX},
volume = {9},
pages = {293-298},
year = {2019},
issn = {2352-7110},
doi = {https://doi.org/10.1016/j.softx.2019.03.005},
author = {Matthew Roughan}
}


@ARTICLE{NietoParityofdyadic,
  AUTHOR = {J. A. Nieto, J. A. and
Escalante-Javalera, J. A. and
Somera-Patr\'on, C. A. and
Villasenor-Gonz\'alez, E. J.},
  TITLE =        {Parity of dyadic rationals and surreal numbers},
  JOURNAL =      {Far East Journal of Mathematical Sciences (FJMS)},
  YEAR =         {2024},
  number =       {2},
  pages =        {155 167},
  month =        {May},
}