Figure 3The depicted controller decides whether σ(P) ≠ 0 using at most B queries

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

1 Paper text

$A row of controller states q_0 (use pi_0), q_1 (use pi_1), dots, q_{B-1} (use pi_{B-1}), linked left to right by arrows labelled r_0 = 0, r_1 = 0 and r_j = 0. From each state an arrow labelled r_j = 1 (a dashed arrow "there exists j with r_j = 1" from the dots) leads to the halting box "sigma(P) is not 0 (declare N)" above. From q_{B-1} an arrow labelled r_{B-1} = 0 leads to the halting box "sigma(P) = 0 (declare P)" below.$

Figure 3: A simple finite-state shootout controller for deciding whether

\sigma(P)=\operatorname{nim}(P)

is zero using the

B

rollout heads of Proposition 5.9. The controller queries heads sequentially and halts as soon as it can certify

\sigma(P)\neq 0

. Reaching the final transition to

\sigma(P)=0

implicitly means

r_0=\cdots=r_{B-1}=0

Generated from paper_jmlr.tex, lines 680–718.

2 Explain this

The figure shows the early-exit controller: query $\pi_0$ ; if it returns $1$ , declare " $\sigma\ne0$ " ( $N$ -position); otherwise query $\pi_1$ , and so on. If all $B$ heads return $0$ , declare " $\sigma=0$ " ( $P$ -position). Because the channel bits are linearly independent functions of $\sigma$ , they are all zero exactly when $\sigma=0$ .

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.

16 component evaluations. Colours: reset move terminal test store and reload store and stop.

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 stop, head 0

16 / 16 Store outcome o0 = 1 and stop (an outcome 1 certifies that the nim-sum is nonzero).

Working board (0, 0, 0)

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

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

Classification

An outcome 1 was observed at head 0, so σ(P) ≠ 0 and the controller stops after 1 of 3 heads. This schedule decides whether the position is winning; it does not collect the bits a move needs.

Counting the work

Simulated moves M = 13 (1 head run).
Evaluations: 1 reset + M moves + 1 terminal test + 1 outcome update = 16. The early-exit schedule ends with its classification; it reads out no move.
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 16 controller ticks as a table

Tick	Kind	Working board	parity	o₀…	What happens
1	reset	(3, 4, 6)	0	000	Reset: load the board, select head 0, clear the outcomes.
2	move	(2, 4, 6)	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	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)	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	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)	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	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)	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	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)	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	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)	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	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)	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)	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 stop	(0, 0, 0)	1	100	Store outcome o0 = 1 and stop (an outcome 1 certifies that the nim-sum is nonzero).

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

Misc.shootout_spec (OR of the outcomes, at most $B$ queries) and Misc.shootout_decides (with the exact structured heads the decision is $[\operatorname{nim}(P)\ne0]$ , for every $B$ -bit board).

Coverage record
Paper anchor	`fig:fsm-shootout-controller` (manuscript label)
Displayed as	Figure 3
Claim	The depicted controller decides whether σ(P) ≠ 0 using at most B queries
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 680–718; SHA-256 of the normalised block source `330e81321971be45…`
Lean declarations	`NimAudit.Misc.shootout_spec` (Misc, lines 456–466, file `07766c03566d…`) `NimAudit.Misc.shootout_decides` (Misc, lines 485–490, file `07766c03566d…`)
Explanations	`explain/fig:fsm-shootout-controller`, `formal/fig:fsm-shootout-controller`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `Misc.shootout_spec`

Module Misc (lean/phase6/Misc.lean, lines 456–466) · file SHA-256 07766c03566dbfca… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

SHOOTOUT CONTROLLER THEOREM: started at head 0 with fuel B + 1 it outputs the OR of the B outcome bits, using at most B queries (one query if head 0 reports 1).

Statement as elaborated and printed by Lean 4.26.0

∀ {B : ℕ},
  1 ≤ B →
    ∀ (o : ℕ → Bool),
      ((NimAudit.Misc.shootout B).run o (B + 1) 0).1 = some ((List.range B).any o) ∧
        ((NimAudit.Misc.shootout B).run o (B + 1) 0).2 ≤ B ∧
          (o 0 = true → ((NimAudit.Misc.shootout B).run o (B + 1) 0).2 = 1)

Exact source text, lines 456–466

