Appendix C, “Local differences and candidate moves”Delta bits by OR under the single-change promise; the shallow test y_i < x_i; the subtract-one fallback

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

1 Paper text

Local differences and candidate moves. On a legal transition only one heap changes. Consequently, bit $k$ of the delta is $\delta_k=\bigvee_{i=0}^{N-1}(x_{i,k}\oplus x'_{i,k}).$ The single-change promise makes OR equal to the required XOR across changed rows. For a target $\delta$ supplied as input bits, form $y_i=x_i\oplus\delta$ in parallel. The test $y_i<x_i$ is shallow: OR over the possible highest differing bit, requiring equality at every higher bit and $y_{i,k}=0,x_{i,k}=1$ at that bit. Each test has size polynomial in $B$ . When no cancelling candidate exists, use the first nonzero heap and subtract one. Bit $k$ of that decrement is $x_{i,k}$ XOR the conjunction saying that all lower bits are zero. The validity bit is false exactly when the board is terminal. In restoration, the target comes from the two-frame delta; in the multi-head readout it comes from reconstruction of the rollout outcomes.

Generated from paper_jmlr.tex, lines 1494–1499.

2 Explain this

Delta bits. On a legal transition only one heap changes, so bit $k$ of the delta is the OR over heaps of $x_{i,k}\oplus x'_{i,k}$ : with at most one changed row, OR equals XOR.

Candidate test. For a target $\delta$ , compute $y_i=x_i\oplus\delta$ for all heaps in parallel and test $y_i<x_i$ with a shallow comparator: OR over the highest differing bit, with equality above it and $y_{i,k}=0$ , $x_{i,k}=1$ there.

Fallback. If no heap cancels, subtract one from the first nonzero heap: bit $k$ of $x-1$ is bit $k$ of $x$ XOR "all lower bits are zero". The move is invalid exactly on the terminal board.

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

LocalRestore.dC_eval and LocalRestore.localDelta_eq: the OR-of-XORs delta, and its equality with $\operatorname{nim}(Q)\oplus\operatorname{nim}(Q')$ when at most one heap differs.
AttainCircuit.cancel_iff_bit: for $t\ne0$ , $x\oplus t<x$ iff $x$ has $t$ 's top bit.
SelectCircuit.genSel_correct: the generic first-index selector (primary test with its new value, fallback "subtract one from the first nonzero heap") is exact.
SelectCircuit.varSel_correct: with the target on input wires, the selector computes the specified move for every target value.

Coverage record
Paper anchor	`par-local-differences-and-candidate-moves-p1` (website anchor; the manuscript has no label here)
Displayed as	Appendix C, “Local differences and candidate moves”
Claim	Delta bits by OR under the single-change promise; the shallow test y_i < x_i; the subtract-one fallback
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 1494–1499; SHA-256 of the normalised block source `35e6316fb7699da7…`
Lean declarations	`NimAudit.LocalRestore.dC_eval` (LocalRestore, lines 136–151, file `fc4c7f908b0c…`) `NimAudit.LocalRestore.localDelta_eq` (LocalRestore, lines 153–174, file `fc4c7f908b0c…`) `NimAudit.AttainCircuit.cancel_iff_bit` (AttainCircuit, lines 29–62, file `13b98daabaa9…`) `NimAudit.SelectCircuit.genSel_correct` (SelectCircuit, lines 155–246, file `922ee44ce0ab…`) `NimAudit.SelectCircuit.varSel_correct` (SelectCircuit, lines 385–397, file `922ee44ce0ab…`)
Depends on	Lemma 5.4
Explanations	`explain/c-candidate-moves`, `formal/c-candidate-moves`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `LocalRestore.dC_eval`

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

Statement as elaborated and printed by Lean 4.26.0

∀ {B N : ℕ} {Q Q' : List ℕ},
  Q.length = N →
    Q'.length = N →
      ∀ (q : ℕ),
        NimAudit.AC0.Circ.eval (NimAudit.LocalRestore.tf B N Q Q')
            (NimAudit.LocalRestore.dC B N q) =
          (NimAudit.LocalRestore.localDelta B N Q Q').testBit q

Exact source text, lines 136–151

136theorem dC_eval {B N : Nat} {Q Q' : List Nat} (hQ : Q.length = N) (hQ' : Q'.length = N) (q : Nat) :137    eval (tf B N Q Q') (dC B N q) = (localDelta B N Q Q').testBit q := by138  unfold dC localDelta139  rw [testBit_ofBits]140  by_cases hq : q < B141  · simp only [hq, if_true, decide_true, Bool.true_and, eval_or, List.any_map]142    apply Bool.eq_iff_iff.mpr143    simp only [List.any_eq_true, List.mem_range, Function.comp_apply]144    constructor145    · rintro ⟨i, hi, h⟩146      refine ⟨i, hi, ?_⟩147      rwa [yC_eval hQ hQ' hi (by omega), show B - 1 - (B - 1 - q) = q by omega] at h148    · rintro ⟨i, hi, h⟩149      refine ⟨i, hi, ?_⟩150      rwa [yC_eval hQ hQ' hi (by omega), show B - 1 - (B - 1 - q) = q by omega]151  · simp [hq]

Project declarations in the statement: AC0.Circ.eval, LocalRestore.dC, LocalRestore.localDelta, LocalRestore.tf

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.const, AC0.Circ.eval, AC0.Circ.eval_const, AC0.Circ.eval_or, AC0.Circ.or, Game.ofBits, Game.testBit_ofBits, LocalRestore.dC, LocalRestore.localDelta, LocalRestore.tf, LocalRestore.yC, LocalRestore.yC_eval

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

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 `SelectCircuit.genSel_correct`

Module SelectCircuit (lean/phase4/SelectCircuit.lean, lines 155–246) · file SHA-256 922ee44ce0ababa9… Axioms reported by the fresh build: propext, Quot.sound

GENERIC SELECTOR EXACTNESS.

Statement as elaborated and printed by Lean 4.26.0

∀ {B N : ℕ} {P : List ℕ},
  P.length = N →
    NimAudit.Game.Width B P →
      ∀ (z : ℕ → Bool),
        (∀ j < B * N, z j = NimAudit.CorrBridge.boardBits B P j) →
          ∀ (prim : ℕ → NimAudit.AC0.Circ) (pv : ℕ → ℕ → NimAudit.AC0.Circ) (pr : ℕ → Bool)
            (f : ℕ → ℕ),
            (∀ i < N, NimAudit.AC0.Circ.eval z (prim i) = pr (P.getD i 0)) →
              (∀ (x : ℕ), pr x = true → 0 < x) →
                (∀ (x : ℕ), pr x = true → x < 2 ^ B → f x < 2 ^ B) →
                  (∀ i < N,
                      ∀ p < B,
                        pr (P.getD i 0) = true →
                          NimAudit.AC0.Circ.eval z (pv i p) =
                            (f (P.getD i 0)).testBit (B - 1 - p)) →
                    NimAudit.SelectCircuit.selReadout (NimAudit.SelectCircuit.genSel B N prim pv)
                        z =
                      NimAudit.SelectCircuit.primOr pr f P

Exact source text, lines 155–246

155/-- GENERIC SELECTOR EXACTNESS. -/156theorem genSel_correct (hP : P.length = N) (hw : Width B P) (z : Nat → Bool)157    (hz : ∀ j < B * N, z j = boardBits B P j) (prim : Nat → Circ) (pv : Nat → Nat → Circ)158    (pr : Nat → Bool) (f : Nat → Nat)159    (hpr : ∀ i < N, eval z (prim i) = pr (P.getD i 0))160    (hpos : ∀ x, pr x = true → 0 < x)161    (hf : ∀ x, pr x = true → x < 2 ^ B → f x < 2 ^ B)162    (hpv : ∀ i < N, ∀ p < B, pr (P.getD i 0) = true →163      eval z (pv i p) = (f (P.getD i 0)).testBit (B - 1 - p)) :164    selReadout (genSel B N prim pv) z = primOr pr f P := by165  have hnzz : ∀ i < N, eval z (AttainCircuit.nzC B i) = decide (0 < P.getD i 0) := by166    intro i hi167    rw [eval_congr_below z (boardBits B P) _ (fun j hj => hz j (Nat.lt_of_lt_of_le hj (max_nzC hi))),168      nz_eval hP hw hi]169  have hdbz : ∀ i < N, ∀ p < B, 0 < P.getD i 0 →170      eval z (decbitC B i p) = (P.getD i 0 - 1).testBit (B - 1 - p) := by171    intro i hi p hp hpos'172    rw [eval_congr_below z (boardBits B P) _173      (fun j hj => hz j (Nat.lt_of_lt_of_le hj (max_decbitC hi hp))), decbit_eval hP hi hp hpos']174  have hcan : (List.range N).map (fun i => eval z (prim i)) = P.map pr := map_getD_eq hP hpr175  have hnz : (List.range N).map (fun i => eval z (AttainCircuit.nzC B i)) = P.map (fun x => decide (0 < x)) :=176    map_getD_eq hP hnzz177  have hany : eval z (anyC' N prim) = (P.map pr).any id := by178    unfold anyC'; rw [eval_or, ← hcan, List.any_map, List.any_map]; rfl179  have hsel : (genSel B N prim pv).sel.map (eval z) =180      (List.range N).map (fun i => eval z (prim i) ||181        (!((List.range N).any (fun i => eval z (prim i))) && eval z (AttainCircuit.nzC B i))) := by182    unfold genSel183    rw [List.map_map]184    apply List.map_congr_left; intro i _185    simp only [Function.comp_apply, eval_or, eval_and, eval_not, List.any_cons, List.any_nil,186      List.all_cons, List.all_nil, Bool.or_false, Bool.and_true, anyC', List.any_map]187    rfl188  have hvalid : eval z (genSel B N prim pv).valid = (P.map (fun x => decide (0 < x))).any id := by189    unfold genSel validA; rw [eval_or, ← hnz, List.any_map, List.any_map]; rfl190  have hanyR : (List.range N).any (fun i => eval z (prim i)) = (P.map pr).any id := by191    rw [← hcan, List.any_map]; rfl192  unfold selReadout primOr firstIdx193  rw [hsel, firstTrue_or, hvalid, hanyR, hcan, hnz, decIdx_firstTrue]194  by_cases hA : (P.map pr).any id = true195  · rw [← firstTrue_isSome] at hA196    obtain ⟨i, hi⟩ := Option.isSome_iff_exists.mp hA197    obtain ⟨hiN, hpri⟩ := firstTrue_map_getD pr rfl hi198    rw [hP] at hiN199    have hvalidT : (P.map (fun x => decide (0 < x))).any id = true := by200      rw [List.any_map]; apply List.any_eq_true.mpr201      exact ⟨P.getD i 0, by202        simp only [List.getD_eq_getElem?_getD]; rw [List.getElem?_eq_getElem (by omega)]; simp,203        by simpa using hpos _ hpri⟩204    rw [firstTrue_isSome] at hA205    simp only [hvalidT, if_true, hA, hi, Option.map_some]206    congr 2207    have hxlt := getD_lt_of_width hP hw hiN208    simp only [genSel, List.map_map]209    apply toNatBE_of_bits (hf _ hpri hxlt)210    intro p hp211    simp only [Function.comp_apply, eval_or, eval_and, eval_not, List.any_cons, List.any_nil, List.all_cons,212      List.all_nil, Bool.and_true, Bool.or_false, hany, hA, Bool.not_true, Bool.false_and,213      Bool.true_and]214    rw [orFirst_eval, hcan, hi]215    exact hpv i hiN p hp hpri216  · have hnone : firstTrue (P.map pr) = none := by217      cases h : firstTrue (P.map pr) with218      | none => rfl219      | some i =>220        exfalso; apply hA; rw [← firstTrue_isSome, h]; rfl221    have hA' : (P.map pr).any id = false := by simpa using hA222    simp only [hA', Bool.false_eq_true, if_false, hnone, Option.map_none]223    by_cases hV : (P.map (fun x => decide (0 < x))).any id = true224    · simp only [hV, if_true]225      rw [← firstTrue_isSome] at hV226      obtain ⟨i, hi⟩ := Option.isSome_iff_exists.mp hV227      obtain ⟨hiN, hposi⟩ := firstTrue_map_getD (fun x => decide (0 < x)) rfl hi228      rw [hP] at hiN229      simp only [hi, Option.map_some]230      congr 2231      have hxlt := getD_lt_of_width hP hw hiN232      have hpos' : 0 < P.getD i 0 := by simpa using hposi233      simp only [genSel, List.map_map]234      apply toNatBE_of_bits (Nat.lt_of_le_of_lt (Nat.sub_le _ _) hxlt)235      intro p hp236      simp only [Function.comp_apply, eval_or, eval_and, eval_not, List.any_cons, List.any_nil, List.all_cons,237        List.all_nil, Bool.and_true, Bool.or_false, hany, hA', Bool.not_false, Bool.false_and,238        Bool.true_and, Bool.false_or]239      rw [orFirst_eval, hnz, hi]240      exact hdbz i hiN p hp hpos'241    · have hV' : (P.map (fun x => decide (0 < x))).any id = false := by simpa using hV242      have hnone' : firstTrue (P.map (fun x => decide (0 < x))) = none := by243        cases h : firstTrue (P.map (fun x => decide (0 < x))) with244        | none => rfl245        | some i => exfalso; apply hV; rw [← firstTrue_isSome, h]; rfl246      simp [hV', hnone']

Project declarations in the statement: AC0.Circ, AC0.Circ.eval, CorrBridge.boardBits, Game.Width, SelectCircuit.genSel, SelectCircuit.primOr, SelectCircuit.selReadout

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.and, AC0.Circ.eval, AC0.Circ.eval_and, AC0.Circ.eval_congr_below, AC0.Circ.eval_not, AC0.Circ.eval_or, AC0.Circ.maxInput, AC0.Circ.not, AC0.Circ.or, Attain.decIdx, AttainCircuit.decIdx_firstTrue, AttainCircuit.decbitC, AttainCircuit.firstTrue_or, AttainCircuit.nzC, AttainCircuit.nz_eval, AttainCircuit.toNatBE_of_bits, AttainCircuit.validA, Bridge.toNatBE, CorrBridge.RCirc.mk, CorrBridge.RCirc.sel, CorrBridge.RCirc.val, CorrBridge.RCirc.valid, CorrBridge.boardBits, CorrBridge.firstTrue, Game.Width, SelectCircuit.anyC', SelectCircuit.decbit_eval, SelectCircuit.firstIdx, SelectCircuit.firstTrue_isSome, SelectCircuit.firstTrue_map_getD, SelectCircuit.genSel, SelectCircuit.getD_lt_of_width, SelectCircuit.map_getD_eq, SelectCircuit.max_decbitC, SelectCircuit.max_nzC, SelectCircuit.orFirst, SelectCircuit.orFirst_eval, SelectCircuit.primOr, SelectCircuit.selReadout

theorem `SelectCircuit.varSel_correct`

Module SelectCircuit (lean/phase4/SelectCircuit.lean, lines 385–397) · file SHA-256 922ee44ce0ababa9… Axioms reported by the fresh build: propext, Quot.sound

VARIABLE-TARGET SELECTOR EXACTNESS: for every σ < 2^B supplied on the σ wires, the circuit outputs `attainT σ P` (= `replayMove σ P`).

Statement as elaborated and printed by Lean 4.26.0

∀ {B N : ℕ} {P : List ℕ},
  P.length = N →
    NimAudit.Game.Width B P →
      ∀ {σ : ℕ},
        σ < 2 ^ B →
          NimAudit.SelectCircuit.selReadout (NimAudit.SelectCircuit.varSel B N)
              (NimAudit.SelectCircuit.selIn B N P σ) =
            NimAudit.AttainCircuit.attainT σ P

Exact source text, lines 385–397

385/-- VARIABLE-TARGET SELECTOR EXACTNESS: for every σ < 2^B supplied on the σ wires, the386    circuit outputs `attainT σ P` (= `replayMove σ P`). -/387theorem varSel_correct (hP : P.length = N) (hw : Width B P) {σ : Nat} (hσ : σ < 2 ^ B) :388    selReadout (varSel B N) (selIn B N P σ) = attainT σ P := by389  rw [attainT_eq_primOr]390  apply genSel_correct hP hw _ (fun j hj => selIn_board σ hj)391  · intro i hi; exact cancV_eval hP hσ hi392  · intro x hx393    rcases Nat.eq_zero_or_pos x with h | h394    · subst h; simp at hx395    · exact h396  · intro x _ hx; exact Nat.xor_lt_two_pow hx hσ397  · intro i hi p hp _; exact xbV_eval hP σ hi hp

Project declarations in the statement: AttainCircuit.attainT, Game.Width, SelectCircuit.selIn, SelectCircuit.selReadout, SelectCircuit.varSel

Project declarations used by the proof or definition body

AttainCircuit.attainT, Game.Width, SelectCircuit.attainT_eq_primOr, SelectCircuit.cancV, SelectCircuit.cancV_eval, SelectCircuit.genSel_correct, SelectCircuit.primOr, SelectCircuit.selIn, SelectCircuit.selIn_board, SelectCircuit.selReadout, SelectCircuit.varSel, SelectCircuit.xbV, SelectCircuit.xbV_eval

Definitions these statements use

def `AC0.Circ.eval`

Module Circuit (lean/phase3/Circuit.lean, lines 44–49) · file SHA-256 af97cc0eec7d8464…

Statement as elaborated and printed by Lean 4.26.0

(ℕ → Bool) → NimAudit.AC0.Circ → Bool

Exact source text, lines 44–49

44def eval (x : Nat → Bool) : Circ → Bool45  | input i => x i46  | const b => b47  | not c => !(eval x c)48  | and cs => cs.attach.all (fun ⟨c, _⟩ => eval x c)49  | or cs => cs.attach.any (fun ⟨c, _⟩ => eval x c)

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.and, AC0.Circ.casesOn, AC0.Circ.const, AC0.Circ.input, AC0.Circ.not, AC0.Circ.or, AC0.Circ.rec, AC0.Circ.rec_1

def `LocalRestore.dC`

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

Little-endian bit q of the single-change delta: OR over heaps of the bit-q XORs.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → ℕ → NimAudit.AC0.Circ

Exact source text, lines 57–58

57/-- Little-endian bit q of the single-change delta: OR over heaps of the bit-q XORs. -/58def dC (B N q : Nat) : Circ := if q < B then or ((List.range N).map (fun i => yC B N i (B - 1 - q))) else const false

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.const, AC0.Circ.or, LocalRestore.yC

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 `LocalRestore.tf`

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

Two-frame input vector.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → List ℕ → List ℕ → ℕ → Bool

Exact source text, lines 29–31

29/-- Two-frame input vector. -/30def tf (B N : Nat) (Q Q' : List Nat) : Nat → Bool := fun j =>31  if j < B * N then boardBits B Q j else boardBits B Q' (j - B * N)

Project declarations in the statement: none

Project declarations used by the proof or definition body

CorrBridge.boardBits

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 `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

inductive `AC0.Circ`

Module Circuit (lean/phase3/Circuit.lean, lines 35–40) · file SHA-256 af97cc0eec7d8464…

Statement as elaborated and printed by Lean 4.26.0

Type

Exact source text, lines 35–40

35inductive Circ where36  | input (i : Nat)37  | const (b : Bool)38  | not (c : Circ)39  | and (cs : List Circ)40  | or (cs : List Circ)

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `CorrBridge.boardBits`

Module NimCorrBridge (lean/phase3/NimCorrBridge.lean, lines 39–41) · file SHA-256 d3fb2e4a64db3e92…

Input bits of a board: heap i, big-endian position p (bit B-1-p) at index B·i + p.

Statement as elaborated and printed by Lean 4.26.0

ℕ → List ℕ → ℕ → Bool

Exact source text, lines 39–41

39/-- Input bits of a board: heap i, big-endian position p (bit B-1-p) at index B·i + p. -/40def boardBits (B : Nat) (P : List Nat) : Nat → Bool := fun j =>41  if j < B * P.length then (P.getD (j / B) 0).testBit (B - 1 - j % B) else false

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `SelectCircuit.genSel`

Module SelectCircuit (lean/phase4/SelectCircuit.lean, lines 87–91) · file SHA-256 922ee44ce0ababa9…

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → (ℕ → NimAudit.AC0.Circ) → (ℕ → ℕ → NimAudit.AC0.Circ) → NimAudit.CorrBridge.RCirc

Exact source text, lines 87–91

87def genSel (B N : Nat) (prim : Nat → Circ) (pv : Nat → Nat → Circ) : RCirc :=88  ⟨validA B N,89   (List.range N).map (fun i => or [prim i, and [not (anyC' N prim), AttainCircuit.nzC B i]]),90   (List.range B).map (fun p => or [and [anyC' N prim, orFirst N prim (fun i => pv i p)],91     and [not (anyC' N prim), orFirst N (AttainCircuit.nzC B) (fun i => decbitC B i p)]])⟩

Project declarations in the statement: AC0.Circ, CorrBridge.RCirc

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.and, AC0.Circ.not, AC0.Circ.or, AttainCircuit.decbitC, AttainCircuit.nzC, AttainCircuit.validA, CorrBridge.RCirc.mk, SelectCircuit.anyC', SelectCircuit.orFirst

def `SelectCircuit.primOr`

Module SelectCircuit (lean/phase4/SelectCircuit.lean, lines 79–83) · file SHA-256 922ee44ce0ababa9…

Primary choice, else fallback (first nonzero heap minus one), else halt.

Statement as elaborated and printed by Lean 4.26.0

(ℕ → Bool) → (ℕ → ℕ) → List ℕ → Option (ℕ × ℕ)

Exact source text, lines 79–83

79/-- Primary choice, else fallback (first nonzero heap minus one), else halt. -/80def primOr (pr : Nat → Bool) (f : Nat → Nat) (P : List Nat) : Option (Nat × Nat) :=81  match firstIdx pr f P with82  | some m => some m83  | none => decIdx P

Project declarations in the statement: none

Project declarations used by the proof or definition body

Attain.decIdx, SelectCircuit.firstIdx

def `SelectCircuit.selReadout`

Module SelectCircuit (lean/phase4/SelectCircuit.lean, lines 26–32) · file SHA-256 922ee44ce0ababa9…

Evaluation of a move readout on an arbitrary input vector.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.CorrBridge.RCirc → (ℕ → Bool) → Option (ℕ × ℕ)

Exact source text, lines 26–32

26/-- Evaluation of a move readout on an arbitrary input vector. -/27def selReadout (R : RCirc) (z : Nat → Bool) : Option (Nat × Nat) :=28  if eval z R.valid then29    match firstTrue (R.sel.map (eval z)) with30    | some i => some (i, toNatBE (R.val.map (eval z)))31    | none => none32  else none

Project declarations in the statement: CorrBridge.RCirc

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.eval, Bridge.toNatBE, CorrBridge.RCirc, CorrBridge.RCirc.sel, CorrBridge.RCirc.val, CorrBridge.RCirc.valid, CorrBridge.firstTrue

def `AttainCircuit.attainT`

Module AttainCircuit (lean/phase3/AttainCircuit.lean, lines 199–203) · file SHA-256 13b98daabaa917e5…

The attainability readout for a single guess t (as in `attainF`).

Statement as elaborated and printed by Lean 4.26.0

ℕ → List ℕ → Option (ℕ × ℕ)

Exact source text, lines 199–203

199/-- The attainability readout for a single guess t (as in `attainF`). -/200def attainT (t : Nat) (P : List Nat) : Option (Nat × Nat) :=201  match cancelIdx t P with202  | some m => some m203  | none => decIdx P

Project declarations in the statement: none

Project declarations used by the proof or definition body

Attain.cancelIdx, Attain.decIdx

def `SelectCircuit.selIn`

Module SelectCircuit (lean/phase4/SelectCircuit.lean, lines 324–326) · file SHA-256 922ee44ce0ababa9…

Input vector: board on wires below B·N, then the bits of σ (little-endian).

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → List ℕ → ℕ → ℕ → Bool

Exact source text, lines 324–326

324/-- Input vector: board on wires below B·N, then the bits of σ (little-endian). -/325def selIn (B N : Nat) (P : List Nat) (σ : Nat) : Nat → Bool := fun j =>326  if j < B * N then boardBits B P j else σ.testBit (j - B * N)

Project declarations in the statement: none

Project declarations used by the proof or definition body

CorrBridge.boardBits

def `SelectCircuit.varSel`

Module SelectCircuit (lean/phase4/SelectCircuit.lean, lines 341–341) · file SHA-256 922ee44ce0ababa9…

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → NimAudit.CorrBridge.RCirc

Exact source text, lines 341–341

341def varSel (B N : Nat) : RCirc := genSel B N (cancV B N) (xbV B N)

Project declarations in the statement: CorrBridge.RCirc

Project declarations used by the proof or definition body

SelectCircuit.cancV, SelectCircuit.genSel, SelectCircuit.xbV

Full modules

Module	File	Lines	Imports
AttainCircuit	`lean/phase3/AttainCircuit.lean`	935	NimCorrBridge, NimAttain
Circuit	`lean/phase3/Circuit.lean`	1151	NimProbability
LocalRestore	`lean/phase4/LocalRestore.lean`	587	SelectCircuit
NimCore	`lean/NimCore.lean`	139	`Std`
NimCorrBridge	`lean/phase3/NimCorrBridge.lean`	922	BitBridge
NimGame	`lean/phase2/NimGame.lean`	634	NimRollout
SelectCircuit	`lean/phase4/SelectCircuit.lean`	1064	ControllerBits

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

Appendix C, “Local differences and candidate moves”Delta bits by OR under the single-change promise; the shallow test y_i < x_i; the subtract-one fallback

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 LocalRestore.dC_eval

theorem LocalRestore.localDelta_eq

theorem AttainCircuit.cancel_iff_bit

theorem SelectCircuit.genSel_correct

theorem SelectCircuit.varSel_correct

Definitions these statements use

def AC0.Circ.eval

def LocalRestore.dC

def LocalRestore.localDelta

def LocalRestore.tf

def Game.Width

def LocalRestore.OneChange

def nimSum

inductive AC0.Circ

def CorrBridge.boardBits

def SelectCircuit.genSel

def SelectCircuit.primOr

def SelectCircuit.selReadout

def AttainCircuit.attainT

def SelectCircuit.selIn

def SelectCircuit.varSel

Full modules

theorem `LocalRestore.dC_eval`

theorem `LocalRestore.localDelta_eq`

theorem `AttainCircuit.cancel_iff_bit`

theorem `SelectCircuit.genSel_correct`

theorem `SelectCircuit.varSel_correct`

def `AC0.Circ.eval`

def `LocalRestore.dC`

def `LocalRestore.localDelta`

def `LocalRestore.tf`

def `Game.Width`

def `LocalRestore.OneChange`

def `nimSum`

inductive `AC0.Circ`

def `CorrBridge.boardBits`

def `SelectCircuit.genSel`

def `SelectCircuit.primOr`

def `SelectCircuit.selReadout`

def `AttainCircuit.attainT`

def `SelectCircuit.selIn`

def `SelectCircuit.varSel`