Checked definition or construction Lean contains the definition or construction, with checked properties.
Generated from paper_jmlr.tex, lines 1317–1317.
The representable parameters are the fixed grid : step , values up to , and the same set for every input length. The appendix stresses that this is a Boolean gate abstraction: neither floating-point nor general signed fixed-point networks satisfy it automatically, and what drives the AC0 containment is that thresholds do not grow with fan-in, not that a number format is finite. Negations on wires are allowed, as in AC0.
AC0.Gate stores integer coefficients, negation flags and an integer threshold;
AC0.Gate.Valid bounds them by ; AC0.gate_rat_iff proves that with denominator
the rational form (weights , threshold , Heaviside) fires exactly when the integer form does.
| Paper anchor | app:precision (manuscript label) |
|---|---|
| Displayed as | Section A.1 |
| Claim | Representable parameters: a fixed finite grid independent of n; negations allowed on wires |
| Coverage category | Checked definition or construction |
| Statement source | paper_jmlr.tex lines 1317–1317; SHA-256 of the normalised block source c9e050abbdbc68da… |
| Lean declarations |
|
| Audited correspondence rows | app:defs, app:precision |
| Explanations | explain/app:precision, formal/app:precision |
| Build evidence | fresh isolated rebuild, audit report |
AC0.Gate.ValidFixed-scale validity: threshold and coefficients in 0..W.
Statement as elaborated and printed by Lean 4.26.0
ℕ → NimAudit.AC0.Gate → Prop348/-- Fixed-scale validity: threshold and coefficients in 0..W. -/349def Valid (W : Nat) (g : Gate) : Prop := g.thr ≤ W ∧ ∀ a ∈ g.coeffs, a ≤ WProject declarations in the statement: AC0.Gate
AC0.gate_rat_iffCLEARING 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 = true367/-- 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 grindProject declarations in the statement: AC0.Gate, AC0.Gate.eval, AC0.ratFires
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
AC0.GateA 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
Type326/-- 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 : NatProject declarations in the statement: none
none
AC0.Gate.evalThe 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) → Bool345/-- 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
AC0.ratFiresPaper'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) → Prop355/-- 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
AC0.Gate, AC0.Gate.coeff, AC0.Gate.fanin, AC0.Gate.lit, AC0.Gate.thr, Prob.rsum
| 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).