Section 4.1, paragraph 2Encoding decisive endings using terminal positions and a forced last move
Informal interpretation Motivation, interpretation or scope; not a formal claim.
1 Paper text
The last-move-wins convention also provides a convenient encoding of other decisive endings. A move that wins by capturing a designated piece or creating a specified configuration can simply lead to a position with no further legal moves. If instead reaching a special position loses for the player who made the move, give the opponent one forced move to a new terminal position. These encodings preserve the winner of the individual play; they must retain player-independent move rules to remain impartial. The theory below concerns the resulting normal-play game.
Generated from paper_jmlr.tex, lines 413–413.
2 Explain this
“Normal play” means that a player with no legal move loses. Many other decisive endings can be expressed with this convention. If a move wins by achieving a configuration, declare that configuration terminal. If the player making the move instead loses on reaching it, give the opponent one forced move to a new terminal position, so the opponent makes the last move.
This preserves the winner of the individual play, provided the encoding tracks the decisive event correctly. To obtain an impartial game, the resulting move rule must still be independent of player identity. It does not make chess impartial or resolve draws and infinite play. Nor does preserving an isolated game's winner imply that its sums under the original ending rule are equivalent: Sprague–Grundy theory applies to the resulting normal-play rules.
3 How this is formalised
This is an explanatory encoding observation, not a new Lean-checked theorem. The formalisation checks NIM with its usual last-move-wins rule; see Definition 4.2 and Theorem 4.4. General impartial games and their Sprague–Grundy theory remain classical background.
| Paper anchor | c-ending-encodings (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 4.1, paragraph 2 |
| Claim | Encoding decisive endings using terminal positions and a forced last move |
| Coverage category | Informal interpretation |
| Statement source | paper_jmlr.tex lines 413–413; SHA-256 of the normalised block source 1f85407c35f08576… |
| Depends on | Definition 4.1, Definition 4.2, Theorem 4.4 |
| Explanations | explain/c-ending-encodings, formal/c-ending-encodings |
| Build evidence | fresh isolated rebuild, audit report |
4 Lean statement and source
No Lean statement corresponds to this claim. This is interpretation or motivation, not a formal mathematical claim.
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).