@ARTICLE{SURREALS.MIZ,
  AUTHOR = {P\k{a}k, Karol},
  TITLE = {Surreal Numbers: A Study of Square Roots},
  SECTION1 = {Surreal Numbers Without Negative Options},
  SECTION2 = {Square Root Construction},
  SECTION3 = {The Square Root of a Surreal Number},
  SECTION4 = {Selected Square Root Properties},
  SECTION5 = {Square Root of Negative Surreal Numbers - Outside the Defined Range},
  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 sets out to formalize the concept of the square root as proposed by Clive Bach 
in the section entitled {\it Properties of Division} in Conway's book. 
The proposed construction extends the classical approach to the square root 
of real numbers to include both infinitely large and infinitely small numbers.
},
INTRODUCTION = {
In the Chapter {\it The class \textbf{\textit{No}} is a field}~\cite{Conway:2001},
Conway also quotes the definition of a square root proposed by Clive Bach.
This definition is formulated in Conway's typical way, using double recursion
and the concept and typical options as follows:
\begin{equation}\label{SqrtEq}
\sqrt{x}=y = \{\sqrt{x^L},\frac{x+y^L\cdot y^R}{y^L+ y^R} \mid
   \sqrt{x^R},\frac{x+y^L\cdot y^{L\bullet}}{y^{L}+ y^{L\bullet}},
   \frac{x+y^R\cdot y^{R\bullet}}{y^{R}+ y^{R\bullet}}\}
\end{equation}
\noindent
where $x^L$, $x^R$ represent non-negative options of $x$, while $y^L$,
$y^{L\bullet}$, $y^R$, $y^{R\bullet}$ denote the options for $y$ such
that no denominator is zero. In addition, the construction of this number
is entirely absent, and the veracity of this definition is left to the reader
to demonstrate through an {\it easy inductive proof}.
\par
In our formalization, we adapt the idea presented for the inverse element proposed
by Schleicher and Stoll~\cite{schleicher}, which was previously employed in our
earlier formalization~\cite{SURREALI.ABS} in the Mizar system formalization \cite{BancerekJAR:2018}.
We first introduce a restriction that limits the members of the sets
$L_x$, $R_x$ to those that are non-negative.
Let $x$ be a surreal number. We define the function $\texttt{NNPart}(x)$ (see~Def1) to be
\begin{equation}
\{0, \{x^L \in L_x \mid x^L \geq 0\}\mid \{x^R \in R_x \mid x^R \geq 0\}\}
\end{equation}
and we prove that $\texttt{NNPart}$ is born no later than $x$ (see~Th3) and
$\approx x$ (see~Th5) for any non-negative $x$.
\par
Then two sequences of sets of surreal numbers are defined, namely,
$\{\sqrt[L]{n,x_0,x}\}_{n\in\mathbb{N}}$,
$\{\sqrt[R]{n,x_0,x}\}_{n\in\mathbb{N}}$ for a given surreal number $x$ and
an initial pair of of surreal number sets $x_0$.
These sequences are defined (see~Def3,Def4,Def5) recursively as follows:
\begin{equation}
  \begin{aligned}
  \sqrt[L]{0,x_0,x} &= L_{x_0},\\ \sqrt[R]{0,x_0,x} &= R_{x_0},\\
  \sqrt[L]{n+1,x_0,x} &= \sqrt[L]{n,x_0,x} \cup \texttt{S}(x,\sqrt[L]{n,x_0,x},\sqrt[R]{n,x_0,x})\\
  \sqrt[R]{n+1,x_0,x} &= \sqrt[R]{n,x_0,x} \cup \texttt{S}(x,\sqrt[L]{n,x_0,x},\sqrt[L]{n,x_0,x})\\
   & \strut\mkern50mu\cup\texttt{S}(x,\sqrt[R]{n,x_0,x},\sqrt[R]{n,x_0,x})\\
\end{aligned}
\end{equation}
\noindent
where $\texttt{S}(x,A,B)=\{\frac{x+a\cdot b}{a+b}\mid a \in X \wedge b \in Y \wedge a+b\neq 0\}$
and $A$ and $B$ represent arbitrary sets of surreal numbers (see~Def2).
\par
The condition \eqref{SqrtEq} can now be expressed in a more formal, but still recursive way, as follows:
\begin{equation}
\sqrt{x} = \langle\bigcup_{n\in\mathbb{N}} \sqrt[L]{n,x_0,x},\bigcup_{n\in\mathbb{N}} \sqrt[R]{n,x_0,x}\rangle
\end{equation} %can be considered to represent a value of $y$ in the equation \eqref{SqrtEq}
where $x_0 = \langle\{\sqrt{x_L}\mid x_L \in L_{\texttt{NNart}(x)}\},
\{\sqrt{x_R}\mid x_R \in R_{\texttt{NNPart}(x)}\}\rangle$.
\par
To implement this kind of recursion in the Mizar system we use a sequence $\sqrt[\alpha]{\,\cdot\,}$,
where $\sqrt[\alpha]{\,\cdot\,}$ is a function defined on day $\alpha$ for each ordinal $\alpha$, with the following definition:
\begin{equation}
\sqrt[\alpha]{x} = \langle\bigcup_{n\in\mathbb{N}}\! \sqrt[L]{n,(\bigcup_{\beta<\alpha}\!\sqrt[\beta]{\,\cdot\,})[L_{\texttt{NNPart}(x)}],x}
\bigcup_{n\in\mathbb{N}} \sqrt[R]{n,(\bigcup_{\beta<\alpha}\!\sqrt[\beta]{\,\cdot\,})[R_{\texttt{NNPart}(x)}],x}\rangle
\end{equation}
\noindent
where $x$ represents an element of day $\alpha$.
It is important for understanding the correctness of the definition that
the constructed sequence is a $\subseteq$-monotone in the set-theoretic sense,
so that we can treat $\bigcup_{\beta<\alpha} \sqrt[\beta]{\,\cdot\,}$ as a function.
We may now define $\sqrt(x)$ as $\sqrt[\alpha](x)$, where $\alpha$ represents the day
on which a given positive $x$ is born (see~Def7)
and satisfies the fundamental properties of square root for non-negative real numbers
such as:  $0\leq \sqrt{x} < \sqrt{y}$ for all surreal numbers $0< x <y$
(see~Th27), $\sqrt{x}^{-1} \approx \sqrt{x^{-1}}$ for positive surreal (see~Th30).
\par
The concept proposed by Clive Bach was initially introduced for non-negative numbers;
however, there are no inherent limitations to its application beyond the natural domain.
We have shown that, outside the domain, the fundamental property
$x\approx y \Rightarrow \sqrt{x} \approx \sqrt{y}$ is lost.
Indeed, we prove that $\sqrt{-1}=-1$ and for any positive $x$ we can construct
a surreal number $y \approx -1$ such that $\sqrt{y}<-x$ (see~Th31).
}
}