Definition A.1Literal-threshold network: layers of gates with grid weights, grid thresholds and negation bits

Checked definition or construction Lean contains the definition or construction, with checked properties.

1 Paper text

Definition A.1 (Literal-threshold network) A fixed-scale quantised $\NN$ of depth $L$ on $n$ Boolean inputs is specified by:

Layer widths $m_0=n$ , $m_1,\dots,m_L$ , where $m_\ell\le \poly(n)$ .
For each layer $\ell\in\{1,\dots,L\}$ and unit $i\in\{1,\dots,m_\ell\}$ :
- weights $w_{\ell,i,j}\in \Qset_{W,D}$ for $j\in\{1,\dots,m_{\ell-1}\}$ ,
- a threshold $\theta_{\ell,i}\in \Qset_{W,D}$ ,
- an optional negation bit $\eta_{\ell,i,j}\in\{0,1\}$ indicating whether input $j$ is negated before weighting.

The computation proceeds as follows. Let $y^{(0)}=x\in\bits^n$ . For $\ell\ge 1$ , $y^{(\ell)}_i \;=\; \Heav\!\Big(\sum_{j=1}^{m_{\ell-1}} w_{\ell,i,j}\cdot (y^{(\ell-1)}_j \oplus \eta_{\ell,i,j}) \;-\; \theta_{\ell,i}\Big),$ where $\Heav(z)=1$ if $z\ge 0$ and $\Heav(z)=0$ otherwise. The network output is $y^{(L)}$ (or a designated subset of its coordinates).

Generated from paper_jmlr.tex, lines 1335–1354.

2 Explain this

A literal-threshold network of depth $L$ : layer $0$ is the input; each unit in layer $\ell$ looks at the previous layer's outputs, possibly negates some of them, takes a weighted sum with grid weights, and outputs $1$ if the sum reaches its grid threshold. The output is the last layer (or some of its coordinates). Widths are polynomial in $n$ .

Example: with weights $1$ and threshold $1$ , a unit is an OR of its (possibly negated) inputs; with one negated input it is a NOT.

3 How this is formalised

AC0.Gate: coefficients $a_j$ , negation bits $\eta_j$ and threshold $b$ ; the gate fires iff $b\le\sum_j a_j[z_j\oplus\eta_j]$ .
AC0.Layer and AC0.evalNet: layers of gates reading the previous layer, applied in order.
AC0.NetValid: every gate valid for the grid bound $W$ .
AC0.gate_rat_iff: equivalence with the paper's rational Heaviside form.
FiniteNet.netFormula_spec: the explicit finite-input semantics (an $n$ -bit input, zero-extended) and its simulation by one formula per output.

