Checked definition or construction Lean contains the definition or construction, with checked properties.
We define a finite set independent of input length. The threshold bound applies after choosing the literal representation. Replacing a signed term by raises the threshold by . With many such terms, the adjusted threshold may grow with the input length. What matters is the amount of evidence needed to activate a gate: our model bounds the number of satisfied input literals that suffice, whereas an unrestricted majority gate needs a number that grows with its inputs. Negative coefficients themselves are not the obstruction; the bound on the adjusted threshold is essential to the simulation.
Generated from paper_jmlr.tex, lines 294–300.
Inhibitory effects are allowed. Negating an input makes a positive literal weight act negatively on the original input. The restriction is the fixed bound on the threshold after this rewriting. A firing gate then has a bounded-size witness of satisfied literals; a general majority gate does not. This is why the threshold bound matters computationally.
The grid. Every weight and threshold is a multiple of between and : for example, with and the allowed values are . The point is that this set is fixed: it does not grow when the input gets longer.
Why negative terms matter. The model only has nonnegative weights on literals (an input or its negation ). A signed term can be rewritten as , so it becomes a nonnegative weight on the negated literal, but the threshold rises by . With many negative terms the threshold can grow with the input length and leave the grid. So "signed weights" are not automatically inside the model.
A gate in Lean (AC0.Gate) stores integer coefficients , negation flags and an integer
threshold ; with denominator the paper's weights are and the threshold is .
AC0.gate_rat_iff proves that the paper's rational Heaviside form fires exactly when the integer
form does (for ). Fixed-scale validity,
AC0.Gate.Valid, bounds the threshold and coefficients by .
The remark about signed terms is the identity Windows.literal_shift: over the integers,
.
| Paper anchor | c-qset (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 2.1, paragraph 4 |
| Claim | The fixed grid Q_{W,D}; rewriting a negative term as a literal raises the threshold |
| Coverage category | Checked definition or construction |
| Statement source | paper_jmlr.tex lines 294–300; SHA-256 of the normalised block source 8a3e62d1a6032e96… |
| Lean declarations |
|
| Assumptions and domain | Constants with ; weights with . |
| Explanations | explain/c-qset, formal/c-qset |
| 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
Windows.literal_shiftThe literal-representation remark: replacing −a·x by a·(1 − x) adds a to the threshold.
Statement as elaborated and printed by Lean 4.26.0
∀ (s a x θ : ℤ), θ ≤ s - a * x ↔ θ + a ≤ s + a * (1 - x)238/-- The literal-representation remark: replacing −a·x by a·(1 − x) adds a to the threshold. -/239theorem literal_shift (s a x θ : Int) : (θ ≤ s - a * x) ↔ (θ + a ≤ s + a * (1 - x)) := by240 rw [Int.mul_sub, Int.mul_one]; omegaProject declarations in the statement: none
none
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.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
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
| Module | File | Lines | Imports |
|---|---|---|---|
| Circuit | lean/phase3/Circuit.lean | 1151 | NimProbability |
| 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).