Definition 2.1Fixed-scale quantised NN, RNN and LTST models: constant depth, polynomial size, fixed grid, bounded unrolling

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

1 Paper text

Definition 2.1 (Quantised inference) A network $\NN$ in this class has constant depth and polynomially many threshold neurons, with weights and thresholds in $\Qset_{W,D}$ . Analogously, fixed-scale quantised $\RNN$ and $\LTST$ models have constant depth and polynomial size per time step and operate within a fixed time window $T$ . For the simulation theorem, $T$ bounds the entire unrolled computation from an input-independent initial state, including any computation used to form a retained state.

Generated from paper_jmlr.tex, lines 304–309.

2 Explain this

Effective precision. The motivation is the scale of distinctions a computation can use reliably, potentially limited by noise and much coarser than float32 rounding. Ordinary finite-precision storage alone does not establish the model's hypotheses. Noise does not automatically imply a Boolean literal-threshold implementation either.

This definition fixes the class of networks the lower bound is about:

constant depth (a fixed number of layers, independent of the input length);
polynomially many threshold neurons;
weights and thresholds on the fixed grid $\mathcal Q_{W,D}$ ;
for recurrent and attention-style models, a fixed time window $T$ that bounds the entire unrolled computation, including anything used to form a retained state.

Example: a 3-layer network on $n$ inputs with $n^2$ neurons, all weights in $\{0,1/2,1\}$ and thresholds at most $2$ , is in the class for every $n$ .

Caveat: this is a restricted logical model inspired by bounded numerical resources. It is not equivalent to arbitrary INT8 or fixed-point inference, and ordinary floating-point layers with signed weights are not automatically covered.

3 How this is formalised

The formal model is the literal-threshold gate network of Appendix A (Definition A.1): gates (AC0.Gate) arranged in layers (AC0.Layer), evaluated by AC0.evalNet, with every gate valid for the grid bound $W$ (AC0.NetValid). Two checked facts support the definition's use:

AC0.gate_ac0: one valid gate is computed exactly by a formula of depth at most 3 (counting NOT) and size at most $1+(m+1)^W(2W+1)$ for fan-in $m$ ;
FiniteNet.netFormula_spec: a network of $L$ layers on an $n$ -bit input is computed output by output by one formula of depth at most $3L$ and size at most $2(2W+3)^L(M+1)^{WL}$ , reading only the $n$ inputs.

The recurrent and attention-style parts of the definition are covered by Definition A.2 and Definition A.3.

Coverage record
Paper anchor	`def:quantised-inference` (manuscript label)
Displayed as	Definition 2.1
Claim	Fixed-scale quantised NN, RNN and LTST models: constant depth, polynomial size, fixed grid, bounded unrolling
Coverage category	Checked definition or construction
Statement source	paper_jmlr.tex lines 304–309; SHA-256 of the normalised block source `2f122daa6a7ac5c1…`
Lean declarations	`NimAudit.AC0.gate_ac0` (Circuit, lines 735–739, file `af97cc0eec7d…`) `NimAudit.FiniteNet.netFormula_spec` (FiniteNet, lines 42–64, file `1d45c4765000…`) `NimAudit.AC0.NetValid` (Circuit, lines 765–766, file `af97cc0eec7d…`)
Assumptions and domain	Nonnegative literal weights; threshold at most $W$ in units of $1/D$ ; Boolean intermediate states; for recurrent and attention-style models, at most $T$ updates in total from an input-independent initial state.
Prose-to-formal notes	The Lean gate model is the literal-threshold gate of Definition A.1 after clearing denominators. It is not a model of arbitrary INT8 or floating-point inference.
Depends on	Definition A.1, Definition A.2, Definition A.3
Audited correspondence rows	`def:quantised-inference`
Explanations	`explain/def:quantised-inference`, `formal/def:quantised-inference`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `AC0.gate_ac0`

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

ONE-GATE LEMMA (paper Lemma unit-ac0): exact, depth ≤ 3, size ≤ 1 + (m+1)^W (2W+1).

Statement as elaborated and printed by Lean 4.26.0

