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

Section 5.4, paragraph 1Restatement of the single-frame barrier as the motivation for rollouts

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

1 Paper text

Theorem 5.2 shows that no AC0\AC^0 circuit can evaluate the nim-sum in a single forward pass. A natural follow-up is whether planning—testing candidate moves and simulating play, as in Monte-Carlo Tree Search (MCTS)—can compensate.

Generated from paper_jmlr.tex, lines 627–628.

2 Explain this

The single-frame barrier rules out computing the needed invariant in one shallow pass. The natural next question is whether planning (simulating play) can make up for it. This subsection studies a deliberately simple planning interface to answer that question precisely.

3 How this is formalised

A restatement of Theorem 5.2 (barrier), whose precise content is winning-move selection on the encoded family; the paper's phrase "evaluate the nim-sum" is the informal reading of that result.

Coverage record
Paper anchorsec:search-gap-p1 (website anchor; the manuscript has no label here)
Displayed asSection 5.4, paragraph 1
ClaimRestatement of the single-frame barrier as the motivation for rollouts
Coverage categoryInformal interpretation
Statement sourcepaper_jmlr.tex lines 627–628; SHA-256 of the normalised block source a5063fd156793c21…
Depends onTheorem 5.2 (barrier)
Explanationsexplain/c-search-intro, formal/c-search-intro
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).