Section 5.3.1, paragraph 2A restoration move can be selected from (Q,Q') by a constant-depth circuit

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

1 Paper text

Moreover, a concrete restoration move can be selected in $\AC^0$ from $(Q,Q')$ by computing $\delta=\Delta(Q,Q')$ and then choosing (with a fixed tie-break rule) a heap $i$ such that $x_i' = x_i \oplus \delta < x_i$ (Appendix C).

Generated from paper_jmlr.tex, lines 542–542.

2 Explain this

The proposition says which differences to match; this sentence says the matching move can be found by a shallow circuit. Compute $\delta$ from the two frames, then pick (by a fixed tie-break) a heap $i$ with $x_i'\oplus\delta < x_i'$ and set it to $x_i'\oplus\delta$ . Under the promise, $\delta$ equals the current nim-sum, so such a heap exists: any heap with the top bit of $\delta$ set works.

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.restore_equiv: for $B$ -bit boards of equal length $N$ , if $\operatorname{nim}(Q)=0$ and $Q\to Q'$ is legal, the explicit circuit LocalRestore.restC (which reads only per-heap bit differences of the two frames) outputs a move $(i,v)$ ; applying it gives exactly the board specified by the global definition Game.restore; the move is legal; the result has nim-sum zero.
LocalRestore.restC_bound: depth at most 17 and polynomial size, reading only the two frames.
Family.rest_semantics: the same objects in the paper's binary output format (valid bit, binary index, binary value), both as formulas and as the compiled threshold network with weights and thresholds in $\{0,1\}$ .
WholeGame.twoFrame_wins: a player that stores its own last board and answers every legal opponent move with the network's reply wins every play from an established zero-nim-sum board.

Coverage record
Paper anchor	`sec:restoration-p2` (website anchor; the manuscript has no label here)
Displayed as	Section 5.3.1, paragraph 2
Claim	A restoration move can be selected from (Q,Q') by a constant-depth circuit
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 542–542; SHA-256 of the normalised block source `f0cd9ede2be2bf39…`
Lean declarations	`NimAudit.LocalRestore.restore_equiv` (LocalRestore, lines 208–229, file `fc4c7f908b0c…`) `NimAudit.LocalRestore.restC_bound` (LocalRestore, lines 423–436, file `fc4c7f908b0c…`) `NimAudit.Family.rest_semantics` (Family, lines 328–340, file `7a647f0a667d…`) `NimAudit.WholeGame.twoFrame_wins` (WholeGame, lines 75–96, file `809a74ad589d…`)
Assumptions and domain	Equal lengths $N$ , heaps below $2^B$ , $\operatorname{nim}(Q)=0$ and $Q\to Q'$ legal.
Depends on	Proposition 5.5, Appendix C, “Local differences and candidate moves”
Audited correspondence rows	`prop:restore`
Explanations	`explain/c-restore-selector`, `formal/c-restore-selector`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `LocalRestore.restore_equiv`

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

LOCAL RESTORATION EQUIVALENCE: under the zero-predecessor / legal-transition promise (nim(Q) = 0 and Q → Q' a legal move), the purely local circuit outputs a move (i, v) whose application is exactly `NimGame.restore Q Q'`; the move is legal and restores nim-sum 0.

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.nimSum Q = 0 →
            NimAudit.Game.Move Q Q' →
              ∃ i v,
                NimAudit.SelectCircuit.selReadout (NimAudit.LocalRestore.restC B N)
                      (NimAudit.LocalRestore.tf B N Q Q') =
                    some (i, v) ∧
                  NimAudit.Game.restore Q Q' = some (Q'.set i v) ∧
                    NimAudit.Game.Move Q' (Q'.set i v) ∧ NimAudit.nimSum (Q'.set i v) = 0

Exact source text, lines 208–229

208/-- LOCAL RESTORATION EQUIVALENCE: under the zero-predecessor / legal-transition209    promise (nim(Q) = 0 and Q → Q' a legal move), the purely local circuit outputs a210    move (i, v) whose application is exactly `NimGame.restore Q Q'`; the move is legal211    and restores nim-sum 0. -/212theorem restore_equiv {B N : Nat} {Q Q' : List Nat} (hQ : Q.length = N) (hQ' : Q'.length = N)213    (hw : Width B Q) (hw' : Width B Q') (h0 : nimSum Q = 0) (hm : Move Q Q') :214    ∃ i v, selReadout (restC B N) (tf B N Q Q') = some (i, v) ∧215      restore Q Q' = some (Q'.set i v) ∧ Move Q' (Q'.set i v) ∧ nimSum (Q'.set i v) = 0 := by216  rw [restC_eval hQ hQ' hw', localDelta_eq hQ hQ' hw hw' (oneChange_of_move hm)]217  obtain ⟨R, hR, hmR, hzR⟩ := restore_correct h0 hm218  have hR' := hR219  unfold restore at hR'220  rw [cancelFirst_eq] at hR'221  cases hc : cancelIdx (nimSum Q ^^^ nimSum Q') Q' with222  | none => rw [hc] at hR'; cases hR'223  | some m =>224    obtain ⟨i, v⟩ := m225    rw [hc] at hR'226    simp only [applyM, Option.some.injEq] at hR'227    subst hR'228    refine ⟨i, v, ?_, hR, hmR, hzR⟩229    unfold attainT; rw [hc]

Project declarations in the statement: Game.Move, Game.Width, Game.restore, LocalRestore.restC, LocalRestore.tf, SelectCircuit.selReadout, nimSum

Project declarations used by the proof or definition body

Attain.cancelIdx, Attain.decIdx, AttainCircuit.attainT, Game.Move, Game.Width, Game.cancelFirst, Game.restore, Game.restore_correct, LocalRestore.cancelFirst_eq, LocalRestore.localDelta, LocalRestore.localDelta_eq, LocalRestore.oneChange_of_move, LocalRestore.restC, LocalRestore.restC_eval, LocalRestore.tf, SelectCircuit.applyM, SelectCircuit.selReadout, nimSum

theorem `LocalRestore.restC_bound`

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

The restoration circuit: depth ≤ 17, polynomial size, reading only the two frames.

Statement as elaborated and printed by Lean 4.26.0

∀ {B N : ℕ},
  NimAudit.SelectCircuit.SelBound (NimAudit.LocalRestore.restC B N) N B (4 + 9 + 4)
    (12 * ((N + 2) * (B + 2) * (B * (2 * B + 3) + 9 + 2)) ^ 8 * (10 * N + 1 + 1)) (2 * (B * N))

Exact source text, lines 423–436

423/-- The restoration circuit: depth ≤ 17, polynomial size, reading only the two frames. -/424theorem restC_bound :425    SelBound (restC B N) N B (4 + 9 + 4)426      (12 * ((N + 2) * (B + 2) * (B * (2 * B + 3) + 9 + 2)) ^ 8 * (10 * N + 1 + 1)) (2 * (B * N)) := by427  apply substR_bound (restSubst B N) varSel_bound428  · intro w; unfold restSubst; split429    · simp430    · exact (dC_res _).1431  · intro w; unfold restSubst; split432    · simp433    · exact (dC_res _).2.1434  · intro w; unfold restSubst; split435    · simp; omega436    · exact (dC_res _).2.2

Project declarations in the statement: LocalRestore.restC, SelectCircuit.SelBound

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.depth, AC0.Circ.depth_input, AC0.Circ.input, AC0.Circ.maxInput, AC0.Circ.maxInput_input, AC0.Circ.size, AC0.Circ.size_input, LocalRestore.dC, LocalRestore.dC_res, LocalRestore.restSubst, SelectCircuit.substR_bound, SelectCircuit.varSel, SelectCircuit.varSel_bound

theorem `Family.rest_semantics`

Module Family (lean/phase6/Family.lean, lines 328–340) · file SHA-256 7a647f0a667d5ede… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

Semantics of the SAME objects on the promised domain (previous nim-sum zero, legal transition): formulas and network output the restoring binary move.

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.nimSum Q = 0 →
            NimAudit.Game.Move Q Q' →
              ∃ i v,
                NimAudit.PriorityEncoder.binSem (NimAudit.Family.restS (B, N)) N
                      (NimAudit.LocalRestore.tf B N Q Q') =
                    some (i, v) ∧
                  NimAudit.ThresholdInst.netBinSem (NimAudit.Family.restN (B, N)) N
                        (NimAudit.WholeGame.rIdx N) B (NimAudit.LocalRestore.tf B N Q Q') =
                      some (i, v) ∧
                    NimAudit.Game.restore Q Q' = some (Q'.set i v) ∧
                      NimAudit.Game.Move Q' (Q'.set i v) ∧ NimAudit.nimSum (Q'.set i v) = 0

Exact source text, lines 328–340

328/-- Semantics of the SAME objects on the promised domain (previous nim-sum zero, legal329    transition): formulas and network output the restoring binary move. -/330theorem rest_semantics {B N : Nat} {Q Q' : List Nat} (hQ : Q.length = N) (hQ' : Q'.length = N)331    (hw : Width B Q) (hw' : Width B Q') (h0 : nimSum Q = 0) (hm : Move Q Q') :332    ∃ i v, binSem (restS (B, N)) N (LocalRestore.tf B N Q Q') = some (i, v) ∧333      netBinSem (restN (B, N)) N (rIdx N) B (LocalRestore.tf B N Q Q') = some (i, v) ∧334      restore Q Q' = some (Q'.set i v) ∧ Move Q' (Q'.set i v) ∧ nimSum (Q'.set i v) = 0 := by335  obtain ⟨i, v, h1, h2, h3, h4⟩ := restBin_correct (rIdx_width N) hQ hQ' hw hw' h0 hm336  have hb := restBin_bound (B := B) (N := N) (rIdx_width N)337  refine ⟨i, v, h1, ?_, h2, h3, h4⟩338  show netBinSem (binNet (restBin B N (rIdx N))) N (rIdx N) B (LocalRestore.tf B N Q Q') = some (i, v)339  rw [binNet_correct _ hb.idx_len hb.val_len]340  exact h1

Project declarations in the statement: Family.restN, Family.restS, Game.Move, Game.Width, Game.restore, LocalRestore.tf, PriorityEncoder.binSem, ThresholdInst.netBinSem, WholeGame.rIdx, nimSum

Project declarations used by the proof or definition body

Family.rIdx_width, Family.restN, Family.restS, Game.Move, Game.Width, Game.restore, LocalRestore.tf, PriorityEncoder.BinBound, PriorityEncoder.BinBound.idx_len, PriorityEncoder.BinBound.val_len, PriorityEncoder.binSem, PriorityEncoder.restBin, PriorityEncoder.restBin_bound, PriorityEncoder.restBin_correct, ThresholdInst.binNet, ThresholdInst.binNet_correct, ThresholdInst.netBinSem, WholeGame.rIdx, nimSum

theorem `WholeGame.twoFrame_wins`

Module WholeGame (lean/phase5/WholeGame.lean, lines 75–96) · file SHA-256 809a74ad589db609… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

TWO-FRAME WHOLE-GAME THEOREM: from an established zero-nim-sum stored board (opponent to move), the network-driven two-frame player answers every legal opponent move legally, keeps the zero invariant, the board length and the bit width, and every play terminates with the player making the last move. Includes terminal and empty boards (no opponent move exists).

Statement as elaborated and printed by Lean 4.26.0

∀ {B : ℕ} (Q : List ℕ),
  NimAudit.Game.Width B Q →
    NimAudit.nimSum Q = 0 → NimAudit.WholeGame.TwoFrameWins (NimAudit.WholeGame.restReply B) Q

Exact source text, lines 75–96

75/-- TWO-FRAME WHOLE-GAME THEOREM: from an established zero-nim-sum stored board (opponent76    to move), the network-driven two-frame player answers every legal opponent move77    legally, keeps the zero invariant, the board length and the bit width, and every play78    terminates with the player making the last move.  Includes terminal and empty79    boards (no opponent move exists). -/80theorem twoFrame_wins {B : Nat} : ∀ (Q : List Nat), Width B Q → nimSum Q = 0 →81    TwoFrameWins (restReply B) Q := by82  intro Q83  induction Q using (measure List.sum).wf.induction with84  | h Q ih =>85    intro hw h086    refine TwoFrameWins.intro Q (fun Q' hm => ?_) (fun Q' R hm hR => ?_) (fun Q' R hm hR => ?_)87    · obtain ⟨R, h1, _⟩ := restReply_step hw h0 hm88      rw [h1]; rfl89    · obtain ⟨R', h1, _, h3, _⟩ := restReply_step hw h0 hm90      rw [h1] at hR; cases hR; exact h391    · obtain ⟨R', h1, _, h3, h4, _, h6⟩ := restReply_step hw h0 hm92      have hRR : R' = R := by rw [h1] at hR; exact Option.some.inj hR93      subst hRR94      refine ih R' ?_ h6 h495      have := move_sum_lt hm; have := move_sum_lt h396      show R'.sum < Q.sum; omega

Project declarations in the statement: Game.Width, WholeGame.TwoFrameWins, WholeGame.restReply, nimSum

Project declarations used by the proof or definition body

Game.Move, Game.Width, Game.move_sum_lt, Game.restore, WholeGame.TwoFrameWins, WholeGame.TwoFrameWins.intro, WholeGame.restReply, WholeGame.restReply_step, nimSum

Definitions these statements use

def `LocalRestore.restC`

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

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → NimAudit.CorrBridge.RCirc

Exact source text, lines 181–181

181def restC (B N : Nat) : RCirc := substR (restSubst B N) (varSel B N)

Project declarations in the statement: CorrBridge.RCirc

Project declarations used by the proof or definition body

LocalRestore.restSubst, SelectCircuit.substR, SelectCircuit.varSel

def `Game.restore`

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

Two-frame restoration selector (paper Prop. restore / Thm search-gap (iii)): from the predecessor Q and current board Q', cancel delta = nim(Q) XOR nim(Q').

Statement as elaborated and printed by Lean 4.26.0

List ℕ → List ℕ → Option (List ℕ)

Exact source text, lines 407–410

407/-- Two-frame restoration selector (paper Prop. restore / Thm search-gap (iii)):408    from the predecessor Q and current board Q', cancel delta = nim(Q) XOR nim(Q'). -/409def restore (Q Q' : List Nat) : Option (List Nat) :=410  cancelFirst (nimSum Q ^^^ nimSum Q') Q'

