Section 5.4, “Finite-state shootout controller (FSM over policy heads)”Early stopping after a nonzero outcome leaves the decision (the OR of all channel bits) unchanged

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

1 Paper text

Finite-state shootout controller (FSM over policy heads). The multi-channel classifier can stop early after a nonzero channel outcome, without changing its Boolean decision rule (the OR of all channel bits). This limited scheduling optimisation does not give the single-channel readout an unrestricted sequential controller. To make this adaptivity explicit (without changing the $\AC^0$ constraints on each head), it is convenient to view head-selection as a small finite-state controller that sits outside the heads and only sees the terminal win/loss bit of each rollout.

Generated from paper_jmlr.tex, lines 658–661.

2 Explain this

The multi-channel classifier only needs to know whether some channel bit is $1$ (that is, whether $\sigma\ne0$ ). So it may stop as soon as one rollout returns $1$ . This early exit saves rollouts but leaves the decision rule unchanged: it is still the OR of all channel bits.

Caveat: early stopping is a scheduling optimisation for classification. It does not give the single-channel readout extra power, and it is not enough for move selection (see the next paragraphs).

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: started at head $0$ with fuel $B+1$ , the depicted controller outputs the OR of the $B$ outcome bits, using at most $B$ queries, and exactly one query when head $0$ reports $1$ .
Misc.channels_or: with the exact structured heads, the OR of the channel bits is " $\operatorname{nim}(P)\ne0$ ".
Shootout.ee_spec: the bit-level outer controller with the early-exit schedule stops after exactly the predicted number of ticks with decision $[\operatorname{nim}(P)\ne0]$ , matching the abstract controller.

Coverage record
Paper anchor	`par:shootout-controller` (manuscript label)
Displayed as	Section 5.4, “Finite-state shootout controller (FSM over policy heads)”
Claim	Early stopping after a nonzero outcome leaves the decision (the OR of all channel bits) unchanged
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 658–661; SHA-256 of the normalised block source `2f827b0e7a8341dc…`
Lean declarations	`NimAudit.Misc.shootout_spec` (Misc, lines 456–466, file `07766c03566d…`) `NimAudit.Misc.channels_or` (Misc, lines 468–483, file `07766c03566d…`) `NimAudit.Shootout.ee_spec` (Shootout, lines 709–733, file `1abd814426d3…`)
Depends on	Proposition 5.9
Audited correspondence rows	`par:shootout-controller`
Explanations	`explain/par:shootout-controller`, `formal/par: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.channels_or`

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

With the exact structured heads, the OR of the channel bits is (nim(P) ≠ 0).

Statement as elaborated and printed by Lean 4.26.0

∀ {B : ℕ},
  1 ≤ B →
    ∀ {P : List ℕ},
      NimAudit.Game.Width B P →
        ((List.range B).any fun j => NimAudit.Game.rolloutWinner j P) =
          decide (NimAudit.nimSum P ≠ 0)

Exact source text, lines 468–483

468/-- With the exact structured heads, the OR of the channel bits is (nim(P) ≠ 0). -/469theorem channels_or {B : Nat} (hB : 1 ≤ B) {P : List Nat} (hw : Width B P) :470    (List.range B).any (fun j => rolloutWinner j P) = decide (nimSum P ≠ 0) := by471  have hσ := nimSum_lt hw472  apply Bool.eq_iff_iff.mpr473  simp only [List.any_eq_true, List.mem_range, decide_eq_true_iff, rolloutWinner_channel, channel]474  constructor475  · rintro ⟨j, hj, h⟩ h0476    rw [h0] at h; split at h <;> simp at h477  · intro h0478    by_cases h1 : (nimSum P).testBit 0 = true479    · exact ⟨0, by omega, by simp [h1]⟩480    · obtain ⟨k, hk, hbit⟩ := (pos_iff_bitLE hσ).1 (by omega)481      have hk0 : k ≠ 0 := by intro e; subst e; exact h1 hbit482      refine ⟨k, hk, ?_⟩483      simp [hk0, hbit, show (nimSum P).testBit 0 = false by simpa using h1]

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

Project declarations used by the proof or definition body

ControllerBits.pos_iff_bitLE, Game.Width, Game.nimSum_lt, Game.rolloutWinner, Game.rolloutWinner_channel, channel, nimSum

theorem `Shootout.ee_spec`

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

