Theorem 4.4A NIM position is losing iff its nim-sum is zero; from a nonzero nim-sum there is a move to zero

The statement. A position is lost for the player to move exactly when the nim-sum is zero. From any position with nonzero nim-sum there is a move that makes it zero.

Example. $(3,5,6)$ has nim-sum $0$: whatever you do, the opponent can restore zero, and eventually you face the empty board. $(3,4,6)$ has nim-sum $1$: reducing $3$ to $2$ makes it zero.

Why it matters. Optimal play is "always move to nim-sum zero". The rule is short and exact, yet it requires the XOR of all heaps, a global parity computation.

How to find the move. Let $s\ne0$ be the nim-sum and $k$ its highest set bit. Some heap $x$ has bit $k$ set; then $x\oplus s<x$, and replacing $x$ by $x\oplus s$ makes the nim-sum $0$.

Semantics. Game.Win and Game.Lose are defined together, by induction, as the normal-play notions for the player to move: a position is winning if some move reaches a losing position; it is losing if every move reaches a winning position (so a terminal position is losing).

Checked statements.

• Game.lose_iff: Lose p ↔ nimSum p = 0, for every board.
• Game.win_iff: Win p ↔ nimSum p ≠ 0.
• Game.exists_move_to_zero: from a nonzero nim-sum some legal move reaches nim-sum zero (the top-bit argument above, proved in Rollout.exists_decreasing_heap).
• Game.move_from_zero: every legal move from a zero nim-sum reaches a nonzero one.

The theorem is the classical one; Lean checks it in exactly the paper's form, for any number of heaps.

Principal declarations

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

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

∀ (p : List ℕ), NimAudit.Game.Win p ↔ NimAudit.nimSum p ≠ 0

117theorem win_iff (p : List Nat) : Win p ↔ nimSum p ≠ 0 := by118  constructor119  · intro hw h120    exact not_win_and_lose p hw ((lose_of_zero_win_of_ne p).1 h)121  · exact (lose_of_zero_win_of_ne p).2

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

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⟩

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

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

Definitions these statements use

List ℕ → Prop

37inductive Win : List Nat → Prop38  | intro (p q : List Nat) : Move p q → Lose q → Win p

List ℕ → Prop

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

List ℕ → ℕ

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

List ℕ → List ℕ → Prop

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

Full modules

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