CSLib circuits unfold to formulas with unchanged depth

A selected output of an unbounded AND/OR circuit, with free edge negations, unfolds to an identical Boolean function. Repeated signed wires are removed before unfolding, so the formula-size bound depends only on the number of inputs and gates, even for arbitrary fan-in.

theorem Complexity.CslibAC0.outputFormula_spec {n : ℕ} [NeZero n] (c : Cslib.Circuits.Circuit Basis.unboundedAndOr.signature n 1) : (∀ (x : BitString n), AC0Formula.eval x (outputFormula c) = c.eval Basis.unboundedAndOr.interpretation x 0) ∧ (outputFormula c).depth ≤ c.depth ∧ (outputFormula c).size ≤ (2 * (n + c.size) + 1) ^ (c.depth + 1)

The selected output has an equivalent formula with no greater depth and the stated size.