Section 2.1, “Why fixed-scale quantisation suggests an AC⁰ abstraction”Fixed scale gives a witness of at most W literals, hence a constant-width DNF for each unit

499/-- BOUNDED WITNESS LEMMA.  If the gate fires on z, there is a list T of at most500    b ≤ W distinct input positions, all with true literal and positive coefficient,501    whose coefficients sum to at least b; T is an initial segment of the active502    literals (T = active literals below a cut c'). -/503theorem bounded_witness (g : Gate) (z : Nat → Bool) (h : g.eval z = true) :504    ∃ c' ≤ g.fanin,505      (g.active z c').length ≤ g.thr ∧506      (∀ j ∈ g.active z c', g.lit z j = true ∧ 1 ≤ g.coeff j ∧ j < c') ∧507      g.thr ≤ nsum g.fanin (fun j => if j ∈ g.active z c' then g.coeff j else 0) := by508  unfold eval wsum at h509  have h' : g.thr ≤ g.psum z g.fanin := of_decide_eq_true h510  obtain ⟨c', hc', h1, h2⟩ := exists_cut g z g.fanin h'511  refine ⟨c', hc', ?_, ?_, ?_⟩512  · -- length bound513    cases c' with514    | zero => simp [active]515    | succ c =>516      have hlt := h2 c (by omega)517      have hlen := active_length_le g z c518      have hstep : (g.active z (c + 1)).length ≤ (g.active z c).length + 1 := by519        unfold active520        rw [List.range_succ, List.filter_append, List.length_append]521        have : (List.filter (fun j => g.lit z j && decide (1 ≤ g.coeff j)) [c]).length ≤ 1 := by522          simp only [List.filter_cons, List.filter_nil]; split <;> simp523        omega524      omega525  · intro j hj526    unfold active at hj527    simp only [List.mem_filter, List.mem_range, Bool.and_eq_true, decide_eq_true_eq] at hj528    exact ⟨hj.2.1, hj.2.2, hj.1⟩529  · have e : nsum g.fanin (fun j => if j ∈ g.active z c' then g.coeff j else 0) =530        nsum g.fanin (fun j => if j < c' then g.coeff j * (if g.lit z j then 1 else 0) else 0) := by531      apply nsum_congr532      intro j _533      unfold active534      simp only [List.mem_filter, List.mem_range, Bool.and_eq_true, decide_eq_true_eq]535      by_cases hjc : j < c' <;> by_cases hl : g.lit z j = true <;>536        by_cases ha : 1 ≤ g.coeff j <;> simp [hjc, hl, ha] <;> omega537    rw [e, nsum_cut _ hc']538    exact h1

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⟩