Separations for AC0, AC0[3], and TC0

The parity family Schnorr.xorBool and the strict-majority family majority are not in the library's nonuniform AC0: no family of polynomial-size, constant-depth, unbounded-fan-in AND/OR circuits with free negation on gate inputs computes either family at every input length.

For parity, the proof normalizes each circuit to a negation-normal formula of no larger depth and polynomial size (Circuit.outputAC0Formula_spec) and contradicts the finite iterated-switching obstruction (AC0Formula.parity_counting_obstruction) at one explicit large input length. For strict majority (majority_not_mem_AC0), the proof applies the top-down Karchmer–Wigderson gate-count lower bound (Circuit.majority_superpolynomial_gates); it lives in Complexitylib.Circuits.AC0.Separation.Internal.Majority.

Since parity is in TC0 (xorBool_mem_TC0), AC0 ⊆ TC0 is strict, and since parity is not in AC0[3] (xorBool_not_mem_AC0Mod_three), TC0 is not contained in AC0[3].

theorem Complexity.xorBool_not_mem_AC0 : Schnorr.xorBool ∉ AC0

Parity is not in AC0. No polynomial-size, constant-depth family of unbounded-fan-in AND/OR circuits computes the parity family.

theorem Complexity.majority_not_mem_AC0 : (fun (x : ℕ) => majority) ∉ AC0

Strict majority is not in AC0. No polynomial-size, constant-depth family of unbounded-fan-in AND/OR circuits computes the strict-majority family majority (ties are rejected), at either parity of input length.

theorem Complexity.AC0_ssubset_TC0 : AC0 ⊂ TC0

AC0 is strictly contained in TC0, as nonuniform classes of Boolean function families. Parity separates them.

theorem Complexity.not_TC0_subset_AC0Mod_three : ¬TC0 ⊆ AC0Mod 3

TC0 is not contained in AC0[3]. Parity is in TC0 (xorBool_mem_TC0) by symmetric threshold decomposition, while Razborov–Smolensky shows that parity is not in AC0[3] (xorBool_not_mem_AC0Mod_three).