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

Remark 2.2 (TC0)Scale-adaptive threshold circuits (TC0) can represent parity-like computations

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

1 Paper text

Remark 2.2 (Scope of the AC0\AC^0 abstraction) Theorem 2.4 formalises a fixed-latency fixed-scale quantised regime in which each unit uses parameters drawn from a bounded-range grid QW,D\Qset_{W,D} with W,DW,D independent of the input length. This yields the constant-witness property exploited in Lemma B.1.

The abstraction is deliberately conservative: it does not model architectures that rely on fan-in dependent re-scaling, numerically large signed biases/thresholds that grow with dimension, or deep computations whose depth scales with nn. Allowing such scale-adaptive behaviour leads naturally to richer threshold-circuit models (e.g. TC0\TC^0), in which parity-like computations can become representable.

Generated from paper_jmlr.tex, lines 320–327.

2 Explain this

Once thresholds may scale with fan-in, constant-depth threshold circuits (the class TC0\mathrm{TC}^0) can count and therefore compute parity. The remark mentions this to explain what the model excludes and why: the lower bound holds only for fixed-scale gates.

3 How this is formalised

A classical fact about threshold circuits, cited and not formalised here.

Coverage record
Paper anchorrem:ac0-scope (manuscript label)
Displayed asRemark 2.2 (TC0)
ClaimScale-adaptive threshold circuits (TC0) can represent parity-like computations
Coverage categoryExternal cited result
Statement sourcepaper_jmlr.tex lines 320–327; SHA-256 of the normalised block source 988fb4fd7142b64b…
Explanationsexplain/rem:ac0-scope.tc0, formal/rem:ac0-scope.tc0
Build evidencefresh 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).