Section 5.3, paragraph 2If one heap changes from x_i to x_i', then Δ = x_i ⊕ x_i'

When a move changes only heap $i$ from $x_i$ to $x_i'$, all other heaps appear in both nim-sums and cancel, so $\Delta(P,P') = x_i\oplus x_i'$. Example: $(3,5,6)\to(3,4,6)$ gives $\Delta = 5\oplus4 = 1$.

So computing $\Delta$ needs only the changed heap, not a parity over all heaps.

one_heap_difference: for lists $\mathit{pre}$, $\mathit{post}$ and values $a,b$, the nim-sums of $\mathit{pre}\mathbin{+\!\!+}[a]\mathbin{+\!\!+}\mathit{post}$ and $\mathit{pre}\mathbin{+!!+}[b]\mathbin{+!!+} \mathit{post}$differ by$a\oplus b$. Misc.delta_bit_local gives the bitwise form for any legal move: bit $k$ of the difference is $a_k\oplus b_k$.

Principal declarations

∀ (pre post : List ℕ) (a b : ℕ),
  NimAudit.nimSum (pre ++ a :: post) ^^^ NimAudit.nimSum (pre ++ b :: post) = a ^^^ b

37theorem one_heap_difference (pre post : List Nat) (a b : Nat) :38    nimSum (pre ++ a :: post) ^^^ nimSum (pre ++ b :: post) = a ^^^ b := by39  simp [nimSum_append, nimSum, Nat.xor_comm, xor_left_comm]

∀ {Q Q' : List ℕ},
  NimAudit.Game.Move Q Q' →
    ∃ pre a post b,
      Q = pre ++ a :: post ∧
        Q' = pre ++ b :: post ∧
          ∀ (k : ℕ),
            (NimAudit.nimSum Q ^^^ NimAudit.nimSum Q').testBit k = (a.testBit k ^^ b.testBit k)

687/-- DELTA BITS ARE TWO-COORDINATE CHARACTERS: across one legal move (heap value a → b),688    bit k of the difference is a_k ⊕ b_k. -/689theorem delta_bit_local {Q Q' : List Nat} (hm : Move Q Q') :690    ∃ pre a post b, Q = pre ++ a :: post ∧ Q' = pre ++ b :: post ∧691      ∀ k, (nimSum Q ^^^ nimSum Q').testBit k = xor (a.testBit k) (b.testBit k) := by692  obtain ⟨pre, a, post, b, h1, h2, _⟩ := hm693  refine ⟨pre, a, post, b, h1, h2, fun k => ?_⟩694  rw [h1, h2, one_heap_difference, Nat.testBit_xor]

Definitions these statements use

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