Internal: Circuit Descriptors and Shannon Counting Bound

This internal module defines the circuit descriptor model used for counting arguments, and proves the Shannon lower bound for this model. The public theorem shannon_lower_bound_circuit (which speaks in terms of Circuit) is in Circ.Internal.Bridge.

Gate and Circuit Descriptors

@[reducible, inline]

abbrev CircuitComplexity.GateSlot (W : ℕ) : Type

A gate in a fan-in-2 circuit over wires 0..W-1. Encodes (isAnd, (wire1, wire2), (neg1, neg2)). Semantics: if isAnd then (neg1 ⊕ v1) && (neg2 ⊕ v2) else (neg1 ⊕ v1) || (neg2 ⊕ v2)

Equations

• CircuitComplexity.GateSlot W = (Bool × (Fin W × Fin W) × Bool × Bool)

@[reducible, inline]

abbrev CircuitComplexity.CircDesc (N s : ℕ) : Type

A circuit descriptor with N primary inputs and s gates. Wires 0..N-1 are primary inputs; wires N..N+s-1 are gate outputs.

Equations

• CircuitComplexity.CircDesc N s = (Fin s → CircuitComplexity.GateSlot (N + s))

Wire and Circuit Evaluation

@[irreducible]

def CircuitComplexity.wireValD {N s : ℕ} (d : CircDesc N s) (input : BitString N) (w : Fin (N + s)) : Bool

Evaluate wire w in a circuit descriptor. Primary input wires return the corresponding input bit. Gate wires evaluate their gate, with forward references defaulting to false.

Equations

• One or more equations did not get rendered due to their size.

def CircuitComplexity.evalD {N s : ℕ} (hs : 0 < s) (d : CircDesc N s) : BitString N → Bool

Evaluate a circuit descriptor: the output is the value of the last gate.

Equations

• CircuitComplexity.evalD hs d input = CircuitComplexity.wireValD d input ⟨N + s - 1, ⋯⟩

Cardinality Lemmas

theorem CircuitComplexity.card_gateSlot (W : ℕ) : Fintype.card (GateSlot W) = 8 * W ^ 2

theorem CircuitComplexity.card_circDesc (N s : ℕ) : Fintype.card (CircDesc N s) = (8 * (N + s) ^ 2) ^ s

theorem CircuitComplexity.card_bool_fun (N : ℕ) : Fintype.card (BitString N → Bool) = 2 ^ 2 ^ N

Arithmetic Lemmas

theorem CircuitComplexity.five_n_le_two_pow (N : ℕ) (hN : 6 ≤ N) : 5 * N ≤ 2 ^ N

For N ≥ 6, the exponential 2^N dominates 5N.

theorem CircuitComplexity.s_pos (N : ℕ) (hN : 6 ≤ N) : 0 < 2 ^ N / (5 * N)

The gate count s = 2^N / (5N) is positive for N ≥ 6.

theorem CircuitComplexity.n_plus_s_lt (N : ℕ) (hN : 6 ≤ N) : N + 2 ^ N / (5 * N) < 2 ^ N

The total wire count N + s is less than 2^N.

theorem CircuitComplexity.mul_s_lt_two_pow (N : ℕ) (hN : 6 ≤ N) : (2 * N + 3) * (2 ^ N / (5 * N)) < 2 ^ N

The exponent (2N+3) * s is less than 2^N, which ensures the power-of-two bound in the main arithmetic inequality.

theorem CircuitComplexity.arith_bound (N : ℕ) (hN : 6 ≤ N) : (8 * (N + 2 ^ N / (5 * N)) ^ 2) ^ (2 ^ N / (5 * N)) < 2 ^ 2 ^ N

Key arithmetic bound: the number of circuit descriptors of size s = 2^N/(5N) is strictly less than the number of Boolean functions on N inputs. The proof chains:

1. N + s < 2^N
2. 8(N+s)² < 2^(2N+3)
3. (2N+3)·s < 2^N
4. (2^(2N+3))^s = 2^((2N+3)·s) < 2^(2^N)

Main Theorem

theorem CircuitComplexity.shannon_lower_bound (N : ℕ) (hN : 6 ≤ N) : ∃ (f : BitString N → Bool), ∀ (d : CircDesc N (2 ^ N / (5 * N))), evalD ⋯ d ≠ f

Shannon counting lower bound: for N ≥ 6, there exists a Boolean function on N inputs that cannot be computed by any fan-in-2 circuit descriptor with at most 2^N / (5N) gates.

This is a formalization of Shannon's 1949 counting argument, which shows that most Boolean functions require circuits of size at least 2^N / (5N).