Lemma B.3A layer of polynomially many fixed-scale units is simulated with constant depth and polynomial size

Checked theorem Lean checks a formal statement corresponding to this claim.

1 Paper text

Lemma B.3 (One layer of fixed-scale quantised units is in $\AC^0$ ) Fix $W,D$ and let a layer consist of $m'$ threshold units whose inputs are outputs of a previous layer of width $m$ , with $m,m'\le \poly(n)$ . Then the layer can be simulated by an $\AC^0$ circuit of constant depth and polynomial size.

Generated from paper_jmlr.tex, lines 1448–1452.

2 Explain this

A layer is $m'$ units side by side. Apply the one-unit lemma to each and place the circuits in parallel: depth stays $2$ and size is $m'\cdot O(m^K)$ , polynomial. Composing a constant number of layers then proves Theorem 2.4.

3 How this is formalised

AC0.eval_compileLayer: substituting the previous layer's formulas into each gate's DNF computes the layer (AC0.compileLayer).
AC0.compileLayer_size: each output's size is at most $G\cdot(S+1)$ with $G=1+(M+1)^W(2W+1)$ , for previous formulas of size at most $S$ and fan-in at most $M$ .
AC0.compileLayer_depth: depth grows by at most $3$ per layer.

Coverage record
Paper anchor	`lem:layer-ac0` (manuscript label)
Displayed as	Lemma B.3
Claim	A layer of polynomially many fixed-scale units is simulated with constant depth and polynomial size
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 1448–1452; SHA-256 of the normalised block source `97b5b3b24707126b…`
Lean declarations	`NimAudit.AC0.eval_compileLayer` (Circuit, lines 771–779, file `af97cc0eec7d…`) `NimAudit.AC0.compileLayer_size` (Circuit, lines 801–816, file `af97cc0eec7d…`) `NimAudit.AC0.compileLayer_depth` (Circuit, lines 818–827, file `af97cc0eec7d…`)
Audited correspondence rows	`lem:layer-ac0`, `app:network`
Explanations	`explain/lem:layer-ac0`, `formal/lem:layer-ac0`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `AC0.eval_compileLayer`

Module Circuit (lean/phase3/Circuit.lean, lines 771–779) · file SHA-256 af97cc0eec7d8464… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

Statement as elaborated and printed by Lean 4.26.0

∀ {W : ℕ} (l : NimAudit.AC0.Layer),
  (∀ g ∈ l, NimAudit.AC0.Gate.Valid W g) →
    ∀ (prev : ℕ → NimAudit.AC0.Circ) (x : ℕ → Bool) (i : ℕ),
      NimAudit.AC0.Circ.eval x (NimAudit.AC0.compileLayer W l prev i) =
        NimAudit.AC0.evalLayer l (fun j => NimAudit.AC0.Circ.eval x (prev j)) i

Exact source text, lines 771–779

771theorem eval_compileLayer {W : Nat} (l : Layer) (hv : ∀ g ∈ l, Gate.Valid W g)772    (prev : Nat → Circ) (x : Nat → Bool) (i : Nat) :773    eval x (compileLayer W l prev i) = evalLayer l (fun j => eval x (prev j)) i := by774  unfold compileLayer evalLayer775  cases h : l[i]? with776  | none => simp777  | some g =>778    simp only779    rw [eval_subst, eval_dnf g (hv g (List.mem_of_getElem? h)).1]

Project declarations in the statement: AC0.Circ, AC0.Circ.eval, AC0.Gate, AC0.Gate.Valid, AC0.Layer, AC0.compileLayer, AC0.evalLayer

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.const, AC0.Circ.eval, AC0.Circ.eval_const, AC0.Circ.eval_subst, AC0.Circ.subst, AC0.Gate, AC0.Gate.Valid, AC0.Gate.coeffs, AC0.Gate.eval, AC0.Gate.thr, AC0.Layer, AC0.compileLayer, AC0.dnf, AC0.evalLayer, AC0.eval_dnf

theorem `AC0.compileLayer_size`