Coverage record
Paper anchor	`def:NN-formal` (manuscript label)
Displayed as	Definition A.1
Claim	Literal-threshold network: layers of gates with grid weights, grid thresholds and negation bits
Coverage category	Checked definition or construction
Statement source	paper_jmlr.tex lines 1335–1354; SHA-256 of the normalised block source `8abbcb663c2c85e1…`
Lean declarations	`NimAudit.AC0.Gate` (Circuit, lines 326–331, file `af97cc0eec7d…`) `NimAudit.AC0.Layer` (Circuit, lines 743–744, file `af97cc0eec7d…`) `NimAudit.AC0.evalNet` (Circuit, lines 751–754, file `af97cc0eec7d…`) `NimAudit.AC0.NetValid` (Circuit, lines 765–766, file `af97cc0eec7d…`) `NimAudit.AC0.gate_rat_iff` (Circuit, lines 367–405, file `af97cc0eec7d…`) `NimAudit.FiniteNet.netFormula_spec` (FiniteNet, lines 42–64, file `1d45c4765000…`)
Prose-to-formal notes	Lean stores integer coefficients $a_j$ and threshold $b$ (weights $a_j/D$ , threshold $b/D$ ) and proves that the rational Heaviside form fires exactly when the integer form does.
Audited correspondence rows	`def:NN-formal`, `app:NN`
Explanations	`explain/def:NN-formal`, `formal/def:NN-formal`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

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.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.evalNet`

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

A network: layers applied in order.

Statement as elaborated and printed by Lean 4.26.0

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

Exact source text, lines 751–754

751/-- A network: layers applied in order. -/752def evalNet : List Layer → (Nat → Bool) → (Nat → Bool)753  | [], z => z754  | l :: ls, z => evalNet ls (evalLayer l z)

Project declarations in the statement: AC0.Layer

Project declarations used by the proof or definition body

AC0.Layer, AC0.evalLayer

def `AC0.NetValid`

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

All gates valid for W.

Statement as elaborated and printed by Lean 4.26.0

ℕ → List NimAudit.AC0.Layer → Prop

Exact source text, lines 765–766

765/-- All gates valid for W. -/766def NetValid (W : Nat) (ls : List Layer) : Prop := ∀ l ∈ ls, ∀ g ∈ l, Gate.Valid W g

Project declarations in the statement: AC0.Layer

Project declarations used by the proof or definition body

AC0.Gate, AC0.Gate.Valid, AC0.Layer

theorem `AC0.gate_rat_iff`

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

CLEARING DENOMINATORS: for D > 0 the rational gate fires iff the integer gate does.

Statement as elaborated and printed by Lean 4.26.0

∀ (g : NimAudit.AC0.Gate) {D : ℕ},
  0 < D → ∀ (z : ℕ → Bool), NimAudit.AC0.ratFires g D z ↔ g.eval z = true

Exact source text, lines 367–405

367/-- CLEARING DENOMINATORS: for D > 0 the rational gate fires iff the integer gate does. -/368theorem gate_rat_iff (g : Gate) {D : Nat} (hD : 0 < D) (z : Nat → Bool) :369    ratFires g D z ↔ g.eval z = true := by370  have hDr : (0 : Rat) < (D : Rat) := Rat.natCast_pos.mpr hD371  have hD' : (D : Rat) ≠ 0 := Rat.ne_of_gt hDr372  have e : rsum (List.range g.fanin)373      (fun j => ((g.coeff j : Nat) : Rat) / (D : Rat) * (if g.lit z j then 1 else 0)) =374      ((g.wsum z : Nat) : Rat) / (D : Rat) := by375    have e1 : rsum (List.range g.fanin)376        (fun j => ((g.coeff j : Nat) : Rat) / (D : Rat) * (if g.lit z j then 1 else 0)) =377        rsum (List.range g.fanin)378          (fun j => (1 / (D : Rat)) * (((g.coeff j * (if g.lit z j then 1 else 0) : Nat)) : Rat)) := by379      apply rsum_congr; intro j _380      by_cases hl : g.lit z j = true <;> simp [hl] <;> grind381    rw [e1, rsum_mul_left, rsum_natCast]382    unfold Gate.wsum Gate.psum383    grind384  unfold ratFires Gate.eval385  rw [e, decide_eq_true_iff]386  generalize g.wsum z = s387  generalize g.thr = b388  constructor389  · intro h390    have h' : ((b : Nat) : Rat) / (D : Rat) ≤ ((s : Nat) : Rat) / (D : Rat) := by grind391    have := Rat.mul_le_mul_of_nonneg_right h' (Rat.le_of_lt hDr)392    have e2 : ((b : Nat) : Rat) / (D : Rat) * (D : Rat) = b := by grind393    have e3 : ((s : Nat) : Rat) / (D : Rat) * (D : Rat) = s := by grind394    rw [e2, e3] at this395    exact Rat.natCast_le_natCast.mp this396  · intro h397    have h1 : ((b : Nat) : Rat) ≤ (s : Rat) := Rat.natCast_le_natCast.mpr h398    have hinv : (0 : Rat) ≤ 1 / (D : Rat) := by399      have := Rat.mul_le_mul_of_nonneg_right (Rat.le_of_lt hDr) (Rat.le_of_lt hDr)400      have h2 : (0 : Rat) < 1 / (D : Rat) := by401        have := (Rat.mul_pos_iff_of_pos_left hDr).mp (by grind : (0 : Rat) < (D : Rat) * (1 / (D : Rat)))402        exact this403      exact Rat.le_of_lt h2404    have := Rat.mul_le_mul_of_nonneg_right h1 hinv405    grind

Project declarations in the statement: AC0.Gate, AC0.Gate.eval, AC0.ratFires

Project declarations used by the proof or definition body

AC0.Gate, AC0.Gate.coeff, AC0.Gate.eval, AC0.Gate.fanin, AC0.Gate.lit, AC0.Gate.psum, AC0.Gate.thr, AC0.Gate.wsum, AC0.ratFires, AC0.rsum_natCast, Prob.rsum, Prob.rsum_congr, Prob.rsum_mul_left

theorem `FiniteNet.netFormula_spec`

Module FiniteNet (lean/phase4/FiniteNet.lean, lines 42–64) · file SHA-256 1d45c47650006bb7… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

FINITE-INPUT SIMULATION THEOREM (same formula for all four properties). For a valid network of L = ls.length layers with fan-ins and widths ≤ M and any input length n, output i is computed (on zero-extended n-bit inputs) by netFormula W n ls i, which has depth ≤ 3L, size ≤ 2 (2W+3)^L (M+1)^(WL) and reads only inputs < n.

Statement as elaborated and printed by Lean 4.26.0

∀ {W M : ℕ} (n : ℕ) (ls : List NimAudit.AC0.Layer),
  NimAudit.AC0.NetValid W ls →
    NimAudit.AC0.NetBounded M ls →
      ∀ (i : ℕ),
        (∀ (x : ℕ → Bool),
            NimAudit.AC0.Circ.eval x (NimAudit.FiniteNet.netFormula W n ls i) =
              NimAudit.AC0.evalNet ls (NimAudit.FiniteNet.pad n x) i) ∧
          (NimAudit.FiniteNet.netFormula W n ls i).depth ≤ 3 * ls.length ∧
            (NimAudit.FiniteNet.netFormula W n ls i).size ≤
                2 * ((2 * W + 3) ^ ls.length * (M + 1) ^ (W * ls.length)) ∧
              (NimAudit.FiniteNet.netFormula W n ls i).maxInput ≤ n

Exact source text, lines 42–64

42/-- FINITE-INPUT SIMULATION THEOREM (same formula for all four properties).43    For a valid network of L = ls.length layers with fan-ins and widths ≤ M and any44    input length n, output i is computed (on zero-extended n-bit inputs) by45    netFormula W n ls i, which has depth ≤ 3L, size ≤ 2 (2W+3)^L (M+1)^(WL) and reads46    only inputs < n. -/47theorem netFormula_spec {W M : Nat} (n : Nat) (ls : List Layer) (hv : NetValid W ls)48    (hb : NetBounded M ls) (i : Nat) :49    (∀ x : Nat → Bool, eval x (netFormula W n ls i) = evalNet ls (pad n x) i) ∧50    depth (netFormula W n ls i) ≤ 3 * ls.length ∧51    size (netFormula W n ls i) ≤ 2 * ((2 * W + 3) ^ ls.length * (M + 1) ^ (W * ls.length)) ∧52    maxInput (netFormula W n ls i) ≤ n := by53  have hsd := compileNet_sd (W := W) ls hb (clip n) 1 0 (clip_size n) (clip_depth n) i54  refine ⟨?_, ?_, ?_, compileNet_max ls (clip n) n (clip_max n) i⟩55  · intro x56    unfold netFormula57    rw [eval_compileNet ls hv]58    congr 159    funext j60    exact eval_clip x n j61  · have := hsd.2; unfold netFormula; omega62  · have h1 := sizeBound_closed W M ls.length63    have h2 := hsd.164    unfold netFormula; omega

Project declarations in the statement: AC0.Circ.depth, AC0.Circ.eval, AC0.Circ.maxInput, AC0.Circ.size, AC0.Layer, AC0.NetBounded, AC0.NetValid, AC0.evalNet, FiniteNet.netFormula, FiniteNet.pad

Project declarations used by the proof or definition body

AC0.Circ.depth, AC0.Circ.eval, AC0.Circ.maxInput, AC0.Circ.size, AC0.Layer, AC0.NetBounded, AC0.NetValid, AC0.compileNet, AC0.compileNet_max, AC0.compileNet_sd, AC0.evalNet, AC0.eval_compileNet, AC0.sizeBound, AC0.sizeBound_closed, FiniteNet.clip, FiniteNet.clip_depth, FiniteNet.clip_max, FiniteNet.clip_size, FiniteNet.eval_clip, FiniteNet.netFormula, FiniteNet.pad

Definitions these statements use

def `AC0.Gate.eval`

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

The gate fires iff b ≤ Σ_j a_j [z_j XOR eta_j].

Statement as elaborated and printed by Lean 4.26.0

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

Exact source text, lines 345–346

345/-- The gate fires iff b ≤ Σ_j a_j [z_j XOR eta_j]. -/346def eval (g : Gate) (z : Nat → Bool) : Bool := decide (g.thr ≤ g.wsum z)

Project declarations in the statement: AC0.Gate

Project declarations used by the proof or definition body

AC0.Gate, AC0.Gate.thr, AC0.Gate.wsum

def `AC0.ratFires`

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

Paper's form: weights a_j/D, threshold b/D, Heaviside(Σ w_j lit_j − θ).

Statement as elaborated and printed by Lean 4.26.0

NimAudit.AC0.Gate → ℕ → (ℕ → Bool) → Prop

Exact source text, lines 355–359

355/-- Paper's form: weights a_j/D, threshold b/D, Heaviside(Σ w_j lit_j − θ). -/356def ratFires (g : Gate) (D : Nat) (z : Nat → Bool) : Prop :=357  0 ≤ rsum (List.range g.fanin)358      (fun j => ((g.coeff j : Nat) : Rat) / (D : Rat) * (if g.lit z j then 1 else 0)) -359    ((g.thr : Nat) : Rat) / (D : Rat)

Project declarations in the statement: AC0.Gate

Project declarations used by the proof or definition body

AC0.Gate, AC0.Gate.coeff, AC0.Gate.fanin, AC0.Gate.lit, AC0.Gate.thr, Prob.rsum

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

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

def `AC0.Circ.maxInput`

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

One more than the largest input index used (0 if none).

Statement as elaborated and printed by Lean 4.26.0

NimAudit.AC0.Circ → ℕ

Exact source text, lines 68–74

68/-- One more than the largest input index used (0 if none). -/69def maxInput : Circ → Nat70  | input i => i + 171  | const _ => 072  | not c => maxInput c73  | and cs => listMax (cs.attach.map (fun ⟨c, _⟩ => maxInput c))74  | or cs => listMax (cs.attach.map (fun ⟨c, _⟩ => maxInput 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.listMax, AC0.Circ.not, AC0.Circ.or, AC0.Circ.rec, AC0.Circ.rec_1

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.NetBounded`

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

