Appendix C, paragraph 2All-head schedule: M+2B+2 component evaluations, with M ≤ BN(2^B−1)

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

1 Paper text

Let $M$ be the total number of simulated legal moves in the all-head schedule. The implementation uses $M+2B+2$ component evaluations: $M$ move updates, $B$ terminal tests, $B$ outcome-consumption updates, one initial reset and one final move readout. Since $M\le BN(2^B-1)$ , this agrees with the rollout-time bound in the main text while making the control overhead explicit. These are circuit evaluations, not measured processor time. The early-exit schedule uses only the visited heads and gives the same classification as the OR of all outcomes. These certificates concern the two specified schedules; the abstract definition of a finite-state controller does not certify arbitrary scheduling logic.

Generated from paper_jmlr.tex, lines 1556–1556.

2 Explain this

Time accounting for the all-head schedule. If the rollouts make $M$ simulated legal moves in total, the implementation uses $M+2B+2$ component evaluations: $M$ move updates, $B$ terminal tests, $B$ outcome-consumption updates, one initial reset and one final move readout. Since $M\le BN(2^B-1)$ , this matches the main text's bound while making control overhead explicit. The early-exit schedule uses only the heads it visits and gives the same classification as the OR of all outcomes.

These are counts of circuit evaluations, not processor time, and they certify the two specified schedules, not arbitrary controller logic.

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

Shootout.ahL_counts: on the executed move path, one reset tick plus exactly the total number of simulated moves plus $2B$ loop ticks, then one readout.
Shootout.ah_counts: the same count ( $M+2B+1$ ticks plus one readout) and $M\le BN(2^B-1)$ .
Shootout.ee_counts: early exit with $R$ heads queried uses $1+\sum_{h<R}L_h+2R$ ticks, with $R=1$ when head 0 reports 1.

Coverage record
Paper anchor	`par:controller-costs-p2` (website anchor; the manuscript has no label here)
Displayed as	Appendix C, paragraph 2
Claim	All-head schedule: M+2B+2 component evaluations, with M ≤ BN(2^B−1)
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 1556–1556; SHA-256 of the normalised block source `8c0ab472930a121f…`
Lean declarations	`NimAudit.Shootout.ahL_counts` (Shootout, lines 1368–1374, file `1abd814426d3…`) `NimAudit.Shootout.ah_counts` (Shootout, lines 1249–1259, file `1abd814426d3…`) `NimAudit.Shootout.ee_counts` (Shootout, lines 1233–1247, file `1abd814426d3…`)
Depends on	Section C, “Outer-controller storage and time”
Audited correspondence rows	`par:controller-costs`
Explanations	`explain/c-controller-evals`, `formal/c-controller-evals`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `Shootout.ahL_counts`

Module Shootout (lean/phase7/Shootout.lean, lines 1368–1374) · file SHA-256 1abd814426d345b9… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

COUNTS OF THE EXECUTED MOVE PATH (B ≥ 1): 1 reset tick + exactly totalRolloutMoves + 2B loop ticks (Σ L_h legal moves, B terminal tests, B consume ticks), then one readout.

Statement as elaborated and printed by Lean 4.26.0

∀ {B N r : ℕ},
  1 ≤ B →
    B ≤ 2 ^ r →
      ∀ {P : List ℕ},
        P.length = N →
          NimAudit.Game.Width B P →
            ∀ (x0 : ℕ → Bool),
              1 +
                  (NimAudit.Shootout.loopRun (NimAudit.Shootout.cstep false B N r P false)
                      (B * N + 2) (NimAudit.Shootout.Tmax B N)
                      (NimAudit.Shootout.cstep false B N r P true x0)).2 =
                NimAudit.Game.totalRolloutMoves B P + 2 * B + 1

Exact source text, lines 1368–1374

1368/-- COUNTS OF THE EXECUTED MOVE PATH (B ≥ 1): 1 reset tick + exactly totalRolloutMoves + 2B1369    loop ticks (Σ L_h legal moves, B terminal tests, B consume ticks), then one readout. -/1370theorem ahL_counts {B N r : Nat} (hB : 1 ≤ B) (hBr : B ≤ 2 ^ r) {P : List Nat} (hP : P.length = N) (hw : Width B P)1371    (x0 : Nat → Bool) :1372    1 + (loopRun (cstep false B N r P false) (B * N + 2) (Tmax B N) (cstep false B N r P true x0)).2 =1373      totalRolloutMoves B P + 2 * B + 1 := by1374  rw [(ah_loop hB hBr hP hw x0).1, ahT_total hB]; omega

