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 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, IH4 and IH24) of the induction hypothesis that are easier to apply (taking IsOption arguments 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 connect 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 induction 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]

def Surreal.Multiplication.P1 (x₁ x₂ x₃ y₁ y₂ y₃ : SetTheory.PGame) : Prop

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

• Surreal.Multiplication.P1 x₁ x₂ x₃ y₁ y₂ y₃ = (⟦x₁ * y₁⟧ + ⟦x₂ * y₂⟧ - ⟦x₁ * y₂⟧ < ⟦x₃ * y₁⟧ + ⟦x₂ * y₃⟧ - ⟦x₃ * y₃⟧)

def Surreal.Multiplication.P2 (x₁ x₂ y : SetTheory.PGame) : Prop

The proposition P2, without numericity assumptions.

Equations

• Surreal.Multiplication.P2 x₁ x₂ y = (x₁ ≈ x₂ → ⟦x₁ * y⟧ = ⟦x₂ * y⟧)

def Surreal.Multiplication.P3 (x₁ x₂ y₁ y₂ : SetTheory.PGame) : Prop

The proposition P3, without the x₁ < x₂ and y₁ < y₂ assumptions.

Equations

• Surreal.Multiplication.P3 x₁ x₂ y₁ y₂ = (⟦x₁ * y₂⟧ + ⟦x₂ * y₁⟧ < ⟦x₁ * y₁⟧ + ⟦x₂ * y₂⟧)

def Surreal.Multiplication.P4 (x₁ x₂ y : SetTheory.PGame) : Prop

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.

def Surreal.Multiplication.P24 (x₁ x₂ y : SetTheory.PGame) : Prop

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)

Symmetry properties of P1, P2, P3, and P4

theorem Surreal.Multiplication.P3_comm {x₁ x₂ y₁ y₂ : SetTheory.PGame} : P3 x₁ x₂ y₁ y₂ ↔ P3 y₁ y₂ x₁ x₂

theorem Surreal.Multiplication.P3.trans {x₁ x₂ x₃ y₁ y₂ : SetTheory.PGame} (h₁ : P3 x₁ x₂ y₁ y₂) (h₂ : P3 x₂ x₃ y₁ y₂) : P3 x₁ x₃ y₁ y₂

theorem Surreal.Multiplication.P3_neg {x₁ x₂ y₁ y₂ : SetTheory.PGame} : P3 x₁ x₂ y₁ y₂ ↔ P3 (-x₂) (-x₁) y₁ y₂

theorem Surreal.Multiplication.P2_neg_left {x₁ x₂ y : SetTheory.PGame} : P2 x₁ x₂ y ↔ P2 (-x₂) (-x₁) y

theorem Surreal.Multiplication.P2_neg_right {x₁ x₂ y : SetTheory.PGame} : P2 x₁ x₂ y ↔ P2 x₁ x₂ (-y)

theorem Surreal.Multiplication.P4_neg_left {x₁ x₂ y : SetTheory.PGame} : P4 x₁ x₂ y ↔ P4 (-x₂) (-x₁) y

theorem Surreal.Multiplication.P4_neg_right {x₁ x₂ y : SetTheory.PGame} : P4 x₁ x₂ y ↔ P4 x₁ x₂ (-y)

theorem Surreal.Multiplication.P24_neg_left {x₁ x₂ y : SetTheory.PGame} : P24 x₁ x₂ y ↔ P24 (-x₂) (-x₁) y

theorem Surreal.Multiplication.P24_neg_right {x₁ x₂ y : SetTheory.PGame} : P24 x₁ x₂ y ↔ P24 x₁ x₂ (-y)

Explicit calculations necessary for the main proof

theorem Surreal.Multiplication.mulOption_lt_iff_P1 {x y : SetTheory.PGame} {i j : x.LeftMoves} {k : y.LeftMoves} {l : (-y).LeftMoves} : ⟦x.mulOption y i k⟧ < -⟦x.mulOption (-y) j l⟧ ↔ P1 (x.moveLeft i) x (x.moveLeft j) y (y.moveLeft k) (-(-y).moveLeft l)

theorem Surreal.Multiplication.mulOption_lt_mul_iff_P3 {x y : SetTheory.PGame} {i : x.LeftMoves} {j : y.LeftMoves} : ⟦x.mulOption y i j⟧ < ⟦x * y⟧ ↔ P3 (x.moveLeft i) x (y.moveLeft j) y

