Theorem 5.12 (ii)B structured heads and an AC⁰ readout select an optimal move with O(BN2^B) rollout steps

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

1 Paper text

Theorem 5.12 (Restricted bound and bypasses) The following statements hold under Definition 5.7.

(i) For each fixed $B\ge2$ , let $P$ be uniform on $\{0,\ldots,2^B-1\}^N$ conditional on $\sigma(P)\ne0$ . For one fixed structured head $\pi_j$ and an $\AC^0$ readout $F_N(P,\mathrm{RO}_{\pi_j}(P))$ , winning-move success is at most $\frac{2}{2^B-1}+\operatorname{negl}(N).$ Here $N\ge1$ , and a negligible error is a nonnegative sequence smaller than every inverse polynomial for sufficiently large $N$ , with circuit depth, polynomial size exponent and $B$ fixed. More precisely, a uniform parity-correlation bound $\eta_N$ for the fixed-bit readout indicators gives the finite upper bound $2/(2^B-1)+(2^B-1)\eta_N$ ; the indicators and correlation premise are specified in Appendix H. The leading constant is asymptotically attainable by guessing one nonzero nim-sum in each channel fibre.
(ii) For any $B$ , the $B$ structured heads and an $\AC^0$ readout select an optimal move using $O(BN2^B)$ rollout steps, as in Proposition 5.9.
(iii) Given a legal transition from a known zero-nim-sum predecessor, a two-frame $\AC^0$ selector restores zero. Once a player has established that invariant, it maintains it against every legal opponent response. This statement does not supply the initial winning move from an arbitrary position.

Generated from paper_jmlr.tex, lines 802–814.

2 Explain this

With all $B$ structured heads, the rollout outcomes reconstruct the nim-sum exactly and a shallow readout plays an optimal move. The cost is the rollouts themselves: $O(BN2^B)$ simulated moves per decision.

Multi-head rollouts and the outer controller, tick by tick

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

Policy $\pi_j$ subtracts $2^j$ from the first heap of size at least $2^j$ , and otherwise subtracts 1 from the first nonzero heap. A rollout lets both simulated players follow $\pi_j$ until no move is left; its outcome bit is the parity of the number of moves. Step through the outer controller one tick at a time: it resets, runs head 0's rollout move by move on a working copy of the board, records the outcome when the rollout ends, reloads the original board for the next head, and, in the all-head schedule, finally reads out a move. Every outcome bit here is produced by actually running the rollout; nothing is supplied from outside. The early-exit schedule (Figure 3) stops at the first outcome 1 and only classifies the position.

35 component evaluations (34 controller ticks and one readout). Colours: reset move terminal test store and reload store and stop readout.

tick 1: reset
tick 2: move, head 0
tick 3: move, head 0
tick 4: move, head 0
tick 5: move, head 0
tick 6: move, head 0
tick 7: move, head 0
tick 8: move, head 0
tick 9: move, head 0
tick 10: move, head 0
tick 11: move, head 0
tick 12: move, head 0
tick 13: move, head 0
tick 14: move, head 0
tick 15: terminal test, head 0
tick 16: store outcome and reload, head 0
tick 17: move, head 1
tick 18: move, head 1
tick 19: move, head 1
tick 20: move, head 1
tick 21: move, head 1
tick 22: move, head 1
tick 23: move, head 1
tick 24: terminal test, head 1
tick 25: store outcome and reload, head 1
tick 26: move, head 2
tick 27: move, head 2
tick 28: move, head 2
tick 29: move, head 2
tick 30: move, head 2
tick 31: move, head 2
tick 32: move, head 2
tick 33: terminal test, head 2
tick 34: store outcome and stop, head 2
readout

35 / 35 Readout: one evaluation of the readout circuit on the original board and the 3 stored outcome bits.

Working board (0, 0, 0)

Original board (read-only input) (3, 4, 6)

head j: 2
parity of moves: 1
rollout finished: 1
running: 0
some outcome 1: 1
stored outcomes: o₀ = 1 o₁ = 1 o₂ = 1

Readout

σ₀ = o₀ = 1; σ₁ = o₁ ⊕ o₀ = 0; σ₂ = o₂ ⊕ o₀ = 0, so σ = 1. The readout tests every heap in parallel and takes the first that decreases:

heap 0: 3 ⊕ 1 = 2 smaller
heap 1: 4 ⊕ 1 = 5 not smaller
heap 2: 6 ⊕ 1 = 7 not smaller