EARLY-EXIT SEMANTIC THEOREM (B ≥ 1): after the reset, the controller stops after exactly T = eeT ticks (running at every earlier tick), with decision dec = [nim(P) ≠ 0]; the decision and the number of queries are those of Misc.shootout run on the actual rollout outcomes; T ≤ Tmax.

Statement as elaborated and printed by Lean 4.26.0

∀ {B : ℕ},
  1 ≤ B →
    ∀ {P : List ℕ},
      NimAudit.Game.Width B P →
        (NimAudit.Shootout.arun true B P (NimAudit.Shootout.eeT B P (B - 1) 0)
                (NimAudit.Shootout.initOS B P)).run =
            false ∧
          (NimAudit.Shootout.arun true B P (NimAudit.Shootout.eeT B P (B - 1) 0)
                  (NimAudit.Shootout.initOS B P)).dec =
              decide (NimAudit.nimSum P ≠ 0) ∧
            (∀ u < NimAudit.Shootout.eeT B P (B - 1) 0,
                (NimAudit.Shootout.arun true B P u (NimAudit.Shootout.initOS B P)).run = true) ∧
              some
                    (NimAudit.Shootout.arun true B P (NimAudit.Shootout.eeT B P (B - 1) 0)
                        (NimAudit.Shootout.initOS B P)).dec =
                  ((NimAudit.Misc.shootout B).run (fun h => NimAudit.Game.rolloutWinner h P) (B + 1)
                      0).1 ∧
                NimAudit.Shootout.eeR P (B - 1) 0 =
                    ((NimAudit.Misc.shootout B).run (fun h => NimAudit.Game.rolloutWinner h P)
                        (B + 1) 0).2 ∧
                  NimAudit.Shootout.eeR P (B - 1) 0 ≤ B ∧
                    NimAudit.Shootout.eeT B P (B - 1) 0 ≤ NimAudit.Shootout.Tmax B P.length ∧
                      (NimAudit.Shootout.arun true B P (NimAudit.Shootout.eeT B P (B - 1) 0)
                              (NimAudit.Shootout.initOS B P)).j +
                          1 =
                        NimAudit.Shootout.eeR P (B - 1) 0

Exact source text, lines 709–733

