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 PGame 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.leftMoves, and x₁ * b + x₂ * y < x₁ * y + x₂ * b when b ∈ y.rightMoves.

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).leftMoves → b ∈ (x * y).rightMoves → 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.rightMoves as -a ∈ (-x).leftMoves. 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

def Surreal.Multiplication.P1 (x y a b c d : IGame) : Prop

P1 x y a b c d means that mulOption x y a b < mulOption x y c d. This is the general form of the statements needed to prove that x * y is numeric.

Equations

• Surreal.Multiplication.P1 x y a b c d = (Game.mk (IGame.mulOption x y a b) < Game.mk (IGame.mulOption x y c d))

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

P2 x₁ x₂ y states that if x₁ ≈ x₂, then x₁ * y ≈ x₂ * y. The RHS is stated in terms of Game.mk for rewriting convenience.

Equations

• Surreal.Multiplication.P2 x₁ x₂ y = (x₁ ≈ x₂ → Game.mk (x₁ * y) = Game.mk (x₂ * y))

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

P3 x₁ x₂ y₁ y₂ states that x₁ * y₂ + x₂ * y₁ < x₁ * y₁ + x₂ * y₂. Using distributivity, this is equivalent to (x₁ - x₂) * (y₁ - y₂) > 0.

Equations

• Surreal.Multiplication.P3 x₁ x₂ y₁ y₂ = (Game.mk (x₁ * y₂) + Game.mk (x₂ * y₁) < Game.mk (x₁ * y₁) + Game.mk (x₂ * y₂))

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

P4 x₁ x₂ y states that if x₁ < x₂, then P3 x₁ x₂ a y when a ∈ y.leftMoves, and P3 x₁ x₂ b y when b ∈ y.rightMoves.

Note that we instead write this second part as P3 x₁ x₂ b (-y) when b ∈ (-y).leftMoves. See the module docstring for an explanation.

Equations

• Surreal.Multiplication.P4 x₁ x₂ y = (x₁ < x₂ → (∀ a ∈ y.leftMoves, Surreal.Multiplication.P3 x₁ x₂ a y) ∧ ∀ b ∈ (-y).leftMoves, Surreal.Multiplication.P3 x₁ x₂ b (-y))

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

The conjunction of P2 and P4. Both statements have the same amount of arguments and satisfy similar symmetry properties, so we can slightly simplify the argument by merging them.

Equations

• Surreal.Multiplication.P24 x₁ x₂ y = (Surreal.Multiplication.P2 x₁ x₂ y ∧ Surreal.Multiplication.P4 x₁ x₂ y)

Symmetry properties of P1 – P4

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

theorem Surreal.Multiplication.P3.trans {x₁ x₂ x₃ y₁ y₂ : IGame} (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₂ : IGame} : P3 (-x₂) (-x₁) y₁ y₂ ↔ P3 x₁ x₂ y₁ y₂

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

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

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

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

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

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

Inductive setup

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

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

• P1 (x y : IGame) : Args
• P24 (x₁ x₂ y : IGame) : Args

def Surreal.Multiplication.Args.toMultiset : Args → Multiset IGame

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}

@[simp]

theorem Surreal.Multiplication.Args.toMultiset_P1 {x y : IGame} : (P1 x y).toMultiset = {x, y}

@[simp]

theorem Surreal.Multiplication.Args.toMultiset_P24 {x₁ x₂ y : IGame} : (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 : IGame} : (P1 x y).Numeric ↔ x.Numeric ∧ y.Numeric

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

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

The well-founded relation specifying when a list of game 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 game from a₂ and adding back one or two options of the game.

See also WellFounded.CutExpand.

Equations

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

theorem Surreal.Multiplication.argsRel_wf : WellFounded ArgsRel

ArgsRel is well-founded.

instance Surreal.Multiplication.instIsWellFoundedArgsArgsRel : IsWellFounded Args ArgsRel

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.P124 : Args → Prop

The statement that we will show by induction for all Numeric args, using the well-founded relation ArgsRel.

The inductive hypothesis in the proof will be ∀ a', ArgsRel a' a → P124 a.

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

