Theorem 2.4Fixed-depth, fixed-grid literal-threshold networks (and bounded-unrolling extensions) are simulated by AC⁰ circuit families

921/-- FEEDFORWARD SIMULATION THEOREM (one network).  A valid network of L layers with922    all fan-ins and widths ≤ M, on inputs x_0..x_{n-1} (n ≤ M), is computed output by923    output by formulas of depth ≤ 3L and size ≤ 2 (2W+3)^L (M+1)^(W L), reading only924    inputs < n. -/925theorem network_ac0 {W M n : Nat} (ls : List Layer) (hv : NetValid W ls) (hb : NetBounded M ls)926    (i : Nat) :927    (∀ x : Nat → Bool, eval x (compileNet W ls input i) = evalNet ls x i) ∧928    depth (compileNet W ls input i) ≤ 3 * ls.length ∧929    size (compileNet W ls input i) ≤ 2 * ((2 * W + 3) ^ ls.length * (M + 1) ^ (W * ls.length)) ∧930    maxInput (compileNet W ls (fun j => if j < n then input j else const false) i) ≤ n := by931  have hb' := compileNet_sd (W := W) ls hb input 1 0 (fun _ => by simp) (fun _ => by simp) i932  refine ⟨fun x => by rw [eval_compileNet ls hv]; simp, by have := hb'.2; omega, ?_, ?_⟩933  · have := sizeBound_closed W M ls.length; have := hb'.1; omega934  · exact compileNet_max (W := W) ls (fun j => if j < n then input j else const false) n935      (fun j => by936        show maxInput (if j < n then input j else const false) ≤ n937        split <;> simp <;> omega) i

164/-- FINITE-INPUT FAMILY THEOREM.  Fix W, L, c, k, c', k'.  For each input length n let165    net n be a valid network with exactly L layers whose fan-ins and widths are166    ≤ c (n+1)^k, with K n ≤ c' (n+1)^k' designated output bits.  Then each output i167    is computed (zero-extended n-bit semantics) by one formula that reads only168    inputs < n, has depth ≤ 3L and size ≤ 2 (2W+3)^L (c+1)^(WL) (n+1)^(kWL); the169    total size of the K n output formulas is ≤ c'(n+1)^k' times that bound. -/170theorem family_finite {W L c k c' k' : Nat} (net : Nat → List Layer) (K : Nat → Nat)171    (hlen : ∀ n, (net n).length = L) (hv : ∀ n, NetValid W (net n))172    (hb : ∀ n, NetBounded (c * (n + 1) ^ k) (net n)) (hK : ∀ n, K n ≤ c' * (n + 1) ^ k')173    (n : Nat) :174    (∀ i, (∀ x : Nat → Bool, eval x (netFormula W n (net n) i) = evalNet (net n) (pad n x) i) ∧175      depth (netFormula W n (net n) i) ≤ 3 * L ∧176      size (netFormula W n (net n) i) ≤177        2 * ((2 * W + 3) ^ L * ((c + 1) ^ (W * L) * (n + 1) ^ (k * (W * L)))) ∧178      maxInput (netFormula W n (net n) i) ≤ n) ∧179    totalSize W n (net n) (K n) ≤180      c' * (n + 1) ^ k' * (2 * ((2 * W + 3) ^ L * ((c + 1) ^ (W * L) * (n + 1) ^ (k * (W * L))))) := by181  have hM : (c * (n + 1) ^ k + 1) ^ (W * L) ≤ (c + 1) ^ (W * L) * (n + 1) ^ (k * (W * L)) := by182    have hp : c * (n + 1) ^ k + 1 ≤ (c + 1) * (n + 1) ^ k := by183      have : 1 ≤ (n + 1) ^ k := Nat.pow_pos (by omega)184      generalize (n + 1) ^ k = p at *185      have e : (c + 1) * p = c * p + p := by rw [Nat.add_mul, Nat.one_mul]186      rw [e]; omega187    calc (c * (n + 1) ^ k + 1) ^ (W * L) ≤ ((c + 1) * (n + 1) ^ k) ^ (W * L) :=188          Nat.pow_le_pow_left hp _189      _ = (c + 1) ^ (W * L) * (n + 1) ^ (k * (W * L)) := by190          rw [Nat.mul_pow, ← Nat.pow_mul, Nat.mul_comm k]191  have hbound : 2 * ((2 * W + 3) ^ (net n).length * (c * (n + 1) ^ k + 1) ^ (W * (net n).length)) ≤192      2 * ((2 * W + 3) ^ L * ((c + 1) ^ (W * L) * (n + 1) ^ (k * (W * L)))) := by193    rw [hlen]194    exact Nat.mul_le_mul_left _ (Nat.mul_le_mul_left _ hM)195  refine ⟨fun i => ?_, ?_⟩196  · obtain ⟨h1, h2, h3, h4⟩ := netFormula_spec n (net n) (hv n) (hb n) i197    rw [hlen] at h2198    exact ⟨h1, h2, Nat.le_trans h3 hbound, h4⟩199  · have := totalSize_le n (net n) (hv n) (hb n) (K n)200    exact Nat.le_trans this (Nat.mul_le_mul (hK n) hbound)

