Section 5.3.2, listThe two-frame components: encoding, changed-heap detection, Δ, and a move selector for a target δ

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

1 Paper text

a binary encoding scheme for heap vectors (Appendix C),
a constant-depth detection of which heaps changed between frames,
an $\AC^0$ circuit computing $\Delta$ on those changed heaps (Lemma 5.4),
an $\AC^0$ selection mechanism for a response move realising a target $\delta$ .

Generated from paper_jmlr.tex, lines 616–621.

2 Explain this

The two-frame player decomposes into four shallow parts: encode heap sizes in binary; detect which heaps changed; compute $\Delta$ on the changed heaps; select a response that realises a target $\delta$ . Each part is a constant-depth circuit; composing a fixed number of them keeps constant depth.

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

Each item has a checked counterpart: changed-heap detection LocalRestore.chgC_eval; the delta LocalRestore.localDelta_eq (one change) and Lemma 5.4 (at most $t$ changes); the variable-target selector SelectCircuit.varSel_correct (the target arrives on input wires); binary output via the priority encoder PriorityEncoder.encode_correct.

Coverage record
Paper anchor	`sec-implementation-overview-list1` (website anchor; the manuscript has no label here)
Displayed as	Section 5.3.2, list
Claim	The two-frame components: encoding, changed-heap detection, Δ, and a move selector for a target δ
Coverage category	Checked definition or construction
Statement source	paper_jmlr.tex lines 616–621; SHA-256 of the normalised block source `a80358fba4a0a3f9…`
Lean declarations	`NimAudit.LocalRestore.chgC_eval` (LocalRestore, lines 80–95, file `fc4c7f908b0c…`) `NimAudit.LocalRestore.localDelta_eq` (LocalRestore, lines 153–174, file `fc4c7f908b0c…`) `NimAudit.SelectCircuit.varSel_correct` (SelectCircuit, lines 385–397, file `922ee44ce0ab…`) `NimAudit.PriorityEncoder.encode_correct` (PriorityEncoder, lines 67–107, file `1be04943f545…`)
Depends on	Lemma 5.4, Appendix C, “A binary index is part of the circuit”
Explanations	`explain/c-impl-overview`, `formal/c-impl-overview`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `LocalRestore.chgC_eval`

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

