Circuit

Comment and keyword shading is a reading aid only. It is not a verification marker; the evidence is the build record on the Build page.

1import NimProbability23/- Phase 3, target C: network-to-AC0 simulation.  Written by Claude (10 October 2026).4   Lean 4.26.0, core/Std only.56   Circuit model.  `Circ` is a Boolean FORMULA (tree, no sharing) over input7   variables indexed by Nat, with constants, NOT, and unbounded fan-in AND/OR.8     size  = number of formula nodes (leaves, NOT, AND, OR).  A formula-size9             bound is also a circuit-size bound (gates + wires is at most twice it).10     depth = longest root-to-leaf path counting every AND, OR and NOT node.11   Gates (paper Definition NN-formal, after clearing the denominator D > 0):12     nonnegative integer coefficients a_j on literals z_j XOR eta_j, integer13     threshold b, firing iff  b ≤ Σ_j a_j [z_j XOR eta_j].  Validity: b ≤ W14     (and a_j ≤ W, which the construction does not need).15   Proved here:16     * rational form with denominator D > 0 ↔ integer form (gate_rat_iff);17     * bounded witness lemma (≤ b ≤ W true literals suffice);18     * DNF compilation with semantic equality, depth ≤ 3 and size19       ≤ 1 + (m+1)^W (2W+1), including b = 0, m = 0 and W = 0;20     * layer/network composition by substitution, with depth ≤ 3L and size21       ≤ 2 (2W+3)^L (M+1)^(W L) for L layers of fan-in/width ≤ M;22     * network-family statement with widths ≤ c (n+1)^k (polynomial bound);23     * recurrent unrolling for a fixed number T of updates from an24       input-independent initial state.25   Not formalised: softmax or any attention primitive not already built from26   these gates; floating-point semantics; trained models. -/2728namespace NimAudit29namespace AC03031open Prob3233attribute [local simp] Rat.add_zero Rat.zero_add Rat.zero_mul Rat.mul_zero Rat.one_mul3435inductive Circ where36  | input (i : Nat)37  | const (b : Bool)38  | not (c : Circ)39  | and (cs : List Circ)40  | or (cs : List Circ)4142namespace Circ4344def 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)5051def 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 + 15758/-- Maximum of a list of naturals (0 for the empty list). -/59def listMax (l : List Nat) : Nat := l.foldr max 06061def 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)) + 16768/-- 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))7576/-- Substitute circuits for input variables. -/77def subst (σ : Nat → Circ) : Circ → Circ78  | input i => σ i79  | const b => const b80  | not c => not (subst σ c)81  | and cs => and (cs.attach.map (fun ⟨c, _⟩ => subst σ c))82  | or cs => or (cs.attach.map (fun ⟨c, _⟩ => subst σ c))8384@[simp] theorem eval_input (x : Nat → Bool) (i : Nat) : eval x (input i) = x i := by simp [eval]85@[simp] theorem eval_const (x : Nat → Bool) (b : Bool) : eval x (const b) = b := by simp [eval]86@[simp] theorem eval_not (x : Nat → Bool) (c : Circ) : eval x (not c) = !(eval x c) := by87  simp [eval]88@[simp] theorem eval_and (x : Nat → Bool) (cs : List Circ) : eval x (and cs) = cs.all (eval x) := by89  simp [eval]90@[simp] theorem eval_or (x : Nat → Bool) (cs : List Circ) : eval x (or cs) = cs.any (eval x) := by91  simp [eval]92@[simp] theorem size_input (i : Nat) : size (input i) = 1 := by simp [size]93@[simp] theorem size_const (b : Bool) : size (const b) = 1 := by simp [size]94@[simp] theorem size_not (c : Circ) : size (not c) = size c + 1 := by simp [size]95@[simp] theorem size_and (cs : List Circ) : size (and cs) = (cs.map size).sum + 1 := by simp [size]96@[simp] theorem size_or (cs : List Circ) : size (or cs) = (cs.map size).sum + 1 := by simp [size]97@[simp] theorem depth_input (i : Nat) : depth (input i) = 0 := by simp [depth]98@[simp] theorem depth_const (b : Bool) : depth (const b) = 0 := by simp [depth]99@[simp] theorem depth_not (c : Circ) : depth (not c) = depth c + 1 := by simp [depth]100@[simp] theorem depth_and (cs : List Circ) : depth (and cs) = listMax (cs.map depth) + 1 := by101  simp [depth]102@[simp] theorem depth_or (cs : List Circ) : depth (or cs) = listMax (cs.map depth) + 1 := by103  simp [depth]104@[simp] theorem maxInput_input (i : Nat) : maxInput (input i) = i + 1 := by simp [maxInput]105@[simp] theorem maxInput_const (b : Bool) : maxInput (const b) = 0 := by simp [maxInput]106@[simp] theorem maxInput_not (c : Circ) : maxInput (not c) = maxInput c := by simp [maxInput]107@[simp] theorem maxInput_and (cs : List Circ) : maxInput (and cs) = listMax (cs.map maxInput) := by108  simp [maxInput]109@[simp] theorem maxInput_or (cs : List Circ) : maxInput (or cs) = listMax (cs.map maxInput) := by110  simp [maxInput]111@[simp] theorem subst_input (σ : Nat → Circ) (i : Nat) : subst σ (input i) = σ i := by simp [subst]112@[simp] theorem subst_const (σ : Nat → Circ) (b : Bool) : subst σ (const b) = const b := by113  simp [subst]114@[simp] theorem subst_not (σ : Nat → Circ) (c : Circ) : subst σ (not c) = not (subst σ c) := by115  simp [subst]116@[simp] theorem subst_and (σ : Nat → Circ) (cs : List Circ) :117    subst σ (and cs) = and (cs.map (subst σ)) := by simp [subst]118@[simp] theorem subst_or (σ : Nat → Circ) (cs : List Circ) :119    subst σ (or cs) = or (cs.map (subst σ)) := by simp [subst]120121theorem le_listMax {l : List Nat} {a : Nat} (h : a ∈ l) : a ≤ listMax l := by122  induction l with123  | nil => simp at h124  | cons b l ih =>125    simp only [listMax, List.foldr_cons] at *126    rcases List.mem_cons.mp h with rfl | h127    · omega128    · have := ih h; omega129130theorem listMax_le {l : List Nat} {d : Nat} (h : ∀ a ∈ l, a ≤ d) : listMax l ≤ d := by131  induction l with132  | nil => simp [listMax]133  | cons b l ih =>134    simp only [listMax, List.foldr_cons]135    have h1 := h b (by simp)136    have h2 := ih (fun a ha => h a (List.mem_cons_of_mem _ ha))137    simp only [listMax] at h2138    omega139140theorem all_congr_mem {α : Type} {l : List α} {f g : α → Bool} (h : ∀ a ∈ l, f a = g a) :141    l.all f = l.all g := by142  induction l with143  | nil => rfl144  | cons a l ih =>145    simp only [List.all_cons]146    rw [h a (by simp), ih (fun b hb => h b (List.mem_cons_of_mem _ hb))]147148theorem any_congr_mem {α : Type} {l : List α} {f g : α → Bool} (h : ∀ a ∈ l, f a = g a) :149    l.any f = l.any g := by150  induction l with151  | nil => rfl152  | cons a l ih =>153    simp only [List.any_cons]154    rw [h a (by simp), ih (fun b hb => h b (List.mem_cons_of_mem _ hb))]155156theorem sum_map_le_mem {α : Type} {l : List α} {f g : α → Nat} (h : ∀ a ∈ l, f a ≤ g a) :157    (l.map f).sum ≤ (l.map g).sum := by158  induction l with159  | nil => simp160  | cons a l ih =>161    simp only [List.map_cons, List.sum_cons]162    have := h a (by simp)163    have := ih (fun b hb => h b (List.mem_cons_of_mem _ hb))164    omega165166theorem sum_map_mul_right {α : Type} (l : List α) (f : α → Nat) (k : Nat) :167    (l.map (fun a => f a * k)).sum = (l.map f).sum * k := by168  induction l with169  | nil => simp170  | cons a l ih => simp only [List.map_cons, List.sum_cons, ih, Nat.add_mul]171172/-- Substitution is composition of semantics. -/173theorem eval_subst (σ : Nat → Circ) (x : Nat → Bool) : ∀ c : Circ,174    eval x (subst σ c) = eval (fun i => eval x (σ i)) c175  | input i => by simp176  | const b => by simp177  | not c => by simp [eval_subst σ x c]178  | and cs => by179    simp only [subst_and, eval_and, List.all_map]180    exact all_congr_mem (fun c _ => eval_subst σ x c)181  | or cs => by182    simp only [subst_or, eval_or, List.any_map]183    exact any_congr_mem (fun c _ => eval_subst σ x c)184185/-- Size of a substitution: each leaf grows to at most S + 1 nodes. -/186theorem size_subst_le (σ : Nat → Circ) (S : Nat) (hσ : ∀ i, size (σ i) ≤ S) : ∀ c : Circ,187    size (subst σ c) ≤ size c * (S + 1)188  | input i => by simp; have := hσ i; omega189  | const b => by simp190  | not c => by191    have := size_subst_le σ S hσ c192    simp only [subst_not, size_not, Nat.add_mul, Nat.one_mul]193    omega194  | and cs => by195    simp only [subst_and, size_and, List.map_map, Nat.add_mul, Nat.one_mul]196    have h := sum_map_le_mem (l := cs) (f := size ∘ subst σ) (g := fun c => size c * (S + 1))197      (fun c _ => size_subst_le σ S hσ c)198    rw [sum_map_mul_right] at h199    omega200  | or cs => by201    simp only [subst_or, size_or, List.map_map, Nat.add_mul, Nat.one_mul]202    have h := sum_map_le_mem (l := cs) (f := size ∘ subst σ) (g := fun c => size c * (S + 1))203      (fun c _ => size_subst_le σ S hσ c)204    rw [sum_map_mul_right] at h205    omega206207/-- Depth of a substitution: at most depth c + D. -/208theorem depth_subst_le (σ : Nat → Circ) (D : Nat) (hσ : ∀ i, depth (σ i) ≤ D) : ∀ c : Circ,209    depth (subst σ c) ≤ depth c + D210  | input i => by simp; exact hσ i211  | const b => by simp212  | not c => by have := depth_subst_le σ D hσ c; simp; omega213  | and cs => by214    simp only [subst_and, depth_and, List.map_map]215    have : listMax (cs.map (depth ∘ subst σ)) ≤ listMax (cs.map depth) + D := by216      apply listMax_le217      intro a ha218      obtain ⟨c, hc, rfl⟩ := List.mem_map.mp ha219      have h1 := depth_subst_le σ D hσ c220      have h2 := le_listMax (List.mem_map_of_mem (f := depth) hc)221      simp only [Function.comp]; omega222    omega223  | or cs => by224    simp only [subst_or, depth_or, List.map_map]225    have : listMax (cs.map (depth ∘ subst σ)) ≤ listMax (cs.map depth) + D := by226      apply listMax_le227      intro a ha228      obtain ⟨c, hc, rfl⟩ := List.mem_map.mp ha229      have h1 := depth_subst_le σ D hσ c230      have h2 := le_listMax (List.mem_map_of_mem (f := depth) hc)231      simp only [Function.comp]; omega232    omega233234/-- Substituting leaves (inputs or constants) preserves size and depth exactly. -/235def IsLeaf : Circ → Prop236  | input _ => True237  | const _ => True238  | _ => False239240theorem size_leaf {c : Circ} (h : IsLeaf c) : size c = 1 := by241  cases c <;> simp_all [IsLeaf]242243theorem depth_leaf {c : Circ} (h : IsLeaf c) : depth c = 0 := by244  cases c <;> simp_all [IsLeaf]245246theorem size_subst_leaf (σ : Nat → Circ) (hσ : ∀ i, IsLeaf (σ i)) : ∀ c : Circ,247    size (subst σ c) = size c248  | input i => by simp [size_leaf (hσ i)]249  | const b => by simp250  | not c => by simp [size_subst_leaf σ hσ c]251  | and cs => by252    simp only [subst_and, size_and, List.map_map]253    congr 2254    exact List.map_congr_left (fun c _ => size_subst_leaf σ hσ c)255  | or cs => by256    simp only [subst_or, size_or, List.map_map]257    congr 2258    exact List.map_congr_left (fun c _ => size_subst_leaf σ hσ c)259260theorem depth_subst_leaf (σ : Nat → Circ) (hσ : ∀ i, IsLeaf (σ i)) : ∀ c : Circ,261    depth (subst σ c) = depth c262  | input i => by simp [depth_leaf (hσ i)]263  | const b => by simp264  | not c => by simp [depth_subst_leaf σ hσ c]265  | and cs => by266    simp only [subst_and, depth_and, List.map_map]267    congr 2268    exact List.map_congr_left (fun c _ => depth_subst_leaf σ hσ c)269  | or cs => by270    simp only [subst_or, depth_or, List.map_map]271    congr 2272    exact List.map_congr_left (fun c _ => depth_subst_leaf σ hσ c)273274/-- Inputs of a substitution: bounded when every substituted circuit is bounded. -/275theorem maxInput_subst_le (σ : Nat → Circ) (m : Nat) (hσ : ∀ i, maxInput (σ i) ≤ m) :276    ∀ c : Circ, maxInput (subst σ c) ≤ m277  | input i => by simp; exact hσ i278  | const b => by simp279  | not c => by simp; exact maxInput_subst_le σ m hσ c280  | and cs => by281    simp only [subst_and, maxInput_and, List.map_map]282    apply listMax_le283    intro a ha284    obtain ⟨c, _, rfl⟩ := List.mem_map.mp ha285    exact maxInput_subst_le σ m hσ c286  | or cs => by287    simp only [subst_or, maxInput_or, List.map_map]288    apply listMax_le289    intro a ha290    obtain ⟨c, _, rfl⟩ := List.mem_map.mp ha291    exact maxInput_subst_le σ m hσ c292293/-- Evaluation depends only on inputs below maxInput. -/294theorem eval_congr_below (x y : Nat → Bool) : ∀ c : Circ,295    (∀ i, i < maxInput c → x i = y i) → eval x c = eval y c296  | input i => by intro h; simp; exact h i (by simp)297  | const b => by intro _; simp298  | not c => by intro h; simp only [eval_not]; rw [eval_congr_below x y c (by simpa using h)]299  | and cs => by300    intro h301    simp only [eval_and]302    apply all_congr_mem303    intro c hc304    apply eval_congr_below x y c305    intro i hi306    apply h i307    simp only [maxInput_and]308    exact Nat.lt_of_lt_of_le hi (le_listMax (List.mem_map_of_mem hc))309  | or cs => by310    intro h311    simp only [eval_or]312    apply any_congr_mem313    intro c hc314    apply eval_congr_below x y c315    intro i hi316    apply h i317    simp only [maxInput_or]318    exact Nat.lt_of_lt_of_le hi (le_listMax (List.mem_map_of_mem hc))319320end Circ321322open Circ323324/-! ## Threshold gates -/325326/-- 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 : Nat332333namespace Gate334335def fanin (g : Gate) : Nat := g.coeffs.length336def coeff (g : Gate) (j : Nat) : Nat := g.coeffs.getD j 0337def lit (g : Gate) (z : Nat → Bool) (j : Nat) : Bool := xor (z j) (g.negs.getD j false)338339/-- Partial weighted sum over the first c inputs. -/340def psum (g : Gate) (z : Nat → Bool) (c : Nat) : Nat :=341  ((List.range c).map (fun j => g.coeff j * (if g.lit z j then 1 else 0))).sum342343def wsum (g : Gate) (z : Nat → Bool) : Nat := g.psum z g.fanin344345/-- 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)347348/-- Fixed-scale validity: threshold and coefficients in 0..W. -/349def Valid (W : Nat) (g : Gate) : Prop := g.thr ≤ W ∧ ∀ a ∈ g.coeffs, a ≤ W350351end Gate352353/-! ### Rational form with denominator D -/354355/-- 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)360361theorem rsum_natCast (l : List Nat) (f : Nat → Nat) :362    rsum l (fun j => ((f j : Nat) : Rat)) = (((l.map f).sum : Nat) : Rat) := by363  induction l with364  | nil => simp365  | cons a l ih => simp only [rsum_cons, ih, List.map_cons, List.sum_cons, Rat.natCast_add]366367/-- 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    grind406407/-! ### Nat sums over ranges -/408409def nsum (c : Nat) (f : Nat → Nat) : Nat := ((List.range c).map f).sum410411theorem nsum_succ (c : Nat) (f : Nat → Nat) : nsum (c + 1) f = nsum c f + f c := by412  simp [nsum, List.range_succ, List.sum_append_nat]413414theorem nsum_zero (f : Nat → Nat) : nsum 0 f = 0 := rfl415416theorem nsum_le {c : Nat} {f g : Nat → Nat} (h : ∀ j < c, f j ≤ g j) : nsum c f ≤ nsum c g := by417  induction c with418  | zero => simp [nsum]419  | succ c ih =>420    rw [nsum_succ, nsum_succ]421    have := ih (fun j hj => h j (by omega))422    have := h c (by omega)423    omega424425theorem nsum_congr {c : Nat} {f g : Nat → Nat} (h : ∀ j < c, f j = g j) : nsum c f = nsum c g := by426  induction c with427  | zero => rfl428  | succ c ih => rw [nsum_succ, nsum_succ, ih (fun j hj => h j (by omega)), h c (by omega)]429430theorem nsum_mono (f : Nat → Nat) {c d : Nat} (h : c ≤ d) : nsum c f ≤ nsum d f := by431  induction d with432  | zero => have : c = 0 := by omega433            subst this; exact Nat.le_refl _434  | succ d ih =>435    by_cases hc : c = d + 1436    · subst hc; exact Nat.le_refl _437    · rw [nsum_succ]; have := ih (by omega); omega438439/-- Restricting the sum to j < c. -/440theorem nsum_cut (f : Nat → Nat) {c m : Nat} (h : c ≤ m) :441    nsum m (fun j => if j < c then f j else 0) = nsum c f := by442  induction m with443  | zero => have : c = 0 := by omega444            subst this; rfl445  | succ m ih =>446    by_cases hc : c = m + 1447    · subst hc448      rw [nsum_succ, nsum_succ]449      rw [nsum_congr (g := f) (fun j hj => by simp [show j < m + 1 by omega])]450      simp451    · rw [nsum_succ, ih (by omega)]452      simp [show ¬ m < c by omega]453454theorem length_filter_eq_nsum (c : Nat) (p : Nat → Bool) :455    ((List.range c).filter p).length = nsum c (fun j => if p j then 1 else 0) := by456  induction c with457  | zero => rfl458  | succ c ih =>459    rw [List.range_succ, List.filter_append, List.length_append, ih, nsum_succ]460    cases hp : p c <;> simp [hp]461462/-! ### Bounded witness lemma -/463464namespace Gate465466theorem psum_succ (g : Gate) (z : Nat → Bool) (c : Nat) :467    g.psum z (c + 1) = g.psum z c + g.coeff c * (if g.lit z c then 1 else 0) := by468  simp [psum, List.range_succ, List.sum_append_nat]469470theorem psum_mono (g : Gate) (z : Nat → Bool) {c d : Nat} (h : c ≤ d) : g.psum z c ≤ g.psum z d :=471  nsum_mono _ h472473/-- The active (true, positive-coefficient) literals among the first c inputs. -/474def active (g : Gate) (z : Nat → Bool) (c : Nat) : List Nat :=475  (List.range c).filter (fun j => g.lit z j && decide (1 ≤ g.coeff j))476477theorem active_length_le (g : Gate) (z : Nat → Bool) (c : Nat) :478    (g.active z c).length ≤ g.psum z c := by479  unfold active480  rw [length_filter_eq_nsum]481  unfold psum482  apply nsum_le483  intro j _484  by_cases hl : g.lit z j = true <;> by_cases ha : 1 ≤ g.coeff j <;> simp [hl, ha] <;> omega485486theorem exists_cut (g : Gate) (z : Nat → Bool) (c : Nat) (h : g.thr ≤ g.psum z c) :487    ∃ c' ≤ c, g.thr ≤ g.psum z c' ∧ ∀ c'' < c', g.psum z c'' < g.thr := by488  induction c with489  | zero => exact ⟨0, Nat.le_refl _, h, fun c'' hc'' => by omega⟩490  | succ c ih =>491    by_cases hc : g.thr ≤ g.psum z c492    · obtain ⟨c', hc', h1, h2⟩ := ih hc493      exact ⟨c', by omega, h1, h2⟩494    · refine ⟨c + 1, Nat.le_refl _, h, ?_⟩495      intro c'' hc''496      have := g.psum_mono z (show c'' ≤ c by omega)497      omega498499/-- 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 h1539540end Gate541542/-! ### DNF compilation of one gate -/543544/-- Literal circuit for input j of gate g. -/545def litC (g : Gate) (j : Nat) : Circ :=546  if g.negs.getD j false then not (input j) else input j547548theorem eval_litC (g : Gate) (z : Nat → Bool) (j : Nat) : eval z (litC g j) = g.lit z j := by549  unfold litC Gate.lit550  cases g.negs.getD j false <;> simp551552/-- Sum of coefficients of the positions (below the fan-in) occurring in tuple t. -/553def selSum (g : Gate) (t : List Nat) : Nat :=554  nsum g.fanin (fun j => if j ∈ t then g.coeff j else 0)555556/-- The conjunction of the literals named in t (entries ≥ fan-in are padding). -/557def termC (g : Gate) (t : List Nat) : Circ :=558  and (t.filterMap (fun j => if j < g.fanin then some (litC g j) else none))559560/-- 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))563564theorem mem_boards_of {q N : Nat} {P : List Nat} (hl : P.length = N) (hb : ∀ x ∈ P, x < q) :565    P ∈ boards q N := by566  induction N generalizing P with567  | zero => cases P with568    | nil => simp [boards]569    | cons _ _ => simp at hl570  | succ N ih =>571    cases P with572    | nil => simp at hl573    | cons x P =>574      simp only [boards, List.mem_flatMap, List.mem_range, List.mem_map]575      refine ⟨x, hb x (by simp), P, ih (by simpa using hl) (fun y hy => hb y (by simp [hy])), rfl⟩576577theorem length_boards (q N : Nat) : (boards q N).length = q ^ N := by578  induction N with579  | zero => simp [boards]580  | succ N ih =>581    simp only [boards, List.length_flatMap, List.length_map, ih]582    rw [List.map_const', List.sum_replicate_nat, List.length_range, Nat.pow_succ, Nat.mul_comm]583584theorem eval_termC (g : Gate) (z : Nat → Bool) (t : List Nat) :585    eval z (termC g t) = true ↔ ∀ j ∈ t, j < g.fanin → g.lit z j = true := by586  unfold termC587  simp only [eval_and, List.all_eq_true, List.mem_filterMap]588  constructor589  · intro h j hj hjm590    have := h (litC g j) ⟨j, hj, by simp [hjm]⟩591    rwa [eval_litC] at this592  · rintro h c ⟨j, hj, hc⟩593    by_cases hjm : j < g.fanin594    · simp only [hjm, if_true, Option.some.injEq] at hc595      subst hc596      rw [eval_litC]597      exact h j hj hjm598    · simp [hjm] at hc599600/-- 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)).1651652theorem size_termC (g : Gate) (t : List Nat) : size (termC g t) ≤ 2 * t.length + 1 := by653  unfold termC654  simp only [size_and]655  have h : ∀ (l : List Nat),656      ((l.filterMap (fun j => if j < g.fanin then some (litC g j) else none)).map size).sum ≤657        2 * l.length := by658    intro l659    induction l with660    | nil => simp661    | cons j l ih =>662      simp only [List.filterMap_cons, List.length_cons]663      by_cases hj : j < g.fanin664      · simp only [hj, if_true, List.map_cons, List.sum_cons]665        have : size (litC g j) ≤ 2 := by unfold litC; split <;> simp666        omega667      · simp only [hj, if_false]; omega668  have := h t669  omega670671theorem depth_termC (g : Gate) (t : List Nat) : depth (termC g t) ≤ 2 := by672  unfold termC673  simp only [depth_and]674  have : listMax ((t.filterMap (fun j => if j < g.fanin then some (litC g j) else none)).map depth) ≤ 1 := by675    apply listMax_le676    intro a ha677    obtain ⟨c, hc, rfl⟩ := List.mem_map.mp ha678    obtain ⟨j, _, hj⟩ := List.mem_filterMap.mp hc679    by_cases hjm : j < g.fanin680    · simp only [hjm, if_true, Option.some.injEq] at hj681      subst hj; unfold litC; split <;> simp682    · simp [hjm] at hj683  omega684685theorem maxInput_termC (g : Gate) (t : List Nat) : maxInput (termC g t) ≤ g.fanin := by686  unfold termC687  simp only [maxInput_and]688  apply listMax_le689  intro a ha690  obtain ⟨c, hc, rfl⟩ := List.mem_map.mp ha691  obtain ⟨j, _, hj⟩ := List.mem_filterMap.mp hc692  by_cases hjm : j < g.fanin693  · simp only [hjm, if_true, Option.some.injEq] at hj694    subst hj; unfold litC; split <;> simp <;> omega695  · simp [hjm] at hj696697/-- DNF SIZE: at most 1 + (m+1)^W (2W+1) formula nodes, m = fan-in. -/698theorem size_dnf (W : Nat) (g : Gate) : size (dnf W g) ≤ 1 + (g.fanin + 1) ^ W * (2 * W + 1) := by699  unfold dnf700  simp only [size_or, List.map_map]701  have hterm : ∀ t ∈ (boards (g.fanin + 1) W).filter (fun t => decide (g.thr ≤ selSum g t)),702      (size ∘ termC g) t ≤ 2 * W + 1 := by703    intro t ht704    have hmem := (List.mem_filter.mp ht).1705    have hl := (mem_boards hmem).1706    have := size_termC g t707    simp only [Function.comp]; omega708  have h1 := sum_map_le_mem hterm709  rw [List.map_const', List.sum_replicate_nat] at h1710  have h2 : ((boards (g.fanin + 1) W).filter (fun t => decide (g.thr ≤ selSum g t))).length ≤711      (g.fanin + 1) ^ W := by712    rw [← length_boards]; exact List.length_filter_le _ _713  have h3 := Nat.mul_le_mul_right (2 * W + 1) h2714  omega715716theorem depth_dnf (W : Nat) (g : Gate) : depth (dnf W g) ≤ 3 := by717  unfold dnf718  simp only [depth_or, List.map_map]719  have : listMax (((boards (g.fanin + 1) W).filter720      (fun t => decide (g.thr ≤ selSum g t))).map (depth ∘ termC g)) ≤ 2 := by721    apply listMax_le722    intro a ha723    obtain ⟨t, _, rfl⟩ := List.mem_map.mp ha724    exact depth_termC g t725  omega726727theorem maxInput_dnf (W : Nat) (g : Gate) : maxInput (dnf W g) ≤ g.fanin := by728  unfold dnf729  simp only [maxInput_or, List.map_map]730  apply listMax_le731  intro a ha732  obtain ⟨t, _, rfl⟩ := List.mem_map.mp ha733  exact maxInput_termC g t734735/-- 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⟩740741/-! ## Layers and networks -/742743/-- A layer: a list of gates reading the previous layer's outputs (indexed by Nat). -/744abbrev Layer := List Gate745746def evalLayer (l : Layer) (z : Nat → Bool) : Nat → Bool :=747  fun i => match l[i]? with748    | some g => g.eval z749    | none => false750751/-- A network: layers applied in order. -/752def evalNet : List Layer → (Nat → Bool) → (Nat → Bool)753  | [], z => z754  | l :: ls, z => evalNet ls (evalLayer l z)755756def compileLayer (W : Nat) (l : Layer) (prev : Nat → Circ) : Nat → Circ :=757  fun i => match l[i]? with758    | some g => subst prev (dnf W g)759    | none => const false760761def compileNet (W : Nat) : List Layer → (Nat → Circ) → (Nat → Circ)762  | [], prev => prev763  | l :: ls, prev => compileNet W ls (compileLayer W l prev)764765/-- All gates valid for W. -/766def NetValid (W : Nat) (ls : List Layer) : Prop := ∀ l ∈ ls, ∀ g ∈ l, Gate.Valid W g767768/-- Fan-in and width bounded by M. -/769def NetBounded (M : Nat) (ls : List Layer) : Prop := ∀ l ∈ ls, l.length ≤ M ∧ ∀ g ∈ l, g.fanin ≤ M770771theorem eval_compileLayer {W : Nat} (l : Layer) (hv : ∀ g ∈ l, Gate.Valid W g)772    (prev : Nat → Circ) (x : Nat → Bool) (i : Nat) :773    eval x (compileLayer W l prev i) = evalLayer l (fun j => eval x (prev j)) i := by774  unfold compileLayer evalLayer775  cases h : l[i]? with776  | none => simp777  | some g =>778    simp only779    rw [eval_subst, eval_dnf g (hv g (List.mem_of_getElem? h)).1]780781/-- NETWORK CORRECTNESS: compiled circuits compute the network. -/782theorem eval_compileNet {W : Nat} : ∀ (ls : List Layer), NetValid W ls →783    ∀ (prev : Nat → Circ) (x : Nat → Bool) (i : Nat),784      eval x (compileNet W ls prev i) = evalNet ls (fun j => eval x (prev j)) i785  | [], _, prev, x, i => rfl786  | l :: ls, hv, prev, x, i => by787    simp only [compileNet, evalNet]788    rw [eval_compileNet ls (fun l' hl' => hv l' (List.mem_cons_of_mem _ hl'))]789    congr 1790    funext j791    exact eval_compileLayer l (hv l (by simp)) prev x j792793/-- Per-layer size factor G = 1 + (M+1)^W (2W+1). -/794def gfac (W M : Nat) : Nat := 1 + (M + 1) ^ W * (2 * W + 1)795796/-- Size bound after L layers starting from circuits of size ≤ S. -/797def sizeBound (W M S : Nat) : Nat → Nat798  | 0 => S799  | L + 1 => gfac W M * (sizeBound W M S L + 1)800801theorem compileLayer_size {W M S : Nat} (l : Layer) (hb : ∀ g ∈ l, g.fanin ≤ M)802    (prev : Nat → Circ) (hp : ∀ j, size (prev j) ≤ S) (i : Nat) :803    size (compileLayer W l prev i) ≤ gfac W M * (S + 1) := by804  unfold compileLayer805  cases h : l[i]? with806  | none => simp only; simp; have : 1 ≤ gfac W M := by unfold gfac; omega807            exact Nat.le_trans this (Nat.le_mul_of_pos_right _ (by omega))808  | some g =>809    simp only810    have h1 := size_subst_le prev S hp (dnf W g)811    have h2 := size_dnf W g812    have hf := hb g (List.mem_of_getElem? h)813    have h3 : (g.fanin + 1) ^ W ≤ (M + 1) ^ W := Nat.pow_le_pow_left (by omega) W814    have h4 : size (dnf W g) ≤ gfac W M := by815      unfold gfac; have := Nat.mul_le_mul_right (2 * W + 1) h3; omega816    exact Nat.le_trans h1 (Nat.mul_le_mul_right _ h4)817818theorem compileLayer_depth {W D : Nat} (l : Layer) (prev : Nat → Circ)819    (hp : ∀ j, depth (prev j) ≤ D) (i : Nat) : depth (compileLayer W l prev i) ≤ D + 3 := by820  unfold compileLayer821  cases h : l[i]? with822  | none => simp823  | some g =>824    simp only825    have h1 := depth_subst_le prev D hp (dnf W g)826    have h2 := depth_dnf W g827    omega828829theorem compileLayer_maxInput {W m : Nat} (l : Layer) (prev : Nat → Circ)830    (hp : ∀ j, maxInput (prev j) ≤ m) (i : Nat) : maxInput (compileLayer W l prev i) ≤ m := by831  unfold compileLayer832  cases h : l[i]? with833  | none => simp834  | some g => exact maxInput_subst_le prev m hp (dnf W g)835836theorem sizeBound_succ' (W M L S : Nat) :837    sizeBound W M (gfac W M * (S + 1)) L = sizeBound W M S (L + 1) := by838  induction L generalizing S with839  | zero => rfl840  | succ L ih => simp only [sizeBound] at *; rw [ih]841842/-- NETWORK SIZE/DEPTH: L = ls.length layers with fan-ins ≤ M, from circuits of size843    ≤ S and depth ≤ D, give circuits of size ≤ sizeBound W M S L and depth ≤ D + 3L. -/844theorem compileNet_sd {W M : Nat} : ∀ (ls : List Layer), NetBounded M ls →845    ∀ (prev : Nat → Circ) (S D : Nat), (∀ j, size (prev j) ≤ S) → (∀ j, depth (prev j) ≤ D) →846      ∀ i, size (compileNet W ls prev i) ≤ sizeBound W M S ls.length ∧847        depth (compileNet W ls prev i) ≤ D + 3 * ls.length848  | [], _, prev, S, D, hs, hd, i => ⟨by simpa [sizeBound] using hs i, by simpa using hd i⟩849  | l :: ls, hb, prev, S, D, hs, hd, i => by850    have hl := hb l (by simp)851    have := compileNet_sd (W := W) ls (fun l' hl' => hb l' (List.mem_cons_of_mem _ hl'))852      (compileLayer W l prev) (gfac W M * (S + 1)) (D + 3)853      (compileLayer_size l hl.2 prev hs) (compileLayer_depth l prev hd) i854    simp only [compileNet, List.length_cons]855    refine ⟨?_, ?_⟩856    · rw [← sizeBound_succ']; exact this.1857    · have := this.2; omega858859/-- Compiled circuits read only inputs read by the starting circuits. -/860theorem compileNet_max {W : Nat} : ∀ (ls : List Layer) (prev : Nat → Circ) (m : Nat),861    (∀ j, maxInput (prev j) ≤ m) → ∀ i, maxInput (compileNet W ls prev i) ≤ m862  | [], prev, m, hm, i => hm i863  | l :: ls, prev, m, hm, i => by864    simp only [compileNet]865    exact compileNet_max ls (compileLayer W l prev) m (compileLayer_maxInput l prev hm) i866867theorem gfac_le (W M : Nat) : gfac W M + 1 ≤ (2 * W + 3) * (M + 1) ^ W := by868  unfold gfac869  have hp : 1 ≤ (M + 1) ^ W := Nat.pow_pos (by omega)870  generalize (M + 1) ^ W = p at *871  have e1 : p * (2 * W + 1) = 2 * (W * p) + p := by grind872  have e2 : (2 * W + 3) * p = 2 * (W * p) + 3 * p := by grind873  rw [e1, e2]874  omega875876theorem pow_step (W M L : Nat) :877    (2 * W + 3) * (M + 1) ^ W * ((2 * W + 3) ^ L * (M + 1) ^ (W * L)) =878      (2 * W + 3) ^ (L + 1) * (M + 1) ^ (W * (L + 1)) := by879  rw [Nat.pow_succ (2 * W + 3) L, show W * (L + 1) = W * L + W by rw [Nat.mul_succ], Nat.pow_add]880  generalize (2 * W + 3) ^ L = A881  generalize (M + 1) ^ (W * L) = B'882  generalize (M + 1) ^ W = C883  generalize 2 * W + 3 = E884  grind885886theorem sizeBound_pos (W M L : Nat) {S : Nat} (hS : 1 ≤ S) : 1 ≤ sizeBound W M S L := by887  induction L with888  | zero => simpa [sizeBound]889  | succ L ih =>890    simp only [sizeBound]891    have : 1 ≤ gfac W M := by unfold gfac; omega892    have := Nat.mul_le_mul this (show 1 ≤ sizeBound W M S L + 1 by omega)893    omega894895/-- Closed form: sizeBound W M S L + 1 ≤ (S+1) (2W+3)^L (M+1)^(W L). -/896theorem sizeBound_affine (W M L S : Nat) :897    sizeBound W M S L + 1 ≤ (S + 1) * ((2 * W + 3) ^ L * (M + 1) ^ (W * L)) := by898  have hG := gfac_le W M899  induction L with900  | zero =>901    simp only [sizeBound, Nat.pow_zero, Nat.mul_zero, Nat.one_mul]902    omega903  | succ L ih =>904    simp only [sizeBound]905    have h1 : gfac W M * (sizeBound W M S L + 1) + 1 ≤ (gfac W M + 1) * (sizeBound W M S L + 1) := by906      rw [Nat.add_mul, Nat.one_mul]; omega907    have h2 := Nat.mul_le_mul hG ih908    have e : (2 * W + 3) * (M + 1) ^ W * ((S + 1) * ((2 * W + 3) ^ L * (M + 1) ^ (W * L))) =909        (S + 1) * ((2 * W + 3) ^ (L + 1) * (M + 1) ^ (W * (L + 1))) := by910      rw [← pow_step]911      generalize (2 * W + 3) * (M + 1) ^ W = X912      generalize (2 * W + 3) ^ L * (M + 1) ^ (W * L) = Y913      grind914    omega915916theorem sizeBound_closed (W M L : Nat) :917    sizeBound W M 1 L + 1 ≤ 2 * ((2 * W + 3) ^ L * (M + 1) ^ (W * L)) := by918  have := sizeBound_affine W M L 1919  omega920921/-- 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) i938939/-- NETWORK-FAMILY SIMULATION.  Fix W, L, c, k.  Let (net n) be valid networks with940    exactly L layers whose fan-ins and widths are ≤ c (n+1)^k.  Then every output of941    net n is computed by a formula of depth ≤ 3L and size942      ≤ 2 (2W+3)^L (c+1)^(W L) (n+1)^(k W L),943    a polynomial in n whose degree k W L and constant depend only on W, L, c, k. -/944theorem family_ac0 {W L c k : Nat} (net : Nat → List Layer) (hlen : ∀ n, (net n).length = L)945    (hv : ∀ n, NetValid W (net n)) (hb : ∀ n, NetBounded (c * (n + 1) ^ k) (net n)) (n i : Nat) :946    (∀ x : Nat → Bool, eval x (compileNet W (net n) input i) = evalNet (net n) x i) ∧947    depth (compileNet W (net n) input i) ≤ 3 * L ∧948    size (compileNet W (net n) input i) ≤949      2 * ((2 * W + 3) ^ L * ((c + 1) ^ (W * L) * (n + 1) ^ (k * (W * L)))) := by950  obtain ⟨h1, h2, h3, _⟩ := network_ac0 (n := 0) (net n) (hv n) (hb n) i951  rw [hlen] at h2 h3952  refine ⟨h1, h2, Nat.le_trans h3 ?_⟩953  apply Nat.mul_le_mul_left954  apply Nat.mul_le_mul_left955  have hM : c * (n + 1) ^ k + 1 ≤ (c + 1) * (n + 1) ^ k := by956    have : 1 ≤ (n + 1) ^ k := Nat.pow_pos (by omega)957    generalize (n + 1) ^ k = p at *958    have e : (c + 1) * p = c * p + p := by rw [Nat.add_mul, Nat.one_mul]959    rw [e]; omega960  calc (c * (n + 1) ^ k + 1) ^ (W * L) ≤ ((c + 1) * (n + 1) ^ k) ^ (W * L) :=961        Nat.pow_le_pow_left hM _962    _ = (c + 1) ^ (W * L) * (n + 1) ^ (k * (W * L)) := by963        rw [Nat.mul_pow, ← Nat.pow_mul, Nat.mul_comm k]964965/-! ## Recurrent unrolling with a fixed number of updates -/966967/-- A recurrent cell: a network reading input bits x_0..x_{n-1} at indices < n and968    state bits h_0.. at indices n + j, producing the new state at indices j. -/969def cellInput (n : Nat) (x : Nat → Bool) (h : Nat → Bool) : Nat → Bool :=970  fun j => if j < n then x j else h (j - n)971972/-- State after t updates from the input-independent initial state h0; the input of973    update t is the global input block x (t*n + j). -/974def rnnState (cell : List Layer) (n : Nat) (h0 : Nat → Bool) (x : Nat → Bool) : Nat → Nat → Bool975  | 0 => h0976  | t + 1 => evalNet cell (cellInput n (fun j => x (t * n + j)) (rnnState cell n h0 x t))977978def rnnCirc (W : Nat) (cell : List Layer) (n : Nat) (h0 : Nat → Bool) : Nat → Nat → Circ979  | 0 => fun i => const (h0 i)980  | t + 1 => compileNet W cell981      (fun j => if j < n then input (t * n + j) else rnnCirc W cell n h0 t (j - n))982983theorem eval_rnnCirc {W : Nat} (cell : List Layer) (hv : NetValid W cell) (n : Nat)984    (h0 x : Nat → Bool) : ∀ t i, eval x (rnnCirc W cell n h0 t i) = rnnState cell n h0 x t i985  | 0, i => by simp [rnnCirc, rnnState]986  | t + 1, i => by987    simp only [rnnCirc, rnnState]988    rw [eval_compileNet cell hv]989    congr 1990    funext j991    unfold cellInput992    by_cases hj : j < n993    · simp [hj]994    · simp only [hj, if_false]; exact eval_rnnCirc cell hv n h0 x t (j - n)995996/-- Size bound after t updates. -/997def rnnSize (W M L : Nat) : Nat → Nat998  | 0 => 1999  | t + 1 => sizeBound W M (rnnSize W M L t) L10001001theorem rnnSize_pos (W M L t : Nat) : 1 ≤ rnnSize W M L t := by1002  induction t with1003  | zero => simp [rnnSize]1004  | succ t ih => simp only [rnnSize]; exact sizeBound_pos W M L ih10051006/-- BOUNDED-UNROLLING RECURRENCE (paper Definition RNN-formal with total unrolling T):1007    the state after T updates of a valid L-layer cell with fan-ins/widths ≤ M is1008    computed by formulas of depth ≤ 3 L T and size ≤ rnnSize W M L T, reading only1009    the inputs of the T blocks (indices < T n). -/1010theorem rnn_ac0 {W M : Nat} (cell : List Layer) (hv : NetValid W cell) (hb : NetBounded M cell)1011    (n : Nat) (h0 : Nat → Bool) : ∀ T i,1012    (∀ x : Nat → Bool, eval x (rnnCirc W cell n h0 T i) = rnnState cell n h0 x T i) ∧1013    size (rnnCirc W cell n h0 T i) ≤ rnnSize W M cell.length T ∧1014    depth (rnnCirc W cell n h0 T i) ≤ 3 * cell.length * T ∧1015    maxInput (rnnCirc W cell n h0 T i) ≤ T * n1016  | 0, i => ⟨fun x => eval_rnnCirc cell hv n h0 x 0 i, by simp [rnnCirc, rnnSize],1017      by simp [rnnCirc], by simp [rnnCirc]⟩1018  | T + 1, i => by1019    have ih := fun j => rnn_ac0 cell hv hb n h0 T j1020    have hp_size : ∀ j, size ((fun j => if j < n then input (T * n + j)1021        else rnnCirc W cell n h0 T (j - n)) j) ≤ rnnSize W M cell.length T := by1022      intro j; simp only; split1023      · simp; exact rnnSize_pos W M cell.length T1024      · exact (ih (j - n)).2.11025    have hp_depth : ∀ j, depth ((fun j => if j < n then input (T * n + j)1026        else rnnCirc W cell n h0 T (j - n)) j) ≤ 3 * cell.length * T := by1027      intro j; simp only; split1028      · simp1029      · exact (ih (j - n)).2.2.11030    have hp_max : ∀ j, maxInput ((fun j => if j < n then input (T * n + j)1031        else rnnCirc W cell n h0 T (j - n)) j) ≤ (T + 1) * n := by1032      intro j; simp only; split1033      · simp; rw [Nat.succ_mul]; omega1034      · have := (ih (j - n)).2.2.2; rw [Nat.succ_mul]; omega1035    have hb' := compileNet_sd (W := W) cell hb _ _ _ hp_size hp_depth i1036    have hm' := compileNet_max (W := W) cell _ _ hp_max i1037    refine ⟨fun x => eval_rnnCirc cell hv n h0 x (T + 1) i, ?_, ?_, ?_⟩1038    · simp only [rnnCirc, rnnSize]; exact hb'.11039    · simp only [rnnCirc]; have := hb'.2; rw [Nat.mul_succ]; omega1040    · simp only [rnnCirc]; exact hm'10411042/-- rnnSize is polynomial in M for fixed W, L, T:1043    rnnSize W M L T + 1 ≤ (2 (2W+3)^L (M+1)^(W L))^T · 2. -/1044theorem sizeBound_mono_S (W M L : Nat) {S S' : Nat} (h : S ≤ S') :1045    sizeBound W M S L ≤ sizeBound W M S' L := by1046  induction L with1047  | zero => simpa [sizeBound]1048  | succ L ih => simp only [sizeBound]; exact Nat.mul_le_mul_left _ (by omega)10491050theorem rnnSize_closed (W M L T : Nat) :1051    rnnSize W M L T + 1 ≤ 2 * ((2 * W + 3) ^ L * (M + 1) ^ (W * L)) ^ T := by1052  induction T with1053  | zero => simp [rnnSize]1054  | succ T ih =>1055    simp only [rnnSize]1056    have h1 := sizeBound_affine W M L (rnnSize W M L T)1057    generalize (2 * W + 3) ^ L * (M + 1) ^ (W * L) = X at *1058    have h2 := Nat.mul_le_mul_right X ih1059    rw [Nat.pow_succ]1060    have e : 2 * X ^ T * X = 2 * (X ^ T * X) := Nat.mul_assoc _ _ _1061    omega10621063#print axioms Circ.eval_input1064#print axioms Circ.eval_const1065#print axioms Circ.eval_not1066#print axioms Circ.eval_and1067#print axioms Circ.eval_or1068#print axioms Circ.size_input1069#print axioms Circ.size_const1070#print axioms Circ.size_not1071#print axioms Circ.size_and1072#print axioms Circ.size_or1073#print axioms Circ.depth_input1074#print axioms Circ.depth_const1075#print axioms Circ.depth_not1076#print axioms Circ.depth_and1077#print axioms Circ.depth_or1078#print axioms Circ.maxInput_input1079#print axioms Circ.maxInput_const1080#print axioms Circ.maxInput_not1081#print axioms Circ.maxInput_and1082#print axioms Circ.maxInput_or1083#print axioms Circ.subst_input1084#print axioms Circ.subst_const1085#print axioms Circ.subst_not1086#print axioms Circ.subst_and1087#print axioms Circ.subst_or1088#print axioms Circ.le_listMax1089#print axioms Circ.listMax_le1090#print axioms Circ.all_congr_mem1091#print axioms Circ.any_congr_mem1092#print axioms Circ.sum_map_le_mem1093#print axioms Circ.sum_map_mul_right1094#print axioms Circ.eval_subst1095#print axioms Circ.size_subst_le1096#print axioms Circ.depth_subst_le1097#print axioms Circ.size_leaf1098#print axioms Circ.depth_leaf1099#print axioms Circ.size_subst_leaf1100#print axioms Circ.depth_subst_leaf1101#print axioms Circ.maxInput_subst_le1102#print axioms Circ.eval_congr_below1103#print axioms rsum_natCast1104#print axioms gate_rat_iff1105#print axioms nsum_succ1106#print axioms nsum_zero1107#print axioms nsum_le1108#print axioms nsum_congr1109#print axioms nsum_mono1110#print axioms nsum_cut1111#print axioms length_filter_eq_nsum1112#print axioms Gate.psum_succ1113#print axioms Gate.psum_mono1114#print axioms Gate.active_length_le1115#print axioms Gate.exists_cut1116#print axioms Gate.bounded_witness1117#print axioms eval_litC1118#print axioms mem_boards_of1119#print axioms length_boards1120#print axioms eval_termC1121#print axioms eval_dnf1122#print axioms size_termC1123#print axioms depth_termC1124#print axioms maxInput_termC1125#print axioms size_dnf1126#print axioms depth_dnf1127#print axioms maxInput_dnf1128#print axioms gate_ac01129#print axioms eval_compileLayer1130#print axioms eval_compileNet1131#print axioms compileLayer_size1132#print axioms compileLayer_depth1133#print axioms compileLayer_maxInput1134#print axioms sizeBound_succ'1135#print axioms compileNet_sd1136#print axioms compileNet_max1137#print axioms gfac_le1138#print axioms pow_step1139#print axioms sizeBound_pos1140#print axioms sizeBound_affine1141#print axioms sizeBound_closed1142#print axioms network_ac01143#print axioms family_ac01144#print axioms eval_rnnCirc1145#print axioms rnnSize_pos1146#print axioms rnn_ac01147#print axioms sizeBound_mono_S1148#print axioms rnnSize_closed11491150end AC01151end NimAudit