Proposition 5.9B structured rollout heads recover all nim-sum bits; an AC⁰ readout then plays a winning move

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

1 Paper text

Proposition 5.9 (Structured rollout sufficiency) The $B$ structured rollout policies below, followed by an $\AC^0$ move selector, achieve strong mastery of NIM on $N$ heaps of bit-width $B$ . They use $B$ root rollouts and $O(BN2^B)$ simulated game moves per decision. Each policy update and the final readout have polynomial circuit size in $NB$ . For $B=O(\log N)$ the resulting bit work is polynomial in $N$ .

Generated from paper_jmlr.tex, lines 731–734.

2 Explain this

The policies. For each bit position $j$ , policy $\pi_j$ repeatedly subtracts $2^j$ from the leftmost heap of size at least $2^j$ ; once all heaps are smaller than $2^j$ it subtracts $1$ from the leftmost nonzero heap.

Why the outcome reveals a bit. The rollout length is $\sum_i\lfloor h_i/2^j\rfloor + \sum_i (h_i \bmod 2^j)$ . Its parity is $\sigma_j\oplus\sigma_0$ for $j\ge1$ (and $\sigma_0$ for $j=0$ ). The first player wins exactly when the length is odd.

Example. $P=(3,5)$ , $\sigma=3\oplus5=6=110_2$ . $\pi_0$ plays $3+5=8$ moves: even, outcome $0=\sigma_0$ . $\pi_1$ plays $\lfloor3/2\rfloor+\lfloor5/2\rfloor=3$ moves of size $2$ , then $1+1=2$ moves of size $1$ : $5$ moves, outcome $1=\sigma_1\oplus\sigma_0$ . $\pi_2$ plays $0+1$ moves of size $4$ and $3+1$ moves of size $1$ : $5$ moves, outcome $1=\sigma_2\oplus\sigma_0$ . So $\sigma=110_2$ .

The move. With $\sigma\ne0$ , take the first heap with $h_i\oplus\sigma<h_i$ and replace it by $h_i\oplus\sigma$ .

Costs. $B$ rollouts, at most $BN(2^B-1)$ simulated moves in total. That is polynomial in $N$ only when $B=O(\log N)$ .

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

Rollout.run_length: every complete run of $\pi_j$ , under any tie-breaking rule, has exactly the length above.
Game.rolloutWinner_channel: the executed outcome is $\sigma_0$ or $\sigma_j\oplus\sigma_0$ .
Game.agent_wins: the agent that runs the $B$ rollouts, reconstructs $\sigma$ (Game.reconstruct) and plays the selected move wins from every nonzero position against every legal opponent.
RolloutExec.mhExec_wins: the same for the fully executed version, in which each rollout runs on a finite register machine with one shallow step circuit per simulated move; no outcome bit is supplied for free.
RolloutExec.mhExec_evals: rollout $j$ makes $L_j+1$ policy evaluations; in total the number of simulated moves plus $B$ , at most $B(N(2^B-1)+1)$ .
Game.totalRolloutMoves_le: total simulated moves at most $BN(2^B-1)$ .
Mastery.mh_strong: the network-driven multi-head player is strongly masterful (in the sense of Definition 5.1) on $B$ -bit boards, for both roles.

The statement's "polynomial circuit size" for each policy update and the readout is certified separately (Appendix C, table).

Coverage record
Paper anchor	`prop:rollout-sufficiency` (manuscript label)
Displayed as	Proposition 5.9
Claim	B structured rollout heads recover all nim-sum bits; an AC⁰ readout then plays a winning move
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 731–734; SHA-256 of the normalised block source `4a1c0cfcc7992190…`
Lean declarations	`NimAudit.Game.rolloutWinner_channel` (NimGame, lines 171–176, file `23df6bb87ecf…`) `NimAudit.Game.agent_wins` (NimGame, lines 376–388, file `23df6bb87ecf…`) `NimAudit.RolloutExec.mhExec_wins` (RolloutExec, lines 517–520, file `c7b63a6e02d1…`) `NimAudit.RolloutExec.mhExec_evals` (RolloutExec, lines 522–547, file `c7b63a6e02d1…`) `NimAudit.Game.totalRolloutMoves_le` (NimGame, lines 454–467, file `23df6bb87ecf…`) `NimAudit.Rollout.run_length` (NimRollout, lines 88–94, file `1a99428d7157…`) `NimAudit.Mastery.mh_strong` (WeakMastery, lines 845–852, file `4c83e573f527…`)
Assumptions and domain	Heaps below $2^B$ ; the opponent may play any legal move; rollouts are executed move by move (no outcome bit is supplied for free).
Prose-to-formal notes	Lean proves the outcome identities for the executed rollout under every tie-breaking rule, the reconstruction, the winning guarantee against every legal opponent, and the bound $BN(2^B-1)$ on simulated moves. Circuit resources of each policy step and of the readout are in the records for Appendix C and Proposition 5.14.
Audited correspondence rows	`prop:rollout-sufficiency`, `app:rollout-proofs`
Explanations	`explain/prop:rollout-sufficiency`, `formal/prop:rollout-sufficiency`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `Game.rolloutWinner_channel`

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

