Section 4.3, paragraph 1Sprague–Grundy theorem; for NIM the Grundy value is the XOR of the heaps
External cited result A published result used as background or input; not proved in Lean here.
1 Paper text
The breadth of impartial games makes the Sprague–Grundy theorem remarkable: every finite terminating impartial position under normal play is equivalent to a single NIM heap of some size, called its nimber or Grundy value. Equivalence here means that replacing the position by that heap preserves the winning or losing status of its sum with any other such game. In a disjunctive sum, a move is made in exactly one component. The nimber of a sum is the bitwise XOR of the component nimbers; in particular, the nimber of a NIM board is the XOR of its heap sizes.
Generated from paper_jmlr.tex, lines 421–422.
2 Explain this
What equivalence means. In a disjunctive sum, each turn changes exactly one component. Replacing a component by its equivalent NIM heap preserves the winning or losing status with every other normal-play impartial component. This makes NIM central to the theory of a very broad class of games, even though computing the equivalent heap size can be difficult.
The Sprague–Grundy theorem says that every finite impartial game position behaves, in sums of games, like a single NIM heap of some size (its nimber or Grundy value). For NIM itself, the Grundy value of a position is the XOR of its heap sizes.
Caveat: the theorem guarantees that a nimber exists, not that it is easy to compute (see Section 8.3).
3 How this is formalised
The general theorem is classical background and is not formalised. For NIM, the fact that matters (losing exactly when the XOR is zero) is checked as Theorem 4.4.
| Paper anchor | sec-sprague-grundy-theory-and-nim-sum-p1 (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 4.3, paragraph 1 |
| Claim | Sprague–Grundy theorem; for NIM the Grundy value is the XOR of the heaps |
| Coverage category | External cited result |
| Statement source | paper_jmlr.tex lines 421–422; SHA-256 of the normalised block source 8a1ce9610f0ac932… |
| Depends on | Theorem 4.4 |
| Explanations | explain/c-sprague-grundy, formal/c-sprague-grundy |
| Build evidence | fresh isolated rebuild, audit report |
4 Lean statement and source
No Lean statement corresponds to this claim. This is a published classical result. It is cited, not proved in this Lean development.
Build evidence: fresh isolated rebuild of all 38 bundled modules with Lean (version 4.26.0, started 2026-10-10T15:21:56Z, finished 2026-10-10T15:27:00Z: 38/38 modules compiled, 1588 axiom reports, no errors. See Build for the commands and the independent audit of 2026-10-10 (dated evidence).