Section 5.4, paragraph 2A finite-state shootout controller: states, head selection, transitions, halting states
Checked definition or constructionLean contains the definition or construction, with checked properties.
1 Paper text
Formally, fix rollout heads π0,…,πk−1. A finite-state shootout controller is a tuple C=(S,sinit,g,δ,halt), where S is a finite set of controller states, sinit∈S is the initial state, g:S→{0,…,k−1} selects which head to use for the next rollout query, δ:S×{0,1}→S updates the controller state after observing a rollout outcome bit r=ROπg(s)(P), and halt⊆S is a set of halting states associated with an output decision. (When halt=∅, the controller simply runs for a fixed number of queries and outputs a decision at the end.)
Generated from paper_jmlr.tex, lines 663–672.
2 Explain this
A finite-state shootout controller is a small automaton that sits outside the policy heads. In each state it names
a head to query; after seeing that rollout's outcome bit it moves to a new state; some states halt with a decision.
It sees nothing but outcome bits.
Multi-head rollouts and the outer controller, tick by tick
Exact construction traceEvery value is computed from the construction’s definitions for the example shown.
Policy πj subtracts 2j from the first heap of size at least 2j, and otherwise subtracts 1 from the first
nonzero heap. A rollout lets both simulated players follow π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
o0 = 1o1 = ?o2 = ?
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 AC0.
All 16 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 stop
(0, 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 σ0 and σj⊕σ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 AC0.
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.FSM is a structure with an initial state, a head-selection map, a transition map on
(state, outcome bit) and an output for halting states; Misc.FSM.run runs it with fuel against an
abstract outcome function o : ℕ → Bool and returns the decision and the number of queries. In the executed controller
(Section 5.4, paragraph 4) each outcome is obtained by actually running the rollout. Misc.shootout is the controller
of Figure 3.
A finite-state controller over rollout heads: states are numbers; `head s` is the head
queried in state s; `next s b` is the successor after outcome b; `out s` is the
decision of a halting state.
Statement as elaborated and printed by Lean 4.26.0
Type
Exact source text, lines 362–369
362/-- A finite-state controller over rollout heads: states are numbers; `head s` is the head363 queried in state s; `next s b` is the successor after outcome b; `out s` is the364 decision of a halting state. -/365structure FSM where366 init : Nat367 head : Nat → Nat368 next : Nat → Bool → Nat369 out : Nat → Option Bool
Project declarations in the statement: none
Project declarations used by the proof or definition body
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)
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⟩
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).