NIM paper · interactive edition Interactive edition · paper, explanations and Lean proofs.

Section 5.5, “From a summary to a move”Board-storage variant: NB+B+r state bits, N+1 updates per decision, plus a reset

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

1 Paper text

From a summary to a move. Computing σt\sigma_t does not by itself retain the heap rows needed to choose a move. One implementation replays the current position after the first scan. If σt≠0\sigma_t\ne0, select the first row ii for which xt,i′=xt,i⊕σt<xt,i.x_{t,i}'=x_{t,i}\oplus\sigma_t<x_{t,i}. Such a row exists: choose a heap containing the highest set bit of σt\sigma_t. Replacing that heap by xt,i′x_{t,i}' leaves nim-sum zero. XOR, binary comparison and conditional selection are constant-depth operations; the replay uses O(B+log⁡N)O(B+\log N) state bits to retain the summary, a selected move and its row index. The explicit protocol is rows(Pt), SEP, rows(Pt), SEP.\mathtt{rows}(P_t),\ \mathtt{SEP},\ \mathtt{rows}(P_t),\ \mathtt{SEP}. The first separator stores the summary and switches to replay; the second emits the move and returns to scan mode. This takes exactly 2N+22N+2 updates, with one additional reset token at the start of a game. If σt=0\sigma_t=0, choose the first nonempty heap and decrement it, or report termination when all heaps are empty. Lean verifies the complete replay controller, including its binary move output and its fixed-scale threshold implementation. With an rr-bit counter satisfying N<2rN<2^r, its state uses 4+5B+3r4+5B+3r bits. The strict inequality allows the counter to hold the end value NN, whereas an output index alone only needs N≤2rN\le2^r. Alternatively, store the current board in O(NB)O(NB) bits during the initial scan and use a constant-depth selector at the separator, as in Appendix C. This avoids replay at the cost of board-sized memory. The distinction matters for a stream in which each position is supplied only once. Both variants have checked bit-level circuits, fixed-scale network implementations and winning-play guarantees. The board-storage variant uses NB+B+rNB+B+r state bits and N+1N+1 updates per decision, with N<2rN<2^r, plus a reset update when initialising the controller.

Generated from paper_jmlr.tex, lines 850–860.

2 Explain this

The alternative stores the board while scanning it once: each row is written into an NBNB-bit board register as it arrives, and at the separator a constant-depth selector picks the move from the stored board and the accumulated nim-sum.

Trade-off. N+1N+1 updates per decision instead of 2N+22N+2, and no replay, but NB+B+rNB+B+r state bits instead of O(B+log⁡N)O(B+\log N). This matters for streams where each position is supplied only once.

Row-wise recurrence: registers, separators and replay

Exact construction trace Every value is computed from the construction’s definitions for the example shown.

The board arrives as a stream of rows, one heap per token, with separators (SEP) between positions and a reset at the start of a game. Step through the replay controller: in scan mode it XORs each row into the accumulator; the first separator outputs the summary, stores it and switches to replay mode; during replay the same rows arrive again and each is tested against the stored summary, keeping the first cancelling candidate and a fallback; the second separator outputs the move. The board-storage variant instead writes the rows into memory and chooses the move at its single separator. In the replay controller a separator clears the accumulator and keeps the summary of the position just completed, with its validity bit; an extra separator is read as an empty position, whose summary is 0. Only a reset returns every register, validity included, to its initial value. The board-storage separator clears its accumulator and pointer and keeps the stored board. The third protocol shows the summary mechanism of Proposition 5.13 alone: it reports summaries and differences but chooses no move.

The current NIM board already determines optimal play. The memory shown here makes that answer computationally accessible by retaining partial results across rows; an earlier game position is needed only for the optional comparison of consecutive positions.

  1. RESETreset
  2. row 3store
  3. row 4store
  4. row 6store
  5. SEPmove

5 / 5 SEP: separator: select the move from the stored board with target acc; clear acc and pointer

Registers after this update

stored board
(3, 4, 6)
accumulator
0 000
write pointer
0

Outputs so far

  • after token 5: summary σ = 1, move heap 0 → 2

Counting the work

  • One decision on 3 heaps takes N + 1 = 4 updates: one pass over the rows and a separator. The price is storing the whole board: NB + B + r bits; here 14 bits.
  • Each single update is a shallow circuit (board storage: state updates of Boolean depth ≤ 8, outputs ≤ 16; ≤ 34 threshold layers). The number of sequential updates grows with N. That no shallow family computes the complete board-to-move map is a separate statement, conditional on the named classical input that parity is not in AC0.