CHANGED-ROW DETECTION.

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' →
          ∀ {i : ℕ},
            i < N →
              NimAudit.AC0.Circ.eval (NimAudit.LocalRestore.tf B N Q Q')
                  (NimAudit.LocalRestore.chgC B N i) =
                decide (Q.getD i 0 ≠ Q'.getD i 0)

Exact source text, lines 80–95

80/-- CHANGED-ROW DETECTION. -/81theorem chgC_eval {B N : Nat} {Q Q' : List Nat} (hQ : Q.length = N) (hQ' : Q'.length = N)82    (hw : Width B Q) (hw' : Width B Q') {i : Nat} (hi : i < N) :83    eval (tf B N Q Q') (chgC B N i) = decide (Q.getD i 0 ≠ Q'.getD i 0) := by84  apply Bool.eq_iff_iff.mpr85  rw [decide_eq_true_iff, testBit_ne_iff (getD_lt_of_width hQ hw hi) (getD_lt_of_width hQ' hw' hi)]86  simp only [chgC, eval_or, List.any_map, List.any_eq_true, List.mem_range, Function.comp_apply]87  constructor88  · rintro ⟨p, hp, h⟩89    rw [yC_eval hQ hQ' hi hp] at h90    refine ⟨B - 1 - p, by omega, ?_⟩91    simpa using h92  · rintro ⟨k, hk, h⟩93    refine ⟨B - 1 - k, by omega, ?_⟩94    rw [yC_eval hQ hQ' hi (by omega), show B - 1 - (B - 1 - k) = k by omega]95    simpa using h

Project declarations in the statement: AC0.Circ.eval, Game.Width, LocalRestore.chgC, LocalRestore.tf

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.eval, AC0.Circ.eval_or, AC0.Circ.or, Game.Width, LocalRestore.chgC, LocalRestore.testBit_ne_iff, LocalRestore.tf, LocalRestore.yC, LocalRestore.yC_eval, SelectCircuit.getD_lt_of_width

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

theorem `PriorityEncoder.encode_correct`

Module PriorityEncoder (lean/phase5/PriorityEncoder.lean, lines 67–107) · file SHA-256 1be04943f5455fc1… Axioms reported by the fresh build: propext, Quot.sound

PRIORITY-ENCODER CORRECTNESS, for every input assignment: the binary output decodes to exactly the selection readout (first true flag, value bits), and to `none` when the readout is invalid or no flag is true.

Statement as elaborated and printed by Lean 4.26.0

∀ (R : NimAudit.CorrBridge.RCirc) (N r : ℕ),
  R.sel.length = N →
    N ≤ 2 ^ r →
      ∀ (z : ℕ → Bool),
        NimAudit.PriorityEncoder.binSem (NimAudit.PriorityEncoder.encode R N r) N z =
          NimAudit.SelectCircuit.selReadout R z

Exact source text, lines 67–107

67/-- PRIORITY-ENCODER CORRECTNESS, for every input assignment: the binary output decodes68    to exactly the selection readout (first true flag, value bits), and to `none` when69    the readout is invalid or no flag is true. -/70theorem encode_correct (R : RCirc) (N r : Nat) (hlen : R.sel.length = N) (hr : N ≤ 2 ^ r)71    (z : Nat → Bool) : binSem (encode R N r) N z = selReadout R z := by72  unfold binSem selReadout encode73  simp only74  by_cases hv : eval z R.valid = true75  · cases hft : firstTrue (R.sel.map (eval z)) with76    | none =>77      have hany : (R.sel.map (eval z)).any id = false := by78        have := firstTrue_isSome (R.sel.map (eval z)); rw [hft] at this; simpa using this.symm79      have hor : eval z (or ((List.range N).map (getC R.sel))) = false := by80        rw [eval_or, List.any_map]81        have e : ((List.range N).any (eval z ∘ getC R.sel)) = (R.sel.map (eval z)).any id := by82          rw [← flags_eq R.sel N hlen z, List.any_map]; rfl83        rw [e, hany]84      simp [hv, hor]85    | some i =>86      have hiN : i < N := by have := firstTrue_lt hft; simpa [hlen] using this87      have hflag : (R.sel.map (eval z)).getD i false = true := ((firstTrue_some_iff _ i).1 hft).2.188      have hor : eval z (or ((List.range N).map (getC R.sel))) = true := by89        rw [eval_or, List.any_map]90        apply List.any_eq_true.mpr91        exact ⟨i, List.mem_range.mpr hiN, by simp only [Function.comp_apply, eval_getC]; exact hflag⟩92      have hidx : toNatBE (((List.range r).map (idxBit R.sel N r)).map (eval z)) = i := by93        rw [List.map_map]94        apply toNatBE_of_bits (Nat.lt_of_lt_of_le hiN hr)95        intro q _96        simp only [Function.comp_apply]97        apply Bool.eq_iff_iff.mpr98        simp only [idxBit, eval_or, List.any_map, List.any_eq_true, List.mem_filter, List.mem_range,99          Function.comp_apply]100        constructor101        · rintro ⟨i', ⟨hi', hb⟩, he⟩102          rw [firstF_eval R.sel hlen z hi', hft, decide_eq_true_iff] at he103          cases he; exact hb104        · intro hb105          exact ⟨i, ⟨hiN, hb⟩, by rw [firstF_eval R.sel hlen z hiN, hft]; simp⟩106      simp only [eval_and, List.all_cons, List.all_nil, hv, hor, Bool.and_true, if_true, hidx, hiN]107  · simp [hv]

Project declarations in the statement: AC0.Circ, CorrBridge.RCirc, CorrBridge.RCirc.sel, PriorityEncoder.binSem, PriorityEncoder.encode, 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_or, AC0.Circ.or, AttainCircuit.firstTrue_lt, AttainCircuit.toNatBE_of_bits, BinReadout.BCirc.idx, BinReadout.BCirc.mk, BinReadout.BCirc.val, BinReadout.BCirc.valid, Bridge.toNatBE, CorrBridge.RCirc, CorrBridge.RCirc.sel, CorrBridge.RCirc.val, CorrBridge.RCirc.valid, CorrBridge.eval_getC, CorrBridge.firstTrue, CorrBridge.firstTrue_some_iff, CorrBridge.getC, PriorityEncoder.binSem, PriorityEncoder.encode, PriorityEncoder.firstF, PriorityEncoder.firstF_eval, PriorityEncoder.flags_eq, PriorityEncoder.idxBit, SelectCircuit.firstTrue_isSome, SelectCircuit.selReadout

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

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

Heap i changed between the frames.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → ℕ → NimAudit.AC0.Circ

Exact source text, lines 54–55

54/-- Heap i changed between the frames. -/55def chgC (B N i : Nat) : Circ := or ((List.range B).map (yC B N i))

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

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

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

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

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

inductive `CorrBridge.RCirc`

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

Statement as elaborated and printed by Lean 4.26.0

Type

Exact source text, lines 34–37

34structure RCirc where35  valid : Circ36  sel : List Circ37  val : List Circ

Project declarations in the statement: none

Project declarations used by the proof or definition body

AC0.Circ

def `CorrBridge.RCirc.sel`

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

Statement as elaborated and printed by Lean 4.26.0

NimAudit.CorrBridge.RCirc → List NimAudit.AC0.Circ

Exact source text, lines 36–36

36  sel : List Circ

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

Project declarations used by the proof or definition body

CorrBridge.RCirc

def `PriorityEncoder.binSem`

Module PriorityEncoder (lean/phase5/PriorityEncoder.lean, lines 40–47) · file SHA-256 1be04943f5455fc1…

Binary-format semantics on an arbitrary input vector (an index ≥ N is invalid); on boards this is exactly `BinReadout.binReadoutOf`.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.BinReadout.BCirc → ℕ → (ℕ → Bool) → Option (ℕ × ℕ)

Exact source text, lines 40–47

40/-- Binary-format semantics on an arbitrary input vector (an index ≥ N is invalid);41    on boards this is exactly `BinReadout.binReadoutOf`. -/42def binSem (S : BCirc) (N : Nat) (z : Nat → Bool) : Option (Nat × Nat) :=43  if eval z S.valid then44    if toNatBE (S.idx.map (eval z)) < N then45      some (toNatBE (S.idx.map (eval z)), toNatBE (S.val.map (eval z)))46    else none47  else none

Project declarations in the statement: BinReadout.BCirc

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.eval, BinReadout.BCirc, BinReadout.BCirc.idx, BinReadout.BCirc.val, BinReadout.BCirc.valid, Bridge.toNatBE

def `PriorityEncoder.encode`

Module PriorityEncoder (lean/phase5/PriorityEncoder.lean, lines 34–38) · file SHA-256 1be04943f5455fc1…

THE PRIORITY ENCODER.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.CorrBridge.RCirc → ℕ → ℕ → NimAudit.BinReadout.BCirc

Exact source text, lines 34–38

34/-- THE PRIORITY ENCODER. -/35def encode (R : RCirc) (N r : Nat) : BCirc :=36  ⟨and [R.valid, or ((List.range N).map (getC R.sel))],37   (List.range r).map (idxBit R.sel N r),38   R.val⟩

Project declarations in the statement: BinReadout.BCirc, CorrBridge.RCirc

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.and, AC0.Circ.or, BinReadout.BCirc.mk, CorrBridge.RCirc, CorrBridge.RCirc.sel, CorrBridge.RCirc.val, CorrBridge.RCirc.valid, CorrBridge.getC, PriorityEncoder.idxBit

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
PriorityEncoder	`lean/phase5/PriorityEncoder.lean`	430	LocalRestore, BinaryReadout
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).

Section 5.3.2, listThe two-frame components: encoding, changed-heap detection, Δ, and a move selector for a target δ

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

theorem LocalRestore.localDelta_eq

theorem SelectCircuit.varSel_correct

theorem PriorityEncoder.encode_correct

Definitions these statements use

def AC0.Circ.eval

def Game.Width

def LocalRestore.chgC

def LocalRestore.tf

def LocalRestore.OneChange

def LocalRestore.localDelta

def nimSum

def AttainCircuit.attainT

def SelectCircuit.selIn

def SelectCircuit.selReadout

def SelectCircuit.varSel

inductive AC0.Circ

inductive CorrBridge.RCirc

def CorrBridge.RCirc.sel

def PriorityEncoder.binSem

def PriorityEncoder.encode

Full modules

theorem `LocalRestore.chgC_eval`

theorem `LocalRestore.localDelta_eq`

theorem `SelectCircuit.varSel_correct`

theorem `PriorityEncoder.encode_correct`

def `AC0.Circ.eval`

def `Game.Width`

def `LocalRestore.chgC`

def `LocalRestore.tf`

def `LocalRestore.OneChange`

def `LocalRestore.localDelta`

def `nimSum`

def `AttainCircuit.attainT`

def `SelectCircuit.selIn`

def `SelectCircuit.selReadout`

def `SelectCircuit.varSel`

inductive `AC0.Circ`

inductive `CorrBridge.RCirc`

def `CorrBridge.RCirc.sel`

def `PriorityEncoder.binSem`

def `PriorityEncoder.encode`