Section 5.4, paragraph 4The implemented outer controller: early-exit classifier and all-head schedule for move selection

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

1 Paper text

The checked implementation includes the outer controller: it selects a head, executes its rollout, records the outcome and either reloads the original board for the next head or halts. For classification it stops at the first outcome 1. For move selection our implementation runs all $B$ heads, since an early classification decision need not supply the invariant bits required by the move readout. Each controller tick is itself an $\AC^0$ map. The original board remains available as a read-only input throughout; it is not an oracle for its nim-sum. Appendix C specifies the storage and update costs.

Generated from paper_jmlr.tex, lines 678–678.

2 Explain this

The checked implementation is a complete machine, not just the abstract automaton. In each tick it does exactly one of: reset (load the board, select head $0$ ); one move of the selected head's rollout; a terminal test that finds the current rollout finished; or consume a finished rollout (store its outcome, then stop or reload the original board for the next head).

Two schedules are distinguished:

early exit for classification: stop at the first outcome $1$ ;
all heads for move selection: run every head, because choosing the move needs every invariant bit, not just "is it nonzero".

The original board is a read-only input during the whole decision. It is not an oracle for the nim-sum: the nim-sum is only obtained by executing the rollouts.

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.ee_spec and Shootout.ee_net: the early-exit classifier, semantically and as a threshold network, decides $[\operatorname{nim}(P)\ne0]$ .
Shootout.ahSel_wins: the all-head controller plus readout wins from every nonzero position against every legal opponent.
Shootout.ahL_counts: the executed all-head path uses one reset tick, exactly the total number of simulated legal moves, and $2B$ further ticks, then one readout.
Shootout.sh_ac0 and Shootout.sh_net: one tick (either schedule) is an AC⁰ formula family of depth at most 34, and a $\{0,1\}$ -weight threshold network family with at most 70 layers.

These are statements about one tick; the number of ticks grows with the board (see Appendix C, paragraph 2).

Coverage record
Paper anchor	`par:shootout-controller-p4` (website anchor; the manuscript has no label here)
Displayed as	Section 5.4, paragraph 4
Claim	The implemented outer controller: early-exit classifier and all-head schedule for move selection
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 678–678; SHA-256 of the normalised block source `f57af1853d04e970…`
Lean declarations	`NimAudit.Shootout.ee_spec` (Shootout, lines 709–733, file `1abd814426d3…`) `NimAudit.Shootout.ee_net` (Shootout, lines 968–972, file `1abd814426d3…`) `NimAudit.Shootout.ahSel_wins` (Shootout, lines 912–915, file `1abd814426d3…`) `NimAudit.Shootout.ahL_counts` (Shootout, lines 1368–1374, file `1abd814426d3…`) `NimAudit.Shootout.sh_ac0` (Shootout, lines 1196–1201, file `1abd814426d3…`) `NimAudit.Shootout.sh_net` (Shootout, lines 1203–1222, file `1abd814426d3…`)
Assumptions and domain	$B\ge1$ , heaps below $2^B$ , head index in $r$ bits with $B\le 2^r$ ; the original board is a read-only input at every tick.
Depends on	Section C, “Outer-controller storage and time”, Proposition 5.9
Audited correspondence rows	`par:shootout-controller`
Explanations	`explain/c-outer-controller`, `formal/c-outer-controller`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

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

theorem `Shootout.ee_net`

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

THE NETWORK-EXECUTED CLASSIFIER and MOVE: the same theorems hold for the threshold network implementation.

Statement as elaborated and printed by Lean 4.26.0

∀ (B N r : ℕ),
  B ≤ 2 ^ r →
    ∀ {P : List ℕ},
      P.length = N →
        NimAudit.Game.Width B P →
          ∀ (x0 : ℕ → Bool),
            NimAudit.Shootout.nimpl true B N r P (NimAudit.Shootout.Tmax B N) x0 (B * N + 3) =
              decide (NimAudit.nimSum P ≠ 0)

Exact source text, lines 968–972

