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 pregames.

In fact, the surreals form a complete ordered field, containing a copy of the reals (and much else besides!) but we do not yet have a complete development.

Order properties

Surreal numbers inherit the relations ≤ and < from games (Surreal.instLE and Surreal.instLT), and these relations satisfy the axioms of a partial order.

Algebraic operations

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

In Mathlib.SetTheory.Surreal.Multiplication, we define multiplication and show that the surreals form a linear ordered commutative ring.

One can also map all the ordinals into the surreals!

TODO

• Define the field structure on the surreals.

References

• [Conway, On numbers and games][Conway2001]
• [Schleicher, Stoll, An introduction to Conway's games and numbers][SchleicherStoll]

def SetTheory.PGame.Numeric : PGame → Prop

A pre-game is numeric if everything in the L set is less than everything in the R set, and all the elements of L and R are also numeric.

Equations

• (SetTheory.PGame.mk α β L R).Numeric = ((∀ (i : α) (j : β), L i < R j) ∧ (∀ (i : α), (L i).Numeric) ∧ ∀ (j : β), (R j).Numeric)

theorem SetTheory.PGame.numeric_def {x : PGame} : x.Numeric ↔ (∀ (i : x.LeftMoves) (j : x.RightMoves), x.moveLeft i < x.moveRight j) ∧ (∀ (i : x.LeftMoves), (x.moveLeft i).Numeric) ∧ ∀ (j : x.RightMoves), (x.moveRight j).Numeric

theorem SetTheory.PGame.Numeric.mk {x : PGame} (h₁ : ∀ (i : x.LeftMoves) (j : x.RightMoves), x.moveLeft i < x.moveRight j) (h₂ : ∀ (i : x.LeftMoves), (x.moveLeft i).Numeric) (h₃ : ∀ (j : x.RightMoves), (x.moveRight j).Numeric) : x.Numeric

theorem SetTheory.PGame.Numeric.left_lt_right {x : PGame} (o : x.Numeric) (i : x.LeftMoves) (j : x.RightMoves) : x.moveLeft i < x.moveRight j

theorem SetTheory.PGame.Numeric.moveLeft {x : PGame} (o : x.Numeric) (i : x.LeftMoves) : (x.moveLeft i).Numeric

theorem SetTheory.PGame.Numeric.moveRight {x : PGame} (o : x.Numeric) (j : x.RightMoves) : (x.moveRight j).Numeric

theorem SetTheory.PGame.Numeric.isOption {x' x : PGame} (h : x'.IsOption x) (hx : x.Numeric) : x'.Numeric

theorem SetTheory.PGame.numeric_rec {C : PGame → Prop} (H : ∀ (l r : Type u_1) (L : l → PGame) (R : r → PGame), (∀ (i : l) (j : r), L i < R j) → (∀ (i : l), (L i).Numeric) → (∀ (i : r), (R i).Numeric) → (∀ (i : l), C (L i)) → (∀ (i : r), C (R i)) → C (mk l r L R)) (x : PGame) : x.Numeric → C x

theorem SetTheory.PGame.Relabelling.numeric_imp {x y : PGame} (r : x.Relabelling y) (ox : x.Numeric) : y.Numeric

theorem SetTheory.PGame.Relabelling.numeric_congr {x y : PGame} (r : x.Relabelling y) : x.Numeric ↔ y.Numeric

Relabellings preserve being numeric.

theorem SetTheory.PGame.lf_asymm {x y : PGame} (ox : x.Numeric) (oy : y.Numeric) : x.LF y → ¬y.LF x

theorem SetTheory.PGame.le_of_lf {x y : PGame} (h : x.LF y) (ox : x.Numeric) (oy : y.Numeric) : x ≤ y

theorem SetTheory.PGame.LF.le {x y : PGame} (h : x.LF y) (ox : x.Numeric) (oy : y.Numeric) : x ≤ y

Alias of SetTheory.PGame.le_of_lf.

theorem SetTheory.PGame.lt_of_lf {x y : PGame} (h : x.LF y) (ox : x.Numeric) (oy : y.Numeric) : x < y

theorem SetTheory.PGame.LF.lt {x y : PGame} (h : x.LF y) (ox : x.Numeric) (oy : y.Numeric) : x < y

Alias of SetTheory.PGame.lt_of_lf.

theorem SetTheory.PGame.lf_iff_lt {x y : PGame} (ox : x.Numeric) (oy : y.Numeric) : x.LF y ↔ x < y

theorem SetTheory.PGame.le_iff_forall_lt {x y : PGame} (ox : x.Numeric) (oy : y.Numeric) : x ≤ y ↔ (∀ (i : x.LeftMoves), x.moveLeft i < y) ∧ ∀ (j : y.RightMoves), x < y.moveRight j

Definition of x ≤ y on numeric pre-games, in terms of <

theorem SetTheory.PGame.lt_iff_exists_le {x y : PGame} (ox : x.Numeric) (oy : y.Numeric) : x < y ↔ (∃ (i : y.LeftMoves), x ≤ y.moveLeft i) ∨ ∃ (j : x.RightMoves), x.moveRight j ≤ y

Definition of x < y on numeric pre-games, in terms of ≤

theorem SetTheory.PGame.lt_of_exists_le {x y : PGame} (ox : x.Numeric) (oy : y.Numeric) : ((∃ (i : y.LeftMoves), x ≤ y.moveLeft i) ∨ ∃ (j : x.RightMoves), x.moveRight j ≤ y) → x < y

theorem SetTheory.PGame.lt_def {x y : PGame} (ox : x.Numeric) (oy : y.Numeric) : x < y ↔ (∃ (i : y.LeftMoves), (∀ (i' : x.LeftMoves), x.moveLeft i' < y.moveLeft i) ∧ ∀ (j : (y.moveLeft i).RightMoves), x < (y.moveLeft i).moveRight j) ∨ ∃ (j : x.RightMoves), (∀ (i : (x.moveRight j).LeftMoves), (x.moveRight j).moveLeft i < y) ∧ ∀ (j' : y.RightMoves), x.moveRight j < y.moveRight j'

The definition of x < y on numeric pre-games, in terms of < two moves later.

theorem SetTheory.PGame.not_fuzzy {x y : PGame} (ox : x.Numeric) (oy : y.Numeric) : ¬x.Fuzzy y

theorem SetTheory.PGame.lt_or_equiv_or_gt {x y : PGame} (ox : x.Numeric) (oy : y.Numeric) : x < y ∨ x ≈ y ∨ y < x

theorem SetTheory.PGame.numeric_of_isEmpty (x : PGame) [IsEmpty x.LeftMoves] [IsEmpty x.RightMoves] : x.Numeric

theorem SetTheory.PGame.numeric_of_isEmpty_leftMoves (x : PGame) [IsEmpty x.LeftMoves] : (∀ (j : x.RightMoves), (x.moveRight j).Numeric) → x.Numeric

theorem SetTheory.PGame.numeric_of_isEmpty_rightMoves (x : PGame) [IsEmpty x.RightMoves] (H : ∀ (i : x.LeftMoves), (x.moveLeft i).Numeric) : x.Numeric

theorem SetTheory.PGame.numeric_zero : Numeric 0

theorem SetTheory.PGame.numeric_one : Numeric 1

theorem SetTheory.PGame.Numeric.neg {x : PGame} : x.Numeric → (-x).Numeric

theorem SetTheory.PGame.insertLeft_numeric {x x' : PGame} (x_num : x.Numeric) (x'_num : x'.Numeric) (h : x' ≤ x) : (x.insertLeft x').Numeric

Inserting a smaller numeric left option into a numeric game results in a numeric game.

theorem SetTheory.PGame.insertRight_numeric {x x' : PGame} (x_num : x.Numeric) (x'_num : x'.Numeric) (h : x ≤ x') : (x.insertRight x').Numeric

Inserting a larger numeric right option into a numeric game results in a numeric game.

theorem SetTheory.PGame.Numeric.moveLeft_lt {x : PGame} (o : x.Numeric) (i : x.LeftMoves) : x.moveLeft i < x

theorem SetTheory.PGame.Numeric.moveLeft_le {x : PGame} (o : x.Numeric) (i : x.LeftMoves) : x.moveLeft i ≤ x

theorem SetTheory.PGame.Numeric.lt_moveRight {x : PGame} (o : x.Numeric) (j : x.RightMoves) : x < x.moveRight j

theorem SetTheory.PGame.Numeric.le_moveRight {x : PGame} (o : x.Numeric) (j : x.RightMoves) : x ≤ x.moveRight j

@[irreducible]

theorem SetTheory.PGame.Numeric.add {x y : PGame} : x.Numeric → y.Numeric → (x + y).Numeric

theorem SetTheory.PGame.Numeric.sub {x y : PGame} (ox : x.Numeric) (oy : y.Numeric) : (x - y).Numeric

theorem SetTheory.PGame.numeric_nat (n : ℕ) : (↑n).Numeric

Pre-games defined by natural numbers are numeric.

theorem SetTheory.PGame.numeric_toPGame (o : Ordinal.{u_1}) : o.toPGame.Numeric

Ordinal games are numeric.

def Surreal : Type (u_1 + 1)

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

Equations

• Surreal = Quotient (inferInstanceAs (Setoid (Subtype SetTheory.PGame.Numeric)))

def Surreal.mk (x : SetTheory.PGame) (h : x.Numeric) : Surreal

Construct a surreal number from a numeric pre-game.

Equations

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

instance Surreal.instZero : Zero Surreal

Equations

• Surreal.instZero = { zero := Surreal.mk 0 SetTheory.PGame.numeric_zero }

instance Surreal.instOne : One Surreal

Equations

• Surreal.instOne = { one := Surreal.mk 1 SetTheory.PGame.numeric_one }

instance Surreal.instInhabited : Inhabited Surreal

Equations

• Surreal.instInhabited = { default := 0 }

theorem Surreal.mk_eq_mk {x y : SetTheory.PGame} {hx : x.Numeric} {hy : y.Numeric} : mk x hx = mk y hy ↔ x ≈ y

theorem Surreal.mk_eq_zero {x : SetTheory.PGame} {hx : x.Numeric} : mk x hx = 0 ↔ x ≈ 0

def Surreal.lift {α : Sort u_1} (f : (x : SetTheory.PGame) → x.Numeric → α) (H : ∀ {x y : SetTheory.PGame} (hx : x.Numeric) (hy : y.Numeric), x.Equiv y → f x hx = f y hy) : Surreal → α

Lift an equivalence-respecting function on pre-games to surreals.

Equations

• Surreal.lift f H = Quotient.lift (fun (x : { x : SetTheory.PGame // x.Numeric }) => f ↑x ⋯) ⋯

def Surreal.lift₂ {α : Sort u_1} (f : (x : SetTheory.PGame) → (y : SetTheory.PGame) → x.Numeric → y.Numeric → α) (H : ∀ {x₁ : SetTheory.PGame} {y₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y₂ : SetTheory.PGame} (ox₁ : x₁.Numeric) (oy₁ : y₁.Numeric) (ox₂ : x₂.Numeric) (oy₂ : y₂.Numeric), x₁.Equiv x₂ → y₁.Equiv y₂ → f x₁ y₁ ox₁ oy₁ = f x₂ y₂ ox₂ oy₂) : Surreal → Surreal → α

Lift a binary equivalence-respecting function on pre-games to surreals.

Equations

• Surreal.lift₂ f H = Surreal.lift (fun (x : SetTheory.PGame) (ox : x.Numeric) => Surreal.lift (fun (y : SetTheory.PGame) (oy : y.Numeric) => f x y ox oy) ⋯) ⋯

instance Surreal.instLE : LE Surreal

Equations

• Surreal.instLE = { le := Surreal.lift₂ (fun (x y : SetTheory.PGame) (x_1 : x.Numeric) (x_2 : y.Numeric) => x ≤ y) @Surreal.instLE._proof_5 }

@[simp]

theorem Surreal.mk_le_mk {x y : SetTheory.PGame} {hx : x.Numeric} {hy : y.Numeric} : mk x hx ≤ mk y hy ↔ x ≤ y

theorem Surreal.zero_le_mk {x : SetTheory.PGame} {hx : x.Numeric} : 0 ≤ mk x hx ↔ 0 ≤ x

instance Surreal.instLT : LT Surreal

Equations

• Surreal.instLT = { lt := Surreal.lift₂ (fun (x y : SetTheory.PGame) (x_1 : x.Numeric) (x_2 : y.Numeric) => x < y) @Surreal.instLT._proof_7 }

theorem Surreal.mk_lt_mk {x y : SetTheory.PGame} {hx : x.Numeric} {hy : y.Numeric} : mk x hx < mk y hy ↔ x < y

theorem Surreal.zero_lt_mk {x : SetTheory.PGame} {hx : x.Numeric} : 0 < mk x hx ↔ 0 < x

theorem Surreal.mk_moveLeft_lt_mk {x : SetTheory.PGame} (o : x.Numeric) (i : x.LeftMoves) : mk (x.moveLeft i) ⋯ < mk x o

Same as moveLeft_lt, but for Surreal instead of PGame

theorem Surreal.mk_lt_mk_moveRight {x : SetTheory.PGame} (o : x.Numeric) (j : x.RightMoves) : mk x o < mk (x.moveRight j) ⋯

Same as lt_moveRight, but for Surreal instead of PGame

instance Surreal.instAdd : Add Surreal

Addition on surreals is inherited from pre-game addition: the sum of x = {xL | xR} and y = {yL | yR} is {xL + y, x + yL | xR + y, x + yR}.

Equations

• Surreal.instAdd = { add := Surreal.lift₂ (fun (x y : SetTheory.PGame) (ox : x.Numeric) (oy : y.Numeric) => ⟦⟨x + y, ⋯⟩⟧) @Surreal.instAdd._proof_8 }

instance Surreal.instNeg : Neg Surreal

Negation for surreal numbers is inherited from pre-game negation: the negation of {L | R} is {-R | -L}.

Equations

• Surreal.instNeg = { neg := Surreal.lift (fun (x : SetTheory.PGame) (ox : x.Numeric) => ⟦⟨-x, ⋯⟩⟧) @Surreal.instNeg._proof_9 }

instance Surreal.addCommGroup : AddCommGroup Surreal

Equations

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

instance Surreal.partialOrder : PartialOrder Surreal

Equations

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

instance Surreal.isOrderedAddMonoid : IsOrderedAddMonoid Surreal

theorem Surreal.mk_add {x y : SetTheory.PGame} (hx : x.Numeric) (hy : y.Numeric) : mk (x + y) ⋯ = mk x hx + mk y hy

theorem Surreal.mk_sub {x y : SetTheory.PGame} (hx : x.Numeric) (hy : y.Numeric) : mk (x - y) ⋯ = mk x hx - mk y hy

theorem Surreal.zero_def : 0 = mk 0 SetTheory.PGame.numeric_zero

noncomputable instance Surreal.instLinearOrder : LinearOrder Surreal

Equations

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

instance Surreal.instAddMonoidWithOne : AddMonoidWithOne Surreal

Equations

• Surreal.instAddMonoidWithOne = AddMonoidWithOne.unary

def Surreal.toGame : Surreal →+o SetTheory.Game

Casts a Surreal number into a Game.

Equations

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

@[simp]

theorem Surreal.zero_toGame : toGame 0 = 0

@[simp]

theorem Surreal.one_toGame : toGame 1 = 1

@[simp]

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

theorem Surreal.bddAbove_range_of_small {ι : Type u_1} [Small.{u, u_1} ι] (f : ι → Surreal) : BddAbove (Set.range f)

A small family of surreals is bounded above.

theorem Surreal.bddAbove_of_small (s : Set Surreal) [Small.{u, u + 1} ↑s] : BddAbove s

A small set of surreals is bounded above.

theorem Surreal.bddBelow_range_of_small {ι : Type u_1} [Small.{u, u_1} ι] (f : ι → Surreal) : BddBelow (Set.range f)

A small family of surreals is bounded below.

theorem Surreal.bddBelow_of_small (s : Set Surreal) [Small.{u, u + 1} ↑s] : BddBelow s

A small set of surreals is bounded below.

noncomputable def Ordinal.toSurreal : Ordinal.{u_1} ↪o Surreal

Converts an ordinal into the corresponding surreal.

Equations

• Ordinal.toSurreal = { toFun := fun (o : Ordinal.{?u.7}) => Surreal.mk o.toPGame ⋯, inj' := Ordinal.toSurreal._proof_35, map_rel_iff' := @Ordinal.toPGame_le_iff }