Definition A.3Gate-realised attention-style model: every operation implemented in the permitted gates

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

1 Paper text

Definition A.3 (Gate-realised attention-style model) Fix a time window $T\in\N$ . A fixed-scale quantised $\LTST$ model processes a sequence $(x_{t-T+1},\dots,x_t)$ by:

computing short-term and long-term attention scores using fixed-scale quantised parameters in $\Qset_{W,D}$ ,
combining attended summaries through a constant number of layers of fixed-scale quantised threshold computations,
producing outputs $o_t\in\bits^k$ .

Every score computation, input-dependent coefficient selection, encoding and value aggregation is required to have a polynomial-size, constant-depth implementation in the Boolean literal-threshold gates of Definition A.1. Intermediate state is Boolean, and total unrolling is bounded as in Definition A.2. Under these explicit implementation assumptions, the simulation theorem applies by composition. Merely requiring parameters or coefficients to lie in a finite set is insufficient. This extension makes no claim about standard softmax attention without such a reduction.

Generated from paper_jmlr.tex, lines 1378–1388.

2 Explain this

An "attention-style" model is admitted only in a gate-realised form: every score computation, input-dependent coefficient selection, encoding and aggregation must itself be a polynomial-size, constant-depth network of the permitted literal-threshold gates, with Boolean intermediate states and bounded total unrolling. Then the simulation theorem applies by composition.

Caveat: merely restricting parameters or coefficients to a finite set is not enough, and nothing is claimed about standard softmax attention.

3 How this is formalised

Windows.staged_ac0: a model given as a list of $K$ stages (Windows.runStages), each a valid network of at most $L$ layers with bounded widths, is computed by formulas of depth at most $3KL$ and explicit size, reading only the inputs. Why a finite coefficient set alone is insufficient: Remark 2.2 (model scope).

Coverage record
Paper anchor	`def:LTST-formal` (manuscript label)
Displayed as	Definition A.3
Claim	Gate-realised attention-style model: every operation implemented in the permitted gates
Coverage category	Checked definition or construction
Statement source	paper_jmlr.tex lines 1378–1388; SHA-256 of the normalised block source `98c0d52ef1343872…`
Lean declarations	`NimAudit.Windows.staged_ac0` (Windows, lines 165–188, file `ff59ec8bf0a0…`)
Prose-to-formal notes	No claim is made about standard softmax attention; Lean covers a model given as a constant number of stages, each a valid gate network.
Audited correspondence rows	`def:LTST-formal`, `app:LTST`
Explanations	`explain/def:LTST-formal`, `formal/def:LTST-formal`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `Windows.staged_ac0`

Module Windows (lean/phase6/Windows.lean, lines 165–188) · file SHA-256 ff59ec8bf0a0de70… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

GATE-REALISED COMPOSITION THEOREM. If every stage is a W-valid network with at most L layers and widths/fan-ins ≤ M, the K-stage model is computed (on zero-extended n-bit inputs) by formulas of depth ≤ 3·K·L, size ≤ 2 (2W+3)^{KL} (M+1)^{W·KL}, reading only the n inputs; the formulas compute the staged evaluation.

Statement as elaborated and printed by Lean 4.26.0

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

Exact source text, lines 165–188

165/-- GATE-REALISED COMPOSITION THEOREM.  If every stage is a W-valid network with at most L166    layers and widths/fan-ins ≤ M, the K-stage model is computed (on zero-extended n-bit167    inputs) by formulas of depth ≤ 3·K·L, size ≤ 2 (2W+3)^{KL} (M+1)^{W·KL}, reading only168    the n inputs; the formulas compute the staged evaluation. -/169theorem staged_ac0 {W M L : Nat} (sts : List (List Layer)) (hv : ∀ st ∈ sts, NetValid W st)170    (hb : ∀ st ∈ sts, NetBounded M st) (hl : ∀ st ∈ sts, st.length ≤ L) (n i : Nat) :171    (∀ x : Nat → Bool, eval x (netFormula W n sts.flatten i) = runStages sts (pad n x) i) ∧172    depth (netFormula W n sts.flatten i) ≤ 3 * (sts.length * L) ∧173    size (netFormula W n sts.flatten i) ≤ 2 * ((2 * W + 3) ^ (sts.length * L) * (M + 1) ^ (W * (sts.length * L))) ∧174    maxInput (netFormula W n sts.flatten i) ≤ n := by175  have hv' : NetValid W sts.flatten := by176    intro l hl' g hg177    obtain ⟨st, hst, hlst⟩ := List.mem_flatten.mp hl'178    exact hv st hst l hlst g hg179  have hb' : NetBounded M sts.flatten := by180    intro l hl'181    obtain ⟨st, hst, hlst⟩ := List.mem_flatten.mp hl'182    exact hb st hst l hlst183  obtain ⟨h1, h2, h3, h4⟩ := netFormula_spec n sts.flatten hv' hb' i184  have hlen := flatten_length_le hl185  refine ⟨fun x => by rw [h1, evalNet_flatten], Nat.le_trans h2 (Nat.mul_le_mul_left 3 hlen), Nat.le_trans h3 ?_, h4⟩186  apply Nat.mul_le_mul_left187  exact Nat.mul_le_mul (Nat.pow_le_pow_right (by omega) hlen)188    (Nat.pow_le_pow_right (by omega) (Nat.mul_le_mul_left W hlen))

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

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.Valid, AC0.Gate.fanin, AC0.Layer, AC0.NetBounded, AC0.NetValid, AC0.evalNet, FiniteNet.netFormula, FiniteNet.netFormula_spec, FiniteNet.pad, Windows.evalNet_flatten, Windows.flatten_length_le, Windows.runStages

Definitions these statements use

def `Windows.runStages`

Module Windows (lean/phase6/Windows.lean, lines 147–150) · file SHA-256 ff59ec8bf0a0de70…

Staged evaluation: stages applied in order.

Statement as elaborated and printed by Lean 4.26.0

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

Exact source text, lines 147–150

147/-- Staged evaluation: stages applied in order. -/148def runStages : List (List Layer) → (Nat → Bool) → (Nat → Bool)149  | [], x => x150  | st :: sts, x => runStages sts (evalNet st x)

Project declarations in the statement: AC0.Layer

Project declarations used by the proof or definition body

AC0.Layer, AC0.evalNet

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

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
Windows	`lean/phase6/Windows.lean`	261	Bypass

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.3Gate-realised attention-style model: every operation implemented in the permitted gates

1 Paper text

2 Explain this

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem Windows.staged_ac0

Definitions these statements use

def Windows.runStages

def AC0.Circ.depth

def AC0.Circ.eval

def AC0.Circ.maxInput

def AC0.Circ.size

def AC0.Layer

def AC0.NetBounded

def AC0.NetValid

def FiniteNet.netFormula

def FiniteNet.pad

Full modules

theorem `Windows.staged_ac0`

def `Windows.runStages`

def `AC0.Circ.depth`

def `AC0.Circ.eval`

def `AC0.Circ.maxInput`

def `AC0.Circ.size`

def `AC0.Layer`

def `AC0.NetBounded`

def `AC0.NetValid`

def `FiniteNet.netFormula`

def `FiniteNet.pad`