Appendix C, “The recurrent update”Scan and replay updates are shallow; bit-level refinement and register bounds hold on well-formed streams

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

1 Paper text

The recurrent update. Scan mode updates the accumulator by two-bit XORs. Replay mode tests the current row against the stored summary, retains the first cancelling candidate and a fallback, and increments the row counter. Counter bit $k$ changes exactly when all lower bits are one, so increment also has a shallow circuit. Mode, validity and reset flags select the appropriate register updates. Induction over well-formed token streams proves that every reachable register fits its allotted width and that the output move uses the summary from the same board’s first scan. The input protocol supplies the repeated rows; the controller does not secretly store the board.

Generated from paper_jmlr.tex, lines 1510–1511.

2 Explain this

In scan mode the update XORs the row into the accumulator, two bits at a time. In replay mode it tests the row against the stored summary, keeps the first cancelling candidate and a fallback, and increments a counter (bit $k$ flips when all lower bits are one, also shallow). Mode, validity and reset flags select which registers change. On well-formed streams every reachable register fits its width, and the emitted move uses the summary from the same board's first scan. The replayed rows come from the input protocol; the controller does not secretly store the board.

Row-wise recurrence: registers, separators and replay

Exact construction trace Every value is computed from the construction’s definitions for the example shown.

The board arrives as a stream of rows, one heap per token, with separators (SEP) between positions and a reset at the start of a game. Step through the replay controller: in scan mode it XORs each row into the accumulator; the first separator outputs the summary, stores it and switches to replay mode; during replay the same rows arrive again and each is tested against the stored summary, keeping the first cancelling candidate and a fallback; the second separator outputs the move. The board-storage variant instead writes the rows into memory and chooses the move at its single separator. In the replay controller a separator clears the accumulator and keeps the summary of the position just completed, with its validity bit; an extra separator is read as an empty position, whose summary is 0. Only a reset returns every register, validity included, to its initial value. The board-storage separator clears its accumulator and pointer and keeps the stored board. The third protocol shows the summary mechanism of Proposition 5.13 alone: it reports summaries and differences but chooses no move.

The current NIM board already determines optimal play. The memory shown here makes that answer computationally accessible by retaining partial results across rows; an earlier game position is needed only for the optional comparison of consecutive positions.

RESETreset
row 3scan
row 4scan
row 6scan
SEPsummary
row 3replay
row 4replay
row 6replay
SEPmove
row 2scan
row 4scan
row 1scan
SEPsummary
row 2replay
row 4replay
row 1replay
SEPmove

17 / 17 SEP: separator after replay: output the move, return to scan mode

Registers after this update

mode: scan
accumulator: 0 000
previous summary: 7 111
stored summary used in replay: 7
heap counter: 0
first candidate: no move
first fallback: no move

Outputs so far

after token 5: summary σ = 1 (no previous summary)
after token 9: move heap 0 → 2
after token 13: summary σ = 7, difference from the previous summary 6
after token 17: move heap 1 → 3

Counting the work

One decision on 3 heaps takes 2N + 2 = 8 updates: N scan rows, a separator, the same N rows again, a separator (plus one reset at the start of a game). The board is supplied twice; the controller does not store it.
Memory: accumulator, previous summary, stored summary, counter, candidate and fallback registers: 4 + 5B + 3r bits with N < 2^r; here B = 3, r = 2, so 25 bits.
Each single update is a shallow circuit (replay controller: Boolean depth ≤ 8, ≤ 18 threshold layers). The number of sequential updates grows with N. That no shallow family computes the complete board-to-move map is a separate statement, conditional on the named classical input that parity is not in AC⁰.

All 17 updates as a table

#	Token	Registers after	Output
1	RESET	scan, acc 0, prev 0*, idx 0, cand no move, fb no move
2	row 3	scan, acc 3, prev 0*, idx 0, cand no move, fb no move
3	row 4	scan, acc 7, prev 0*, idx 0, cand no move, fb no move
4	row 6	scan, acc 1, prev 0*, idx 0, cand no move, fb no move
5	SEP	replay, acc 0, prev 1, idx 0, cand no move, fb no move	σ = 1
6	row 3	replay, acc 0, prev 1, idx 1, cand heap 0 → 2, fb heap 0 → 2
7	row 4	replay, acc 0, prev 1, idx 2, cand heap 0 → 2, fb heap 0 → 2
8	row 6	replay, acc 0, prev 1, idx 3, cand heap 0 → 2, fb heap 0 → 2
9	SEP	scan, acc 0, prev 1, idx 0, cand no move, fb no move	move heap 0 → 2
10	row 2	scan, acc 2, prev 1, idx 0, cand no move, fb no move
11	row 4	scan, acc 6, prev 1, idx 0, cand no move, fb no move
12	row 1	scan, acc 7, prev 1, idx 0, cand no move, fb no move
13	SEP	replay, acc 0, prev 7, idx 0, cand no move, fb no move	σ = 7, diff 6
14	row 2	replay, acc 0, prev 7, idx 1, cand no move, fb heap 0 → 1
15	row 4	replay, acc 0, prev 7, idx 2, cand heap 1 → 3, fb heap 0 → 1
16	row 1	replay, acc 0, prev 7, idx 3, cand heap 1 → 3, fb heap 0 → 1
17	SEP	scan, acc 0, prev 7, idx 0, cand no move, fb no move	move heap 1 → 3