Module Circuit (lean/phase3/Circuit.lean, lines 801–816) · file SHA-256 af97cc0eec7d8464… Axioms reported by the fresh build: propext, Quot.sound

Statement as elaborated and printed by Lean 4.26.0

∀ {W M S : ℕ} (l : NimAudit.AC0.Layer),
  (∀ g ∈ l, g.fanin ≤ M) →
    ∀ (prev : ℕ → NimAudit.AC0.Circ),
      (∀ (j : ℕ), (prev j).size ≤ S) →
        ∀ (i : ℕ), (NimAudit.AC0.compileLayer W l prev i).size ≤ NimAudit.AC0.gfac W M * (S + 1)

Exact source text, lines 801–816

801theorem compileLayer_size {W M S : Nat} (l : Layer) (hb : ∀ g ∈ l, g.fanin ≤ M)802    (prev : Nat → Circ) (hp : ∀ j, size (prev j) ≤ S) (i : Nat) :803    size (compileLayer W l prev i) ≤ gfac W M * (S + 1) := by804  unfold compileLayer805  cases h : l[i]? with806  | none => simp only; simp; have : 1 ≤ gfac W M := by unfold gfac; omega807            exact Nat.le_trans this (Nat.le_mul_of_pos_right _ (by omega))808  | some g =>809    simp only810    have h1 := size_subst_le prev S hp (dnf W g)811    have h2 := size_dnf W g812    have hf := hb g (List.mem_of_getElem? h)813    have h3 : (g.fanin + 1) ^ W ≤ (M + 1) ^ W := Nat.pow_le_pow_left (by omega) W814    have h4 : size (dnf W g) ≤ gfac W M := by815      unfold gfac; have := Nat.mul_le_mul_right (2 * W + 1) h3; omega816    exact Nat.le_trans h1 (Nat.mul_le_mul_right _ h4)

Project declarations in the statement: AC0.Circ, AC0.Circ.size, AC0.Gate, AC0.Gate.fanin, AC0.Layer, AC0.compileLayer, AC0.gfac

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.const, AC0.Circ.size, AC0.Circ.size_const, AC0.Circ.size_subst_le, AC0.Circ.subst, AC0.Gate, AC0.Gate.fanin, AC0.Layer, AC0.compileLayer, AC0.dnf, AC0.gfac, AC0.size_dnf

theorem `AC0.compileLayer_depth`

Module Circuit (lean/phase3/Circuit.lean, lines 818–827) · file SHA-256 af97cc0eec7d8464… Axioms reported by the fresh build: propext, Quot.sound

Statement as elaborated and printed by Lean 4.26.0

∀ {W D : ℕ} (l : NimAudit.AC0.Layer) (prev : ℕ → NimAudit.AC0.Circ),
  (∀ (j : ℕ), (prev j).depth ≤ D) → ∀ (i : ℕ), (NimAudit.AC0.compileLayer W l prev i).depth ≤ D + 3

Exact source text, lines 818–827

818theorem compileLayer_depth {W D : Nat} (l : Layer) (prev : Nat → Circ)819    (hp : ∀ j, depth (prev j) ≤ D) (i : Nat) : depth (compileLayer W l prev i) ≤ D + 3 := by820  unfold compileLayer821  cases h : l[i]? with822  | none => simp823  | some g =>824    simp only825    have h1 := depth_subst_le prev D hp (dnf W g)826    have h2 := depth_dnf W g827    omega

Project declarations in the statement: AC0.Circ, AC0.Circ.depth, AC0.Layer, AC0.compileLayer

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.const, AC0.Circ.depth, AC0.Circ.depth_const, AC0.Circ.depth_subst_le, AC0.Circ.subst, AC0.Gate, AC0.Layer, AC0.compileLayer, AC0.depth_dnf, AC0.dnf

Definitions these statements use

def `AC0.compileLayer`

Module Circuit (lean/phase3/Circuit.lean, lines 756–759) · file SHA-256 af97cc0eec7d8464…

Statement as elaborated and printed by Lean 4.26.0

ℕ → NimAudit.AC0.Layer → (ℕ → NimAudit.AC0.Circ) → ℕ → NimAudit.AC0.Circ