968/-- THE NETWORK-EXECUTED CLASSIFIER and MOVE: the same theorems hold for the threshold969    network implementation. -/970theorem ee_net (B N r : Nat) (hBr : B ≤ 2 ^ r) {P : List Nat} (hP : P.length = N) (hw : Width B P) (x0 : Nat → Bool) :971    nimpl true B N r P (Tmax B N) x0 (B * N + 3) = decide (nimSum P ≠ 0) := by972  rw [nimpl_eq]; exact ee_impl_padded B N r hBr hP hw x0

Project declarations in the statement: Game.Width, Shootout.Tmax, Shootout.nimpl, nimSum

Project declarations used by the proof or definition body

Game.Width, Shootout.Tmax, Shootout.ee_impl_padded, Shootout.impl, Shootout.nimpl, Shootout.nimpl_eq, nimSum

theorem `Shootout.ahSel_wins`

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

WINNING: the implemented all-head controller plus readout wins from every nonzero position against every legal opponent (reusing the whole-game theorem mhExec_wins).

Statement as elaborated and printed by Lean 4.26.0

∀ {B : ℕ} {P : List ℕ},
  NimAudit.Game.Width B P → NimAudit.nimSum P ≠ 0 → NimAudit.Game.Wins (NimAudit.Shootout.ahSel B) P

Exact source text, lines 912–915

912/-- WINNING: the implemented all-head controller plus readout wins from every nonzero913    position against every legal opponent (reusing the whole-game theorem mhExec_wins). -/914theorem ahSel_wins {B : Nat} {P : List Nat} (hw : Width B P) (h : nimSum P ≠ 0) : Wins (ahSel B) P :=915  wins_congr (fun Q hQ => by unfold ahSel mhExecSel; rw [ahMove_eq hQ]) hw (mhExec_wins hw h)

Project declarations in the statement: Game.Width, Game.Wins, Shootout.ahSel, nimSum

Project declarations used by the proof or definition body

Game.Width, RolloutExec.mhExec, RolloutExec.mhExecSel, RolloutExec.mhExec_wins, SelectCircuit.applyM, Shootout.ahMove, Shootout.ahMove_eq, Shootout.ahSel, WholeGame.wins_congr, nimSum

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

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

AC0 FAMILY CERTIFICATE of the outer controller's update (either schedule): depth ≤ 34, input width IW = 2BN + B + r + 5, total size polynomial in IW (uniformly in B and N).

Statement as elaborated and printed by Lean 4.26.0

∀ (early : Bool),
  NimAudit.Family.AC0Fam NimAudit.Family.restAdm NimAudit.Shootout.shLen
    (NimAudit.Shootout.shF early) 34

Exact source text, lines 1196–1201

1196/-- AC0 FAMILY CERTIFICATE of the outer controller's update (either schedule): depth ≤ 34,1197    input width IW = 2BN + B + r + 5, total size polynomial in IW (uniformly in B and N). -/1198theorem sh_ac0 (early : Bool) : AC0Fam restAdm shLen (shF early) 34 := by1199  refine ⟨shLen_pos, fun i _ c hc => (cForms_res early i.1 i.2 (rIdx i.1) c hc).1,1200    fun i _ c hc => (cForms_res early i.1 i.2 (rIdx i.1) c hc).2.2, ?_⟩1201  exact polyIn_mono (fun i _ => shF_tsize early i) (polyE shLen_pos leafS sh_leaves shSizeE _ (fun _ => rfl))

Project declarations in the statement: Family.AC0Fam, Family.restAdm, Shootout.shF, Shootout.shLen

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.depth, AC0.Circ.maxInput, AC0.Circ.size, Family.AC0Fam.mk, Family.polyE, Family.polyIn_mono, Family.restAdm, Family.tsize, Shootout.Fz, Shootout.IW, Shootout.SW, Shootout.cForms_res, Shootout.leafS, Shootout.shF, Shootout.shF_tsize, Shootout.shLen, Shootout.shLen_pos, Shootout.shSizeE, Shootout.sh_leaves, WholeGame.rIdx

theorem `Shootout.sh_net`

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