RO_{pi_0}(P) = sigma_0 and RO_{pi_j}(P) = sigma_j XOR sigma_0 (j ≥ 1), proved for the executed rollout.

Statement as elaborated and printed by Lean 4.26.0

∀ (j : ℕ) (p : List ℕ), NimAudit.Game.rolloutWinner j p = NimAudit.channel j (NimAudit.nimSum p)

Exact source text, lines 171–176

171/-- RO_{pi_0}(P) = sigma_0 and RO_{pi_j}(P) = sigma_j XOR sigma_0 (j ≥ 1), proved for172    the executed rollout. -/173theorem rolloutWinner_channel (j : Nat) (p : List Nat) :174    rolloutWinner j p = channel j (nimSum p) := by175  rw [rolloutWinner_eq]176  exact rolloutMoves_parity j p

Project declarations in the statement: Game.rolloutWinner, channel, nimSum

Project declarations used by the proof or definition body

Game.rolloutWinner, Game.rolloutWinner_eq, Rollout.rolloutMoves, Rollout.rolloutMoves_parity, channel, nimSum

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

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

EVALUATION ACCOUNTING for one multi-head decision: rollout j makes L_j + 1 policy evaluations; together Σ_j (L_j + 1) = (total simulated moves) + B ≤ B·(N(2^B−1)+1); in addition there are B reset steps (one per rollout) and ONE readout evaluation.

Statement as elaborated and printed by Lean 4.26.0

∀ {B : ℕ} {P : List ℕ},
  NimAudit.Game.Width B P →
    (∀ (j : ℕ), NimAudit.RolloutExec.polEvals B j P = NimAudit.Rollout.rolloutMoves j P + 1) ∧
      (List.map (fun j => NimAudit.RolloutExec.polEvals B j P) (List.range B)).sum =
          NimAudit.Game.totalRolloutMoves B P + B ∧
        NimAudit.Game.totalRolloutMoves B P + B ≤ B * NimAudit.RolloutExec.clockBound B P.length

Exact source text, lines 522–547

522/-- EVALUATION ACCOUNTING for one multi-head decision: rollout j makes L_j + 1 policy523    evaluations; together Σ_j (L_j + 1) = (total simulated moves) + B ≤ B·(N(2^B−1)+1);524    in addition there are B reset steps (one per rollout) and ONE readout evaluation. -/525theorem mhExec_evals {B : Nat} {P : List Nat} (hw : Width B P) :526    (∀ j, polEvals B j P = rolloutMoves j P + 1) ∧527    ((List.range B).map (fun j => polEvals B j P)).sum = totalRolloutMoves B P + B ∧528    totalRolloutMoves B P + B ≤ B * clockBound B P.length := by529  have he : ∀ j, polEvals B j P = rolloutMoves j P + 1 := fun j => (execRollN_spec _ hw).2.2530  refine ⟨he, ?_, ?_⟩531  · unfold totalRolloutMoves532    rw [List.map_congr_left (fun j _ => he j)]533    induction B with534    | zero => simp535    | succ k ih =>536      rw [List.range_succ, List.map_append, List.map_append, List.sum_append_nat, List.sum_append_nat]537      simp only [List.map_cons, List.map_nil, List.sum_cons, List.sum_nil]538      have : ((List.range k).map (fun j => rolloutMoves j P + 1)).sum = ((List.range k).map (fun j => rolloutMoves j P)).sum + k := by539        clear ih he hw540        induction k with541        | zero => simp542        | succ k ih2 =>543          rw [List.range_succ, List.map_append, List.map_append, List.sum_append_nat, List.sum_append_nat, ih2]544          simp; omega545      omega546  · have := totalRolloutMoves_le hw547    unfold clockBound; rw [Nat.mul_add, Nat.mul_one]; omega

Project declarations in the statement: Game.Width, Game.totalRolloutMoves, Rollout.rolloutMoves, RolloutExec.clockBound, RolloutExec.polEvals

Project declarations used by the proof or definition body