Project declarations in the statement: Game.Width, Game.totalRolloutMoves, Shootout.Tmax, Shootout.cstep, Shootout.loopRun

Project declarations used by the proof or definition body

Game.Width, Game.rolloutWinner, Game.totalRolloutMoves, Shootout.Tmax, Shootout.ahT, Shootout.ahT_total, Shootout.ah_loop, Shootout.cstep, Shootout.loopRun, Shootout.oW

theorem `Shootout.ah_counts`

Module Shootout (lean/phase7/Shootout.lean, lines 1249–1259) · file SHA-256 1abd814426d345b9… Axioms reported by the fresh build: propext, Quot.sound

COUNTS, ALL HEADS (move path, B ≥ 1): 1 reset tick + totalRolloutMoves legal moves + B terminal tests + B consume ticks = totalRolloutMoves + 2B + 1 controller ticks, then ONE readout-network evaluation: totalRolloutMoves + 2B + 2 network evaluations in all (phase 6's functional composition counted totalRolloutMoves + 2B + 1: B separate resets instead of 1 reset + B consume/reload ticks).

Statement as elaborated and printed by Lean 4.26.0

∀ {B : ℕ},
  1 ≤ B →
    ∀ {P : List ℕ},
      NimAudit.Game.Width B P →
        1 + NimAudit.Shootout.ahT P (B - 1) 0 = NimAudit.Game.totalRolloutMoves B P + 2 * B + 1 ∧
          NimAudit.Shootout.ahT P (B - 1) 0 ≤ NimAudit.Shootout.Tmax B P.length ∧
            NimAudit.Game.totalRolloutMoves B P ≤ B * (P.length * (2 ^ B - 1))

Exact source text, lines 1249–1259

1249/-- COUNTS, ALL HEADS (move path, B ≥ 1): 1 reset tick + totalRolloutMoves legal moves + B1250    terminal tests + B consume ticks = totalRolloutMoves + 2B + 1 controller ticks, then ONE1251    readout-network evaluation: totalRolloutMoves + 2B + 2 network evaluations in all1252    (phase 6's functional composition counted totalRolloutMoves + 2B + 1: B separate1253    resets instead of 1 reset + B consume/reload ticks). -/1254theorem ah_counts {B : Nat} (hB : 1 ≤ B) {P : List Nat} (hw : Width B P) :1255    1 + ahT P (B - 1) 0 = totalRolloutMoves B P + 2 * B + 1 ∧1256    ahT P (B - 1) 0 ≤ Tmax B P.length ∧1257    totalRolloutMoves B P ≤ B * (P.length * (2 ^ B - 1)) := by1258  refine ⟨by rw [ahT_total hB]; omega, ?_, totalRolloutMoves_le hw⟩1259  have := ahT_le B hw (B - 1) 0; unfold Tmax; rw [show B - 1 + 1 = B by omega] at this; exact this

Project declarations in the statement: Game.Width, Game.totalRolloutMoves, Shootout.Tmax, Shootout.ahT

Project declarations used by the proof or definition body

Game.Width, Game.totalRolloutMoves, Game.totalRolloutMoves_le, RolloutExec.clockBound, Shootout.Tmax, Shootout.ahT, Shootout.ahT_le, Shootout.ahT_total

theorem `Shootout.ee_counts`

Module Shootout (lean/phase7/Shootout.lean, lines 1233–1247) · file SHA-256 1abd814426d345b9… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

COUNTS, EARLY EXIT (B ≥ 1): with R = number of heads queried (R ≤ B, R = 1 when RO_{π₀}(P) = 1), the controller executes 1 reset tick + Σ_{h<R} L_h policy steps that are legal simulated moves + R terminal-test steps + R consume ticks (R − 1 of which also reload the board for the next head; the last stops) — i.e. 1 + Σ_{h<R} L_h + 2R ticks — and then holds. The padded clock runs 1 + Tmax ticks instead.

Statement as elaborated and printed by Lean 4.26.0

∀ {B : ℕ},
  1 ≤ B →
    ∀ {P : List ℕ},
      NimAudit.Game.Width B P →
        NimAudit.Shootout.eeT B P (B - 1) 0 =
            (List.map (fun h => NimAudit.Rollout.rolloutMoves h P)
                  (List.range (NimAudit.Shootout.eeR P (B - 1) 0))).sum +
              2 * NimAudit.Shootout.eeR P (B - 1) 0 ∧
          NimAudit.Shootout.eeR P (B - 1) 0 ≤ B ∧
            (NimAudit.Game.rolloutWinner 0 P = true → NimAudit.Shootout.eeR P (B - 1) 0 = 1) ∧
              NimAudit.Shootout.eeT B P (B - 1) 0 ≤ NimAudit.Shootout.Tmax B P.length

Exact source text, lines 1233–1247

1233/-- COUNTS, EARLY EXIT (B ≥ 1): with R = number of heads queried (R ≤ B, R = 1 when1234    RO_{π₀}(P) = 1), the controller executes 1 reset tick + Σ_{h<R} L_h policy steps that1235    are legal simulated moves + R terminal-test steps + R consume ticks (R − 1 of which also1236    reload the board for the next head; the last stops) — i.e. 1 + Σ_{h<R} L_h + 2R ticks —1237    and then holds.  The padded clock runs 1 + Tmax ticks instead. -/1238theorem ee_counts {B : Nat} (hB : 1 ≤ B) {P : List Nat} (hw : Width B P) :1239    eeT B P (B - 1) 0 = ((List.range (eeR P (B - 1) 0)).map (fun h => rolloutMoves h P)).sum + 2 * eeR P (B - 1) 0 ∧1240    eeR P (B - 1) 0 ≤ B ∧ (rolloutWinner 0 P = true → eeR P (B - 1) 0 = 1) ∧1241    eeT B P (B - 1) 0 ≤ Tmax B P.length := by1242  refine ⟨by rw [eeT_sum, sum_plus_two, List.range_eq_range'], (ee_spec hB hw).2.2.2.2.2.1, fun h0 => ?_,1243    (ee_spec hB hw).2.2.2.2.2.2.1⟩1244  obtain ⟨k, hk⟩ : ∃ k, B - 1 = k := ⟨_, rfl⟩1245  rw [hk]; cases k with1246  | zero => rfl1247  | succ k => simp [eeR, h0]

Project declarations in the statement: Game.Width, Game.rolloutWinner, Rollout.rolloutMoves, Shootout.Tmax, Shootout.eeR, Shootout.eeT

Project declarations used by the proof or definition body

Game.Width, Game.rolloutWinner, Misc.FSM.run, Misc.shootout, Rollout.rolloutMoves, Shootout.OS.dec, Shootout.OS.j, Shootout.OS.run, Shootout.Tmax, Shootout.arun, Shootout.eeR, Shootout.eeT, Shootout.eeT_sum, Shootout.ee_spec, Shootout.initOS, Shootout.sum_plus_two, nimSum

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

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

Module Shootout (lean/phase7/Shootout.lean, lines 706–707) · file SHA-256 1abd814426d345b9…

The fixed padded clock (ticks after the reset tick): B·(N(2^B − 1) + 2).

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → ℕ

Exact source text, lines 706–707

706/-- The fixed padded clock (ticks after the reset tick): B·(N(2^B − 1) + 2). -/707def Tmax (B N : Nat) : Nat := B * (clockBound B N + 1)

Project declarations in the statement: none

Project declarations used by the proof or definition body

RolloutExec.clockBound

def `Shootout.cstep`

Module Shootout (lean/phase7/Shootout.lean, lines 139–141) · file SHA-256 1abd814426d345b9…

One clocked bit-level update.

Statement as elaborated and printed by Lean 4.26.0

Bool → ℕ → ℕ → ℕ → List ℕ → Bool → (ℕ → Bool) → ℕ → Bool

Exact source text, lines 139–141

139/-- One clocked bit-level update. -/140def cstep (early : Bool) (B N r : Nat) (P : List Nat) (rst : Bool) (x : Nat → Bool) : Nat → Bool := fun w =>141  if w < SW B N r then eval (zIn B N r x rst P) ((cForms early B N r).getD w (const false)) else false

Project declarations in the statement: none

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.const, AC0.Circ.eval, Shootout.SW, Shootout.cForms, Shootout.zIn

def `Shootout.loopRun`

Module Shootout (lean/phase7/Shootout.lean, lines 776–780) · file SHA-256 1abd814426d345b9…

Clock the update while the run wire is 1 (fuel f); returns the registers and the number of ticks executed.

Statement as elaborated and printed by Lean 4.26.0

((ℕ → Bool) → ℕ → Bool) → ℕ → ℕ → (ℕ → Bool) → (ℕ → Bool) × ℕ

Exact source text, lines 776–780

776/-- Clock the update while the run wire is 1 (fuel f); returns the registers and the number777    of ticks executed. -/778def loopRun (step : (Nat → Bool) → (Nat → Bool)) (hw : Nat) : Nat → (Nat → Bool) → (Nat → Bool) × Nat779  | 0, x => (x, 0)780  | f + 1, x => if x hw = true then ((loopRun step hw f (step x)).1, (loopRun step hw f (step x)).2 + 1) else (x, 0)

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Shootout.ahT`

Module Shootout (lean/phase7/Shootout.lean, lines 814–817) · file SHA-256 1abd814426d345b9…

Ticks of the all-head schedule from head j with k + 1 heads left.

Statement as elaborated and printed by Lean 4.26.0

List ℕ → ℕ → ℕ → ℕ

Exact source text, lines 814–817

814/-- Ticks of the all-head schedule from head j with k + 1 heads left. -/815def ahT (P : List Nat) : Nat → Nat → Nat816  | 0, j => rolloutMoves j P + 2817  | k + 1, j => rolloutMoves j P + 2 + ahT P k (j + 1)

Project declarations in the statement: none

Project declarations used by the proof or definition body

Rollout.rolloutMoves

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

Module Shootout (lean/phase7/Shootout.lean, lines 617–620) · file SHA-256 1abd814426d345b9…

Rollouts (head queries) executed by the early-exit schedule.

Statement as elaborated and printed by Lean 4.26.0

List ℕ → ℕ → ℕ → ℕ

Exact source text, lines 617–620

617/-- Rollouts (head queries) executed by the early-exit schedule. -/618def eeR (P : List Nat) : Nat → Nat → Nat619  | 0, _ => 1620  | k + 1, j => if rolloutWinner j P then 1 else eeR P k (j + 1) + 1

Project declarations in the statement: none

Project declarations used by the proof or definition body

Game.rolloutWinner

def `Shootout.eeT`

Module Shootout (lean/phase7/Shootout.lean, lines 612–615) · file SHA-256 1abd814426d345b9…

Ticks used by the early-exit schedule from head j with k + 1 heads left.

Statement as elaborated and printed by Lean 4.26.0

ℕ → List ℕ → ℕ → ℕ → ℕ

Exact source text, lines 612–615

612/-- Ticks used by the early-exit schedule from head j with k + 1 heads left. -/613def eeT (B : Nat) (P : List Nat) : Nat → Nat → Nat614  | 0, j => rolloutMoves j P + 2615  | k + 1, j => if rolloutWinner j P then rolloutMoves j P + 2 else rolloutMoves j P + 2 + eeT B P k (j + 1)

Project declarations in the statement: none

Project declarations used by the proof or definition body

Game.rolloutWinner, Rollout.rolloutMoves

Full modules

Module	File	Lines	Imports
NimGame	`lean/phase2/NimGame.lean`	634	NimRollout
NimRollout	`lean/NimRollout.lean`	349	NimCore
Shootout	`lean/phase7/Shootout.lean`	1491	Misc, BoardStore

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

Appendix C, paragraph 2All-head schedule: M+2B+2 component evaluations, with M ≤ BN(2^B−1)

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

theorem Shootout.ah_counts

theorem Shootout.ee_counts

Definitions these statements use

def Game.Width

def Game.totalRolloutMoves

def Shootout.Tmax

def Shootout.cstep

def Shootout.loopRun

def Shootout.ahT

def Game.rolloutWinner

def Rollout.rolloutMoves

def Shootout.eeR

def Shootout.eeT

Full modules

theorem `Shootout.ahL_counts`

theorem `Shootout.ah_counts`

theorem `Shootout.ee_counts`

def `Game.Width`

def `Game.totalRolloutMoves`

def `Shootout.Tmax`

def `Shootout.cstep`

def `Shootout.loopRun`

def `Shootout.ahT`

def `Game.rolloutWinner`

def `Rollout.rolloutMoves`

def `Shootout.eeR`

def `Shootout.eeT`