P1 follows from the inductive hypothesis

theorem Surreal.Multiplication.numeric_isOption_mul_of_IH {x x' y : IGame} (IH : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a) (h : x'.IsOption x) : (x' * y).Numeric

theorem Surreal.Multiplication.numeric_mul_isOption_of_IH {x y y' : IGame} (IH : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a) (h : y'.IsOption y) : (x * y').Numeric

theorem Surreal.Multiplication.numeric_isOption_mul_isOption_of_IH {x x' y y' : IGame} (IH : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a) (hx : x'.IsOption x) (hy : y'.IsOption y) : (x' * y').Numeric

def Surreal.Multiplication.IH1 (x y : IGame) : Prop

A specialization of the inductive hypothesis used to prove P1.

Equations

• Surreal.Multiplication.IH1 x y = ∀ ⦃x₁ x₂ y' : IGame⦄, x₁.IsOption x → x₂.IsOption x → y' = y ∨ y'.IsOption y → Surreal.Multiplication.P24 x₁ x₂ y'

theorem Surreal.Multiplication.IH1_of_IH {x y : IGame} (IH : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a) : IH1 x y

IH1 x y follows from the inductive hypothesis for P1 x y.

theorem Surreal.Multiplication.IH1_swap_of_IH {x y : IGame} (IH : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a) : IH1 y x

IH1 y x follows from the inductive hypothesis for P1 x y.

theorem Surreal.Multiplication.IH1_neg_left {x y : IGame} : IH1 x y → IH1 (-x) y

theorem Surreal.Multiplication.IH1_neg_right {x y : IGame} : IH1 x y → IH1 x (-y)

theorem Surreal.Multiplication.P1_of_P3 {x₁ x₂ x₃ y₁ y₂ y₃ : IGame} (h₁ : P3 x₃ x₂ y₂ y₃) (h₂ : P3 x₁ x₃ y₂ y₁) : P1 x₂ y₁ x₁ y₂ x₃ y₃

theorem Surreal.Multiplication.P3_of_IH1 {x y a b d : IGame} [y.Numeric] (ihyx : IH1 y x) (ha : a ∈ x.leftMoves) (hb : b ∈ y.leftMoves) (hd : d ∈ (-y).leftMoves) : P3 a x b (-d)

theorem Surreal.Multiplication.P24_of_IH1 {x y a b : IGame} (ihxy : IH1 x y) (ha : a ∈ x.leftMoves) (hb : b ∈ x.leftMoves) : P24 a b y

theorem Surreal.Multiplication.mulOption_lt_iff_P1 {x y a b c d : IGame} : Game.mk (IGame.mulOption x y a b) < -Game.mk (IGame.mulOption x (-y) c d) ↔ P1 x y a b c (-d)

theorem Surreal.Multiplication.mulOption_lt_of_lt {x y : IGame} [y.Numeric] (ihxy : IH1 x y) (ihyx : IH1 y x) {a b c d : IGame} (h : a < c) (ha : a ∈ x.leftMoves) (hb : b ∈ y.leftMoves) (hc : c ∈ x.leftMoves) (hd : d ∈ (-y).leftMoves) : Game.mk (IGame.mulOption x y a b) < -Game.mk (IGame.mulOption x (-y) c d)

theorem Surreal.Multiplication.mulOption_lt {x y : IGame} [x.Numeric] [y.Numeric] (ihxy : IH1 x y) (ihyx : IH1 y x) {a b c d : IGame} (ha : a ∈ x.leftMoves) (hb : b ∈ y.leftMoves) (hc : c ∈ x.leftMoves) (hd : d ∈ (-y).leftMoves) : Game.mk (IGame.mulOption x y a b) < -Game.mk (IGame.mulOption x (-y) c d)

theorem Surreal.Multiplication.P1_of_IH {x y : IGame} (IH : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a) [x.Numeric] [y.Numeric] : (x * y).Numeric

P1 follows from the induction hypothesis.

P2 follows from the inductive hypothesis

theorem Surreal.Multiplication.numeric_of_IH {x₁ x₂ y : IGame} (IH : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a) : (x₁ * y).Numeric ∧ (x₂ * y).Numeric

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

A specialization of the inductive 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 : IGame) : Prop

A specialization of the induction hypothesis used to prove P4.

Equations

• Surreal.Multiplication.IH4 x₁ x₂ y = ∀ ⦃z w : IGame⦄, w.IsOption y → (z.IsOption x₁ → Surreal.Multiplication.P2 z x₂ w) ∧ (z.IsOption x₂ → Surreal.Multiplication.P2 x₁ z w)

theorem Surreal.Multiplication.IH24_of_IH {x₁ x₂ y : IGame} (IH : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a) : IH24 x₁ x₂ y

IH24 x₁ x₂ y follows from the inductive hypothesis for P24 x₁ x₂ y.

theorem Surreal.Multiplication.IH24_swap_of_IH {x₁ x₂ y : IGame} (IH : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a) : IH24 x₂ x₁ y

IH24 x₂ x₁ y follows from the inductive hypothesis for P24 x₁ x₂ y.

theorem Surreal.Multiplication.IH4_of_IH {x₁ x₂ y : IGame} (IH : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a) : IH4 x₁ x₂ y

IH4 x₁ x₂ y follows from the inductive hypothesis for P24 x₁ x₂ y.

theorem Surreal.Multiplication.IH24_neg {x₁ x₂ y : IGame} : IH24 x₁ x₂ y → IH24 (-x₂) (-x₁) y ∧ IH24 x₁ x₂ (-y)

theorem Surreal.Multiplication.IH4_neg {x₁ x₂ y : IGame} : IH4 x₁ x₂ y → IH4 (-x₂) (-x₁) y ∧ IH4 x₁ x₂ (-y)

P4 follows from the inductive hypothesis

theorem Surreal.Multiplication.mulOption_lt_mul_iff_P3 {x y a b : IGame} : IGame.mulOption x y a b < x * y ↔ P3 a x b y

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

A specialization of the induction hypothesis used to prove P3.

Equations

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

theorem Surreal.Multiplication.IH3_of_IH {x₁ x₂ y a b : IGame} (ih24 : IH24 x₁ x₂ y) (ih4 : IH4 x₁ x₂ y) (hi : a ∈ x₂.leftMoves) (hb : b ∈ y.leftMoves) (hl : IGame.mulOption x₂ y a b < x₂ * y) : IH3 x₁ a x₂ b y

IH3 follows from the induction hypothesis for P24 x₁ x₂ y.

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

theorem Surreal.Multiplication.P3_of_IH3 {x₁ x₂ y₁ y₂ : IGame} (h : ∀ i ∈ x₂.leftMoves, IH3 x₁ i x₂ y₁ y₂) (hs : ∀ i ∈ (-x₁).leftMoves, IH3 (-x₂) 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.P4_of_IH {x₁ x₂ y : IGame} (IH : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a) : P4 x₁ x₂ y

P4 follows from the induction hypothesis.

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

We tie everything together to complete the induction.

theorem Surreal.Multiplication.main_P24 (x₁ x₂ y : IGame) [hx₁ : x₁.Numeric] [hx₂ : x₂.Numeric] [hy : y.Numeric] : P24 x₁ x₂ y

@[irreducible]

theorem Surreal.Multiplication.P3_of_lt_of_lt {x₁ x₂ y₁ y₂ : IGame} [x₁.Numeric] [x₂.Numeric] [y₁.Numeric] [y₂.Numeric] (hx : x₁ < x₂) (hy : y₁ < y₂) : P3 x₁ x₂ y₁ y₂

One additional inductive argument proves P3.

Instances and corollaries

instance IGame.Numeric.mul (x y : IGame) [hx : x.Numeric] [hy : y.Numeric] : (x * y).Numeric

instance IGame.Numeric.mulOption (x y a b : IGame) [x.Numeric] [y.Numeric] [a.Numeric] [b.Numeric] : (mulOption x y a b).Numeric

theorem IGame.Numeric.mul_pos {x₁ x₂ : IGame} [x₁.Numeric] [x₂.Numeric] (hp₁ : 0 < x₁) (hp₂ : 0 < x₂) : 0 < x₁ * x₂

noncomputable instance Surreal.instCommRing : CommRing Surreal

Equations

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

instance Surreal.instIsStrictOrderedRing : IsStrictOrderedRing Surreal

@[simp]

theorem Surreal.mk_mul (x y : IGame) [x.Numeric] [y.Numeric] : mk (x * y) = mk x * mk y

theorem IGame.Numeric.mul_neg_of_pos_of_neg {x y : IGame} [x.Numeric] [y.Numeric] (hx : 0 < x) (hy : y < 0) : x * y < 0

theorem IGame.Numeric.mul_neg_of_neg_of_pos {x y : IGame} [x.Numeric] [y.Numeric] (hx : x < 0) (hy : 0 < y) : x * y < 0

theorem IGame.Numeric.mul_pos_of_neg_of_neg {x y : IGame} [x.Numeric] [y.Numeric] (hx : x < 0) (hy : y < 0) : 0 < x * y

theorem IGame.Numeric.mul_nonneg {x y : IGame} [x.Numeric] [y.Numeric] (hx : 0 ≤ x) (hy : 0 ≤ y) : 0 ≤ x * y

theorem IGame.Numeric.mul_nonpos_of_nonneg_of_nonpos {x y : IGame} [x.Numeric] [y.Numeric] (hx : 0 ≤ x) (hy : y ≤ 0) : x * y ≤ 0

theorem IGame.Numeric.mul_nonpos_of_nonpos_of_nonneg {x y : IGame} [x.Numeric] [y.Numeric] (hx : x ≤ 0) (hy : 0 ≤ y) : x * y ≤ 0

theorem IGame.Numeric.mul_nonneg_of_nonpos_of_nonpos {x y : IGame} [x.Numeric] [y.Numeric] (hx : x ≤ 0) (hy : y ≤ 0) : 0 ≤ x * y

@[simp]

theorem IGame.Numeric.mul_le_mul_left {x y z : IGame} [x.Numeric] [y.Numeric] [z.Numeric] (hx : 0 < x) : x * y ≤ x * z ↔ y ≤ z

@[simp]

theorem IGame.Numeric.mul_le_mul_right {x y z : IGame} [x.Numeric] [y.Numeric] [z.Numeric] (hx : 0 < x) : y * x ≤ z * x ↔ y ≤ z

@[simp]

theorem IGame.Numeric.mul_lt_mul_left {x y z : IGame} [x.Numeric] [y.Numeric] [z.Numeric] (hx : 0 < x) : x * y < x * z ↔ y < z

@[simp]

theorem IGame.Numeric.mul_lt_mul_right {x y z : IGame} [x.Numeric] [y.Numeric] [z.Numeric] (hx : 0 < x) : y * x < z * x ↔ y < z

@[simp]

theorem IGame.Numeric.mul_le_mul_left_of_neg {x y z : IGame} [x.Numeric] [y.Numeric] [z.Numeric] (hz : z < 0) : z * x ≤ z * y ↔ y ≤ x

@[simp]

theorem IGame.Numeric.mul_le_mul_right_of_neg {x y z : IGame} [x.Numeric] [y.Numeric] [z.Numeric] (hz : z < 0) : x * z ≤ y * z ↔ y ≤ x

@[simp]

theorem IGame.Numeric.mul_lt_mul_left_of_neg {x y z : IGame} [x.Numeric] [y.Numeric] [z.Numeric] (hz : z < 0) : z * x < z * y ↔ y < x

@[simp]

theorem IGame.Numeric.mul_lt_mul_right_of_neg {x y z : IGame} [x.Numeric] [y.Numeric] [z.Numeric] (hz : z < 0) : x * z < y * z ↔ y < x

theorem IGame.Numeric.mul_equiv_zero {x y : IGame} [x.Numeric] [y.Numeric] : x * y ≈ 0 ↔ x ≈ 0 ∨ y ≈ 0