theorem Surreal.Multiplication.P1_of_eq {x₁ x₂ x₃ y₁ y₂ y₃ : SetTheory.PGame} (he : x₁ ≈ x₃) (h₁ : P2 x₁ x₃ y₁) (h₃ : P2 x₁ x₃ y₃) (h3 : P3 x₁ x₂ y₂ y₃) : P1 x₁ x₂ x₃ y₁ y₂ y₃

theorem Surreal.Multiplication.P1_of_lt {x₁ x₂ x₃ y₁ y₂ y₃ : SetTheory.PGame} (h₁ : P3 x₃ x₂ y₂ y₃) (h₂ : P3 x₁ x₃ y₂ y₁) : P1 x₁ x₂ x₃ y₁ y₂ y₃

inductive Surreal.Multiplication.Args : Type (u + 1)

The type of lists of arguments for P1, P2, and P4.

• P1 (x y : SetTheory.PGame) : Args
• P24 (x₁ x₂ y : SetTheory.PGame) : Args

def Surreal.Multiplication.Args.toMultiset : Args → Multiset SetTheory.PGame

The multiset associated to a list of arguments.

Equations

• (Surreal.Multiplication.Args.P1 x_1 y).toMultiset = {x_1, y}
• (Surreal.Multiplication.Args.P24 x₁ x₂ y).toMultiset = {x₁, x₂, y}

def Surreal.Multiplication.Args.Numeric (a : Args) : Prop

A list of arguments is numeric if all the arguments are.

Equations

• a.Numeric = ∀ x ∈ a.toMultiset, x.Numeric

theorem Surreal.Multiplication.Args.numeric_P1 {x y : SetTheory.PGame} : (P1 x y).Numeric ↔ x.Numeric ∧ y.Numeric

theorem Surreal.Multiplication.Args.numeric_P24 {x₁ x₂ y : SetTheory.PGame} : (P24 x₁ x₂ y).Numeric ↔ x₁.Numeric ∧ x₂.Numeric ∧ y.Numeric

def Surreal.Multiplication.ArgsRel : Args → Args → Prop

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

• Surreal.Multiplication.ArgsRel = InvImage (Relation.TransGen (Relation.CutExpand SetTheory.PGame.IsOption)) Surreal.Multiplication.Args.toMultiset

theorem Surreal.Multiplication.argsRel_wf : WellFounded ArgsRel

ArgsRel is well-founded.

def Surreal.Multiplication.P124 : Args → Prop

The statement that we will show by induction using the well-founded relation ArgsRel.

Equations

• Surreal.Multiplication.P124 (Surreal.Multiplication.Args.P1 x_1 y) = (x_1 * y).Numeric
• Surreal.Multiplication.P124 (Surreal.Multiplication.Args.P24 x₁ x₂ y) = Surreal.Multiplication.P24 x₁ x₂ y

