Section 5.3.1, paragraph 2Testing whether a candidate move realises δ is a local check on the heap being changed

Checked theorem Lean checks a formal statement corresponding to this claim.

1 Paper text

Proposition 5.5 is structural: it describes a response pattern that keeps returning the game to nim-sum zero, provided the player can (i) compute $\delta=\Delta(Q,Q')$ from the last two frames and (ii) choose a legal move $Q'\to R$ that realises the same $\delta$ . In NIM, when the opponent changes exactly one heap, $\delta$ is simply $x_i\oplus x_i'$ , and testing whether a candidate response move realises $\delta$ is a local check on the heap being changed.

Generated from paper_jmlr.tex, lines 610–610.

2 Explain this

Two local facts make the response pattern shallow. First, when the opponent changes one heap, $\delta$ is that heap's old value XOR its new value. Second, whether changing heap $i$ realises $\delta$ legally is a test on heap $i$ alone: $x_i\oplus\delta<x_i$ holds exactly when $x_i$ has a 1 at the highest set bit of $\delta$ .

Two-frame restoration, step by step

Exact construction trace Every value is computed from the construction’s definitions for the example shown.

This is the checked two-frame selector run on one example, gate group by gate group. It starts from the two frames of Figure 2 and ends with the binary output fields shown in Figure 7. Every value below is computed from the selector's definition for the boards shown. Choose another example to see several candidates at once, the fallback, or a terminal board. The two examples marked "outside the promise" do not start from a zero-nim-sum board after a legal move, so the guarantee does not apply to them.

Inside the promise. The earlier board has nim-sum 0 and the opponent decreased one heap, so the restoration theorem guarantees that the output restores nim-sum 0.

Earlier board Q (3, 5, 6)nim-sum 0

Current board Q′ (3, 4, 6)nim-sum 1; changed: heap 1

After the reply (2, 4, 6)nim-sum 0; reply in heap 0

Compare the frames bit by bit
Each heap is a 3-bit block. For every heap and every bit position, one two-input XOR compares Q with Q′, all in parallel.
Heap Q Q′ XOR Heap
0 3 011 3 011 000 same
1 5 101 4 100 001 changed
2 6 110 6 110 000 same
Extract the difference δ
Bit k of δ is the OR of column k of the XOR table: 001 = δ = 1.
At most one heap changed, so at most one row is nonzero and the OR equals the XOR of the rows, which is nim(Q) ⊕ nim(Q′).
Propose replacements and test them in parallel
For every heap at once: replace Q′_i by Q′_i ⊕ δ and test whether that is a decrease. The decisive bit is the highest set bit of δ (weight 1): a heap passes exactly when it has that bit set.
Heap Q′ Q′ ⊕ δ Test
0 3 011 2 010 passes: 2 < 3
1 4 100 5 101 fails: 5 > 4
2 6 110 7 111 fails: 7 > 6
Show the bit comparisons
The test x ⊕ δ < x is a fixed-depth circuit: an OR over the possible highest differing bit, requiring equality above it, a 1 in x and a 0 in the replacement at that bit.
- Heap 0: 011 vs 010 — the highest differing bit has weight 1; the heap has 1 there, so the replacement is smaller.
- Heap 1: 100 vs 101 — the highest differing bit has weight 1; the heap has 0 there, so the replacement is larger.
- Heap 2: 110 vs 111 — the highest differing bit has weight 1; the heap has 0 there, so the replacement is larger.
Candidates passing: 1.
Choose between cancelling and the fallback
cancelling move At least one replacement passes, so the flags are the passing tests and the fallback is masked off.
Heap passes nonzero fallback value flag s_i
0 1 1 3 − 1 = 2 1
1 0 1 4 − 1 = 3 0
2 0 1 6 − 1 = 5 0
Encode the first flagged heap as a binary index
For N = 3 heaps the construction uses r = ⌊log₂ N⌋ + 1 = 2 index bits (the encoder itself needs only N ≤ 2^r). The first flag is at heap 0, so the index bits are 00.
Show the priority encoder
f_i = s_i ∧ ¬s_j for all j < i keeps only the first flag; index bit k is the OR of f_i over the heaps i whose binary index has a 1 at bit k. This is a fixed-depth circuit, not a search.
Heap i i in binary s_i first f_i
0 00 1 1
1 01 0 0
2 10 0 0
Index bits (OR of the f_i in each 1-column): 00
Output the move
validity1index (2 bits)00value (3 bits)010
Decoded move: set heap 0 to 2. New board (2, 4, 6), nim-sum 0.

Heap	Q	Q′	XOR	Heap
0	3 011	3 011	000	same
1	5 101	4 100	001	changed
2	6 110	6 110	000	same

Heap	Q′	Q′ ⊕ δ	Test
0	3 011	2 010	passes: 2 < 3
1	4 100	5 101	fails: 5 > 4
2	6 110	7 111	fails: 7 > 6

Heap	passes	nonzero	fallback value	flag s_i
0	1	1	3 − 1 = 2	1
1	0	1	4 − 1 = 3	0
2	0	1	6 − 1 = 5	0

Heap i	i in binary	s_i	first f_i
0	00	1	1
1	01	0	0
2	10	0	0

How this relates to the Lean proof. The selector is Family.restS (B, N): the local difference circuits LocalRestore.dC, the candidate tests of SelectCircuit.varSel and the priority encoder PriorityEncoder.encode, read on the two-frame input LocalRestore.tf. Family.rest_semantics proves that, on the promised domain, these formulas and the compiled network output a legal move that restores nim-sum 0. Outside the promise the circuit still computes the values shown, and no theorem says that the result restores 0.

What this does not show. The selector does not find a first winning move from an arbitrary board. Given a zero-nim-sum predecessor it maintains the invariant (Theorem 5.12(iii)). The boxes of Figure 7 group operations; the stages here group gates, not network layers.

Depicted in Lean: Family.rest_semantics, LocalRestore.restore_equiv, LocalRestore.localDelta_eq, LocalRestore.restC_eval, SelectCircuit.varSel_correct, AttainCircuit.cancel_iff_bit, PriorityEncoder.encode_correct, Family.rest_ac0, Family.rest_net. Explains the paper’s Figure 2, Figure 7.

Computed in your browser by a short re-implementation of the definitions above (tools/visuals/nimvis-core.js). It is not itself checked by Lean. At build time it agreed with Lean's own evaluation of those definitions on all 12,299 reference cases. Lean's evaluation fixes the output wires, the difference δ and the decoded move; the intermediate tables (flags, first-flag bits) are re-derived from the same definitions.

3 How this is formalised

AttainCircuit.cancel_iff_bit: for $t\neq0$ , $x\oplus t<x$ iff bit $\lfloor\log_2 t\rfloor$ of $x$ is set (one input literal). LocalRestore.localDelta_eq: the OR-of-XORs delta read off the two frames equals $\operatorname{nim}(Q)\oplus\operatorname{nim}(Q')$ whenever the frames differ in at most one heap.

Coverage record
Paper anchor	`par-interpretation-mirror-the-delta-p2` (website anchor; the manuscript has no label here)
Displayed as	Section 5.3.1, paragraph 2
Claim	Testing whether a candidate move realises δ is a local check on the heap being changed
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 610–610; SHA-256 of the normalised block source `8d048be4dc49977c…`
Lean declarations	`NimAudit.AttainCircuit.cancel_iff_bit` (AttainCircuit, lines 29–62, file `13b98daabaa9…`) `NimAudit.LocalRestore.localDelta_eq` (LocalRestore, lines 153–174, file `fc4c7f908b0c…`)
Depends on	Proposition 5.5, Section 5.3, paragraph 2
Explanations	`explain/c-mirror-delta`, `formal/c-mirror-delta`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `AttainCircuit.cancel_iff_bit`

Module AttainCircuit (lean/phase3/AttainCircuit.lean, lines 29–62) · file SHA-256 13b98daabaa917e5… Axioms reported by the fresh build: propext, Quot.sound

x XOR t < x iff x has t's top bit (t ≠ 0).

Statement as elaborated and printed by Lean 4.26.0

∀ {x t : ℕ}, t ≠ 0 → (x ^^^ t < x ↔ x.testBit t.log2 = true)

Exact source text, lines 29–62

29/-- x XOR t < x iff x has t's top bit (t ≠ 0). -/30theorem cancel_iff_bit {x t : Nat} (ht : t ≠ 0) : x ^^^ t < x ↔ x.testBit t.log2 = true := by31  have htk : t.testBit t.log2 = true := by32    cases hb : t.testBit t.log2 with33    | true => rfl34    | false =>35      exfalso36      have hlt : t < 2 ^ t.log2 := by37        apply Nat.lt_pow_two_of_testBit38        intro i hi39        by_cases hik : i = t.log240        · subst hik; exact hb41        · exact Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le Nat.lt_log2_self42            (Nat.pow_le_pow_right (by decide) (by omega)))43      exact absurd (Nat.log2_self_le ht) (Nat.not_le.mpr hlt)44  have habove : ∀ i, t.log2 < i → t.testBit i = false := fun i hi =>45    Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le Nat.lt_log2_self46      (Nat.pow_le_pow_right (by decide) (by omega)))47  constructor48  · intro hlt49    cases hx : x.testBit t.log2 with50    | true => rfl51    | false =>52      exfalso53      have : x < x ^^^ t := by54        apply lt_of_top_testBit (k := t.log2) hx55        · rw [Nat.testBit_xor, hx, htk]; rfl56        · intro i hi; rw [Nat.testBit_xor, habove i hi, Bool.xor_false]57      omega58  · intro hx59    apply lt_of_top_testBit (k := t.log2)60    · rw [Nat.testBit_xor, hx, htk]; rfl61    · exact hx62    · intro i hi; rw [Nat.testBit_xor, habove i hi, Bool.xor_false]

Project declarations in the statement: none

Project declarations used by the proof or definition body

Rollout.lt_of_top_testBit

theorem `LocalRestore.localDelta_eq`

Module LocalRestore (lean/phase4/LocalRestore.lean, lines 153–174) · file SHA-256 fc4c7f908b0c9c58… Axioms reported by the fresh build: propext, Quot.sound

SINGLE-CHANGE DELTA: on frames differing in at most one heap the local delta is nim(Q) ⊕ nim(Q').

Statement as elaborated and printed by Lean 4.26.0

∀ {B N : ℕ} {Q Q' : List ℕ},
  Q.length = N →
    Q'.length = N →
      NimAudit.Game.Width B Q →
        NimAudit.Game.Width B Q' →
          NimAudit.LocalRestore.OneChange Q Q' →
            NimAudit.LocalRestore.localDelta B N Q Q' = NimAudit.nimSum Q ^^^ NimAudit.nimSum Q'

Exact source text, lines 153–174

153/-- SINGLE-CHANGE DELTA: on frames differing in at most one heap the local delta is154    nim(Q) ⊕ nim(Q'). -/155theorem localDelta_eq {B N : Nat} {Q Q' : List Nat} (hQ : Q.length = N) (hQ' : Q'.length = N)156    (hw : Width B Q) (hw' : Width B Q') (h1 : OneChange Q Q') :157    localDelta B N Q Q' = nimSum Q ^^^ nimSum Q' := by158  apply ofBits_testBit_eq (Nat.xor_lt_two_pow (nimSum_lt hw) (nimSum_lt hw'))159  intro q _160  rcases h1 with rfl | ⟨pre, x, post, y, rfl, rfl⟩161  · simp162  · rw [delta_oneChange, Nat.testBit_xor]163    have hN : N = pre.length + 1 + post.length := by rw [← hQ]; simp; omega164    apply Bool.eq_iff_iff.mpr165    simp only [List.any_eq_true, List.mem_range, getD_split]166    constructor167    · rintro ⟨i, _, hi⟩168      by_cases h1 : i < pre.length169      · simp [h1] at hi170      · by_cases h2 : i = pre.length171        · simpa [h2] using hi172        · simp [h1, h2] at hi173    · intro h174      exact ⟨pre.length, by omega, by simpa using h⟩

Project declarations in the statement: Game.Width, LocalRestore.OneChange, LocalRestore.localDelta, nimSum

Project declarations used by the proof or definition body

Game.Width, Game.nimSum_lt, LocalRestore.OneChange, LocalRestore.delta_oneChange, LocalRestore.getD_split, Recurrent.ofBits_testBit_eq, nimSum

Definitions these statements use

def `Game.Width`

Module NimGame (lean/phase2/NimGame.lean, lines 31–32) · file SHA-256 23df6bb87ecfd344…

B-bit board: every heap is below 2^B.

Statement as elaborated and printed by Lean 4.26.0

ℕ → List ℕ → Prop

Exact source text, lines 31–32

31/-- B-bit board: every heap is below 2^B. -/32def Width (B : Nat) (p : List Nat) : Prop := ∀ x ∈ p, x < 2 ^ B

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `LocalRestore.OneChange`

Module LocalRestore (lean/phase4/LocalRestore.lean, lines 99–101) · file SHA-256 fc4c7f908b0c9c58…

The frames differ in at most one heap.

Statement as elaborated and printed by Lean 4.26.0

List ℕ → List ℕ → Prop

Exact source text, lines 99–101

99/-- The frames differ in at most one heap. -/100def OneChange (Q Q' : List Nat) : Prop :=101  Q = Q' ∨ ∃ pre x post y, Q = pre ++ x :: post ∧ Q' = pre ++ y :: post

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `LocalRestore.localDelta`

Module LocalRestore (lean/phase4/LocalRestore.lean, lines 132–134) · file SHA-256 fc4c7f908b0c9c58…

The local delta value read off the circuit (no promise).

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → List ℕ → List ℕ → ℕ

Exact source text, lines 132–134

132/-- The local delta value read off the circuit (no promise). -/133def localDelta (B N : Nat) (Q Q' : List Nat) : Nat :=134  ofBits B (fun q => (List.range N).any (fun i => (Q.getD i 0).testBit q != (Q'.getD i 0).testBit q))

Project declarations in the statement: none

Project declarations used by the proof or definition body

Game.ofBits

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
AttainCircuit	`lean/phase3/AttainCircuit.lean`	935	NimCorrBridge, NimAttain
LocalRestore	`lean/phase4/LocalRestore.lean`	587	SelectCircuit
NimCore	`lean/NimCore.lean`	139	`Std`
NimGame	`lean/phase2/NimGame.lean`	634	NimRollout

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

Section 5.3.1, paragraph 2Testing whether a candidate move realises δ is a local check on the heap being changed

1 Paper text

2 Explain this

Two-frame restoration, step by step

Compare the frames bit by bit

Extract the difference δ

Propose replacements and test them in parallel

Choose between cancelling and the fallback

Encode the first flagged heap as a binary index

Output the move

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem AttainCircuit.cancel_iff_bit

theorem LocalRestore.localDelta_eq

Definitions these statements use

def Game.Width

def LocalRestore.OneChange

def LocalRestore.localDelta

def nimSum

Full modules

theorem `AttainCircuit.cancel_iff_bit`

theorem `LocalRestore.localDelta_eq`

def `Game.Width`

def `LocalRestore.OneChange`

def `LocalRestore.localDelta`

def `nimSum`