Surreal numbers

The basic theory of surreal numbers, built on top of the theory of combinatorial (pre-)games.

A pregame is Numeric if all the Left options are strictly smaller than all the Right options, and all those options are themselves numeric. In terms of combinatorial games, the numeric games have "frozen"; you can only make your position worse by playing, and Left is some definite "number" of moves ahead (or behind) Right.

A surreal number is an equivalence class of numeric games.

Surreal numbers inherit the relations ≤ and < from games, and these relations satisfy the axioms of a linear order. In fact, the surreals form a complete ordered field, containing a copy of the reals, and much else besides!

Algebraic operations

In this file, we show that the surreals form a linear ordered commutative group.

In CombinatorialGames.Surreal.Multiplication, we define multiplication and show that the surreals form a linear ordered commutative ring. In CombinatorialGames.Surreal.Division we further show the surreals are a field.

Numeric games

class IGame.Numeric (x : IGame) : Prop

A game !{s | t} is numeric if everything in s is less than everything in t, and all the elements of these sets are also numeric.

The Surreal numbers are built as the quotient of numeric games under equivalence.

• of_NumericAux :: (
• out : IGame.NumericAux✝ x
• )

theorem IGame.numeric_iff_aux (x : IGame) : x.Numeric ↔ IGame.NumericAux✝ x

theorem IGame.numeric_def {x : IGame} : x.Numeric ↔ (∀ y ∈ moves left x, ∀ z ∈ moves right x, y < z) ∧ ∀ (p : Player), ∀ y ∈ moves p x, y.Numeric

theorem IGame.Numeric.mk {x : IGame} (h₁ : ∀ y ∈ moves left x, ∀ z ∈ moves right x, y < z) (h₂ : ∀ (p : Player), ∀ y ∈ moves p x, y.Numeric) : x.Numeric

theorem IGame.Numeric.left_lt_right {x y z : IGame} [h : x.Numeric] (hy : y ∈ moves left x) (hz : z ∈ moves right x) : y < z

theorem IGame.Numeric.of_mem_moves {x y : IGame} {p : Player} [h : x.Numeric] (hy : y ∈ moves p x) : y.Numeric

def IGame.Numeric.tacticNumeric : Lean.ParserDescr

numeric eagerly adds all possible Numeric hypotheses.

Equations

