Surreal multiplication #
In this file, we show that multiplication of surreal numbers is well-defined, and thus the surreal numbers form a linear ordered commutative ring. This is Theorem 8 in [Conway2001], or Theorem 3.8 in [SchleicherStoll].
An inductive argument proves the following three main theorems:
- P1: being numeric is closed under multiplication,
- P2: multiplying a numeric pregame by equivalent numeric pregames results in equivalent pregames,
- P3: the product of two positive numeric pregames is positive (
mul_pos).
P1 allows us to define multiplication as an operation on numeric pregames, P2 says that this is
well-defined as an operation on the quotient by IGame.Equiv, namely the surreal numbers, and P3 is
an axiom that needs to be satisfied for the surreals to be a OrderedRing.
We follow the proof in [SchleicherStoll], except that we use the well-foundedness of the hydra
relation CutExpand on Multiset IGame instead of the argument based on a depth function in the
paper. As in said argument, P3 is proven by proxy of an auxiliary P4, which states that for
x₁ < x₂ and y, then x₁ * y + x₂ * a < x₁ * a + x₂ * y when a ∈ yᴸ, and
x₁ * b + x₂ * y < x₁ * y + x₂ * b when b ∈ yᴿ.
Reducing casework #
This argument is very casework heavy in a way that's difficult to automate. For instance, in P1, we
have to prove four different inequalities of the form
a ∈ (x * y)ᴸ → b ∈ (x * y)ᴿ → a < b, and depending on what form the options of
x * y take, we have to apply different instantiations of the inductive hypothesis.
To greatly simplify things, we work uniquely in terms of left options, which we achieve by rewriting
a ∈ xᴿ as -a ∈ (-x)ᴸ. We then show that our distinct lemmas and inductive
hypotheses are invariant under the appropriate sign changes. In the P1 example, this makes it so
that one case (mulOption_lt_of_lt) is enough to conclude the others (mulOption_lt), and the same
goes for the other parts of the proof.
Note also that we express all inequalities in terms of Game instead of IGame; this allows us to
make use of abel and all of the theorems on OrderedAddCommGroup.
Predicates P1 – P4 #
Symmetry properties of P1 – P4 #
Inductive setup #
P1 follows from the inductive hypothesis #
P2 follows from the inductive hypothesis #
P4 follows from the inductive hypothesis #
Instances and corollaries #
Equations
- One or more equations did not get rendered due to their size.