Remark 2.2 (model scope)The model has bounded thresholds; a fan-in-dependent threshold such as majority lies outside it
Checked definition or constructionLean contains the definition or construction, with checked properties.
1 Paper text
Remark 2.2(Scope of the AC0 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 with W,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 n. Allowing such scale-adaptive behaviour leads naturally to richer threshold-circuit models (e.g. TC0), in which parity-like computations can become representable.
Generated from paper_jmlr.tex, lines 320–327.
2 Explain this
The remark says what the abstraction deliberately leaves out: fan-in-dependent re-scaling, large signed biases
that grow with dimension, and computations whose depth grows with n.
Concrete example: majority of m bits is a threshold gate with all weights 1 and threshold ⌈m/2⌉.
Its weights are on the grid, but its threshold grows with m. So majority is not in the model once m>2W, even
though "all coefficients lie in a finite set". This is why the model bounds thresholds, not only weights.
3 How this is formalised
Windows.majGate_not_valid: for every W and every m>2W, the {0,1}-coefficient majority gate
Windows.majGate is not valid for the grid bound W (AC0.Gate.Valid). This checks
the precise reason why finite coefficient sets alone do not give the constant-witness property.
The remark describes what the model leaves out. Lean checks the precise boundary case: a majority gate with coefficients in {0,1} has threshold ⌈m/2⌉, which exceeds every fixed W once m>2W.
Module Windows
(lean/phase6/Windows.lean, lines 193–197) · file SHA-256 ff59ec8bf0a0de70…Axioms reported by the fresh build: propext, Quot.sound
Finite coefficients are not enough: the majority gate's threshold exceeds every fixed
W once m > 2W, so it is outside the fixed-scale model although all its coefficients
lie in {0,1}.
Statement as elaborated and printed by Lean 4.26.0
∀ (W m : ℕ), 2 * W < m → ¬NimAudit.AC0.Gate.Valid W (NimAudit.Windows.majGate m)
Exact source text, lines 193–197
193/-- Finite coefficients are not enough: the majority gate's threshold exceeds every fixed194 W once m > 2W, so it is outside the fixed-scale model although all its coefficients195 lie in {0,1}. -/196theorem majGate_not_valid (W m : Nat) (hm : 2 * W < m) : ¬ Gate.Valid W (majGate m) := by197 intro h; have := h.1; simp [majGate] at this; omega
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).