AC0 circuit normalization

Every selected output of an unbounded AND/OR circuit unfolds to an equivalent negation-normal unbounded formula. Duplicate signed inputs are removed before unfolding, so the formula has:

• depth no larger than the selected circuit-output depth; and
• tree size at most (2 * (N + G) + 1) ^ (outputDepth + 1).

For constant-depth, polynomial-gate circuit families this bound is polynomial. No uniformity assumption is used.

theorem Complexity.Gate.signedSupport_card_le {W : ℕ} (gate : Gate Basis.unboundedAndOr W) (outerNegated : Bool) : (gate.signedSupport outerNegated).card ≤ 2 * W

A gate has at most two distinct signed occurrences of each available source wire, regardless of how many duplicate incidences its raw input table contains.

theorem Complexity.Circuit.eval_wireAC0Formula {N M G : ℕ} [NeZero N] [NeZero M] (circuit : Circuit Basis.unboundedAndOr N M G) (input : BitString N) (negated : Bool) (wire : Fin (N + G)) : AC0Formula.eval input (circuit.wireAC0Formula negated wire) = (negated ^^ circuit.wireValue input wire)

Wire normalization preserves semantics, including an optional requested complement.

theorem Complexity.Circuit.eval_outputAC0Formula {N M G : ℕ} [NeZero N] [NeZero M] (circuit : Circuit Basis.unboundedAndOr N M G) (input : BitString N) (output : Fin M) : AC0Formula.eval input (circuit.outputAC0Formula output) = circuit.eval input output

Output normalization preserves the selected output bit exactly.

theorem Complexity.Circuit.depth_wireAC0Formula {N M G : ℕ} [NeZero N] [NeZero M] (circuit : Circuit Basis.unboundedAndOr N M G) (negated : Bool) (wire : Fin (N + G)) : (circuit.wireAC0Formula negated wire).depth ≤ circuit.wireDepth wire

Normalizing a wire does not increase its circuit depth.

theorem Complexity.Circuit.depth_outputAC0Formula {N M G : ℕ} [NeZero N] [NeZero M] (circuit : Circuit Basis.unboundedAndOr N M G) (output : Fin M) : (circuit.outputAC0Formula output).depth ≤ circuit.outputDepth output

Normalizing an output does not increase its output depth.

theorem Complexity.Circuit.size_wireAC0Formula {N M G : ℕ} [NeZero N] [NeZero M] (circuit : Circuit Basis.unboundedAndOr N M G) (negated : Bool) (wire : Fin (N + G)) : (circuit.wireAC0Formula negated wire).size ≤ (2 * (N + G) + 1) ^ (circuit.wireDepth wire + 1)

The normalized formula below a wire has an explicit tree-size bound in terms of the number of available signed wires and wire depth.

theorem Complexity.Circuit.size_outputAC0Formula {N M G : ℕ} [NeZero N] [NeZero M] (circuit : Circuit Basis.unboundedAndOr N M G) (output : Fin M) : (circuit.outputAC0Formula output).size ≤ (2 * (N + G) + 1) ^ (circuit.outputDepth output + 1)

The normalized selected-output formula has polynomial tree size whenever gate count is polynomial and depth is constant.

theorem Complexity.Circuit.outputAC0Formula_spec {N M G : ℕ} [NeZero N] [NeZero M] (circuit : Circuit Basis.unboundedAndOr N M G) (output : Fin M) : (∀ (input : BitString N), AC0Formula.eval input (circuit.outputAC0Formula output) = circuit.eval input output) ∧ (circuit.outputAC0Formula output).depth ≤ circuit.outputDepth output ∧ (circuit.outputAC0Formula output).size ≤ (2 * (N + G) + 1) ^ (circuit.outputDepth output + 1)

Bundled finite AC0 normalization theorem.