Majority is not in AC⁰[p], and AC⁰[p] is strictly contained in TC⁰

The AC⁰[p] basis contains the unbounded fan-in basis, so parity reduces to majority there in constant depth (ConstDepth.parity_mem_of_majority_mem). As parity is not in AC⁰[p] for an odd prime p (parity_notMem_AC0Mod), neither is majority, and since majority is in TC⁰, TC⁰ is not contained in AC⁰[p] (TC0_not_subset_AC0Mod). Together with AC⁰[p] ⊆ TC⁰ (AC0Mod_subset_TC0), AC⁰[p] is strictly contained in TC⁰ (AC0Mod_ssubset_TC0) [Raz87], [Smo87].

Main results

• Cslib.Circuits.Boolean.Smolensky.majority_notMem_AC0Mod: majority is not in AC⁰[p].
• Cslib.Circuits.Boolean.Smolensky.TC0_not_subset_AC0Mod: TC⁰ ⊄ AC⁰[p].
• Cslib.Circuits.Boolean.Smolensky.AC0Mod_ssubset_TC0: AC⁰[p] ⊊ TC⁰.

References

• A. A. Razborov, Lower bounds on the size of bounded depth circuits over a complete basis with logical addition
• R. Smolensky, Algebraic methods in the theory of lower bounds for Boolean circuit complexity

theorem Cslib.Circuits.Boolean.Smolensky.majority_notMem_AC0Mod {p : ℕ} [Fact (Nat.Prime p)] (hp2 : p ≠ 2) : Language.ofSlices majority ∉ AC0Mod p

Majority is not in AC⁰[p] for an odd prime p.

theorem Cslib.Circuits.Boolean.Smolensky.TC0_not_subset_AC0Mod {p : ℕ} [Fact (Nat.Prime p)] (hp2 : p ≠ 2) : ¬TC0 ⊆ AC0Mod p

TC⁰ is not contained in AC⁰[p] for an odd prime p.

theorem Cslib.Circuits.Boolean.Smolensky.AC0Mod_ssubset_TC0 {p : ℕ} [Fact (Nat.Prime p)] (hp2 : p ≠ 2) : AC0Mod p ⊂ TC0

AC⁰[p] is strictly contained in TC⁰ for an odd prime p.