For addition, use the well-founded induction on pairs of surreal representatives from Definition 2.13. By Definition 3.1, every option of \(a+b\) replaces exactly one of \(a,b\) by one of its options. Lemma 2.3 makes the resulting pair smaller, so the induction hypothesis proves that every option of \(a+b\) is surreal, as required by Definition 2.9.

It remains to separate a left option from a right option. There are four cases:

In the first case Theorem 2.10 and strict transitivity from Theorem 2.7 give \(a^L\prec a^R\), and strict translation invariance from Theorem 3.3 gives \(a^L+b\prec a^R+b\). The second case is identical with \(a,b\) interchanged. In the third case, \(a^L\prec a\) and \(b\preceq b^R\); in the fourth, \(a\prec a^R\) and \(b^L\preceq b\). The two mixed monotonicity statements of Theorem 3.3 again put the chosen left option strictly below the chosen right option. By Definition 2.4, this strict inequality excludes the reverse weak comparison, which is exactly the separation condition in Definition 2.9.

For negation, induct on the birthday of the underlying game of the surreal representative \(a\). Definition 3.4 says that a left option of \(-a\) is \(-a^R\), while a right option is \(-a^L\). Theorem 2.10 and strict transitivity from Theorem 2.7 give \(a^L\prec a\prec a^R\), hence \(a^L\prec a^R\). If \(-a^L\preceq -a^R\), order reversal in Theorem 3.5 would give \(a^R\preceq a^L\), contradicting that strict comparison. Thus the left and right options of \(-a\) satisfy the separation condition of Definition 2.9. Each negated option is surreal by the induction hypothesis and Lemma 2.3. Thus \(-a\) satisfies Definition 2.9. Finally, Definition 2.12 turns each game, together with the surrealness just proved, into the corresponding operation on representatives.

The addition and negation formulas are independent of the representatives by the congruence assertions in Theorems 3.3 and 3.5.

The order is also independent of representatives. Indeed, suppose \(a\sim a'\), \(b\sim b'\), and \(a\preceq b\). The two appropriate components of the equivalences give \(a'\preceq a\) and \(b\preceq b'\); transitivity from Theorem 2.7 yields \(a'\preceq b'\). The converse follows symmetrically. Reflexivity and transitivity therefore pass to classes. If \([a]\leq [b]\) and \([b]\leq [a]\), then \(a\sim b\) by Definition 2.5, so \([a]=[b]\) by the definition of an equivalence class. Thus the quotient order is a partial order. The asserted characterization of strict order now follows from the definitions of \(\prec \) and strict order in a partial order.

The zero, associativity, and commutativity laws descend from Theorem 3.2, and the inverse law descends from Theorem 3.6; an equivalence of representatives is precisely equality of their classes. Finally, translation monotonicity is the class-level form of Theorem 3.3. Commutativity from Theorem 3.2 permits the common summand to be placed on either side.

There is a natural injective map

This is well defined and injective because both quotients identify representatives exactly when their underlying games are game equivalent. Pull back the quotient order along \(\iota \), so \([s]\leq [t]\) precisely when \(s_{\mathrm{game}}\preceq t_{\mathrm{game}}\). Definition 3.10 and Theorem 3.7 show that the image contains zero and is closed under addition and negation. Hence Theorem 3.9 supplies the additive commutative group, partial order, and order compatibility on \(\mathbf{No}_{\mathrm{short}}\). Theorem 2.11 upgrades this partial order to a linear order.