Game.Width, Game.rolloutWinner, Game.totalRolloutMoves, Game.totalRolloutMoves_le, Rollout.rolloutMoves, RolloutExec.clockBound, RolloutExec.execRollN, RolloutExec.execRollN_spec, RolloutExec.polEvals

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

theorem `Rollout.run_length`

Module NimRollout (lean/NimRollout.lean, lines 88–94) · file SHA-256 1a99428d71573d31… Axioms reported by the fresh build: propext, Quot.sound

EXECUTION COUNT: every complete run of `pi_j`, under any tie-breaking rule, has exactly `sum_h (h / 2^j + h % 2^j)` moves.

Statement as elaborated and printed by Lean 4.26.0

∀ {j : ℕ} {p : List ℕ} {n : ℕ}, NimAudit.Rollout.Run j p n → n = NimAudit.rolloutCount j p

Exact source text, lines 88–94

88/-- EXECUTION COUNT: every complete run of `pi_j`, under any tie-breaking rule,89    has exactly `sum_h (h / 2^j + h % 2^j)` moves. -/90theorem run_length {j : Nat} {p : List Nat} {n : Nat} (hr : Run j p n) :91    n = rolloutCount j p := by92  induction hr with93  | done p hz => exact (rolloutCount_zero hz).symm94  | step p q n hm _ ih => rw [ih, policyMove_count hm]

Project declarations in the statement: Rollout.Run, rolloutCount

Project declarations used by the proof or definition body

Rollout.PolicyMove, Rollout.Run, Rollout.Run.rec, Rollout.policyMove_count, Rollout.rolloutCount_zero, rolloutCount

theorem `Mastery.mh_strong`

Module WeakMastery (lean/phase8/WeakMastery.lean, lines 845–852) · file SHA-256 4c83e573f527989c… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

The multi-head player is in fact STRONGLY masterful on B-bit families, for both roles.

Statement as elaborated and printed by Lean 4.26.0

∀ (B : ℕ) (r : NimAudit.Mastery.Role),
  NimAudit.Mastery.StrongMastery (fun P => NimAudit.Game.Width B P) r
    (NimAudit.Mastery.ofSel (NimAudit.WholeGame.mhSelect B))

Exact source text, lines 845–852

845/-- The multi-head player is in fact STRONGLY masterful on B-bit families, for both roles. -/846theorem mh_strong (B : Nat) (r : Role) : StrongMastery (fun P => Width B P) r (ofSel (mhSelect B)) := by847  intro P0 hw h hl _ hnz848  have hwh : Width B (cur h) := legal_width hl hw849  obtain ⟨i, v, hd, hz⟩ := (Controller.decision_correct (cur h)).2.2 hnz850  obtain ⟨x, _, _, hmv⟩ := (Controller.decision_correct (cur h)).2.1 i v hd851  refine ⟨(cur h).set i v, ?_, hmv, hz⟩852  unfold ofSel; rw [mhSelect_eq hwh]; simp [Controller.ctrlSel, hd]

Project declarations in the statement: Game.Width, Mastery.Role, Mastery.StrongMastery, Mastery.ofSel, WholeGame.mhSelect

Project declarations used by the proof or definition body

Controller.ctrlSel, Controller.decisionMove, Controller.decision_correct, Game.Move, Game.Terminal, Game.Width, Mastery.Hist, Mastery.Legal, Mastery.Role, Mastery.cur, Mastery.legal_width, Mastery.mover, Mastery.ofSel, WholeGame.mhSelect, WholeGame.mhSelect_eq, nimSum

Definitions these statements use

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

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

The nim-sum reconstructed from the B rollout outcomes o 0, ..., o (B-1).

Statement as elaborated and printed by Lean 4.26.0

ℕ → (ℕ → Bool) → ℕ

Exact source text, lines 211–212

211/-- The nim-sum reconstructed from the B rollout outcomes o 0, ..., o (B-1). -/212def reconstruct (B : Nat) (o : Nat → Bool) : Nat := ofBits B (recoverBit o)

Project declarations in the statement: none

Project declarations used by the proof or definition body

Game.ofBits, Game.recoverBit

def `Game.rolloutWinner`

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

Rollout outcome RO_{pi_j}(P) as a game: both players follow pi_j; the result is `true` iff the player to move at P (the first player) wins under normal play. At a terminal start it is `false`.

Statement as elaborated and printed by Lean 4.26.0

ℕ → List ℕ → Bool

Exact source text, lines 142–152

142/-- Rollout outcome RO_{pi_j}(P) as a game: both players follow pi_j; the result is143    `true` iff the player to move at P (the first player) wins under normal play.144    At a terminal start it is `false`. -/145def rolloutWinner (j : Nat) (p : List Nat) : Bool :=146  match h : policyStep j p with147  | none => false148  | some q => !rolloutWinner j q149termination_by rolloutCount j p150decreasing_by151  have := policyMove_count (policyStep_some h)152  omega

