Lemma B.1One fixed-scale threshold gate is a depth-2 DNF of size O(m^W)

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⟩

211/-- Lemma lem:unit-ac0 in the paper's convention: one fixed-scale gate is a DEPTH-2 DNF212    when negations on inputs are not counted (our NOT-counting depth bound was 3). -/213theorem dnf_aoDepth (W : Nat) (g : Gate) : aoDepth (dnf W g) ≤ 2 := by214  unfold dnf215  rw [aoDepth_or]216  have : listMax ((((boards (g.fanin + 1) W).filter (fun t => decide (g.thr ≤ selSum g t))).map (termC g)).map aoDepth) ≤ 1 := by217    apply listMax_le; intro a ha218    obtain ⟨c, hc, rfl⟩ := List.mem_map.mp ha219    obtain ⟨t, _, rfl⟩ := List.mem_map.mp hc220    unfold termC; rw [aoDepth_and]221    have : listMax ((t.filterMap (fun j => if j < g.fanin then some (litC g j) else none)).map aoDepth) ≤ 0 := by222      apply listMax_le; intro b hb223      obtain ⟨c', hc', rfl⟩ := List.mem_map.mp hb224      obtain ⟨j, _, hj⟩ := List.mem_filterMap.mp hc'225      split at hj226      · cases hj; unfold litC; split <;> simp [aoDepth]227      · cases hj228    omega229  omega