+By Axiom \autoref{ax:leq-relation}, this creates two possible cases. Either
+$\exists (x_L)_L \in (X_L)_L$ such that $(x_L)_L \geq x$ or $\exists x_R \in
+X_R$ such that $x_R \leq x_L$. By Axiom \autoref{ax:number-definition}, the
+latter case is impossible.
+
+We address the remaining case by inductively noting that $(x_L)_L \leq x_L$,
+thus $x \leq (x_L)_L$. However, since this means that $x \leq (x_L)_L \leq
+x_L$, by \autoref{thm:transitive}, $x \leq x_L$. By definition, this means $X_L
+\nleq x_L$, a contradiction since $x_L \in X_L$.
+
+The proof of $x \leq X_R$ follows similarly.
+\end{proof}
+
+\begin{theorem} \label{thm:all-comparable}
+For every $x$ and $y$ in the universe, if $y \nleq x$, then $x \leq y$.
+\end{theorem}
+
+\begin{proof}
+Seeking a contradiction, let $x$ and $y$ be numbers such that $y \nleq x$ and
+$x \nleq y$.
+
+By Axiom \autoref{ax:leq-relation}, this creates two possible cases. Either
+$\exists x_L \in X_L$ such that $x_L \geq y$ or $\exists y_R \in Y_R$ such that
+$x \geq y_R$. In the first case, by \autoref{thm:weak-self-relation}, $x_L \leq
+x$, so by \autoref{thm:transitive}, $y \leq x$, a contradiction. A similar
+contradiction is reached in the other case.
+\end{proof}
+
+Well, that's it. We have a total order, but we're no longer in the same
+universe as Knuth. We can even go one step further and note that, by only
+considering a finite number of generations, we are guaranteed to only generate
+a finite quantity of numbers, and a finite totally ordered set is automatically
+well ordered.
+
+With a total order in hand, we can strengthen $x \nleq y$ into $x > y$,
+motivating the following theorem.
+
+\begin{theorem} \label{thm:strong-self-relation}
+For any number $x = \surreal{X_L}{X_R}$, it holds that $X_L < x < X_R$.
+\end{theorem}
+
+\begin{proof}
+Simply recognize why `linear order' is a synonym for `total order'.
+\end{proof}
+
+Moving away from considering order, note that creating Definition
+\autoref{defi:similar} imposed order on our universe at the cost of some
+uniqueness. Let's examine that loss of uniqueness a bit further.
+
+The twenty numbers from generations 0-2 break down into seven similarity-based
+equivalence classes, as shown below.
+
+$$\surreal{}{-1} \similar \surreal{}{-1,0} \similar \surreal{}{-1,1} \similar \surreal{}{-1,0,1}$$
+$$\surreal{}{0} \similar \surreal{}{0,1}$$
+$$\surreal{-1}{0} \similar \surreal{-1}{0,1} \similar \surreal{-1}{}$$
+$$\surreal{}{} \similar \surreal{-1}{1}$$
+$$\surreal{0}{1} \similar \surreal{-1,0}{1}$$
+$$\surreal{0}{} \similar \surreal{-1,0}{} \similar \surreal{}{1}$$
+$$\surreal{1}{} \similar \surreal{0,1}{} \similar \surreal{-1,1}{} \similar \surreal{-1,0,1}{}$$
+
+Thus, whereas Knuth's universe has 20 numbers by generation-2, our universe
+only has seven numbers. For convenience when writing our program which creates
+a (finite set based) surreal numberline, we desire a unique representation for
+each equivalence class. Toward that end, we introduce the following
+definition and theorem.
+
+\begin{theorem} \label{thm:reduced-form}
+Given an arbitrary number $x$, there exists a number $x' =
+\surreal{X'_L}{X'_R}$ which is similar to $x$ and has the property that the
+cardinality of both $X'_L$ and $X'_R$ are one or zero.
+\end{theorem}
+
+\begin{proof}
+Let $x = \surreal{X_L}{X_R}$. Since a finite, total ordered set contains a
+maximum and minimum element, it follows that we can define $X'_L$ as containing
+only the maximum element of $X_L$ and define $X'_R$ as containing only the
+minimum element of $X_R$. If either $X_L$ or $X_R$ are the empty set, the
+corresponding $X'_L$ or $X'_R$ are also the empty set.
+
+Use these two newly defined sets to construct $x' = \surreal{X'_L}{X'_R}$. This
+clearly satisfies Axiom \autoref{ax:number-definition} by inheritance. Then,
+to show that $x \similar x'$, we apply Axiom \autoref{ax:leq-relation} in both
+directions.
+
+In the forward direction, $x \leq x'$ requires that, $\forall x_L \in X_L$, it
+must hold that $x_L \ngeq x'$. Indeed, from \autoref{thm:strong-self-relation},
+\autoref{thm:transitive}, and our explicit construction of $X'_L$ as the
+maximum element of $X_L$, the desired relation holds since $X_L \leq X'_L <
+x'$.
+
+Also in the forward direction, $x \leq x'$ requires that, $\forall x'_R \in
+X'_R$, it holds that $x'_R \nleq x$. By the same theorems/construction as
+before, the desired relation holds since $x < X_R \leq X'_R$.
+
+The reverse direction follows via a similar pair of arguments.
+\end{proof}
projects / surreal-numbers / blobdiff