Appendix C, “A binary index is part of the circuit”The priority encoder produces the binary index of the first candidate, for every flag pattern

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

1 Paper text

A binary index is part of the circuit. Let $s_i$ be the candidate flags after choosing between cancellation and fallback. More than one may be true. Define $f_i=s_i\wedge\bigwedge_{j<i}\neg s_j, \qquad I_k=\bigvee_{\substack{0\le i<N\\\text{bit }k\text{ of }i\text{ is }1}}f_i.$ The $f_i$ flags select the first candidate; the $I_k$ wires give its binary index. Masking the candidate replacement bits by $f_i$ and taking OR gives the value output. Combining validity with $\bigvee_i s_i$ handles the absence of candidates. This uses constant additional depth and polynomial size, rather than an uncosted external search for the first true flag. The Lean priority encoder proves agreement for every flag pattern, including invalid outputs, no candidates, and the cases $N=0$ and $N=1$ . A move index uses $r$ bits with $N\le2^r$ ; the replay counter also stores $N$ and therefore requires $N<2^r$ .

Generated from paper_jmlr.tex, lines 1501–1508.

2 Explain this

Several heaps may qualify; the circuit must pick the first and output its index in binary. With candidate flags $s_i$ : $f_i=s_i\wedge\bigwedge_{j<i}\neg s_j$ marks the first candidate, and index bit $k$ is the OR of the $f_i$ whose index has bit $k$ set. Masking the candidate values by $f_i$ and taking ORs gives the value bits. All of this is constant depth and polynomial size: no hidden "search for the first true flag".

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

PriorityEncoder.encode_correct: for every input assignment the encoder's binary output decodes to exactly the selection readout (first true flag and its value), and to "no move" when the readout is invalid or no flag is true, provided $N\le2^r$ .
PriorityEncoder.encode_noflag, PriorityEncoder.encode_least, PriorityEncoder.encode_zero, PriorityEncoder.encode_one: the edge cases named in the paper (no candidate, several candidates, $N=0$ , $N=1$ with zero index width).
PriorityEncoder.encode_bound: depth grows by at most $3$ ; each formula has size at most $4U^3$ with $U=(N+2)(S+2)$ .

Coverage record
Paper anchor	`par-a-binary-index-is-part-of-the-circuit-p1` (website anchor; the manuscript has no label here)
Displayed as	Appendix C, “A binary index is part of the circuit”
Claim	The priority encoder produces the binary index of the first candidate, for every flag pattern
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 1501–1508; SHA-256 of the normalised block source `979453a04f351f49…`
Lean declarations	`NimAudit.PriorityEncoder.encode_correct` (PriorityEncoder, lines 67–107, file `1be04943f545…`) `NimAudit.PriorityEncoder.encode_bound` (PriorityEncoder, lines 131–200, file `1be04943f545…`) `NimAudit.PriorityEncoder.encode_noflag` (PriorityEncoder, lines 342–348, file `1be04943f545…`) `NimAudit.PriorityEncoder.encode_least` (PriorityEncoder, lines 350–361, file `1be04943f545…`) `NimAudit.PriorityEncoder.encode_zero` (PriorityEncoder, lines 363–366, file `1be04943f545…`) `NimAudit.PriorityEncoder.encode_one` (PriorityEncoder, lines 368–371, file `1be04943f545…`)
Assumptions and domain	Index width $r$ with $N\le 2^r$ (the replay counter needs $N<2^r$ ).
Audited correspondence rows	`app:impl`
Explanations	`explain/c-binary-index`, `formal/c-binary-index`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

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

theorem `PriorityEncoder.encode_bound`

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

ENCODER RESOURCES: from source formulas of depth ≤ D, size ≤ S on inputs below M, every output formula has depth ≤ D + 3, size ≤ 4·((N+2)(S+2))^3 and inputs below M.

Statement as elaborated and printed by Lean 4.26.0