Move: set heap 0 to 2 → (2, 4, 6), nim-sum 0.

Counting the work

Simulated moves M = 13 + 7 + 7 = 27 (3 heads run).
Evaluations M + 2B + 2 = 27 + 6 + 2 = 35: 27 move updates, 3 terminal tests, 3 outcome updates, 1 reset, 1 readout.
Bound on M: BN(2^B − 1) = 63.
Each single evaluation is a shallow circuit: one policy step has Boolean depth ≤ 17 (≤ 36 threshold layers), the readout ≤ 19 (≤ 40), one controller tick ≤ 34 (≤ 70). Those bounds are per evaluation; the number of evaluations 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 AC⁰.

All 34 controller ticks as a table

Tick	Kind	Working board	j	parity	o₀…	What happens
1	reset	(3, 4, 6)	0	0	000	Reset: load the board, select head 0, clear the outcomes.
2	move	(2, 4, 6)	0	1	000	Head 0 moves: heap 0 from 3 to 2 (subtract 1 from the first heap of size at least 1).
3	move	(1, 4, 6)	0	0	000	Head 0 moves: heap 0 from 2 to 1 (subtract 1 from the first heap of size at least 1).
4	move	(0, 4, 6)	0	1	000	Head 0 moves: heap 0 from 1 to 0 (subtract 1 from the first heap of size at least 1).
5	move	(0, 3, 6)	0	0	000	Head 0 moves: heap 1 from 4 to 3 (subtract 1 from the first heap of size at least 1).
6	move	(0, 2, 6)	0	1	000	Head 0 moves: heap 1 from 3 to 2 (subtract 1 from the first heap of size at least 1).
7	move	(0, 1, 6)	0	0	000	Head 0 moves: heap 1 from 2 to 1 (subtract 1 from the first heap of size at least 1).
8	move	(0, 0, 6)	0	1	000	Head 0 moves: heap 1 from 1 to 0 (subtract 1 from the first heap of size at least 1).
9	move	(0, 0, 5)	0	0	000	Head 0 moves: heap 2 from 6 to 5 (subtract 1 from the first heap of size at least 1).
10	move	(0, 0, 4)	0	1	000	Head 0 moves: heap 2 from 5 to 4 (subtract 1 from the first heap of size at least 1).
11	move	(0, 0, 3)	0	0	000	Head 0 moves: heap 2 from 4 to 3 (subtract 1 from the first heap of size at least 1).
12	move	(0, 0, 2)	0	1	000	Head 0 moves: heap 2 from 3 to 2 (subtract 1 from the first heap of size at least 1).
13	move	(0, 0, 1)	0	0	000	Head 0 moves: heap 2 from 2 to 1 (subtract 1 from the first heap of size at least 1).
14	move	(0, 0, 0)	0	1	000	Head 0 moves: heap 2 from 1 to 0 (subtract 1 from the first heap of size at least 1).
15	terminal test	(0, 0, 0)	0	1	000	Head 0: no legal move, so the rollout has ended after an odd number of moves; the outcome bit is 1.
16	store outcome and reload	(3, 4, 6)	1	0	100	Store outcome o0 = 1, reload the original board and select head 1.
17	move	(1, 4, 6)	1	1	100	Head 1 moves: heap 0 from 3 to 1 (subtract 2 from the first heap of size at least 2).
18	move	(1, 2, 6)	1	0	100	Head 1 moves: heap 1 from 4 to 2 (subtract 2 from the first heap of size at least 2).
19	move	(1, 0, 6)	1	1	100	Head 1 moves: heap 1 from 2 to 0 (subtract 2 from the first heap of size at least 2).
20	move	(1, 0, 4)	1	0	100	Head 1 moves: heap 2 from 6 to 4 (subtract 2 from the first heap of size at least 2).
21	move	(1, 0, 2)	1	1	100	Head 1 moves: heap 2 from 4 to 2 (subtract 2 from the first heap of size at least 2).
22	move	(1, 0, 0)	1	0	100	Head 1 moves: heap 2 from 2 to 0 (subtract 2 from the first heap of size at least 2).
23	move	(0, 0, 0)	1	1	100	Head 1 moves: heap 0 from 1 to 0 (no heap has 2 or more: subtract 1 from the first nonzero heap).
24	terminal test	(0, 0, 0)	1	1	100	Head 1: no legal move, so the rollout has ended after an odd number of moves; the outcome bit is 1.
25	store outcome and reload	(3, 4, 6)	2	0	110	Store outcome o1 = 1, reload the original board and select head 2.
26	move	(3, 0, 6)	2	1	110	Head 2 moves: heap 1 from 4 to 0 (subtract 4 from the first heap of size at least 4).
27	move	(3, 0, 2)	2	0	110	Head 2 moves: heap 2 from 6 to 2 (subtract 4 from the first heap of size at least 4).
28	move	(2, 0, 2)	2	1	110	Head 2 moves: heap 0 from 3 to 2 (no heap has 4 or more: subtract 1 from the first nonzero heap).
29	move	(1, 0, 2)	2	0	110	Head 2 moves: heap 0 from 2 to 1 (no heap has 4 or more: subtract 1 from the first nonzero heap).
30	move	(0, 0, 2)	2	1	110	Head 2 moves: heap 0 from 1 to 0 (no heap has 4 or more: subtract 1 from the first nonzero heap).
31	move	(0, 0, 1)	2	0	110	Head 2 moves: heap 2 from 2 to 1 (no heap has 4 or more: subtract 1 from the first nonzero heap).
32	move	(0, 0, 0)	2	1	110	Head 2 moves: heap 2 from 1 to 0 (no heap has 4 or more: subtract 1 from the first nonzero heap).
33	terminal test	(0, 0, 0)	2	1	110	Head 2: no legal move, so the rollout has ended after an odd number of moves; the outcome bit is 1.
34	store outcome and stop	(0, 0, 0)	2	1	111	Store outcome o2 = 1 and stop (last head).