156/-- NETWORK-TO-AC0 AT FAMILY LEVEL.  If a network family satisfies NetFam with fixed W and157    L, then its first K i outputs (K polynomial) are computed by the compiled formulas158    netFormula W (len i) (net i), which form an AC0 family of depth ≤ 3L reading only the159    len inputs; on unpadded inputs the formulas equal the networks (Wired, nonempty). -/160theorem netFam_ac0 {ι : Type} {adm : ι → Prop} {len : ι → Nat} {net : ι → List Layer} {W L : Nat}161    (h : NetFam adm len net W L) (K : ι → Nat) (hK : PolyIn adm len K) :162    AC0Fam adm len (fun i => (List.range (K i)).map (netFormula W (len i) (net i))) (3 * L) ∧163    (∀ i, adm i → net i ≠ [] → ∀ o (x : Nat → Bool), eval x (netFormula W (len i) (net i) o) = evalNet (net i) x o) := by164  obtain ⟨c, k, hb⟩ := h.bounded165  have spec := fun i (hi : adm i) o => netFormula_spec (len i) (net i) (h.valid i hi) (hb i hi) o166  refine ⟨⟨h.pos, ?_, ?_, ?_⟩, ?_⟩167  · intro i hi c' hc168    obtain ⟨o, _, rfl⟩ := List.mem_map.mp hc169    have := (spec i hi o).2.1; have := h.layers i hi; omega170  · intro i hi c' hc171    obtain ⟨o, _, rfl⟩ := List.mem_map.mp hc172    exact (spec i hi o).2.2.2173  · -- each formula ≤ 2 (2W+3)^L (c len^k + 1)^(W L)174    have hpos := h.pos175    have hone : ∀ i, adm i → ∀ o, size (netFormula W (len i) (net i) o) ≤176        2 * ((2 * W + 3) ^ L * (c * len i ^ k + 1) ^ (W * L)) := by177      intro i hi o178      have h1 := (spec i hi o).2.2.1179      have hl := h.layers i hi180      have e1 : (2 * W + 3) ^ (net i).length ≤ (2 * W + 3) ^ L := Nat.pow_le_pow_right (by omega) hl181      have e2 : (c * len i ^ k + 1) ^ (W * (net i).length) ≤ (c * len i ^ k + 1) ^ (W * L) :=182        Nat.pow_le_pow_right (by omega) (Nat.mul_le_mul_left W hl)183      have := Nat.mul_le_mul e1 e2184      omega185    apply polyIn_mono (g := fun i => K i * (2 * ((2 * W + 3) ^ L * (c * len i ^ k + 1) ^ (W * L))))186    · intro i hi187      unfold tsize188      have := sum_map_le_mem (l := List.range (K i)) (f := fun o => size (netFormula W (len i) (net i) o))189        (g := fun _ => 2 * ((2 * W + 3) ^ L * (c * len i ^ k + 1) ^ (W * L))) (fun o _ => hone i hi o)190      rw [List.map_const', List.sum_replicate_nat, List.length_range] at this191      rw [List.map_map]192      exact this193    · apply polyIn_mul hK194      apply polyIn_mul (polyIn_const _ _ 2)195      apply polyIn_mul (polyIn_const _ _ _)196      apply polyIn_pow197      apply polyIn_add hpos _ (polyIn_const _ _ 1)198      apply polyIn_mul (polyIn_const _ _ c)199      apply polyIn_pow200      exact polyIn_leaf (fun i _ => Nat.le_refl _)201  · intro i hi hne o x202    exact (netFormula_wired (len i) (net i) (h.valid i hi) (hb i hi) (h.wired i hi) o203      (fun he => absurd he hne)).1 x

79/-- WINDOW SIMULATION THEOREM.  For a valid L-layer cell with fan-ins/widths ≤ M reading80    the input block and the w most recent states, the state after T updates is computed by81    formulas with depth ≤ 3·L·T, size ≤ rnnSize W M L T, reading only the T input blocks. -/82theorem window_ac0 {W M : Nat} (cell : List Layer) (hv : NetValid W cell) (hb : NetBounded M cell)83    (n m w : Nat) (h0 : Nat → Bool) : ∀ T i,84    (∀ x : Nat → Bool, eval x (wCirc W cell n m w h0 T i) = wState cell n m w h0 x T i) ∧85    size (wCirc W cell n m w h0 T i) ≤ rnnSize W M cell.length T ∧86    depth (wCirc W cell n m w h0 T i) ≤ 3 * cell.length * T ∧87    maxInput (wCirc W cell n m w h0 T i) ≤ T * n := by88  intro T89  induction T using Nat.strongRecOn with90  | ind T ih =>91    intro i92    cases T with93    | zero => simp [wCirc.eq_1, wState.eq_1, rnnSize]94    | succ t =>95      -- the leaves of the last update96      let prev : Nat → Circ := fun j => if j < n then input (t * n + j) else if j < n + w * m then97        (if (j - n) / m ≤ t then wCirc W cell n m w h0 (t - (j - n) / m) ((j - n) % m) else const (h0 ((j - n) % m)))98        else const false99      have hprev : ∀ j, size (prev j) ≤ rnnSize W M cell.length t ∧ depth (prev j) ≤ 3 * cell.length * t ∧100          maxInput (prev j) ≤ (t + 1) * n := by101        intro j102        simp only [prev]103        split104        · simp; refine ⟨rnnSize_pos _ _ _ _, ?_⟩; rw [Nat.succ_mul]; omega105        · split106          · split107            · next hδ =>108              have hlt : t - (j - n) / m < t + 1 := Nat.lt_succ_of_le (Nat.sub_le _ _)109              have hle : t - (j - n) / m ≤ t := Nat.sub_le _ _110              obtain ⟨_, h2, h3, h4⟩ := ih (t - (j - n) / m) hlt ((j - n) % m)111              refine ⟨Nat.le_trans h2 (rnnSize_mono W M _ hle), Nat.le_trans h3 (Nat.mul_le_mul_left _ hle),112                Nat.le_trans h4 ?_⟩113              rw [Nat.succ_mul]; exact Nat.le_trans (Nat.mul_le_mul_right n hle) (Nat.le_add_right _ _)114            · simp; exact rnnSize_pos _ _ _ _115          · simp; exact rnnSize_pos _ _ _ _116      have hsd := compileNet_sd (W := W) cell hb prev (rnnSize W M cell.length t) (3 * cell.length * t)117        (fun j => (hprev j).1) (fun j => (hprev j).2.1) i118      have hmx := compileNet_max (W := W) cell prev ((t + 1) * n) (fun j => (hprev j).2.2) i119      refine ⟨fun x => ?_, ?_, ?_, ?_⟩120      · rw [wCirc_succ, wState_succ, eval_compileNet cell hv]121        congr 1122        funext j123        unfold winIn124        split125        · simp126        · split127          · split128            · next hδ => simp only [if_pos hδ]; exact (ih (t - (j - n) / m) (Nat.lt_succ_of_le (Nat.sub_le _ _)) ((j - n) % m)).1 x129            · next hδ => simp [hδ]130          · simp131      · rw [wCirc_succ]; simp only [rnnSize]; exact hsd.1132      · rw [wCirc_succ]; have := hsd.2; rw [Nat.mul_succ]; omega133      · rw [wCirc_succ]; exact hmx

165/-- GATE-REALISED COMPOSITION THEOREM.  If every stage is a W-valid network with at most L166    layers and widths/fan-ins ≤ M, the K-stage model is computed (on zero-extended n-bit167    inputs) by formulas of depth ≤ 3·K·L, size ≤ 2 (2W+3)^{KL} (M+1)^{W·KL}, reading only168    the n inputs; the formulas compute the staged evaluation. -/169theorem staged_ac0 {W M L : Nat} (sts : List (List Layer)) (hv : ∀ st ∈ sts, NetValid W st)170    (hb : ∀ st ∈ sts, NetBounded M st) (hl : ∀ st ∈ sts, st.length ≤ L) (n i : Nat) :171    (∀ x : Nat → Bool, eval x (netFormula W n sts.flatten i) = runStages sts (pad n x) i) ∧172    depth (netFormula W n sts.flatten i) ≤ 3 * (sts.length * L) ∧173    size (netFormula W n sts.flatten i) ≤ 2 * ((2 * W + 3) ^ (sts.length * L) * (M + 1) ^ (W * (sts.length * L))) ∧174    maxInput (netFormula W n sts.flatten i) ≤ n := by175  have hv' : NetValid W sts.flatten := by176    intro l hl' g hg177    obtain ⟨st, hst, hlst⟩ := List.mem_flatten.mp hl'178    exact hv st hst l hlst g hg179  have hb' : NetBounded M sts.flatten := by180    intro l hl'181    obtain ⟨st, hst, hlst⟩ := List.mem_flatten.mp hl'182    exact hb st hst l hlst183  obtain ⟨h1, h2, h3, h4⟩ := netFormula_spec n sts.flatten hv' hb' i184  have hlen := flatten_length_le hl185  refine ⟨fun x => by rw [h1, evalNet_flatten], Nat.le_trans h2 (Nat.mul_le_mul_left 3 hlen), Nat.le_trans h3 ?_, h4⟩186  apply Nat.mul_le_mul_left187  exact Nat.mul_le_mul (Nat.pow_le_pow_right (by omega) hlen)188    (Nat.pow_le_pow_right (by omega) (Nat.mul_le_mul_left W hlen))