Checked definition or construction Lean contains the definition or construction, with checked properties.
Serialising positions and retaining state. Write position , with each heap represented by one -bit row. Feed successive positions as the stream Each row arrives as a block of bits together with a row/separator tag. A separator marks the end of a complete position; the agent chooses a move only after that position has been read. The next observed position is then appended to the stream. For comparisons of individual heaps, indices remain aligned across positions, including rows for empty heaps. A scan of the current board suffices for nim-sum evaluation without earlier game positions; cross-position memory additionally supports the comparisons below. The hidden state is carried across rows and position boundaries. A separator resets the accumulator for the next scan while preserving selected information about the completed position; it does not reset the entire memory.
Generated from paper_jmlr.tex, lines 827–834.
The input protocol. Positions are fed one row (heap) at a time, in a fixed heap order. After all rows of each position comes a
separator token SEP. Rows for empty heaps are still sent, so heap is always the -th row.
What the separator does. It marks a complete position. It resets the accumulator for the next scan but keeps selected information about the finished position (its summary). It does not wipe the whole memory.
Example. Positions then become the stream .
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.
11 / 11 SEP: separator after replay: output the move, return to scan mode
Edge case outside the protocol: the extra separator is read as an empty position. No theorem is stated for such streams; the update rule is simply applied.
| # | Token | Registers after | Output |
|---|---|---|---|
| 1 | RESET | scan, acc 0, prev 0*, idx 0, cand no move, fb no move | |
| 2 | row 3 | scan, acc 3, prev 0*, idx 0, cand no move, fb no move | |
| 3 | row 4 | scan, acc 7, prev 0*, idx 0, cand no move, fb no move | |
| 4 | row 6 | scan, acc 1, prev 0*, idx 0, cand no move, fb no move | |
| 5 | SEP | replay, acc 0, prev 1, idx 0, cand no move, fb no move | σ = 1 |
| 6 | row 3 | replay, acc 0, prev 1, idx 1, cand heap 0 → 2, fb heap 0 → 2 | |
| 7 | row 4 | replay, acc 0, prev 1, idx 2, cand heap 0 → 2, fb heap 0 → 2 | |
| 8 | row 6 | replay, acc 0, prev 1, idx 3, cand heap 0 → 2, fb heap 0 → 2 | |
| 9 | SEP | scan, acc 0, prev 1, idx 0, cand no move, fb no move | move heap 0 → 2 |
| 10 | SEP | replay, acc 0, prev 0, idx 0, cand no move, fb no move | σ = 0, diff 1 |
| 11 | SEP | scan, acc 0, prev 0, idx 0, cand no move, fb no move | move no move |
* no previous summary yet (validity bit 0).
Game: (3, 4, 6) —your move (δ = 1)→ (2, 4, 6) —opponent (δ = 7)→ (2, 4, 1)
| Position fed | summary σ | difference |
|---|---|---|
| (3, 4, 6) | 1 | — |
| (2, 4, 1) | 7 | 6 |
The difference 6 = 1 ⊕ 7 spans two moves: yours and the opponent’s.
| Position fed | summary σ | difference |
|---|---|---|
| (3, 4, 6) | 1 | — |
| (2, 4, 6) | 0 | 1 |
| (2, 4, 1) | 7 | 7 |
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 (, or 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 . 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.
Recurrent.serialize turns a list of positions into rows followed by SEP;
Recurrent.step is one recurrent update. Recurrent.sep_resets: after SEP the
accumulator is , the summary is retained and the validity bit is set; rows never change the summary.
Recurrent.fold_invariant describes the outputs for any finite sequence of positions, including the
first position and empty positions (consecutive separators).
| Paper anchor | par-serialising-positions-and-retaining-state-p1 (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 5.5, “Serialising positions and retaining state” |
| Claim | Serialisation: rows of each position, a separator, aligned indices; the separator resets only the accumulator |
| Coverage category | Checked definition or construction |
| Statement source | paper_jmlr.tex lines 827–834; SHA-256 of the normalised block source 1b991b2a8d9d385c… |
| Lean declarations |
|
| Explanations | explain/c-stream, formal/c-stream |
| Build evidence | fresh isolated rebuild, audit report |
Recurrent.serializeSerialise positions: rows then SEP, position after position.
Statement as elaborated and printed by Lean 4.26.0
List (List ℕ) → List NimAudit.Recurrent.Token57/-- Serialise positions: rows then SEP, position after position. -/58def serialize (Ps : List (List Nat)) : List Token :=59 Ps.flatMap (fun P => P.map Token.row ++ [Token.sep])Project declarations in the statement: Recurrent.Token
Recurrent.stepOne recurrent update; SEP produces an output.
Statement as elaborated and printed by Lean 4.26.0
NimAudit.Recurrent.State →
NimAudit.Recurrent.Token → NimAudit.Recurrent.State × Option NimAudit.Recurrent.Out47/-- One recurrent update; SEP produces an output. -/48def step (s : State) : Token → State × Option Out49 | .row x => (⟨s.acc ^^^ x, s.prev, s.valid⟩, none)50 | .sep => (⟨0, s.acc, true⟩, some ⟨s.acc, if s.valid then some (s.prev ^^^ s.acc) else none⟩)Project declarations in the statement: Recurrent.Out, Recurrent.State, Recurrent.Token
Recurrent.Out, Recurrent.Out.mk, Recurrent.State, Recurrent.State.acc, Recurrent.State.mk, Recurrent.State.prev, Recurrent.State.valid, Recurrent.Token, Recurrent.Token.casesOn, Recurrent.Token.row, Recurrent.Token.sep
Recurrent.sep_resetsRESET BEHAVIOUR: after SEP the accumulator is 0, the summary is retained and the validity bit is set; rows never change prev or valid.
Statement as elaborated and printed by Lean 4.26.0
∀ (s : NimAudit.Recurrent.State),
(NimAudit.Recurrent.step s NimAudit.Recurrent.Token.sep).1 =
{ acc := 0, prev := s.acc, valid := true }130/-- RESET BEHAVIOUR: after SEP the accumulator is 0, the summary is retained and the131 validity bit is set; rows never change prev or valid. -/132theorem sep_resets (s : State) :133 (step s Token.sep).1 = ⟨0, s.acc, true⟩ := rflProject declarations in the statement: Recurrent.Out, Recurrent.State, Recurrent.State.acc, Recurrent.State.mk, Recurrent.Token.sep, Recurrent.step
Recurrent.Out, Recurrent.State, Recurrent.Token.sep, Recurrent.step
Recurrent.fold_invariantFOLD INVARIANT. From any state with empty accumulator, for ANY finite sequence of positions (empty positions allowed): the t-th output is (sigma(P_t), Delta) where Delta = prev XOR sigma(P_1) if the starting state is valid (none otherwise) for t = 1 and sigma(P_{t-1}) XOR sigma(P_t) for t ≥ 2; the final state retains the last summary with valid = true and acc = 0.
Statement as elaborated and printed by Lean 4.26.0
∀ (s : NimAudit.Recurrent.State),
s.acc = 0 →
∀ (Ps : List (List ℕ)),
NimAudit.Recurrent.run s (NimAudit.Recurrent.serialize Ps) =
(NimAudit.Recurrent.expectedState s Ps, NimAudit.Recurrent.expectedOuts s.valid s.prev Ps)95/-- FOLD INVARIANT. From any state with empty accumulator, for ANY finite sequence96 of positions (empty positions allowed): the t-th output is97 (sigma(P_t), Delta) where Delta = prev XOR sigma(P_1) if the starting state is98 valid (none otherwise) for t = 1 and sigma(P_{t-1}) XOR sigma(P_t) for t ≥ 2;99 the final state retains the last summary with valid = true and acc = 0. -/100theorem fold_invariant (s : State) (hs : s.acc = 0) (Ps : List (List Nat)) :101 run s (serialize Ps) = (expectedState s Ps, expectedOuts s.valid s.prev Ps) := by102 induction Ps generalizing s with103 | nil => simp [serialize, run, expectedState, expectedOuts]104 | cons P Ps ih =>105 have e : serialize (P :: Ps) = (P.map Token.row ++ [Token.sep]) ++ serialize Ps := by106 simp [serialize]107 rw [e, run_append, run_position, hs, Nat.zero_xor]108 rw [ih ⟨0, nimSum P, true⟩ rfl]109 simp [expectedState, expectedOuts]Project declarations in the statement: Recurrent.Out, Recurrent.State, Recurrent.State.acc, Recurrent.State.prev, Recurrent.State.valid, Recurrent.expectedOuts, Recurrent.expectedState, Recurrent.run, Recurrent.serialize
Recurrent.Out, Recurrent.Out.mk, Recurrent.State, Recurrent.State.acc, Recurrent.State.mk, Recurrent.State.prev, Recurrent.State.valid, Recurrent.Token, Recurrent.Token.row, Recurrent.Token.sep, Recurrent.expectedOuts, Recurrent.expectedState, Recurrent.run, Recurrent.run_append, Recurrent.run_position, Recurrent.serialize, nimSum
Recurrent.TokenStatement as elaborated and printed by Lean 4.26.0
TypeProject declarations in the statement: none
none
Recurrent.OutStatement as elaborated and printed by Lean 4.26.0
TypeProject declarations in the statement: none
none
Recurrent.StateStatement as elaborated and printed by Lean 4.26.0
TypeProject declarations in the statement: none
none
Recurrent.State.accStatement as elaborated and printed by Lean 4.26.0
NimAudit.Recurrent.State → ℕ37 acc : NatProject declarations in the statement: Recurrent.State
Recurrent.State.prevStatement as elaborated and printed by Lean 4.26.0
NimAudit.Recurrent.State → ℕ38 prev : NatProject declarations in the statement: Recurrent.State
Recurrent.State.validStatement as elaborated and printed by Lean 4.26.0
NimAudit.Recurrent.State → Bool39 valid : BoolProject declarations in the statement: Recurrent.State
Recurrent.expectedOutsExpected 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.Out84/-- 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) PsProject declarations in the statement: Recurrent.Out
Recurrent.expectedStateExpected final state.
Statement as elaborated and printed by Lean 4.26.0
NimAudit.Recurrent.State → List (List ℕ) → NimAudit.Recurrent.State90/-- Expected final state. -/91def expectedState : State → List (List Nat) → State92 | s, [] => s93 | _, P :: Ps => expectedState ⟨0, nimSum P, true⟩ PsProject declarations in the statement: Recurrent.State
Recurrent.runRun the recurrence over a token list, collecting outputs.
Statement as elaborated and printed by Lean 4.26.0
NimAudit.Recurrent.State →
List NimAudit.Recurrent.Token → NimAudit.Recurrent.State × List NimAudit.Recurrent.Out52/-- Run the recurrence over a token list, collecting outputs. -/53def run : State → List Token → State × List Out54 | s, [] => (s, [])55 | s, t :: ts => ((run (step s t).1 ts).1, (step s t).2.toList ++ (run (step s t).1 ts).2)Project declarations in the statement: Recurrent.Out, Recurrent.State, Recurrent.Token
Recurrent.Out, Recurrent.State, Recurrent.Token, Recurrent.step
| Module | File | Lines | Imports |
|---|---|---|---|
| NimRecurrent | lean/phase3/NimRecurrent.lean | 555 | NimAttain, Circuit |
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).