How this relates to the Lean proof. Each tick is one step of Shootout.ostep, with the policy step SelectCircuit.policyIdx inside the rollout registers RolloutExec.rsStep. Rollout.run_parity identifies the outcome bits with $\sigma_0$ and $\sigma_j\oplus\sigma_0$ , and Shootout.ah_counts proves that the all-head schedule takes $M+2B+1$ controller ticks, the reset included; with the single readout this gives $M+2B+2$ evaluations. The browser re-implements these steps; the agreement is checked against Lean's own evaluation of them.

What this does not show. Simulated moves and circuit evaluations are different counts: the $M$ moves are part of the $M+2B+2$ evaluations. The depth bounds (17 per policy step, 19 for the readout, 34 per controller tick) apply to one evaluation each. The complete board-to-move computation repeats them a number of times that grows with the board. That no shallow family computes the complete map is a separate statement (Proposition 5.14 and the text after it), conditional on the named classical input that parity is not in $\mathrm{AC}^0$ .

Depicted in Lean: SelectCircuit.policyIdx, RolloutExec.rsStep, Shootout.ostep, Shootout.initOS, Shootout.query_step, Rollout.run_parity, Game.recoverBit, Game.reconstruct_eq, Shootout.ahMove_eq, Shootout.ah_counts, Shootout.ahL_counts, Shootout.ee_spec, Shootout.ee_counts. Explains the paper’s Figure 3.

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 313 reference cases.

3 How this is formalised

Game.agent_wins and RolloutExec.mhExec_wins (winning against every legal opponent from every nonzero position, the second with fully executed rollouts) and Game.totalRolloutMoves_le (at most $BN(2^B-1)$ simulated moves). Details in Proposition 5.9.

Coverage record
Paper anchor	`thm:search-gap` (manuscript label)
Displayed as	Theorem 5.12 (ii)
Claim	B structured heads and an AC⁰ readout select an optimal move with O(BN2^B) rollout steps
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 802–814; SHA-256 of the normalised block source `6a8c9a4107356a14…`
Lean declarations	`NimAudit.Game.agent_wins` (NimGame, lines 376–388, file `23df6bb87ecf…`) `NimAudit.RolloutExec.mhExec_wins` (RolloutExec, lines 517–520, file `c7b63a6e02d1…`) `NimAudit.Game.totalRolloutMoves_le` (NimGame, lines 454–467, file `23df6bb87ecf…`)
Depends on	Proposition 5.9
Audited correspondence rows	`thm:search-gap`
Explanations	`explain/thm:search-gap.ii`, `formal/thm:search-gap.ii`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `Game.agent_wins`

Module NimGame (lean/phase2/NimGame.lean, lines 376–388) · file SHA-256 23df6bb87ecfd344… Axioms reported by the fresh build: propext, Quot.sound