• IGame.Numeric.tacticNumeric = Lean.ParserDescr.node `IGame.Numeric.tacticNumeric 1024 (Lean.ParserDescr.nonReservedSymbol "numeric" false)

theorem IGame.Numeric.isOption {x y : IGame} [x.Numeric] (h : y.IsOption x) : y.Numeric

theorem IGame.IsOption.numeric {x y : IGame} [x.Numeric] (h : y.IsOption x) : y.Numeric

Alias of IGame.Numeric.isOption.

@[simp]

instance IGame.Numeric.zero : Numeric 0

@[simp]

instance IGame.Numeric.one : Numeric 1

@[simp]

instance IGame.Numeric.half : ½.Numeric

instance IGame.Numeric.subtype (x : Subtype Numeric) : (↑x).Numeric

instance IGame.Numeric.moves {x : IGame} [x.Numeric] {p : Player} (y : ↑(moves p x)) : (↑y).Numeric

@[irreducible]

theorem IGame.Numeric.le_of_not_le {x y : IGame} [x.Numeric] [y.Numeric] : ¬x ≤ y → y ≤ x

theorem IGame.Numeric.le_total (x y : IGame) [x.Numeric] [y.Numeric] : x ≤ y ∨ y ≤ x

theorem IGame.Numeric.lt_of_not_ge {x y : IGame} [x.Numeric] [y.Numeric] (h : ¬x ≤ y) : y < x

@[simp]

theorem IGame.Numeric.not_le {x y : IGame} [x.Numeric] [y.Numeric] : ¬x ≤ y ↔ y < x

@[simp]

theorem IGame.Numeric.not_lt {x y : IGame} [x.Numeric] [y.Numeric] : ¬x < y ↔ y ≤ x

theorem IGame.Numeric.le_or_gt (x y : IGame) [x.Numeric] [y.Numeric] : x ≤ y ∨ y < x

theorem IGame.Numeric.lt_or_ge (x y : IGame) [x.Numeric] [y.Numeric] : x < y ∨ y ≤ x

theorem IGame.Numeric.not_fuzzy (x y : IGame) [x.Numeric] [y.Numeric] : ¬x ‖ y

theorem IGame.Numeric.lt_or_equiv_or_gt (x y : IGame) [x.Numeric] [y.Numeric] : x < y ∨ x ≈ y ∨ y < x

theorem IGame.Numeric.mk_of_lf {x : IGame} (h₁ : ∀ y ∈ moves left x, ∀ z ∈ moves right x, ¬z ≤ y) (h₂ : ∀ (p : Player), ∀ y ∈ moves p x, y.Numeric) : x.Numeric

To prove a game is numeric, it suffices to show the left options are less or fuzzy to the right options.

theorem IGame.Numeric.le_iff_forall_lt {x y : IGame} [x.Numeric] [y.Numeric] : x ≤ y ↔ (∀ z ∈ moves left x, z < y) ∧ ∀ z ∈ moves right y, x < z

theorem IGame.Numeric.lt_iff_exists_le {x y : IGame} [x.Numeric] [y.Numeric] : x < y ↔ (∃ z ∈ moves left y, x ≤ z) ∨ ∃ z ∈ moves right x, z ≤ y

theorem IGame.Numeric.left_lt {x y : IGame} [x.Numeric] (h : y ∈ moves left x) : y < x

theorem IGame.Numeric.lt_right {x y : IGame} [x.Numeric] (h : y ∈ moves right x) : x < y

@[irreducible]

instance IGame.Numeric.neg (x : IGame) [x.Numeric] : (-x).Numeric

@[simp]

theorem IGame.Numeric.neg_iff {x : IGame} : (-x).Numeric ↔ x.Numeric

@[irreducible]

instance IGame.Numeric.add (x y : IGame) [x.Numeric] [y.Numeric] : (x + y).Numeric

instance IGame.Numeric.sub (x y : IGame) [x.Numeric] [y.Numeric] : (x - y).Numeric

instance IGame.Numeric.natCast (n : ℕ) : (↑n).Numeric

instance IGame.Numeric.ofNat (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).Numeric

instance IGame.Numeric.intCast (n : ℤ) : (↑n).Numeric

Simplicity theorem

def IGame.Fits (x y : IGame) : Prop

x fits within y when z ⧏ x for every z ∈ yᴸ, and x ⧏ z for every z ∈ yᴿ.

The simplicity theorem states that if a game fits a numeric game, but none of its options do, then the games are equivalent. In particular, a numeric game is equivalent to the game of the least birthday that fits in it

Equations

• x.Fits y = ((∀ z ∈ IGame.moves Player.left y, ¬x ≤ z) ∧ ∀ z ∈ IGame.moves Player.right y, ¬z ≤ x)

theorem IGame.fits_of_equiv {x y : IGame} (h : x ≈ y) : x.Fits y

theorem IGame.AntisymmRel.Fits {x y : IGame} (h : x ≈ y) : x.Fits y

Alias of IGame.fits_of_equiv.

theorem IGame.Fits.refl (x : IGame) : x.Fits x

instance IGame.instIsReflFits : IsRefl IGame Fits

theorem IGame.Fits.antisymm {x y : IGame} (h₁ : x.Fits y) (h₂ : y.Fits x) : x ≈ y

@[simp]

theorem IGame.fits_neg_iff {x y : IGame} : (-x).Fits (-y) ↔ x.Fits y

theorem IGame.Fits.neg {x y : IGame} : x.Fits y → (-x).Fits (-y)

Alias of the reverse direction of IGame.fits_neg_iff.

theorem IGame.not_fits_iff {x y : IGame} : ¬x.Fits y ↔ (∃ z ∈ moves left y, x ≤ z) ∨ ∃ z ∈ moves right y, z ≤ x

theorem IGame.Fits.le_of_forall_leftMoves_not_fits {x y : IGame} [x.Numeric] (hx : x.Fits y) (hl : ∀ z ∈ moves left x, ¬z.Fits y) : x ≤ y

theorem IGame.Fits.le_of_forall_rightMoves_not_fits {x y : IGame} [x.Numeric] (hx : x.Fits y) (hr : ∀ z ∈ moves right x, ¬z.Fits y) : y ≤ x

theorem IGame.Fits.equiv_of_forall_not_fits {x y : IGame} [x.Numeric] (hx : x.Fits y) (hl : ∀ z ∈ moves left x, ¬z.Fits y) (hr : ∀ z ∈ moves right x, ¬z.Fits y) : x ≈ y

A variant of the simplicity theorem: if a numeric game x fits within a game y, but none of its options do, then x ≈ y.

theorem IGame.Fits.equiv_of_forall_birthday_le {x y : IGame} [x.Numeric] (hx : x.Fits y) (H : ∀ (z : IGame), z.Numeric → z.Fits y → x.birthday ≤ z.birthday) : x ≈ y

A variant of the simplicity theorem: if x is the numeric game with the least birthday that fits within y, then x ≈ y.

@[simp]

theorem IGame.fits_zero_iff_equiv {x : IGame} : Fits 0 x ↔ x ≈ 0

A specialization of the simplicity theorem to 0.

theorem IGame.equiv_one_of_fits {x : IGame} (hx : Fits 1 x) (h : ¬x ≈ 0) : x ≈ 1

A specialization of the simplicity theorem to 1.

Surreal numbers

def Surreal : Type (u + 1)

The type of surreal numbers. These are the numeric games quotiented by the antisymmetrization relation x ≈ y ↔ x ≤ y ∧ y ≤ x. In the quotient, the order becomes a total order.

Equations

• Surreal = Antisymmetrization (Subtype IGame.Numeric) fun (x1 x2 : Subtype IGame.Numeric) => x1 ≤ x2

def Surreal.mk (x : IGame) [h : x.Numeric] : Surreal

The quotient map from the subtype of numeric IGames into Game.

Equations

• Surreal.mk x = ⟦⟨x, h⟩⟧

theorem Surreal.mk_eq_mk {x y : IGame} [x.Numeric] [y.Numeric] : mk x = mk y ↔ x ≈ y

theorem Surreal.mk_eq {x y : IGame} [x.Numeric] [y.Numeric] : x ≈ y → mk x = mk y

Alias of the reverse direction of Surreal.mk_eq_mk.

theorem Surreal.ind {motive : Surreal → Prop} (mk : ∀ (y : IGame) [inst : y.Numeric], motive (mk y)) (x : Surreal) : motive x

def Surreal.out (x : Surreal) : IGame

Choose an element of the equivalence class using the axiom of choice.

Equations

• x.out = ↑(Quotient.out x)

@[simp]

instance Surreal.instNumericOut (x : Surreal) : x.out.Numeric

@[simp]

theorem Surreal.out_eq (x : Surreal) : mk x.out = x

theorem Surreal.mk_out_equiv (x : IGame) [h : x.Numeric] : (mk x).out ≈ x

theorem Surreal.equiv_mk_out (x : IGame) [x.Numeric] : x ≈ (mk x).out

instance Surreal.instZero : Zero Surreal

Equations

• Surreal.instZero = { zero := Surreal.mk 0 }

instance Surreal.instOne : One Surreal

Equations

• Surreal.instOne = { one := Surreal.mk 1 }

instance Surreal.instInhabited : Inhabited Surreal

Equations

• Surreal.instInhabited = { default := 0 }

instance Surreal.instAdd : Add Surreal

Equations

• Surreal.instAdd = { add := Quotient.map₂ (fun (a b : Subtype IGame.Numeric) => ⟨↑a + ↑b, ⋯⟩) Surreal.instAdd._proof_2 }

instance Surreal.instNeg : Neg Surreal

Equations

• Surreal.instNeg = { neg := Quotient.map (fun (a : Subtype IGame.Numeric) => ⟨-↑a, ⋯⟩) Surreal.instNeg._proof_2 }

instance Surreal.instPartialOrder : PartialOrder Surreal

Equations

• Surreal.instPartialOrder = inferInstanceAs (PartialOrder (Antisymmetrization (Subtype IGame.Numeric) fun (x1 x2 : Subtype IGame.Numeric) => x1 ≤ x2))

instance Surreal.instLinearOrder : LinearOrder Surreal

Equations

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

instance Surreal.instAddCommGroup : AddCommGroup Surreal

Equations

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

instance Surreal.instAddGroupWithOne : AddGroupWithOne Surreal

Equations

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

instance Surreal.instIsOrderedAddMonoid : IsOrderedAddMonoid Surreal

@[simp]

theorem Surreal.mk_zero : mk 0 = 0

@[simp]

theorem Surreal.mk_one : mk 1 = 1

@[simp]

theorem Surreal.mk_add (x y : IGame) [x.Numeric] [y.Numeric] : mk (x + y) = mk x + mk y

@[simp]

theorem Surreal.mk_neg (x : IGame) [x.Numeric] : mk (-x) = -mk x

@[simp]

theorem Surreal.mk_sub (x y : IGame) [x.Numeric] [y.Numeric] : mk (x - y) = mk x - mk y

@[simp]

theorem Surreal.mk_le_mk {x y : IGame} [x.Numeric] [y.Numeric] : mk x ≤ mk y ↔ x ≤ y

@[simp]

theorem Surreal.mk_lt_mk {x y : IGame} [x.Numeric] [y.Numeric] : mk x < mk y ↔ x < y

@[simp]

theorem Surreal.mk_natCast (n : ℕ) : mk ↑n = ↑n

@[simp]

theorem Surreal.mk_intCast (n : ℤ) : mk ↑n = ↑n

instance Surreal.instZeroLEOneClass : ZeroLEOneClass Surreal

instance Surreal.instNeZeroOfNat : NeZero 1

instance Surreal.instNontrivial : Nontrivial Surreal

def Surreal.toGame : Surreal ↪o Game

Casts a Surreal number into a Game.

Equations

• Surreal.toGame = { toFun := Quotient.lift (fun (x : Subtype IGame.Numeric) => Game.mk ↑x) Surreal.toGame._proof_1, inj' := Surreal.toGame._proof_2, map_rel_iff' := @Surreal.toGame._proof_3 }

@[simp]

theorem Surreal.toGame_mk (x : IGame) [x.Numeric] : toGame (mk x) = Game.mk x

@[simp]

theorem Surreal.toGame_zero : toGame 0 = 0

@[simp]

theorem Surreal.toGame_one : toGame 1 = 1

theorem Surreal.toGame_le_iff {a b : Surreal} : toGame a ≤ toGame b ↔ a ≤ b

theorem Surreal.toGame_lt_iff {a b : Surreal} : toGame a < toGame b ↔ a < b

theorem Surreal.toGame_inj {a b : Surreal} : toGame a = toGame b ↔ a = b

def Surreal.toGameAddHom : Surreal →+o Game

Surreal.toGame as an OrderAddMonoidHom

Equations

• Surreal.toGameAddHom = { toFun := ⇑Surreal.toGame, map_zero' := Surreal.toGameAddHom._proof_1, map_add' := Surreal.toGameAddHom._proof_2, monotone' := Surreal.toGameAddHom._proof_3 }

@[simp]

theorem Surreal.toGameAddHom_apply (a : Surreal) : toGameAddHom a = toGame a

@[simp]

theorem Surreal.toGame_add (x y : Surreal) : toGame (x + y) = toGame x + toGame y

@[simp]

theorem Surreal.toGame_neg (x : Surreal) : toGame (-x) = -toGame x

@[simp]

theorem Surreal.toGame_sub (x y : Surreal) : toGame (x - y) = toGame x - toGame y

@[simp]

theorem Surreal.toGame_natCast (n : ℕ) : toGame ↑n = ↑n

@[simp]

theorem Surreal.toGame_intCast (n : ℤ) : toGame ↑n = ↑n

@[simp]

theorem Surreal.game_out_eq (x : Surreal) : Game.mk x.out = toGame x

instance Surreal.instOfSetsForallForallMemSetLeftForallForallRightLt : OfSets Surreal fun (st : Player → Set Surreal) => ∀ x ∈ st Player.left, ∀ y ∈ st Player.right, x < y

Construct a Surreal from its left and right sets, and a proof that all elements from the left set are less than all the elements of the right set.

Note that although this function is well-defined, this function isn't injective, nor do equivalence classes in Surreal have a canonical representative. (Note however that every short numeric game has a unique "canonical" form!)

Equations

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

theorem Surreal.toGame_ofSets' (st : Player → Set Surreal) [Small.{u, u + 1} ↑(st Player.left)] [Small.{u, u + 1} ↑(st Player.right)] {H : ∀ x ∈ st Player.left, ∀ y ∈ st Player.right, x < y} : toGame !{st} = !{fun (p : Player) => ⇑toGame '' st p}

@[simp]

theorem Surreal.toGame_ofSets (s t : Set Surreal) [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] {H : ∀ x ∈ s, ∀ y ∈ t, x < y} : toGame !{s | t} = !{⇑toGame '' s | ⇑toGame '' t}

theorem Surreal.mk_ofSets' {st : Player → Set IGame} [Small.{u, u + 1} ↑(st Player.left)] [Small.{u, u + 1} ↑(st Player.right)] {H : !{st}.Numeric} : mk !{st} = !{fun (p : Player) => Set.range fun (x : ↑(st p)) => mk ↑x}

theorem Surreal.mk_ofSets {s t : Set IGame} [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] {H : !{s | t}.Numeric} : mk !{s | t} = !{Set.range fun (x : ↑s) => mk ↑x | Set.range fun (x : ↑t) => mk ↑x}

theorem Surreal.lt_ofSets_of_mem_left {s t : Set Surreal} [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] {H : ∀ x ∈ s, ∀ y ∈ t, x < y} {x : Surreal} (hx : x ∈ s) : x < !{s | t}

theorem Surreal.ofSets_lt_of_mem_right {s t : Set Surreal} [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] {H : ∀ x ∈ s, ∀ y ∈ t, x < y} {x : Surreal} (hx : x ∈ t) : !{s | t} < x

theorem Surreal.zero_def : 0 = !{fun (x : Player) => ∅}

theorem Surreal.one_def : 1 = !{{0} | ∅}

instance Surreal.instDenselyOrdered : DenselyOrdered Surreal