* no previous summary yet (validity bit 0).

Game: (3, 4, 6) —your move (δ = 1)→ (2, 4, 6) —opponent (δ = 7)→ (2, 4, 1)

Only the boards at your decision times

Position fed	summary σ	difference
(3, 4, 6)	1	—
(2, 4, 1)	7	6

The difference 6 = 1 ⊕ 7 spans two moves: yours and the opponent’s.

Including your own post-move board

Position fed	summary σ	difference
(3, 4, 6)	1	—
(2, 4, 6)	0	1
(2, 4, 1)	7	7

Now the last difference is 7, the opponent’s move alone, because your post-move board (2, 4, 6) is the preceding frame.

Computed with the replay controller; feeding your post-move board costs another 2N + 2 updates, and the move it then outputs is discarded.

How this relates to the Lean proof. Each update is one step of Controller.cstep (replay) or BoardStore.bsStep (board storage) on the token streams Controller.dtoks and BoardStore.btoks. The whole-game theorems WholeGame.replay_wins and BoardStore.bits_store_wins prove that, from every board with nonzero nim-sum, iterating these updates wins against every legal opponent. The summary mechanism is Recurrent.step. The comparison of decision-time boards with the post-move board is Bypass.diff_with_postMove and Bypass.diff_decision_only.

What this does not show. Each single update is shallow; the number of updates per decision ( $2N+2$ , or $N+1$ with board storage) grows with the board. That no shallow family computes the complete board-to-move map is a separate statement, conditional on the named classical input that parity is not in $\mathrm{AC}^0$ . The edge cases (an extra separator, a reset) lie outside the protocol streams that the theorems quantify over; the update rule is simply applied. The recurrent strategies are proved in their own stateful game semantics; connecting them to the later history model of weak mastery is a separate adapter that has not been built (coverage record). No recurrent network was trained.

Depicted in Lean: Controller.cstep, Controller.dtoks, Recurrent.replayStep, Recurrent.step, Recurrent.sep_resets, ControllerBits.bstep_reset, BoardStore.bsStep, BoardStore.btoks, Controller.crun_decision, Controller.stream_fits, WholeGame.replay_wins, BoardStore.bits_store_wins, Bypass.diff_with_postMove, Bypass.diff_decision_only, Recurrent.circuit_resources, BoardStore.bsForms_res, BoardStore.bsOuts_res, BoardStore.bs_net.

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 566 reference cases. The comparison compares every register and output after every token.

3 How this is formalised

ControllerBits.step_refines and ControllerBits.brun_refines: the bit-level update (one formula per state and output bit, depth at most 8) tracks the semantic controller exactly, step by step and over whole runs, on states whose registers fit.
ControllerBits.bstep_reset: a reset token restores the initial encoding from any bit state whatsoever.
Controller.stream_fits: along well-formed streams every visited state fits its fields.
Family.ctrl_ac0: the update formulas form an AC⁰ family of depth at most 8.

Coverage record
Paper anchor	`par-the-recurrent-update-p1` (website anchor; the manuscript has no label here)
Displayed as	Appendix C, “The recurrent update”
Claim	Scan and replay updates are shallow; bit-level refinement and register bounds hold on well-formed streams
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 1510–1511; SHA-256 of the normalised block source `9ef288e7140f8527…`
Lean declarations	`NimAudit.ControllerBits.step_refines` (ControllerBits, lines 555–561, file `4e23680da471…`) `NimAudit.ControllerBits.brun_refines` (ControllerBits, lines 649–656, file `4e23680da471…`) `NimAudit.ControllerBits.bstep_reset` (ControllerBits, lines 706–719, file `4e23680da471…`) `NimAudit.Controller.stream_fits` (Controller, lines 324–378, file `63d0e09c002d…`) `NimAudit.Family.ctrl_ac0` (Family, lines 475–479, file `7a647f0a667d…`)
Depends on	Section 5.5, “From a summary to a move”
Explanations	`explain/c-recurrent-update`, `formal/c-recurrent-update`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `ControllerBits.step_refines`

Module ControllerBits (lean/phase4/ControllerBits.lean, lines 555–561) · file SHA-256 4e23680da471fd69… Axioms reported by the fresh build: propext, Quot.sound

ONE-STEP REFINEMENT: on the canonical encoding of a state, one evaluation of the per-update circuits yields the canonical encoding of the semantic successor state and (after decoding the output wires) exactly the semantic output.

