Section 7.2, paragraph 1After any move from a zero-nim-sum position, every optimal reply restores nim-sum zero

Checked theorem Lean checks a formal statement corresponding to this claim.

1 Paper text

This experiment isolates the restoration response as a supervised learning problem. In normal-play impartial games, a restoration response is the move that returns play to a losing ( $P$ -)position after the opponent departs from it. In Nim, this is equivalent to selecting an optimal (winning) move from the post-opponent position: if the previous position had nim-sum $0$ , then after any opponent move the position is winning, and any optimal reply restores nim-sum $0$ .

Generated from paper_jmlr.tex, lines 1044–1046.

2 Explain this

In NIM, "restore after the opponent leaves a $P$ -position" is the same task as "find a winning move from the current position", provided the previous position had nim-sum zero: any opponent move from a zero nim-sum produces a nonzero one (a winning position for the agent), and every optimal reply returns to zero.

3 How this is formalised

Game.move_from_zero (every legal move from nim-sum zero reaches a nonzero nim-sum), Game.exists_move_to_zero (a move back to zero exists) and Game.lose_iff (the positions with nim-sum zero are exactly the losing ones, so "optimal" means "to nim-sum zero").

Coverage record
Paper anchor	`c-restoration-equivalence` (website anchor; the manuscript has no label here)
Displayed as	Section 7.2, paragraph 1
Claim	After any move from a zero-nim-sum position, every optimal reply restores nim-sum zero
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 1044–1046; SHA-256 of the normalised block source `267c518dee953357…`
Lean declarations	`NimAudit.Game.move_from_zero` (NimGame, lines 71–78, file `23df6bb87ecf…`) `NimAudit.Game.lose_iff` (NimGame, lines 108–115, file `23df6bb87ecf…`) `NimAudit.Game.exists_move_to_zero` (NimGame, lines 80–84, file `23df6bb87ecf…`)
Depends on	Theorem 4.4
Explanations	`explain/c-restoration-equivalence`, `formal/c-restoration-equivalence`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `Game.move_from_zero`

Module NimGame (lean/phase2/NimGame.lean, lines 71–78) · file SHA-256 23df6bb87ecfd344… Axioms reported by the fresh build: propext, Quot.sound

Every legal move from a zero-nim-sum board reaches a nonzero nim-sum.

Statement as elaborated and printed by Lean 4.26.0

∀ {p q : List ℕ}, NimAudit.Game.Move p q → NimAudit.nimSum p = 0 → NimAudit.nimSum q ≠ 0

Exact source text, lines 71–78

71/-- Every legal move from a zero-nim-sum board reaches a nonzero nim-sum. -/72theorem move_from_zero {p q : List Nat} (hm : Move p q) (h0 : nimSum p = 0) :73    nimSum q ≠ 0 := by74  obtain ⟨pre, x, post, y, rfl, rfl, hlt⟩ := hm75  rw [nimSum_move, h0, Nat.zero_xor]76  intro h77  have := xor_eq_zero_imp h78  omega

Project declarations in the statement: Game.Move, nimSum

Project declarations used by the proof or definition body

Game.Move, Game.nimSum_move, Game.xor_eq_zero_imp, nimSum

theorem `Game.lose_iff`

Module NimGame (lean/phase2/NimGame.lean, lines 108–115) · file SHA-256 23df6bb87ecfd344… Axioms reported by the fresh build: propext, Quot.sound

CLASSICAL CHARACTERISATION (paper Theorem nim-win).

Statement as elaborated and printed by Lean 4.26.0

∀ (p : List ℕ), NimAudit.Game.Lose p ↔ NimAudit.nimSum p = 0

Exact source text, lines 108–115

108/-- CLASSICAL CHARACTERISATION (paper Theorem nim-win). -/109theorem lose_iff (p : List Nat) : Lose p ↔ nimSum p = 0 := by110  constructor111  · intro hl112    by_cases h : nimSum p = 0113    · exact h114    · exact (not_win_and_lose p ((lose_of_zero_win_of_ne p).2 h) hl).elim115  · exact (lose_of_zero_win_of_ne p).1

Project declarations in the statement: Game.Lose, nimSum

Project declarations used by the proof or definition body

Game.Lose, Game.Win, Game.lose_of_zero_win_of_ne, Game.not_win_and_lose, nimSum

theorem `Game.exists_move_to_zero`

Module NimGame (lean/phase2/NimGame.lean, lines 80–84) · file SHA-256 23df6bb87ecfd344… Axioms reported by the fresh build: propext, Quot.sound

From a nonzero nim-sum there is a legal move to nim-sum zero (from NimRollout).

Statement as elaborated and printed by Lean 4.26.0

∀ {p : List ℕ}, NimAudit.nimSum p ≠ 0 → ∃ q, NimAudit.Game.Move p q ∧ NimAudit.nimSum q = 0

Exact source text, lines 80–84

80/-- From a nonzero nim-sum there is a legal move to nim-sum zero (from NimRollout). -/81theorem exists_move_to_zero {p : List Nat} (h : nimSum p ≠ 0) :82    ∃ q, Move p q ∧ nimSum q = 0 := by83  obtain ⟨pre, x, post, rfl, hlt, hz⟩ := exists_decreasing_heap p h84  exact ⟨_, ⟨pre, x, post, _, rfl, rfl, hlt⟩, hz⟩

Project declarations in the statement: Game.Move, nimSum

Project declarations used by the proof or definition body

Game.Move, Rollout.exists_decreasing_heap, nimSum

Definitions these statements use

def `Game.Move`

Module NimGame (lean/phase2/NimGame.lean, lines 24–26) · file SHA-256 23df6bb87ecfd344…

An ordinary legal Nim move: exactly one heap strictly decreases.

Statement as elaborated and printed by Lean 4.26.0

List ℕ → List ℕ → Prop

Exact source text, lines 24–26

24/-- An ordinary legal Nim move: exactly one heap strictly decreases. -/25def Move (p q : List Nat) : Prop :=26  ∃ pre x post y, p = pre ++ x :: post ∧ q = pre ++ y :: post ∧ y < x

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `nimSum`

Module NimCore (lean/NimCore.lean, lines 7–9) · file SHA-256 b07db6c505210d5a…

Statement as elaborated and printed by Lean 4.26.0

List ℕ → ℕ

Exact source text, lines 7–9

7def nimSum : List Nat → Nat8  | [] => 09  | h :: t => h ^^^ nimSum t

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

inductive `Game.Lose`

Module NimGame (lean/phase2/NimGame.lean, lines 39–40) · file SHA-256 23df6bb87ecfd344…

Statement as elaborated and printed by Lean 4.26.0

List ℕ → Prop

Exact source text, lines 39–40

39inductive Lose : List Nat → Prop40  | intro (p : List Nat) : (∀ q, Move p q → Win q) → Lose p

Project declarations in the statement: none

Project declarations used by the proof or definition body

Game.Move, Game.Win

Full modules

Module	File	Lines	Imports
NimCore	`lean/NimCore.lean`	139	`Std`
NimGame	`lean/phase2/NimGame.lean`	634	NimRollout

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).

Section 7.2, paragraph 1After any move from a zero-nim-sum position, every optimal reply restores nim-sum zero

1 Paper text

2 Explain this

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem Game.move_from_zero

theorem Game.lose_iff

theorem Game.exists_move_to_zero

Definitions these statements use

def Game.Move

def nimSum

inductive Game.Lose

Full modules

theorem `Game.move_from_zero`

theorem `Game.lose_iff`

theorem `Game.exists_move_to_zero`

def `Game.Move`

def `nimSum`

inductive `Game.Lose`