END-TO-END STRATEGY GUARANTEE (Target 1C): on B-bit boards, the agent that queries the B structured rollouts, reconstructs the nim-sum and plays the selected move wins from every nonzero-nim-sum position against every legal opponent.

Statement as elaborated and printed by Lean 4.26.0

∀ {B : ℕ} (p : List ℕ),
  NimAudit.Game.Width B p → NimAudit.nimSum p ≠ 0 → NimAudit.Game.Wins (NimAudit.Game.agent B) p

Exact source text, lines 376–388

376/-- END-TO-END STRATEGY GUARANTEE (Target 1C): on B-bit boards, the agent that377    queries the B structured rollouts, reconstructs the nim-sum and plays the378    selected move wins from every nonzero-nim-sum position against every legal379    opponent. -/380theorem agent_wins {B : Nat} (p : List Nat) (hw : Width B p) (h : nimSum p ≠ 0) :381    Wins (agent B) p := by382  obtain ⟨q, hsel, hm, hq⟩ := selectMove_zero h383  refine Wins.intro p q (by rw [agent_eq hw]; exact hsel) hm ?_384  intro r hr385  have h1 := move_sum_lt hm386  have h2 := move_sum_lt hr387  exact agent_wins r (width_move (width_move hw hm) hr) (move_from_zero hr hq)388termination_by p.sum

Project declarations in the statement: Game.Width, Game.Wins, Game.agent, nimSum

Project declarations used by the proof or definition body

Game.Move, Game.Width, Game.Wins, Game.Wins.intro, Game.agent, Game.agent_eq, Game.move_from_zero, Game.move_sum_lt, Game.selectMove, Game.selectMove_zero, Game.width_move, nimSum

theorem `RolloutExec.mhExec_wins`

Module RolloutExec (lean/phase6/RolloutExec.lean, lines 517–520) · file SHA-256 c7b63a6e02d1d425… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

WHOLE-GAME THEOREM FOR THE FULLY EXECUTED MULTI-HEAD PLAYER: from every nonzero board of width B it wins against every legal opponent; no outcome bit is supplied for free.

Statement as elaborated and printed by Lean 4.26.0

∀ {B : ℕ} {P : List ℕ},
  NimAudit.Game.Width B P →
    NimAudit.nimSum P ≠ 0 → NimAudit.Game.Wins (NimAudit.RolloutExec.mhExecSel B) P

Exact source text, lines 517–520

517/-- WHOLE-GAME THEOREM FOR THE FULLY EXECUTED MULTI-HEAD PLAYER: from every nonzero board518    of width B it wins against every legal opponent; no outcome bit is supplied for free. -/519theorem mhExec_wins {B : Nat} {P : List Nat} (hw : Width B P) (h : nimSum P ≠ 0) : Wins (mhExecSel B) P :=520  wins_congr (fun Q hQ => mhExecSel_eq hQ) hw (ctrl_wins P h)

Project declarations in the statement: Game.Width, Game.Wins, RolloutExec.mhExecSel, nimSum

Project declarations used by the proof or definition body

Controller.ctrlSel, Controller.ctrl_wins, Game.Width, RolloutExec.mhExecSel, RolloutExec.mhExecSel_eq, WholeGame.wins_congr, nimSum

theorem `Game.totalRolloutMoves_le`

Module NimGame (lean/phase2/NimGame.lean, lines 454–467) · file SHA-256 23df6bb87ecfd344… Axioms reported by the fresh build: propext, Quot.sound

Statement as elaborated and printed by Lean 4.26.0

∀ {B : ℕ} {p : List ℕ},
  NimAudit.Game.Width B p → NimAudit.Game.totalRolloutMoves B p ≤ B * (p.length * (2 ^ B - 1))

Exact source text, lines 454–467

454theorem totalRolloutMoves_le {B : Nat} {p : List Nat} (hw : Width B p) :455    totalRolloutMoves B p ≤ B * (p.length * (2 ^ B - 1)) := by456  unfold totalRolloutMoves457  have key : ∀ k, ((List.range k).map (fun j => rolloutMoves j p)).sum ≤458      k * (p.length * (2 ^ B - 1)) := by459    intro k460    induction k with461    | zero => simp462    | succ k ih =>463      rw [List.range_succ, List.map_append, List.sum_append_nat, Nat.succ_mul]464      simp only [List.map_cons, List.map_nil, List.sum_cons, List.sum_nil, Nat.add_zero]465      have := rolloutMoves_le (j := k) hw466      omega467  exact key B

