Section 2.1, “Circuit complexity primer”Circuit-complexity background: PARITY ∉ AC0, TC0 computes parity, fixed scale collapses to AC0
External cited result A published result used as background or input; not proved in Lean here.
1 Paper text
Circuit complexity primer. is the class of Boolean functions computable by constant-depth, polynomial-size circuits with unbounded fan-in AND/OR/NOT gates. A classical result is that . In contrast, augments with unbounded fan-in threshold gates and can compute parity. Our focus here is a fixed-scale quantised regime in which thresholds do not scale with fan-in; in that regime, each threshold unit admits a constant-witness DNF expansion and the overall computation collapses to (Theorem 2.4).
Generated from paper_jmlr.tex, lines 355–356.
2 Explain this
Background in one paragraph: AC0 is constant depth, polynomial size, unbounded fan-in AND, OR and NOT; PARITY is not in AC0 (a classical theorem); TC0 adds threshold gates of unbounded fan-in and can compute parity. In the fixed-scale regime each threshold unit has a constant-size witness, so the computation collapses to AC0.
3 How this is formalised
The definitions and the PARITY lower bound are classical background (the lower bound enters Lean as the named
input HastadNegl, Remark 2.3 (global parity)). The collapse statement is
Theorem 2.4.
| Paper anchor | c-primer (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 2.1, “Circuit complexity primer” |
| Claim | Circuit-complexity background: PARITY ∉ AC0, TC0 computes parity, fixed scale collapses to AC0 |
| Coverage category | External cited result |
| Statement source | paper_jmlr.tex lines 355–356; SHA-256 of the normalised block source 93fabe384e22e9ff… |
| Depends on | Theorem 2.4, Remark 2.3 (global parity) |
| Explanations | explain/c-primer, formal/c-primer |
| 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).