Circuit Complexity Library

A Lean 4 formalization of classical results in Boolean circuit complexity, built on Mathlib.

The circuit model

A Circuit B N M G is an acyclic Boolean circuit over basis B with N primary inputs, M outputs, and G internal gates. The circuit's size is G + M: internal and output gates are counted, while primary-input vertices and per-edge negation flags are not. For an arbitrary basis, sizeComplexityWithTop is the minimum size of any circuit computing a Boolean function, with ⊤ for an unrealizable function. The natural-valued sizeComplexity interface is available for complete bases.

Main results

• Functional completeness (CompleteBasis Basis.unboundedAndOr): Unbounded fan-in AND/OR (with free negation) can compute every Boolean function, via DNF construction.

• Shannon counting lower bound (shannon_lower_bound_circuit): For N ≥ 6, there exists a Boolean function on N inputs that cannot be computed by any fan-in-2 AND/OR circuit of total size G + 1 at most ⌊2^N / (5N)⌋, where G counts internal gates.

• Essential-input lower bound (Circuit.card_essentialInputs_le_totalFanIn): Over every basis, essential inputs are bounded by total fan-in. For bounded fan-in k AND/OR this yields n' ≤ k · size.

• Schnorr's XOR lower bound (schnorr_lower_bound_circuit, parity_size_ge_three_mul): Any fan-in-2 AND/OR circuit computing N-input XOR (or its complement) requires at least 2(N − 1) internal gates, and has size at least 3(N − 1) by three-gate elimination.

• CNF/DNF lower bound for XOR (DNF.two_pow_le_complexity_of_xorBool, CNF.two_pow_le_complexity_of_xorBool): Any DNF (resp. CNF) computing N-input XOR requires at least 2^{N-1} terms (resp. clauses).

• Nondeterministic quantification (sizeComplexity_existsQuantify_le): If f has circuit complexity s, then ∃ x ∈ {0,1}^k, f(x,y) has circuit complexity at most 2^k · (s + 1). Combined with the Shannon upper bound (sizeComplexity_existsQuantify_le_min).

• Valiant's depth reduction (Valiant.depth_reduction): In any acyclic digraph with S edges and depth at most 2^k, for any r ≤ k one can remove a set of at most r · S / k edges so that the remaining digraph has depth at most 2^k / 2^r.

• Barrington's theorem (barrington_equivalence): Variable-bounded logarithmic-depth formula families are exactly variable-bounded polynomial-length width-5 permutation branching-program families as sets of typed BoolFunFamily. The finite forward theorem barrington_representation_depth_four gives the textbook length bound 4 ^ depth, and barrington_quadratic_of_log_depth specializes it to n² at depth at most log₂ n. barringtonCompile_representation supplies the same finite theorem through an explicit executable compiler rather than an existential choice. NC1_subset_Width5BP applies the typed theorem directly to actual nonuniform NC1 circuit families. The older barrington_equivalence_onTotalAssignments remains as an explicitly named theorem for syntax families whose domain really is ℕ → Bool.

• Spira formula balancing (BoolFormula.exists_spira_balanced): Every finite Boolean formula has an equivalent formula of logarithmic depth and polynomial tree size, with explicit quantitative bounds.

• Monotone Karchmer--Wigderson correspondence (KarchmerWigderson.Protocol.exists_protocol_depth_iff_formula_depth): root communication protocols and monotone formulas exist at exactly the same depth.

• Threshold simulation (AC_subset_TC): Exact basis transport embeds every nonuniform AC^i family in nonuniform TC^i without changing circuit size or depth.

• Finite AC0 obstruction for parity (AC0Formula.parity_counting_obstruction): Iterated width switching, exact staged-restriction semantics, and the decision-tree lower bound for parity yield a division-free finite counting inequality for every depth-bounded unbounded AND/OR formula computing parity.

• Parity separates AC0 from TC0 (xorBool_not_mem_AC0, xorBool_mem_TC0, AC0_ssubset_TC0): parity is not computed by any polynomial-size constant-depth unbounded AND/OR family, but depth-two threshold circuits of size N + 1 compute it, so AC0 ⊂ TC0. Strict majority is not in AC0 either (majority_not_mem_AC0), by the top-down gate-count bound.

