Remark 5.8Each rollout follows one policy and yields one bit; different heads give independent linear functionals

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

1 Paper text

Remark 5.8 (Why multiple heads are not redundant) Since $\AC^0$ is closed under parallel composition, one could compute all $k$ policies simultaneously as a single $\AC^0$ circuit. The distinction is not about computational power at the circuit level but about the rollout interface: each rollout query simulates a complete game under one policy, and at each game step only that policy determines the next move. A single rollout trajectory under a fixed policy $\pi$ produces one outcome bit; merging $k$ circuits into a single circuit does not change the fact that any one rollout follows a single deterministic rule, yielding a single bit of information. Multiple heads are useful because the agent can issue separate rollout queries under different policies $\pi_j$ , producing different game trajectories that reveal independent linear functionals of the nim-sum (cf. Propositions 5.9 and 5.10).

Generated from paper_jmlr.tex, lines 650–656.

2 Explain this

Could one big circuit simply contain all $B$ policies? At the circuit level, yes: AC⁰ is closed under parallel composition. The point is the rollout interface: one rollout follows one deterministic rule from start to end and returns one bit. Merging circuits does not change that one trajectory yields one bit.

Several heads help because separate rollouts under different policies follow different trajectories, and their outcome bits are linearly independent functions of the nim-sum: $\pi_0$ gives $\sigma_0$ ; $\pi_j$ gives $\sigma_j\oplus\sigma_0$ . Together they determine $\sigma$ .

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.rolloutWinner_channel: the executed outcome of $\pi_j$ is the channel value channel $j$ of the nim-sum: bit $0$ for $j=0$ , bit $j$ XOR bit $0$ for $j\ge1$ .
Prob.rollout_outcome_linear: the same as an inner product $\langle w_j,\sigma\rangle$ over $\mathbb F_2$ ( $w_0=1$ , $w_j=2^j\oplus1$ ).
Game.reconstruct_eq: the $B$ outcomes determine the full nim-sum on every $B$ -bit board, which is the checked form of their independence.

Coverage record
Paper anchor	`rem:why-multi-head` (manuscript label)
Displayed as	Remark 5.8
Claim	Each rollout follows one policy and yields one bit; different heads give independent linear functionals
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 650–656; SHA-256 of the normalised block source `f4008ef5ce03a22b…`
Lean declarations	`NimAudit.Game.rolloutWinner_channel` (NimGame, lines 171–176, file `23df6bb87ecf…`) `NimAudit.Prob.rollout_outcome_linear` (NimProbability, lines 920–923, file `1d5d7977a43e…`) `NimAudit.Game.reconstruct_eq` (NimGame, lines 224–240, file `23df6bb87ecf…`)
Audited correspondence rows	`rem:why-multi-head`
Explanations	`explain/rem:why-multi-head`, `formal/rem:why-multi-head`
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 `Prob.rollout_outcome_linear`

Module NimProbability (lean/phase2/NimProbability.lean, lines 920–923) · file SHA-256 1d5d7977a43e854d… Axioms reported by the fresh build: propext, Quot.sound

RO_{pi_j}(P), the executed rollout outcome, is the linear functional <w_j, sigma(P)>.

Statement as elaborated and printed by Lean 4.26.0

∀ {B j : ℕ},
  j < B →
    ∀ (P : List ℕ),
      NimAudit.Game.rolloutWinner j P =
        NimAudit.Prob.dotB B (NimAudit.Prob.headVec j) (NimAudit.nimSum P)

Exact source text, lines 920–923

920/-- RO_{pi_j}(P), the executed rollout outcome, is the linear functional <w_j, sigma(P)>. -/921theorem rollout_outcome_linear {B j : Nat} (hj : j < B) (P : List Nat) :922    rolloutWinner j P = dotB B (headVec j) (nimSum P) := by923  rw [rolloutWinner_channel, head_linear hj]

Project declarations in the statement: Game.rolloutWinner, Prob.dotB, Prob.headVec, nimSum

Project declarations used by the proof or definition body

Game.rolloutWinner, Game.rolloutWinner_channel, Prob.dotB, Prob.headVec, Prob.head_linear, channel, nimSum

theorem `Game.reconstruct_eq`

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

RECONSTRUCTION: on a B-bit board (any N, including the empty and terminal boards), the B rollout outcomes determine the full nim-sum.

