Lower bounds for AC0 circuits

TheoremMajority is not in AC0#●ready to prove

The majority language is not in the class \(\mathsf{AC}^0\).

public theorem_wanted majority_not_in_ac0 :
    majorityDec ∉ AC0

def majorityDec : MetaMathlibExt.ComplexityTheory.DecisionProblem :=
  fun x : List Bool => decide (2 * (x.filter fun b => b).length > x.length)

CSLibExt/Computability/Complexity/Classes.lean:584

def AC0 : DecisionComplexityClass :=
  {L | ∃ d, ∃ p : Polynomial ℕ, ∃ C : (n : ℕ) → List (ACGate n),
    ∀ n, WellFormedCircuit (C n) ∧ IsModFree (C n) ∧ (C n).length ≤ p.eval n ∧
      circuitDepth (C n) ≤ d ∧
      ∀ x : List Bool, x.length = n →
        (L x = true ↔
          (circuitEval (C n) (fun i => x.getD (i : ℕ) false)).getLast? = some true)}

CSLibExt/Computability/Complexity/Classes.lean:558

Sources

M. Ajtai, "Σ₁¹-formulae on finite structures", Annals of Pure and Applied Logic 24 (1983), 1-48; J. Håstad, "Almost optimal lower bounds for small depth circuits" (STOC 1986).

Uses 4

Statement usesThe class \(\mathsf{AC}^0\) · The majority language · Complexity classes · Decision problems

TheoremParity is not in AC0#●ready to prove

The parity language, which accepts a bitstring exactly when an odd number of its entries are true, is not in the class \(\mathsf{AC}^0\).

public theorem_wanted parity_not_in_ac0 :
    parityDec ∉ AC0

def parityDec : MetaMathlibExt.ComplexityTheory.DecisionProblem :=
  fun x : List Bool => decide ((x.filter fun b => b).length % 2 = 1)

CSLibExt/Computability/Complexity/Classes.lean:580

def AC0 : DecisionComplexityClass :=
  {L | ∃ d, ∃ p : Polynomial ℕ, ∃ C : (n : ℕ) → List (ACGate n),
    ∀ n, WellFormedCircuit (C n) ∧ IsModFree (C n) ∧ (C n).length ≤ p.eval n ∧
      circuitDepth (C n) ≤ d ∧
      ∀ x : List Bool, x.length = n →
        (L x = true ↔
          (circuitEval (C n) (fun i => x.getD (i : ℕ) false)).getLast? = some true)}

CSLibExt/Computability/Complexity/Classes.lean:558

Sources

M. Furst, J. Saxe, and M. Sipser, "Parity, circuits, and the polynomial-time hierarchy", Mathematical Systems Theory 17 (1984), 13-27; M. Ajtai, "Σ₁¹-formulae on finite structures", Annals of Pure and Applied Logic 24 (1983), 1-48; J. Håstad, "Almost optimal lower bounds for small depth circuits", Proceedings of the Eighteenth Annual ACM Symposium on Theory of Computing (STOC 1986), 6-20.

Uses 4

Statement usesThe class \(\mathsf{AC}^0\) · The parity language · Complexity classes · Decision problems

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.