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

Section 1, paragraph 6AC0 representability is necessary within the restricted model, not sufficient for training and not universal

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

1 Paper text

The value of identifying a bottleneck is that it tells us what an architectural change must supply. Instead of asking a shallow network to rediscover a global invariant from every board, we can expose a useful transition, obtain complementary information from rollouts, or accumulate the invariant over time. Our contribution is this barrier-to-bypass approach: a computational obstruction guides three concrete constructions. Representability in AC0\AC^0 is a necessary condition for a fixed-latency computation in our restricted model; it is neither sufficient for successful training nor a universal condition on what neural networks can learn.

Generated from paper_jmlr.tex, lines 93–93.

2 Explain this

This sentence states the logical role of AC0 in the paper.

  • Necessary within the model. By Theorem 2.4, anything a fixed-latency network of the restricted kind can compute is in AC0. So if a decision rule is provably not in AC0, no such network can implement it.
  • Not sufficient for training. A function can be in AC0 and still be hard to learn by gradient descent or self-play.
  • Not universal. Networks outside the model (scale-adaptive thresholds, growing depth, ordinary floating-point layers) are not constrained by this argument.

The "barrier-to-bypass" idea is to use the obstruction constructively: it tells us what an architecture must add.

3 How this is formalised

This is an interpretation of Theorem 2.4. The formal content is that theorem (checked in Lean, see Theorem 2.4); the statements about training and about networks outside the model are deliberately not formal claims.

Coverage record
Paper anchorc-intro-necessary (website anchor; the manuscript has no label here)
Displayed asSection 1, paragraph 6
ClaimAC0 representability is necessary within the restricted model, not sufficient for training and not universal
Coverage categoryInformal interpretation
Statement sourcepaper_jmlr.tex lines 93–93; SHA-256 of the normalised block source 65533ae04feda29a…
Depends onTheorem 2.4
Explanationsexplain/c-intro-necessary, formal/c-intro-necessary
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).