FiniteNet

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 Circuit23/- Phase 4, Priority 1: finite-input network simulation.  Written by Claude4   (10 October 2026).  Lean 4.26.0, core/Std only.56   Repair of the phase-3 specification gap found by the audit: `network_ac0` bounded7   the inputs of a clipped formula, while correctness/depth/size were proved for the8   unclipped one.  Here ONE formula, `netFormula W n ls i = compileNet W ls (clip n) i`,9   carries all four properties:10     * semantics: it computes the network on the n-bit input, zero-extended11       (explicit finite-input semantics `pad n x`);12     * depth ≤ 3L, size ≤ 2 (2W+3)^L (M+1)^(WL);13     * it reads only inputs 0..n-1 (maxInput ≤ n).14   For WIRED networks (first-layer fan-in ≤ n) the zero-extension is irrelevant and15   the same formula computes the unpadded network (outputs i < n for zero layers).16   The audit's one-layer counterexample violates the wiring premise and is handled17   by the padded semantics (`audit_example`).  Families with polynomially many output18   bits get per-output and total formula-size bounds. -/1920namespace NimAudit21namespace FiniteNet2223open AC0 AC0.Circ2425/-- Zero-extension of an n-bit assignment. -/26def pad (n : Nat) (x : Nat → Bool) : Nat → Bool := fun j => if j < n then x j else false2728/-- Input leaves for an n-bit input: variables 0..n-1, constant false beyond. -/29def clip (n : Nat) : Nat → Circ := fun j => if j < n then input j else const false3031/-- THE compiled formula for output i of network ls on n inputs. -/32def netFormula (W n : Nat) (ls : List Layer) (i : Nat) : Circ := compileNet W ls (clip n) i3334theorem eval_clip (x : Nat → Bool) (n j : Nat) : eval x (clip n j) = pad n x j := by35  unfold clip pad; split <;> simp3637theorem clip_size (n j : Nat) : size (clip n j) ≤ 1 := by unfold clip; split <;> simp38theorem clip_depth (n j : Nat) : depth (clip n j) ≤ 0 := by unfold clip; split <;> simp39theorem clip_max (n j : Nat) : maxInput (clip n j) ≤ n := by40  unfold clip; split <;> simp <;> omega4142/-- FINITE-INPUT SIMULATION THEOREM (same formula for all four properties).43    For a valid network of L = ls.length layers with fan-ins and widths ≤ M and any44    input length n, output i is computed (on zero-extended n-bit inputs) by45    netFormula W n ls i, which has depth ≤ 3L, size ≤ 2 (2W+3)^L (M+1)^(WL) and reads46    only inputs < n. -/47theorem netFormula_spec {W M : Nat} (n : Nat) (ls : List Layer) (hv : NetValid W ls)48    (hb : NetBounded M ls) (i : Nat) :49    (∀ x : Nat → Bool, eval x (netFormula W n ls i) = evalNet ls (pad n x) i) ∧50    depth (netFormula W n ls i) ≤ 3 * ls.length ∧51    size (netFormula W n ls i) ≤ 2 * ((2 * W + 3) ^ ls.length * (M + 1) ^ (W * ls.length)) ∧52    maxInput (netFormula W n ls i) ≤ n := by53  have hsd := compileNet_sd (W := W) ls hb (clip n) 1 0 (clip_size n) (clip_depth n) i54  refine ⟨?_, ?_, ?_, compileNet_max ls (clip n) n (clip_max n) i⟩55  · intro x56    unfold netFormula57    rw [eval_compileNet ls hv]58    congr 159    funext j60    exact eval_clip x n j61  · have := hsd.2; unfold netFormula; omega62  · have h1 := sizeBound_closed W M ls.length63    have h2 := hsd.164    unfold netFormula; omega6566/-- The formula depends only on the first n input bits. -/67theorem netFormula_local {W M : Nat} (n : Nat) (ls : List Layer) (hb : NetBounded M ls) (i : Nat)68    (x y : Nat → Bool) (hxy : ∀ j, j < n → x j = y j) :69    eval x (netFormula W n ls i) = eval y (netFormula W n ls i) :=70  eval_congr_below x y _ (fun j hj =>71    hxy j (Nat.lt_of_lt_of_le hj (compileNet_max ls (clip n) n (clip_max n) i)))7273/-! ## Wired networks: unpadded semantics -/7475/-- First-layer gates read only the n input bits. -/76def Wired (n : Nat) : List Layer → Prop77  | [] => True78  | l :: _ => ∀ g ∈ l, g.fanin ≤ n7980theorem gate_eval_congr (g : Gate) (z z' : Nat → Bool) (h : ∀ j, j < g.fanin → z j = z' j) :81    g.eval z = g.eval z' := by82  unfold Gate.eval Gate.wsum Gate.psum83  congr 284  have : ∀ j ∈ List.range g.fanin, g.coeff j * (if g.lit z j then 1 else 0) =85      g.coeff j * (if g.lit z' j then 1 else 0) := by86    intro j hj87    unfold Gate.lit88    rw [h j (List.mem_range.mp hj)]89  rw [List.map_congr_left this]9091theorem evalLayer_congr (l : Layer) (n : Nat) (hl : ∀ g ∈ l, g.fanin ≤ n) (z z' : Nat → Bool)92    (h : ∀ j, j < n → z j = z' j) : evalLayer l z = evalLayer l z' := by93  funext i94  unfold evalLayer95  cases hi : l[i]? with96  | none => rfl97  | some g =>98    simp only99    exact gate_eval_congr g z z' (fun j hj =>100      h j (Nat.lt_of_lt_of_le hj (hl g (List.mem_of_getElem? hi))))101102/-- For wired networks the zero-extension does not change any output (outputs103    i < n in the zero-layer case). -/104theorem wired_pad (n : Nat) (ls : List Layer) (hw : Wired n ls) (x : Nat → Bool) (i : Nat)105    (hi : ls = [] → i < n) : evalNet ls (pad n x) i = evalNet ls x i := by106  cases ls with107  | nil => simp [evalNet, pad, hi rfl]108  | cons l ls =>109    simp only [evalNet]110    rw [evalLayer_congr l n hw (pad n x) x (fun j hj => by simp [pad, hj])]111112/-- WIRED SIMULATION THEOREM: for a wired valid network the SAME formula computes113    the unpadded network on every assignment, with the same depth/size/input bounds. -/114theorem netFormula_wired {W M : Nat} (n : Nat) (ls : List Layer) (hv : NetValid W ls)115    (hb : NetBounded M ls) (hw : Wired n ls) (i : Nat) (hi : ls = [] → i < n) :116    (∀ x : Nat → Bool, eval x (netFormula W n ls i) = evalNet ls x i) ∧117    depth (netFormula W n ls i) ≤ 3 * ls.length ∧118    size (netFormula W n ls i) ≤ 2 * ((2 * W + 3) ^ ls.length * (M + 1) ^ (W * ls.length)) ∧119    maxInput (netFormula W n ls i) ≤ n := by120  obtain ⟨h1, h2, h3, h4⟩ := netFormula_spec n ls hv hb i121  exact ⟨fun x => by rw [h1, wired_pad n ls hw x i hi], h2, h3, h4⟩122123/-! ## The audit counterexample -/124125def probeNet : List Layer := [[⟨[0, 1], [false, false], 1⟩]]126127/-- The audit's network is not wired for n = 1 (it reads input 1). -/128theorem probe_not_wired : ¬ Wired 1 probeNet := by129  intro h130  have := h ⟨[0, 1], [false, false], 1⟩ (by simp [probeNet])131  simp [Gate.fanin] at this132133/-- Under the explicit finite-input semantics the audit network on n = 1 inputs is134    the constant-false function, and netFormula computes exactly that while reading135    only input 0. -/136theorem audit_example (x : Nat → Bool) :137    eval x (netFormula 1 1 probeNet 0) = false ∧ maxInput (netFormula 1 1 probeNet 0) ≤ 1 := by138  have hv : NetValid 1 probeNet := by simp [NetValid, probeNet, Gate.Valid]139  have hb : NetBounded 2 probeNet := by simp [NetBounded, probeNet, Gate.fanin]140  obtain ⟨h1, _, _, h4⟩ := netFormula_spec 1 probeNet hv hb 0141  refine ⟨?_, h4⟩142  rw [h1]143  have : pad 1 x 1 = false := by simp [pad]144  simp only [probeNet, evalNet, evalLayer, List.getElem?_cons_zero, Gate.eval, Gate.wsum,145    Gate.psum, Gate.fanin, Gate.coeff, Gate.lit]146  simp [List.range_succ, this]147148/-! ## Families with polynomially many output bits -/149150/-- Total formula size of the first K outputs (no sharing between outputs). -/151def totalSize (W n : Nat) (ls : List Layer) (K : Nat) : Nat :=152  ((List.range K).map (fun i => size (netFormula W n ls i))).sum153154theorem totalSize_le {W M : Nat} (n : Nat) (ls : List Layer) (hv : NetValid W ls)155    (hb : NetBounded M ls) (K : Nat) :156    totalSize W n ls K ≤ K * (2 * ((2 * W + 3) ^ ls.length * (M + 1) ^ (W * ls.length))) := by157  unfold totalSize158  have h := sum_map_le_mem (l := List.range K) (f := fun i => size (netFormula W n ls i))159    (g := fun _ => 2 * ((2 * W + 3) ^ ls.length * (M + 1) ^ (W * ls.length)))160    (fun i _ => (netFormula_spec n ls hv hb i).2.2.1)161  rw [List.map_const', List.sum_replicate_nat, List.length_range] at h162  exact h163164/-- 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)201202203/-! ## Axiom audit -/204205#print axioms eval_clip206#print axioms clip_size207#print axioms clip_depth208#print axioms clip_max209#print axioms netFormula_spec210#print axioms netFormula_local211#print axioms gate_eval_congr212#print axioms evalLayer_congr213#print axioms wired_pad214#print axioms netFormula_wired215#print axioms probe_not_wired216#print axioms audit_example217#print axioms totalSize_le218#print axioms family_finite219end FiniteNet220end NimAudit