Remark B.2Negated inputs replace z_j by ¬z_j in each conjunction; the lemma still applies

Checked theorem Lean checks a formal statement corresponding to this claim.

1 Paper text

Remark B.2 (Negations) If some inputs are negated before weighting, i.e. $(z_j\oplus \eta_j)$ , this simply replaces $z_j$ by either $z_j$ or $\neg z_j$ in each conjunction term. Since $\AC^0$ allows NOT gates, Lemma B.1 still applies.

Generated from paper_jmlr.tex, lines 1440–1443.

2 Explain this

If some inputs are negated before weighting, each term of the DNF simply uses $\neg z_j$ instead of $z_j$ for those inputs. AC⁰ has NOT gates, so the lemma still applies.

3 How this is formalised

Negation flags are part of the Lean gate model from the start, so AC0.gate_ac0 and the DNF correctness theorem AC0.eval_dnf already cover negated inputs.

Coverage record
Paper anchor	`x-remark-negations` (website anchor; the manuscript has no label here)
Displayed as	Remark B.2
Claim	Negated inputs replace z_j by ¬z_j in each conjunction; the lemma still applies
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 1440–1443; SHA-256 of the normalised block source `26b89f049e457335…`
Lean declarations	`NimAudit.AC0.gate_ac0` (Circuit, lines 735–739, file `af97cc0eec7d…`) `NimAudit.AC0.eval_dnf` (Circuit, lines 600–650, file `af97cc0eec7d…`)
Depends on	Lemma B.1
Explanations	`explain/x-remark-negations`, `formal/x-remark-negations`
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 `AC0.eval_dnf`

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

DNF CORRECTNESS: for b ≤ W, the DNF computes the gate exactly (any fan-in, including 0; b = 0 gives the constant-true DNF).

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

Exact source text, lines 600–650

600/-- DNF CORRECTNESS: for b ≤ W, the DNF computes the gate exactly (any fan-in,601    including 0; b = 0 gives the constant-true DNF). -/602theorem eval_dnf {W : Nat} (g : Gate) (hW : g.thr ≤ W) (z : Nat → Bool) :603    eval z (dnf W g) = g.eval z := by604  apply Bool.eq_iff_iff.mpr605  unfold dnf606  simp only [eval_or, List.any_map, List.any_eq_true, List.mem_filter, decide_eq_true_eq,607    Function.comp]608  constructor609  · rintro ⟨t, ⟨_, hsel⟩, ht⟩610    have hlit := (eval_termC g z t).1 ht611    unfold Gate.eval Gate.wsum Gate.psum612    apply decide_eq_true613    apply Nat.le_trans hsel614    unfold selSum615    apply nsum_le616    intro j hj617    by_cases hjt : j ∈ t618    · simp [hjt, hlit j hjt hj]619    · simp [hjt]620  · intro h621    obtain ⟨c', hc', hlen, hact, hsum⟩ := g.bounded_witness z h622    generalize g.active z c' = L at hlen hact hsum623    let t := L ++ List.replicate (W - L.length) g.fanin624    have hmemt : ∀ j, j < g.fanin → (j ∈ t ↔ j ∈ L) := by625      intro j hj626      simp only [t, List.mem_append, List.mem_replicate]627      constructor628      · rintro (h | ⟨_, h⟩)629        · exact h630        · omega631      · exact Or.inl632    refine ⟨t, ⟨?_, ?_⟩, ?_⟩633    · apply mem_boards_of634      · simp only [t, List.length_append, List.length_replicate]; omega635      · intro x hx636        simp only [t, List.mem_append, List.mem_replicate] at hx637        rcases hx with hx | ⟨_, rfl⟩638        · have := (hact x hx).2.2; omega639        · omega640    · unfold selSum641      rw [nsum_congr (g := fun j => if j ∈ L then g.coeff j else 0)]642      · exact hsum643      · intro j hj644        by_cases hjL : j ∈ L645        · simp [hjL, (hmemt j hj).2 hjL]646        · have : j ∉ t := fun h' => hjL ((hmemt j hj).1 h')647          simp [hjL, this]648    · rw [eval_termC]649      intro j hjt hjm650      exact (hact j ((hmemt j hjm).1 hjt)).1

Project declarations in the statement: AC0.Circ.eval, AC0.Gate, AC0.Gate.eval, AC0.Gate.thr, AC0.dnf

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.eval, AC0.Circ.eval_or, AC0.Circ.or, AC0.Gate, AC0.Gate.active, AC0.Gate.bounded_witness, AC0.Gate.coeff, AC0.Gate.eval, AC0.Gate.fanin, AC0.Gate.lit, AC0.Gate.psum, AC0.Gate.thr, AC0.Gate.wsum, AC0.dnf, AC0.eval_termC, AC0.mem_boards_of, AC0.nsum, AC0.nsum_congr, AC0.nsum_le, AC0.selSum, AC0.termC, Prob.boards

Definitions these statements use

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

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

Full modules

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

Remark B.2Negated inputs replace z_j by ¬z_j in each conjunction; the lemma still applies

1 Paper text

2 Explain this

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem AC0.gate_ac0

theorem AC0.eval_dnf

Definitions these statements use

def AC0.Circ.depth

def AC0.Circ.eval

def AC0.Circ.maxInput

def AC0.Circ.size

inductive AC0.Gate

def AC0.Gate.eval

def AC0.Gate.fanin

def AC0.Gate.thr

def AC0.dnf

Full modules

theorem `AC0.gate_ac0`

theorem `AC0.eval_dnf`

def `AC0.Circ.depth`

def `AC0.Circ.eval`

def `AC0.Circ.maxInput`

def `AC0.Circ.size`

inductive `AC0.Gate`

def `AC0.Gate.eval`

def `AC0.Gate.fanin`

def `AC0.Gate.thr`

def `AC0.dnf`