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

Section 5.5, “Connecting recurrence to the history bypass”Retained summaries give Δ of consecutive supplied boards; with decision-time boards only it spans two moves

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

1 Paper text

Connecting recurrence to the history bypass. The retained summaries allow the agent to compare consecutive positions through σt−1⊕σt=nim⁡(Pt−1)⊕nim⁡(Pt)=Δ(Pt−1,Pt).\sigma_{t-1}\oplus\sigma_t =\operatorname{nim}(P_{t-1})\oplus\operatorname{nim}(P_t) =\Delta(P_{t-1},P_t). When one heap changes from aa to bb, this equals a⊕ba\oplus b. If the preceding position has nim-sum zero, the difference is exactly the invariant that the restoration rule must cancel. Storing the preceding board additionally permits direct row-by-row comparison as the new board arrives. A summary of O(B)O(B) bits preserves the invariant, rather than the full game history; arbitrary access to old positions requires additional storage or replay. The difference always refers to consecutive completed boards actually supplied to the controller. If these are only the boards at the player’s decision times, they usually span two game moves. Comparing just the opponent’s move instead requires the player’s own post-move board as the preceding frame. The initial scan also computes the invariant from an arbitrary starting position, without assuming an earlier zero-nim-sum frame. Thus memory across row updates is sufficient for this route; an earlier game position is useful for transition comparisons but is not required to compute the current nim-sum. This initialisation uses the growing recurrent horizon and is therefore an additional resource beyond the fixed-latency two-frame construction.

Generated from paper_jmlr.tex, lines 862–870.

2 Explain this

NIM's legal moves and optimal play depend only on the current board. Memory supplies computational context, rather than missing game-theoretic information. Accumulating the current board row by row is already sufficient to compute its nim-sum; retaining an earlier position additionally supports transition comparisons.

Connecting to the two-frame idea. The retained summaries give σt−1⊕σt=Δ(Pt−1,Pt)\sigma_{t-1}\oplus\sigma_t=\Delta(P_{t-1},P_t) for consecutive supplied boards. If one heap changed from aa to bb, this is a⊕ba\oplus b.

Which boards are consecutive matters. If the controller sees only the boards at the player's decision times, consecutive boards are two moves apart (the player's own move and the opponent's), and the difference mixes both. To isolate the opponent's move, the player's own post-move board must be supplied as the preceding frame.

Initialisation. The first scan computes the invariant from an arbitrary starting position, with no earlier zero-nim-sum frame. That uses the growing recurrent horizon, an extra resource beyond the fixed-latency two-frame construction.

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 3scan
  3. row 4scan
  4. row 6scan
  5. SEPsummary
  6. row 3replay
  7. row 4replay
  8. row 6replay
  9. SEPmove
  10. row 2scan
  11. row 4scan
  12. row 1scan
  13. SEPsummary
  14. row 2replay
  15. row 4replay
  16. row 1replay
  17. SEPmove

17 / 17 SEP: separator after replay: output the move, return to scan mode

Registers after this update

mode
scan
accumulator
0 000
previous summary
7 111
stored summary used in replay
7
heap counter
0
first candidate
no move
first fallback
no move

Outputs so far

  • after token 5: summary σ = 1 (no previous summary)
  • after token 9: move heap 0 → 2
  • after token 13: summary σ = 7, difference from the previous summary 6
  • after token 17: move heap 1 → 3