Project declarations in the statement: Game.Width, Game.totalRolloutMoves

Project declarations used by the proof or definition body

Game.Width, Game.rolloutMoves_le, Game.totalRolloutMoves, Rollout.rolloutMoves

Definitions these statements use

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

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

`Wins sel p`: the player to move at `p`, always playing the successor chosen by `sel`, wins against EVERY legal opponent. The selected move is legal, and after every legal opponent reply the player is again in a `Wins` position. Because the predicate is inductive, every such play is finite and ends with the opponent facing a terminal board (normal play: the opponent loses).

Statement as elaborated and printed by Lean 4.26.0

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

Exact source text, lines 125–132

125/-- `Wins sel p`: the player to move at `p`, always playing the successor chosen by126    `sel`, wins against EVERY legal opponent.  The selected move is legal, and after127    every legal opponent reply the player is again in a `Wins` position.  Because128    the predicate is inductive, every such play is finite and ends with the129    opponent facing a terminal board (normal play: the opponent loses). -/130inductive Wins (sel : List Nat → Option (List Nat)) : List Nat → Prop131  | intro (p q : List Nat) : sel p = some q → Move p q →132      (∀ r, Move q r → Wins sel r) → Wins sel p

Project declarations in the statement: none

Project declarations used by the proof or definition body

Game.Move

def `Game.agent`

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

The agent: reconstruct the nim-sum from the B root rollouts, then select.

Statement as elaborated and printed by Lean 4.26.0

ℕ → List ℕ → Option (List ℕ)

Exact source text, lines 257–259

257/-- The agent: reconstruct the nim-sum from the B root rollouts, then select. -/258def agent (B : Nat) (p : List Nat) : Option (List Nat) :=259  selectMove (reconstruct B (outcomes p)) p

Project declarations in the statement: none

Project declarations used by the proof or definition body

Game.outcomes, Game.reconstruct, Game.selectMove

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

Module RolloutExec (lean/phase6/RolloutExec.lean, lines 501–501) · file SHA-256 c7b63a6e02d1d425…

Statement as elaborated and printed by Lean 4.26.0

ℕ → List ℕ → Option (List ℕ)

Exact source text, lines 501–501

501def mhExecSel (B : Nat) (P : List Nat) : Option (List Nat) := applyM P (mhExec B P)

Project declarations in the statement: none

Project declarations used by the proof or definition body

RolloutExec.mhExec, SelectCircuit.applyM

def `Game.totalRolloutMoves`

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

Total simulated moves of the B root rollouts.

Statement as elaborated and printed by Lean 4.26.0

ℕ → List ℕ → ℕ

Exact source text, lines 450–452

450/-- Total simulated moves of the B root rollouts. -/451def totalRolloutMoves (B : Nat) (p : List Nat) : Nat :=452  ((List.range B).map (fun j => rolloutMoves j p)).sum

Project declarations in the statement: none

Project declarations used by the proof or definition body

Rollout.rolloutMoves

Full modules

Module	File	Lines	Imports
NimCore	`lean/NimCore.lean`	139	`Std`
NimGame	`lean/phase2/NimGame.lean`	634	NimRollout
RolloutExec	`lean/phase6/RolloutExec.lean`	896	Barrier

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

Theorem 5.12 (ii)B structured heads and an AC0 readout select an optimal move with O(BN2^B) rollout steps

1 Paper text

2 Explain this

Multi-head rollouts and the outer controller, tick by tick

Readout

Counting the work

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem Game.agent_wins

theorem RolloutExec.mhExec_wins

theorem Game.totalRolloutMoves_le

Definitions these statements use

def Game.Width

inductive Game.Wins

def Game.agent

def nimSum

def RolloutExec.mhExecSel

def Game.totalRolloutMoves

Full modules

Theorem 5.12 (ii)B structured heads and an AC⁰ readout select an optimal move with O(BN2^B) rollout steps

theorem `Game.agent_wins`

theorem `RolloutExec.mhExec_wins`

theorem `Game.totalRolloutMoves_le`

def `Game.Width`

inductive `Game.Wins`

def `Game.agent`

def `nimSum`

def `RolloutExec.mhExecSel`

def `Game.totalRolloutMoves`