Exact source text, lines 756–759

756def compileLayer (W : Nat) (l : Layer) (prev : Nat → Circ) : Nat → Circ :=757  fun i => match l[i]? with758    | some g => subst prev (dnf W g)759    | none => const false

Project declarations in the statement: AC0.Circ, AC0.Layer

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.const, AC0.Circ.subst, AC0.Gate, AC0.Layer, AC0.dnf

inductive `AC0.Circ`

Module Circuit (lean/phase3/Circuit.lean, lines 35–40) · file SHA-256 af97cc0eec7d8464…

Statement as elaborated and printed by Lean 4.26.0

Type

Exact source text, lines 35–40

35inductive Circ where36  | input (i : Nat)37  | const (b : Bool)38  | not (c : Circ)39  | and (cs : List Circ)40  | or (cs : List Circ)

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `AC0.Circ.eval`

Module Circuit (lean/phase3/Circuit.lean, lines 44–49) · file SHA-256 af97cc0eec7d8464…

Statement as elaborated and printed by Lean 4.26.0

(ℕ → Bool) → NimAudit.AC0.Circ → Bool

Exact source text, lines 44–49

44def eval (x : Nat → Bool) : Circ → Bool45  | input i => x i46  | const b => b47  | not c => !(eval x c)48  | and cs => cs.attach.all (fun ⟨c, _⟩ => eval x c)49  | or cs => cs.attach.any (fun ⟨c, _⟩ => eval x c)

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.and, AC0.Circ.casesOn, AC0.Circ.const, AC0.Circ.input, AC0.Circ.not, AC0.Circ.or, AC0.Circ.rec, AC0.Circ.rec_1

inductive `AC0.Gate`

Module Circuit (lean/phase3/Circuit.lean, lines 326–331) · file SHA-256 af97cc0eec7d8464…

A literal-threshold gate after clearing denominators: coefficients a_j, negation bits eta_j, threshold b. Its fan-in is `coeffs.length`.

Statement as elaborated and printed by Lean 4.26.0

Type

Exact source text, lines 326–331

326/-- A literal-threshold gate after clearing denominators: coefficients a_j,327    negation bits eta_j, threshold b.  Its fan-in is `coeffs.length`. -/328structure Gate where329  coeffs : List Nat330  negs : List Bool331  thr : Nat

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `AC0.Gate.Valid`

Module Circuit (lean/phase3/Circuit.lean, lines 348–349) · file SHA-256 af97cc0eec7d8464…

Fixed-scale validity: threshold and coefficients in 0..W.

Statement as elaborated and printed by Lean 4.26.0

ℕ → NimAudit.AC0.Gate → Prop

Exact source text, lines 348–349

348/-- Fixed-scale validity: threshold and coefficients in 0..W. -/349def Valid (W : Nat) (g : Gate) : Prop := g.thr ≤ W ∧ ∀ a ∈ g.coeffs, a ≤ W

Project declarations in the statement: AC0.Gate

Project declarations used by the proof or definition body

AC0.Gate, AC0.Gate.coeffs, AC0.Gate.thr

def `AC0.Layer`

Module Circuit (lean/phase3/Circuit.lean, lines 743–744) · file SHA-256 af97cc0eec7d8464…

A layer: a list of gates reading the previous layer's outputs (indexed by Nat).

Statement as elaborated and printed by Lean 4.26.0

Type

Exact source text, lines 743–744

743/-- A layer: a list of gates reading the previous layer's outputs (indexed by Nat). -/744abbrev Layer := List Gate

Project declarations in the statement: none

Project declarations used by the proof or definition body

AC0.Gate

def `AC0.evalLayer`

Module Circuit (lean/phase3/Circuit.lean, lines 746–749) · file SHA-256 af97cc0eec7d8464…

Statement as elaborated and printed by Lean 4.26.0

NimAudit.AC0.Layer → (ℕ → Bool) → ℕ → Bool

Exact source text, lines 746–749