709/-- EARLY-EXIT SEMANTIC THEOREM (B ≥ 1): after the reset, the controller stops after exactly710    T = eeT ticks (running at every earlier tick), with decision dec = [nim(P) ≠ 0]; the711    decision and the number of queries are those of Misc.shootout run on the actual712    rollout outcomes; T ≤ Tmax. -/713theorem ee_spec {B : Nat} (hB : 1 ≤ B) {P : List Nat} (hw : Width B P) :714    (arun true B P (eeT B P (B - 1) 0) (initOS B P)).run = false ∧715    (arun true B P (eeT B P (B - 1) 0) (initOS B P)).dec = decide (nimSum P ≠ 0) ∧716    (∀ u, u < eeT B P (B - 1) 0 → (arun true B P u (initOS B P)).run = true) ∧717    some (arun true B P (eeT B P (B - 1) 0) (initOS B P)).dec =718      ((Misc.shootout B).run (fun h => rolloutWinner h P) (B + 1) 0).1 ∧719    eeR P (B - 1) 0 = ((Misc.shootout B).run (fun h => rolloutWinner h P) (B + 1) 0).2 ∧720    eeR P (B - 1) 0 ≤ B ∧ eeT B P (B - 1) 0 ≤ Tmax B P.length ∧721    (arun true B P (eeT B P (B - 1) 0) (initOS B P)).j + 1 = eeR P (B - 1) 0 := by722  have hinit : initOS B P = ld P 0 false (fun _ => false) := by723    simp [initOS, ld]; omega724  rw [hinit]725  obtain ⟨h1, h2, h3, h4⟩ := ee_run B P (B - 1) 0 (by omega) (fun _ => false)726  have hsh := Misc.shootout_from (B := B) (fun h => rolloutWinner h P) (B - 1) 0 (by omega)727  rw [show B - 1 + 2 = B + 1 by omega] at hsh728  have hR := eeR_shootout B P (B - 1) 0 (by omega)729  rw [show B - 1 + 2 = B + 1 by omega] at hR730  refine ⟨h1, ?_, h3, ?_, hR, by have := eeR_le P (B - 1) 0; omega, ?_, by rw [h4]; omega⟩731  · rw [h2, show B - 1 + 1 = B by omega, ← List.range_eq_range']; exact Misc.channels_or hB hw732  · rw [hsh, h2]733  · have := eeT_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.rolloutWinner, Misc.FSM.run, Misc.shootout, Shootout.OS.dec, Shootout.OS.j, Shootout.OS.run, Shootout.Tmax, Shootout.arun, Shootout.eeR, Shootout.eeT, Shootout.initOS, nimSum

Project declarations used by the proof or definition body

Game.Width, Game.rolloutWinner, Misc.FSM.run, Misc.channels_or, Misc.firstHit, Misc.shootout, Misc.shootout_from, RolloutExec.RS, RolloutExec.RS.mk, RolloutExec.clockBound, Shootout.OS, Shootout.OS.dec, Shootout.OS.j, Shootout.OS.mk, Shootout.OS.noConfusion, Shootout.OS.run, Shootout.Tmax, Shootout.arun, Shootout.eeR, Shootout.eeR_le, Shootout.eeR_shootout, Shootout.eeT, Shootout.eeT_le, Shootout.ee_run, Shootout.initOS, Shootout.ld, 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

def `Shootout.OS.dec`

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

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Shootout.OS → Bool

Exact source text, lines 38–38

38  dec : Bool

Project declarations in the statement: Shootout.OS

Project declarations used by the proof or definition body

Shootout.OS

def `Shootout.OS.j`

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

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Shootout.OS → ℕ

Exact source text, lines 39–39

39  j : Nat

Project declarations in the statement: Shootout.OS

Project declarations used by the proof or definition body

Shootout.OS

def `Shootout.OS.run`

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

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Shootout.OS → Bool

Exact source text, lines 37–37

37  run : Bool

Project declarations in the statement: Shootout.OS

Project declarations used by the proof or definition body

Shootout.OS

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

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

Semantic run of k ticks (no reset).

Statement as elaborated and printed by Lean 4.26.0

Bool → ℕ → List ℕ → ℕ → NimAudit.Shootout.OS → NimAudit.Shootout.OS

Exact source text, lines 503–506

503/-- Semantic run of k ticks (no reset). -/504def arun (early : Bool) (B : Nat) (P : List Nat) : Nat → OS → OS505  | 0, s => s506  | k + 1, s => arun early B P k (ostep early B P false s)

Project declarations in the statement: Shootout.OS

Project declarations used by the proof or definition body

Shootout.OS, Shootout.ostep

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

def `Shootout.initOS`

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

Total reset (from any register contents): load the board, head 0, nothing stored. Convention B = 0: there are no heads, run = 0 at once and dec = 0.

Statement as elaborated and printed by Lean 4.26.0

ℕ → List ℕ → NimAudit.Shootout.OS

Exact source text, lines 42–44

42/-- Total reset (from any register contents): load the board, head 0, nothing stored.43    Convention B = 0: there are no heads, run = 0 at once and dec = 0. -/44def initOS (B : Nat) (P : List Nat) : OS := ⟨⟨P, false, false⟩, decide (1 ≤ B), false, 0, fun _ => false⟩

Project declarations in the statement: Shootout.OS

Project declarations used by the proof or definition body

RolloutExec.RS.mk, Shootout.OS.mk

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

Section 5.4, “Finite-state shootout controller (FSM over policy heads)”Early stopping after a nonzero outcome leaves the decision (the OR of all channel bits) unchanged

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

theorem Shootout.ee_spec

Definitions these statements use

def Misc.FSM.run

def Misc.shootout

def Game.Width

def Game.rolloutWinner

def nimSum

def Shootout.OS.dec

def Shootout.OS.j

def Shootout.OS.run

def Shootout.Tmax

def Shootout.arun

def Shootout.eeR

def Shootout.eeT

def Shootout.initOS

Full modules

theorem `Misc.shootout_spec`

theorem `Misc.channels_or`

theorem `Shootout.ee_spec`

def `Misc.FSM.run`

def `Misc.shootout`

def `Game.Width`

def `Game.rolloutWinner`

def `nimSum`

def `Shootout.OS.dec`

def `Shootout.OS.j`

def `Shootout.OS.run`

def `Shootout.Tmax`

def `Shootout.arun`

def `Shootout.eeR`

def `Shootout.eeT`

def `Shootout.initOS`