A Blueprint for Short Surreal Numbers in Lean

5.1 Multiplication on equivalence classes

Theorem 5.1 Multiplication on surreal representatives
✓

If \(a,b\) are surreal representatives, their game product is surreal. Moreover, replacing either representative by an equivalent one does not change the equivalence class of the product. Thus multiplication is a well-defined operation on representatives modulo \(\sim \).

Proof ▶

By Definition 2.12, write

\[ a=(a_{\mathrm{game}},a_{\mathrm{proof}}),\qquad b=(b_{\mathrm{game}},b_{\mathrm{proof}}). \]

Thus \(a_{\mathrm{proof}}\) and \(b_{\mathrm{proof}}\) witness that the short games \(a_{\mathrm{game}}\) and \(b_{\mathrm{game}}\) satisfy Definition 2.9. Theorem 4.10 shows that the product \(a_{\mathrm{game}}b_{\mathrm{game}}\), formed as in Definition 4.1, is again surreal. Hence

\[ \bigl(a_{\mathrm{game}}b_{\mathrm{game}},(ab)_{\mathrm{proof}}\bigr) \]

is a surreal representative, where \((ab)_{\mathrm{proof}}\) denotes the resulting witness.

For alternative representatives

\[ a'=(a'_{\mathrm{game}},a'_{\mathrm{proof}}),\qquad b'=(b'_{\mathrm{game}},b'_{\mathrm{proof}}), \]

assume that their underlying games satisfy \(a_{\mathrm{game}}\sim a'_{\mathrm{game}}\) and \(b_{\mathrm{game}}\sim b'_{\mathrm{game}}\) in the sense of Definition 2.5. Theorem 4.13 then gives

\[ a_{\mathrm{game}}b_{\mathrm{game}} \sim a'_{\mathrm{game}}b'_{\mathrm{game}}. \]

Thus the equivalence class of the product is independent of both chosen representatives.

Definition 5.2 Multiplication on short surreal numbers
✓

Define multiplication on \(\mathbf{No}_{\mathrm{short}}\) by taking the game product of any two representatives and then passing to the quotient.

Multiplication on \(\mathbf{No}_{\mathrm{short}}\) is associative and commutative, has identity \(1\), and has \(0\) as an absorbing element.

Proof ▶

By Definition 3.10, choose surreal representatives \(a_0,b_0,c_0\) for three arbitrary classes. Definition 5.2 identifies their products with the classes of the corresponding game products. The commutativity, unit, and zero equivalences of Theorem 4.2 therefore give

\[ [a_0b_0]=[b_0a_0],\qquad [1\cdot a_0]=[a_0]=[a_0\cdot 1], \qquad [0\cdot a_0]=[0]=[a_0\cdot 0]. \]

Likewise, Theorem 4.14, applied to the surreal games \(a_0,b_0,c_0\), gives

\[ [(a_0b_0)c_0]=[a_0(b_0c_0)]. \]

Equality of each displayed pair of classes follows precisely because the representative games are equivalent. Since the representatives were arbitrary, all the asserted laws hold on \(\mathbf{No}_{\mathrm{short}}\).

Theorem 5.4 Distributivity on the quotient
✓

For \(a,b,c\in \mathbf{No}_{\mathrm{short}}\),

\[ a(b+c)=ab+ac, \qquad (a+b)c=ac+bc. \]
Proof ▶

Choose surreal representatives \(a_0,b_0,c_0\) as permitted by Definition 3.10. By Definition 5.2, left distributivity reduces to the equivalence

\[ a_0(b_0+c_0)\sim a_0b_0+a_0c_0, \]

which is Theorem 4.3. Equivalent representatives define the same class, so this proves \(a(b+c)=ab+ac\).

For right distributivity, use the commutativity in Theorem 5.3 to write

\[ (a+b)c=c(a+b)=ca+cb=ac+bc, \]

where the middle equality is the left distributive law just proved and the last equality again uses commutativity.

Theorem 5.5 Commutative ring structure
✓
#

The short surreal numbers \(\mathbf{No}_{\mathrm{short}}\) form a commutative ring.

Proof ▶

Theorem 3.11 supplies the additive commutative group, including associativity, commutativity, the zero element, and additive inverses. Definition 5.2 supplies multiplication. Its associativity, commutativity, identity element, and zero laws are exactly Theorem 5.3, while both distributive axioms are Theorem 5.4. These are precisely the axioms of a commutative ring.