Fan-in and width bounded by M.

Statement as elaborated and printed by Lean 4.26.0

ℕ → List NimAudit.AC0.Layer → Prop

Exact source text, lines 768–769

768/-- Fan-in and width bounded by M. -/769def NetBounded (M : Nat) (ls : List Layer) : Prop := ∀ l ∈ ls, l.length ≤ M ∧ ∀ g ∈ l, g.fanin ≤ M

Project declarations in the statement: AC0.Layer

Project declarations used by the proof or definition body

AC0.Gate, AC0.Gate.fanin, AC0.Layer

def `FiniteNet.netFormula`

Module FiniteNet (lean/phase4/FiniteNet.lean, lines 31–32) · file SHA-256 1d45c47650006bb7…

THE compiled formula for output i of network ls on n inputs.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → List NimAudit.AC0.Layer → ℕ → NimAudit.AC0.Circ

Exact source text, lines 31–32

31/-- THE compiled formula for output i of network ls on n inputs. -/32def netFormula (W n : Nat) (ls : List Layer) (i : Nat) : Circ := compileNet W ls (clip n) i

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

Project declarations used by the proof or definition body

AC0.Layer, AC0.compileNet, FiniteNet.clip

def `FiniteNet.pad`

Module FiniteNet (lean/phase4/FiniteNet.lean, lines 25–26) · file SHA-256 1d45c47650006bb7…

