@ARTICLE{SURREALC.MIZ,
  AUTHOR = {P\k{a}k, Karol},
  TITLE = {Conway's Normal Form in the {M}izar System},
  SECTION1 = {Commensurability in Archimedean Classes of Surreal Numbers},
  SECTION2 = {Conway's $\omega$-map},
  SECTION3 = {Unique Characterization of Surreal Number},
  SECTION4 = {$\alpha$-term - An Essential Component of the Conway Normal Form},
  SECTION5 = {Conway's Generalization of Partial Sums},
  SECTION6 = {Conway Names for Surreal Numbers},
  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 = {
This paper presents a formal definition of the Conway normal form,
 a structured representation uniquely suited to characterising 
 surreal numbers by expressing them as sums within a hierarchically ordered group.
 To this end, we formalise the first sections of 
 the chapter {\it The Structure of the General Surreal Number} 
 in Conway's book. In particular, we define
omega maps and prove the existence and uniqueness of the Conway name for surreal numbers.
},
INTRODUCTION = {
Conway surreal numbers can be constructed according to two independent principles: the game-theoretic approach (\cite{Conway:2001,holzf}) and the tree-theoretic approach (\cite{Ehrlich2011,Ehrlich2012}).
In this formalization we use our construction of the
$\approx$ equivalence class representative of a surreal number $x$, called {\it uniq-surreal}, denoted as $\textrm{Uniq}_{\bf No} x$ (\cite{SURREALO.ABS}),
to unify these two approaches in order to formalize
the canonical representation, called normal forms by Conway.
The definition of the {\it Conway Normal Form} allows an analysis of the structure
of surreal numbers as an ordered vector space over $\mathbb{R}$.
This framework provides a path for future research on
surreal numbers, as it allows e.g. the reformulation
of basic arithmetic operations in terms of vector space operations,
thus facilitating the application of vector space theory to the analysis of surreal numbers.
\par
The formalization follows \cite{Conway:2001,Ehrlich,Ehrlich2012}, 
selected fragments have been described in \cite{CNFPakKaliczyk24}.
\par  
In Section 1, we define the relation between two numbers, x and y, as commensurate if and only if
$x < n \cdot y$ and $y < m \cdot x$, for some $n,m\in\mathbb{N}^+$ (see~Def1).
Then we prove that this relation is both an equivalence and a convex relation.
Conway defines this relation using only one natural number, which is equivalent to our approach (see~Th7).
Additionally, we define and prove the fundamental property of the {\it infinitesimal less} operator (see~Def2), as follows:
$x <^\infty y$ if $x \cdot n < y$ for all $n\in  \mathbb{N}^+$.
\par
Section 2 introduces the Conway $\boldsymbol\omega$-map (\cite{Conway:2001}) and demonstrates the fundamental property
$\boldsymbol\omega^0=1$ (see~Th26), $\boldsymbol\omega^{(x+y)}\approx \boldsymbol\omega^x \cdot \boldsymbol\omega^y$ (see~Th27)
which are typical for the standard power function. Note that it has an additional properties, namely that $\boldsymbol\omega^x <^\infty \boldsymbol\omega^y $ for $x < y$.
We also examines the behaviour of $\boldsymbol\omega$-map in the context of the commensurate and infinitesimal less relations, as well as applying the standard absolute value to extend context for negative surreal numbers.
\par
In Section 3 we  prove the existence of
the unique characterization of non zero surreal numbers $x$
as pairs consisting of a commensurate leader $y$ and a non zero real number $r$
for a given $x\not\approx 0$ such that $|x-r\cdot\boldsymbol\omega^y|<^\infty |x|$.
We define $\boldsymbol\omega_r(x) = r$, $\boldsymbol\omega_y(x)=y$ (see~Def7, Def8)
\par
In the following section, we direct our attention to the convex subclass of surreal numbers
differing from s by infinitesimal less than $\boldsymbol\omega^y$, which is referred to
as the $\beta$-term in Conway's handbook, where $\beta$ is defined in the context of this work.
We say that $x$ is $(s,y,r)-\textrm{term}$ if and only if $|x  - (s +  r\cdot\boldsymbol\omega^y)| <^\infty \boldsymbol\omega^y$ (Def12)
Note that our definition of the $\beta$-term is based on an explanation provided by Ehrlich (\cite{Ehrlich}, Theorem 13).
\par
In Section 5, in accordance with Ehrlich's approach, we formally introduce the convex subclass
$\bigcap \boldsymbol s,\boldsymbol y, \boldsymbol r,\alpha$ as follows:
$$x\:\textrm{is}\:\bigcap \boldsymbol s,\boldsymbol y, \boldsymbol r,\alpha\; \Longleftrightarrow \;\forall_{\beta<\alpha}\: x\: \textrm{is}\:(\boldsymbol s(\beta),\boldsymbol y(\beta),\boldsymbol r(\beta))-\textrm{term},$$
where $\boldsymbol s$, $\boldsymbol y$ are sequences of surreal numbers and $\boldsymbol r$ is real numbers, each of at least $\alpha$-length.
Next proceed to assume that the length of $\boldsymbol s$ is at least $\alpha+1$.
A triple $(\boldsymbol s,\boldsymbol y, \boldsymbol r)$ {\it simplest on} $\alpha$ if $\alpha=0$ and $\boldsymbol s(\alpha)=0$ or $\alpha\neq 0$,
$\boldsymbol s(\alpha)$ is  $\bigcap \boldsymbol s,\boldsymbol y, \boldsymbol r,\alpha$ and has the smallest birth of all
 $\bigcap \boldsymbol s,\boldsymbol y, \boldsymbol r,\alpha$ surreal numbers (see~Def15).
Additionally, we call a triple $(\boldsymbol s,\boldsymbol y, \boldsymbol r)$ {\it simplest up to} $\alpha$ if $(\boldsymbol s,\boldsymbol y, \boldsymbol r,\beta)$ simplest for all $\beta<\alpha$ (see~Def16).
This section is concluded with the proof of two properties of the sequence $\boldsymbol s$.
Firstly, we demonstrate that the sequence $\boldsymbol s$ is unique up to position $\alpha$
if it contains only uniq-surreal numbers and if $(\boldsymbol s,\boldsymbol y, \boldsymbol r)$ is in its simplest up to $\alpha$ (Th77,Th80)
Secondly, we provide an example of a sequence $\boldsymbol s$ of uniq-surreal numbers
for which $(\boldsymbol s,\boldsymbol y, \boldsymbol r)$ is simplest up to $\alpha$
 under the assumption that $\boldsymbol y$ is a strictly decreasing sequence, and that $\boldsymbol r$
  is a sequence of non-zero real numbers (Th82).
 Using these properties, we define Conway's generalistion of partial sums as follows.
\begin{definition}[Def18]
Let $\alpha$ be an ordinal, $\boldsymbol y = \{\boldsymbol y_\beta\}_{\beta<\alpha}$ be a strictly decreasing sequence of surreal numbers,
$\boldsymbol r = \{\boldsymbol r_\beta\}_{\beta<\alpha}$ be a sequence of non-zero real.
Consider $\boldsymbol s = \{\boldsymbol s_\beta\}_{\beta\leq\alpha}$ where the triple $(\boldsymbol s,\boldsymbol y, \boldsymbol r)$ is simplest up to $\alpha$.
For each each $\beta\leq \alpha$ we define unique expression $\sum_{\gamma<\beta} {\boldsymbol\omega}^{{\boldsymbol y_\gamma}}\cdot {\boldsymbol r_\gamma}$
to be $\boldsymbol s_\beta$ called $\beta$th Conway's partial sum.
\end{definition}
\par
In Section 6, we concentrate on the approximation of a given number $x\not\approx 0$ using commensurate leaders.
Applying $\boldsymbol \omega$-maps, we get $x_1 :\!= x - \boldsymbol \omega^{\boldsymbol y_0}\cdot \boldsymbol r_0 $
which is infinitely smaller in absolute terms than $x$
where
$\boldsymbol r_0:\!= \boldsymbol \omega_r(x)$,
$\boldsymbol y_0 :\!= \boldsymbol \omega_y(x)$.
Then, if $x_1\not\approx 0$, it is possible to produce another $\boldsymbol r_1$, $\boldsymbol y_1$, $x_2$ in a similar manner where $|x_2| <^\infty |x_1| <^\infty |x|$
and $x = \boldsymbol \omega^{\boldsymbol y_0}\cdot \boldsymbol r_0 + \boldsymbol \omega^{\boldsymbol y_1}\cdot \boldsymbol r_1 + x_2$.
We call the constructed sequences
$(\boldsymbol r,\boldsymbol y)$ the $\alpha$-{\it{}name} of $x$ if the remainder is non-zero in each iteration
$\beta$ for $\beta<\alpha$ where $\alpha$ is an ordinal.
As we illustrated in Theorem Th101, for any a strictly decreasing sequence of surreal numbers
$\boldsymbol y = \{\boldsymbol y_\beta\}_{\beta<\alpha}$ and  a sequence of non-zero real
$\boldsymbol r = \{\boldsymbol r_\beta\}_{\beta<\alpha}$, $(\boldsymbol r,\boldsymbol y)$ is the $\alpha$-name of
$\sum_{\beta<\alpha} {\boldsymbol\omega}^{{\boldsymbol y_\beta}}\cdot {\boldsymbol r_\beta}$.
We constructed also an ordinal $\alpha$ and two $\alpha$-length sequences $(\boldsymbol r,\boldsymbol y)$, for a given $x$ such that $\sum_{\beta<\alpha} {\boldsymbol\omega}^{{\boldsymbol y_\beta}}\cdot {\boldsymbol r_\beta}\approx x$ (see~Th100).
Finally, we prove that this pair of sequences is unique (see~Th102), known as the Conway Normal Form (\cite{Conway:2001}).
}
}

@inproceedings{CNFPakKaliczyk24,
  author       = {Karol Pak and
                  Cezary Kaliszyk},
  editor       = {Yves Bertot and
                  Temur Kutsia and
                  Michael Norrish},
  title        = {Conway Normal Form: Bridging Approaches for Comprehensive Formalization
                  of Surreal Numbers},
  booktitle    = {15th International Conference on Interactive Theorem Proving, {ITP}
                  2024, September 9-14, 2024, Tbilisi, Georgia},
  series       = {LIPIcs},
  volume       = {309},
  pages        = {29:1--29:18},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2024},
  doi          = {10.4230/LIPICS.ITP.2024.29}
}