SharedCircuit

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 BinaryReadout23/- Phase 4, Priority 2b: formula versus shared-circuit (DAG) conventions.4   Written by Claude (10 October 2026).  Lean 4.26.0, core/Std only.56   All earlier circuit statements use FORMULAS (`AC0.Circ`, trees without sharing).7   The classical parity theorem is normally stated for CIRCUITS with sharing.  This8   file defines bounded-depth straight-line circuits (DAGs) and proves both9   translations, so that the two conventions are related precisely:1011     * EMBEDDING   formula C  ↦  DAG `toDag C` with the same function, the same depth12                   (NOT counted), exactly `size C` gates, reading the same inputs;13     * UNFOLDING   DAG D with fan-in ≤ F (F ≥ 1)  ↦  formula `D.formula` with the same14                   function, the same depth, size ≤ (F+1)^depth, reading the same inputs.1516   Consequences: the DAG form of the parity-correlation premise implies the formula17   form at the SAME depth and size (`formula_premise_of_dag`), so every conditional18   readout theorem may assume the classical theorem in the shared-circuit convention19   (`network_readout_bound_dag`); conversely the formula premise at size (F+1)^d20   implies the DAG premise for fan-in-F circuits of depth d (`dag_premise_of_formula`),21   which is polynomial for constant d.2223   DAG semantics: a program is a list of gates in topological order; gate k reads the24   values of gates with smaller index; a reference to any other index reads a fixed25   default (false), so every list of gates is a well-defined circuit. -/2627namespace NimAudit28namespace Shared2930open AC0 AC0.Circ Prob Bridge CorrBridge3132inductive DGate where33  | inp (i : Nat)34  | cst (b : Bool)35  | neg (a : Nat)36  | conj (as : List Nat)37  | disj (as : List Nat)3839/-- An interpretation of the gate types over a carrier (values, depths, formulas, …). -/40structure Alg (α : Type) where41  dflt : α42  inp : Nat → α43  cst : Bool → α44  neg : α → α45  conj : List α → α46  disj : List α → α4748def rd {α : Type} (A : Alg α) (acc : List α) (a : Nat) : α := acc.getD a A.dflt4950def gstep {α : Type} (A : Alg α) (acc : List α) : DGate → α51  | .inp i => A.inp i52  | .cst b => A.cst b53  | .neg a => A.neg (rd A acc a)54  | .conj as => A.conj (as.map (rd A acc))55  | .disj as => A.disj (as.map (rd A acc))5657/-- Sequential evaluation: append the value of each gate in turn. -/58def run {α : Type} (A : Alg α) (acc : List α) : List DGate → List α59  | [] => acc60  | g :: C => run A (acc ++ [gstep A acc g]) C6162section Generic63variable {α β : Type}6465theorem run_append (A : Alg α) : ∀ (acc : List α) (C D : List DGate),66    run A acc (C ++ D) = run A (run A acc C) D67  | _, [], _ => rfl68  | acc, g :: C, D => run_append A (acc ++ [gstep A acc g]) C D6970theorem run_prefix (A : Alg α) : ∀ (acc : List α) (C : List DGate),71    ∃ W, run A acc C = acc ++ W ∧ W.length = C.length72  | acc, [] => ⟨[], by simp [run]⟩73  | acc, g :: C => by74    obtain ⟨W, h1, h2⟩ := run_prefix A (acc ++ [gstep A acc g]) C75    exact ⟨gstep A acc g :: W, by simp [run, h1], by simp [h2]⟩7677theorem run_length (A : Alg α) (acc : List α) (C : List DGate) :78    (run A acc C).length = acc.length + C.length := by79  obtain ⟨W, h1, h2⟩ := run_prefix A acc C80  rw [h1, List.length_append, h2]8182theorem rd_append_left (A : Alg α) (l W : List α) {a : Nat} (h : a < l.length) :83    rd A (l ++ W) a = rd A l a := by84  simp [rd, List.getD_eq_getElem?_getD, List.getElem?_append_left h]8586theorem rd_snoc (A : Alg α) (l : List α) (v : α) : rd A (l ++ [v]) l.length = v := by87  simp [rd, List.getD_eq_getElem?_getD]8889theorem rd_map (A : Alg α) (B : Alg β) (h : α → β) (hd : h A.dflt = B.dflt) (l : List α) (a : Nat) :90    h (rd A l a) = rd B (l.map h) a := by91  simp only [rd, List.getD_eq_getElem?_getD, List.getElem?_map]92  cases l[a]? <;> simp [hd]9394theorem rd_inv (A : Alg α) (P : α → Prop) (l : List α) (a : Nat) (hl : ∀ v ∈ l, P v) (hd : P A.dflt) :95    P (rd A l a) := by96  simp only [rd, List.getD_eq_getElem?_getD]97  cases h : l[a]? with98  | none => simpa using hd99  | some v => simpa using hl v (List.mem_of_getElem? h)100101/-- An invariant preserved by every gate step is preserved by evaluation. -/102theorem run_inv (A : Alg α) (P : α → Prop) (Q : DGate → Prop)103    (hstep : ∀ acc g, Q g → (∀ v ∈ acc, P v) → P (gstep A acc g)) :104    ∀ (C : List DGate) (acc : List α), (∀ g ∈ C, Q g) → (∀ v ∈ acc, P v) → ∀ v ∈ run A acc C, P v105  | [], _, _, hacc => hacc106  | g :: C, acc, hC, hacc => by107    apply run_inv A P Q hstep C _ (fun g' hg' => hC g' (by simp [hg']))108    intro v hv109    simp only [List.mem_append, List.mem_singleton] at hv110    rcases hv with hv | rfl111    · exact hacc v hv112    · exact hstep acc g (hC g (by simp)) hacc113114/-- Homomorphism of interpretations. -/115structure Hom (A : Alg α) (B : Alg β) (h : α → β) : Prop where116  dflt : h A.dflt = B.dflt117  inp : ∀ i, h (A.inp i) = B.inp i118  cst : ∀ b, h (A.cst b) = B.cst b119  neg : ∀ a, h (A.neg a) = B.neg (h a)120  conj : ∀ l, h (A.conj l) = B.conj (l.map h)121  disj : ∀ l, h (A.disj l) = B.disj (l.map h)122123theorem gstep_hom {A : Alg α} {B : Alg β} {h : α → β} (hh : Hom A B h) (acc : List α) (g : DGate) :124    h (gstep A acc g) = gstep B (acc.map h) g := by125  cases g with126  | inp i => exact hh.inp i127  | cst b => exact hh.cst b128  | neg a => simp only [gstep]; rw [hh.neg, rd_map A B h hh.dflt]129  | conj as =>130    simp only [gstep]; rw [hh.conj, List.map_map]131    congr 1; apply List.map_congr_left; intro a _; exact rd_map A B h hh.dflt acc a132  | disj as =>133    simp only [gstep]; rw [hh.disj, List.map_map]134    congr 1; apply List.map_congr_left; intro a _; exact rd_map A B h hh.dflt acc a135136theorem run_hom {A : Alg α} {B : Alg β} {h : α → β} (hh : Hom A B h) :137    ∀ (acc : List α) (C : List DGate), (run A acc C).map h = run B (acc.map h) C138  | _, [] => rfl139  | acc, g :: C => by140    simp only [run]141    rw [run_hom hh _ C, List.map_append, List.map_cons, List.map_nil, gstep_hom hh]142143end Generic144145/-! ## Interpretations -/146147def valAlg (x : Nat → Bool) : Alg Bool := ⟨false, x, id, (!·), fun l => l.all id, fun l => l.any id⟩148def depAlg : Alg Nat := ⟨0, fun _ => 0, fun _ => 0, (· + 1), fun l => listMax l + 1, fun l => listMax l + 1⟩149def maxAlg : Alg Nat := ⟨0, (· + 1), fun _ => 0, id, listMax, listMax⟩150def frmAlg : Alg Circ := ⟨const false, input, const, not, and, or⟩151152theorem eval_hom (x : Nat → Bool) : Hom frmAlg (valAlg x) (eval x) :=153  ⟨by simp [frmAlg, valAlg], fun _ => by simp [frmAlg, valAlg], fun _ => by simp [frmAlg, valAlg],154   fun _ => by simp [frmAlg, valAlg], fun _ => by simp [frmAlg, valAlg, List.all_map],155   fun _ => by simp [frmAlg, valAlg, List.any_map]⟩156157theorem depth_hom : Hom frmAlg depAlg depth :=158  ⟨by simp [frmAlg, depAlg], fun _ => by simp [frmAlg, depAlg], fun _ => by simp [frmAlg, depAlg],159   fun _ => by simp [frmAlg, depAlg], fun _ => by simp [frmAlg, depAlg],160   fun _ => by simp [frmAlg, depAlg]⟩161162theorem maxIn_hom : Hom frmAlg maxAlg maxInput :=163  ⟨by simp [frmAlg, maxAlg], fun _ => by simp [frmAlg, maxAlg], fun _ => by simp [frmAlg, maxAlg],164   fun _ => by simp [frmAlg, maxAlg], fun _ => by simp [frmAlg, maxAlg],165   fun _ => by simp [frmAlg, maxAlg]⟩166167/-! ## Shared circuits -/168169/-- A bounded-depth shared circuit: a gate program and an output gate. -/170structure Dag where171  prog : List DGate172  out : Nat173174def gmax : DGate → Nat175  | .inp i => i + 1176  | _ => 0177178def gfan : DGate → Nat179  | .neg _ => 1180  | .conj as => as.length181  | .disj as => as.length182  | _ => 0183184namespace Dag185186def val {α : Type} (A : Alg α) (D : Dag) : α := rd A (run A [] D.prog) D.out187def eval (x : Nat → Bool) (D : Dag) : Bool := D.val (valAlg x)188/-- Depth of the output gate (NOT counted, as for formulas). -/189def depth (D : Dag) : Nat := D.val depAlg190/-- Number of gates (input and constant nodes included, as for formula size). -/191def size (D : Dag) : Nat := D.prog.length192/-- The unfolded formula. -/193def formula (D : Dag) : Circ := D.val frmAlg194def Reads (m : Nat) (D : Dag) : Prop := ∀ g ∈ D.prog, gmax g ≤ m195def Fanin (F : Nat) (D : Dag) : Prop := ∀ g ∈ D.prog, gfan g ≤ F196197end Dag198199theorem val_hom {α β : Type} {A : Alg α} {B : Alg β} {h : α → β} (hh : Hom A B h) (D : Dag) :200    h (D.val A) = D.val B := by201  simp only [Dag.val]202  rw [rd_map A B h hh.dflt, run_hom hh]203  rfl204205/-! ## Unfolding a DAG into a formula -/206207theorem formula_eval (x : Nat → Bool) (D : Dag) : eval x D.formula = D.eval x := val_hom (eval_hom x) D208209theorem formula_depth (D : Dag) : depth D.formula = D.depth := val_hom depth_hom D210211theorem formula_maxInput {m : Nat} (D : Dag) (h : D.Reads m) : maxInput D.formula ≤ m := by212  rw [show maxInput D.formula = D.val maxAlg from val_hom maxIn_hom D]213  apply rd_inv maxAlg (· ≤ m) _ _ _ (Nat.zero_le m)214  apply run_inv maxAlg (· ≤ m) (fun g => gmax g ≤ m) _ D.prog [] h (by simp)215  intro acc g hg hacc216  cases g with217  | inp i => exact hg218  | cst b => exact Nat.zero_le m219  | neg a => exact rd_inv maxAlg (· ≤ m) acc a hacc (Nat.zero_le m)220  | conj as =>221    apply listMax_le; intro v hv222    obtain ⟨a, _, rfl⟩ := List.mem_map.mp hv223    exact rd_inv maxAlg (· ≤ m) acc a hacc (Nat.zero_le m)224  | disj as =>225    apply listMax_le; intro v hv226    obtain ⟨a, _, rfl⟩ := List.mem_map.mp hv227    exact rd_inv maxAlg (· ≤ m) acc a hacc (Nat.zero_le m)228229theorem size_list_pow {F M : Nat} (cs : List Circ) (hlen : cs.length ≤ F)230    (h : ∀ c ∈ cs, size c ≤ (F + 1) ^ depth c) (hM : ∀ c ∈ cs, depth c ≤ M) :231    (cs.map size).sum + 1 ≤ (F + 1) ^ (M + 1) := by232  have h1 : ∀ c ∈ cs, size c ≤ (F + 1) ^ M := fun c hc =>233    Nat.le_trans (h c hc) (Nat.pow_le_pow_right (by omega) (hM c hc))234  have h2 := sum_le_len_mul h1235  have h3 : cs.length * (F + 1) ^ M ≤ F * (F + 1) ^ M := Nat.mul_le_mul_right _ hlen236  have h4 : 0 < (F + 1) ^ M := Nat.pow_pos (by omega)237  have h5 : (F + 1) ^ (M + 1) = F * (F + 1) ^ M + (F + 1) ^ M := by238    rw [Nat.pow_succ, Nat.mul_comm, Nat.succ_mul]239  omega240241/-- UNFOLDING: a shared circuit of depth D and fan-in ≤ F (F ≥ 1) unfolds into a242    formula computing the same function, of the same depth and size ≤ (F+1)^D. -/243theorem formula_size {F : Nat} (hF1 : 1 ≤ F) (D : Dag) (hF : D.Fanin F) :244    size D.formula ≤ (F + 1) ^ D.depth := by245  rw [← formula_depth]246  let P : Circ → Prop := fun c => size c ≤ (F + 1) ^ depth c247  have hd : P (const false) := by simp [P]248  show P (D.val frmAlg)249  apply rd_inv frmAlg P _ _ _ hd250  apply run_inv frmAlg P (fun g => gfan g ≤ F) _ D.prog [] hF (by simp)251  intro acc g hg hacc252  have hrd : ∀ a, P (rd frmAlg acc a) := fun a => rd_inv frmAlg P acc a hacc hd253  cases g with254  | inp i => show size (input i) ≤ (F + 1) ^ depth (input i); simp255  | cst b => show size (const b) ≤ (F + 1) ^ depth (const b); simp256  | neg a =>257    have h := hrd a258    show size (not (rd frmAlg acc a)) ≤ (F + 1) ^ depth (not (rd frmAlg acc a))259    generalize rd frmAlg acc a = c at h ⊢260    simp only [P] at h261    rw [size_not, depth_not, Nat.pow_succ]262    have h1 : 0 < (F + 1) ^ depth c := Nat.pow_pos (by omega)263    have h2 : (F + 1) ^ depth c * 2 ≤ (F + 1) ^ depth c * (F + 1) := Nat.mul_le_mul_left _ (by omega)264    omega265  | conj as =>266    show size (and (as.map (rd frmAlg acc))) ≤ (F + 1) ^ depth (and (as.map (rd frmAlg acc)))267    rw [size_and, depth_and]268    apply size_list_pow269    · simp only [List.length_map]; exact hg270    · intro c hc; obtain ⟨a, _, rfl⟩ := List.mem_map.mp hc; exact hrd a271    · intro c hc; exact le_listMax (List.mem_map_of_mem hc)272  | disj as =>273    show size (or (as.map (rd frmAlg acc))) ≤ (F + 1) ^ depth (or (as.map (rd frmAlg acc)))274    rw [size_or, depth_or]275    apply size_list_pow276    · simp only [List.length_map]; exact hg277    · intro c hc; obtain ⟨a, _, rfl⟩ := List.mem_map.mp hc; exact hrd a278    · intro c hc; exact le_listMax (List.mem_map_of_mem hc)279280/-! ## Embedding a formula into a DAG -/281282mutual283/-- Gates for formula c, appended to a program that already has `base` gates. -/284def emit (base : Nat) : Circ → List DGate285  | .input i => [.inp i]286  | .const b => [.cst b]287  | .not c => emit base c ++ [.neg (base + (emit base c).length - 1)]288  | .and cs => (emitL base cs).1 ++ [.conj (emitL base cs).2]289  | .or cs => (emitL base cs).1 ++ [.disj (emitL base cs).2]290/-- Gates for a list of formulas, with the indices of their output gates. -/291def emitL (base : Nat) : List Circ → List DGate × List Nat292  | [] => ([], [])293  | c :: cs => (emit base c ++ (emitL (base + (emit base c).length) cs).1,294      (base + (emit base c).length - 1) :: (emitL (base + (emit base c).length) cs).2)295end296297mutual298theorem emit_len (base : Nat) : ∀ c : Circ, (emit base c).length = size c299  | .input i => by simp [emit]300  | .const b => by simp [emit]301  | .not c => by simp [emit, emit_len base c]302  | .and cs => by simp [emit, (emitL_len base cs).1]303  | .or cs => by simp [emit, (emitL_len base cs).1]304theorem emitL_len (base : Nat) : ∀ cs : List Circ,305    (emitL base cs).1.length = (cs.map size).sum ∧ (emitL base cs).2.length = cs.length306  | [] => by simp [emitL]307  | c :: cs => by308    have h := emitL_len (base + (emit base c).length) cs309    rw [emit_len base c] at h310    simp [emitL, emit_len base c, h.1, h.2]311end312313theorem size_pos' (c : Circ) : 1 ≤ size c := by314  cases c <;> simp [size_input, size_const, size_not, size_and, size_or]315316/-- Formula-side equations of an interpretation-valued function. -/317structure FHom {α : Type} (A : Alg α) (f : Circ → α) : Prop where318  inp : ∀ i, f (input i) = A.inp i319  cst : ∀ b, f (const b) = A.cst b320  neg : ∀ c, f (not c) = A.neg (f c)321  conj : ∀ cs, f (and cs) = A.conj (cs.map f)322  disj : ∀ cs, f (or cs) = A.disj (cs.map f)323324section Emit325variable {α : Type} (A : Alg α) (f : Circ → α)326327mutual328theorem emit_val (hf : FHom A f) (base : Nat) : ∀ (c : Circ) (acc : List α), acc.length = base →329    rd A (run A acc (emit base c)) (base + size c - 1) = f c330  | .input i, acc, hl => by331    simp only [emit, run, size_input]332    rw [show base + 1 - 1 = acc.length by omega, rd_snoc]; exact (hf.inp i).symm333  | .const b, acc, hl => by334    simp only [emit, run, size_const]335    rw [show base + 1 - 1 = acc.length by omega, rd_snoc]; exact (hf.cst b).symm336  | .not c, acc, hl => by337    have ih := emit_val hf base c acc hl338    have hlen := run_length A acc (emit base c)339    rw [emit_len] at hlen340    simp only [emit, run_append, run, size_not, emit_len]341    rw [show base + (size c + 1) - 1 = (run A acc (emit base c)).length by omega, rd_snoc]342    simp only [gstep]; rw [ih, hf.neg]343  | .and cs, acc, hl => by344    have ih := emitL_val hf base cs acc hl345    have hlen := run_length A acc (emitL base cs).1346    rw [(emitL_len base cs).1] at hlen347    simp only [emit, run_append, run, size_and]348    rw [show base + ((cs.map size).sum + 1) - 1 = (run A acc (emitL base cs).1).length by omega, rd_snoc]349    simp only [gstep]; rw [ih, hf.conj]350  | .or cs, acc, hl => by351    have ih := emitL_val hf base cs acc hl352    have hlen := run_length A acc (emitL base cs).1353    rw [(emitL_len base cs).1] at hlen354    simp only [emit, run_append, run, size_or]355    rw [show base + ((cs.map size).sum + 1) - 1 = (run A acc (emitL base cs).1).length by omega, rd_snoc]356    simp only [gstep]; rw [ih, hf.disj]357theorem emitL_val (hf : FHom A f) (base : Nat) : ∀ (cs : List Circ) (acc : List α), acc.length = base →358    (emitL base cs).2.map (rd A (run A acc (emitL base cs).1)) = cs.map f359  | [], _, _ => by simp [emitL]360  | c :: cs, acc, hl => by361    have h1 := emit_val hf base c acc hl362    have hlen := run_length A acc (emit base c)363    have hpos := size_pos' c364    rw [emit_len] at hlen365    have h2 := emitL_val hf (base + (emit base c).length) cs (run A acc (emit base c))366      (by rw [hlen, emit_len]; omega)367    simp only [emitL, List.map_cons, run_append]368    obtain ⟨W, hW, _⟩ := run_prefix A (run A acc (emit base c)) (emitL (base + (emit base c).length) cs).1369    rw [h2, hW, rd_append_left A _ W (by rw [hlen, emit_len]; omega), emit_len, h1]370end371372end Emit373374mutual375theorem emit_reads (base : Nat) : ∀ c : Circ, ∀ g ∈ emit base c, gmax g ≤ maxInput c376  | .input i => by intro g hg; simp [emit] at hg; subst hg; simp [gmax]377  | .const b => by intro g hg; simp [emit] at hg; subst hg; simp [gmax]378  | .not c => by379    intro g hg380    simp only [emit, List.mem_append, List.mem_singleton] at hg381    rcases hg with hg | rfl382    · simpa using emit_reads base c g hg383    · simp [gmax]384  | .and cs => by385    intro g hg386    simp only [emit, List.mem_append, List.mem_singleton] at hg387    rcases hg with hg | rfl388    · simpa using emitL_reads base cs g hg389    · simp [gmax]390  | .or cs => by391    intro g hg392    simp only [emit, List.mem_append, List.mem_singleton] at hg393    rcases hg with hg | rfl394    · simpa using emitL_reads base cs g hg395    · simp [gmax]396theorem emitL_reads (base : Nat) : ∀ cs : List Circ, ∀ g ∈ (emitL base cs).1, gmax g ≤ listMax (cs.map maxInput)397  | [] => by intro g hg; simp [emitL] at hg398  | c :: cs => by399    intro g hg400    simp only [emitL, List.mem_append] at hg401    simp only [List.map_cons, listMax, List.foldr_cons]402    rcases hg with hg | hg403    · have := emit_reads base c g hg; omega404    · have := emitL_reads (base + (emit base c).length) cs g hg405      simp only [listMax] at this; omega406end407408/-- The DAG of a formula: one gate per formula node, output = last gate. -/409def toDag (c : Circ) : Dag := ⟨emit 0 c, size c - 1⟩410411/-- EMBEDDING: same function, same depth, exactly `size c` gates, same inputs read. -/412theorem toDag_spec (c : Circ) :413    (∀ x, (toDag c).eval x = eval x c) ∧ (toDag c).depth = depth c ∧ (toDag c).size = size c ∧414      (toDag c).Reads (maxInput c) := by415  refine ⟨fun x => ?_, ?_, ?_, emit_reads 0 c⟩416  · have hf : FHom (valAlg x) (eval x) :=417      ⟨fun _ => by simp [valAlg], fun _ => by simp [valAlg], fun _ => by simp [valAlg],418       fun _ => by simp [valAlg, List.all_map], fun _ => by simp [valAlg, List.any_map]⟩419    have := emit_val (valAlg x) (eval x) hf 0 c [] rfl420    simpa [Dag.eval, Dag.val, toDag] using this421  · have hf : FHom depAlg depth :=422      ⟨fun _ => by simp [depAlg], fun _ => by simp [depAlg], fun _ => by simp [depAlg],423       fun _ => by simp [depAlg], fun _ => by simp [depAlg]⟩424    have := emit_val depAlg depth hf 0 c [] rfl425    simpa [Dag.depth, Dag.val, toDag] using this426  · simp [Dag.size, toDag, emit_len]427428/-! ## The two premise conventions -/429430/-- The parity-correlation premise in the SHARED-CIRCUIT convention. -/431def DagParityPremise (d S m : Nat) (ε : Rat) : Prop :=432  ∀ D : Dag, D.depth ≤ d → D.size ≤ S → D.Reads m →433    -ε ≤ rsum (bitvecs m) (fun y => ind (D.eval (vfun y)) * sgn (par y)) / (2 : Rat) ^ m ∧434    rsum (bitvecs m) (fun y => ind (D.eval (vfun y)) * sgn (par y)) / (2 : Rat) ^ m ≤ ε435436/-- The same, restricted to fan-in ≤ F (any number of gates). -/437def DagParityPremiseF (d F m : Nat) (ε : Rat) : Prop :=438  ∀ D : Dag, D.depth ≤ d → D.Fanin F → D.Reads m →439    -ε ≤ rsum (bitvecs m) (fun y => ind (D.eval (vfun y)) * sgn (par y)) / (2 : Rat) ^ m ∧440    rsum (bitvecs m) (fun y => ind (D.eval (vfun y)) * sgn (par y)) / (2 : Rat) ^ m ≤ ε441442/-- The shared-circuit premise implies the formula premise at the same depth and size. -/443theorem formula_premise_of_dag {d S m : Nat} {ε : Rat} (h : DagParityPremise d S m ε) :444    ParityCorrPremise d S m ε := by445  intro C hd hs hm446  obtain ⟨he, hdep, hsz, hrd⟩ := toDag_spec C447  have := h (toDag C) (by rw [hdep]; exact hd) (by rw [hsz]; exact hs)448    (fun g hg => Nat.le_trans (hrd g hg) hm)449  simpa only [he] using this450451/-- The formula premise at size (F+1)^d implies the shared-circuit premise for fan-in-F452    circuits of depth d (polynomial size for constant d and polynomial F). -/453theorem dag_premise_of_formula {d F m : Nat} {ε : Rat} (hF1 : 1 ≤ F)454    (h : ParityCorrPremise d ((F + 1) ^ d) m ε) : DagParityPremiseF d F m ε := by455  intro D hd hF hm456  have := h D.formula (by rw [formula_depth]; exact hd)457    (Nat.le_trans (formula_size hF1 D hF) (Nat.pow_le_pow_right (by omega) hd))458    (formula_maxInput D hm)459  simpa only [formula_eval] using this460461/-- The network readout bound with the classical theorem assumed in the shared-circuit462    convention (same depth and size parameters as `BinReadout.network_readout_bound`). -/463theorem network_readout_bound_dag {W M B N j r L : Nat} (hj : j < B) (nets : Bool → List Layer)464    (hlen : ∀ b, (nets b).length = L) (hv : ∀ b, NetValid W (nets b))465    (hb : ∀ b, NetBounded M (nets b)) (hr : N + 1 ≤ 2 ^ r) {ε : Rat}466    (hprem : ∀ m, N + 1 ≤ m → m ≤ B * (N + 1) →467      DagParityPremise (3 * L + 2 + 11)468        (12 * Upar (N + 1) B ((r + 1) * (2 * ((2 * W + 3) ^ L * (M + 1) ^ (W * L)) + 1)) ^ 10) m ε) :469    succCountRO B (N + 1) (BinReadout.binReadoutOf B (N + 1)470        (fun b => BinReadout.netBCirc W B (N + 1) r (nets b))) j /471        nonzeroCount B (N + 1) ≤472      2 / (((2 ^ B : Nat) : Rat) - 1) + (((2 ^ B : Nat) : Rat) - 1) * ε :=473  BinReadout.network_readout_bound hj nets hlen hv hb hr474    (fun m h1 h2 => formula_premise_of_dag (hprem m h1 h2))475476477/-! ## Axiom audit -/478479#print axioms run_append480#print axioms run_prefix481#print axioms run_length482#print axioms rd_append_left483#print axioms rd_snoc484#print axioms rd_map485#print axioms rd_inv486#print axioms run_inv487#print axioms gstep_hom488#print axioms run_hom489#print axioms eval_hom490#print axioms depth_hom491#print axioms maxIn_hom492#print axioms val_hom493#print axioms formula_eval494#print axioms formula_depth495#print axioms formula_maxInput496#print axioms size_list_pow497#print axioms formula_size498#print axioms emit_len499#print axioms emitL_len500#print axioms size_pos'501#print axioms emit_val502#print axioms emitL_val503#print axioms emit_reads504#print axioms emitL_reads505#print axioms toDag_spec506#print axioms formula_premise_of_dag507#print axioms dag_premise_of_formula508#print axioms network_readout_bound_dag509end Shared510end NimAudit