Documentation

Mathlib.SetTheory.Nimber.Basic

Nimbers #

The goal of this file is to define the 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. There is also a nim product, defined in the Mathlib/SetTheory/Nimber/Field.lean file.

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][conway2001] (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.

Basic casts between `Ordinal` and `Nimber` #

def Nimber :

Type (u_1 + 1)

A type synonym for ordinals with nimber addition and multiplication.

Equations

Instances For

instance instNimberZero :

Equations

instance instNimberInhabited :

Inhabited Nimber

Equations

instance instNimberOne :

Equations

instance instNimberNontrivial :

Nontrivial Nimber

Equations

instance instNimberWellFoundedRelation :

WellFoundedRelation Nimber

Equations

instance Nimber.instLinearOrder :

LinearOrder Nimber

Equations

instance Nimber.instSuccOrder :

SuccOrder Nimber

Equations

instance Nimber.instOrderBot :

OrderBot Nimber

Equations

instance Nimber.instNoMaxOrder :

NoMaxOrder Nimber

instance Nimber.instZeroLEOneClass :

ZeroLEOneClass Nimber

instance Nimber.instNeZeroOne :

@[match_pattern]

def Ordinal.toNimber :

Ordinal.{u_1} ≃o Nimber

The identity function between Ordinal and Nimber.

Equations

Instances For

@[match_pattern]

def Nimber.toOrdinal :

Nimber ≃o Ordinal.{u_1}

The identity function between Nimber and Ordinal.

Equations

Instances For

def Nimber.«term∗_» :

Lean.ParserDescr

The identity function between Ordinal and Nimber.

Equations

Instances For

@[simp]

theorem Nimber.toOrdinal_symm_eq :

toOrdinal.symm = Ordinal.toNimber

@[simp]

theorem Nimber.toOrdinal_toNimber (a : Nimber) :

Ordinal.toNimber (toOrdinal a) = a

theorem Nimber.lt_wf :

WellFounded fun (x1 x2 : Nimber) => x1 < x2

instance Nimber.instWellFoundedLT :

WellFoundedLT Nimber

instance Nimber.instConditionallyCompleteLinearOrderBot :

ConditionallyCompleteLinearOrderBot Nimber

Equations

@[simp]

theorem Nimber.bot_eq_zero :

@[simp]

theorem Nimber.toOrdinal_zero :

toOrdinal 0 = 0

@[simp]

theorem Nimber.toOrdinal_one :

toOrdinal 1 = 1

@[simp]

theorem Nimber.toOrdinal_eq_zero {a : Nimber} :

toOrdinal a = 0 ↔ a = 0

@[simp]

theorem Nimber.toOrdinal_eq_one {a : Nimber} :

toOrdinal a = 1 ↔ a = 1

@[simp]

theorem Nimber.toOrdinal_max (a b : Nimber) :

toOrdinal (max a b) = max (toOrdinal a) (toOrdinal b)

@[simp]

theorem Nimber.toOrdinal_min (a b : Nimber) :

toOrdinal (min a b) = min (toOrdinal a) (toOrdinal b)

theorem Nimber.succ_def (a : Nimber) :

Order.succ a = Ordinal.toNimber (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

Instances For

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

theorem Nimber.lt_one_iff_zero {a : Nimber} :

a < 1 ↔ a = 0

theorem Nimber.one_le_iff_ne_zero {a : Nimber} :

1 ≤ a ↔ a ≠ 0

theorem Nimber.eq_nat_of_le_nat {a : Nimber} {b : ℕ} (h : a ≤ Ordinal.toNimber ↑b) :

∃ (c : ℕ), a = Ordinal.toNimber ↑c

instance Nimber.small_Iio (a : Nimber) :

Small.{u, u + 1} ↑(Set.Iio a)

instance Nimber.small_Iic (a : Nimber) :

Small.{u, u + 1} ↑(Set.Iic a)

instance Nimber.small_Ico (a b : Nimber) :

Small.{u, u + 1} ↑(Set.Ico a b)

instance Nimber.small_Icc (a b : Nimber) :

Small.{u, u + 1} ↑(Set.Icc a b)

instance Nimber.small_Ioo (a b : Nimber) :

Small.{u, u + 1} ↑(Set.Ioo a b)

instance Nimber.small_Ioc (a b : Nimber) :

Small.{u, u + 1} ↑(Set.Ioc a b)

theorem Nimber.not_bddAbove_compl_of_small (s : Set Nimber) [Small.{u, u + 1} ↑s] :

¬BddAbove sᶜ

theorem not_small_nimber :

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

instance Nimber.uncountable :

Uncountable Nimber

@[simp]

theorem Ordinal.toNimber_symm_eq :

toNimber.symm = Nimber.toOrdinal

@[simp]

theorem Ordinal.toNimber_toOrdinal (a : Ordinal.{u_1}) :

Nimber.toOrdinal (toNimber a) = a

@[simp]

theorem Ordinal.toNimber_zero :

@[simp]

theorem Ordinal.toNimber_one :

@[simp]

theorem Ordinal.toNimber_eq_zero {a : Ordinal.{u_1}} :

toNimber a = 0 ↔ a = 0

@[simp]

theorem Ordinal.toNimber_eq_one {a : Ordinal.{u_1}} :

toNimber a = 1 ↔ a = 1

@[simp]

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

toNimber (max a b) = max (toNimber a) (toNimber b)

@[simp]

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

toNimber (min a b) = min (toNimber a) (toNimber b)

Nimber addition #

@[irreducible]

def Nimber.add (a b : Nimber) :

Nimber addition is recursively defined so that a + b is the smallest nimber not equal to a' + b or a + b' for a' < a and b' < b.

Equations

Instances For

instance Nimber.instAdd :

Equations

theorem Nimber.add_def (a b : Nimber) :

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

theorem Nimber.exists_of_lt_add {a b c : Nimber} (h : c < a + b) :

(∃ a' < a, a' + b = c) ∨ ∃ b' < b, a + b' = c

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

a + b ≤ c

instance Nimber.instIsLeftCancelAdd :

IsLeftCancelAdd Nimber

instance Nimber.instIsRightCancelAdd :

IsRightCancelAdd Nimber

@[irreducible]

theorem Nimber.add_comm (a b : Nimber) :

a + b = b + a

@[irreducible]

theorem Nimber.add_eq_zero {a b : Nimber} :

a + b = 0 ↔ a = b

theorem Nimber.add_ne_zero_iff {a b : Nimber} :

a + b ≠ 0 ↔ a ≠ b

@[simp]

theorem Nimber.add_self (a : Nimber) :

a + a = 0

@[irreducible]

theorem Nimber.add_assoc (a b 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 :

Equations

@[simp]

theorem Nimber.neg_eq (a : Nimber) :

-a = a

instance Nimber.instAddCommGroupWithOne :

AddCommGroupWithOne Nimber

Equations

@[simp]

theorem Nimber.add_cancel_right (a b : Nimber) :

a + b + b = a

@[simp]

theorem Nimber.add_cancel_left (a b : Nimber) :

a + (a + b) = b

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

b + c < a ∨ c + a < b ∨ a + b < c

theorem Nimber.lt_add_cases {a b c : Nimber} (h : a < b + c) :

a + c < b ∨ a + b < c

@[irreducible]

theorem Nimber.add_nat (a b : ℕ) :

Ordinal.toNimber ↑a + Ordinal.toNimber ↑b = Ordinal.toNimber ↑(a ^^^ b)

Nimber addition of naturals corresponds to the bitwise XOR operation.