• Razborov–Smolensky (xorBool_not_mem_AC0Mod_three, Smolensky.parity_size_lower_bound): parity is not in AC0[3]; a depth-d AND/OR/MOD_3 circuit computing n-bit parity has size at least (2/5) · 2^ℓ whenever (40ℓ)^{2d} ≤ n, by approximation with low-degree functions over ZMod 3. Hence TC0 ⊄ AC0[3] (not_TC0_subset_AC0Mod_three).

• Exponentially small correlation (Correlation.eventually_correlation_hardForm_le): fan-in-two circuits over any basis with at most c n gates of positive arity, for any c < 1 + π/(6 arccos((1 + 2√2)/4)) ≈ 2.78, have correlation 2^{-Ω(n)} with an explicit family of bilinear forms over GF(2), by Lindsey's lemma on the rectangles of the frontier method.

Module structure

Public modules (definitions a reviewer should read):

• Complexitylib.Circuits.Basis.Defs — BitString, BoolFunFamily, Arity, Basis, and a basis as a CSLib signature (Basis.GateKind, Basis.signature, Basis.interpretation)
• Complexitylib.Circuits.Typed.Defs — Gate, Circuit, eval, wireDepth, depth, size, CompleteBasis
• Complexitylib.Circuits.Basic — Realizable, sizeComplexityWithTop, sizeComplexity; re-exports Basis.Defs and Typed.Defs
• Complexitylib.Circuits.BitString — canonical bridges between BitString n and List Bool
• Complexitylib.Circuits.Composition — serial circuit composition with exact additive size, exact semantics, and additive depth
• Complexitylib.Circuits.OracleInlining — exact one-step adaptive oracle replacement with explicit size accounting
• Complexitylib.Circuits.OracleInlining.Adaptive — fixed-round adaptive oracle programs and exact compilation to ordinary circuits
• Complexitylib.Circuits.Dependency — the finite circuit dependency DAG, its canonical topological order, and its edge bound by total fan-in
• Complexitylib.Circuits.DecisionTree.Restriction — semantic restriction with nonincreasing decision-tree depth
• Complexitylib.Circuits.DecisionTree.Finite — arity-indexed decision trees with exact finite restriction semantics
• Complexitylib.Circuits.DecisionTree.NormalForm — exact decision-tree compilation to CNF and DNF with depth-controlled width
• Complexitylib.Circuits.RandomRestriction — the finite sparse-restriction sample space with exact cardinalities
• Complexitylib.Circuits.Spira — finite nonuniform formula balancing with explicit logarithmic-depth and polynomial-size bounds
• Complexitylib.Circuits.CircuitFormula — exact selected-output unfolding from fan-in-two circuit DAGs to Boolean formulas, with a factor-two depth bound
• Complexitylib.Circuits.FormulaEncoding — canonical iterative postfix formula codec with exact round trips and code length
• Complexitylib.Circuits.CircuitFormula.Family — family-level unfolding and the typed-NC1 bridge to width-5 branching programs
• Complexitylib.Circuits.Family — circuit families, list semantics, pointwise size/depth bounds, and the polynomial-size characterization
• Complexitylib.Circuits.BarringtonConverse — balanced branching-program evaluation and the explicitly total-assignment equivalence
• Complexitylib.Circuits.BarringtonTyped — variable-bounded fixed-arity formula/program families and the typed nonuniform Barrington equivalence
• Complexitylib.Circuits.BarringtonCompiler — executable finite S₅ search and formula-to-program compilation with the 4 ^ depth bound
• Complexitylib.Circuits.BranchingProgramEncoding — canonical seven-bit permutation ranks, instruction/program codecs, and exact size bounds
• Complexitylib.Circuits.BarringtonCodeGenerator — the total bitstring-level formula-code-to-program-code target for the remaining FL implementation
• Complexitylib.Circuits.Encoding — canonical proof-free encoding, validation, and iterative evaluation of fan-in-two AND/OR circuits
• Complexitylib.Circuits.Encoding.Family — tagged encoding and evaluation at every input length, including the explicit empty-input answer
• Complexitylib.Circuits.Encoding.Machine — total linear-time validation and tape staging plus the verified end-to-end quadratic serialized circuit-family evaluator
• Complexitylib.Circuits.Encoding.Machine.NatCode — framed, one-way terminated-unary natural-code emission from a preserved binary value, with reusable zero scratch and explicit time/all-prefix-space bounds
• Complexitylib.Circuits.AndOrNot.Defs — AndOrOp, Basis.unboundedAndOr, Basis.boundedAndOr, Basis.andOr2
• Complexitylib.Circuits.AndOrNot — functional completeness and a semantic, total-fan-in size bound for compiling unbounded AND/OR to fan-in two
• Complexitylib.Circuits.AndOrMod.Defs — AndOrModOp, Basis.unboundedAndOrMod (unbounded AND, OR, and MOD_m gates)
• Complexitylib.Circuits.BasisHom — exact semantics-, size-, depth-, and topology-preserving circuit transport between compatible bases
• Complexitylib.Circuits.Threshold — unweighted threshold gates, strict majority, and exact unbounded-AND/OR simulation
• Complexitylib.Circuits.Threshold.Parity — depth-two threshold circuits for parity and parity in TC0
• Complexitylib.Circuits.Monotone — typed monotone formulas, locality, monotonicity, and essential-input leaf lower bounds
• Complexitylib.Circuits.KarchmerWigderson — rectangle-indexed deterministic protocols and the depth-exact monotone formula correspondence
• Complexitylib.Circuits.NormalForm.Defs — Literal, CNF, DNF, clause/term count, and width
• Complexitylib.Circuits.NormalForm — CNF/DNF lower bound for XOR (two_pow_le_complexity_of_xorBool)
• Complexitylib.Circuits.NormalForm.Operations — semantic negation, conjunction, and disjunction operations on CNFs and DNFs
• Complexitylib.Circuits.NormalForm.Restriction — semantic CNF/DNF simplification with nonincreasing width and clause/term count
• Complexitylib.Circuits.XOR — Schnorr.xorBool (N-input parity)
• Complexitylib.Circuits.EssentialInput — IsEssentialInput, essentialInputs
• Complexitylib.Circuits.DepthClasses — DEPTH, the nonuniform NC, AC, ACMod, and TC hierarchies, and the aliases NC0, NC1, AC0, AC0Mod, and TC0
• Complexitylib.Circuits.AC0 — the AC0 class plus finite nonuniform negation-normal formulas, circuit normalization, exact restrictions, width-sensitive switching, finite staged iteration, the exact parity counting obstruction, parity outside AC0, and AC0 ⊂ TC0
• Complexitylib.Circuits.Smolensky.Defs — Smolensky.monomial and Smolensky.lowDegree, low-degree functions {0,1}^n → ZMod 3
• Complexitylib.Circuits.Correlation.Defs — Correlation.correlation, quadratic forms over GF(2) (Correlation.quadForm, Correlation.bilinForm), block and cut ranks, and submatrix-robust matrices
• Complexitylib.Circuits.Nondeterminism.Defs — existsQuantify, forallQuantify
• Complexitylib.Circuits.Hardwiring — exact-size prefix hardwiring
• Complexitylib.Circuits.Unrolling — bounded machine-configuration layouts, initialization, verified trace tiling, typed acceptance circuits, exact-size fixed-choice hardwiring, and parallel strict-majority amplification

