Section 9, paragraph 2Conclusion: what the three constructions supply
Informal interpretation Motivation, interpretation or scope; not a formal claim.
1 Paper text
Three constructions identify resources beyond that restricted inference problem. Two-frame access supports constant-depth restoration when the preceding position has nim-sum zero. Distinct structured rollout policies reveal complementary invariant bits; a single-channel limitation holds only under our explicit query and readout restrictions. Persistent recurrence implements running XOR over heap rows, exchanging fixed total latency for a growing sequence of simple updates. Cross-position memory additionally supports comparisons, while replay or board storage supplies the heaps needed for move selection.
Generated from paper_jmlr.tex, lines 1278–1278.
2 Explain this
The second paragraph summarises what the constructions supply: two-frame access gives constant-depth restoration when the preceding position has nim-sum zero; distinct structured rollout policies reveal complementary invariant bits, with a single-channel limitation only under the explicit query and readout restrictions; persistent recurrence implements running XOR over heap rows, trading fixed total latency for a growing number of simple updates; cross-position memory supports comparisons; replay or board storage supplies the heaps needed for move selection.
The three bypasses side by side
Schematic Boxes summarise resources or group operations; they are not gates, layers or measurements.
In the restricted model, no family of polynomial-size, fixed-depth networks that reads only the current board strongly masters NIM (Theorem 5.2, which uses the named classical input on parity). Each bypass adds a different resource: an extra frame and a promise, executed rollouts, or a growing number of recurrent updates. This schematic summarises Figure 4 and Proposition 5.14; each bypass column links to a worked, exact construction.
One frame, one evaluation
- Input
- the current board
- Kept state
- none
- Sequential time per decision
- 1 evaluation
In the restricted model no such network family strongly masters NIM: it would give a shallow circuit for parity (using the named classical input on parity).
Two-frame restoration
- Input
- previous zero-nim-sum board and current board
- Kept state
- the restored board, kept as the next previous frame
- Sequential time per decision
- 1 evaluation per decision
Shallow selector (Boolean depth ≤ 20). Maintains a winning position once established; does not find the first winning move.
Multi-head rollouts
- Input
- the current board (read-only); the controller runs the B rollouts itself
- Kept state
- working board, head index, outcome bits
- Sequential time per decision
- M + 2B + 2 evaluations, M ≤ BN(2B − 1)
Each policy step, tick and the readout is shallow; the rollouts supply the nim-sum bits.
Row-wise recurrence
- Input
- the board as a stream of rows, supplied twice (board storage: once)
- Kept state
- O(B + log N) bits: summary, counter, candidate (board storage: NB + B + r bits)
- Sequential time per decision
- 2N + 2 updates (board storage: N + 1)
Each update is shallow (Boolean depth ≤ 8); the number of updates grows with N.
All three routes use shallow (AC0) components. The complete rollout and recurrent board-to-move computations are not AC0 families, given the named classical input that parity is not in AC0: otherwise they would give shallow parity circuits. Their sequential time grows with the board; that growing computation is the resource the single-frame model lacks. The two-frame route instead changes the input and relies on a promise.
How this relates to the Lean proof. Bypass.prop_bypass_interfaces packages the three
constructions with their shallow components and complete winning strategies;
Bypass.bypass_barriers records why the complete rollout and recurrent maps cannot themselves be
families, assuming the named classical input that parity is not in
(Barrier.ParityNotAC0).
What this does not show. Nothing here claims that self-play training discovers these constructions, and the restricted model is not a model of every neural network.
3 How this is formalised
A summary of Proposition 5.14, Theorem 5.12 (i), Section 5.5, “From a summary to a move” and Section 5.5, “From a summary to a move”.
| Paper anchor | sec:conclusion-p2 (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 9, paragraph 2 |
| Claim | Conclusion: what the three constructions supply |
| Coverage category | Informal interpretation |
| Statement source | paper_jmlr.tex lines 1278–1278; SHA-256 of the normalised block source 1a0bd11281cdd207… |
| Depends on | Proposition 5.14, Theorem 5.12 (i) |
| Explanations | explain/c-conclusion-bypasses, formal/c-conclusion-bypasses |
| Build evidence | fresh 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).