Circuit realizations of unbounded formula trees

Every AC0Formula over a positive input width has an equivalent circuit over Basis.unboundedAndOr with exactly the same size and depth at most one greater. The extra layer accounts for the circuit model's counted output gates at leaves. Empty connectives are realized by nullary gates.

This is a finite existence theorem. It imposes no uniformity condition on a family of circuits chosen at different input lengths.

theorem Complexity.AC0Formula.exists_circuit {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

An unbounded formula has a circuit realization with exact size and at most one extra depth layer, including constants and empty connectives.