Zero-extension of an n-bit assignment.

Statement as elaborated and printed by Lean 4.26.0

ℕ → (ℕ → Bool) → ℕ → Bool

Exact source text, lines 25–26

25/-- Zero-extension of an n-bit assignment. -/26def pad (n : Nat) (x : Nat → Bool) : Nat → Bool := fun j => if j < n then x j else false

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

Full modules

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

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

Definition A.1Literal-threshold network: layers of gates with grid weights, grid thresholds and negation bits

1 Paper text

2 Explain this

3 How this is formalised

4 Lean statement and source

Principal declarations

inductive AC0.Gate

def AC0.Layer

def AC0.evalNet

def AC0.NetValid

theorem AC0.gate_rat_iff

theorem FiniteNet.netFormula_spec

Definitions these statements use

def AC0.Gate.eval

def AC0.ratFires

def AC0.Circ.depth

def AC0.Circ.eval

def AC0.Circ.maxInput

def AC0.Circ.size

def AC0.NetBounded

def FiniteNet.netFormula

def FiniteNet.pad

Full modules

inductive `AC0.Gate`

def `AC0.Layer`

def `AC0.evalNet`

def `AC0.NetValid`

theorem `AC0.gate_rat_iff`

theorem `FiniteNet.netFormula_spec`

def `AC0.Gate.eval`

def `AC0.ratFires`

def `AC0.Circ.depth`

def `AC0.Circ.eval`

def `AC0.Circ.maxInput`

def `AC0.Circ.size`

def `AC0.NetBounded`

def `FiniteNet.netFormula`

def `FiniteNet.pad`