Negation-normal unbounded formulas for AC0

This public surface provides the semantic and quantitative De Morgan laws for AC0Formula, the tree representation used by AC0 normalization and restriction arguments.

theorem Complexity.AC0Formula.eval_neg {N : ℕ} (input : BitString N) (formula : AC0Formula N) : eval input formula.neg = !eval input formula

De Morgan negation computes Boolean complement.

theorem Complexity.AC0Formula.size_neg {N : ℕ} (formula : AC0Formula N) : formula.neg.size = formula.size

Negation preserves total tree size.

theorem Complexity.AC0Formula.depth_neg {N : ℕ} (formula : AC0Formula N) : formula.neg.depth = formula.depth

Negation preserves formula depth.