NETWORK FAMILY CERTIFICATE: W = 1 (weights and thresholds in {0,1}), ≤ 70 layers, polynomial widths, fan-ins and gate count; the network's outputs are the formulas.

Statement as elaborated and printed by Lean 4.26.0

∀ (early : Bool),
  NimAudit.Family.NetFam NimAudit.Family.restAdm NimAudit.Shootout.shLen
    (NimAudit.Shootout.shN early) 1 70

Exact source text, lines 1203–1222

1203/-- NETWORK FAMILY CERTIFICATE: W = 1 (weights and thresholds in {0,1}), ≤ 70 layers,1204    polynomial widths, fan-ins and gate count; the network's outputs are the formulas. -/1205theorem sh_net (early : Bool) : NetFam restAdm shLen (shN early) 1 70 := by1206  have spec := fun i => compileF_spec (shF early i) (shLen i) 341207    (fun c hc => (cForms_res early i.1 i.2 (rIdx i.1) c hc).2.2) (fun c hc => (cForms_res early i.1 i.2 (rIdx i.1) c hc).1)1208  have hT := polyE shLen_pos leafS sh_leaves shSizeE1209    (fun i => SW i.1 i.2 (rIdx i.1) * Fz i.1 i.2 (rIdx i.1)) (fun _ => rfl)1210  refine ⟨shLen_pos, fun i _ => (spec i).2.2.1, fun i _ => (spec i).2.2.2.1, fun i _ => (spec i).2.2.2.2.1, ?_, ?_⟩1211  · obtain ⟨c, k, h⟩ := polyIn_add shLen_pos hT (polyIn_leaf (fun i _ => Nat.le_refl (shLen i)))1212    refine ⟨c, k, fun i hi => netBounded_mono (spec i).2.2.2.2.2.1 ?_⟩1213    have := shF_tsize early i; have := h i hi; dsimp only at *; unfold tsize at *; omega1214  · have h2 := polyIn_add shLen_pos (polyIn_mul (polyIn_const _ _ (2 * 34 + 1)) hT)1215      (polyE shLen_pos leafS sh_leaves (vB * vN + 4 + vRB + vB) (fun i => SW i.1 i.2 (rIdx i.1)) (fun _ => rfl))1216    refine polyIn_mono (fun i _ => ?_) h21217    have g := (spec i).2.2.2.2.2.21218    have := Nat.mul_le_mul_left (2 * 34 + 1) (shF_tsize early i)1219    have hl : (shF early i).length = SW i.1 i.2 (rIdx i.1) := by unfold shF; rw [cForms_length]1220    unfold tsize at this; rw [hl] at g1221    show gateCount (cNet early i.1 i.2 (rIdx i.1)) ≤ _1222    exact Nat.le_trans g (by omega)

Project declarations in the statement: Family.NetFam, Family.restAdm, Shootout.shLen, Shootout.shN

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.depth, AC0.Circ.eval, AC0.Circ.maxInput, AC0.Circ.size, AC0.Layer, AC0.NetBounded, AC0.NetValid, AC0.evalNet, Family.NetFam.mk, Family.PE, Family.PolyIn, Family.instAddPE, Family.instMulPE, Family.instOfNatPE, Family.netBounded_mono, Family.polyE, Family.polyIn_add, Family.polyIn_const, Family.polyIn_leaf, Family.polyIn_mono, Family.polyIn_mul, Family.restAdm, Family.tsize, Family.vB, Family.vN, FiniteNet.Wired, Shootout.Fz, Shootout.IW, Shootout.SW, Shootout.cForms, Shootout.cForms_length, Shootout.cForms_res, Shootout.cNet, Shootout.leafS, Shootout.shF, Shootout.shF_tsize, Shootout.shLen, Shootout.shLen_pos, Shootout.shN, Shootout.shSizeE, Shootout.sh_leaves, Shootout.vRB, ThresholdNet.compileF, ThresholdNet.compileF_spec, ThresholdNet.gateCount, WholeGame.rIdx

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

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

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

Statement as elaborated and printed by Lean 4.26.0

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

Exact source text, lines 956–957

