Lemma 5.4With at most t changed heaps (t fixed), Δ is computed by polynomial-size constant-depth circuits

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

1 Paper text

Lemma 5.4 (Bounded-change differences) Fix a constant $t\in\N$ . Let $P$ and $P'$ be NIM positions whose heap vectors differ in at most $t$ heaps. Then $\Delta(P,P')$ can be computed by an $\AC^0$ circuit of polynomial size (in the input length).

Generated from paper_jmlr.tex, lines 502–507.

2 Explain this

The statement. If two boards differ in at most a fixed number $t$ of heaps, their nimber difference can be computed by an AC⁰ circuit.

Why. Compare the two boards heap by heap to find which heaps changed (a local test), XOR each changed pair, and XOR together at most $t$ such values, which is a constant-size parity. The circuit has to find where the changes are; it does this by trying every possible set of at most $t$ changed heaps in parallel ( $O(N^t)$ sets).

Why it matters. It is the formal core of the two-frame bypass: the transition is easy even though the state is hard.

Caveat. $t$ must be a constant: the depth bound grows with $t$ and the size bound is polynomial with an exponent depending on $t$ . With an unbounded number of changes the problem becomes global parity again.

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

The two frames are laid out as one bit vector (LocalRestore.tf). For each bit $q$ , the circuit LocalRestore.bdC $B\ N\ t\ q$ is built from per-heap comparisons and exact "at least $k$ of these heaps differ in bit $q$ " counters (valid because at most $t$ heaps differ).

