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 #
We show that the surreals form a linear ordered commutative group.
One can also map all the ordinals into the surreals!
Multiplication of surreal numbers #
The proof that multiplication lifts to surreal numbers is surprisingly difficult and is currently missing in the library. A sample proof can be found in Theorem 3.8 in the second reference below. The difficulty lies in the length of the proof and the number of theorems that need to proven simultaneously. This will make for a fun and challenging project.
The branch surreal_mul
contains some progress on this proof.
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][schleicher_stoll]
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.Numeric (SetTheory.PGame.mk α β L R) = ((∀ (i : α) (j : β), L i < R j) ∧ (∀ (i : α), SetTheory.PGame.Numeric (L i)) ∧ ∀ (j : β), SetTheory.PGame.Numeric (R j))
Instances For
Relabellings preserve being numeric.
Alias of SetTheory.PGame.le_of_lf
.
Alias of SetTheory.PGame.lt_of_lf
.
Definition of x ≤ y
on numeric pre-games, in terms of <
Definition of x < y
on numeric pre-games, in terms of ≤
The definition of x < y
on numeric pre-games, in terms of <
two moves later.
Pre-games defined by natural numbers are numeric.
Ordinal games are numeric.
Construct a surreal number from a numeric pre-game.
Instances For
Lift an equivalence-respecting function on pre-games to surreals.
Instances For
Lift a binary equivalence-respecting function on pre-games to surreals.
Instances For
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}
.
Negation for surreal numbers is inherited from pre-game negation:
the negation of {L | R}
is {-R | -L}
.
Casts a Surreal
number into a Game
.
Instances For
Converts an ordinal into the corresponding surreal.