Section 3, “Circuit complexity and neural networks”Related results on parity, threshold circuits and attention models

External cited result A published result used as background or input; not proved in Lean here.

1 Paper text

Circuit complexity and neural networks. Parity is outside $\AC^0$ (Furst et al., 1984; Håstad, 1986), while constant-depth threshold circuits ( $\TC^0$ ) can compute it. Attention results depend on the precise model: Hao, Angluin and Frank analyse hard-attention variants, including $\AC^0$ restrictions for unique hard attention (Hao et al., 2022). Merrill and Sabharwal study the additional power of intermediate decoding over a $\TC^0$ baseline (Merrill and Sabharwal, 2024); that containment does not rule out parity. Their sequential-computation perspective is relevant to our recurrent bypass, although the architectures and formal assumptions differ. Our contribution applies these distinctions to NIM policies and a restricted rollout-measurement interface.

Generated from paper_jmlr.tex, lines 380–383.

2 Explain this

Related work on circuits and neural models: parity is outside AC⁰ but inside $\mathrm{TC}^0$ ; results on attention depend on the exact model (hard attention can be in AC⁰; other variants have $\mathrm{TC}^0$ bounds that do not rule out parity). The sequential-computation view of chain-of-thought work is mentioned because it resembles the recurrent bypass, though the formal settings differ.

3 How this is formalised

Cited literature, not formalised here. The paper's own use of these distinctions is in Theorem 2.4 and Proposition 5.13.

Coverage record
Paper anchor	`par-circuit-complexity-and-neural-networks-p1` (website anchor; the manuscript has no label here)
Displayed as	Section 3, “Circuit complexity and neural networks”
Claim	Related results on parity, threshold circuits and attention models
Coverage category	External cited result
Statement source	paper_jmlr.tex lines 380–383; SHA-256 of the normalised block source `e47d558f65a93f01…`
Explanations	`explain/c-rw-circuits`, `formal/c-rw-circuits`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

No Lean statement corresponds to this claim. This is a published classical result. It is cited, not proved in this Lean development.

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).