Documentation

Mathlib.SetTheory.Game.Birthday

Birthdays of games #

There are two related but distinct notions of a birthday within combinatorial game theory. One is the birthday of a pre-game, which represents the "step" at which it is constructed. We define it recursively as the least ordinal larger than the birthdays of its left and right options. On the other hand, the birthday of a game is the smallest birthday among all pre-games that quotient to it.

The birthday of a pre-game can be understood as representing the depth of its game tree. On the other hand, the birthday of a game more closely matches Conway's original description. The lemma SetTheory.Game.birthday_eq_pGameBirthday links both definitions together.

Main declarations #

Todo #

source
noncomputable def SetTheory.PGame.birthday :
SetTheory.PGame → Ordinal.{u}

The birthday of a pre-game is inductively defined as the least strict upper bound of the birthdays of its left and right games. It may be thought as the "step" in which a certain game is constructed.

Equations
Instances For
    source
    theorem SetTheory.PGame.birthday_def (x : SetTheory.PGame) :
    x.birthday = (Ordinal.lsub fun (i : x.LeftMoves) => (x.moveLeft i).birthday) ⊔ Ordinal.lsub fun (i : x.RightMoves) => (x.moveRight i).birthday
    source
    theorem SetTheory.PGame.birthday_moveLeft_lt {x : SetTheory.PGame} (i : x.LeftMoves) :
    (x.moveLeft i).birthday < x.birthday
    source
    theorem SetTheory.PGame.birthday_moveRight_lt {x : SetTheory.PGame} (i : x.RightMoves) :
    (x.moveRight i).birthday < x.birthday
    source
    theorem SetTheory.PGame.lt_birthday_iff {x : SetTheory.PGame} {o : Ordinal.{u_1}} :
    o < x.birthday ↔ (∃ (i : x.LeftMoves), o ≤ (x.moveLeft i).birthday) ∨ ∃ (i : x.RightMoves), o ≤ (x.moveRight i).birthday
    source
    theorem SetTheory.PGame.Relabelling.birthday_congr {x y : SetTheory.PGame} :
    x.Relabelling y → x.birthday = y.birthday
    source
    @[simp]
    theorem SetTheory.PGame.birthday_eq_zero {x : SetTheory.PGame} :
    x.birthday = 0 ↔ IsEmpty x.LeftMoves ∧ IsEmpty x.RightMoves
    source
    @[simp]
    theorem SetTheory.PGame.birthday_zero :
    SetTheory.PGame.birthday 0 = 0
    source
    @[simp]
    theorem SetTheory.PGame.birthday_one :
    SetTheory.PGame.birthday 1 = 1
    source
    @[simp]
    theorem SetTheory.PGame.birthday_star :
    SetTheory.PGame.star.birthday = 1
    source
    @[simp]
    theorem SetTheory.PGame.birthday_neg (x : SetTheory.PGame) :
    (-x).birthday = x.birthday
    source
    @[simp]
    theorem SetTheory.PGame.birthday_ordinalToPGame (o : Ordinal.{u_1}) :
    o.toPGame.birthday = o
    source
    theorem SetTheory.PGame.le_birthday (x : SetTheory.PGame) :
    x ≤ x.birthday.toPGame
    source
    theorem SetTheory.PGame.neg_birthday_le (x : SetTheory.PGame) :
    -x.birthday.toPGame ≤ x
    source
    @[simp, irreducible]
    theorem SetTheory.PGame.birthday_add (x y : SetTheory.PGame) :
    (x + y).birthday = x.birthday.nadd y.birthday
    source
    @[simp]
    theorem SetTheory.PGame.birthday_sub (x y : SetTheory.PGame) :
    (x - y).birthday = x.birthday.nadd y.birthday
    source
    @[simp]
    theorem SetTheory.PGame.birthday_natCast (n : ℕ) :
    (↑n).birthday = ↑n
    source
    noncomputable def SetTheory.Game.birthday (x : SetTheory.Game) :
    Ordinal.{u}

    The birthday of a game is defined as the least birthday among all pre-games that define it.

    Equations
    Instances For
      source
      theorem SetTheory.Game.birthday_eq_pGameBirthday (x : SetTheory.Game) :
      ∃ (y : SetTheory.PGame), ⟦y⟧ = x ∧ y.birthday = x.birthday
      source
      theorem SetTheory.Game.birthday_quot_le_pGameBirthday (x : SetTheory.PGame) :
      SetTheory.Game.birthday ⟦x⟧ ≤ x.birthday
      source
      @[simp]
      theorem SetTheory.Game.birthday_zero :
      SetTheory.Game.birthday 0 = 0
      source
      @[simp]
      theorem SetTheory.Game.birthday_eq_zero {x : SetTheory.Game} :
      x.birthday = 0 ↔ x = 0
      source
      @[simp]
      theorem SetTheory.Game.birthday_ordinalToGame (o : Ordinal.{u_1}) :
      o.toGame.birthday = o
      source
      @[simp]
      theorem SetTheory.Game.birthday_natCast (n : ℕ) :
      (↑n).birthday = ↑n
      source
      @[simp]
      theorem SetTheory.Game.birthday_ofNat (n : ℕ) [n.AtLeastTwo] :
      (OfNat.ofNat n).birthday = OfNat.ofNat n
      source
      @[simp]
      theorem SetTheory.Game.birthday_one :
      SetTheory.Game.birthday 1 = 1
      source
      @[simp]
      theorem SetTheory.Game.birthday_star :
      SetTheory.Game.birthday ⟦SetTheory.PGame.star⟧ = 1
      source
      @[simp]
      theorem SetTheory.Game.birthday_neg (x : SetTheory.Game) :
      (-x).birthday = x.birthday
      source
      theorem SetTheory.Game.le_birthday (x : SetTheory.Game) :
      x ≤ x.birthday.toGame
      source
      theorem SetTheory.Game.neg_birthday_le (x : SetTheory.Game) :
      -x.birthday.toGame ≤ x
      source
      theorem SetTheory.Game.birthday_add_le (x y : SetTheory.Game) :
      (x + y).birthday ≤ x.birthday.nadd y.birthday
      source
      theorem SetTheory.Game.birthday_sub_le (x y : SetTheory.Game) :
      (x - y).birthday ≤ x.birthday.nadd y.birthday
      source
      theorem SetTheory.Game.small_setOf_birthday_lt (o : Ordinal.{u}) :
      Small.{u, u + 1} { x : SetTheory.Game // x.birthday < o }

      Games with bounded birthday are a small set.