∀ {W : ℕ} (g : NimAudit.AC0.Gate),
  g.thr ≤ W →
    (∀ (z : ℕ → Bool), NimAudit.AC0.Circ.eval z (NimAudit.AC0.dnf W g) = g.eval z) ∧
      (NimAudit.AC0.dnf W g).depth ≤ 3 ∧
        (NimAudit.AC0.dnf W g).size ≤ 1 + (g.fanin + 1) ^ W * (2 * W + 1) ∧
          (NimAudit.AC0.dnf W g).maxInput ≤ g.fanin

Exact source text, lines 735–739

735/-- ONE-GATE LEMMA (paper Lemma unit-ac0): exact, depth ≤ 3, size ≤ 1 + (m+1)^W (2W+1). -/736theorem gate_ac0 {W : Nat} (g : Gate) (hW : g.thr ≤ W) :737    (∀ z, eval z (dnf W g) = g.eval z) ∧ depth (dnf W g) ≤ 3 ∧738      size (dnf W g) ≤ 1 + (g.fanin + 1) ^ W * (2 * W + 1) ∧ maxInput (dnf W g) ≤ g.fanin :=739  ⟨eval_dnf g hW, depth_dnf W g, size_dnf W g, maxInput_dnf W g⟩

Project declarations in the statement: AC0.Circ.depth, AC0.Circ.eval, AC0.Circ.maxInput, AC0.Circ.size, AC0.Gate, AC0.Gate.eval, AC0.Gate.fanin, AC0.Gate.thr, AC0.dnf

Project declarations used by the proof or definition body

AC0.Circ.depth, AC0.Circ.eval, AC0.Circ.maxInput, AC0.Circ.size, AC0.Gate, AC0.Gate.eval, AC0.Gate.fanin, AC0.Gate.thr, AC0.depth_dnf, AC0.dnf, AC0.eval_dnf, AC0.maxInput_dnf, AC0.size_dnf

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

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

Definitions these statements use

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.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.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.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.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.Gate.thr`

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

Statement as elaborated and printed by Lean 4.26.0

NimAudit.AC0.Gate → ℕ

Exact source text, lines 331–331

331  thr : Nat

Project declarations in the statement: AC0.Gate

Project declarations used by the proof or definition body

AC0.Gate

def `AC0.dnf`

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

DNF: OR over padded tuples t ∈ {0..m}^W with selSum ≥ b of termC t.

Statement as elaborated and printed by Lean 4.26.0

ℕ → NimAudit.AC0.Gate → NimAudit.AC0.Circ

Exact source text, lines 560–562

560/-- DNF: OR over padded tuples t ∈ {0..m}^W with selSum ≥ b of termC t. -/561def dnf (W : Nat) (g : Gate) : Circ :=562  or (((boards (g.fanin + 1) W).filter (fun t => decide (g.thr ≤ selSum g t))).map (termC g))

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

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.or, AC0.Gate, AC0.Gate.fanin, AC0.Gate.thr, AC0.selSum, AC0.termC, Prob.boards

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 2.1Fixed-scale quantised NN, RNN and LTST models: constant depth, polynomial size, fixed grid, bounded unrolling

1 Paper text

2 Explain this

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem AC0.gate_ac0

theorem FiniteNet.netFormula_spec

def AC0.NetValid

Definitions these statements use

inductive AC0.Gate

def AC0.Gate.Valid

def AC0.Layer

def AC0.evalNet

def AC0.Circ.depth

def AC0.Circ.eval

def AC0.Circ.maxInput

def AC0.Circ.size

def AC0.Gate.eval

def AC0.Gate.fanin

def AC0.Gate.thr

def AC0.dnf

def AC0.NetBounded

def FiniteNet.netFormula

def FiniteNet.pad

Full modules

theorem `AC0.gate_ac0`

theorem `FiniteNet.netFormula_spec`

def `AC0.NetValid`

inductive `AC0.Gate`

def `AC0.Gate.Valid`

def `AC0.Layer`

def `AC0.evalNet`

def `AC0.Circ.depth`

def `AC0.Circ.eval`

def `AC0.Circ.maxInput`

def `AC0.Circ.size`

def `AC0.Gate.eval`

def `AC0.Gate.fanin`

def `AC0.Gate.thr`

def `AC0.dnf`

def `AC0.NetBounded`

def `FiniteNet.netFormula`

def `FiniteNet.pad`