Section 9, paragraph 1Conclusion: AC0 simulation and the single-frame barrier, restated
Informal interpretation Motivation, interpretation or scope; not a formal claim.
1 Paper text
A fixed-depth Boolean literal-threshold model with nonnegative fixed-grid weights and bounded thresholds is simulable in . The NIM parity reduction then rules out strong single-frame mastery in that model.
Generated from paper_jmlr.tex, lines 1274–1276.
2 Explain this
The first conclusion paragraph restates the two main theorems: a fixed-depth Boolean literal-threshold model with nonnegative fixed-grid weights and bounded thresholds is simulable in AC0, and the NIM parity reduction then rules out strong single-frame mastery in that model.
3 How this is formalised
A restatement of Theorem 2.4 (checked) and Theorem 5.2 (barrier) (checked conditional on the
named classical input HastadNegl).
| Paper anchor | sec:conclusion-p1 (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 9, paragraph 1 |
| Claim | Conclusion: AC0 simulation and the single-frame barrier, restated |
| Coverage category | Informal interpretation |
| Statement source | paper_jmlr.tex lines 1274–1276; SHA-256 of the normalised block source 4821796746fb25bd… |
| Depends on | Theorem 2.4, Theorem 5.2 (barrier) |
| Explanations | explain/c-conclusion, formal/c-conclusion |
| 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).