All 5 updates as a table
#TokenRegisters afterOutput
1RESETboard (0, 0, 0), acc 0, ptr 0
2row 3board (3, 0, 0), acc 3, ptr 1
3row 4board (3, 4, 0), acc 7, ptr 2
4row 6board (3, 4, 6), acc 1, ptr 3
5SEPboard (3, 4, 6), acc 0, ptr 0σ = 1, move heap 0 → 2

How this relates to the Lean proof. Each update is one step of Controller.cstep (replay) or BoardStore.bsStep (board storage) on the token streams Controller.dtoks and BoardStore.btoks. The whole-game theorems WholeGame.replay_wins and BoardStore.bits_store_wins prove that, from every board with nonzero nim-sum, iterating these updates wins against every legal opponent. The summary mechanism is Recurrent.step. The comparison of decision-time boards with the post-move board is Bypass.diff_with_postMove and Bypass.diff_decision_only.

What this does not show. Each single update is shallow; the number of updates per decision (2N+22N+2, or N+1N+1 with board storage) grows with the board. That no shallow family computes the complete board-to-move map is a separate statement, conditional on the named classical input that parity is not in AC0\mathrm{AC}^0. The edge cases (an extra separator, a reset) lie outside the protocol streams that the theorems quantify over; the update rule is simply applied. The recurrent strategies are proved in their own stateful game semantics; connecting them to the later history model of weak mastery is a separate adapter that has not been built (coverage record). No recurrent network was trained.

Depicted in Lean: Controller.cstep, Controller.dtoks, Recurrent.replayStep, Recurrent.step, Recurrent.sep_resets, ControllerBits.bstep_reset, BoardStore.bsStep, BoardStore.btoks, Controller.crun_decision, Controller.stream_fits, WholeGame.replay_wins, BoardStore.bits_store_wins, Bypass.diff_with_postMove, Bypass.diff_decision_only, Recurrent.circuit_resources, BoardStore.bsForms_res, BoardStore.bsOuts_res, BoardStore.bs_net.

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 566 reference cases. The comparison compares every register and output after every token.

3 How this is formalised

Coverage record
Paper anchorc-board-storage (website anchor; the manuscript has no label here)
Displayed asSection 5.5, “From a summary to a move”
ClaimBoard-storage variant: NB+B+r state bits, N+1 updates per decision, plus a reset
Coverage categoryChecked theorem
Statement sourcepaper_jmlr.tex lines 850–860; SHA-256 of the normalised block source 96c224147ee6fabe…
Lean declarations
Assumptions and domain

N<2rN<2^r; heaps below 2B2^B; each position is supplied once.

Depends onProposition 5.13
Audited correspondence rowsprop:bypass-interfaces
Explanationsexplain/c-board-storage, formal/c-board-storage
Build evidencefresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem BoardStore.bs_decision

Module BoardStore (lean/phase6/BoardStore.lean, lines 99–105) · file SHA-256 c35ac76d5db6e833… Axioms reported by the fresh build: propext, Quot.sound

ONE DECISION: from any idle state whose board has N slots, rows(P), SEP stores P, reports nim(P) and the winning-move selector's move, and returns to idle.

Statement as elaborated and printed by Lean 4.26.0

∀ {N : ℕ} (b : List ℕ),
  b.length = N →
    ∀ (P : List ℕ),
      P.length = N →
        NimAudit.BoardStore.bsRun N { board := b, acc := 0, idx := 0 }
            (NimAudit.BoardStore.btoks P) =
          ({ board := P, acc := 0, idx := 0 },
            [{ sum := NimAudit.nimSum P, move := NimAudit.Controller.decisionMove P }])
Exact source text, lines 99–105
99/-- ONE DECISION: from any idle state whose board has N slots, rows(P), SEP stores P,100    reports nim(P) and the winning-move selector's move, and returns to idle. -/101theorem bs_decision {N : Nat} (b : List Nat) (hb : b.length = N) (P : List Nat) (hP : P.length = N) :102    bsRun N ⟨b, 0, 0⟩ (btoks P) = (⟨P, 0, 0⟩, [⟨nimSum P, decisionMove P⟩]) := by103  unfold btoks104  rw [bsRun_append, bsRun_rows N P b 0 0, writes_eq P b 0 (by omega)]105  simp [bsRun, bsStep, attainT_eq_replayMove, decisionMove]