Statement as elaborated and printed by Lean 4.26.0

∀ {B : ℕ} {p : List ℕ},
  NimAudit.Game.Width B p →
    NimAudit.Game.reconstruct B (NimAudit.Game.outcomes p) = NimAudit.nimSum p

Exact source text, lines 224–240

224/-- RECONSTRUCTION: on a B-bit board (any N, including the empty and terminal225    boards), the B rollout outcomes determine the full nim-sum. -/226theorem reconstruct_eq {B : Nat} {p : List Nat} (hw : Width B p) :227    reconstruct B (outcomes p) = nimSum p := by228  apply Nat.eq_of_testBit_eq229  intro i230  rw [reconstruct, testBit_ofBits]231  by_cases hi : i < B232  · simp only [hi, decide_true, Bool.true_and, recoverBit, outcomes, rolloutWinner_channel]233    by_cases h0 : i = 0234    · subst h0; simp [channel]235    · simp only [h0, if_false, channel, if_true]236      cases (nimSum p).testBit i <;> cases (nimSum p).testBit 0 <;> rfl237  · simp only [hi, decide_false, Bool.false_and]238    symm239    apply Nat.testBit_lt_two_pow240    exact Nat.lt_of_lt_of_le (nimSum_lt hw) (Nat.pow_le_pow_right (by decide) (by omega))

Project declarations in the statement: Game.Width, Game.outcomes, Game.reconstruct, nimSum

Project declarations used by the proof or definition body

Game.Width, Game.nimSum_lt, Game.ofBits, Game.outcomes, Game.reconstruct, Game.recoverBit, Game.rolloutWinner, Game.rolloutWinner_channel, Game.testBit_ofBits, channel, nimSum

Definitions these statements use

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

Module NimProbability (lean/phase2/NimProbability.lean, lines 259–262) · file SHA-256 1d5d7977a43e854d…

The F_2 inner product of the first B bits of u and v.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → ℕ → Bool

Exact source text, lines 259–262

259/-- The F_2 inner product of the first B bits of u and v. -/260def dotB : Nat → Nat → Nat → Bool261  | 0, _, _ => false262  | B + 1, u, v => xor (dotB B u v) (u.testBit B && v.testBit B)

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Prob.headVec`

Module NimProbability (lean/phase2/NimProbability.lean, lines 875–876) · file SHA-256 1d5d7977a43e854d…

The vector w_j with RO_{pi_j}(P) = <w_j, sigma(P)>: w_0 = 1, w_j = 2^j XOR 1.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ

Exact source text, lines 875–876

875/-- The vector w_j with RO_{pi_j}(P) = <w_j, sigma(P)>: w_0 = 1, w_j = 2^j XOR 1. -/876def headVec (j : Nat) : Nat := if j = 0 then 1 else 2 ^ j ^^^ 1

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

def `Game.outcomes`

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

The B actual rollout measurements of board p.

Statement as elaborated and printed by Lean 4.26.0

List ℕ → ℕ → Bool

Exact source text, lines 214–215

214/-- The B actual rollout measurements of board p. -/215def outcomes (p : List Nat) : Nat → Bool := fun j => rolloutWinner j p

Project declarations in the statement: none

Project declarations used by the proof or definition body

Game.rolloutWinner

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

Full modules

Module	File	Lines	Imports
NimCore	`lean/NimCore.lean`	139	`Std`
NimGame	`lean/phase2/NimGame.lean`	634	NimRollout
NimProbability	`lean/phase2/NimProbability.lean`	1074	NimGame

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

Remark 5.8Each rollout follows one policy and yields one bit; different heads give independent linear functionals

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 Prob.rollout_outcome_linear

theorem Game.reconstruct_eq

Definitions these statements use

def channel

def Game.rolloutWinner

def nimSum

def Prob.dotB

def Prob.headVec

def Game.Width

def Game.outcomes

def Game.reconstruct

Full modules

theorem `Game.rolloutWinner_channel`

theorem `Prob.rollout_outcome_linear`

theorem `Game.reconstruct_eq`

def `channel`

def `Game.rolloutWinner`

def `nimSum`

def `Prob.dotB`

def `Prob.headVec`

def `Game.Width`

def `Game.outcomes`

def `Game.reconstruct`