Appendix C, “Realisation with fixed-scale threshold gates”Compiler from formulas to {0,1}-weight threshold networks: ≤2d+2 layers, ≤(2d+1)S+K gates, widths ≤ S+n

698/-- THE COMPILER THEOREM (all properties of the one network `compileF cs`). -/699theorem compileF_spec (cs : List Circ) (n D : Nat) (hn : ∀ c ∈ cs, maxInput c ≤ n)700    (hD : ∀ c ∈ cs, depth c ≤ D) :701    (∀ x : Nat → Bool, ∀ k (hk : k < cs.length), evalNet (compileF cs) x k = eval x cs[k]) ∧702    (∀ x : Nat → Bool, ∀ k, cs.length ≤ k → evalNet (compileF cs) x k = false) ∧703    NetValid 1 (compileF cs) ∧ Wired n (compileF cs) ∧704    (compileF cs).length ≤ 2 * D + 2 ∧705    NetBounded ((cs.map size).sum + n) (compileF cs) ∧706    gateCount (compileF cs) ≤ (2 * D + 1) * (cs.map size).sum + cs.length := by707  have hd : dmax cs ≤ D := listMax_le (fun a ha => by obtain ⟨c, hc, rfl⟩ := List.mem_map.mp ha; exact hD c hc)708  refine ⟨fun x k hk => compileF_eval cs x hk, fun x k hk => compileF_eval_out cs x hk, compileF_valid cs,709    compileF_wired cs n hn, by rw [compileF_length]; omega, compileF_bounded cs n hn, ?_⟩710  rw [compileF_gates]711  have : (2 * dmax cs + 1) * (cs.map size).sum ≤ (2 * D + 1) * (cs.map size).sum :=712    Nat.mul_le_mul_right _ (by omega)713  omega

715/-- FIXED GRID: every gate of a compiled network fires in the paper's rational form with716    denominator D = 1 exactly when it fires in integer form (weights in {0,1}, threshold717    in {0,1}). -/718theorem compileF_fixed_grid (cs : List Circ) :719    ∀ l ∈ compileF cs, ∀ g ∈ l, Gate.Valid 1 g ∧ ∀ z, (ratFires g 1 z ↔ g.eval z = true) :=720  fun l hl g hg => ⟨compileF_valid cs l hl g hg, fun z => gate_rat_iff g (by decide) z⟩

639/-- BOUNDED WIDTH AND FAN-IN: every layer has ≤ S + n gates, every gate fan-in ≤ S + n,640    where S = Σ size(c_k) is the program size. -/641theorem compileF_bounded (cs : List Circ) (n : Nat) (hn : ∀ c ∈ cs, maxInput c ≤ n) :642    NetBounded ((cs.map size).sum + n) (compileF cs) := by643  have hmx : listMax (cs.map maxInput) ≤ n := listMax_le (fun a ha => by644    obtain ⟨c, hc, rfl⟩ := List.mem_map.mp ha; exact hn c hc)645  have hS := prog_length cs646  intro l hl647  simp only [compileF, List.mem_append, List.mem_map, List.mem_range, List.mem_singleton] at hl648  rcases hl with ⟨t, _, rfl⟩ | rfl649  · refine ⟨by simp only [layerAt]; split <;> simp [hS], ?_⟩650    intro g hg651    simp only [layerAt] at hg652    split at hg653    · simp only [List.mem_map, List.mem_range] at hg654      obtain ⟨g', hg', rfl⟩ := hg655      have hmem : (progOf cs).getD g' (.cst false) ∈ progOf cs := by656        rw [getD_eq_getElem' hg']; exact List.getElem_mem hg'657      have hr := emitL_reads 0 cs _ hmem658      generalize (progOf cs).getD g' (.cst false) = d at hr659      cases d with660      | inp i => simp only [gate1, orGate_fanin]; simp [gmax] at hr; omega661      | cst b => simp [gate1, constGate_fanin]662      | neg a => simp only [gate1]; split <;> simp [constGate_fanin]663      | disj as => simp [gate1, constGate_fanin]664      | conj as => simp only [gate1]; split <;> (try split) <;> simp [constGate_fanin]665    · simp only [List.mem_map, List.mem_range] at hg666      obtain ⟨g', _, rfl⟩ := hg667      generalize (progOf cs).getD g' (.cst false) = d668      unfold gateT669      split670      · rw [orGate_fanin]; omega671      · split672        · cases d <;> simp only <;> (try split) <;>673            first | (rw [orGate_fanin]; omega) | (rw [constGate_fanin]; omega)674        · split675          · cases d <;> simp only <;> (try split) <;>676              first | (rw [orGate_fanin]; omega) | (rw [constGate_fanin]; omega)677          · rw [constGate_fanin]; omega678  · refine ⟨by simp [outs_length]; have := cs_le_prog cs; omega, ?_⟩679    intro g hg680    simp only [List.mem_map] at hg681    obtain ⟨o, _, rfl⟩ := hg682    rw [orGate_fanin]; omega