Definition 4.3The nim-sum is the bitwise XOR of the heap sizes

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

1 Paper text

Definition 4.3 (Nim-sum) For heap sizes $x_1,\dots,x_h$ , define $\operatorname{nim}(x_1,\dots,x_h) \;=\; x_1 \oplus x_2 \oplus \cdots \oplus x_h,$ where $\oplus$ denotes bitwise XOR.

Generated from paper_jmlr.tex, lines 424–431.

2 Explain this

The nim-sum of heap sizes is their bitwise XOR: write each size in binary and, in each bit position, count the ones; the result has a 1 exactly where that count is odd. Example: $3\oplus5\oplus6$ : $011\oplus101\oplus110 = 000 $, so the nim-sum is$ 0$.

Each bit of the nim-sum is therefore a parity over all heaps, which is what makes it hard for shallow circuits.

3 How this is formalised

nimSum folds Lean's bitwise XOR over the list of heaps (empty board: $0$ ). nimSum_append proves that the nim-sum of two concatenated lists is the XOR of their nim-sums, the basic tool for local reasoning about one changed heap.

Coverage record
Paper anchor	`def:nimsum` (manuscript label)
Displayed as	Definition 4.3
Claim	The nim-sum is the bitwise XOR of the heap sizes
Coverage category	Checked definition or construction
Statement source	paper_jmlr.tex lines 424–431; SHA-256 of the normalised block source `c868301621191346…`
Lean declarations	`NimAudit.nimSum` (NimCore, lines 7–9, file `b07db6c50521…`) `NimAudit.nimSum_append` (NimCore, lines 20–24, file `b07db6c50521…`)
Audited correspondence rows	`def:nimsum`
Explanations	`explain/def:nimsum`, `formal/def:nimsum`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

def `nimSum`

Module NimCore (lean/NimCore.lean, lines 7–9) · file SHA-256 b07db6c505210d5a…

Statement as elaborated and printed by Lean 4.26.0

List ℕ → ℕ

Exact source text, lines 7–9

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

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

theorem `nimSum_append`

Module NimCore (lean/NimCore.lean, lines 20–24) · file SHA-256 b07db6c505210d5a… Axioms reported by the fresh build: propext, Quot.sound

Statement as elaborated and printed by Lean 4.26.0

∀ (xs ys : List ℕ), NimAudit.nimSum (xs ++ ys) = NimAudit.nimSum xs ^^^ NimAudit.nimSum ys

Exact source text, lines 20–24

20theorem nimSum_append (xs ys : List Nat) :21    nimSum (xs ++ ys) = nimSum xs ^^^ nimSum ys := by22  induction xs with23  | nil => simp [nimSum]24  | cons h t ih => simp [nimSum, ih, Nat.xor_assoc]

Project declarations in the statement: nimSum

Project declarations used by the proof or definition body

nimSum

Full modules

Module	File	Lines	Imports
NimCore	`lean/NimCore.lean`	139	`Std`

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