Statement as elaborated and printed by Lean 4.26.0

∀ {B r : ℕ} {s : NimAudit.Controller.CState} {t : NimAudit.Controller.Tok},
  NimAudit.ControllerBits.Decodable B r s t →
    NimAudit.ControllerBits.bstep B r (NimAudit.ControllerBits.sbits B r s) t =
      (NimAudit.ControllerBits.sbits B r (NimAudit.Controller.cstep s t).1,
        (NimAudit.Controller.cstep s t).2)

Exact source text, lines 555–561

555/-- ONE-STEP REFINEMENT: on the canonical encoding of a state, one evaluation of the556    per-update circuits yields the canonical encoding of the semantic successor state and557    (after decoding the output wires) exactly the semantic output. -/558theorem step_refines (hd : Decodable B r s t) :559    bstep B r (sbits B r s) t = (sbits B r (cstep s t).1, (cstep s t).2) := by560  show ((fun j => eval (enc B r s t) (nextC B r j)), decodeOut B r (enc B r s t)) = _561  rw [step_state hd, step_out hd]

Project declarations in the statement: Controller.COut, Controller.CState, Controller.Tok, Controller.cstep, ControllerBits.Decodable, ControllerBits.bstep, ControllerBits.sbits

Project declarations used by the proof or definition body

AC0.Circ.eval, Controller.COut, Controller.CState, Controller.Tok, Controller.cstep, ControllerBits.Decodable, ControllerBits.bstep, ControllerBits.decodeOut, ControllerBits.enc, ControllerBits.nextC, ControllerBits.sbits, ControllerBits.step_out, ControllerBits.step_state

theorem `ControllerBits.brun_refines`

Module ControllerBits (lean/phase4/ControllerBits.lean, lines 649–656) · file SHA-256 4e23680da471fd69… Axioms reported by the fresh build: propext, Quot.sound

RUN REFINEMENT: started on the canonical encoding of s, the bit-level machine tracks the semantic controller exactly along the whole token stream.

Statement as elaborated and printed by Lean 4.26.0

∀ {B r : ℕ} (s : NimAudit.Controller.CState) (ts : List NimAudit.Controller.Tok),
  NimAudit.ControllerBits.AllDec B r s ts →
    NimAudit.ControllerBits.brun B r (NimAudit.ControllerBits.sbits B r s) ts =
      (NimAudit.ControllerBits.sbits B r (NimAudit.Controller.crun s ts).1,
        (NimAudit.Controller.crun s ts).2)

Exact source text, lines 649–656

649/-- RUN REFINEMENT: started on the canonical encoding of s, the bit-level machine tracks650    the semantic controller exactly along the whole token stream. -/651theorem brun_refines {B r : Nat} : ∀ (s : CState) (ts : List Tok), AllDec B r s ts →652    brun B r (sbits B r s) ts = (sbits B r (crun s ts).1, (crun s ts).2)653  | s, [], _ => rfl654  | s, t :: ts, ⟨hd, hrest⟩ => by655    simp only [brun, crun]656    rw [step_refines hd, brun_refines _ ts hrest]

Project declarations in the statement: Controller.COut, Controller.CState, Controller.Tok, Controller.crun, ControllerBits.AllDec, ControllerBits.brun, ControllerBits.sbits

Project declarations used by the proof or definition body

Controller.COut, Controller.CState, Controller.Tok, Controller.crun, Controller.cstep, ControllerBits.AllDec, ControllerBits.Decodable, ControllerBits.brun, ControllerBits.bstep, ControllerBits.sbits, ControllerBits.step_refines

theorem `ControllerBits.bstep_reset`

Module ControllerBits (lean/phase4/ControllerBits.lean, lines 706–719) · file SHA-256 4e23680da471fd69… Axioms reported by the fresh build: propext, Quot.sound

RESET: from ANY state vector whatsoever (not necessarily a valid encoding), a reset token produces the all-zero encoding of the initial state and no output.

Statement as elaborated and printed by Lean 4.26.0

∀ (B r : ℕ) (v : ℕ → Bool),
  NimAudit.ControllerBits.bstep B r v NimAudit.Controller.Tok.reset =
    (NimAudit.ControllerBits.sbits B r NimAudit.Controller.cinit, none)

Exact source text, lines 706–719

706/-- RESET: from ANY state vector whatsoever (not necessarily a valid encoding), a reset707    token produces the all-zero encoding of the initial state and no output. -/708theorem bstep_reset (B r : Nat) (v : Nat → Bool) : bstep B r v Tok.reset = (sbits B r cinit, none) := by709  have h1 : (fun j => eval (inp B r v Tok.reset) (nextC B r j)) = sbits B r cinit := by710    funext j711    unfold nextC sbits712    rw [layout_map (eval (inp B r v Tok.reset))]713    apply layout_congr <;> intros <;>714      simp [modeN, accN, prevN, validN, sigN, idxN, selFN, selIN, selVN, fnzFN, fnzIN, fnzVN, Rc,715        inp_rst, tokRst, cinit, optI, optV]716  have h2 : decodeOut B r (inp B r v Tok.reset) = none := by717    simp [decodeOut, sumOutC, moveOutC, Ec, inp_row, inp_rst, tokRow, tokRst]718  show ((fun j => eval (inp B r v Tok.reset) (nextC B r j)), decodeOut B r (inp B r v Tok.reset)) = _719  rw [h1, h2]

