AC0 circuit normalization -- proof internals

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

theorem Complexity.Circuit.eval_wireAC0Formula_internal {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)

theorem Complexity.Circuit.eval_outputAC0Formula_internal {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

theorem Complexity.Circuit.depth_wireAC0Formula_internal {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

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

theorem Complexity.Circuit.size_wireAC0Formula_internal {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)

theorem Complexity.Circuit.size_outputAC0Formula_internal {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)