Project declarations in the statement: none

Project declarations used by the proof or definition body

Game.cancelFirst, nimSum

def `Game.Move`

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

An ordinary legal Nim move: exactly one heap strictly decreases.

Statement as elaborated and printed by Lean 4.26.0

List ℕ → List ℕ → Prop

Exact source text, lines 24–26

24/-- An ordinary legal Nim move: exactly one heap strictly decreases. -/25def Move (p q : List Nat) : Prop :=26  ∃ pre x post y, p = pre ++ x :: post ∧ q = pre ++ y :: post ∧ y < x

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

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

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

All formulas of a readout: depth ≤ D, size ≤ S, inputs below M.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.CorrBridge.RCirc → ℕ → ℕ → ℕ → ℕ → ℕ → Prop

Exact source text, lines 574–577

574/-- All formulas of a readout: depth ≤ D, size ≤ S, inputs below M. -/575def SelBound (R : RCirc) (N B D S M : Nat) : Prop :=576  R.sel.length = N ∧ R.val.length = B ∧577    ∀ c ∈ R.valid :: (R.sel ++ R.val), depth c ≤ D ∧ size c ≤ S ∧ maxInput c ≤ M

Project declarations in the statement: CorrBridge.RCirc

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.depth, AC0.Circ.maxInput, AC0.Circ.size, CorrBridge.RCirc, CorrBridge.RCirc.sel, CorrBridge.RCirc.val, CorrBridge.RCirc.valid