Project declarations in the statement: Controller.COut, Controller.Tok.reset, Controller.cinit, ControllerBits.bstep, ControllerBits.sbits

Project declarations used by the proof or definition body

theorem `Controller.stream_fits`

Module Controller (lean/phase4/Controller.lean, lines 324–378) · file SHA-256 63d0e09c002db91e… Axioms reported by the fresh build: propext, Quot.sound

REACHABLE-STATE BOUNDS: along a well-formed stream of boards of N heaps below 2^B, started from an idle fitting state, EVERY visited state has acc, prev, sig < 2^B, counter ≤ N, and selected/fallback moves with index < N and value < 2^B. With N < 2^r, every register fits its r- or B-bit field; the counter never overflows.

Statement as elaborated and printed by Lean 4.26.0

∀ {B N : ℕ} (s : NimAudit.Controller.CState),
  NimAudit.Controller.Idle s →
    NimAudit.Controller.Fits B N s →
      ∀ (Ps : List (List ℕ)),
        (∀ P ∈ Ps, P.length = N ∧ NimAudit.Game.Width B P) →
          ∀ st ∈ NimAudit.Controller.crunStates s (NimAudit.Controller.stream Ps),
            NimAudit.Controller.Fits B N st

Exact source text, lines 324–378

324/-- REACHABLE-STATE BOUNDS: along a well-formed stream of boards of N heaps below 2^B,325    started from an idle fitting state, EVERY visited state has acc, prev, sig < 2^B,326    counter ≤ N, and selected/fallback moves with index < N and value < 2^B.  With327    N < 2^r, every register fits its r- or B-bit field; the counter never overflows. -/328theorem stream_fits {B N : Nat} (s : CState) (hs : Idle s) (hf : Fits B N s) (Ps : List (List Nat))329    (hP : ∀ P ∈ Ps, P.length = N ∧ Width B P) : ∀ st ∈ crunStates s (stream Ps), Fits B N st := by330  induction Ps generalizing s with331  | nil => intro st h; simp [stream, crunStates] at h; subst h; exact hf332  | cons P Ps ih =>333    have e : stream (P :: Ps) = dtoks P ++ stream Ps := by simp [stream]334    rw [e]335    intro st h336    obtain ⟨hlenP, hwP⟩ := hP P (by simp)337    rcases crunStates_append s _ _ st h with h1 | h1338    · -- inside the decision339      unfold dtoks at h1340      rcases crunStates_append s _ _ st h1 with h2 | h2341      · rcases crunStates_append s _ _ st h2 with h3 | h3342        · rcases crunStates_append s _ _ st h3 with h4 | h4343          · exact scan_rows_fit s hs.1 hf P hwP st h4344          · rw [crun_scan_rows s hs.1] at h4345            simp only [crunStates, cstep, Bool.false_eq_true, if_false, List.mem_cons,346              List.mem_singleton] at h4347            have ha : s.acc ^^^ nimSum P < 2 ^ B := Nat.xor_lt_two_pow hf.1 (nimSum_lt hwP)348            rcases h4 with rfl | rfl | h4349            · exact ⟨ha, hf.2.1, hf.2.2.1, hf.2.2.2.1, hf.2.2.2.2.1, hf.2.2.2.2.2⟩350            · exact ⟨Nat.two_pow_pos B, ha, ha, Nat.zero_le _, by simp, by simp⟩351            · simp at h4352        · rw [crun_append, crun_scan_rows s hs.1] at h3353          simp only [crun, cstep, Bool.false_eq_true, if_false] at h3354          have ha : s.acc ^^^ nimSum P < 2 ^ B := Nat.xor_lt_two_pow hf.1 (nimSum_lt hwP)355          exact replay_rows_fit _ rfl ⟨Nat.two_pow_pos B, ha, ha⟩ (by simp) (by simp) P356            (by simp [hlenP]) hwP st h3357      · rw [crun_append, crun_append, crun_scan_rows s hs.1] at h2358        simp only [crun, cstep, Bool.false_eq_true, if_false] at h2359        have ha : s.acc ^^^ nimSum P < 2 ^ B := Nat.xor_lt_two_pow hf.1 (nimSum_lt hwP)360        generalize hS1 : (⟨true, 0, s.acc ^^^ nimSum P, true, s.acc ^^^ nimSum P, 0, none, none⟩ :361          CState) = S1 at h2362        have hS1m : S1.replayMode = true := by rw [← hS1]363        simp only [crunStates, List.mem_cons, List.mem_singleton] at h2364        rcases h2 with rfl | rfl | h2365        · subst hS1366          exact replay_rows_fit _ rfl ⟨Nat.two_pow_pos B, ha, ha⟩ (by simp) (by simp) P367            (by simp [hlenP]) hwP _ (crun_mem_states _ _)368        · rw [crun_replay_rows _ hS1m]369          subst hS1370          simp only [cstep, if_true]371          exact ⟨Nat.two_pow_pos B, ha, ha, Nat.zero_le _, by simp, by simp⟩372        · simp at h2373    · rw [crun_decision s hs P] at h1374      have hidle : Idle (⟨false, 0, nimSum P, true, nimSum P, 0, none, none⟩ : CState) :=375        ⟨rfl, rfl, rfl, rfl, rfl⟩376      have hfit : Fits B N (⟨false, 0, nimSum P, true, nimSum P, 0, none, none⟩ : CState) :=377        ⟨Nat.two_pow_pos B, nimSum_lt hwP, nimSum_lt hwP, Nat.zero_le _, by simp, by simp⟩378      exact ih _ hidle hfit (fun Q hQ => hP Q (by simp [hQ])) st h1

