Compiling unbounded formula trees to circuit DAGs

Pack child circuits in parallel and add one connective gate. Parallel packing retains a common depth bound and sums sizes exactly; serial composition adds the single parent gate. Constants and literals supply the base cases.

theorem Complexity.AC0Formula.constantCircuit_eval {N : ℕ} [NeZero N] (value : Bool) (input : BitString N) : (constantCircuit value).eval input 0 = value

theorem Complexity.AC0Formula.literalCircuit_eval {N : ℕ} [NeZero N] (literal : Literal N) (input : BitString N) : (literalCircuit literal).eval input 0 = literal.eval input

theorem Complexity.AC0Formula.connectiveCircuit_eval {N : ℕ} [NeZero N] (op : AndOrOp) (input : BitString N) : (connectiveCircuit op).eval input 0 = op.eval N input

theorem Complexity.AC0Formula.depth_no_internal {N : ℕ} [NeZero N] {B : Basis} (c : Circuit B N 1 0) : c.depth = 1

theorem Complexity.AC0Formula.size_le_forestSize_of_mem {N : ℕ} (f : AC0Formula N) (fs : AC0Forest N) (h : f ∈ fs.toList) : f.size ≤ forestSize fs

theorem Complexity.AC0Formula.exists_circuit_internal {N : ℕ} [NeZero N] (f : AC0Formula N) : ∃ (gates : ℕ) (c : Circuit Basis.unboundedAndOr N 1 gates), c.size = f.size ∧ c.depth ≤ f.depth + 1 ∧ ∀ (input : BitString N), c.eval input 0 = eval input f