746def evalLayer (l : Layer) (z : Nat → Bool) : Nat → Bool :=747  fun i => match l[i]? with748    | some g => g.eval z749    | none => false

Project declarations in the statement: AC0.Layer

Project declarations used by the proof or definition body

AC0.Gate, AC0.Gate.eval, AC0.Layer

def `AC0.Circ.size`

Module Circuit (lean/phase3/Circuit.lean, lines 51–56) · file SHA-256 af97cc0eec7d8464…

Statement as elaborated and printed by Lean 4.26.0

NimAudit.AC0.Circ → ℕ

Exact source text, lines 51–56

51def size : Circ → Nat52  | input _ => 153  | const _ => 154  | not c => size c + 155  | and cs => (cs.attach.map (fun ⟨c, _⟩ => size c)).sum + 156  | or cs => (cs.attach.map (fun ⟨c, _⟩ => size c)).sum + 1

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.and, AC0.Circ.casesOn, AC0.Circ.const, AC0.Circ.input, AC0.Circ.not, AC0.Circ.or, AC0.Circ.rec, AC0.Circ.rec_1

def `AC0.Gate.fanin`

Module Circuit (lean/phase3/Circuit.lean, lines 335–335) · file SHA-256 af97cc0eec7d8464…

Statement as elaborated and printed by Lean 4.26.0

NimAudit.AC0.Gate → ℕ

Exact source text, lines 335–335

335def fanin (g : Gate) : Nat := g.coeffs.length

Project declarations in the statement: AC0.Gate

Project declarations used by the proof or definition body

AC0.Gate, AC0.Gate.coeffs

def `AC0.gfac`

Module Circuit (lean/phase3/Circuit.lean, lines 793–794) · file SHA-256 af97cc0eec7d8464…

Per-layer size factor G = 1 + (M+1)^W (2W+1).

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → ℕ

Exact source text, lines 793–794

793/-- Per-layer size factor G = 1 + (M+1)^W (2W+1). -/794def gfac (W M : Nat) : Nat := 1 + (M + 1) ^ W * (2 * W + 1)

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `AC0.Circ.depth`

Module Circuit (lean/phase3/Circuit.lean, lines 61–66) · file SHA-256 af97cc0eec7d8464…

Statement as elaborated and printed by Lean 4.26.0

NimAudit.AC0.Circ → ℕ

Exact source text, lines 61–66

61def depth : Circ → Nat62  | input _ => 063  | const _ => 064  | not c => depth c + 165  | and cs => listMax (cs.attach.map (fun ⟨c, _⟩ => depth c)) + 166  | or cs => listMax (cs.attach.map (fun ⟨c, _⟩ => depth c)) + 1

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.and, AC0.Circ.casesOn, AC0.Circ.const, AC0.Circ.input, AC0.Circ.listMax, AC0.Circ.not, AC0.Circ.or, AC0.Circ.rec, AC0.Circ.rec_1

Full modules

Module	File	Lines	Imports
Circuit	`lean/phase3/Circuit.lean`	1151	NimProbability

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

Lemma B.3A layer of polynomially many fixed-scale units is simulated with constant depth and polynomial size

1 Paper text

2 Explain this

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem AC0.eval_compileLayer

theorem AC0.compileLayer_size

theorem AC0.compileLayer_depth

Definitions these statements use

def AC0.compileLayer

inductive AC0.Circ

def AC0.Circ.eval

inductive AC0.Gate

def AC0.Gate.Valid

def AC0.Layer

def AC0.evalLayer

def AC0.Circ.size

def AC0.Gate.fanin

def AC0.gfac

def AC0.Circ.depth

Full modules

theorem `AC0.eval_compileLayer`

theorem `AC0.compileLayer_size`

theorem `AC0.compileLayer_depth`

def `AC0.compileLayer`

inductive `AC0.Circ`

def `AC0.Circ.eval`

inductive `AC0.Gate`

def `AC0.Gate.Valid`

def `AC0.Layer`

def `AC0.evalLayer`

def `AC0.Circ.size`

def `AC0.Gate.fanin`

def `AC0.gfac`

def `AC0.Circ.depth`