Project declarations in the statement: Controller.CState, Controller.Fits, Controller.Idle, Controller.crunStates, Controller.stream, Game.Width

Project declarations used by the proof or definition body

theorem `Family.ctrl_ac0`

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

RECURRENT UPDATE: formula family certificate (depth ≤ 8, input = state + token, total size polynomial in that width, hence in B + log N).

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Family.AC0Fam NimAudit.Family.ctrlAdm NimAudit.Family.ctrlLen NimAudit.Family.ctrlF 8

Exact source text, lines 475–479

475/-- RECURRENT UPDATE: formula family certificate (depth ≤ 8, input = state + token,476    total size polynomial in that width, hence in B + log N). -/477theorem ctrl_ac0 : AC0Fam ctrlAdm ctrlLen ctrlF 8 := by478  refine ⟨ctrlLen_pos, fun i _ c hc => (ctrlForms_res _ _ c hc).1, fun i _ c hc => (ctrlForms_res _ _ c hc).2.2, ?_⟩479  exact polyIn_mono (fun i _ => ctrlForms_size _ _) (polyE ctrlLen_pos leafBr ctrl_leaves ctrlSzE _ (fun _ => rfl))

Project declarations in the statement: Family.AC0Fam, Family.ctrlAdm, Family.ctrlF, Family.ctrlLen

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.depth, AC0.Circ.maxInput, AC0.Circ.size, ControllerBits.cellSize, ControllerBits.stateWidth, Family.AC0Fam.mk, Family.ctrlAdm, Family.ctrlF, Family.ctrlLen, Family.ctrlLen_pos, Family.ctrlSzE, Family.ctrl_leaves, Family.leafBr, Family.polyE, Family.polyIn_mono, Family.tsize, ThresholdInst.ctrlForms_res, ThresholdInst.ctrlForms_size, ThresholdInst.inWidth, ThresholdInst.outCount, WholeGame.rIdx

Definitions these statements use

inductive `Controller.COut`

Module Controller (lean/phase4/Controller.lean, lines 44–46) · file SHA-256 63d0e09c002db91e…

Statement as elaborated and printed by Lean 4.26.0

Type

Exact source text, lines 44–46

44inductive COut where45  | summary (s : Nat) (diff : Option Nat)46  | move (m : Option (Nat × Nat))

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

inductive `Controller.CState`

Module Controller (lean/phase4/Controller.lean, lines 34–42) · file SHA-256 63d0e09c002db91e…

Statement as elaborated and printed by Lean 4.26.0

Type

Exact source text, lines 34–42

34structure CState where35  replayMode : Bool36  acc : Nat37  prev : Nat38  valid : Bool39  sig : Nat40  idx : Nat41  sel : Option (Nat × Nat)42  fnz : Option (Nat × Nat)

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

inductive `Controller.Tok`

Module Controller (lean/phase4/Controller.lean, lines 29–32) · file SHA-256 63d0e09c002db91e…

Statement as elaborated and printed by Lean 4.26.0

Type

Exact source text, lines 29–32

