Documentation

CombinatorialGames.Form.Birthday

Birthdays of games #

There are two related but distinct notions of a birthday within combinatorial game theory. One is the birthday of an GameForm, which represents the "step" at which it is constructed; the day on which it is born. This is sometimes called the formal birthday of a game (see Siegel, Definition 1.27 on p. 61).

It can be defined recursively as the least ordinal strictly larger than the birthdays of its Left and Right options.

The birthday of an GameForm can also be understood as the depth of its game tree.

source
@[irreducible]
noncomputable def Form.birthday {G : Type (u + 1)} [g_form : Form G] (x : G) :
NatOrdinal

The birthday of a form is inductively defined as the least ordinal strictly larger than the birthdays of its options. It may be thought as the "step" in which the given game is constructed.

Equations
Instances For
    source
    theorem Form.lt_birthday_iff' {G : Type (u + 1)} [g_form : Form G] {x : G} {o : NatOrdinal} :
    o < birthday x ↔ ∃ (y : G), IsOption y x ∧ o ≤ birthday y
    source
    theorem Form.birthday_le_iff' {G : Type (u + 1)} [g_form : Form G] {x : G} {o : NatOrdinal} :
    birthday x ≤ o ↔ ∀ (y : G), IsOption y x → birthday y < o
    source
    theorem Form.lt_birthday_iff {G : Type (u + 1)} [g_form : Form G] {x : G} {o : NatOrdinal} :
    o < birthday x ↔ (∃ y ∈ moves Player.left x, o ≤ birthday y) ∨ ∃ y ∈ moves Player.right x, o ≤ birthday y
    source
    theorem Form.birthday_le_iff {G : Type (u + 1)} [g_form : Form G] {x : G} {o : NatOrdinal} :
    birthday x ≤ o ↔ (∀ y ∈ moves Player.left x, birthday y < o) ∧ ∀ y ∈ moves Player.right x, birthday y < o
    source
    theorem Form.birthday_eq_max {G : Type (u + 1)} [g_form : Form G] (x : G) :
    birthday x = max (⨆ (y : ↑(moves Player.left x)), Order.succ (birthday ↑y)) (⨆ (y : ↑(moves Player.right x)), Order.succ (birthday ↑y))
    source
    theorem Form.birthday_lt_of_mem_moves {G : Type (u + 1)} [g_form : Form G] {p : Player} {x y : G} (hy : y ∈ moves p x) :
    birthday y < birthday x
    source
    theorem Form.birthday_lt_of_isOption {G : Type (u + 1)} [g_form : Form G] {x y : G} (hy : IsOption y x) :
    birthday y < birthday x
    source
    @[irreducible]
    theorem Form.birthday_lt_of_subposition {G : Type (u + 1)} [g_form : Form G] {x y : G} (hy : Subposition y x) :
    birthday y < birthday x
    source
    @[simp, irreducible]
    theorem Form.birthday_neg {G : Type (u + 1)} [g_form : Form G] (x : G) :
    birthday (-x) = birthday x
    source
    @[simp, irreducible]
    theorem Form.birthday_add {G : Type (u + 1)} [g_form : Form G] (g h : G) :
    birthday (g + h) = birthday g + birthday h
    source
    theorem Form.birthday_add_lt_left {G : Type (u + 1)} [g_form : Form G] {g' g h : G} (hlt : birthday g' < birthday g) :
    birthday g' + birthday h < birthday g + birthday h
    source
    theorem Form.birthday_add_lt_right {G : Type (u + 1)} [g_form : Form G] {g h' h : G} (hlt : birthday h' < birthday h) :
    birthday g + birthday h' < birthday g + birthday h
    source
    @[simp]
    theorem Form.birthday_ofSets {G : Type (u + 1)} [g_form : Form G] (s t : Set G) [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] :
    birthday !{s | t} = max (sSup (Order.succ ∘ birthday '' s)) (sSup (Order.succ ∘ birthday '' t))
    source
    @[simp]
    theorem Form.birthday_ofSets_const {G : Type (u + 1)} [g_form : Form G] (s : Set G) [Small.{u, u + 1} ↑s] :
    birthday !{fun (x : Player) => s} = sSup (Order.succ ∘ birthday '' s)
    source
    @[simp]
    theorem Form.birthday_zero {G : Type (u + 1)} [g_form : Form G] :
    birthday 0 = 0
    source
    @[simp]
    theorem Form.birthday_one {G : Type (u + 1)} [g_form : Form G] :
    birthday 1 = 1
    source
    @[simp]
    theorem Form.birthday_natCast {G : Type (u + 1)} [g_form : Form G] (n : ℕ) :
    birthday ↑n = ↑n
    source
    @[simp]
    theorem Form.birthday_ofNat {G : Type (u + 1)} [g_form : Form G] (n : ℕ) [n.AtLeastTwo] :
    birthday (OfNat.ofNat n) = ↑n
    source
    @[simp]
    theorem Form.birthday_intCast {G : Type (u + 1)} [g_form : Form G] (k : ℤ) :
    birthday ↑k = ↑k.natAbs
    source
    def Form.tacticGameform_birthday :
    Lean.ParserDescr
    Equations
    Instances For