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

Section 3, “History and memory in RL”History can reduce computational complexity even in fully observable games, given the zero-nim-sum promise

Informal interpretation Motivation, interpretation or scope; not a formal claim.

1 Paper text

History and memory in RL. Using short history windows is standard in partially observable settings, where stacked frames recover hidden variables such as velocity (Mnih et al., 2015). Our point is different and perhaps surprising: even in Markovian, fully observable games—where the current state is informationally sufficient and the past is theoretically irrelevant—history can reduce computational complexity by exposing local differences that would otherwise require expensive search or unbounded-depth inference to extract from the current state alone. In our restoration setting, the previous frame carries a promise established by an earlier successful move: its nim-sum is zero. That promise makes a local difference sufficient for the next response. Establishing the promise initially remains a separate computational task.

Generated from paper_jmlr.tex, lines 393–396.

2 Explain this

Frame stacking is usually justified by partial observability: velocity cannot be read off one frame. NIM is fully observable, so the previous board is informationally redundant. The point here is different: the previous board can still reduce the computation needed, because it carries a promise (its nim-sum is zero) established by an earlier correct move. Given that promise, the local difference is enough for the next reply.

Caveat: establishing the promise in the first place is a separate task (the initialisation boundary).

3 How this is formalised

An interpretive paragraph. The formal content is Proposition 5.5 (restoration under the promise) and Section 5.4, “The initialisation boundary for restoration” (why the promise matters).

Coverage record
Paper anchorpar-history-and-memory-in-rl-p1 (website anchor; the manuscript has no label here)
Displayed asSection 3, “History and memory in RL”
ClaimHistory can reduce computational complexity even in fully observable games, given the zero-nim-sum promise
Coverage categoryInformal interpretation
Statement sourcepaper_jmlr.tex lines 393–396; SHA-256 of the normalised block source 15c33f2f9ded8365…
Depends onProposition 5.5, Section 5.4, “The initialisation boundary for restoration”
Explanationsexplain/c-rw-history, formal/c-rw-history
Build evidencefresh isolated rebuild, audit report

4 Lean statement and source

No Lean statement corresponds to this claim. This is interpretation or motivation, not a formal mathematical claim.

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