29inductive Tok where30  | row (x : Nat)31  | sep32  | reset

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Controller.cstep`

Module Controller (lean/phase4/Controller.lean, lines 50–64) · file SHA-256 63d0e09c002db91e…

One update of the controller.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Controller.CState →
  NimAudit.Controller.Tok → NimAudit.Controller.CState × Option NimAudit.Controller.COut

Exact source text, lines 50–64

50/-- One update of the controller. -/51def cstep (s : CState) : Tok → CState × Option COut52  | .reset => (cinit, none)53  | .row x =>54    if s.replayMode then55      (⟨s.replayMode, s.acc, s.prev, s.valid, s.sig, (replayStep s.sig ⟨s.idx, s.sel, s.fnz⟩ x).idx,56        (replayStep s.sig ⟨s.idx, s.sel, s.fnz⟩ x).sel, (replayStep s.sig ⟨s.idx, s.sel, s.fnz⟩ x).fnz⟩,57       none)58    else (⟨s.replayMode, s.acc ^^^ x, s.prev, s.valid, s.sig, s.idx, s.sel, s.fnz⟩, none)59  | .sep =>60    if s.replayMode then61      (⟨false, s.acc, s.prev, s.valid, s.sig, 0, none, none⟩, some (.move (firstSome s.sel s.fnz)))62    else63      (⟨true, 0, s.acc, true, s.acc, 0, none, none⟩,64       some (.summary s.acc (if s.valid then some (s.prev ^^^ s.acc) else none)))

Project declarations in the statement: Controller.COut, Controller.CState, Controller.Tok

Project declarations used by the proof or definition body

inductive `ControllerBits.Decodable`

Module ControllerBits (lean/phase4/ControllerBits.lean, lines 483–490) · file SHA-256 4e23680da471fd69…

Field-width hypotheses needed for one exact update.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → NimAudit.Controller.CState → NimAudit.Controller.Tok → Prop

Exact source text, lines 483–490

483/-- Field-width hypotheses needed for one exact update. -/484structure Decodable (B r : Nat) (s : CState) (t : Tok) : Prop where485  acc : s.acc < 2 ^ B486  prev : s.prev < 2 ^ B487  sig : s.sig < 2 ^ B488  sel : ∀ i v, s.sel = some (i, v) → i < 2 ^ r ∧ v < 2 ^ B489  fnz : ∀ i v, s.fnz = some (i, v) → i < 2 ^ r ∧ v < 2 ^ B490  tok : tokX t < 2 ^ B

Project declarations in the statement: Controller.CState, Controller.Tok

Project declarations used by the proof or definition body

Controller.CState, Controller.CState.acc, Controller.CState.fnz, Controller.CState.prev, Controller.CState.sel, Controller.CState.sig, Controller.Tok, ControllerBits.tokX

def `ControllerBits.bstep`

Module ControllerBits (lean/phase4/ControllerBits.lean, lines 478–481) · file SHA-256 4e23680da471fd69…

One update of the bit-level machine: evaluate the next-state circuits and the output circuits on (state vector, token).

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → (ℕ → Bool) → NimAudit.Controller.Tok → (ℕ → Bool) × Option NimAudit.Controller.COut

Exact source text, lines 478–481

478/-- One update of the bit-level machine: evaluate the next-state circuits and the output479    circuits on (state vector, token). -/480def bstep (B r : Nat) (v : Nat → Bool) (t : Tok) : (Nat → Bool) × Option COut :=481  (fun j => eval (inp B r v t) (nextC B r j), decodeOut B r (inp B r v t))

Project declarations in the statement: Controller.COut, Controller.Tok

Project declarations used by the proof or definition body

AC0.Circ.eval, Controller.COut, Controller.Tok, ControllerBits.decodeOut, ControllerBits.inp, ControllerBits.nextC

def `ControllerBits.sbits`

Module ControllerBits (lean/phase4/ControllerBits.lean, lines 104–108) · file SHA-256 4e23680da471fd69…

The canonical state vector (4 + 5B + 3r bits; false beyond).

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → NimAudit.Controller.CState → ℕ → Bool

Exact source text, lines 104–108

104/-- The canonical state vector (4 + 5B + 3r bits; false beyond). -/105def sbits (B r : Nat) (s : CState) : Nat → Bool :=106  layout B r false s.replayMode s.acc.testBit s.prev.testBit s.valid s.sig.testBit s.idx.testBit107    s.sel.isSome (optI s.sel).testBit (optV s.sel).testBit s.fnz.isSome (optI s.fnz).testBit108    (optV s.fnz).testBit

Project declarations in the statement: Controller.CState

Project declarations used by the proof or definition body

Controller.CState, Controller.CState.acc, Controller.CState.fnz, Controller.CState.idx, Controller.CState.prev, Controller.CState.replayMode, Controller.CState.sel, Controller.CState.sig, Controller.CState.valid, ControllerBits.layout, ControllerBits.optI, ControllerBits.optV

def `Controller.crun`

Module Controller (lean/phase4/Controller.lean, lines 66–68) · file SHA-256 63d0e09c002db91e…

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Controller.CState →
  List NimAudit.Controller.Tok → NimAudit.Controller.CState × List NimAudit.Controller.COut

Exact source text, lines 66–68

66def crun : CState → List Tok → CState × List COut67  | s, [] => (s, [])68  | s, t :: ts => ((crun (cstep s t).1 ts).1, (cstep s t).2.toList ++ (crun (cstep s t).1 ts).2)

Project declarations in the statement: Controller.COut, Controller.CState, Controller.Tok

Project declarations used by the proof or definition body

Controller.COut, Controller.CState, Controller.Tok, Controller.cstep

def `ControllerBits.AllDec`

Module ControllerBits (lean/phase4/ControllerBits.lean, lines 644–647) · file SHA-256 4e23680da471fd69…

Every visited (state, token) pair satisfies the one-step width hypotheses.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → NimAudit.Controller.CState → List NimAudit.Controller.Tok → Prop

Exact source text, lines 644–647

644/-- Every visited (state, token) pair satisfies the one-step width hypotheses. -/645def AllDec (B r : Nat) : CState → List Tok → Prop646  | _, [] => True647  | s, t :: ts => Decodable B r s t ∧ AllDec B r (cstep s t).1 ts

Project declarations in the statement: Controller.CState, Controller.Tok

Project declarations used by the proof or definition body

Controller.COut, Controller.CState, Controller.Tok, Controller.cstep, ControllerBits.Decodable

def `ControllerBits.brun`

Module ControllerBits (lean/phase4/ControllerBits.lean, lines 633–635) · file SHA-256 4e23680da471fd69…

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → (ℕ → Bool) → List NimAudit.Controller.Tok → (ℕ → Bool) × List NimAudit.Controller.COut

Exact source text, lines 633–635

633def brun (B r : Nat) : (Nat → Bool) → List Tok → (Nat → Bool) × List COut634  | v, [] => (v, [])635  | v, t :: ts => ((brun B r (bstep B r v t).1 ts).1, (bstep B r v t).2.toList ++ (brun B r (bstep B r v t).1 ts).2)

Project declarations in the statement: Controller.COut, Controller.Tok

Project declarations used by the proof or definition body

Controller.COut, Controller.Tok, ControllerBits.bstep

def `Controller.cinit`

Module Controller (lean/phase4/Controller.lean, lines 48–48) · file SHA-256 63d0e09c002db91e…

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Controller.CState

Exact source text, lines 48–48

48def cinit : CState := ⟨false, 0, 0, false, 0, 0, none, none⟩

Project declarations in the statement: Controller.CState

Project declarations used by the proof or definition body

Controller.CState.mk

def `Controller.Fits`

Module Controller (lean/phase4/Controller.lean, lines 237–241) · file SHA-256 63d0e09c002db91e…

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → NimAudit.Controller.CState → Prop

Exact source text, lines 237–241

237/-- Register bounds for N heaps of B bits and an r-bit counter (N < 2^r). -/238def Fits (B N : Nat) (s : CState) : Prop :=239  s.acc < 2 ^ B ∧ s.prev < 2 ^ B ∧ s.sig < 2 ^ B ∧ s.idx ≤ N ∧240  (∀ i v, s.sel = some (i, v) → i < N ∧ v < 2 ^ B) ∧241  (∀ i v, s.fnz = some (i, v) → i < N ∧ v < 2 ^ B)

Project declarations in the statement: Controller.CState

Project declarations used by the proof or definition body

Controller.CState, Controller.CState.acc, Controller.CState.fnz, Controller.CState.idx, Controller.CState.prev, Controller.CState.sel, Controller.CState.sig

def `Controller.Idle`

Module Controller (lean/phase4/Controller.lean, lines 83–84) · file SHA-256 63d0e09c002db91e…

Idle: scan mode with empty accumulator and cleared replay registers.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Controller.CState → Prop

Exact source text, lines 83–84

83/-- Idle: scan mode with empty accumulator and cleared replay registers. -/84def Idle (s : CState) : Prop := s.replayMode = false ∧ s.acc = 0 ∧ s.idx = 0 ∧ s.sel = none ∧ s.fnz = none

Project declarations in the statement: Controller.CState

Project declarations used by the proof or definition body

Controller.CState, Controller.CState.acc, Controller.CState.fnz, Controller.CState.idx, Controller.CState.replayMode, Controller.CState.sel

def `Controller.crunStates`

Module Controller (lean/phase4/Controller.lean, lines 70–73) · file SHA-256 63d0e09c002db91e…

All states visited (initial state included).

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Controller.CState → List NimAudit.Controller.Tok → List NimAudit.Controller.CState

Exact source text, lines 70–73

70/-- All states visited (initial state included). -/71def crunStates : CState → List Tok → List CState72  | s, [] => [s]73  | s, t :: ts => s :: crunStates (cstep s t).1 ts

Project declarations in the statement: Controller.CState, Controller.Tok

Project declarations used by the proof or definition body

Controller.COut, Controller.CState, Controller.Tok, Controller.cstep

def `Controller.stream`

Module Controller (lean/phase4/Controller.lean, lines 78–78) · file SHA-256 63d0e09c002db91e…

Statement as elaborated and printed by Lean 4.26.0

List (List ℕ) → List NimAudit.Controller.Tok

Exact source text, lines 78–78

78def stream (Ps : List (List Nat)) : List Tok := Ps.flatMap dtoks

Project declarations in the statement: Controller.Tok

Project declarations used by the proof or definition body

Controller.Tok, Controller.dtoks

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

inductive `Family.AC0Fam`

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

AC0 FAMILY CERTIFICATE (nonuniform, multi-output). For every admissible member: the input length is positive, every output formula has depth ≤ d and reads only the first len inputs, and the total size of the outputs is ≤ c·len^k with c, k independent of the member.

Statement as elaborated and printed by Lean 4.26.0

{ι : Type} → (ι → Prop) → (ι → ℕ) → (ι → List NimAudit.AC0.Circ) → ℕ → Prop

Exact source text, lines 126–134

126/-- AC0 FAMILY CERTIFICATE (nonuniform, multi-output).  For every admissible member:127    the input length is positive, every output formula has depth ≤ d and reads only128    the first len inputs, and the total size of the outputs is ≤ c·len^k with c, k129    independent of the member. -/130structure AC0Fam {ι : Type} (adm : ι → Prop) (len : ι → Nat) (outs : ι → List Circ) (d : Nat) : Prop where131  pos : ∀ i, adm i → 1 ≤ len i132  depth_le : ∀ i, adm i → ∀ c ∈ outs i, depth c ≤ d133  reads : ∀ i, adm i → ∀ c ∈ outs i, maxInput c ≤ len i134  size_poly : PolyIn adm len (fun i => tsize (outs i))

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.depth, AC0.Circ.maxInput, Family.PolyIn, Family.tsize

def `Family.ctrlAdm`

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

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → Prop

Exact source text, lines 445–445

445def ctrlAdm : Nat × Nat → Prop := restAdm

Project declarations in the statement: none

Project declarations used by the proof or definition body

Family.restAdm

def `Family.ctrlF`

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

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → List NimAudit.AC0.Circ

Exact source text, lines 448–448

448def ctrlF (i : Nat × Nat) : List Circ := ctrlForms i.1 (rIdx i.2)

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

ThresholdInst.ctrlForms, WholeGame.rIdx

def `Family.ctrlLen`

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

Per-update input: state (4 + 5B + 3r bits) plus one token (2 + B bits), r = log₂N + 1.

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → ℕ

Exact source text, lines 446–447

446/-- Per-update input: state (4 + 5B + 3r bits) plus one token (2 + B bits), r = log₂N + 1. -/447def ctrlLen : Nat × Nat → Nat := fun i => inWidth i.1 (rIdx i.2)

Project declarations in the statement: none

Project declarations used by the proof or definition body

ThresholdInst.inWidth, WholeGame.rIdx

Full modules

Module	File	Lines	Imports
Controller	`lean/phase4/Controller.lean`	401	NimRecurrent, AttainCircuit
ControllerBits	`lean/phase4/ControllerBits.lean`	1148	Controller, NimCorrBridge
Family	`lean/phase6/Family.lean`	574	WholeGame
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).

Appendix C, “The recurrent update”Scan and replay updates are shallow; bit-level refinement and register bounds hold on well-formed streams

1 Paper text

2 Explain this

Row-wise recurrence: registers, separators and replay

Registers after this update

Outputs so far

Counting the work

Only the boards at your decision times

Including your own post-move board

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem ControllerBits.step_refines

theorem ControllerBits.brun_refines

theorem ControllerBits.bstep_reset

theorem Controller.stream_fits

theorem Family.ctrl_ac0

Definitions these statements use

inductive Controller.COut

inductive Controller.CState

inductive Controller.Tok

def Controller.cstep

inductive ControllerBits.Decodable

def ControllerBits.bstep

def ControllerBits.sbits

def Controller.crun

def ControllerBits.AllDec

def ControllerBits.brun

def Controller.cinit

def Controller.Fits

def Controller.Idle

def Controller.crunStates

def Controller.stream

def Game.Width

inductive Family.AC0Fam

def Family.ctrlAdm

def Family.ctrlF

def Family.ctrlLen

Full modules

theorem `ControllerBits.step_refines`

theorem `ControllerBits.brun_refines`

theorem `ControllerBits.bstep_reset`

theorem `Controller.stream_fits`

theorem `Family.ctrl_ac0`

inductive `Controller.COut`

inductive `Controller.CState`

inductive `Controller.Tok`

def `Controller.cstep`

inductive `ControllerBits.Decodable`

def `ControllerBits.bstep`

def `ControllerBits.sbits`

def `Controller.crun`

def `ControllerBits.AllDec`

def `ControllerBits.brun`

def `Controller.cinit`

def `Controller.Fits`

def `Controller.Idle`

def `Controller.crunStates`

def `Controller.stream`

def `Game.Width`

inductive `Family.AC0Fam`

def `Family.ctrlAdm`

def `Family.ctrlF`

def `Family.ctrlLen`