956def nimpl (early : Bool) (B N r : Nat) (P : List Nat) (T : Nat) (x0 : Nat → Bool) : Nat → Bool :=957  nrun early B N r P T (nstep early B N r P true x0)

Project declarations in the statement: none

Project declarations used by the proof or definition body

Shootout.nrun, Shootout.nstep

inductive `Game.Wins`

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

`Wins sel p`: the player to move at `p`, always playing the successor chosen by `sel`, wins against EVERY legal opponent. The selected move is legal, and after every legal opponent reply the player is again in a `Wins` position. Because the predicate is inductive, every such play is finite and ends with the opponent facing a terminal board (normal play: the opponent loses).

Statement as elaborated and printed by Lean 4.26.0

(List ℕ → Option (List ℕ)) → List ℕ → Prop

Exact source text, lines 125–132

125/-- `Wins sel p`: the player to move at `p`, always playing the successor chosen by126    `sel`, wins against EVERY legal opponent.  The selected move is legal, and after127    every legal opponent reply the player is again in a `Wins` position.  Because128    the predicate is inductive, every such play is finite and ends with the129    opponent facing a terminal board (normal play: the opponent loses). -/130inductive Wins (sel : List Nat → Option (List Nat)) : List Nat → Prop131  | intro (p q : List Nat) : sel p = some q → Move p q →132      (∀ r, Move q r → Wins sel r) → Wins sel p

Project declarations in the statement: none

Project declarations used by the proof or definition body

Game.Move

def `Shootout.ahSel`

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

Statement as elaborated and printed by Lean 4.26.0

ℕ → List ℕ → Option (List ℕ)

Exact source text, lines 890–890

890def ahSel (B : Nat) (P : List Nat) : Option (List Nat) := applyM P (ahMove B P)

Project declarations in the statement: none

Project declarations used by the proof or definition body

SelectCircuit.applyM, Shootout.ahMove

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

inductive `Family.AC0Fam`

Module Family (lean/phase6/Family.lean, lines 126–134) · file SHA-256 7a647f0a667d5ede…

AC0 FAMILY CERTIFICATE (nonuniform, multi-output). For every admissible member: the input length is positive, every output formula has depth ≤ d and reads only the first len inputs, and the total size of the outputs is ≤ c·len^k with c, k independent of the member.

Statement as elaborated and printed by Lean 4.26.0

{ι : Type} → (ι → Prop) → (ι → ℕ) → (ι → List NimAudit.AC0.Circ) → ℕ → Prop

Exact source text, lines 126–134

126/-- AC0 FAMILY CERTIFICATE (nonuniform, multi-output).  For every admissible member:127    the input length is positive, every output formula has depth ≤ d and reads only128    the first len inputs, and the total size of the outputs is ≤ c·len^k with c, k129    independent of the member. -/130structure AC0Fam {ι : Type} (adm : ι → Prop) (len : ι → Nat) (outs : ι → List Circ) (d : Nat) : Prop where131  pos : ∀ i, adm i → 1 ≤ len i132  depth_le : ∀ i, adm i → ∀ c ∈ outs i, depth c ≤ d133  reads : ∀ i, adm i → ∀ c ∈ outs i, maxInput c ≤ len i134  size_poly : PolyIn adm len (fun i => tsize (outs i))

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.depth, AC0.Circ.maxInput, Family.PolyIn, Family.tsize

def `Family.restAdm`

Module Family (lean/phase6/Family.lean, lines 282–282) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → Prop

Exact source text, lines 282–282