def `Family.restN`

Module Family (lean/phase6/Family.lean, lines 318–318) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → List NimAudit.AC0.Layer

Exact source text, lines 318–318

318def restN (i : Nat × Nat) : List Layer := restNet i.1 i.2 (rIdx i.2)

Project declarations in the statement: AC0.Layer

Project declarations used by the proof or definition body

ThresholdInst.restNet, WholeGame.rIdx

def `Family.restS`

Module Family (lean/phase6/Family.lean, lines 285–285) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → NimAudit.BinReadout.BCirc

Exact source text, lines 285–285

285def restS (i : Nat × Nat) : BCirc := restBin i.1 i.2 (rIdx i.2)

Project declarations in the statement: BinReadout.BCirc

Project declarations used by the proof or definition body

PriorityEncoder.restBin, WholeGame.rIdx

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

Module ThresholdInst (lean/phase5/ThresholdInst.lean, lines 322–329) · file SHA-256 c8c66599c8e24804…

Decoding the output wires of a binary-selector network (bit reading only).

Statement as elaborated and printed by Lean 4.26.0

List NimAudit.AC0.Layer → ℕ → ℕ → ℕ → (ℕ → Bool) → Option (ℕ × ℕ)

Exact source text, lines 322–329

322/-- Decoding the output wires of a binary-selector network (bit reading only). -/323def netBinSem (net : List Layer) (N r B : Nat) (x : Nat → Bool) : Option (Nat × Nat) :=324  if evalNet net x 0 then325    if toNatBE ((List.range r).map (fun q => evalNet net x (1 + q))) < N then326      some (toNatBE ((List.range r).map (fun q => evalNet net x (1 + q))),327        toNatBE ((List.range B).map (fun k => evalNet net x (1 + r + k))))328    else none329  else none

