Shannon's circuit-size lower bound

DefinitionWire count of a flat circuit#✓fully proved

The wire count of a flat Boolean circuit on \(n\) inputs, given as a list of gates, is the sum over its gates of the lengths of their predecessor lists: every reference of a gate to a gate index is counted, with multiplicity, while input variables and constants contribute nothing and the modulus of a mod gate is not counted.

def wireCount {n : ℕ} (C : List (ACGate n)) : ℕ :=
  (C.map gateInputs).flatten.length

Uses 2 · Used by 1

Statement usesGates of a flat Boolean circuit · Predecessors of a gate

Used byShannon: most Boolean functions need exponential circuits

TheoremShannon: most Boolean functions need exponential circuits#●ready to prove

For every natural number \(n \ge 10\), at least \(2^{2^n}/2\) of the Boolean functions \(f\) on \(n\) input bits have the following property: for every well-formed flat Boolean circuit \(C\) on \(n\) inputs without mod gates whose wire count (the total length of the predecessor lists of its gates) is at most \(\lfloor 2^n / (10 n) \rfloor\), there is an input \(x \in \{0,1\}^n\) such that \(C\) has no gates or the value of the last gate of \(C\) on \(x\) differs from \(f(x)\).

public theorem_wanted shannon_hard_function :
    ∀ n : ℕ, 10 ≤ n →
      (Set.ncard {f : (Fin n → Bool) → Bool | ∀ C : List (ACGate n),
        WellFormedCircuit C → IsModFree C → wireCount C ≤ 2 ^ n / (10 * n) →
          ∃ x : Fin n → Bool, (circuitEval C x).getLast? ≠ some (f x)} ≥
        2 ^ (2 ^ n) / 2)

Sources

• C. E. Shannon, "The synthesis of two-terminal switching circuits", Bell System Technical Journal 28 (1949), 59-98.

Uses 5

Statement usesGates of a flat Boolean circuit · Circuits without mod gates · Well-formed flat circuits · Evaluation of a flat Boolean circuit · Wire count of a flat circuit

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.