Section 5.4, “The initialisation boundary for restoration”Matching deltas preserves nim(Q); a completed matching-delta policy loses from the winning position (2)

Matching the last difference only says $\operatorname{nim}(R)=\operatorname{nim}(Q)$. If $Q$ did not have nim-sum zero, neither does $R$. So restoration cannot, by itself, tell whether an arbitrary starting position is winning.

Counterexample. Complete a matching-delta policy by "subtract one from the first nonempty heap" whenever no matching reply exists or no previous frame is available. From $(2)$, a winning position, the first player plays $(2)\to(1)$ (no previous frame). The opponent's reply from $(1)$ is computed by the same policy: the difference to match is $2\oplus1=3$, which cannot be realised from $(1)$, so it falls back and plays $(1)\to(0)$. The first player has lost from a winning position.

What it shows: conditional restoration plus an unspecified fallback is not a verifier. It does not rule out every possible verifier. Initial moves can come from the multi-channel construction or the recurrent scan instead.

• Misc.init_counterexample checks the counterexample step by step: $(2)$ is winning; the completed policy Misc.mdPolicy plays $(2)\to(1)$; no move from $(1)$ cancels $2\oplus1$; the fallback plays $(1)\to(0)$; $(1)$ is winning and $(0)$ is losing.
• Rollout.matching_deltas_do_not_force_zero: the universal statement "matching deltas forces nim-sum zero" is false without the zero promise; no_zero_without_zero_promise is the concrete instance $1\oplus3=3\oplus1$ with $1\ne0$.

Principal declarations

NimAudit.Game.Win [2] ∧
  NimAudit.Misc.mdPolicy none [2] = some [1] ∧
    NimAudit.Game.cancelFirst (NimAudit.nimSum [2] ^^^ NimAudit.nimSum [1]) [1] = none ∧
      NimAudit.Misc.mdPolicy (some [2]) [1] = some [0] ∧
        NimAudit.Game.Win [1] ∧ NimAudit.Game.Lose [0]

707/-- From the winning position (2) the completed matching-delta policy plays (2) → (1) and708    then (as the next mover, delta 2 ⊕ 1 = 3 is not realisable from (1)) (1) → (0): the709    first player loses although (2) is winning. -/710theorem init_counterexample :711    Win [2] ∧ mdPolicy none [2] = some [1] ∧ cancelFirst (nimSum [2] ^^^ nimSum [1]) [1] = none ∧712    mdPolicy (some [2]) [1] = some [0] ∧ Win [1] ∧ Lose [0] := by713  refine ⟨(win_iff _).2 (by decide), by decide, by decide, by decide, (win_iff _).2 (by decide),714    (lose_iff _).2 (by decide)⟩

¬∀ (q q' r : ℕ), q ^^^ q' = q' ^^^ r → r = 0

318/-- Matching deltas alone never force a zero result: the universal statement is false. -/319theorem matching_deltas_do_not_force_zero :320    ¬ ∀ q q' r : Nat, q ^^^ q' = q' ^^^ r → r = 0 := by321  intro h322  have := h 1 3 1 (by decide)323  exact absurd this (by decide)

1 ^^^ 3 = 3 ^^^ 1 ∧ 1 ≠ 0

72theorem no_zero_without_zero_promise :73    (1 ^^^ 3 = 3 ^^^ 1) ∧ (1 : Nat) ≠ 0 := by decide

Definitions these statements use

Option (List ℕ) → List ℕ → Option (List ℕ)

698/-- The matching-delta policy completed by "subtract one from the first nonempty heap"699    whenever there is no previous frame or no matching response. -/700def mdPolicy (prev : Option (List Nat)) (cur : List Nat) : Option (List Nat) :=701  match prev with702  | none => subFirstPos cur703  | some Q => match cancelFirst (nimSum Q ^^^ nimSum cur) cur with704    | some R => some R705    | none => subFirstPos cur

List ℕ → Prop

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

List ℕ → Prop

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

ℕ → List ℕ → Option (List ℕ)

244/-- Replace the first heap x with x ^^^ s < x by x ^^^ s. -/245def cancelFirst (s : Nat) : List Nat → Option (List Nat)246  | [] => none247  | x :: t => if x ^^^ s < x then some ((x ^^^ s) :: t) else (cancelFirst s t).map (x :: ·)

List ℕ → ℕ

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

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