theorem Surreal.Multiplication.ArgsRel.numeric_closed {a' a : Args} : ArgsRel a' a → a.Numeric → a'.Numeric

The property that all arguments are numeric is leftward-closed under ArgsRel.

def Surreal.Multiplication.IH1 (x y : SetTheory.PGame) : Prop

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'

Symmetry properties of IH1

theorem Surreal.Multiplication.ih1_neg_left {x y : SetTheory.PGame} : IH1 x y → IH1 (-x) y

theorem Surreal.Multiplication.ih1_neg_right {x y : SetTheory.PGame} : IH1 x y → IH1 x (-y)

Specialize ih to obtain specialized induction hypotheses for P1

theorem Surreal.Multiplication.numeric_option_mul {x x' y : SetTheory.PGame} (ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a) (h : x'.IsOption x) : (x' * y).Numeric

theorem Surreal.Multiplication.numeric_mul_option {x y y' : SetTheory.PGame} (ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a) (h : y'.IsOption y) : (x * y').Numeric

theorem Surreal.Multiplication.numeric_option_mul_option {x x' y y' : SetTheory.PGame} (ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a) (hx : x'.IsOption x) (hy : y'.IsOption y) : (x' * y').Numeric

theorem Surreal.Multiplication.ih1 {x y : SetTheory.PGame} (ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a) : IH1 x y

theorem Surreal.Multiplication.ih1_swap {x y : SetTheory.PGame} (ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a) : IH1 y x

theorem Surreal.Multiplication.P3_of_ih {x y : SetTheory.PGame} (hy : y.Numeric) (ihyx : IH1 y x) (i : x.LeftMoves) (k : y.LeftMoves) (l : (-y).LeftMoves) : P3 (x.moveLeft i) x (y.moveLeft k) (-(-y).moveLeft l)

theorem Surreal.Multiplication.P24_of_ih {x y : SetTheory.PGame} (ihxy : IH1 x y) (i j : x.LeftMoves) : P24 (x.moveLeft i) (x.moveLeft j) y

theorem Surreal.Multiplication.mulOption_lt_of_lt {x y : SetTheory.PGame} (hy : y.Numeric) (ihxy : IH1 x y) (ihyx : IH1 y x) (i j : x.LeftMoves) (k : y.LeftMoves) (l : (-y).LeftMoves) (h : x.moveLeft i < x.moveLeft j) : ⟦x.mulOption y i k⟧ < -⟦x.mulOption (-y) j l⟧

theorem Surreal.Multiplication.mulOption_lt {x y : SetTheory.PGame} (hx : x.Numeric) (hy : y.Numeric) (ihxy : IH1 x y) (ihyx : IH1 y x) (i j : x.LeftMoves) (k : y.LeftMoves) (l : (-y).LeftMoves) : ⟦x.mulOption y i k⟧ < -⟦x.mulOption (-y) j l⟧

theorem Surreal.Multiplication.P1_of_ih {x y : SetTheory.PGame} (ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a) (hx : x.Numeric) (hy : y.Numeric) : (x * y).Numeric

P1 follows from the induction hypothesis.

def Surreal.Multiplication.IH24 (x₁ x₂ y : SetTheory.PGame) : Prop

A specialized induction hypothesis used to prove P2 and P4.

Equations

• One or more equations did not get rendered due to their size.

def Surreal.Multiplication.IH4 (x₁ x₂ y : SetTheory.PGame) : Prop

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)

Specialize ih' to obtain specialized induction hypotheses for P2 and P4

theorem Surreal.Multiplication.ih₁₂ {x₁ x₂ y : SetTheory.PGame} (ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a) : IH24 x₁ x₂ y

theorem Surreal.Multiplication.ih₂₁ {x₁ x₂ y : SetTheory.PGame} (ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a) : IH24 x₂ x₁ y

theorem Surreal.Multiplication.ih4 {x₁ x₂ y : SetTheory.PGame} (ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a) : IH4 x₁ x₂ y

theorem Surreal.Multiplication.numeric_of_ih {x₁ x₂ y : SetTheory.PGame} (ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a) : (x₁ * y).Numeric ∧ (x₂ * y).Numeric

theorem Surreal.Multiplication.ih24_neg {x₁ x₂ y : SetTheory.PGame} : IH24 x₁ x₂ y → IH24 (-x₂) (-x₁) y ∧ IH24 x₁ x₂ (-y)

Symmetry properties of IH24.

theorem Surreal.Multiplication.ih4_neg {x₁ x₂ y : SetTheory.PGame} : IH4 x₁ x₂ y → IH4 (-x₂) (-x₁) y ∧ IH4 x₁ x₂ (-y)

Symmetry properties of IH4.

theorem Surreal.Multiplication.mulOption_lt_mul_of_equiv {x₁ x₂ y : SetTheory.PGame} (hn : x₁.Numeric) (h : IH24 x₁ x₂ y) (he : x₁ ≈ x₂) (i : x₁.LeftMoves) (j : y.LeftMoves) : ⟦x₁.mulOption y i j⟧ < ⟦x₂ * y⟧

theorem Surreal.Multiplication.mul_right_le_of_equiv {x₁ x₂ y : SetTheory.PGame} (h₁ : x₁.Numeric) (h₂ : x₂.Numeric) (h₁₂ : IH24 x₁ x₂ y) (h₂₁ : IH24 x₂ x₁ y) (he : x₁ ≈ x₂) : x₁ * y ≤ x₂ * y

P2 follows from specialized induction hypotheses (one half of the equality).

def Surreal.Multiplication.MulOptionsLTMul (x y : SetTheory.PGame) : Prop

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⟧

theorem Surreal.Multiplication.mulOptionsLTMul_of_numeric {x y : SetTheory.PGame} (hn : (x * y).Numeric) : (MulOptionsLTMul x y ∧ MulOptionsLTMul (-x) (-y)) ∧ MulOptionsLTMul x (-y) ∧ MulOptionsLTMul (-x) y

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.

def Surreal.Multiplication.IH3 (x₁ x' x₂ y₁ y₂ : SetTheory.PGame) : Prop

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.

theorem Surreal.Multiplication.ih3_of_ih {x₁ x₂ y : SetTheory.PGame} (h24 : IH24 x₁ x₂ y) (h4 : IH4 x₁ x₂ y) (hl : MulOptionsLTMul x₂ y) (i : x₂.LeftMoves) (j : y.LeftMoves) : IH3 x₁ (x₂.moveLeft i) x₂ (y.moveLeft j) y

theorem Surreal.Multiplication.P3_of_le_left {x₁ x₂ y₁ y₂ : SetTheory.PGame} (i : x₂.LeftMoves) (h : IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂) (hl : x₁ ≤ x₂.moveLeft i) : P3 x₁ x₂ y₁ y₂

theorem Surreal.Multiplication.P3_of_lt {x₁ x₂ y₁ y₂ : SetTheory.PGame} (h : ∀ (i : x₂.LeftMoves), IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂) (hs : ∀ (i : (-x₁).LeftMoves), IH3 (-x₂) ((-x₁).moveLeft i) (-x₁) y₁ y₂) (hl : x₁ < x₂) : P3 x₁ x₂ y₁ y₂

P3 follows from IH3 (so P4 (with y₁ a left option of y₂) follows from the induction hypothesis).

theorem Surreal.Multiplication.main (a : Args) : a.Numeric → P124 a

The main chunk of Theorem 8 in [Conway2001] / Theorem 3.8 in [SchleicherStoll].

theorem SetTheory.PGame.Numeric.mul {x y : PGame} (hx : x.Numeric) (hy : y.Numeric) : (x * y).Numeric

theorem SetTheory.PGame.P24 {x₁ x₂ y : PGame} (hx₁ : x₁.Numeric) (hx₂ : x₂.Numeric) (hy : y.Numeric) : Surreal.Multiplication.P24 x₁ x₂ y

theorem SetTheory.PGame.Equiv.mul_congr_left {x₁ x₂ y : PGame} (hx₁ : x₁.Numeric) (hx₂ : x₂.Numeric) (hy : y.Numeric) (he : x₁ ≈ x₂) : x₁ * y ≈ x₂ * y

theorem SetTheory.PGame.Equiv.mul_congr_right {x y₁ y₂ : PGame} (hx : x.Numeric) (hy₁ : y₁.Numeric) (hy₂ : y₂.Numeric) (he : y₁ ≈ y₂) : x * y₁ ≈ x * y₂

theorem SetTheory.PGame.Equiv.mul_congr {x₁ x₂ y₁ y₂ : PGame} (hx₁ : x₁.Numeric) (hx₂ : x₂.Numeric) (hy₁ : y₁.Numeric) (hy₂ : y₂.Numeric) (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) : x₁ * y₁ ≈ x₂ * y₂

theorem SetTheory.PGame.P3_of_lt_of_lt {x₁ x₂ y₁ y₂ : PGame} (hx₁ : x₁.Numeric) (hx₂ : x₂.Numeric) (hy₁ : y₁.Numeric) (hy₂ : y₂.Numeric) (hx : x₁ < x₂) (hy : y₁ < y₂) : Surreal.Multiplication.P3 x₁ x₂ y₁ y₂

One additional inductive argument that supplies the last missing part of Theorem 8.

theorem SetTheory.PGame.Numeric.mul_pos {x₁ x₂ : PGame} (hx₁ : x₁.Numeric) (hx₂ : x₂.Numeric) (hp₁ : 0 < x₁) (hp₂ : 0 < x₂) : 0 < x₁ * x₂

noncomputable instance Surreal.instLinearOrderedCommRing : LinearOrderedCommRing Surreal

Equations

• Surreal.instLinearOrderedCommRing = LinearOrderedCommRing.mk Surreal.instLinearOrderedCommRing.proof_37