LocalRestore.bdC_eval: if at most $t$ heaps differ, the circuit outputs bit $q$ of $\operatorname{nim}(Q)\oplus\operatorname{nim}(Q')$ .
LocalRestore.bdDelta_eq: the $B$ output bits assemble to exactly that number.
LocalRestore.bdC_res: depth at most $2t+8$ , size at most $(2t+6)(N+t+11)^{3t+6}$ , reading only the two frames.

The construction differs in detail from the subset enumeration in Appendix E (it counts instead of enumerating subsets) but proves the same lemma with explicit bounds.

Coverage record
Paper anchor	`lem:nimber-diff-ac0` (manuscript label)
Displayed as	Lemma 5.4
Claim	With at most t changed heaps (t fixed), Δ is computed by polynomial-size constant-depth circuits
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 502–507; SHA-256 of the normalised block source `f7c70f3c55b3196c…`
Lean declarations	`NimAudit.LocalRestore.bdC_eval` (LocalRestore, lines 343–375, file `fc4c7f908b0c…`) `NimAudit.LocalRestore.bdDelta_eq` (LocalRestore, lines 377–382, file `fc4c7f908b0c…`) `NimAudit.LocalRestore.bdC_res` (LocalRestore, lines 518–545, file `fc4c7f908b0c…`)
Assumptions and domain	Both boards have $N$ heaps of $B$ bits and differ in at most $t$ heaps; $t$ is a fixed constant (the depth bound $2t+8$ and the size exponent depend on $t$ ).
Audited correspondence rows	`lem:nimber-diff-ac0`, `app:nimberdiff`
Explanations	`explain/lem:nimber-diff-ac0`, `formal/lem:nimber-diff-ac0`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `LocalRestore.bdC_eval`

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

BOUNDED-CHANGE DIFFERENCES: if at most t heaps changed, the delta circuits compute nim(Q) ⊕ nim(Q') exactly.

Statement as elaborated and printed by Lean 4.26.0

∀ {B N t : ℕ} {Q Q' : List ℕ},
  Q.length = N →
    Q'.length = N →
      NimAudit.Game.Width B Q →
        NimAudit.Game.Width B Q' →
          NimAudit.LocalRestore.cntR (fun i => decide (Q.getD i 0 ≠ Q'.getD i 0)) N ≤ t →
            ∀ (q : ℕ),
              NimAudit.AC0.Circ.eval (NimAudit.LocalRestore.tf B N Q Q')
                  (NimAudit.LocalRestore.bdC B N t q) =
                (NimAudit.nimSum Q ^^^ NimAudit.nimSum Q').testBit q

Exact source text, lines 343–375

343/-- BOUNDED-CHANGE DIFFERENCES: if at most t heaps changed, the delta circuits compute344    nim(Q) ⊕ nim(Q') exactly. -/345theorem bdC_eval {B N t : Nat} {Q Q' : List Nat} (hQ : Q.length = N) (hQ' : Q'.length = N)346    (hw : Width B Q) (hw' : Width B Q')347    (ht : cntR (fun i => decide (Q.getD i 0 ≠ Q'.getD i 0)) N ≤ t) (q : Nat) :348    eval (tf B N Q Q') (bdC B N t q) = (nimSum Q ^^^ nimSum Q').testBit q := by349  unfold bdC350  by_cases hq : q < B351  · simp only [hq, if_true]352    have hyc : (fun i => eval (tf B N Q Q') (yC B N i (B - 1 - q))) =353        fun i => if i < N then ((Q.getD i 0).testBit q != (Q'.getD i 0).testBit q) else354          eval (tf B N Q Q') (yC B N i (B - 1 - q)) := by355      funext i356      by_cases hi : i < N357      · rw [if_pos hi, yC_eval hQ hQ' hi (by omega), show B - 1 - (B - 1 - q) = q by omega]358      · rw [if_neg hi]359    have hcnt : cntR (fun i => eval (tf B N Q Q') (yC B N i (B - 1 - q))) N =360        cntR (fun i => (Q.getD i 0).testBit q != (Q'.getD i 0).testBit q) N := by361      unfold cntR362      congr 1363      apply List.filter_congr364      intro i hi365      rw [yC_eval hQ hQ' (List.mem_range.mp hi) (by omega), show B - 1 - (B - 1 - q) = q by omega]366    have hle : cntR (fun i => (Q.getD i 0).testBit q != (Q'.getD i 0).testBit q) N ≤ t := by367      refine Nat.le_trans (cntR_mono N (fun i hi h => ?_)) ht368      simp only [bne_iff_ne, ne_eq] at h369      simp only [decide_eq_true_iff]370      intro he; rw [he] at h; exact h rfl371    rw [parC_eval _ _ t N (by rw [hcnt]; exact hle), hcnt,372      nimSum_xor_testBit Q Q' (by rw [hQ, hQ']) q, hQ]373  · simp only [hq, if_false, eval_const]374    rw [Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le (Nat.xor_lt_two_pow (nimSum_lt hw) (nimSum_lt hw'))375      (Nat.pow_le_pow_right (by decide) (by omega)))]

Project declarations in the statement: AC0.Circ.eval, Game.Width, LocalRestore.bdC, LocalRestore.cntR, LocalRestore.tf, nimSum

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.const, AC0.Circ.eval, AC0.Circ.eval_const, Game.Width, Game.nimSum_lt, LocalRestore.bdC, LocalRestore.cntR, LocalRestore.cntR_mono, LocalRestore.nimSum_xor_testBit, LocalRestore.parC, LocalRestore.parC_eval, LocalRestore.tf, LocalRestore.yC, LocalRestore.yC_eval, nimSum

theorem `LocalRestore.bdDelta_eq`

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

Statement as elaborated and printed by Lean 4.26.0

∀ {B N t : ℕ} {Q Q' : List ℕ},
  Q.length = N →
    Q'.length = N →
      NimAudit.Game.Width B Q →
        NimAudit.Game.Width B Q' →
          NimAudit.LocalRestore.cntR (fun i => decide (Q.getD i 0 ≠ Q'.getD i 0)) N ≤ t →
            (NimAudit.Game.ofBits B fun q =>
                NimAudit.AC0.Circ.eval (NimAudit.LocalRestore.tf B N Q Q')
                  (NimAudit.LocalRestore.bdC B N t q)) =
              NimAudit.nimSum Q ^^^ NimAudit.nimSum Q'

Exact source text, lines 377–382

377theorem bdDelta_eq {B N t : Nat} {Q Q' : List Nat} (hQ : Q.length = N) (hQ' : Q'.length = N)378    (hw : Width B Q) (hw' : Width B Q')379    (ht : cntR (fun i => decide (Q.getD i 0 ≠ Q'.getD i 0)) N ≤ t) :380    ofBits B (fun q => eval (tf B N Q Q') (bdC B N t q)) = nimSum Q ^^^ nimSum Q' :=381  ofBits_testBit_eq (Nat.xor_lt_two_pow (nimSum_lt hw) (nimSum_lt hw')) _382    (fun q _ => bdC_eval hQ hQ' hw hw' ht q)

Project declarations in the statement: AC0.Circ.eval, Game.Width, Game.ofBits, LocalRestore.bdC, LocalRestore.cntR, LocalRestore.tf, nimSum

Project declarations used by the proof or definition body

AC0.Circ.eval, Game.Width, Game.nimSum_lt, LocalRestore.bdC, LocalRestore.bdC_eval, LocalRestore.cntR, LocalRestore.tf, Recurrent.ofBits_testBit_eq, nimSum

theorem `LocalRestore.bdC_res`

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

BOUNDED-CHANGE DELTA RESOURCES: depth ≤ 2t + 8 and size ≤ (2t+6)·U^(3t+6) with U = N + t + 11; inputs from the two frames only. Constant depth and polynomial size for every fixed t.

Statement as elaborated and printed by Lean 4.26.0

∀ {B N : ℕ} (t q : ℕ),
  (NimAudit.LocalRestore.bdC B N t q).depth ≤ 2 * t + 8 ∧
    (NimAudit.LocalRestore.bdC B N t q).size ≤ (2 * t + 6) * (N + t + 11) ^ (3 * t + 6) ∧
      (NimAudit.LocalRestore.bdC B N t q).maxInput ≤ 2 * (B * N)

Exact source text, lines 518–545

518/-- BOUNDED-CHANGE DELTA RESOURCES: depth ≤ 2t + 8 and size ≤ (2t+6)·U^(3t+6) with519    U = N + t + 11; inputs from the two frames only.  Constant depth and polynomial size520    for every fixed t. -/521theorem bdC_res (t q : Nat) :522    depth (bdC B N t q) ≤ 2 * t + 8 ∧ size (bdC B N t q) ≤ (2 * t + 6) * (N + t + 11) ^ (3 * t + 6) ∧523      maxInput (bdC B N t q) ≤ 2 * (B * N) := by524  unfold bdC525  by_cases hq : q < B526  · simp only [hq, if_true]527    have hy : ∀ i, size (yC B N i (B - 1 - q)) ≤ N + t + 11 ∧ depth (yC B N i (B - 1 - q)) ≤ 3 :=528      fun i => ⟨by have := (yC_res (B := B) (N := N) i (B - 1 - q)).2; omega, (yC_res i _).1⟩529    have h := parC_res (by omega) _ hy t N (by omega) (by omega)530    refine ⟨by omega, h.1, ?_⟩531    unfold parC532    apply ControllerBits.maxInput_or_le; intro c hc533    obtain ⟨k, _, rfl⟩ := List.mem_map.mp hc534    split535    · apply ControllerBits.maxInput_and_le; intro c hc536      simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc537      have hyM : ∀ i < N, maxInput (yC B N i (B - 1 - q)) ≤ 2 * (B * N) := fun i hi => yC_max hi (by omega)538      rcases hc with rfl | rfl539      · exact atLeast_max _ hyM k N (Nat.le_refl _)540      · simp only [maxInput_not]; exact atLeast_max _ hyM (k + 1) N (Nat.le_refl _)541    · simp542  · simp only [hq, if_false, depth_const, size_const, maxInput_const]543    refine ⟨by omega, ?_, by omega⟩544    have h1 : 1 ≤ (N + t + 11) ^ (3 * t + 6) := Nat.pow_pos (by omega)545    exact Nat.le_trans h1 (Nat.le_mul_of_pos_left _ (by omega))

Project declarations in the statement: AC0.Circ.depth, AC0.Circ.maxInput, AC0.Circ.size, LocalRestore.bdC

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.and, AC0.Circ.const, AC0.Circ.depth, AC0.Circ.depth_const, AC0.Circ.maxInput, AC0.Circ.maxInput_const, AC0.Circ.maxInput_not, AC0.Circ.not, AC0.Circ.size, AC0.Circ.size_const, ControllerBits.maxInput_and_le, ControllerBits.maxInput_or_le, LocalRestore.atLeastC, LocalRestore.atLeast_max, LocalRestore.bdC, LocalRestore.parC, LocalRestore.parC_res, LocalRestore.yC, LocalRestore.yC_max, LocalRestore.yC_res

Definitions these statements use

def `LocalRestore.bdC`

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

Little-endian bit q of the bounded-change delta (t = maximum number of changed heaps).

Statement as elaborated and printed by Lean 4.26.0

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

Exact source text, lines 303–304

303/-- Little-endian bit q of the bounded-change delta (t = maximum number of changed heaps). -/304def bdC (B N t q : Nat) : Circ := if q < B then parC (fun i => yC B N i (B - 1 - q)) t N else const false

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.const, LocalRestore.parC, 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 `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.cntR`

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

Number of indices below n satisfying p.

Statement as elaborated and printed by Lean 4.26.0

(ℕ → Bool) → ℕ → ℕ

Exact source text, lines 233–234

233/-- Number of indices below n satisfying p. -/234def cntR (p : Nat → Bool) (n : Nat) : Nat := ((List.range n).filter p).length

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `nimSum`

Module NimCore (lean/NimCore.lean, lines 7–9) · file SHA-256 b07db6c505210d5a…

Statement as elaborated and printed by Lean 4.26.0

List ℕ → ℕ

Exact source text, lines 7–9

7def nimSum : List Nat → Nat8  | [] => 09  | h :: t => h ^^^ nimSum t

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Game.ofBits`

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

The number with bits f 0, ..., f (B-1).

Statement as elaborated and printed by Lean 4.26.0

ℕ → (ℕ → Bool) → ℕ

Exact source text, lines 178–181

178/-- The number with bits f 0, ..., f (B-1). -/179def ofBits : Nat → (Nat → Bool) → Nat180  | 0, _ => 0181  | B + 1, f => 2 ^ B * (if f B then 1 else 0) + ofBits B f

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

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

Full modules

Module	File	Lines	Imports
Circuit	`lean/phase3/Circuit.lean`	1151	NimProbability
LocalRestore	`lean/phase4/LocalRestore.lean`	587	SelectCircuit
NimCore	`lean/NimCore.lean`	139	`Std`
NimGame	`lean/phase2/NimGame.lean`	634	NimRollout

Build evidence: fresh isolated rebuild of all 38 bundled modules with Lean (version 4.26.0, started 2026-10-10T15:21:56Z, finished 2026-10-10T15:27:00Z: 38/38 modules compiled, 1588 axiom reports, no errors. See Build for the commands and the independent audit of 2026-10-10 (dated evidence).

Lemma 5.4With at most t changed heaps (t fixed), Δ is computed by polynomial-size constant-depth circuits

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

theorem LocalRestore.bdDelta_eq

theorem LocalRestore.bdC_res

Definitions these statements use

def LocalRestore.bdC

def LocalRestore.tf

def AC0.Circ.eval

def Game.Width

def LocalRestore.cntR

def nimSum

def Game.ofBits

def AC0.Circ.depth

def AC0.Circ.maxInput

def AC0.Circ.size

Full modules

theorem `LocalRestore.bdC_eval`

theorem `LocalRestore.bdDelta_eq`

theorem `LocalRestore.bdC_res`

def `LocalRestore.bdC`

def `LocalRestore.tf`

def `AC0.Circ.eval`

def `Game.Width`

def `LocalRestore.cntR`

def `nimSum`

def `Game.ofBits`

def `AC0.Circ.depth`

def `AC0.Circ.maxInput`

def `AC0.Circ.size`