Counting the work

  • One decision on 3 heaps takes 2N + 2 = 8 updates: N scan rows, a separator, the same N rows again, a separator (plus one reset at the start of a game). The board is supplied twice; the controller does not store it.
  • Memory: accumulator, previous summary, stored summary, counter, candidate and fallback registers: 4 + 5B + 3r bits with N < 2r; here B = 3, r = 2, so 25 bits.
  • Each single update is a shallow circuit (replay controller: Boolean depth ≤ 8, ≤ 18 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 17 updates as a table
#TokenRegisters afterOutput
1RESETscan, acc 0, prev 0*, idx 0, cand no move, fb no move
2row 3scan, acc 3, prev 0*, idx 0, cand no move, fb no move
3row 4scan, acc 7, prev 0*, idx 0, cand no move, fb no move
4row 6scan, acc 1, prev 0*, idx 0, cand no move, fb no move
5SEPreplay, acc 0, prev 1, idx 0, cand no move, fb no moveσ = 1
6row 3replay, acc 0, prev 1, idx 1, cand heap 0 → 2, fb heap 0 → 2
7row 4replay, acc 0, prev 1, idx 2, cand heap 0 → 2, fb heap 0 → 2
8row 6replay, acc 0, prev 1, idx 3, cand heap 0 → 2, fb heap 0 → 2
9SEPscan, acc 0, prev 1, idx 0, cand no move, fb no movemove heap 0 → 2
10row 2scan, acc 2, prev 1, idx 0, cand no move, fb no move
11row 4scan, acc 6, prev 1, idx 0, cand no move, fb no move
12row 1scan, acc 7, prev 1, idx 0, cand no move, fb no move
13SEPreplay, acc 0, prev 7, idx 0, cand no move, fb no moveσ = 7, diff 6
14row 2replay, acc 0, prev 7, idx 1, cand no move, fb heap 0 → 1
15row 4replay, acc 0, prev 7, idx 2, cand heap 1 → 3, fb heap 0 → 1
16row 1replay, acc 0, prev 7, idx 3, cand heap 1 → 3, fb heap 0 → 1
17SEPscan, acc 0, prev 7, idx 0, cand no move, fb no movemove heap 1 → 3

* no previous summary yet (validity bit 0).

Game: (3, 4, 6) —your move (δ = 1)→ (2, 4, 6) —opponent (δ = 7)→ (2, 4, 1)

Only the boards at your decision times

Position fedsummary σdifference
(3, 4, 6)1—
(2, 4, 1)76

The difference 6 = 1 ⊕ 7 spans two moves: yours and the opponent’s.

Including your own post-move board

Position fedsummary σdifference
(3, 4, 6)1—
(2, 4, 6)01
(2, 4, 1)77

Now the last difference is 7, the opponent’s move alone, because your post-move board (2, 4, 6) is the preceding frame.

Computed with the replay controller; feeding your post-move board costs another 2N + 2 updates, and the move it then outputs is discarded.

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

  • Bypass.diff_of_transition: when consecutive supplied boards differ by one legal move, the threshold controller reports exactly that heap's XOR difference.
  • Bypass.diff_with_postMove: if the player's own post-move board RR (nim-sum zero) is supplied before the opponent's board P′P', the reported difference is the opponent's delta, which equals nim⁡(P′)\operatorname{nim}(P'), the restoration target.
  • Bypass.diff_decision_only: a concrete counterexample with decision-time boards only: (1,2)→(1,1)→(0,1)(1,2)\to(1,1)\to(0,1); supplying only (1,2)(1,2) and (0,1)(0,1), the controller reports difference 22, while the opponent's delta was 11.
  • Recurrent.stream_reports_delta: the summary-level statement.
Coverage record
Paper anchorpar-connecting-recurrence-to-the-history-bypass-p1 (website anchor; the manuscript has no label here)
Displayed asSection 5.5, “Connecting recurrence to the history bypass”
ClaimRetained summaries give Δ of consecutive supplied boards; with decision-time boards only it spans two moves
Coverage categoryChecked theorem
Statement sourcepaper_jmlr.tex lines 862–870; SHA-256 of the normalised block source c43d305b98d3cb23…
Lean declarations
Depends onProposition 5.13, Proposition 5.5
Explanationsexplain/c-recurrence-history, formal/c-recurrence-history
Build evidencefresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem Bypass.diff_of_transition

Module Bypass (lean/phase6/Bypass.lean, lines 197–210) · file SHA-256 d2e3ef2e71220448… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

ONE-LEGAL-TRANSITION FORM: when consecutive supplied boards differ by one legal move, the threshold controller reports exactly that heap's XOR difference.

Statement as elaborated and printed by Lean 4.26.0

∀ {B N : ℕ} {Q Q' : List ℕ},
  N < 2 ^ NimAudit.WholeGame.rIdx N →
    Q.length = N →
      Q'.length = N →
        NimAudit.Game.Width B Q →
          NimAudit.Game.Width B Q' →
            NimAudit.Game.Move Q Q' →
              ∃ pre x post z,
                Q = pre ++ x :: post ∧
                  Q' = pre ++ z :: post ∧
                    (NimAudit.ThresholdInst.trun B (NimAudit.WholeGame.rIdx N)
                            (NimAudit.ControllerBits.sbits B (NimAudit.WholeGame.rIdx N)
                              NimAudit.Controller.cinit)
                            (NimAudit.Controller.stream [Q, Q'])).2[2]? =
                      some (NimAudit.Controller.COut.summary (NimAudit.nimSum Q') (some (x ^^^ z)))
Exact source text, lines 197–210
197/-- ONE-LEGAL-TRANSITION FORM: when consecutive supplied boards differ by one legal move,198    the threshold controller reports exactly that heap's XOR difference. -/199theorem diff_of_transition {B N : Nat} {Q Q' : List Nat} (hN : N < 2 ^ rIdx N) (hQ : Q.length = N)200    (hQ' : Q'.length = N) (hw : Width B Q) (hw' : Width B Q') (hm : Move Q Q') :201    ∃ pre x post z, Q = pre ++ x :: post ∧ Q' = pre ++ z :: post ∧202      (trun B (rIdx N) (sbits B (rIdx N) cinit) (stream [Q, Q'])).2[2]? =203        some (COut.summary (nimSum Q') (some (x ^^^ z))) := by204  obtain ⟨pre, x, post, z, h1, h2, _, h4⟩ := one_transition_diff hm205  refine ⟨pre, x, post, z, h1, h2, ?_⟩206  rw [trun_stream hN [Q, Q'] (by207    intro P hP; simp only [List.mem_cons, List.mem_nil_iff, or_false] at hP208    rcases hP with rfl | rfl209    · exact ⟨hQ, hw⟩210    · exact ⟨hQ', hw'⟩), ctrlOuts_two, h4]

Project declarations in the statement: Controller.COut, Controller.COut.summary, Controller.cinit, Controller.stream, ControllerBits.sbits, Game.Move, Game.Width, ThresholdInst.trun, WholeGame.rIdx, nimSum

Project declarations used by the proof or definition body

Bypass.ctrlOuts_two, Bypass.one_transition_diff, Controller.COut, Controller.COut.summary, Controller.cinit, Controller.ctrlOuts, Controller.stream, ControllerBits.sbits, Game.Move, Game.Width, ThresholdInst.trun, ThresholdInst.trun_stream, WholeGame.rIdx, nimSum

theorem Bypass.diff_with_postMove

Module Bypass (lean/phase6/Bypass.lean, lines 212–229) · file SHA-256 d2e3ef2e71220448… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

POST-MOVE BOARD SUPPLIED: if the protocol also supplies the player's own post-move board R (nim(R) = 0) before the opponent's board P', the reported difference at P' is the opponent's one-heap delta x ⊕ z, which equals nim(P') (the restoration target).

Statement as elaborated and printed by Lean 4.26.0

∀ {B N : ℕ} {P0 R P' : List ℕ},
  N < 2 ^ NimAudit.WholeGame.rIdx N →
    P0.length = N ∧ NimAudit.Game.Width B P0 →
      R.length = N ∧ NimAudit.Game.Width B R →
        P'.length = N ∧ NimAudit.Game.Width B P' →
          NimAudit.nimSum R = 0 →
            NimAudit.Game.Move R P' →
              ∃ pre x post z,
                R = pre ++ x :: post ∧
                  P' = pre ++ z :: post ∧
                    (NimAudit.ThresholdInst.trun B (NimAudit.WholeGame.rIdx N)
                              (NimAudit.ControllerBits.sbits B (NimAudit.WholeGame.rIdx N)
                                NimAudit.Controller.cinit)
                              (NimAudit.Controller.stream [P0, R, P'])).2[4]? =
                        some
                          (NimAudit.Controller.COut.summary (NimAudit.nimSum P') (some (x ^^^ z))) ∧
                      x ^^^ z = NimAudit.nimSum P'
Exact source text, lines 212–229
212/-- POST-MOVE BOARD SUPPLIED: if the protocol also supplies the player's own post-move213    board R (nim(R) = 0) before the opponent's board P', the reported difference at P'214    is the opponent's one-heap delta x ⊕ z, which equals nim(P') (the restoration target). -/215theorem diff_with_postMove {B N : Nat} {P0 R P' : List Nat} (hN : N < 2 ^ rIdx N)216    (h0 : P0.length = N ∧ Width B P0) (h1 : R.length = N ∧ Width B R) (h2 : P'.length = N ∧ Width B P')217    (hz : nimSum R = 0) (hm : Move R P') :218    ∃ pre x post z, R = pre ++ x :: post ∧ P' = pre ++ z :: post ∧219      (trun B (rIdx N) (sbits B (rIdx N) cinit) (stream [P0, R, P'])).2[4]? =220        some (COut.summary (nimSum P') (some (x ^^^ z))) ∧ x ^^^ z = nimSum P' := by221  obtain ⟨pre, x, post, z, e1, e2, _, e4⟩ := one_transition_diff hm222  refine ⟨pre, x, post, z, e1, e2, ?_, by rw [← e4, hz, Nat.zero_xor]⟩223  rw [trun_stream hN [P0, R, P'] (by224    intro P hP; simp only [List.mem_cons, List.mem_nil_iff, or_false] at hP225    rcases hP with rfl | rfl | rfl226    · exact h0227    · exact h1228    · exact h2), ← e4]229  simp [ctrlOuts]

Project declarations in the statement: Controller.COut, Controller.COut.summary, Controller.cinit, Controller.stream, ControllerBits.sbits, Game.Move, Game.Width, ThresholdInst.trun, WholeGame.rIdx, nimSum

Project declarations used by the proof or definition body

Bypass.one_transition_diff, Controller.COut, Controller.COut.move, Controller.COut.summary, Controller.cinit, Controller.ctrlOuts, Controller.stream, ControllerBits.sbits, Game.Move, Game.Width, Recurrent.replayMove, ThresholdInst.trun, ThresholdInst.trun_stream, WholeGame.rIdx, nimSum

theorem Bypass.diff_decision_only

Module Bypass (lean/phase6/Bypass.lean, lines 231–245) · file SHA-256 d2e3ef2e71220448… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

DECISION-TIME BOARDS ONLY: the reported difference spans two moves and is in general NOT the opponent's delta. Concretely: P0 = [1,2] (player to move), the player moves to R = [1,1] (nim 0), the opponent moves to P1 = [0,1] (delta 1); supplying only P0 and P1, the threshold controller reports difference 2.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Game.Move [1, 2] [1, 1] ∧
  NimAudit.nimSum [1, 1] = 0 ∧
    NimAudit.Game.Move [1, 1] [0, 1] ∧
      1 ^^^ 0 = 1 ∧
        (NimAudit.ThresholdInst.trun 2 (NimAudit.WholeGame.rIdx 2)
                (NimAudit.ControllerBits.sbits 2 (NimAudit.WholeGame.rIdx 2)
                  NimAudit.Controller.cinit)
                (NimAudit.Controller.stream [[1, 2], [0, 1]])).2[2]? =
          some (NimAudit.Controller.COut.summary 1 (some 2))
Exact source text, lines 231–245
231/-- DECISION-TIME BOARDS ONLY: the reported difference spans two moves and is in general232    NOT the opponent's delta.  Concretely: P0 = [1,2] (player to move), the player moves to233    R = [1,1] (nim 0), the opponent moves to P1 = [0,1] (delta 1); supplying only P0 and P1,234    the threshold controller reports difference 2. -/235theorem diff_decision_only :236    Move [1, 2] [1, 1] ∧ nimSum [1, 1] = 0 ∧ Move [1, 1] [0, 1] ∧ (1 ^^^ 0 : Nat) = 1 ∧237    (trun 2 (rIdx 2) (sbits 2 (rIdx 2) cinit) (stream [[1, 2], [0, 1]])).2[2]? =238      some (COut.summary 1 (some 2)) := by239  refine ⟨⟨[1], 2, [], 1, rfl, rfl, by decide⟩, by decide, ⟨[], 1, [1], 0, rfl, rfl, by decide⟩, by decide, ?_⟩240  rw [trun_stream (rIdx_counter 2) _ (by241    intro P hP; simp only [List.mem_cons, List.mem_nil_iff, or_false] at hP242    rcases hP with rfl | rfl243    · exact ⟨rfl, by intro x hx; simp at hx; omega⟩244    · exact ⟨rfl, by intro x hx; simp at hx; omega⟩), ctrlOuts_two]245  rfl

Project declarations in the statement: Controller.COut, Controller.COut.summary, Controller.cinit, Controller.stream, ControllerBits.sbits, Game.Move, ThresholdInst.trun, WholeGame.rIdx, nimSum

Project declarations used by the proof or definition body

Bypass.ctrlOuts_two, Controller.COut, Controller.COut.summary, Controller.cinit, Controller.ctrlOuts, Controller.stream, ControllerBits.sbits, Family.rIdx_counter, Game.Move, Game.Width, ThresholdInst.trun, ThresholdInst.trun_stream, WholeGame.rIdx, nimSum

theorem Recurrent.stream_reports_delta

Module NimRecurrent (lean/phase3/NimRecurrent.lean, lines 173–177) · file SHA-256 1f2994aefc75e7f5… Axioms reported by the fresh build: propext

Statement as elaborated and printed by Lean 4.26.0

∀ (Q Q' : List ℕ) (Ps : List (List ℕ)),
  NimAudit.Recurrent.expectedOuts false 0 (Q :: Q' :: Ps) =
    { summary := NimAudit.nimSum Q, diff := none } ::
      { summary := NimAudit.nimSum Q', diff := some (NimAudit.nimSum Q ^^^ NimAudit.nimSum Q') } ::
        NimAudit.Recurrent.expectedOuts true (NimAudit.nimSum Q') Ps
Exact source text, lines 173–177
173theorem stream_reports_delta (Q Q' : List Nat) (Ps : List (List Nat)) :174    expectedOuts false 0 (Q :: Q' :: Ps) =175      ⟨nimSum Q, none⟩ :: ⟨nimSum Q', some (nimSum Q ^^^ nimSum Q')⟩ ::176        expectedOuts true (nimSum Q') Ps := by177  simp [expectedOuts]

Project declarations in the statement: Recurrent.Out, Recurrent.Out.mk, Recurrent.expectedOuts, nimSum

Project declarations used by the proof or definition body

Recurrent.Out, Recurrent.Out.mk, Recurrent.expectedOuts, nimSum

Definitions these statements use

inductive Controller.COut

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

Statement as elaborated and printed by Lean 4.26.0

Type
Exact source text, lines 44–46
44inductive COut where45  | summary (s : Nat) (diff : Option Nat)46  | move (m : Option (Nat × Nat))

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def Controller.cinit

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

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Controller.CState
Exact source text, lines 48–48
48def cinit : CState := ⟨false, 0, 0, false, 0, 0, none, none⟩

Project declarations in the statement: Controller.CState

Project declarations used by the proof or definition body

Controller.CState.mk

def Controller.stream

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

Statement as elaborated and printed by Lean 4.26.0

List (List ℕ) → List NimAudit.Controller.Tok
Exact source text, lines 78–78
78def stream (Ps : List (List Nat)) : List Tok := Ps.flatMap dtoks

Project declarations in the statement: Controller.Tok

Project declarations used by the proof or definition body

Controller.Tok, Controller.dtoks

def ControllerBits.sbits

Module ControllerBits (lean/phase4/ControllerBits.lean, lines 104–108) · file SHA-256 4e23680da471fd69…

The canonical state vector (4 + 5B + 3r bits; false beyond).

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → NimAudit.Controller.CState → ℕ → Bool
Exact source text, lines 104–108
104/-- The canonical state vector (4 + 5B + 3r bits; false beyond). -/105def sbits (B r : Nat) (s : CState) : Nat → Bool :=106  layout B r false s.replayMode s.acc.testBit s.prev.testBit s.valid s.sig.testBit s.idx.testBit107    s.sel.isSome (optI s.sel).testBit (optV s.sel).testBit s.fnz.isSome (optI s.fnz).testBit108    (optV s.fnz).testBit

Project declarations in the statement: Controller.CState

Project declarations used by the proof or definition body

Controller.CState, Controller.CState.acc, Controller.CState.fnz, Controller.CState.idx, Controller.CState.prev, Controller.CState.replayMode, Controller.CState.sel, Controller.CState.sig, Controller.CState.valid, ControllerBits.layout, ControllerBits.optI, ControllerBits.optV

def Game.Move

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

An ordinary legal Nim move: exactly one heap strictly decreases.

Statement as elaborated and printed by Lean 4.26.0

List ℕ → List ℕ → Prop
Exact source text, lines 24–26
24/-- An ordinary legal Nim move: exactly one heap strictly decreases. -/25def Move (p q : List Nat) : Prop :=26  ∃ pre x post y, p = pre ++ x :: post ∧ q = pre ++ y :: post ∧ y < x

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

def ThresholdInst.trun

Module ThresholdInst (lean/phase5/ThresholdInst.lean, lines 155–158) · file SHA-256 c8c66599c8e24804…

Runs of the threshold controller.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → (ℕ → Bool) → List NimAudit.Controller.Tok → (ℕ → Bool) × List NimAudit.Controller.COut
Exact source text, lines 155–158
155/-- Runs of the threshold controller. -/156def trun (B r : Nat) : (Nat → Bool) → List Tok → (Nat → Bool) × List COut157  | v, [] => (v, [])158  | v, t :: ts => ((trun B r (tstep B r v t).1 ts).1, (tstep B r v t).2.toList ++ (trun B r (tstep B r v t).1 ts).2)

Project declarations in the statement: Controller.COut, Controller.Tok

Project declarations used by the proof or definition body

Controller.COut, Controller.Tok, ThresholdInst.tstep

def WholeGame.rIdx

Module WholeGame (lean/phase5/WholeGame.lean, lines 108–109) · file SHA-256 809a74ad589db609…

Index width used for N heaps.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ
Exact source text, lines 108–109
108/-- Index width used for N heaps. -/109def rIdx (N : Nat) : Nat := N.log2 + 1

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

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

Module NimRecurrent (lean/phase3/NimRecurrent.lean, lines 41–43) · file SHA-256 1f2994aefc75e7f5…

Statement as elaborated and printed by Lean 4.26.0

Type
Exact source text, lines 41–43
41structure Out where42  summary : Nat43  diff : Option Nat

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def Recurrent.expectedOuts

Module NimRecurrent (lean/phase3/NimRecurrent.lean, lines 84–88) · file SHA-256 1f2994aefc75e7f5…

Expected outputs for a sequence of positions from a state with empty accumulator.

Statement as elaborated and printed by Lean 4.26.0

Bool → ℕ → List (List ℕ) → List NimAudit.Recurrent.Out
Exact source text, lines 84–88
84/-- Expected outputs for a sequence of positions from a state with empty accumulator. -/85def expectedOuts : Bool → Nat → List (List Nat) → List Out86  | _, _, [] => []87  | v, q, P :: Ps =>88    ⟨nimSum P, if v then some (q ^^^ nimSum P) else none⟩ :: expectedOuts true (nimSum P) Ps

Project declarations in the statement: Recurrent.Out

Project declarations used by the proof or definition body

Recurrent.Out, Recurrent.Out.mk, nimSum

Full modules

ModuleFileLinesImports
Bypasslean/phase6/Bypass.lean275RolloutExec
Controllerlean/phase4/Controller.lean401NimRecurrent, AttainCircuit
ControllerBitslean/phase4/ControllerBits.lean1148Controller, NimCorrBridge
NimCorelean/NimCore.lean139Std
NimGamelean/phase2/NimGame.lean634NimRollout
NimRecurrentlean/phase3/NimRecurrent.lean555NimAttain, Circuit
ThresholdInstlean/phase5/ThresholdInst.lean475ThresholdNet, PriorityEncoder
WholeGamelean/phase5/WholeGame.lean347ThresholdInst

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