Nimbers #
The goal of this file is to define the field of nimbers, constructed as ordinals endowed with new
arithmetical operations. The nim sum a + b
is recursively defined as the least ordinal not equal
to any a' + b
or a + b'
for a' < a
and b' < b
. The nim product a * b
is likewise
recursively defined as the least ordinal not equal to any a' * b + a * b' + a' * b'
for a' < a
and b' < b
.
Nim addition arises within the context of impartial games. By the Sprague-Grundy theorem, each
impartial game is equivalent to some game of nim. If x ≈ nim o₁
and y ≈ nim o₂
, then
x + y ≈ nim (o₁ + o₂)
, where the ordinals are summed together as nimbers. Unfortunately, the
nim product admits no such characterization.
Notation #
Following On Numbers And Games (p. 121), we define notation ∗o
for the cast from
Ordinal
to Nimber
. Note that for general n : ℕ
, ∗n
is not the same as ↑n
. For
instance, ∗2 ≠ 0
, whereas ↑2 = ↑1 + ↑1 = 0
.
Implementation notes #
The nimbers inherit the order from the ordinals - this makes working with minimum excluded values much more convenient. However, the fact that nimbers are of characteristic 2 prevents the order from interacting with the arithmetic in any nice way.
To reduce API duplication, we opt not to implement operations on Nimber
on Ordinal
. The order
isomorphisms Ordinal.toNimber
and Nimber.toOrdinal
allow us to cast between them whenever
needed.
Todo #
- Add a
CharP 2
instance. - Define nim multiplication and prove nimbers are a commutative ring.
- Define nim division and prove nimbers are a field.
- Show the nimbers are algebraically closed.
Equations
- Nimber.linearOrder = LinearOrder.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯
Equations
- Nimber.succOrder = { succ := SuccOrder.succ, le_succ := Nimber.succOrder.proof_1, max_of_succ_le := @Nimber.succOrder.proof_2, succ_le_of_lt := @Nimber.succOrder.proof_3 }
The identity function between Ordinal
and Nimber
.
Equations
- Nimber.«term∗_» = Lean.ParserDescr.node `Nimber.term∗_ 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∗") (Lean.ParserDescr.cat `term 75))
Instances For
Equations
A recursor for Nimber
. Use as induction x
.
Equations
- Nimber.rec h a = h (Nimber.toOrdinal a)
Instances For
Ordinal.induction
but for Nimber
.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Nimber addition #
Nimber addition is recursively defined so that a + b
is the smallest number not equal to
a' + b
or a + b'
for a' < a
and b' < b
.
Equations
Instances For
Equations
Equations
Equations
- One or more equations did not get rendered due to their size.