∀ (R : NimAudit.CorrBridge.RCirc) {N B r D S M : ℕ},
  R.sel.length = N →
    R.val.length = B →
      N ≤ 2 ^ r →
        (∀ c ∈ R.valid :: (R.sel ++ R.val), c.depth ≤ D ∧ c.size ≤ S ∧ c.maxInput ≤ M) →
          NimAudit.PriorityEncoder.BinBound (NimAudit.PriorityEncoder.encode R N r) N B r (D + 3)
            (4 * ((N + 2) * (S + 2)) ^ 3) M

Exact source text, lines 131–200

131/-- ENCODER RESOURCES: from source formulas of depth ≤ D, size ≤ S on inputs below M,132    every output formula has depth ≤ D + 3, size ≤ 4·((N+2)(S+2))^3 and inputs below M. -/133theorem encode_bound (R : RCirc) {N B r D S M : Nat} (hlen : R.sel.length = N) (hvl : R.val.length = B)134    (hr : N ≤ 2 ^ r)135    (hall : ∀ c ∈ R.valid :: (R.sel ++ R.val), depth c ≤ D ∧ size c ≤ S ∧ maxInput c ≤ M) :136    BinBound (encode R N r) N B r (D + 3) (4 * ((N + 2) * (S + 2)) ^ 3) M := by137  generalize hU : (N + 2) * (S + 2) = U138  have hNU : N + 2 ≤ U := by139    rw [← hU]; exact Nat.le_mul_of_pos_right (N + 2) (by omega)140  have hSU : S + 2 ≤ U := by141    rw [← hU]; exact Nat.le_mul_of_pos_left (S + 2) (by omega)142  have hU1 : 1 ≤ U := by omega143  have hsel : ∀ i < N, depth (getC R.sel i) ≤ D ∧ size (getC R.sel i) ≤ S ∧ maxInput (getC R.sel i) ≤ M :=144    fun i hi => hall _ (by simp [getC_mem (show i < R.sel.length by omega)])145  have hsel1 : ∀ i < N, size (getC R.sel i) ≤ 1 * U ^ 1 := fun i hi => by146    have := (hsel i hi).2.1; simp; omega147  have hF : ∀ i < N, depth (firstF R.sel i) ≤ D + 2 ∧ size (firstF R.sel i) ≤ 3 * U ^ 2 ∧148      maxInput (firstF R.sel i) ≤ M := by149    intro i hi150    refine ⟨dp_firstC (fun i' hi' => (hsel i' (by omega)).1),151      sz_firstC hU1 (by omega) (fun i' hi' => hsel1 i' (by omega)),152      mx_firstC (fun i' hi' => (hsel i' (by omega)).2.2)⟩153  refine ⟨by simp [encode], by simp [encode, hvl], hr, ?_⟩154  intro c hc155  simp only [encode, List.mem_cons, List.mem_append, List.mem_map, List.mem_range] at hc156  rcases hc with rfl | ⟨q, _, rfl⟩ | hcv157  · -- validity158    have hv := hall R.valid (by simp)159    refine ⟨?_, ?_, ?_⟩160    · apply depth_and_le; intro c hc161      simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc162      rcases hc with rfl | rfl163      · omega164      · apply depth_or_le; intro c hc165        obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc166        have := (hsel i (List.mem_range.mp hi)).1; omega167    · apply size_and_le hU1 (by simp; omega)168      intro c hc169      simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc170      rcases hc with rfl | rfl171      · exact lift1 hU1 (show size R.valid ≤ 1 * U ^ 1 by simp; omega) (by omega) (by omega)172      · exact lift1 hU1 (size_or_le hU1 (by simp; omega) (fun c hc => by173          obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc; exact hsel1 i (List.mem_range.mp hi)))174          (by omega) (by omega)175    · apply ControllerBits.maxInput_and_le; intro c hc176      simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc177      rcases hc with rfl | rfl178      · exact hv.2.2179      · apply ControllerBits.maxInput_or_le; intro c hc180        obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc181        exact (hsel i (List.mem_range.mp hi)).2.2182  · -- index bit q183    refine ⟨?_, ?_, ?_⟩184    · unfold idxBit; apply depth_or_le; intro c hc185      obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc186      exact (hF i (List.mem_range.mp (List.mem_filter.mp hi).1)).1187    · unfold idxBit188      apply size_or_le hU1 (by189        have := List.length_filter_le (fun i => i.testBit (r - 1 - q)) (List.range N)190        simp only [List.length_map, List.length_range] at this ⊢; omega)191      intro c hc192      obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc193      exact (hF i (List.mem_range.mp (List.mem_filter.mp hi).1)).2.1194    · unfold idxBit; apply ControllerBits.maxInput_or_le; intro c hc195      obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc196      exact (hF i (List.mem_range.mp (List.mem_filter.mp hi).1)).2.2197  · -- value bit (unchanged)198    have h := hall c (by simp [hcv])199    refine ⟨by omega, ?_, h.2.2⟩200    exact lift1 hU1 (show size c ≤ 1 * U ^ 1 by simp; omega) (by omega) (by omega)

Project declarations in the statement: AC0.Circ, AC0.Circ.depth, AC0.Circ.maxInput, AC0.Circ.size, CorrBridge.RCirc, CorrBridge.RCirc.sel, CorrBridge.RCirc.val, CorrBridge.RCirc.valid, PriorityEncoder.BinBound, PriorityEncoder.encode

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.and, AC0.Circ.depth, AC0.Circ.maxInput, AC0.Circ.or, AC0.Circ.size, BinReadout.BCirc.idx, BinReadout.BCirc.val, BinReadout.BCirc.valid, BinReadout.getC_mem, ControllerBits.maxInput_and_le, ControllerBits.maxInput_or_le, CorrBridge.RCirc, CorrBridge.RCirc.sel, CorrBridge.RCirc.val, CorrBridge.RCirc.valid, CorrBridge.depth_and_le, CorrBridge.depth_or_le, CorrBridge.getC, CorrBridge.size_and_le, CorrBridge.size_or_le, PriorityEncoder.BinBound.mk, PriorityEncoder.encode, PriorityEncoder.firstF, PriorityEncoder.idxBit, SelectCircuit.dp_firstC, SelectCircuit.lift1, SelectCircuit.mx_firstC, SelectCircuit.sz_firstC

theorem `PriorityEncoder.encode_noflag`

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

No true candidate flag: no move (even if the source valid flag is true).

Statement as elaborated and printed by Lean 4.26.0

∀ (R : NimAudit.CorrBridge.RCirc) (N r : ℕ),
  R.sel.length = N →
    ∀ (z : ℕ → Bool),
      (∀ i < N, NimAudit.AC0.Circ.eval z (NimAudit.CorrBridge.getC R.sel i) = false) →
        NimAudit.PriorityEncoder.binSem (NimAudit.PriorityEncoder.encode R N r) N z = none

Exact source text, lines 342–348

342/-- No true candidate flag: no move (even if the source valid flag is true). -/343theorem encode_noflag (R : RCirc) (N r : Nat) (hlen : R.sel.length = N) (z : Nat → Bool)344    (hno : ∀ i < N, eval z (getC R.sel i) = false) : binSem (encode R N r) N z = none := by345  have hor : eval z (or ((List.range N).map (getC R.sel))) = false := by346    rw [eval_or, List.any_map]; apply List.any_eq_false.mpr347    intro i hi; simpa using hno i (List.mem_range.mp hi)348  simp [binSem, encode, hor]

Project declarations in the statement: AC0.Circ, AC0.Circ.eval, CorrBridge.RCirc, CorrBridge.RCirc.sel, CorrBridge.getC, PriorityEncoder.binSem, PriorityEncoder.encode

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, BinReadout.BCirc.idx, BinReadout.BCirc.val, BinReadout.BCirc.valid, Bridge.toNatBE, CorrBridge.RCirc, CorrBridge.RCirc.sel, CorrBridge.RCirc.valid, CorrBridge.getC, PriorityEncoder.encode

theorem `PriorityEncoder.encode_least`

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

Several true flags: the encoded index is the least true one.

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.AC0.Circ.eval z R.valid = true →
          ∀ {i : ℕ},
            i < N →
              NimAudit.AC0.Circ.eval z (NimAudit.CorrBridge.getC R.sel i) = true →
                (∀ k < i, NimAudit.AC0.Circ.eval z (NimAudit.CorrBridge.getC R.sel k) = false) →
                  NimAudit.PriorityEncoder.binSem (NimAudit.PriorityEncoder.encode R N r) N z =
                    some (i, NimAudit.Bridge.toNatBE (List.map (NimAudit.AC0.Circ.eval z) R.val))

Exact source text, lines 350–361

350/-- Several true flags: the encoded index is the least true one. -/351theorem encode_least (R : RCirc) (N r : Nat) (hlen : R.sel.length = N) (hr : N ≤ 2 ^ r) (z : Nat → Bool)352    (hv : eval z R.valid = true) {i : Nat} (hi : i < N) (hti : eval z (getC R.sel i) = true)353    (hlow : ∀ k < i, eval z (getC R.sel k) = false) :354    binSem (encode R N r) N z = some (i, toNatBE (R.val.map (eval z))) := by355  rw [encode_correct R N r hlen hr z]356  have hft : firstTrue (R.sel.map (eval z)) = some i := by357    rw [firstTrue_some_iff]358    refine ⟨by simp [hlen, hi], ?_, ?_⟩359    · rw [← eval_getC]; exact hti360    · intro k hk; rw [← eval_getC]; exact hlow k hk361  simp [selReadout, hv, hft]

Project declarations in the statement: AC0.Circ, AC0.Circ.eval, Bridge.toNatBE, CorrBridge.RCirc, CorrBridge.RCirc.sel, CorrBridge.RCirc.val, CorrBridge.RCirc.valid, CorrBridge.getC, PriorityEncoder.binSem, PriorityEncoder.encode

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.eval_getC, CorrBridge.firstTrue, CorrBridge.firstTrue_some_iff, CorrBridge.getC, PriorityEncoder.binSem, PriorityEncoder.encode, PriorityEncoder.encode_correct, SelectCircuit.selReadout

theorem `PriorityEncoder.encode_zero`

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

N = 0: never a move, for any index width.

Statement as elaborated and printed by Lean 4.26.0

∀ (R : NimAudit.CorrBridge.RCirc) (r : ℕ),
  R.sel.length = 0 →
    ∀ (z : ℕ → Bool),
      NimAudit.PriorityEncoder.binSem (NimAudit.PriorityEncoder.encode R 0 r) 0 z = none

Exact source text, lines 363–366

363/-- N = 0: never a move, for any index width. -/364theorem encode_zero (R : RCirc) (r : Nat) (hlen : R.sel.length = 0) (z : Nat → Bool) :365    binSem (encode R 0 r) 0 z = none :=366  encode_noflag R 0 r hlen z (fun i hi => absurd hi (by omega))

Project declarations in the statement: AC0.Circ, CorrBridge.RCirc, CorrBridge.RCirc.sel, PriorityEncoder.binSem, PriorityEncoder.encode

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.eval, CorrBridge.RCirc, CorrBridge.RCirc.sel, CorrBridge.getC, PriorityEncoder.encode_noflag

theorem `PriorityEncoder.encode_one`

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

N = 1 with zero index width (r = 0): the index list is empty and decodes to 0.

Statement as elaborated and printed by Lean 4.26.0

∀ (R : NimAudit.CorrBridge.RCirc),
  R.sel.length = 1 →
    ∀ (z : ℕ → Bool),
      (NimAudit.PriorityEncoder.encode R 1 0).idx = [] ∧
        NimAudit.PriorityEncoder.binSem (NimAudit.PriorityEncoder.encode R 1 0) 1 z =
          NimAudit.SelectCircuit.selReadout R z

Exact source text, lines 368–371

368/-- N = 1 with zero index width (r = 0): the index list is empty and decodes to 0. -/369theorem encode_one (R : RCirc) (hlen : R.sel.length = 1) (z : Nat → Bool) :370    (encode R 1 0).idx = [] ∧ binSem (encode R 1 0) 1 z = selReadout R z :=371  ⟨rfl, encode_correct R 1 0 hlen (by decide) z⟩

Project declarations in the statement: AC0.Circ, BinReadout.BCirc.idx, CorrBridge.RCirc, CorrBridge.RCirc.sel, PriorityEncoder.binSem, PriorityEncoder.encode, SelectCircuit.selReadout

Project declarations used by the proof or definition body

AC0.Circ, BinReadout.BCirc.idx, CorrBridge.RCirc, CorrBridge.RCirc.sel, PriorityEncoder.binSem, PriorityEncoder.encode, PriorityEncoder.encode_correct, SelectCircuit.selReadout

Definitions these statements use

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

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 `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 `AC0.Circ.depth`

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

Statement as elaborated and printed by Lean 4.26.0

NimAudit.AC0.Circ → ℕ

Exact source text, lines 61–66

61def depth : Circ → Nat62  | input _ => 063  | const _ => 064  | not c => depth c + 165  | and cs => listMax (cs.attach.map (fun ⟨c, _⟩ => depth c)) + 166  | or cs => listMax (cs.attach.map (fun ⟨c, _⟩ => depth c)) + 1

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.listMax, AC0.Circ.not, AC0.Circ.or, AC0.Circ.rec, AC0.Circ.rec_1

def `AC0.Circ.maxInput`

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

One more than the largest input index used (0 if none).

Statement as elaborated and printed by Lean 4.26.0

NimAudit.AC0.Circ → ℕ

Exact source text, lines 68–74

68/-- One more than the largest input index used (0 if none). -/69def maxInput : Circ → Nat70  | input i => i + 171  | const _ => 072  | not c => maxInput c73  | and cs => listMax (cs.attach.map (fun ⟨c, _⟩ => maxInput c))74  | or cs => listMax (cs.attach.map (fun ⟨c, _⟩ => maxInput 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.listMax, AC0.Circ.not, AC0.Circ.or, AC0.Circ.rec, AC0.Circ.rec_1

def `AC0.Circ.size`

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

Statement as elaborated and printed by Lean 4.26.0

NimAudit.AC0.Circ → ℕ

Exact source text, lines 51–56

51def size : Circ → Nat52  | input _ => 153  | const _ => 154  | not c => size c + 155  | and cs => (cs.attach.map (fun ⟨c, _⟩ => size c)).sum + 156  | or cs => (cs.attach.map (fun ⟨c, _⟩ => size c)).sum + 1

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 `CorrBridge.RCirc.val`

Module NimCorrBridge (lean/phase3/NimCorrBridge.lean, lines 37–37) · 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 37–37

37  val : List Circ

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

Project declarations used by the proof or definition body

CorrBridge.RCirc

def `CorrBridge.RCirc.valid`

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

Statement as elaborated and printed by Lean 4.26.0

NimAudit.CorrBridge.RCirc → NimAudit.AC0.Circ

Exact source text, lines 35–35

35  valid : Circ

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

Project declarations used by the proof or definition body

CorrBridge.RCirc

inductive `PriorityEncoder.BinBound`

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

Resource bounds for binary readout formulas on an arbitrary input support M.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.BinReadout.BCirc → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → Prop

Exact source text, lines 111–116

111/-- Resource bounds for binary readout formulas on an arbitrary input support M. -/112structure BinBound (S : BCirc) (N B r D Sz M : Nat) : Prop where113  idx_len : S.idx.length = r114  val_len : S.val.length = B115  width : N ≤ 2 ^ r116  all : ∀ c ∈ S.valid :: (S.idx ++ S.val), depth c ≤ D ∧ size c ≤ Sz ∧ maxInput c ≤ M

Project declarations in the statement: BinReadout.BCirc

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.depth, AC0.Circ.maxInput, AC0.Circ.size, BinReadout.BCirc, BinReadout.BCirc.idx, BinReadout.BCirc.val, BinReadout.BCirc.valid

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

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

Statement as elaborated and printed by Lean 4.26.0

List NimAudit.AC0.Circ → ℕ → NimAudit.AC0.Circ

Exact source text, lines 87–87

87def getC (cs : List Circ) (i : Nat) : Circ := cs.getD i (const false)

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.const

def `Bridge.toNatBE`

Module BitBridge (lean/phase3/BitBridge.lean, lines 57–60) · file SHA-256 000644dc271d27f9…

Big-endian value of a bit list.

Statement as elaborated and printed by Lean 4.26.0

List Bool → ℕ

Exact source text, lines 57–60

57/-- Big-endian value of a bit list. -/58def toNatBE : List Bool → Nat59  | [] => 060  | b :: v => (if b then 2 ^ v.length else 0) + toNatBE v

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `BinReadout.BCirc.idx`

Module BinaryReadout (lean/phase4/BinaryReadout.lean, lines 27–27) · file SHA-256 17ef1a62ba9edafb…

Statement as elaborated and printed by Lean 4.26.0

NimAudit.BinReadout.BCirc → List NimAudit.AC0.Circ

Exact source text, lines 27–27

27  idx : List Circ

Project declarations in the statement: AC0.Circ, BinReadout.BCirc

Project declarations used by the proof or definition body

BinReadout.BCirc

Full modules

Module	File	Lines	Imports
BinaryReadout	`lean/phase4/BinaryReadout.lean`	333	FiniteNet, NimCorrBridge
BitBridge	`lean/phase3/BitBridge.lean`	560	Circuit
Circuit	`lean/phase3/Circuit.lean`	1151	NimProbability
NimCorrBridge	`lean/phase3/NimCorrBridge.lean`	922	BitBridge
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).

Appendix C, “A binary index is part of the circuit”The priority encoder produces the binary index of the first candidate, for every flag pattern

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 PriorityEncoder.encode_correct

theorem PriorityEncoder.encode_bound

theorem PriorityEncoder.encode_noflag

theorem PriorityEncoder.encode_least

theorem PriorityEncoder.encode_zero

theorem PriorityEncoder.encode_one

Definitions these statements use

def PriorityEncoder.encode

inductive AC0.Circ

inductive CorrBridge.RCirc

def CorrBridge.RCirc.sel

def PriorityEncoder.binSem

def SelectCircuit.selReadout

def AC0.Circ.depth

def AC0.Circ.maxInput

def AC0.Circ.size

def CorrBridge.RCirc.val

def CorrBridge.RCirc.valid

inductive PriorityEncoder.BinBound

def AC0.Circ.eval

def CorrBridge.getC

def Bridge.toNatBE

def BinReadout.BCirc.idx

Full modules

theorem `PriorityEncoder.encode_correct`

theorem `PriorityEncoder.encode_bound`

theorem `PriorityEncoder.encode_noflag`

theorem `PriorityEncoder.encode_least`

theorem `PriorityEncoder.encode_zero`

theorem `PriorityEncoder.encode_one`

def `PriorityEncoder.encode`

inductive `AC0.Circ`

inductive `CorrBridge.RCirc`

def `CorrBridge.RCirc.sel`

def `PriorityEncoder.binSem`

def `SelectCircuit.selReadout`

def `AC0.Circ.depth`

def `AC0.Circ.maxInput`

def `AC0.Circ.size`

def `CorrBridge.RCirc.val`

def `CorrBridge.RCirc.valid`

inductive `PriorityEncoder.BinBound`

def `AC0.Circ.eval`

def `CorrBridge.getC`

def `Bridge.toNatBE`

def `BinReadout.BCirc.idx`