Section C, “Outer-controller storage and time”Shootout controller: NB+4+r+B state bits plus the read-only original board

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

1 Paper text

Outer-controller storage and time. For $B,N\ge1$ and $B\le2^r$ , the shootout controller uses $NB+4+r+B$ state bits: a working board, control flags, a head index and the collected outcomes. Its input also contains the original $NB$ -bit board, held fixed throughout the decision. This external storage is additional to the state count. The circuit handles head selection, board reload, outcome collection, increment and halt; the depth bound in the table applies to either the early-exit classifier or the all-head schedule.

Generated from paper_jmlr.tex, lines 1552–1554.

2 Explain this

The shootout controller's memory: a working copy of the board, a few control flags, a head index of $r$ bits and the $B$ collected outcomes, $NB+4+r+B$ state bits in all (for $B,N\ge1$ , $B\le2^r$ ). In addition, the original $NB$ -bit board is an input held fixed for the whole decision; it is counted separately, not as state. One circuit handles head selection, board reload, outcome collection, increment and halting; the table's depth bound covers both schedules.

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

The register layout is Shootout.enc, and one tick reads $IW=2BN+B+r+5$ input wires (Shootout.IW): the $NB+4+r+B$ register bits, a reset bit and the $NB$ bits of the original board. Shootout.sh_ac0 and Shootout.sh_net certify one tick for either schedule; Shootout.ee_spec (early exit) and Shootout.ahSel_wins (all heads) give the semantics.

Coverage record
Paper anchor	`par:controller-costs` (manuscript label)
Displayed as	Section C, “Outer-controller storage and time”
Claim	Shootout controller: NB+4+r+B state bits plus the read-only original board
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 1552–1554; SHA-256 of the normalised block source `739b9626e71ac7a8…`
Lean declarations	`NimAudit.Shootout.sh_ac0` (Shootout, lines 1196–1201, file `1abd814426d3…`) `NimAudit.Shootout.sh_net` (Shootout, lines 1203–1222, file `1abd814426d3…`) `NimAudit.Shootout.ee_spec` (Shootout, lines 709–733, file `1abd814426d3…`) `NimAudit.Shootout.ahSel_wins` (Shootout, lines 912–915, file `1abd814426d3…`)
Prose-to-formal notes	The certified input width of one tick is $IW=2BN+B+r+5$ : the $NB+4+r+B$ register bits, one reset bit and the $NB$ bits of the original board, which is held fixed.
Audited correspondence rows	`par:controller-costs`
Explanations	`explain/par:controller-costs`, `formal/par:controller-costs`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

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

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

Definitions these statements use

def `Shootout.enc`

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

Register encoding: rollout registers (wires < BN+2), run (BN+2), dec (BN+3), head index bits (BN+4 …), stored outcomes (BN+4+r …); zero beyond SW.

Statement as elaborated and printed by Lean 4.26.0

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

Exact source text, lines 74–82

74/-- Register encoding: rollout registers (wires < BN+2), run (BN+2), dec (BN+3), head index75    bits (BN+4 …), stored outcomes (BN+4+r …); zero beyond SW. -/76def enc (B N r : Nat) (s : OS) : Nat → Bool := fun w =>77  if w < B * N + 2 then rsBits B N s.rs w78  else if w = B * N + 2 then s.run79  else if w = B * N + 3 then s.dec80  else if w < B * N + 4 + r then s.j.testBit (w - (B * N + 4))81  else if w < SW B N r then s.outs (w - (B * N + 4 + r))82  else false

Project declarations in the statement: Shootout.OS

Project declarations used by the proof or definition body

RolloutExec.rsBits, Shootout.OS, Shootout.OS.dec, Shootout.OS.j, Shootout.OS.outs, Shootout.OS.rs, Shootout.OS.run, Shootout.SW

def `Shootout.IW`

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

Total input width of one update.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → ℕ → ℕ

Exact source text, lines 88–89

88/-- Total input width of one update. -/89def IW (B N r : Nat) : Nat := SW B N r + 1 + B * N

Project declarations in the statement: none

Project declarations used by the proof or definition body

Shootout.SW

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

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

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

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 C, “Outer-controller storage and time”Shootout controller: NB+4+r+B state bits plus the read-only original board

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

theorem Shootout.sh_net

theorem Shootout.ee_spec

theorem Shootout.ahSel_wins

Definitions these statements use

def Shootout.enc

def Shootout.IW

inductive Family.AC0Fam

def Family.restAdm

def Shootout.shF

def Shootout.shLen

inductive Family.NetFam

def Shootout.shN

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

inductive Game.Wins

def Shootout.ahSel

Full modules

theorem `Shootout.sh_ac0`

theorem `Shootout.sh_net`

theorem `Shootout.ee_spec`

theorem `Shootout.ahSel_wins`

def `Shootout.enc`

def `Shootout.IW`

inductive `Family.AC0Fam`

def `Family.restAdm`

def `Shootout.shF`

def `Shootout.shLen`

inductive `Family.NetFam`

def `Shootout.shN`

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`

inductive `Game.Wins`

def `Shootout.ahSel`