Definition 4.2NIM positions and legal moves

Checked definition or construction Lean contains the definition or construction, with checked properties.

1 Paper text

Definition 4.2 (NIM) A NIM position consists of $h$ heaps with sizes $x_1,\dots,x_h\in\N_0$ . A legal move reduces exactly one heap: choose $i$ with $x_i>0$ and replace $x_i$ by some $x_i'<x_i$ .

Generated from paper_jmlr.tex, lines 416–419.

2 Explain this

A NIM position is a list of heap sizes. A move picks one nonempty heap and replaces it by any strictly smaller size. Example: from $(3,5,6)$ one legal move is $(3,4,6)$ ; $(3,5,7)$ is not a move (heaps never grow), and neither is $(2,4,6)$ (two heaps changed).

3 How this is formalised

Game.Move: $q$ is reached from $p$ when $p = \mathit{pre} \mathbin{+!!+} [x] \mathbin{+!!+} \mathit{post} $and$ q = \mathit{pre}\mathbin{+!!+}[y]\mathbin{+!!+}\mathit{post} $with$ y<x$: exactly one heap strictly decreases and the heap positions stay aligned. Game.move_sum_lt proves that every move lowers the total number of stones, which is how termination is proved throughout.

Coverage record
Paper anchor	`def:nim` (manuscript label)
Displayed as	Definition 4.2
Claim	NIM positions and legal moves
Coverage category	Checked definition or construction
Statement source	paper_jmlr.tex lines 416–419; SHA-256 of the normalised block source `a7ecd52cdc483f24…`
Lean declarations	`NimAudit.Game.Move` (NimGame, lines 24–26, file `23df6bb87ecf…`) `NimAudit.Game.move_sum_lt` (NimGame, lines 43–46, file `23df6bb87ecf…`)
Audited correspondence rows	`def:nim`
Explanations	`explain/def:nim`, `formal/def:nim`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

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

theorem `Game.move_sum_lt`

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

Statement as elaborated and printed by Lean 4.26.0

∀ {p q : List ℕ}, NimAudit.Game.Move p q → q.sum < p.sum

Exact source text, lines 43–46

43theorem move_sum_lt {p q : List Nat} (hm : Move p q) : q.sum < p.sum := by44  obtain ⟨pre, x, post, y, rfl, rfl, hlt⟩ := hm45  simp only [List.sum_append_nat, List.sum_cons]46  omega

Project declarations in the statement: Game.Move

Project declarations used by the proof or definition body

Game.Move

Full modules

Module	File	Lines	Imports
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).