Project declarations in the statement: none

Project declarations used by the proof or definition body

Rollout.policyMove_count, Rollout.policyStep, Rollout.policyStep_some, rolloutCount

def `channel`

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

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → Bool

Exact source text, lines 77–78

77def channel (j sigma : Nat) : Bool :=78  if j = 0 then sigma.testBit 0 else xor (sigma.testBit j) (sigma.testBit 0)

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

def `Rollout.rolloutMoves`

Module NimRollout (lean/NimRollout.lean, lines 205–214) · file SHA-256 1a99428d71573d31…

The simulator: apply `policyStep` until no move is available, counting moves. Termination is justified by `policyMove_count`.

Statement as elaborated and printed by Lean 4.26.0

ℕ → List ℕ → ℕ

Exact source text, lines 205–214

205/-- The simulator: apply `policyStep` until no move is available, counting moves.206    Termination is justified by `policyMove_count`. -/207def rolloutMoves (j : Nat) (p : List Nat) : Nat :=208  match h : policyStep j p with209  | none => 0210  | some q => rolloutMoves j q + 1211termination_by rolloutCount j p212decreasing_by213  have := policyMove_count (policyStep_some h)214  omega

Project declarations in the statement: none

Project declarations used by the proof or definition body

Rollout.policyMove_count, Rollout.policyStep, Rollout.policyStep_some, rolloutCount

def `RolloutExec.clockBound`

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

The fixed clock bound (a function of B and N only).

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → ℕ

Exact source text, lines 97–98

97/-- The fixed clock bound (a function of B and N only). -/98def clockBound (B N : Nat) : Nat := N * (2 ^ B - 1) + 1

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `RolloutExec.polEvals`

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

Policy-network evaluations used by rollout j (clocked steps of the executor).

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → List ℕ → ℕ

Exact source text, lines 492–493

492/-- Policy-network evaluations used by rollout j (clocked steps of the executor). -/493def polEvals (B j : Nat) (P : List Nat) : Nat := (execRollN B j (fun _ => false) P).2

Project declarations in the statement: none

Project declarations used by the proof or definition body

RolloutExec.execRollN

inductive `Rollout.Run`

Module NimRollout (lean/NimRollout.lean, lines 34–38) · file SHA-256 1a99428d71573d31…

`Run j p n`: following `pi_j` from board `p` reaches the all-zero board after exactly `n` policy moves.

Statement as elaborated and printed by Lean 4.26.0

ℕ → List ℕ → ℕ → Prop

Exact source text, lines 34–38

34/-- `Run j p n`: following `pi_j` from board `p` reaches the all-zero board after35    exactly `n` policy moves. -/36inductive Run (j : Nat) : List Nat → Nat → Prop37  | done (p : List Nat) : (∀ x ∈ p, x = 0) → Run j p 038  | step (p q : List Nat) (n : Nat) : PolicyMove j p q → Run j q n → Run j p (n + 1)

Project declarations in the statement: none

Project declarations used by the proof or definition body

Rollout.PolicyMove

def `rolloutCount`

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

Statement as elaborated and printed by Lean 4.26.0

ℕ → List ℕ → ℕ

Exact source text, lines 82–82

82def rolloutCount (j : Nat) (rows : List Nat) : Nat := (rows.map (heapCount j)).sum

Project declarations in the statement: none

Project declarations used by the proof or definition body

heapCount

inductive `Mastery.Role`

Module WeakMastery (lean/phase8/WeakMastery.lean, lines 37–40) · file SHA-256 4c83e573f527989c…

Statement as elaborated and printed by Lean 4.26.0

Type

Exact source text, lines 37–40