Project declarations in the statement: AC0.Layer

Project declarations used by the proof or definition body

AC0.Layer, AC0.evalNet, Bridge.toNatBE

def `WholeGame.rIdx`

Module WholeGame (lean/phase5/WholeGame.lean, lines 108–109) · file SHA-256 809a74ad589db609…

Index width used for N heaps.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ

Exact source text, lines 108–109

108/-- Index width used for N heaps. -/109def rIdx (N : Nat) : Nat := N.log2 + 1

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

inductive `WholeGame.TwoFrameWins`

Module WholeGame (lean/phase5/WholeGame.lean, lines 41–50) · file SHA-256 809a74ad589db609…

Stateful two-frame game predicate (opponent to move at the stored board Q): every legal opponent move is answered by a legal reply, the reply's board becomes the new stored board, and play continues. Being inductive, every such play is finite; at a terminal stored board the opponent cannot move and loses.

Statement as elaborated and printed by Lean 4.26.0

(List ℕ → List ℕ → Option (List ℕ)) → List ℕ → Prop

Exact source text, lines 41–50

41/-- Stateful two-frame game predicate (opponent to move at the stored board Q): every42    legal opponent move is answered by a legal reply, the reply's board becomes the new43    stored board, and play continues.  Being inductive, every such play is finite; at a44    terminal stored board the opponent cannot move and loses. -/45inductive TwoFrameWins (reply : List Nat → List Nat → Option (List Nat)) : List Nat → Prop46  | intro (Q : List Nat) :47      (∀ Q', Move Q Q' → (reply Q Q').isSome = true) →48      (∀ Q' R, Move Q Q' → reply Q Q' = some R → Move Q' R) →49      (∀ Q' R, Move Q Q' → reply Q Q' = some R → TwoFrameWins reply R) →50      TwoFrameWins reply Q

Project declarations in the statement: none

Project declarations used by the proof or definition body

Game.Move

def `WholeGame.restReply`

Module WholeGame (lean/phase5/WholeGame.lean, lines 35–39) · file SHA-256 809a74ad589db609…

The player's reply: evaluate the compiled restoration network on (Q, Q'), decode its output wires and apply the decoded move to Q'. Index width r = log₂N + 1.

