Documentation

LeanPool.CircuitComplexity.AC0.Defs

AC0 — Core Definitions #

This module defines the AC0 circuit complexity class.

Main definitions #

A Boolean function family is in AC0 if there exist constants d (depth bound) and c (size exponent) such that for every input length N ≥ 1, some unbounded-fan-in AND/OR circuit of depth at most d and size at most N ^ c computes f N.

This captures the standard definition of AC0:

  • Constant depth: the circuit depth does not grow with N.
  • Polynomial size: the number of gates is bounded by a polynomial in N.
  • Unbounded fan-in: AND and OR gates may have arbitrarily many inputs.
  • Free negation: each gate input carries a negation flag (standard in circuit complexity).
Equations
  • One or more equations did not get rendered due to their size.
Instances For