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.

TODO

• Prove that surreals with finite birthday are dyadic rationals.
• Build the embedding from reals into surreals.
• Define sign sequences.

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.

• 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 ∈ x.leftMoves, ∀ z ∈ x.rightMoves, y < z) ∧ (∀ y ∈ x.leftMoves, y.Numeric) ∧ ∀ y ∈ x.rightMoves, y.Numeric

theorem IGame.Numeric.mk' {x : IGame} (h₁ : ∀ y ∈ x.leftMoves, ∀ z ∈ x.rightMoves, y < z) (h₂ : ∀ y ∈ x.leftMoves, y.Numeric) (h₃ : ∀ y ∈ x.rightMoves, y.Numeric) : x.Numeric

theorem IGame.Numeric.leftMove_lt_rightMove {x y z : IGame} [h : x.Numeric] (hy : y ∈ x.leftMoves) (hz : z ∈ x.rightMoves) : y < z

theorem IGame.Numeric.of_mem_leftMoves {x y : IGame} [h : x.Numeric] (hy : y ∈ x.leftMoves) : y.Numeric

theorem IGame.Numeric.of_mem_rightMoves {x y : IGame} [h : x.Numeric] (hy : y ∈ x.rightMoves) : y.Numeric

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

instance IGame.Numeric.subtype (x : Subtype Numeric) : (↑x).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_le {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_lt (x y : IGame) [x.Numeric] [y.Numeric] : x ≤ y ∨ y < x

theorem IGame.Numeric.lt_or_le (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 ∈ x.leftMoves, ∀ z ∈ x.rightMoves, ¬z ≤ y) (h₂ : ∀ y ∈ x.leftMoves, y.Numeric) (h₃ : ∀ y ∈ x.rightMoves, 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 ∈ x.leftMoves, z < y) ∧ ∀ z ∈ y.rightMoves, x < z

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

theorem IGame.Numeric.leftMove_lt {x y : IGame} [x.Numeric] (h : y ∈ x.leftMoves) : y < x

theorem IGame.Numeric.lt_rightMove {x y : IGame} [x.Numeric] (h : y ∈ x.rightMoves) : 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.leftMoves, and y ⧏ z for every z ∈ y.rightMoves.

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 ∈ y.leftMoves, ¬x ≤ z) ∧ ∀ z ∈ y.rightMoves, ¬z ≤ x)

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

@[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 ∈ y.leftMoves, x ≤ z) ∨ ∃ z ∈ y.rightMoves, z ≤ x

theorem IGame.Fits.le_of_forall_leftMoves_not_fits {x y : IGame} [x.Numeric] (hx : x.Fits y) (hl : ∀ z ∈ x.leftMoves, ¬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 ∈ x.rightMoves, ¬z.Fits y) : y ≤ x

theorem IGame.Fits.equiv_of_forall_not_fits {x y : IGame} [x.Numeric] (hx : x.Fits y) (hl : ∀ z ∈ x.leftMoves, ¬z.Fits y) (hr : ∀ z ∈ x.rightMoves, ¬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.

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

A specialization of the simplicity theorem to 0.

theorem IGame.equiv_one_of_fits {x : IGame} [x.Numeric] (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 {P : Surreal → Prop} (H : ∀ (y : IGame) [inst : y.Numeric], P (mk y)) (x : Surreal) : P 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

def Surreal.ofSets (s t : Set Surreal) [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] (H : ∀ x ∈ s, ∀ y ∈ t, x < y) : Surreal

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.

This is given notation {s | t}ˢ, where the superscript s is to disambiguate from set builder notation, and from the analogous constructors on IGame and Game. This notation will attempt to construct the relevant proof using aesop.

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

• Surreal.ofSets s t H = Surreal.mk {Surreal.out '' s | Surreal.out '' t}ᴵ

def Surreal.«term{_|_}ˢ» : Lean.ParserDescr

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.

This is given notation {s | t}ˢ, where the superscript s is to disambiguate from set builder notation, and from the analogous constructors on IGame and Game. This notation will attempt to construct the relevant proof using aesop.

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 (s t : Set Surreal) [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] (H : ∀ x ∈ s, ∀ y ∈ t, x < y) : toGame (ofSets s t ⋯) = {⇑toGame '' s | ⇑toGame '' t}ᴳ

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}ᴵ = ofSets (Set.range fun (x : ↑s) => have this := ⋯; mk ↑x) (Set.range fun (x : ↑t) => have this := ⋯; mk ↑x) ⋯

theorem Surreal.zero_def : 0 = ofSets ∅ ∅ ⋯

theorem Surreal.one_def : 1 = ofSets {0} ∅ ⋯