ThresholdNet

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 SharedCircuit2import FiniteNet34/- Phase 5, task 2: compiling bounded-depth Boolean formulas into the paper's5   fixed-scale literal-threshold networks (the existing AC0.Gate / Layer / evalNet6   model), in the direction opposite to Circuit.compileNet.  Written by Claude7   (10 October 2026).  Lean 4.26.0, core/Std only.89   Gates used (W = 1, i.e. the fixed grid with denominator D = 1):10     * OR of literals: coefficients in {0,1}, one negation flag, threshold 1;11     * constants: no inputs, threshold 0 (true) or 1 (false).12   AND is never realised by a threshold equal to its fan-in: an AND node takes two13   layers, OR of negated children (= NOT AND) followed by OR of the negated result14   (De Morgan).  NOT costs one layer (an OR of one negated literal).1516   Construction.  The formulas are first laid out as one shared gate program17   (SharedCircuit.emitL, one gate per formula node).  Every layer has one wire per18   program gate (width S); gate g is computed at layer lvl(g) (inputs and constants19   at layer 1, NOT and OR one layer above their children, AND two layers above),20   and identity buffers carry each value to all later layers.  A final layer copies21   the K output gates to wires 0, …, K−1.  Layer 1 reads the n input wires only22   through single-literal buffers of input i (fan-in i + 1 ≤ n).23   Proved for the one compiled network `compileF n cs`: exact outputs on every input,24   NetValid 1, Wired n, exactly 2D + 2 layers for depth bound D, width and fan-in25   ≤ S + n, and gate count (2D+1)·S + K, where S = Σ size(c_k). -/2627namespace NimAudit28namespace ThresholdNet2930open AC0 AC0.Circ Shared FiniteNet3132/-! ## The two gate shapes -/3334/-- OR of the literals (z j XOR ng) over the wires j < K with sel j. -/35def orGate (K : Nat) (sel : Nat → Bool) (ng : Bool) : Gate :=36  ⟨(List.range K).map (fun j => if sel j then 1 else 0), (List.range K).map (fun _ => ng), 1⟩3738/-- Constant gate (no inputs). -/39def constGate (b : Bool) : Gate := ⟨[], [], if b then 0 else 1⟩4041theorem sum_range_pos (f : Nat → Nat) : ∀ K, 1 ≤ ((List.range K).map f).sum ↔ ∃ j < K, 1 ≤ f j42  | 0 => by simp43  | K + 1 => by44    have ih := sum_range_pos f K45    rw [List.range_succ, List.map_append, List.sum_append_nat]46    simp only [List.map_cons, List.map_nil, List.sum_cons, List.sum_nil, Nat.add_zero]47    constructor48    · intro h49      by_cases h1 : 1 ≤ f K50      · exact ⟨K, by omega, h1⟩51      · obtain ⟨j, hj, hf⟩ := ih.1 (by omega)52        exact ⟨j, by omega, hf⟩53    · rintro ⟨j, hj, hf⟩54      by_cases hjK : j = K55      · subst hjK; omega56      · have := ih.2 ⟨j, by omega, hf⟩; omega5758theorem orGate_eval (K : Nat) (sel : Nat → Bool) (ng : Bool) (z : Nat → Bool) :59    (orGate K sel ng).eval z = decide (∃ j < K, sel j = true ∧ xor (z j) ng = true) := by60  unfold Gate.eval Gate.wsum Gate.psum Gate.fanin orGate61  simp only [List.length_map, List.length_range]62  apply Bool.eq_iff_iff.mpr63  simp only [decide_eq_true_iff]64  have e : ∀ j ∈ List.range K, (Gate.coeff ⟨(List.range K).map (fun j => if sel j then 1 else 0),65      (List.range K).map (fun _ => ng), 1⟩ j) * (if Gate.lit ⟨(List.range K).map (fun j => if sel j then 1 else 0),66      (List.range K).map (fun _ => ng), 1⟩ z j then 1 else 0) =67      (if sel j = true ∧ xor (z j) ng = true then 1 else 0) := by68    intro j hj69    have hj' := List.mem_range.mp hj70    simp only [Gate.coeff, Gate.lit, List.getD_eq_getElem?_getD, List.getElem?_map, List.getElem?_range hj',71      Option.map_some, Option.getD_some]72    cases sel j <;> cases xor (z j) ng <;> simp73  rw [List.map_congr_left e, sum_range_pos]74  constructor75  · rintro ⟨j, hj, h⟩; refine ⟨j, hj, ?_⟩; split at h <;> simp_all76  · rintro ⟨j, hj, h⟩; exact ⟨j, hj, by simp [h]⟩7778theorem constGate_eval (b : Bool) (z : Nat → Bool) : (constGate b).eval z = b := by79  cases b <;> simp [constGate, Gate.eval, Gate.wsum, Gate.psum, Gate.fanin]8081theorem orGate_valid (K : Nat) (sel : Nat → Bool) (ng : Bool) : Gate.Valid 1 (orGate K sel ng) := by82  refine ⟨by simp [orGate], ?_⟩83  intro a ha84  simp only [orGate, List.mem_map, List.mem_range] at ha85  obtain ⟨j, _, rfl⟩ := ha86  split <;> omega8788theorem constGate_valid (b : Bool) : Gate.Valid 1 (constGate b) := by89  refine ⟨by cases b <;> simp [constGate], by simp [constGate]⟩9091theorem orGate_fanin (K : Nat) (sel : Nat → Bool) (ng : Bool) : (orGate K sel ng).fanin = K := by92  simp [orGate, Gate.fanin]9394theorem constGate_fanin (b : Bool) : (constGate b).fanin = 0 := rfl9596/-! ## Levels of program gates -/9798/-- Layer at which a program gate is available: 1 for inputs/constants, +1 for NOT99    and OR, +2 for AND (De Morgan). -/100def lvlAlg : Alg Nat := ⟨0, fun _ => 1, fun _ => 1, (· + 1), fun l => listMax l + 2, fun l => listMax l + 1⟩101102mutual103def lvl : Circ → Nat104  | .input _ => 1105  | .const _ => 1106  | .not c => lvl c + 1107  | .and cs => lvlL cs + 2108  | .or cs => lvlL cs + 1109def lvlL : List Circ → Nat110  | [] => 0111  | c :: cs => max (lvl c) (lvlL cs)112end113114theorem lvlL_eq : ∀ cs : List Circ, lvlL cs = listMax (cs.map lvl)115  | [] => rfl116  | c :: cs => by simp only [lvlL, List.map_cons, listMax, List.foldr_cons]; rw [lvlL_eq cs]; rfl117118theorem lvl_fhom : FHom lvlAlg lvl :=119  ⟨fun _ => rfl, fun _ => rfl, fun _ => rfl, fun cs => by simp [lvl, lvlAlg, lvlL_eq],120   fun cs => by simp [lvl, lvlAlg, lvlL_eq]⟩121122mutual123theorem lvl_le : ∀ c : Circ, lvl c ≤ 2 * depth c + 1124  | .input _ => by simp [lvl]125  | .const _ => by simp [lvl]126  | .not c => by have := lvl_le c; simp [lvl]; omega127  | .and cs => by have := lvlL_le cs; simp only [lvl, depth_and]; omega128  | .or cs => by have := lvlL_le cs; simp only [lvl, depth_or]; omega129theorem lvlL_le : ∀ cs : List Circ, lvlL cs ≤ 2 * listMax (cs.map depth) + 1130  | [] => by simp [lvlL]131  | c :: cs => by132    have h1 := lvl_le c133    have h2 := lvlL_le cs134    simp only [lvlL, List.map_cons, listMax, List.foldr_cons] at h2 ⊢135    omega136end137138/-! ## Generic facts on sequential evaluation -/139140section RunFacts141variable {α : Type}142143theorem run_take (A : Alg α) (C : List DGate) (g : Nat) (hg : g ≤ C.length) :144    (run A [] C).take g = run A [] (C.take g) := by145  have e : C = C.take g ++ C.drop g := (List.take_append_drop g C).symm146  conv => lhs; rw [e]147  rw [run_append]148  obtain ⟨W, hW, _⟩ := run_prefix A (run A [] (C.take g)) (C.drop g)149  rw [hW]150  have hl : (run A [] (C.take g)).length = g := by rw [run_length]; simp; omega151  rw [List.take_append_of_le_length (by omega), List.take_of_length_le (by omega)]152153theorem run_getD (A : Alg α) (C : List DGate) (g : Nat) (hg : g < C.length) :154    (run A [] C).getD g A.dflt = gstep A ((run A [] C).take g) C[g] := by155  have e : C = C.take (g + 1) ++ C.drop (g + 1) := (List.take_append_drop (g + 1) C).symm156  have et : C.take (g + 1) = C.take g ++ [C[g]] := by157    rw [List.take_add_one, List.getElem?_eq_getElem hg]; rfl158  have hlen : (run A [] (C.take g)).length = g := by rw [run_length]; simp; omega159  have h1 : (run A [] C).getD g A.dflt = (run A [] (C.take (g + 1))).getD g A.dflt := by160    conv => lhs; rw [e]161    rw [run_append]162    obtain ⟨W, hW, _⟩ := run_prefix A (run A [] (C.take (g + 1))) (C.drop (g + 1))163    rw [hW]164    have hl2 : (run A [] (C.take (g + 1))).length = g + 1 := by rw [run_length]; simp; omega165    exact rd_append_left A _ W (by omega)166  rw [h1, et, run_append]167  simp only [run]168  rw [run_take A C g (by omega)]169  have := rd_snoc A (run A [] (C.take g)) (gstep A (run A [] (C.take g)) C[g])170  rw [hlen] at this171  exact this172173theorem rd_take (A : Alg α) (l : List α) (g a : Nat) (hg : g ≤ l.length) :174    rd A (l.take g) a = if a < g then rd A l a else A.dflt := by175  unfold rd176  simp only [List.getD_eq_getElem?_getD, List.getElem?_take]177  by_cases h : a < g <;> simp [h]178179end RunFacts180181/-! ## The layered network for a gate program -/182183section Prog184variable (prog : List DGate)185186/-- Value of program gate g on input x (false out of range). -/187def vl (x : Nat → Bool) (g : Nat) : Bool := (run (valAlg x) [] prog).getD g false188189/-- Level of program gate g. -/190def lv (g : Nat) : Nat := (run lvlAlg [] prog).getD g 0191192/-- Layer-1 gate for program gate g (reads only input wires). -/193def gate1 (g : Nat) : DGate → Gate194  | .inp i => orGate (i + 1) (fun j => j == i) false195  | .cst b => constGate b196  | .neg a => if a < g then constGate false else constGate true197  | .disj _ => constGate false198  | .conj as => if as.any (fun a => decide (a < g)) then constGate false199      else if as.isEmpty then constGate false else constGate true200201/-- Gate for program gate g at layer t ≥ 2 (reads the S wires of layer t − 1). -/202def gateT (t g : Nat) (d : DGate) : Gate :=203  if lv prog g < t then orGate prog.length (fun j => j == g) false204  else if lv prog g = t then205    match d with206    | .inp _ => constGate false207    | .cst b => constGate b208    | .neg a => if a < g then orGate prog.length (fun j => j == a) true else constGate true209    | .disj as => orGate prog.length (fun j => decide (j ∈ as ∧ j < g)) false210    | .conj _ => orGate prog.length (fun j => j == g) true211  else if lv prog g = t + 1 then212    match d with213    | .conj as => if as.any (fun a => !decide (a < g)) then constGate true214        else orGate prog.length (fun j => decide (j ∈ as)) true215    | _ => constGate false216  else constGate false217218def layerAt (t : Nat) : Layer :=219  if t ≤ 1 then (List.range prog.length).map (fun g => gate1 g (prog.getD g (.cst false)))220  else (List.range prog.length).map (fun g => gateT prog t g (prog.getD g (.cst false)))221222/-- Wire values after t layers. -/223def ys (x : Nat → Bool) : Nat → (Nat → Bool)224  | 0 => x225  | t + 1 => evalLayer (layerAt prog (t + 1)) (ys x t)226227end Prog228229section ProgFacts230variable {prog : List DGate}231232theorem lvlAlg_pos : ∀ v ∈ run lvlAlg [] prog, 1 ≤ v :=233  run_inv lvlAlg (fun v => 1 ≤ v) (fun _ => True)234    (fun acc g _ _ => by cases g <;> simp [gstep, lvlAlg]) prog [] (fun _ _ => trivial) (by simp)235236theorem lv_pos {g : Nat} (hg : g < prog.length) : 1 ≤ lv prog g := by237  unfold lv238  have hl : g < (run lvlAlg [] prog).length := by rw [run_length]; simp; omega239  rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hl]240  exact lvlAlg_pos _ (List.getElem_mem hl)241242theorem getD_eq_getElem' (hg : g < prog.length) : prog.getD g (.cst false) = prog[g] := by243  rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hg]; rfl244245/-- Local value equation. -/246theorem vl_eq (x : Nat → Bool) {g : Nat} (hg : g < prog.length) :247    vl prog x g = gstep (valAlg x) ((run (valAlg x) [] prog).take g) prog[g] :=248  run_getD (valAlg x) prog g hg249250theorem lv_eq {g : Nat} (hg : g < prog.length) :251    lv prog g = gstep lvlAlg ((run lvlAlg [] prog).take g) prog[g] :=252  run_getD lvlAlg prog g hg253254theorem rdv_take (x : Nat → Bool) {g a : Nat} (hg : g < prog.length) :255    rd (valAlg x) ((run (valAlg x) [] prog).take g) a = if a < g then vl prog x a else false := by256  rw [rd_take _ _ _ _ (by rw [run_length]; simp; omega)]; rfl257258theorem rdl_take {g a : Nat} (hg : g < prog.length) :259    rd lvlAlg ((run lvlAlg [] prog).take g) a = if a < g then lv prog a else 0 := by260  rw [rd_take _ _ _ _ (by rw [run_length]; simp; omega)]; rfl261262theorem evalLayer_at {l : Layer} {z : Nat → Bool} {g : Nat} (f : Nat → Gate) (K : Nat) (hl : l = (List.range K).map f)263    (hg : g < K) : evalLayer l z g = (f g).eval z := by264  subst hl; simp [evalLayer, List.getElem?_range hg]265266theorem listMax_ge {l : List Nat} {a : Nat} (h : a ∈ l) : a ≤ listMax l := le_listMax h267268theorem vl_inp (x : Nat → Bool) {g i : Nat} (hg : g < prog.length) (hd : prog[g] = .inp i) :269    vl prog x g = x i := by rw [vl_eq x hg, hd]; rfl270271theorem vl_cst (x : Nat → Bool) {g : Nat} {b : Bool} (hg : g < prog.length) (hd : prog[g] = .cst b) :272    vl prog x g = b := by rw [vl_eq x hg, hd]; rfl273274theorem vl_neg (x : Nat → Bool) {g a : Nat} (hg : g < prog.length) (hd : prog[g] = .neg a) :275    vl prog x g = !(if a < g then vl prog x a else false) := by276  rw [vl_eq x hg, hd]; simp only [gstep]; rw [rdv_take x hg]; rfl277278theorem vl_disj (x : Nat → Bool) {g : Nat} {as : List Nat} (hg : g < prog.length) (hd : prog[g] = .disj as) :279    vl prog x g = as.any (fun a => if a < g then vl prog x a else false) := by280  rw [vl_eq x hg, hd]; simp only [gstep]281  rw [List.map_congr_left (fun a _ => rdv_take (a := a) x hg)]282  simp [valAlg, List.any_map, Function.comp_def]283284theorem vl_conj (x : Nat → Bool) {g : Nat} {as : List Nat} (hg : g < prog.length) (hd : prog[g] = .conj as) :285    vl prog x g = as.all (fun a => if a < g then vl prog x a else false) := by286  rw [vl_eq x hg, hd]; simp only [gstep]287  rw [List.map_congr_left (fun a _ => rdv_take (a := a) x hg)]288  simp [valAlg, List.all_map, Function.comp_def]289290theorem lv_inp {g i : Nat} (hg : g < prog.length) (hd : prog[g] = .inp i) : lv prog g = 1 := by291  rw [lv_eq hg, hd]; rfl292293theorem lv_cst {g : Nat} {b : Bool} (hg : g < prog.length) (hd : prog[g] = .cst b) : lv prog g = 1 := by294  rw [lv_eq hg, hd]; rfl295296theorem lv_neg {g a : Nat} (hg : g < prog.length) (hd : prog[g] = .neg a) :297    lv prog g = (if a < g then lv prog a else 0) + 1 := by298  rw [lv_eq hg, hd]; simp only [gstep]; rw [rdl_take hg]; rfl299300theorem lv_disj {g : Nat} {as : List Nat} (hg : g < prog.length) (hd : prog[g] = .disj as) :301    lv prog g = listMax (as.map (fun a => if a < g then lv prog a else 0)) + 1 := by302  rw [lv_eq hg, hd]; simp only [gstep]303  rw [List.map_congr_left (fun a _ => rdl_take (a := a) hg)]; rfl304305theorem lv_conj {g : Nat} {as : List Nat} (hg : g < prog.length) (hd : prog[g] = .conj as) :306    lv prog g = listMax (as.map (fun a => if a < g then lv prog a else 0)) + 2 := by307  rw [lv_eq hg, hd]; simp only [gstep]308  rw [List.map_congr_left (fun a _ => rdl_take (a := a) hg)]; rfl309310theorem child_lv {g a : Nat} {as : List Nat} (ha : a ∈ as) (hag : a < g) :311    lv prog a ≤ listMax (as.map (fun a => if a < g then lv prog a else 0)) := by312  apply le_listMax; rw [List.mem_map]; exact ⟨a, ha, by rw [if_pos hag]⟩313314theorem decide_or1 {K i : Nat} (hi : i < K) (z : Nat → Bool) (ng : Bool) :315    decide (∃ j < K, (j == i) = true ∧ xor (z j) ng = true) = xor (z i) ng := by316  apply Bool.eq_iff_iff.mpr317  simp only [decide_eq_true_iff]318  constructor319  · rintro ⟨j, _, hj, h⟩; simp at hj; subst hj; exact h320  · intro h; exact ⟨i, hi, by simp, h⟩321322/-- THE LAYER INVARIANT: after t ≥ 1 layers, wire g carries the value of program gate g323    as soon as t ≥ lvl(g); an AND gate carries its complement one layer earlier. -/324theorem ys_spec (x : Nat → Bool) : ∀ t, 1 ≤ t → ∀ g (hg : g < prog.length),325    (lv prog g ≤ t → ys prog x t g = vl prog x g) ∧326    (∀ as, prog[g] = .conj as → lv prog g = t + 1 → ys prog x t g = !vl prog x g)327  | 0, h, _, _ => absurd h (by omega)328  | 1, _, g, hg => by329    have hy : ys prog x 1 g = (gate1 g prog[g]).eval x := by330      simp only [ys]331      rw [evalLayer_at (fun g => gate1 g (prog.getD g (.cst false))) prog.length332        (by simp [layerAt]) hg, getD_eq_getElem' hg]333    rw [hy]334    cases hd : prog[g] with335    | inp i =>336      refine ⟨fun _ => ?_, fun as h => by cases h⟩337      rw [vl_inp x hg hd]; simp only [gate1, orGate_eval]338      rw [decide_or1 (by omega : i < i + 1)]; simp339    | cst b =>340      refine ⟨fun _ => ?_, fun as h => by cases h⟩341      rw [vl_cst x hg hd]; simp [gate1, constGate_eval]342    | neg a =>343      refine ⟨fun hle => ?_, fun as h => by cases h⟩344      have hl := lv_neg hg hd345      by_cases ha : a < g346      · exfalso; rw [if_pos ha] at hl347        have := lv_pos (prog := prog) (show a < prog.length by omega); omega348      · rw [vl_neg x hg hd]; simp [gate1, ha, constGate_eval]349    | disj as =>350      refine ⟨fun hle => ?_, fun as' h => by cases h⟩351      have hl := lv_disj hg hd352      rw [vl_disj x hg hd]353      simp only [gate1, constGate_eval]354      symm355      apply List.any_eq_false.mpr356      intro a ha357      by_cases hag : a < g358      · exfalso359        have h1 := child_lv (prog := prog) ha hag360        have := lv_pos (prog := prog) (show a < prog.length by omega); omega361      · simp [hag]362    | conj as =>363      have hl := lv_conj hg hd364      refine ⟨fun hle => by omega, fun as' h hlv => ?_⟩365      cases h366      have hnone : ∀ a ∈ as, ¬ a < g := by367        intro a ha hag368        have h1 := child_lv (prog := prog) ha hag369        have := lv_pos (prog := prog) (show a < prog.length by omega); omega370      have hany : as.any (fun a => decide (a < g)) = false := by371        apply List.any_eq_false.mpr; intro a ha; simpa using hnone a ha372      rw [vl_conj x hg hd]373      simp only [gate1, hany, Bool.false_eq_true, if_false]374      cases as with375      | nil => simp [constGate_eval]376      | cons a as =>377        simp only [List.isEmpty_cons, Bool.false_eq_true, if_false, constGate_eval]378        have : (a :: as).all (fun a => if a < g then vl prog x a else false) = false := by379          apply List.all_eq_false.mpr380          exact ⟨a, by simp, by simp [hnone a (by simp)]⟩381        rw [this]; rfl382  | t + 2, _, g, hg => by383    have IH := fun g hg => ys_spec x (t + 1) (by omega) g hg384    have hy : ys prog x (t + 2) g = (gateT prog (t + 2) g prog[g]).eval (ys prog x (t + 1)) := by385      simp only [ys]386      rw [evalLayer_at (fun g => gateT prog (t + 2) g (prog.getD g (.cst false))) prog.length387        (by simp [layerAt]) hg, getD_eq_getElem' hg]388    rw [hy]389    constructor390    · intro hle391      by_cases hlt : lv prog g < t + 2392      · -- buffer393        unfold gateT; rw [if_pos hlt, orGate_eval, decide_or1 hg, (IH g hg).1 (by omega)]; simp394      · have heq : lv prog g = t + 2 := by omega395        unfold gateT; rw [if_neg hlt, if_pos heq]396        cases hd : prog[g] with397        | inp i => exfalso; have := lv_inp hg hd; omega398        | cst b => exfalso; have := lv_cst hg hd; omega399        | neg a =>400          have hl := lv_neg hg hd401          by_cases ha : a < g402          · rw [if_pos ha] at hl403            simp only [ha, if_true, orGate_eval]404            rw [vl_neg x hg hd, if_pos ha, decide_or1 (show a < prog.length by omega),405              (IH a (by omega)).1 (by omega)]406            cases vl prog x a <;> rfl407          · exfalso; rw [if_neg ha] at hl; omega408        | disj as =>409          have hl := lv_disj hg hd410          simp only [orGate_eval]411          rw [vl_disj x hg hd]412          have hch : ∀ a ∈ as, a < g → lv prog a ≤ t + 1 := by413            intro a ha hag; have := child_lv (prog := prog) ha hag; omega414          apply Bool.eq_iff_iff.mpr415          simp only [decide_eq_true_iff, List.any_eq_true]416          constructor417          · rintro ⟨j, hj, hsel, h⟩418            try simp only [decide_eq_true_iff] at hsel419            refine ⟨j, hsel.1, ?_⟩420            rw [if_pos hsel.2, ← (IH j hj).1 (hch j hsel.1 hsel.2)]; simpa using h421          · rintro ⟨a, ha, h⟩422            by_cases hag : a < g423            · rw [if_pos hag] at h424              refine ⟨a, by omega, by simp [ha, hag], ?_⟩425              rw [(IH a (by omega)).1 (hch a ha hag)]; simpa using h426            · rw [if_neg hag] at h; cases h427        | conj as =>428          simp only [orGate_eval]429          rw [decide_or1 hg, (IH g hg).2 as hd (by omega)]430          cases vl prog x g <;> rfl431    · intro as hd hlv432      have hl := lv_conj hg hd433      unfold gateT434      rw [if_neg (show ¬ lv prog g < t + 2 by omega), if_neg (show ¬ lv prog g = t + 2 by omega),435        if_pos hlv, hd]436      simp only437      rw [vl_conj x hg hd]438      by_cases hout : as.any (fun a => !decide (a < g)) = true439      · simp only [hout, if_true, constGate_eval]440        obtain ⟨a, ha, hna⟩ := List.any_eq_true.mp hout441        simp only [Bool.not_eq_true', decide_eq_false_iff_not] at hna442        have : as.all (fun a => if a < g then vl prog x a else false) = false := by443          apply List.all_eq_false.mpr444          exact ⟨a, ha, by simp [hna]⟩445        rw [this]; rfl446      · simp only [Bool.not_eq_true] at hout447        simp only [hout, Bool.false_eq_true, if_false, orGate_eval]448        have hin : ∀ a ∈ as, a < g := by449          intro a ha450          have := List.any_eq_false.mp hout a ha451          simpa using this452        have hch : ∀ a ∈ as, lv prog a ≤ t + 1 := by453          intro a ha; have := child_lv (prog := prog) ha (hin a ha); omega454        apply Bool.eq_iff_iff.mpr455        simp only [decide_eq_true_iff, Bool.not_eq_true', List.all_eq_false]456        constructor457        · rintro ⟨j, hj, hsel, h⟩458          try simp only [decide_eq_true_iff] at hsel459          refine ⟨j, hsel, ?_⟩460          rw [if_pos (hin j hsel), ← (IH j hj).1 (hch j hsel)]; simpa using h461        · rintro ⟨a, ha, h⟩462          rw [if_pos (hin a ha)] at h463          refine ⟨a, by have := hin a ha; omega, by simp [ha], ?_⟩464          rw [(IH a (by have := hin a ha; omega)).1 (hch a ha)]; simpa using h465466end ProgFacts467468/-! ## Compiling a list of formulas -/469470/-- The shared program and output gates of a formula list. -/471def progOf (cs : List Circ) : List DGate := (emitL 0 cs).1472def outsOf (cs : List Circ) : List Nat := (emitL 0 cs).2473474/-- Depth bound used for the layer count. -/475def dmax (cs : List Circ) : Nat := listMax (cs.map depth)476477/-- Number of computing layers: 2·D + 1. -/478def nLayers (cs : List Circ) : Nat := 2 * dmax cs + 1479480/-- THE COMPILED NETWORK for formulas cs on n input wires: 2·D + 1 computing layers of481    width S, then one output layer of width K = cs.length. -/482def compileF (cs : List Circ) : List Layer :=483  (List.range (nLayers cs)).map (fun t => layerAt (progOf cs) (t + 1)) ++484    [(outsOf cs).map (fun o => orGate (progOf cs).length (fun j => j == o) false)]485486theorem evalNet_append (ls : List Layer) (l : Layer) (z : Nat → Bool) :487    evalNet (ls ++ [l]) z = evalLayer l (evalNet ls z) := by488  induction ls generalizing z with489  | nil => rfl490  | cons l' ls ih => simp only [List.cons_append, evalNet]; exact ih _491492theorem evalNet_layers (prog : List DGate) (x : Nat → Bool) : ∀ L,493    evalNet ((List.range L).map (fun t => layerAt prog (t + 1))) x = ys prog x L494  | 0 => rfl495  | L + 1 => by rw [List.range_succ, List.map_append, List.map_cons, List.map_nil, evalNet_append,496      evalNet_layers prog x L]; rfl497498theorem outs_range : ∀ (cs : List Circ) (base : Nat),499    ∀ a ∈ (emitL base cs).2, base ≤ a ∧ a < base + (emitL base cs).1.length500  | [], _ => by simp [emitL]501  | c :: cs, base => by502    intro a ha503    have hpos := size_pos' c504    have hlc := emit_len base c505    simp only [emitL, List.mem_cons] at ha506    have hlen : (emitL base (c :: cs)).1.length =507        (emit base c).length + (emitL (base + (emit base c).length) cs).1.length := by simp [emitL]508    rw [hlen]509    rcases ha with rfl | ha510    · omega511    · have := outs_range cs (base + (emit base c).length) a ha; omega512513theorem outs_length (cs : List Circ) : (outsOf cs).length = cs.length := (emitL_len 0 cs).2514515theorem prog_length (cs : List Circ) : (progOf cs).length = (cs.map size).sum := (emitL_len 0 cs).1516517theorem valAlg_fhom (x : Nat → Bool) : FHom (valAlg x) (eval x) :=518  ⟨fun _ => by simp [valAlg], fun _ => by simp [valAlg], fun _ => by simp [valAlg],519   fun _ => by simp [valAlg, List.all_map], fun _ => by simp [valAlg, List.any_map]⟩520521theorem outs_val (cs : List Circ) (x : Nat → Bool) {k : Nat} (hk : k < cs.length) :522    vl (progOf cs) x ((outsOf cs)[k]'(by rw [outs_length]; exact hk)) = eval x cs[k] := by523  have h := emitL_val (valAlg x) (eval x) (valAlg_fhom x) 0 cs [] rfl524  have h2 := congrArg (fun l => l[k]?) h525  simp only [List.getElem?_map] at h2526  rw [List.getElem?_eq_getElem (by rw [(emitL_len 0 cs).2]; exact hk), List.getElem?_eq_getElem hk] at h2527  simp only [Option.map_some, Option.some.injEq] at h2528  exact h2529530theorem outs_lv (cs : List Circ) {k : Nat} (hk : k < cs.length) :531    lv (progOf cs) ((outsOf cs)[k]'(by rw [outs_length]; exact hk)) ≤ nLayers cs := by532  have h := emitL_val lvlAlg lvl lvl_fhom 0 cs [] rfl533  have h2 := congrArg (fun l => l[k]?) h534  simp only [List.getElem?_map] at h2535  rw [List.getElem?_eq_getElem (by rw [(emitL_len 0 cs).2]; exact hk), List.getElem?_eq_getElem hk] at h2536  simp only [Option.map_some, Option.some.injEq] at h2537  unfold lv538  have e : (run lvlAlg [] (progOf cs)).getD ((outsOf cs)[k]'(by rw [outs_length]; exact hk)) 0 =539      lvl cs[k] := h2540  rw [e]541  have h3 := lvl_le cs[k]542  have h4 : depth cs[k] ≤ dmax cs := le_listMax (List.mem_map_of_mem (List.getElem_mem hk))543  unfold nLayers; omega544545/-- OUTPUT CORRECTNESS: output k of the compiled network is formula k, on every input. -/546theorem compileF_eval (cs : List Circ) (x : Nat → Bool) {k : Nat} (hk : k < cs.length) :547    evalNet (compileF cs) x k = eval x cs[k] := by548  unfold compileF549  rw [evalNet_append, evalNet_layers]550  have hk' : k < (outsOf cs).length := by rw [outs_length]; exact hk551  rw [evalLayer_at (fun k => orGate (progOf cs).length (fun j => j == (outsOf cs).getD k 0) false)552    (outsOf cs).length (by553      apply List.ext_getElem (by simp)554      intro n h1 h2; simp [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem (by simpa using h1)]) hk']555  simp only [orGate_eval]556  have ho : (outsOf cs).getD k 0 = (outsOf cs)[k] := by557    rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hk']; rfl558  have hor := outs_range cs 0 (outsOf cs)[k] (List.getElem_mem hk')559  have hS : (outsOf cs)[k] < (progOf cs).length := by simpa [progOf] using hor.2560  have hspec := (ys_spec (prog := progOf cs) x (nLayers cs) (by unfold nLayers; omega) _ hS).1 (outs_lv cs hk)561  rw [ho]562  apply Bool.eq_iff_iff.mpr563  simp only [decide_eq_true_iff]564  constructor565  · rintro ⟨j, _, hj, h⟩; simp at hj; subst hj; rw [hspec, outs_val cs x hk] at h; simpa using h566  · intro h; exact ⟨_, hS, by simp, by rw [hspec, outs_val cs x hk]; simpa using h⟩567568/-- Outputs beyond K are false. -/569theorem compileF_eval_out (cs : List Circ) (x : Nat → Bool) {k : Nat} (hk : cs.length ≤ k) :570    evalNet (compileF cs) x k = false := by571  unfold compileF572  rw [evalNet_append]573  simp [evalLayer, List.getElem?_eq_none (show (outsOf cs).length ≤ k by rw [outs_length]; exact hk)]574575/-! ## Resources of the compiled network -/576577theorem compileF_valid (cs : List Circ) : NetValid 1 (compileF cs) := by578  intro l hl g hg579  simp only [compileF, List.mem_append, List.mem_map, List.mem_range, List.mem_singleton] at hl580  rcases hl with ⟨t, _, rfl⟩ | rfl581  · simp only [layerAt] at hg582    split at hg583    · simp only [List.mem_map, List.mem_range] at hg584      obtain ⟨g', _, rfl⟩ := hg585      generalize (progOf cs).getD g' (.cst false) = d586      cases d <;> simp only [gate1] <;> (try split) <;> (try split) <;>587        first | exact orGate_valid _ _ _ | exact constGate_valid _588    · simp only [List.mem_map, List.mem_range] at hg589      obtain ⟨g', _, rfl⟩ := hg590      generalize (progOf cs).getD g' (.cst false) = d591      unfold gateT592      split593      · exact orGate_valid _ _ _594      · split595        · cases d <;> simp only <;> (try split) <;> first | exact orGate_valid _ _ _ | exact constGate_valid _596        · split597          · cases d <;> simp only <;> (try split) <;> first | exact orGate_valid _ _ _ | exact constGate_valid _598          · exact constGate_valid _599  · simp only [List.mem_map] at hg600    obtain ⟨o, _, rfl⟩ := hg601    exact orGate_valid _ _ _602603/-- WIRED: if every formula reads only inputs below n, every first-layer gate has604    fan-in ≤ n. -/605theorem compileF_wired (cs : List Circ) (n : Nat) (hn : ∀ c ∈ cs, maxInput c ≤ n) :606    Wired n (compileF cs) := by607  have hlay : nLayers cs = (nLayers cs - 1) + 1 := by unfold nLayers; omega608  unfold compileF609  rw [hlay, List.range_succ_eq_map, List.map_cons, List.cons_append]610  intro g hg611  simp only [show (0 : Nat) + 1 ≤ 1 by omega, layerAt, if_true, List.mem_map, List.mem_range] at hg612  obtain ⟨g', hg', rfl⟩ := hg613  have hmem : (progOf cs).getD g' (.cst false) ∈ progOf cs := by614    rw [getD_eq_getElem' hg']; exact List.getElem_mem hg'615  have hr := emitL_reads 0 cs _ hmem616  have hmx : listMax (cs.map maxInput) ≤ n := listMax_le (fun a ha => by617    obtain ⟨c, hc, rfl⟩ := List.mem_map.mp ha; exact hn c hc)618  generalize (progOf cs).getD g' (.cst false) = d at hr619  cases d with620  | inp i => simp only [gate1, orGate_fanin]; simp [gmax] at hr; omega621  | cst b => simp [gate1, constGate_fanin]622  | neg a => simp only [gate1]; split <;> simp [constGate_fanin]623  | disj as => simp [gate1, constGate_fanin]624  | conj as => simp only [gate1]; split <;> (try split) <;> simp [constGate_fanin]625626theorem compileF_length (cs : List Circ) : (compileF cs).length = 2 * dmax cs + 2 := by627  simp [compileF, nLayers]628629theorem cs_le_prog (cs : List Circ) : cs.length ≤ (progOf cs).length := by630  rw [prog_length]631  have h : ∀ c ∈ cs, 1 ≤ size c := fun c _ => size_pos' c632  induction cs with633  | nil => simp634  | cons c cs ih =>635    simp only [List.length_cons, List.map_cons, List.sum_cons]636    have := ih (fun c' hc' => h c' (by simp [hc']))637    have := h c (by simp); omega638639/-- 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]; omega683684/-- Total number of gates: (2D + 1)·S computing gates and K output buffers. -/685def gateCount (ls : List Layer) : Nat := (ls.map List.length).sum686687theorem compileF_gates (cs : List Circ) :688    gateCount (compileF cs) = (2 * dmax cs + 1) * (cs.map size).sum + cs.length := by689  unfold gateCount compileF690  simp only [List.map_append, List.map_map, List.sum_append_nat, List.map_cons, List.map_nil, List.sum_cons,691    List.sum_nil, List.length_map, outs_length, Nat.add_zero]692  have e : ∀ t ∈ List.range (nLayers cs), (List.length ∘ fun t => layerAt (progOf cs) (t + 1)) t =693      (cs.map size).sum := by694    intro t _; simp only [Function.comp_apply, layerAt]; split <;> simp [prog_length]695  rw [List.map_congr_left e, List.map_const', List.sum_replicate_nat, List.length_range]696  unfold nLayers; rfl697698/-- 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  omega714715/-- 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⟩721722723/-! ## Axiom audit -/724725#print axioms sum_range_pos726#print axioms orGate_eval727#print axioms constGate_eval728#print axioms orGate_valid729#print axioms constGate_valid730#print axioms orGate_fanin731#print axioms constGate_fanin732#print axioms lvlL_eq733#print axioms lvl_fhom734#print axioms lvl_le735#print axioms lvlL_le736#print axioms run_take737#print axioms run_getD738#print axioms rd_take739#print axioms lvlAlg_pos740#print axioms lv_pos741#print axioms getD_eq_getElem'742#print axioms vl_eq743#print axioms lv_eq744#print axioms rdv_take745#print axioms rdl_take746#print axioms evalLayer_at747#print axioms listMax_ge748#print axioms vl_inp749#print axioms vl_cst750#print axioms vl_neg751#print axioms vl_disj752#print axioms vl_conj753#print axioms lv_inp754#print axioms lv_cst755#print axioms lv_neg756#print axioms lv_disj757#print axioms lv_conj758#print axioms child_lv759#print axioms decide_or1760#print axioms ys_spec761#print axioms evalNet_append762#print axioms evalNet_layers763#print axioms outs_range764#print axioms outs_length765#print axioms prog_length766#print axioms valAlg_fhom767#print axioms outs_val768#print axioms outs_lv769#print axioms compileF_eval770#print axioms compileF_eval_out771#print axioms compileF_valid772#print axioms compileF_wired773#print axioms compileF_length774#print axioms cs_le_prog775#print axioms compileF_bounded776#print axioms compileF_gates777#print axioms compileF_spec778#print axioms compileF_fixed_grid779end ThresholdNet780end NimAudit