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.

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.

Basic casts between Ordinal and Nimber

def Nimber : Type (u_1 + 1)

A type synonym for ordinals with natural addition and multiplication.

Equations

• Nimber = Ordinal.{?u.3}

instance Nimber.linearOrder : LinearOrder Nimber

Equations

• Nimber.linearOrder = LinearOrder.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

instance Nimber.succOrder : SuccOrder Nimber

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 }

instance Nimber.orderBot : OrderBot Nimber

Equations

• Nimber.orderBot = OrderBot.mk Nimber.orderBot.proof_1

instance Nimber.noMaxOrder : NoMaxOrder Nimber

Equations

• Nimber.noMaxOrder = ⋯

instance Nimber.zeroLEOneClass : ZeroLEOneClass Nimber

Equations

• Nimber.zeroLEOneClass = ⋯

@[match_pattern]

def Ordinal.toNimber : Ordinal.{u_1} ≃o Nimber

The identity function between Ordinal and Nimber.

Equations

• Ordinal.toNimber = OrderIso.refl Ordinal.{?u.3}

@[match_pattern]

def Nimber.toOrdinal : Nimber ≃o Ordinal.{u_1}

The identity function between Nimber and Ordinal.

Equations

• Nimber.toOrdinal = OrderIso.refl Nimber

@[simp]

theorem Nimber.toOrdinal_symm_eq : Nimber.toOrdinal.symm = Ordinal.toNimber

@[simp]

theorem Nimber.toOrdinal_toNimber (a : Nimber) : Ordinal.toNimber (Nimber.toOrdinal a) = a

theorem Nimber.lt_wf : WellFounded fun (x1 x2 : Nimber) => x1 < x2

instance Nimber.instWellFoundedLT : WellFoundedLT Nimber

Equations

• Nimber.instWellFoundedLT = Ordinal.wellFoundedLT

instance Nimber.instIsWellOrderLt : IsWellOrder Nimber fun (x1 x2 : Nimber) => x1 < x2

Equations

• Nimber.instIsWellOrderLt = ⋯

instance Nimber.instConditionallyCompleteLinearOrderBot : ConditionallyCompleteLinearOrderBot Nimber

Equations

• Nimber.instConditionallyCompleteLinearOrderBot = WellFoundedLT.conditionallyCompleteLinearOrderBot Nimber

@[simp]

theorem Nimber.bot_eq_zero : ⊥ = 0

@[simp]

theorem Nimber.toOrdinal_zero : Nimber.toOrdinal 0 = 0

@[simp]

theorem Nimber.toOrdinal_one : Nimber.toOrdinal 1 = 1

@[simp]

theorem Nimber.toOrdinal_eq_zero (a : Nimber) : Nimber.toOrdinal a = 0 ↔ a = 0

@[simp]

theorem Nimber.toOrdinal_eq_one (a : Nimber) : Nimber.toOrdinal a = 1 ↔ a = 1

@[simp]

theorem Nimber.toOrdinal_max {a : Nimber} {b : Nimber} : Nimber.toOrdinal (max a b) = max (Nimber.toOrdinal a) (Nimber.toOrdinal b)

@[simp]

theorem Nimber.toOrdinal_min {a : Nimber} {b : Nimber} : Nimber.toOrdinal (min a b) = min (Nimber.toOrdinal a) (Nimber.toOrdinal b)

theorem Nimber.succ_def (a : Nimber) : Order.succ a = Ordinal.toNimber (Nimber.toOrdinal a + 1)

def Nimber.rec {β : Nimber → Sort u_1} (h : (a : Ordinal.{u_2}) → β (Ordinal.toNimber a)) (a : Nimber) : β a

A recursor for Nimber. Use as induction x.

Equations

• Nimber.rec h a = h (Nimber.toOrdinal a)

theorem Nimber.induction {p : Nimber → Prop} (i : Nimber) : (∀ (j : Nimber), (∀ k < j, p k) → p j) → p i

Ordinal.induction but for Nimber.

theorem Nimber.le_zero {a : Nimber} : a ≤ 0 ↔ a = 0

theorem Nimber.not_lt_zero (a : Nimber) : ¬a < 0

theorem Nimber.pos_iff_ne_zero {a : Nimber} : 0 < a ↔ a ≠ 0

instance Nimber.instSmallElemIio (a : Nimber) : Small.{u, u + 1} ↑(Set.Iio a)

