Figure 4Resource table for the three bypasses

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

1 Paper text

Resource	What stays in $\AC^0$	Additional information or time
One structured channel	Policy step and final readout	One complete rollout; one invariant bit
$B$ structured channels	Each policy step; reconstruction and move selection	$B$ complete rollouts supply all invariant bits
Two-frame transition	Local difference and binary move selection	Previous zero-nim-sum board and a legal transition
Persistent row scan	One state update and its output bits	Two scans per decision; $O(B+\log N)$ state bits

Figure 4: The three bypasses use different resources. Conditional restoration does not classify arbitrary starting positions; the rollout and recurrent constructions supply additional sequential computation.

Generated from paper_jmlr.tex, lines 786–800.

2 Explain this

The table compares what each bypass keeps shallow and what it adds:

one structured channel: a shallow step and readout, but one complete rollout gives only one invariant bit;
$B$ channels: still shallow steps, but $B$ complete rollouts supply all bits;
two frames: shallow difference and selection, given a previous zero-nim-sum board and a legal transition;
persistent row scan: one shallow update, but two scans per decision and $O(B+\log N)$ state bits.

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).
Theorem on single-frame inference
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.
worked restoration
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(2^B − 1)
Each policy step, tick and the readout is shallow; the rollouts supply the nim-sum bits.
worked rollouts
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.
worked recurrence

All three routes use shallow (AC⁰) components. The complete rollout and recurrent board-to-move computations are not AC⁰ families, given the named classical input that parity is not in AC⁰: 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 $\mathrm{AC}^0$ families, assuming the named classical input that parity is not in $\mathrm{AC}^0$ (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.

Depicted in Lean: Bypass.prop_bypass_interfaces, Bypass.bypass_barriers. Explains the paper’s Figure 4.

Schematic: nothing on this panel is computed; the numbers are the bounds stated in the paper.

3 How this is formalised

A summary table. Its entries are covered by Proposition 5.10, Proposition 5.9, Section 5.3.1, paragraph 2, Section 5.5, “From a summary to a move” and Proposition 5.14.

Coverage record
Paper anchor	`fig:rollout_gap` (manuscript label)
Displayed as	Figure 4
Claim	Resource table for the three bypasses
Coverage category	Informal interpretation
Statement source	paper_jmlr.tex lines 786–800; SHA-256 of the normalised block source `c144c2a208289732…`
Depends on	Proposition 5.14, Proposition 5.10, Proposition 5.9
Explanations	`explain/fig:rollout_gap`, `formal/fig:rollout_gap`
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).

Figure 4Resource table for the three bypasses

1 Paper text

2 Explain this

The three bypasses side by side

One frame, one evaluation

Two-frame restoration

Multi-head rollouts

Row-wise recurrence

3 How this is formalised

4 Lean statement and source