Project declarations in the statement: BoardStore.BOut, BoardStore.BOut.mk, BoardStore.BS, BoardStore.BS.mk, BoardStore.bsRun, BoardStore.btoks, Controller.decisionMove, nimSum

Project declarations used by the proof or definition body

AttainCircuit.attainT, BoardStore.BOut, BoardStore.BOut.mk, BoardStore.BS, BoardStore.BS.mk, BoardStore.bsRun, BoardStore.bsRun_append, BoardStore.bsRun_rows, BoardStore.btoks, BoardStore.writes, BoardStore.writes_eq, Controller.Tok, Controller.Tok.row, Controller.Tok.sep, Controller.decisionMove, Recurrent.replayMove, SelectCircuit.attainT_eq_replayMove, nimSum

theorem BoardStore.bits_decision

Module BoardStore (lean/phase6/BoardStore.lean, lines 460–479) · file SHA-256 c35ac76d5db6e833… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

BIT-LEVEL DECISION THEOREM: from the encoding of any idle state with N slots, the N row updates and the separator update produce the encoding of the idle state storing P, and the outputs at the separator decode to (nim(P), decisionMove P).

Statement as elaborated and printed by Lean 4.26.0

∀ {B N r r' : ℕ},
  N < 2 ^ r →
    N ≤ 2 ^ r' →
      ∀ (b : List ℕ),
        b.length = N →
          NimAudit.Game.Width B b →
            ∀ (P : List ℕ),
              P.length = N →
                NimAudit.Game.Width B P →
                  NimAudit.BoardStore.bsBitRun B N r
                        (NimAudit.BoardStore.bsBits B N r { board := b, acc := 0, idx := 0 })
                        (NimAudit.BoardStore.btoks P) =
                      NimAudit.BoardStore.bsBits B N r { board := P, acc := 0, idx := 0 } ∧
                    NimAudit.BoardStore.bsDecode B N r r'
                        (NimAudit.BoardStore.inB B N r
                          (NimAudit.BoardStore.bsBitRun B N r
                            (NimAudit.BoardStore.bsBits B N r { board := b, acc := 0, idx := 0 })
                            (List.map NimAudit.Controller.Tok.row P))
                          NimAudit.Controller.Tok.sep) =
                      some { sum := NimAudit.nimSum P, move := NimAudit.Controller.decisionMove P }
Exact source text, lines 460–479
460/-- BIT-LEVEL DECISION THEOREM: from the encoding of any idle state with N slots, the461    N row updates and the separator update produce the encoding of the idle state storing462    P, and the outputs at the separator decode to (nim(P), decisionMove P). -/463theorem bits_decision {B N r r' : Nat} (hN : N < 2 ^ r) (hr' : N ≤ 2 ^ r') (b : List Nat) (hb : b.length = N)464    (hwb : Width B b) (P : List Nat) (hP : P.length = N) (hw : Width B P) :465    bsBitRun B N r (bsBits B N r ⟨b, 0, 0⟩) (btoks P) = bsBits B N r ⟨P, 0, 0⟩ ∧466    bsDecode B N r r' (inB B N r (bsBitRun B N r (bsBits B N r ⟨b, 0, 0⟩) (P.map Tok.row)) Tok.sep) =467      some ⟨nimSum P, decisionMove P⟩ := by468  have hf0 : FitsB B N r ⟨b, 0, 0⟩ := ⟨hb, hwb, Nat.two_pow_pos B, Nat.zero_le _, hN⟩469  obtain ⟨h1, h2⟩ := bits_rows P b 0 0 hf0 hw (by omega)470  rw [writes_eq P b 0 (by omega), Nat.zero_xor, Nat.zero_add] at h1 h2471  simp only [List.take_zero, List.nil_append] at h1 h2472  constructor473  · unfold btoks474    rw [bsBitRun_append, h1]475    simp only [bsBitRun]476    rw [bsBitStep_spec _ h2 Tok.sep (fun _ h => by cases h)]477    simp [bsStep]478  · rw [h1, bsDecode_sep hr' _ h2]479    simp [bsStep, attainT_eq_replayMove, decisionMove]

Project declarations in the statement: BoardStore.BOut, BoardStore.BOut.mk, BoardStore.BS.mk, BoardStore.bsBitRun, BoardStore.bsBits, BoardStore.bsDecode, BoardStore.btoks, BoardStore.inB, Controller.Tok, Controller.Tok.row, Controller.Tok.sep, Controller.decisionMove, Game.Width, nimSum

Project declarations used by the proof or definition body

AttainCircuit.attainT, BoardStore.BOut, BoardStore.BOut.mk, BoardStore.BS, BoardStore.BS.idx, BoardStore.BS.mk, BoardStore.FitsB, BoardStore.FitsB.mk, BoardStore.bits_rows, BoardStore.bsBitRun, BoardStore.bsBitRun_append, BoardStore.bsBitStep, BoardStore.bsBitStep_spec, BoardStore.bsBits, BoardStore.bsDecode, BoardStore.bsDecode_sep, BoardStore.bsStep, BoardStore.btoks, BoardStore.inB, BoardStore.writes, BoardStore.writes_eq, Controller.Tok, Controller.Tok.casesOn, Controller.Tok.row, Controller.Tok.sep, Controller.decisionMove, Game.Width, Recurrent.replayMove, SelectCircuit.attainT_eq_replayMove, nimSum

theorem BoardStore.bits_store_wins

Module BoardStore (lean/phase6/BoardStore.lean, lines 527–546) · file SHA-256 c35ac76d5db6e833… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

BIT-LEVEL WHOLE-GAME THEOREM: with N < 2^r and N ≤ 2^r', from the encoding of any idle state storing a width-B board of N slots, the one-pass bit-level machine wins from every nonzero board of width B against every legal opponent.

Statement as elaborated and printed by Lean 4.26.0

∀ {B N r r' : ℕ},
  N < 2 ^ r →
    N ≤ 2 ^ r' →
      ∀ (P : List ℕ),
        P.length = N →
          NimAudit.Game.Width B P →
            NimAudit.nimSum P ≠ 0 →
              ∀ (b : List ℕ),
                b.length = N →
                  NimAudit.Game.Width B b →
                    NimAudit.BoardStore.BitStoreWins B N r r'
                      (NimAudit.BoardStore.bsBits B N r { board := b, acc := 0, idx := 0 }) P
Exact source text, lines 527–546
527/-- BIT-LEVEL WHOLE-GAME THEOREM: with N < 2^r and N ≤ 2^r', from the encoding of any idle528    state storing a width-B board of N slots, the one-pass bit-level machine wins from every529    nonzero board of width B against every legal opponent. -/530theorem bits_store_wins {B N r r' : Nat} (hN : N < 2 ^ r) (hr' : N ≤ 2 ^ r') :531    ∀ (P : List Nat), P.length = N → Width B P → nimSum P ≠ 0 →532    ∀ b, b.length = N → Width B b → BitStoreWins B N r r' (bsBits B N r ⟨b, 0, 0⟩) P := by533  intro P534  induction P using (measure List.sum).wf.induction with535  | h P ih =>536    intro hP hw h0 b hb hwb537    obtain ⟨h1, h2⟩ := bits_decision (r' := r') hN hr' b hb hwb P hP hw538    obtain ⟨i, v, hd, hz⟩ := (decision_correct P).2.2 h0539    obtain ⟨x, _, _, hmv⟩ := (decision_correct P).2.1 i v hd540    refine BitStoreWins.intro _ P (P.set i v) ?_ hmv h1 ?_541    · unfold bitMove; rw [h2]; simp [hd, applyM]542    · intro P' hm'543      have hlt1 := move_sum_lt hmv544      have hlt2 := move_sum_lt hm'545      exact ih P' (by show P'.sum < P.sum; omega) (by rw [move_length hm', move_length hmv, hP])546        (width_move (width_move hw hmv) hm') (move_from_zero hm' hz) P hP hw

Project declarations in the statement: BoardStore.BS.mk, BoardStore.BitStoreWins, BoardStore.bsBits, Game.Width, nimSum

Project declarations used by the proof or definition body

BoardStore.BOut, BoardStore.BOut.mk, BoardStore.BOut.move, BoardStore.BS.mk, BoardStore.BitStoreWins, BoardStore.BitStoreWins.intro, BoardStore.bitMove, BoardStore.bits_decision, BoardStore.bsBitRun, BoardStore.bsBits, BoardStore.bsDecode, BoardStore.btoks, BoardStore.inB, Controller.Tok, Controller.Tok.row, Controller.Tok.sep, Controller.decisionMove, Controller.decision_correct, Game.Move, Game.Terminal, Game.Width, Game.move_from_zero, Game.move_sum_lt, Game.width_move, SelectCircuit.applyM, WholeGame.move_length, nimSum

theorem BoardStore.bs_counts

Module BoardStore (lean/phase6/BoardStore.lean, lines 503–506) · file SHA-256 c35ac76d5db6e833… Axioms reported by the fresh build: propext, Quot.sound

Memory and update counts: B·N + B + r state bits; N + 1 updates per decision.

Statement as elaborated and printed by Lean 4.26.0

∀ (B N r : ℕ) (P : List ℕ),
  P.length = N →
    NimAudit.BoardStore.sw B N r = B * N + B + r ∧
      (NimAudit.BoardStore.btoks P).length = N + 1 ∧
        (NimAudit.BoardStore.bsForms B N r).length = NimAudit.BoardStore.sw B N r
Exact source text, lines 503–506
503/-- Memory and update counts: B·N + B + r state bits; N + 1 updates per decision. -/504theorem bs_counts (B N r : Nat) (P : List Nat) (hP : P.length = N) :505    sw B N r = B * N + B + r ∧ (btoks P).length = N + 1 ∧ (bsForms B N r).length = sw B N r :=506  ⟨rfl, by rw [btoks_length, hP], bsForms_length B N r⟩

Project declarations in the statement: AC0.Circ, BoardStore.bsForms, BoardStore.btoks, BoardStore.sw, Controller.Tok

Project declarations used by the proof or definition body

AC0.Circ, BoardStore.bsForms, BoardStore.bsForms_length, BoardStore.btoks, BoardStore.btoks_length, BoardStore.sw, Controller.Tok

theorem BoardStore.bs_ac0

Module BoardStore (lean/phase6/BoardStore.lean, lines 700–711) · file SHA-256 c35ac76d5db6e833… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

BOARD-STORAGE FAMILY CERTIFICATE: update and output formulas together have depth ≤ 16, read only the registers and one token, and have total size polynomial in that width.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Family.AC0Fam NimAudit.Family.restAdm NimAudit.BoardStore.bsLen NimAudit.BoardStore.bsAll
  16
Exact source text, lines 700–711
700/-- BOARD-STORAGE FAMILY CERTIFICATE: update and output formulas together have depth ≤ 16,701    read only the registers and one token, and have total size polynomial in that width. -/702theorem bs_ac0 : AC0Fam restAdm bsLen bsAll 16 := by703  refine ⟨bsLen_pos, fun i _ c hc => ?_, fun i _ c hc => ?_, ?_⟩704  · rcases List.mem_append.mp hc with h | h705    · have := (bsForms_res _ _ _ c h).1; omega706    · exact (bsOuts_res (rIdx_width i.2) c h).1707  · rcases List.mem_append.mp hc with h | h708    · exact (bsForms_res _ _ _ c h).2.2709    · exact (bsOuts_res (rIdx_width i.2) c h).2.2710  · exact polyIn_mono (fun i _ => bsAll_tsize i)711      (polyE bsLen_pos leafBN bs_leaves bsSizeE _ (fun i => (bsSizeE_eval i).symm))

Project declarations in the statement: BoardStore.bsAll, BoardStore.bsLen, Family.AC0Fam, Family.restAdm

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.depth, AC0.Circ.maxInput, AC0.Circ.size, BoardStore.bsAll, BoardStore.bsAll_tsize, BoardStore.bsForms, BoardStore.bsForms_res, BoardStore.bsLen, BoardStore.bsLen_pos, BoardStore.bsOuts, BoardStore.bsOuts_res, BoardStore.bsSizeE, BoardStore.bsSizeE_eval, BoardStore.bs_leaves, BoardStore.sw, BoardStore.varSz, Family.AC0Fam.mk, Family.PE.eval, Family.leafBN, Family.polyE, Family.polyIn_mono, Family.rIdx_width, Family.restAdm, Family.tsize, WholeGame.rIdx

theorem BoardStore.bs_net

Module BoardStore (lean/phase6/BoardStore.lean, lines 753–775) · file SHA-256 c35ac76d5db6e833… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

BOARD-STORAGE NETWORK CERTIFICATE (W = 1, ≤ 34 layers).

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Family.NetFam NimAudit.Family.restAdm NimAudit.BoardStore.bsLen NimAudit.BoardStore.bsNet 1
  34
Exact source text, lines 753–775
753/-- BOARD-STORAGE NETWORK CERTIFICATE (W = 1, ≤ 34 layers). -/754theorem bs_net : NetFam restAdm bsLen bsNet 1 34 := by755  have spec := fun i => compileF_spec (bsAll i) (bsLen i) 16756    (fun c hc => by757      rcases List.mem_append.mp hc with h | h758      · exact (bsForms_res _ _ _ c h).2.2759      · exact (bsOuts_res (rIdx_width i.2) c h).2.2)760    (fun c hc => by761      rcases List.mem_append.mp hc with h | h762      · have := (bsForms_res _ _ _ c h).1; omega763      · exact (bsOuts_res (rIdx_width i.2) c h).1)764  have hT := polyE bsLen_pos leafBN bs_leaves bsSizeE _ (fun i => (bsSizeE_eval i).symm)765  refine ⟨bsLen_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, ?_, ?_⟩766  · obtain ⟨c, k, h⟩ := polyIn_add bsLen_pos hT (polyIn_leaf (fun i _ => Nat.le_refl (bsLen i)))767    refine ⟨c, k, fun i hi => netBounded_mono (spec i).2.2.2.2.2.1 ?_⟩768    have := bsAll_tsize i; have := h i hi; dsimp only at *; unfold tsize at *; omega769  · refine polyIn_mono (fun i _ => ?_) (polyIn_mul (polyIn_const _ _ 34) hT)770    have g := (spec i).2.2.2.2.2.2771    have h1 := bsAll_tsize i772    have h2 := length_le_tsize (bsAll i)773    unfold tsize at h1 h2774    show gateCount (compileF (bsAll i)) ≤ 34 * _775    omega

Project declarations in the statement: BoardStore.bsLen, BoardStore.bsNet, Family.NetFam, Family.restAdm

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, BoardStore.bsAll, BoardStore.bsAll_tsize, BoardStore.bsForms, BoardStore.bsForms_res, BoardStore.bsLen, BoardStore.bsLen_pos, BoardStore.bsNet, BoardStore.bsOuts, BoardStore.bsOuts_res, BoardStore.bsSizeE, BoardStore.bsSizeE_eval, BoardStore.bs_leaves, BoardStore.sw, BoardStore.varSz, Family.NetFam.mk, Family.PE.eval, Family.PolyIn, Family.leafBN, Family.length_le_tsize, Family.netBounded_mono, Family.polyE, Family.polyIn_add, Family.polyIn_const, Family.polyIn_leaf, Family.polyIn_mono, Family.polyIn_mul, Family.rIdx_width, Family.restAdm, Family.tsize, FiniteNet.Wired, ThresholdNet.compileF, ThresholdNet.compileF_spec, ThresholdNet.gateCount, WholeGame.rIdx

Definitions these statements use

inductive BoardStore.BOut

Module BoardStore (lean/phase6/BoardStore.lean, lines 39–42) · file SHA-256 c35ac76d5db6e833…

Output at a separator: summary and selected move.

Statement as elaborated and printed by Lean 4.26.0

Type
Exact source text, lines 39–42
39/-- Output at a separator: summary and selected move. -/40structure BOut where41  sum : Nat42  move : Option (Nat × Nat)

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

inductive BoardStore.BS

Module BoardStore (lean/phase6/BoardStore.lean, lines 32–35) · file SHA-256 c35ac76d5db6e833…

Statement as elaborated and printed by Lean 4.26.0

Type
Exact source text, lines 32–35
32structure BS where33  board : List Nat34  acc : Nat35  idx : Nat

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def BoardStore.bsRun

Module BoardStore (lean/phase6/BoardStore.lean, lines 49–51) · file SHA-256 c35ac76d5db6e833…

Statement as elaborated and printed by Lean 4.26.0

ℕ →
  NimAudit.BoardStore.BS →
    List NimAudit.Controller.Tok → NimAudit.BoardStore.BS × List NimAudit.BoardStore.BOut
Exact source text, lines 49–51
49def bsRun (N : Nat) : BS → List Tok → BS × List BOut50  | s, [] => (s, [])51  | s, t :: ts => ((bsRun N (bsStep N s t).1 ts).1, (bsStep N s t).2.toList ++ (bsRun N (bsStep N s t).1 ts).2)

Project declarations in the statement: BoardStore.BOut, BoardStore.BS, Controller.Tok

Project declarations used by the proof or definition body

BoardStore.BOut, BoardStore.BS, BoardStore.bsStep, Controller.Tok

def BoardStore.btoks

Module BoardStore (lean/phase6/BoardStore.lean, lines 53–54) · file SHA-256 c35ac76d5db6e833…

The tokens of one decision: one pass over the rows, then a separator.

Statement as elaborated and printed by Lean 4.26.0

List ℕ → List NimAudit.Controller.Tok
Exact source text, lines 53–54
53/-- The tokens of one decision: one pass over the rows, then a separator. -/54def btoks (P : List Nat) : List Tok := P.map Tok.row ++ [Tok.sep]

Project declarations in the statement: Controller.Tok

Project declarations used by the proof or definition body

Controller.Tok, Controller.Tok.row, Controller.Tok.sep

def Controller.decisionMove

Module Controller (lean/phase4/Controller.lean, lines 206–207) · file SHA-256 63d0e09c002db91e…

The move output of a decision (independent of the retained summary state).

Statement as elaborated and printed by Lean 4.26.0

List ℕ → Option (ℕ × ℕ)
Exact source text, lines 206–207
206/-- The move output of a decision (independent of the retained summary state). -/207def decisionMove (P : List Nat) : Option (Nat × Nat) := replayMove (nimSum P) P

Project declarations in the statement: none

Project declarations used by the proof or definition body

Recurrent.replayMove, nimSum

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

Module BoardStore (lean/phase6/BoardStore.lean, lines 428–430) · file SHA-256 c35ac76d5db6e833…

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → ℕ → (ℕ → Bool) → List NimAudit.Controller.Tok → ℕ → Bool
Exact source text, lines 428–430
428def bsBitRun (B N r : Nat) : (Nat → Bool) → List Tok → (Nat → Bool)429  | v, [] => v430  | v, t :: ts => bsBitRun B N r (bsBitStep B N r v t) ts

Project declarations in the statement: Controller.Tok

Project declarations used by the proof or definition body

BoardStore.bsBitStep, Controller.Tok

def BoardStore.bsBits

Module BoardStore (lean/phase6/BoardStore.lean, lines 154–157) · file SHA-256 c35ac76d5db6e833…

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → ℕ → NimAudit.BoardStore.BS → ℕ → Bool
Exact source text, lines 154–157
154def bsBits (B N r : Nat) (s : BS) : Nat → Bool := fun w =>155  if w < B * N then boardBits B s.board w156  else if w < B * N + B then s.acc.testBit (w - B * N)157  else if w < sw B N r then s.idx.testBit (w - (B * N + B)) else false

Project declarations in the statement: BoardStore.BS

Project declarations used by the proof or definition body

BoardStore.BS, BoardStore.BS.acc, BoardStore.BS.board, BoardStore.BS.idx, BoardStore.sw, CorrBridge.boardBits

def BoardStore.bsDecode

Module BoardStore (lean/phase6/BoardStore.lean, lines 370–374) · file SHA-256 c35ac76d5db6e833…

Output decoding at a separator: flag, summary, selected move.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → ℕ → ℕ → (ℕ → Bool) → Option NimAudit.BoardStore.BOut
Exact source text, lines 370–374
370/-- Output decoding at a separator: flag, summary, selected move. -/371def bsDecode (B N r r' : Nat) (z : Nat → Bool) : Option BOut :=372  if z (sw B N r + 1) then373    some ⟨ofBits B (fun q => z (accW B N q)), binSem (varBin B N r') N z⟩374  else none

Project declarations in the statement: BoardStore.BOut

Project declarations used by the proof or definition body

BoardStore.BOut, BoardStore.BOut.mk, BoardStore.accW, BoardStore.sw, Game.ofBits, PriorityEncoder.binSem, PriorityEncoder.varBin

def BoardStore.inB

Module BoardStore (lean/phase6/BoardStore.lean, lines 165–166) · file SHA-256 c35ac76d5db6e833…

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → ℕ → (ℕ → Bool) → NimAudit.Controller.Tok → ℕ → Bool
Exact source text, lines 165–166
165def inB (B N r : Nat) (v : Nat → Bool) (t : Tok) : Nat → Bool := fun w =>166  if w < sw B N r then v w else tokB t (w - sw B N r)

Project declarations in the statement: Controller.Tok

Project declarations used by the proof or definition body

BoardStore.sw, BoardStore.tokB, Controller.Tok

inductive Controller.Tok

Module Controller (lean/phase4/Controller.lean, lines 29–32) · file SHA-256 63d0e09c002db91e…

Statement as elaborated and printed by Lean 4.26.0

Type
Exact source text, lines 29–32
29inductive Tok where30  | row (x : Nat)31  | sep32  | reset

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

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

inductive BoardStore.BitStoreWins

Module BoardStore (lean/phase6/BoardStore.lean, lines 515–520) · file SHA-256 c35ac76d5db6e833…

Stateful interaction driven by the BIT-LEVEL machine (register vector v).

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → ℕ → ℕ → (ℕ → Bool) → List ℕ → Prop
Exact source text, lines 515–520
515/-- Stateful interaction driven by the BIT-LEVEL machine (register vector v). -/516inductive BitStoreWins (B N r r' : Nat) : (Nat → Bool) → List Nat → Prop517  | intro (v : Nat → Bool) (P R : List Nat) :518      applyM P (bitMove B N r r' v P) = some R → Move P R →519      bsBitRun B N r v (btoks P) = bsBits B N r ⟨P, 0, 0⟩ →520      (∀ P', Move R P' → BitStoreWins B N r r' (bsBits B N r ⟨P, 0, 0⟩) P') → BitStoreWins B N r r' v P

Project declarations in the statement: none

Project declarations used by the proof or definition body

BoardStore.BS.mk, BoardStore.bitMove, BoardStore.bsBitRun, BoardStore.bsBits, BoardStore.btoks, Game.Move, SelectCircuit.applyM

inductive AC0.Circ

Module Circuit (lean/phase3/Circuit.lean, lines 35–40) · file SHA-256 af97cc0eec7d8464…

Statement as elaborated and printed by Lean 4.26.0

Type
Exact source text, lines 35–40
35inductive Circ where36  | input (i : Nat)37  | const (b : Bool)38  | not (c : Circ)39  | and (cs : List Circ)40  | or (cs : List Circ)

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def BoardStore.bsForms

Module BoardStore (lean/phase6/BoardStore.lean, lines 191–193) · file SHA-256 c35ac76d5db6e833…

The update formulas: board, accumulator, pointer.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → ℕ → List NimAudit.AC0.Circ
Exact source text, lines 191–193
191/-- The update formulas: board, accumulator, pointer. -/192def bsForms (B N r : Nat) : List Circ :=193  (List.range (B * N)).map (bBoard B N r) ++ (List.range B).map (bAcc B N r) ++ (List.range r).map (bIdx B N r)

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

AC0.Circ, BoardStore.bAcc, BoardStore.bBoard, BoardStore.bIdx

def BoardStore.sw

Module BoardStore (lean/phase6/BoardStore.lean, lines 148–149) · file SHA-256 c35ac76d5db6e833…

State width B·N + B + r.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → ℕ → ℕ
Exact source text, lines 148–149
148/-- State width B·N + B + r. -/149def sw (B N r : Nat) : Nat := B * N + B + r

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def BoardStore.bsAll

Module BoardStore (lean/phase6/BoardStore.lean, lines 665–665) · file SHA-256 c35ac76d5db6e833…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → List NimAudit.AC0.Circ
Exact source text, lines 665–665
665def bsAll (i : Nat × Nat) : List Circ := bsForms i.1 i.2 (rIdx i.2) ++ bsOuts i.1 i.2 (rIdx i.2) (rIdx i.2)

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

AC0.Circ, BoardStore.bsForms, BoardStore.bsOuts, WholeGame.rIdx

def BoardStore.bsLen

Module BoardStore (lean/phase6/BoardStore.lean, lines 663–664) · file SHA-256 c35ac76d5db6e833…

Members (B, N), B, N ≥ 1, r = r' = log₂N + 1; input = registers + token.

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → ℕ
Exact source text, lines 663–664
663/-- Members (B, N), B, N ≥ 1, r = r' = log₂N + 1; input = registers + token. -/664def bsLen : Nat × Nat → Nat := fun i => sw i.1 i.2 (rIdx i.2) + 3 + i.1

Project declarations in the statement: none

Project declarations used by the proof or definition body

BoardStore.sw, WholeGame.rIdx

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

Module BoardStore (lean/phase6/BoardStore.lean, lines 713–713) · file SHA-256 c35ac76d5db6e833…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → List NimAudit.AC0.Layer
Exact source text, lines 713–713
713def bsNet (i : Nat × Nat) : List Layer := compileF (bsAll i)

Project declarations in the statement: AC0.Layer

Project declarations used by the proof or definition body

BoardStore.bsAll, ThresholdNet.compileF

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

Full modules

ModuleFileLinesImports
BoardStorelean/phase6/BoardStore.lean824Bypass
Circuitlean/phase3/Circuit.lean1151NimProbability
Controllerlean/phase4/Controller.lean401NimRecurrent, AttainCircuit
Familylean/phase6/Family.lean574WholeGame
NimCorelean/NimCore.lean139Std
NimGamelean/phase2/NimGame.lean634NimRollout

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