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

Figure 1Schematic of the barrier and the three bypasses

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

1 Paper text

Four rows of boxes and arrows. (a) Barrier, single-frame, single-head: input P_t (global) feeds a single-head network whose output is marked with a cross, labelled "Cannot compute global parity in this model". (b) Bypass 1, multi-frame input: input (P_{t-1}, P_t) (transition) feeds a single-head network whose output is marked with a check, labelled "Computes local difference Delta". (c) Bypass 2, multiple rollout heads: input P_t splits into heads pi_0 through pi_{B-1}, which join at a check mark labelled "Rollout outcomes recover B bits". (d) Bypass 3, persistent recurrence: rows of P_t then P_{t+1} feed a recurrent state s <- s XOR x_i, ending at a check mark labelled "Nim-sum after N row updates (growing latency)".
Figure 1: The parity barrier and three structural bypasses. (a) Fixed-scale quantised inference (FSQI) with fixed latency cannot compute global parity across arbitrarily large boards. Here fixed latency means a bounded number of sequential computation steps, independent of board size. (b) Two frames expose Δ\Delta for restoration when the predecessor has nim-sum zero. (c) Distinct policy heads recover complementary information through complete rollouts. (d) Persistent recurrence accumulates the nim-sum row by row and retains summaries across positions. Each update has constant depth; the full scan has depth growing with NN.

Generated from paper_jmlr.tex, lines 104–215.

2 Explain this

Terminology. FSQI means fixed-scale quantised inference. Fixed latency means that the number of sequential computation steps stays bounded as the board grows, rather than a fixed measured running time in seconds.

The figure is a map of the paper. Row (a) is the obstruction: a single network that sees one board cannot compute global parity under the fixed-scale model. Rows (b)–(d) are the three bypasses, each supplying something different: (b) the transition between two boards, given a zero-nim-sum predecessor; (c) the outcomes of complete rollouts under several policy heads; (d) a recurrent state carried over many row updates, so that total latency grows with the number of heaps.

Caveat: a check mark in the figure means "this computation becomes available", not "learning succeeds".

3 How this is formalised

A schematic, not a formal statement. Each row corresponds to checked results: (a) Theorem 5.2 (barrier); (b) Proposition 5.5 and Section 5.3.1, paragraph 2; (c) Proposition 5.9; (d) Proposition 5.13 and Section 5.5, “From a summary to a move”.

Coverage record
Paper anchorfig:barrier-blueprint (manuscript label)
Displayed asFigure 1
ClaimSchematic of the barrier and the three bypasses
Coverage categoryInformal interpretation
Statement sourcepaper_jmlr.tex lines 104–215; SHA-256 of the normalised block source 06f62014098be66f…
Depends onTheorem 5.2 (barrier), Proposition 5.5, Proposition 5.9, Proposition 5.13
Explanationsexplain/fig:barrier-blueprint, formal/fig:barrier-blueprint
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).