Theorem modules (re-export definitions + main results):

• Complexitylib.Circuits.AndOrNot — functional completeness of AND/OR
• Complexitylib.Circuits.Shannon — Shannon counting lower bound
• Complexitylib.Circuits.Shallow — the Lecomte--Ramakrishnan shallow-circuit upper bound for symmetric functions, directly in CSLib's circuit model
• Complexitylib.Circuits.LowerBound — gate elimination lower bound
• Complexitylib.Circuits.Frontier — the frontier method: circuit lower bounds from graph layouts over any finite alphabet, basis, and fan-in
• Complexitylib.Circuits.Correlation — exponentially small correlation of fan-in-two circuits with fewer than 2.78 n gates with explicit quadratic forms over GF(2)
• Complexitylib.Circuits.Schnorr — Schnorr's XOR lower bound
• Complexitylib.Circuits.Smolensky — the Razborov–Smolensky lower bound for AC0[3]
• Complexitylib.Circuits.Nondeterminism — nondeterministic quantification complexity bounds
• Complexitylib.Circuits.Valiant — Valiant's depth reduction lemma for digraphs
• Complexitylib.Circuits.StraightLine — typed circuits as CSLib straight-line programs, with the same function and size

Internal modules contain proof machinery (CircDesc, DNF construction, restriction/elimination arguments) and are not intended for direct use.