Equations

• ⋯ = ⋯

instance Nimber.instSmallElemIic (a : Nimber) : Small.{u, u + 1} ↑(Set.Iic a)

Equations

• ⋯ = ⋯

theorem not_small_nimber : ¬Small.{u, max (u + 1) (v + 1)} Nimber

@[simp]

theorem Ordinal.toNimber_symm_eq : Ordinal.toNimber.symm = Nimber.toOrdinal

@[simp]

theorem Ordinal.toNimber_toOrdinal (a : Ordinal.{u_1}) : Nimber.toOrdinal (Ordinal.toNimber a) = a

@[simp]

theorem Ordinal.toNimber_zero : Ordinal.toNimber 0 = 0

@[simp]

theorem Ordinal.toNimber_one : Ordinal.toNimber 1 = 1

@[simp]

theorem Ordinal.toNimber_eq_zero (a : Ordinal.{u_1}) : Ordinal.toNimber a = 0 ↔ a = 0

@[simp]

theorem Ordinal.toNimber_eq_one (a : Ordinal.{u_1}) : Ordinal.toNimber a = 1 ↔ a = 1

@[simp]

theorem Ordinal.toNimber_max (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) : Ordinal.toNimber (max a b) = max (Ordinal.toNimber a) (Ordinal.toNimber b)

@[simp]

theorem Ordinal.toNimber_min (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) : Ordinal.toNimber (min a b) = min (Ordinal.toNimber a) (Ordinal.toNimber b)

Nimber addition

@[irreducible]

def Nimber.add (a : Nimber) (b : Nimber) : Nimber

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

• a.add b = sInf {x : Nimber | (∃ (a' : Nimber) (_ : a' < a), a'.add b = x) ∨ ∃ (b' : Nimber) (_ : b' < b), a.add b' = x}ᶜ

instance Nimber.instAdd : Add Nimber

Equations

• Nimber.instAdd = { add := Nimber.add }

theorem Nimber.add_def (a : Nimber) (b : Nimber) : a + b = sInf {x : Nimber | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ

theorem Nimber.exists_of_lt_add {a : Nimber} {b : Nimber} {c : Nimber} (h : c < a + b) : (∃ a' < a, a' + b = c) ∨ ∃ b' < b, a + b' = c

theorem Nimber.add_le_of_forall_ne {a : Nimber} {b : Nimber} {c : Nimber} (h₁ : ∀ a' < a, a' + b ≠ c) (h₂ : ∀ b' < b, a + b' ≠ c) : a + b ≤ c

instance Nimber.instIsLeftCancelAdd : IsLeftCancelAdd Nimber

Equations

• Nimber.instIsLeftCancelAdd = ⋯

instance Nimber.instIsRightCancelAdd : IsRightCancelAdd Nimber

Equations

• Nimber.instIsRightCancelAdd = ⋯

@[irreducible]

theorem Nimber.add_comm (a : Nimber) (b : Nimber) : a + b = b + a

@[irreducible]

theorem Nimber.add_eq_zero {a : Nimber} {b : Nimber} : a + b = 0 ↔ a = b

theorem Nimber.add_ne_zero_iff {a : Nimber} {b : Nimber} : a + b ≠ 0 ↔ a ≠ b

@[simp]

theorem Nimber.add_self (a : Nimber) : a + a = 0

@[irreducible]

theorem Nimber.add_assoc (a : Nimber) (b : Nimber) (c : Nimber) : a + b + c = a + (b + c)

@[irreducible]

theorem Nimber.add_zero (a : Nimber) : a + 0 = a

theorem Nimber.zero_add (a : Nimber) : 0 + a = a

instance Nimber.instNeg : Neg Nimber

Equations

• Nimber.instNeg = { neg := id }

@[simp]

theorem Nimber.neg_eq (a : Nimber) : -a = a

instance Nimber.instAddCommGroupWithOne : AddCommGroupWithOne Nimber

Equations

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

@[simp]

theorem Nimber.add_cancel_right (a : Nimber) (b : Nimber) : a + b + b = a

@[simp]

theorem Nimber.add_cancel_left (a : Nimber) (b : Nimber) : a + (a + b) = b

theorem Nimber.add_trichotomy {a : Nimber} {b : Nimber} {c : Nimber} (h : a + b + c ≠ 0) : b + c < a ∨ c + a < b ∨ a + b < c