456/-- SHOOTOUT CONTROLLER THEOREM: started at head 0 with fuel B + 1 it outputs the OR of the457    B outcome bits, using at most B queries (one query if head 0 reports 1). -/458theorem shootout_spec {B : Nat} (hB : 1 ≤ B) (o : Nat → Bool) :459    ((shootout B).run o (B + 1) 0).1 = some ((List.range B).any o) ∧460    ((shootout B).run o (B + 1) 0).2 ≤ B ∧461    (o 0 = true → ((shootout B).run o (B + 1) 0).2 = 1) := by462  obtain ⟨k, rfl⟩ : ∃ k, B = k + 1 := ⟨B - 1, by omega⟩463  have h := shootout_from (B := k + 1) o k 0 (by omega)464  rw [show k + 1 + 1 = k + 2 by omega, h, List.range_eq_range']465  refine ⟨rfl, by simp; omega, fun h0 => ?_⟩466  simp [firstHit_hit (show 0 < k + 1 by omega) h0]

Project declarations in the statement: Misc.FSM.run, Misc.shootout

Project declarations used by the proof or definition body

Misc.FSM.run, Misc.firstHit, Misc.firstHit_hit, Misc.shootout, Misc.shootout_from

theorem `Misc.shootout_decides`

Module Misc (lean/phase6/Misc.lean, lines 485–490) · file SHA-256 07766c03566dbfca… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

The shootout over the exact structured heads decides whether P is an N-position.

Statement as elaborated and printed by Lean 4.26.0

∀ {B : ℕ},
  1 ≤ B →
    ∀ {P : List ℕ},
      NimAudit.Game.Width B P →
        ((NimAudit.Misc.shootout B).run (fun j => NimAudit.Game.rolloutWinner j P) (B + 1) 0).1 =
            some (decide (NimAudit.nimSum P ≠ 0)) ∧
          ((NimAudit.Misc.shootout B).run (fun j => NimAudit.Game.rolloutWinner j P) (B + 1) 0).2 ≤
            B

Exact source text, lines 485–490

485/-- The shootout over the exact structured heads decides whether P is an N-position. -/486theorem shootout_decides {B : Nat} (hB : 1 ≤ B) {P : List Nat} (hw : Width B P) :487    ((shootout B).run (fun j => rolloutWinner j P) (B + 1) 0).1 = some (decide (nimSum P ≠ 0)) ∧488    ((shootout B).run (fun j => rolloutWinner j P) (B + 1) 0).2 ≤ B := by489  obtain ⟨h1, h2, _⟩ := shootout_spec hB (fun j => rolloutWinner j P)490  exact ⟨by rw [h1, channels_or hB hw], h2⟩

Project declarations in the statement: Game.Width, Game.rolloutWinner, Misc.FSM.run, Misc.shootout, nimSum

Project declarations used by the proof or definition body

Game.Width, Game.rolloutWinner, Misc.FSM.run, Misc.channels_or, Misc.shootout, Misc.shootout_spec, nimSum

Definitions these statements use

def `Misc.FSM.run`

Module Misc (lean/phase6/Misc.lean, lines 371–376) · file SHA-256 07766c03566dbfca…

Run with fuel against outcome oracle o: decision and number of queries.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Misc.FSM → (ℕ → Bool) → ℕ → ℕ → Option Bool × ℕ

Exact source text, lines 371–376

371/-- Run with fuel against outcome oracle o: decision and number of queries. -/372def FSM.run (C : FSM) (o : Nat → Bool) : Nat → Nat → Option Bool × Nat373  | 0, _ => (none, 0)374  | f + 1, s => match C.out s with375    | some d => (some d, 0)376    | none => ((C.run o f (C.next s (o (C.head s)))).1, (C.run o f (C.next s (o (C.head s)))).2 + 1)

Project declarations in the statement: Misc.FSM

Project declarations used by the proof or definition body

Misc.FSM, Misc.FSM.head, Misc.FSM.next, Misc.FSM.out

def `Misc.shootout`

Module Misc (lean/phase6/Misc.lean, lines 378–382) · file SHA-256 07766c03566dbfca…

The controller of the figure: states 0..B−1 query heads 0..B−1 in turn; state B declares σ ≠ 0 (N-position), state B+1 declares σ = 0 (P-position).

Statement as elaborated and printed by Lean 4.26.0

ℕ → NimAudit.Misc.FSM

Exact source text, lines 378–382

378/-- The controller of the figure: states 0..B−1 query heads 0..B−1 in turn; state B379    declares σ ≠ 0 (N-position), state B+1 declares σ = 0 (P-position). -/380def shootout (B : Nat) : FSM :=381  ⟨0, id, fun s b => if b then B else if s + 1 < B then s + 1 else B + 1,382   fun s => if s = B then some true else if s = B + 1 then some false else none⟩

Project declarations in the statement: Misc.FSM

Project declarations used by the proof or definition body

Misc.FSM.mk

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

Full modules

Module	File	Lines	Imports
Misc	`lean/phase6/Misc.lean`	912	Bypass
NimCore	`lean/NimCore.lean`	139	`Std`
NimGame	`lean/phase2/NimGame.lean`	634	NimRollout

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

Figure 3The depicted controller decides whether σ(P) ≠ 0 using at most B queries

1 Paper text

2 Explain this

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

Classification

Counting the work

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem Misc.shootout_spec

theorem Misc.shootout_decides

Definitions these statements use

def Misc.FSM.run

def Misc.shootout

def Game.Width

def Game.rolloutWinner

def nimSum

Full modules

theorem `Misc.shootout_spec`

theorem `Misc.shootout_decides`

def `Misc.FSM.run`

def `Misc.shootout`

def `Game.Width`

def `Game.rolloutWinner`

def `nimSum`