SetTheory.PGame.birthday_def
theorem SetTheory.PGame.birthday_def :
∀ (x : SetTheory.PGame),
x.birthday =
max (Ordinal.lsub fun i => (x.moveLeft i).birthday) (Ordinal.lsub fun i => (x.moveRight i).birthday)
The theorem `SetTheory.PGame.birthday_def` states that for any pre-game `x`, the birthday of `x` is defined as the maximum of two values: the least strict upper bound of the birthdays of the games resulting from all possible left moves from `x`, and the least strict upper bound of the birthdays of the games resulting from all possible right moves from `x`. In other words, the birthday of a game is determined by the highest birthday of any subsequent game that can be reached by making a legal move, either by the Left or the Right player.
More concisely: The birthday of a pre-game is the maximum of the least upper bounds of the birthdays of its possible left and right successor games.
|
SetTheory.PGame.birthday_zero
theorem SetTheory.PGame.birthday_zero : SetTheory.PGame.birthday 0 = 0
This theorem states that the "birthday" of the zero game in set theory is zero. The birthday of a pre-game is defined as the least strict upper bound of the birthdays of its left and right games. In the context of games, it can be viewed as the "step" in which a certain game is constructed. In the case of the zero game, since there are no preceding steps (or in other words, no left or right games), its birthday is thus defined to be zero.
More concisely: The birthday of the zero game in set theory is defined as 0.
|
SetTheory.PGame.birthday_one
theorem SetTheory.PGame.birthday_one : SetTheory.PGame.birthday 1 = 1
This theorem states that the "birthday" of the pre-game `1` in Set theory is `1`. Here, the birthday of a pre-game is defined inductively as the least strict upper bound of the birthdays of its left and right games, which can be thought of as the "step" in which a certain game is constructed. So in this case, the construction "step" of the pre-game `1` is `1`.
More concisely: The birthday of the pre-game 1 in Set theory is 1.
|
SetTheory.PGame.birthday_add
theorem SetTheory.PGame.birthday_add : ∀ (x y : SetTheory.PGame), (x + y).birthday = x.birthday.nadd y.birthday := by
sorry
This theorem states that for any two pre-games `x` and `y`, the "birthday" of their sum (`x + y`) is equal to the Hessenberg sum (or natural addition) of their individual birthdays. The birthday of a pre-game is conceptually the "step" in which the game is constructed, while the Hessenberg sum is a form of ordinal addition that is commutative and based on adding up corresponding coefficients in the Cantor normal forms of the ordinals.
More concisely: For any pre-games x and y, the birthday of their sum (x + y) equals the Hessenberg sum of their individual birthdays.
|