Section 4.1, paragraph 1A position with no legal moves is terminal

A terminal position is one with no legal moves. In NIM, these are exactly the boards whose heaps are all empty; the player to move there has lost (normal play).

Game.Terminal defines a terminal board as one whose heaps are all zero, and Game.terminal_iff_no_move proves that this is equivalent to having no legal move.

Principal declarations

∀ (p : List ℕ), NimAudit.Game.Terminal p ↔ ∀ (q : List ℕ), ¬NimAudit.Game.Move p q

48theorem terminal_iff_no_move (p : List Nat) : Terminal p ↔ ∀ q, ¬ Move p q := by49  constructor50  · intro ht q ⟨pre, x, post, y, hp, _, hlt⟩51    have : x = 0 := ht x (by rw [hp]; simp)52    omega53  · intro hno x hx54    obtain ⟨pre, post, rfl⟩ := List.append_of_mem hx55    by_cases h0 : x = 056    · exact h057    · exact absurd ⟨pre, x, post, 0, rfl, rfl, by omega⟩ (hno (pre ++ 0 :: post))

Definitions these statements use

List ℕ → Prop

28/-- Terminal board: every heap is empty. -/29def Terminal (p : List Nat) : Prop := ∀ x ∈ p, x = 0

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