282def restAdm : Nat × Nat → Prop := fun i => 1 ≤ i.1 ∧ 1 ≤ i.2

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Shootout.shF`

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

Statement as elaborated and printed by Lean 4.26.0

Bool → ℕ × ℕ → List NimAudit.AC0.Circ

Exact source text, lines 1162–1162

1162def shF (early : Bool) (i : Nat × Nat) : List Circ := cForms early i.1 i.2 (rIdx i.1)

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

Shootout.cForms, WholeGame.rIdx

def `Shootout.shLen`

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

Input width of one update of the (B, N) controller (registers, reset, board).

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → ℕ

Exact source text, lines 1160–1161

1160/-- Input width of one update of the (B, N) controller (registers, reset, board). -/1161def shLen (i : Nat × Nat) : Nat := IW i.1 i.2 (rIdx i.1)

Project declarations in the statement: none

Project declarations used by the proof or definition body

Shootout.IW, WholeGame.rIdx

inductive `Family.NetFam`

Module Family (lean/phase6/Family.lean, lines 141–149) · file SHA-256 7a647f0a667d5ede…

NETWORK FAMILY CERTIFICATE: fixed grid W, at most L layers, valid gates, first layer reading only the len inputs, polynomial widths/fan-ins and polynomial gate count.

Statement as elaborated and printed by Lean 4.26.0

{ι : Type} → (ι → Prop) → (ι → ℕ) → (ι → List NimAudit.AC0.Layer) → ℕ → ℕ → Prop

Exact source text, lines 141–149

141/-- NETWORK FAMILY CERTIFICATE: fixed grid W, at most L layers, valid gates, first layer142    reading only the len inputs, polynomial widths/fan-ins and polynomial gate count. -/143structure NetFam {ι : Type} (adm : ι → Prop) (len : ι → Nat) (net : ι → List Layer) (W L : Nat) : Prop where144  pos : ∀ i, adm i → 1 ≤ len i145  valid : ∀ i, adm i → NetValid W (net i)146  wired : ∀ i, adm i → Wired (len i) (net i)147  layers : ∀ i, adm i → (net i).length ≤ L148  bounded : ∃ c k, ∀ i, adm i → NetBounded (c * len i ^ k) (net i)149  gates : PolyIn adm len (fun i => gateCount (net i))

Project declarations in the statement: AC0.Layer

Project declarations used by the proof or definition body

AC0.Layer, AC0.NetBounded, AC0.NetValid, Family.PolyIn, FiniteNet.Wired, ThresholdNet.gateCount

def `Shootout.shN`

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

Statement as elaborated and printed by Lean 4.26.0

Bool → ℕ × ℕ → List NimAudit.AC0.Layer

Exact source text, lines 1163–1163

1163def shN (early : Bool) (i : Nat × Nat) : List Layer := cNet early i.1 i.2 (rIdx i.1)

Project declarations in the statement: AC0.Layer

Project declarations used by the proof or definition body

Shootout.cNet, WholeGame.rIdx

Full modules

Module	File	Lines	Imports
Family	`lean/phase6/Family.lean`	574	WholeGame
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, paragraph 4The implemented outer controller: early-exit classifier and all-head schedule for move selection

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

theorem Shootout.ee_net

theorem Shootout.ahSel_wins

theorem Shootout.ahL_counts

theorem Shootout.sh_ac0

theorem Shootout.sh_net

Definitions these statements use

def Game.Width

def Game.rolloutWinner

def Misc.FSM.run

def Misc.shootout

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

def nimSum

def Shootout.nimpl

inductive Game.Wins

def Shootout.ahSel

def Game.totalRolloutMoves

def Shootout.cstep

def Shootout.loopRun

inductive Family.AC0Fam

def Family.restAdm

def Shootout.shF

def Shootout.shLen

inductive Family.NetFam

def Shootout.shN

Full modules

theorem `Shootout.ee_spec`

theorem `Shootout.ee_net`

theorem `Shootout.ahSel_wins`

theorem `Shootout.ahL_counts`

theorem `Shootout.sh_ac0`

theorem `Shootout.sh_net`

def `Game.Width`

def `Game.rolloutWinner`

def `Misc.FSM.run`

def `Misc.shootout`

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`

def `nimSum`

def `Shootout.nimpl`

inductive `Game.Wins`

def `Shootout.ahSel`

def `Game.totalRolloutMoves`

def `Shootout.cstep`

def `Shootout.loopRun`

inductive `Family.AC0Fam`

def `Family.restAdm`

def `Shootout.shF`

def `Shootout.shLen`

inductive `Family.NetFam`

def `Shootout.shN`