37inductive Role where38  | first39  | second40  deriving DecidableEq

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Mastery.StrongMastery`

Module WeakMastery (lean/phase8/WeakMastery.lean, lines 812–817) · file SHA-256 4c83e573f527989c…

Strong mastery (Definition def:mastery, first clause) relative to F and r: at EVERY legal history (arbitrary actions by both players) with the agent to move at an N-position, σ plays a move to a P-position.

Statement as elaborated and printed by Lean 4.26.0

(List ℕ → Prop) → NimAudit.Mastery.Role → NimAudit.Mastery.Strat → Prop

Exact source text, lines 812–817

812/-- Strong mastery (Definition def:mastery, first clause) relative to F and r: at EVERY813    legal history (arbitrary actions by both players) with the agent to move at an814    N-position, σ plays a move to a P-position. -/815def StrongMastery (F : List Nat → Prop) (r : Role) (σ : Strat) : Prop :=816  ∀ P0, F P0 → ∀ h, Legal P0 h → mover h = r → nimSum (cur h) ≠ 0 →817    ∃ Q, σ h = some Q ∧ Move (cur h) Q ∧ nimSum Q = 0

Project declarations in the statement: Mastery.Role, Mastery.Strat

Project declarations used by the proof or definition body

Game.Move, Mastery.Hist, Mastery.Legal, Mastery.Role, Mastery.Strat, Mastery.cur, Mastery.mover, nimSum

def `Mastery.ofSel`

Module WeakMastery (lean/phase8/WeakMastery.lean, lines 498–499) · file SHA-256 4c83e573f527989c…

The memoryless strategy defined by a board selector.

Statement as elaborated and printed by Lean 4.26.0

(List ℕ → Option (List ℕ)) → NimAudit.Mastery.Strat

Exact source text, lines 498–499

498/-- The memoryless strategy defined by a board selector. -/499def ofSel (sel : List Nat → Option (List Nat)) : Strat := fun h => sel (cur h)

Project declarations in the statement: Mastery.Strat

Project declarations used by the proof or definition body

Mastery.Hist, Mastery.cur

def `WholeGame.mhSelect`

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

The multi-head player: run the B network rollouts, feed their outcomes and the board to the compiled multi-head network, decode its output wires and apply the move.

Statement as elaborated and printed by Lean 4.26.0

ℕ → List ℕ → Option (List ℕ)

Exact source text, lines 159–163

159/-- The multi-head player: run the B network rollouts, feed their outcomes and the board160    to the compiled multi-head network, decode its output wires and apply the move. -/161def mhSelect (B : Nat) (P : List Nat) : Option (List Nat) :=162  applyM P (netBinSem (mhNet B P.length (rIdx P.length)) P.length (rIdx P.length) B163    (obsIn B P.length P (fun j => rollOut B j P)))

Project declarations in the statement: none

Project declarations used by the proof or definition body

SelectCircuit.applyM, SelectCircuit.obsIn, ThresholdInst.mhNet, ThresholdInst.netBinSem, WholeGame.rIdx, WholeGame.rollOut

Full modules

Module	File	Lines	Imports
NimCore	`lean/NimCore.lean`	139	`Std`
NimGame	`lean/phase2/NimGame.lean`	634	NimRollout
NimRollout	`lean/NimRollout.lean`	349	NimCore
RolloutExec	`lean/phase6/RolloutExec.lean`	896	Barrier
WeakMastery	`lean/phase8/WeakMastery.lean`	959	Misc
WholeGame	`lean/phase5/WholeGame.lean`	347	ThresholdInst

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

Proposition 5.9B structured rollout heads recover all nim-sum bits; an AC0 readout then plays a winning move

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

theorem Game.agent_wins

theorem RolloutExec.mhExec_wins

theorem RolloutExec.mhExec_evals

theorem Game.totalRolloutMoves_le

theorem Rollout.run_length

theorem Mastery.mh_strong

Definitions these statements use

def Game.agent

def Game.reconstruct

def Game.rolloutWinner

def channel

def nimSum

def Game.Width

inductive Game.Wins

def RolloutExec.mhExecSel

def Game.totalRolloutMoves

def Rollout.rolloutMoves

def RolloutExec.clockBound

def RolloutExec.polEvals

inductive Rollout.Run

def rolloutCount

inductive Mastery.Role

def Mastery.StrongMastery

def Mastery.ofSel

def WholeGame.mhSelect

Full modules

Proposition 5.9B structured rollout heads recover all nim-sum bits; an AC⁰ readout then plays a winning move

theorem `Game.rolloutWinner_channel`

theorem `Game.agent_wins`

theorem `RolloutExec.mhExec_wins`

theorem `RolloutExec.mhExec_evals`

theorem `Game.totalRolloutMoves_le`

theorem `Rollout.run_length`

theorem `Mastery.mh_strong`

def `Game.agent`

def `Game.reconstruct`

def `Game.rolloutWinner`

def `channel`

def `nimSum`

def `Game.Width`

inductive `Game.Wins`

def `RolloutExec.mhExecSel`

def `Game.totalRolloutMoves`

def `Rollout.rolloutMoves`

def `RolloutExec.clockBound`

def `RolloutExec.polEvals`

inductive `Rollout.Run`

def `rolloutCount`

inductive `Mastery.Role`

def `Mastery.StrongMastery`

def `Mastery.ofSel`

def `WholeGame.mhSelect`