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

Section 1, paragraph 8Shallow components versus the complete sequential computation in the three bypasses

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

1 Paper text

The central observation is that while the state can be hard to process, the transition can be easy: under the promise that the preceding position has nim-sum zero, short history converts winning-move selection into local difference computation and restoration. A second route uses distinct rollout policies to extract complementary bits of the invariant. A third route processes each position sequentially, retaining recurrent state as rows and then successive positions arrive. Here a sequence of simple updates computes the global invariant, and memory connects the new position to the preceding one. These mechanisms use different resources: explicit transition information, multiple rollout channels, or a growing recurrent computation horizon. The distinction between a shallow component and the complete computation is essential. Two-frame restoration is a shallow map on a promised pair of boards. In the other two constructions, each policy step or recurrent update is shallow, but generating the information needed for a decision takes a sequence of such steps. Thus the bypasses preserve simple network components while changing the input information or total processing time. The complete sequential computation need not itself lie in AC0\AC^0. Figure 1 summarises the three routes for NIM.

Generated from paper_jmlr.tex, lines 97–102.

2 Explain this

The key distinction. A state (a single NIM board) can be hard to process, while a transition (one board and the next) can be easy: if the previous board had nim-sum zero, the difference δ\delta that the reply must cancel depends only on the heap that changed, and a reply realising δ\delta is found by a separate local test on each heap.

Three routes. Two frames expose that transition; several rollout policies extract complementary bits of the invariant; a recurrent scan accumulates it row by row.

Shallow parts versus the whole computation. In all three routes each component is shallow. But the rollout and recurrent routes run a sequence of shallow steps whose number grows with the board, and the complete computation is not itself an AC0 circuit. That is how the bypasses coexist with the lower bound.

3 How this is formalised

An overview paragraph. Its precise counterparts are Proposition 5.5 (with Section 5.3.1, paragraph 2), Proposition 5.14 (shallow components and winning strategies) and Section 5.6, paragraph 1, which proves, conditional on the classical parity bound, that the complete multi-head and recurrent board-to-move maps are not AC0 families.

Coverage record
Paper anchorc-intro-transition (website anchor; the manuscript has no label here)
Displayed asSection 1, paragraph 8
ClaimShallow components versus the complete sequential computation in the three bypasses
Coverage categoryInformal interpretation
Statement sourcepaper_jmlr.tex lines 97–102; SHA-256 of the normalised block source 8dcd11f9c9d1749d…
Depends onProposition 5.5, Proposition 5.14, Section 5.6, paragraph 1
Explanationsexplain/c-intro-transition, formal/c-intro-transition
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).