Statement as elaborated and printed by Lean 4.26.0

ℕ → List ℕ → List ℕ → Option (List ℕ)

Exact source text, lines 35–39

35/-- The player's reply: evaluate the compiled restoration network on (Q, Q'), decode its36    output wires and apply the decoded move to Q'.  Index width r = log₂N + 1. -/37def restReply (B : Nat) (Q Q' : List Nat) : Option (List Nat) :=38  applyM Q' (netBinSem (restNet B Q'.length (Q'.length.log2 + 1)) Q'.length (Q'.length.log2 + 1) B39    (LocalRestore.tf B Q'.length Q Q'))

Project declarations in the statement: none

Project declarations used by the proof or definition body

LocalRestore.tf, SelectCircuit.applyM, ThresholdInst.netBinSem, ThresholdInst.restNet

Full modules

Module	File	Lines	Imports
Family	`lean/phase6/Family.lean`	574	WholeGame
LocalRestore	`lean/phase4/LocalRestore.lean`	587	SelectCircuit
NimCore	`lean/NimCore.lean`	139	`Std`
NimGame	`lean/phase2/NimGame.lean`	634	NimRollout
PriorityEncoder	`lean/phase5/PriorityEncoder.lean`	430	LocalRestore, BinaryReadout
SelectCircuit	`lean/phase4/SelectCircuit.lean`	1064	ControllerBits
ThresholdInst	`lean/phase5/ThresholdInst.lean`	475	ThresholdNet, PriorityEncoder
WholeGame	`lean/phase5/WholeGame.lean`	347	ThresholdInst

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 2A restoration move can be selected from (Q,Q') by a constant-depth circuit

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

theorem LocalRestore.restC_bound

theorem Family.rest_semantics

theorem WholeGame.twoFrame_wins

Definitions these statements use

def LocalRestore.restC

def Game.restore

def Game.Move

def Game.Width

def LocalRestore.tf

def SelectCircuit.selReadout

def nimSum

def SelectCircuit.SelBound

def Family.restN

def Family.restS

def PriorityEncoder.binSem

def ThresholdInst.netBinSem

def WholeGame.rIdx

inductive WholeGame.TwoFrameWins

def WholeGame.restReply

Full modules

theorem `LocalRestore.restore_equiv`

theorem `LocalRestore.restC_bound`

theorem `Family.rest_semantics`

theorem `WholeGame.twoFrame_wins`

def `LocalRestore.restC`

def `Game.restore`

def `Game.Move`

def `Game.Width`

def `LocalRestore.tf`

def `SelectCircuit.selReadout`

def `nimSum`

def `SelectCircuit.SelBound`

def `Family.restN`

def `Family.restS`

def `PriorityEncoder.binSem`

def `ThresholdInst.netBinSem`

def `WholeGame.rIdx`

inductive `WholeGame.TwoFrameWins`

def `WholeGame.restReply`