SetTheory.PGame.moveRight_nim'
theorem SetTheory.PGame.moveRight_nim' :
∀ {o : Ordinal.{u_1}} (i : (SetTheory.PGame.nim o).RightMoves),
(SetTheory.PGame.nim o).moveRight i = SetTheory.PGame.nim ↑(SetTheory.PGame.toRightMovesNim.symm i)
This theorem states that for any ordinal 'o' and any right move 'i' in the game of Nim on 'o', when the right player makes a move 'i' in this game, the resulting game position is the Nim game on the ordinal that corresponds to the inverse of 'i' under the mapping from initial ordinals less than 'o' to the set of right moves in the game of Nim on 'o'. In simple terms, this theorem is describing the dynamics of the game of Nim: when the right player makes a move, the game transitions to a state that corresponds to a smaller ordinal number.
More concisely: For any ordinal 'o' and right move 'i' in the game of Nim, the resulting game position is the Nim game on the ordinal 'o' corresponding to the inverse of 'i' under the mapping from initial ordinals to right moves.
|
SetTheory.PGame.grundyValue_eq_iff_equiv_nim
theorem SetTheory.PGame.grundyValue_eq_iff_equiv_nim :
∀ {G : SetTheory.PGame} [inst : G.Impartial] {o : Ordinal.{u_1}}, G.grundyValue = o ↔ G ≈ SetTheory.PGame.nim o
This theorem in set theory, specifically in the study of combinatorial games, states that for any impartial game `G` (a game where the allowable moves depend only on the position and not on which of the two players is currently moving), the Grundy value of `G` is equal to an ordinal `o` if and only if `G` is equivalent to a game of nim with `o` stones. Here equivalence means that the two games have the same outcome under optimal play. Nim is a particular type of game where players alternately take one or more stones from a single pile, with the player taking the last stone winning. The Grundy value of an impartial game is a kind of "nim-value" which measures how the game behaves under the mex (minimum excludant) operation.
More concisely: For any impartial game G in set theory, its Grundy value equals an ordinal o if and only if G is equivalent to a game of Nim with o stones under optimal play.
|
SetTheory.PGame.nim_def
theorem SetTheory.PGame.nim_def :
∀ (o : Ordinal.{u_1}),
let_fun this := ⋯;
SetTheory.PGame.nim o =
SetTheory.PGame.mk (Quotient.out o).α (Quotient.out o).α
(fun o₂ => SetTheory.PGame.nim (Ordinal.typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
SetTheory.PGame.nim (Ordinal.typein (fun x x_1 => x < x_1) o₂)
The theorem `SetTheory.PGame.nim_def` states that for any ordinal `o`, the game of single-heap nim with `o` stones is the game where each player can choose an index from `o` (represented as the equivalence class of the well-order `o`), and the moves are to play a game of nim with a heap size given by the order type of elements less than the chosen index in the well-order `o`. This highlights that the nature of a nim game is completely determined by the ordinal number of stones it starts with.
More concisely: For any ordinal number `o`, the game of single-heap nim with `o` stones is the recursively defined game where each player chooses an index from `o` and plays a game of nim with a heap size equal to the cardinality of the set of indices less than the chosen index in the well-order `o`.
|
SetTheory.PGame.toLeftMovesNim.proof_1
theorem SetTheory.PGame.toLeftMovesNim.proof_1 :
∀ {o : Ordinal.{u_1}}, (Quotient.out o).α = (SetTheory.PGame.nim o).LeftMoves
This theorem, named `SetTheory.PGame.toLeftMovesNim.proof_1`, states that for every ordinal `o`, the set of elements in the equivalence class represented by `o` (denoted as `(Quotient.out o).α`) is identical to the set of valid moves for the left player in the game of Nim with a heap size corresponding to the ordinal `o` (denoted as `SetTheory.PGame.LeftMoves (SetTheory.PGame.nim o)`). In other words, in the game of Nim, the valid moves for the left player are in one-to-one correspondence with the elements of the equivalence class defined by the ordinal number representing the size of the heap.
More concisely: For every ordinal `o`, the set of elements in the equivalence class represented by `o` is equal to the set of valid moves for the left player in the Nim game with heap size `o`.
|
SetTheory.PGame.grundyValue_nim_add_nim
theorem SetTheory.PGame.grundyValue_nim_add_nim :
∀ (n m : ℕ), (SetTheory.PGame.nim ↑n + SetTheory.PGame.nim ↑m).grundyValue = ↑(n ^^^ m)
This theorem states that the Grundy value (which is a concept related to game theory, specifically impartial games) of the sum of two Nim games (where each game has a pile of stones, and players take turns removing a positive number of stones from the pile), where each game has a natural number of piles, is equal to the bitwise XOR of the number of piles in the two games. In other words, given two natural numbers 'n' and 'm' that represent the number of piles in two Nim games, the Grundy value of the game that results from adding these two games together is equal to the natural number that results from applying the bitwise XOR operation to 'n' and 'm'.
More concisely: The Grundy value of the sum of two Nim games, each having a natural number of piles, is equal to the XOR of the number of piles in the respective games.
|
SetTheory.PGame.toRightMovesNim.proof_1
theorem SetTheory.PGame.toRightMovesNim.proof_1 :
∀ {o : Ordinal.{u_1}}, (Quotient.out o).α = (SetTheory.PGame.nim o).RightMoves
The theorem `SetTheory.PGame.toRightMovesNim.proof_1` states that for every ordinal `o`, the cardinality of the set of elements in `o` (denoted as `(Quotient.out o).α`) is equal to the set of right moves in the Game Theory scenario where the game is "nim" with `o` piles of stones. In the game of "nim", players take turns to remove any positive number of stones from any single pile, and the player who makes the last move (i.e., removes the last stone) wins.
More concisely: For every ordinal `o`, the cardinality of `Quotient.out o` equals the number of valid moves in the "nim" game with `o` piles.
|
SetTheory.PGame.equiv_nim_grundyValue
theorem SetTheory.PGame.equiv_nim_grundyValue :
∀ (G : SetTheory.PGame) [inst : G.Impartial], G ≈ SetTheory.PGame.nim G.grundyValue
The theorem `SetTheory.PGame.equiv_nim_grundyValue` is a statement of the Sprague-Grundy theorem in the context of set theory and game theory. This theorem asserts that every impartial game, denoted by `G`, is equivalent to a game of nim. More specifically, it's equivalent to the game of nim that corresponds to the Grundy value of the game `G`. An impartial game is one where the allowable moves and winning conditions are solely determined by the current position and not by which player is currently moving. The Grundy value of a game is a kind of "nim-value" that predicts the outcome of combinatorial games under optimal play.
More concisely: Every impartial game is equivalent to the game of nim with the same Grundy value.
|
SetTheory.PGame.moveLeft_nim'
theorem SetTheory.PGame.moveLeft_nim' :
∀ {o : Ordinal.{u}} (i : (SetTheory.PGame.nim o).LeftMoves),
(SetTheory.PGame.nim o).moveLeft i = SetTheory.PGame.nim ↑(SetTheory.PGame.toLeftMovesNim.symm i)
The theorem `SetTheory.PGame.moveLeft_nim'` states that for any ordinal 'o' and any legal left move 'i' in the game of Nim on 'o', making the move 'i' results in a game state equivalent to playing Nim on the ordinal obtained by applying the inverse of the function `toLeftMovesNim` to 'i'. In other words, it describes how the game state changes when the left player makes a move in the game of Nim.
More concisely: For any ordinal o and left move i in the game of Nim, making move i is equivalent to playing Nim on the ordinal obtained by applying the inverse of `toLeftMovesNim` to i.
|