Definition 5.3The nimber difference Δ(P,P') = nim(P) ⊕ nim(P')

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

1 Paper text

Definition 5.3 (Nimber difference) Given consecutive positions $P$ and $P'$ in a play sequence, define the nimber difference $\Delta(P,P') \;=\; \operatorname{nim}(P)\ \oplus\ \operatorname{nim}(P').$

Generated from paper_jmlr.tex, lines 488–494.

2 Explain this

The nimber difference of two positions is the XOR of their nim-sums. Because XOR is its own inverse, $\operatorname{nim}(P') = \operatorname{nim}(P)\oplus\Delta(P,P')$ : the difference is exactly what has to be "cancelled" to get from one invariant to the other.

3 How this is formalised

Lean does not introduce a separate name: the difference is written nimSum P ^^^ nimSum P' wherever it is used. The key property is one_heap_difference (next record).

Coverage record
Paper anchor	`def:nimber-difference` (manuscript label)
Displayed as	Definition 5.3
Claim	The nimber difference Δ(P,P') = nim(P) ⊕ nim(P')
Coverage category	Checked definition or construction
Statement source	paper_jmlr.tex lines 488–494; SHA-256 of the normalised block source `787b3d99be2e3250…`
Lean declarations	`NimAudit.one_heap_difference` (NimCore, lines 37–39, file `b07db6c50521…`)
Prose-to-formal notes	Lean writes $\Delta$ inline as `nimSum P ^^^ nimSum P'`; there is no separate named definition.
Audited correspondence rows	`def:nimber-difference`
Explanations	`explain/def:nimber-difference`, `formal/def:nimber-difference`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `one_heap_difference`

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

Statement as elaborated and printed by Lean 4.26.0

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

Exact source text, lines 37–39

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]

Project declarations in the statement: nimSum

Project declarations used by the proof or definition body

nimSum, nimSum_append, xor_left_comm

Definitions these statements use

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

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