English
The Sprague-Grundy theorem asserts that impartial G is equivalent to Nim of its Grundy value; explicitly, G ≈ nim(toOrdinal(grundyValue G)).
Русский
Теорема Спрага-Гранд утверждает, что беспристрастная G эквивалентна Nim с её значением Гранди; то есть G ≈ nim(toOrdinal(grundyValue G)).
LaTeX
$$$ G \approx nim\bigl(toOrdinal(\operatorname{grundyValue}(G))\bigr). $$$
Lean4
/-- The **Sprague-Grundy theorem** states that every impartial game is equivalent to a game of nim,
namely the game of nim corresponding to the game's Grundy value. -/
theorem equiv_nim_grundyValue (G : PGame.{u}) [G.Impartial] : G ≈ nim (toOrdinal (grundyValue G)) :=
by
rw [Impartial.equiv_iff_add_equiv_zero, ← Impartial.forall_leftMoves_fuzzy_iff_equiv_zero]
intro x
apply leftMoves_add_cases x <;> intro i
· rw [add_moveLeft_inl, ← fuzzy_congr_left (add_congr_left (Equiv.symm (equiv_nim_grundyValue _))),
nim_add_fuzzy_zero_iff]
exact grundyValue_ne_moveLeft i
· rw [add_moveLeft_inr, ← Impartial.exists_left_move_equiv_iff_fuzzy_zero]
obtain ⟨j, hj⟩ := exists_grundyValue_moveLeft_of_lt <| toLeftMovesNim_symm_lt i
use toLeftMovesAdd (Sum.inl j)
rw [add_moveLeft_inl, moveLeft_nim]
exact Equiv.trans (add_congr_left (equiv_nim_grundyValue _)) (hj ▸ Impartial.add_self _)
termination_by G
