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.
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).
This is Theorem 8 in [Conway2001], or Theorem 3.8 in [SchleicherStoll]. 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 PGame.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 PGame instead of the argument based
on a depth function in the paper.
In the argument, P3 is stated with four variables x₁, x₂, y₁, y₂ satisfying x₁ < x₂ and
y₁ < y₂, and says that x₁ * y₂ + x₂ * x₁ < x₁ * y₁ + x₂ * y₂, which is equivalent to
0 < x₂ - x₁ → 0 < y₂ - y₁ → 0 < (x₂ - x₁) * (y₂ - y₁), i.e.
@mul_pos PGame _ (x₂ - x₁) (y₂ - y₁). It has to be stated in this form and not in terms of
mul_pos because we need to show show P1, P2 and (a specialized form of) P3 simultaneously, and
for example P1 x y will be deduced from P3 with variables taking values simpler than x or y
(among other induction hypotheses), but if you subtract two pregames simpler than x or y,
the result may no longer be simpler.
The specialized version of P3 is called P4, which takes only three arguments x₁, x₂, y and
requires that y₂ = y or -y and that y₁ is a left option of y₂. After P1, P2 and P4 are
shown, a further inductive argument (this time using the GameAdd relation) proves P3 in full.
Implementation strategy of the inductive argument: we
- extract specialized versions (
IH1,IH2,IH3,IH4andIH24) of the induction hypothesis that are easier to apply (takesIsOptionarguments directly), and - show they are invariant under certain symmetries (permutation and negation of arguments) and that the induction hypothesis indeed implies the specialized versions.
- utilize the symmetries to minimize calculation.
The whole proof features a clear separation into lemmas of different roles:
- verification of symmetry properties of P and IH (
P3_comm,ih1_neg_left, etc.), - calculations that connects P1, P2, P3, and inequalities between the product of
two surreals and its options (
mulOption_lt_iff_P1, etc.), - specializations of the induction hypothesis
(
numeric_option_mul,ih1,ih1_swap,ih₁₂,ih4, etc.), - application of specialized indution hypothesis
(
P1_of_ih,mul_right_le_of_equiv,P3_of_lt, etc.).
References #
- [Conway, On numbers and games][Conway2001]
- [Schleicher, Stoll, An introduction to Conway's games and numbers][SchleicherStoll]
The nontrivial part of P1 in [SchleicherStoll] says that the left options of x * y
are less than the right options, and this is the general form of these statements.
Equations
Instances For
The proposition P2, without numericity assumptions.
Instances For
The proposition P3, without the x₁ < x₂ and y₁ < y₂ assumptions.
Instances For
The proposition P4, without numericity assumptions. In the references, the second part of the
conjunction is stated as ∀ j, P3 x₁ x₂ y (y.moveRight j), which is equivalent to our statement
by P3_comm and P3_neg. We choose to state everything in terms of left options for uniform
treatment.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The conjunction of P2 and P4.
Equations
- Surreal.Multiplication.P24 x₁ x₂ y = (Surreal.Multiplication.P2 x₁ x₂ y ∧ Surreal.Multiplication.P4 x₁ x₂ y)
Instances For
Symmetry properties of P1, P2, P3, and P4 #
Explicit calculations necessary for the main proof #
The type of lists of arguments for P1, P2, and P4.
- P1: SetTheory.PGame → SetTheory.PGame → Surreal.Multiplication.Args
- P24: SetTheory.PGame → SetTheory.PGame → SetTheory.PGame → Surreal.Multiplication.Args
Instances For
The multiset associated to a list of arguments.
Equations
- x.toMultiset = match x with | Surreal.Multiplication.Args.P1 x y => {x, y} | Surreal.Multiplication.Args.P24 x₁ x₂ y => {x₁, x₂, y}
Instances For
A list of arguments is numeric if all the arguments are.
Equations
- a.Numeric = ∀ x ∈ a.toMultiset, x.Numeric
Instances For
The relation specifying when a list of (pregame) arguments is considered simpler than another:
ArgsRel a₁ a₂ is true if a₁, considered as a multiset, can be obtained from a₂ by
repeatedly removing a pregame from a₂ and adding back one or two options of the pregame.
Equations
Instances For
ArgsRel is well-founded.
The statement that we will show by induction using the well-founded relation ArgsRel.
Equations
- Surreal.Multiplication.P124 x = match x with | Surreal.Multiplication.Args.P1 x y => (x * y).Numeric | Surreal.Multiplication.Args.P24 x₁ x₂ y => Surreal.Multiplication.P24 x₁ x₂ y
Instances For
The property that all arguments are numeric is leftward-closed under ArgsRel.
A specialized induction hypothesis used to prove P1.
Equations
- Surreal.Multiplication.IH1 x y = ∀ ⦃x₁ x₂ y' : SetTheory.PGame⦄, x₁.IsOption x → x₂.IsOption x → y' = y ∨ y'.IsOption y → Surreal.Multiplication.P24 x₁ x₂ y'
Instances For
Specialize ih to obtain specialized induction hypotheses for P1 #
P1 follows from the induction hypothesis.
A specialized induction hypothesis used to prove P2 and P4.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A specialized induction hypothesis used to prove P4.
Equations
- Surreal.Multiplication.IH4 x₁ x₂ y = ∀ ⦃z w : SetTheory.PGame⦄, w.IsOption y → (z.IsOption x₁ → Surreal.Multiplication.P2 z x₂ w) ∧ (z.IsOption x₂ → Surreal.Multiplication.P2 x₁ z w)
Instances For
Specialize ih' to obtain specialized induction hypotheses for P2 and P4 #
Symmetry properties of IH24.
Symmetry properties of IH4.
P2 follows from specialized induction hypotheses (one half of the equality).
The statement that all left options of x * y of the first kind are less than itself.
Equations
- Surreal.Multiplication.MulOptionsLTMul x y = ∀ ⦃i : x.LeftMoves⦄ ⦃j : y.LeftMoves⦄, ⟦x.mulOption y i j⟧ < ⟦x * y⟧
Instances For
That the left options of x * y are less than itself and the right options are greater, which
is part of the condition that x * y is numeric, is equivalent to the conjunction of various
MulOptionsLTMul statements for x, y and their negations. We only show the forward
direction.
A condition just enough to deduce P3, which will always be used with x' being a left
option of x₂. When y₁ is a left option of y₂, it can be deduced from induction hypotheses
IH24 x₁ x₂ y₂, IH4 x₁ x₂ y₂, and (x₂ * y₂).Numeric (ih3_of_ih); when y₁ is
not necessarily an option of y₂, it follows from the induction hypothesis for P3 (with x₂
replaced by a left option x') after the main theorem (P124) is established, and is used to
prove P3 in full (P3_of_lt_of_lt).
Equations
- One or more equations did not get rendered due to their size.
Instances For
P3 follows from IH3 (so P4 (with y₁ a left option of y₂) follows from the induction
hypothesis).
The main chunk of Theorem 8 in [Conway2001] / Theorem 3.8 in [SchleicherStoll].
One additional inductive argument that supplies the last missing part of Theorem 8.