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 Complexitylib.Circuits.Internal.Bridge.

Gate and Circuit Descriptors

@[reducible, inline]

abbrev Complexity.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

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

@[reducible, inline]

abbrev Complexity.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

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

def Complexity.CircDesc.Ordered {N s : ℕ} (d : CircDesc N s) : Prop

A descriptor is ordered when every gate only references primary inputs or strictly earlier gates. For gate i, those are exactly the wires with indices below N + i.

Equations

• d.Ordered = ∀ (i : Fin s), ↑(d i).2.1.1 < N + ↑i ∧ ↑(d i).2.1.2 < N + ↑i

Wire and Circuit Evaluation

@[irreducible]

def Complexity.CircDesc.wireVal {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 Complexity.CircDesc.eval {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

• Complexity.CircDesc.eval hs d input = d.wireVal input ⟨N + s - 1, ⋯⟩

Cardinality Lemmas

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

There are exactly 8 * W² gate slots over W wires: a choice of gate type (AND/OR), two input wires, and two negation flags.

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

There are exactly (8 * (N + s)²)^s circuit descriptors with N inputs and s gates: each of the s gates independently picks a slot over N + s wires.

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

There are exactly 2^(2^N) Boolean functions on N input bits.

Arithmetic Lemmas

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

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

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

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

theorem Complexity.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 Complexity.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 Complexity.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 Complexity.shannon_lower_bound (N : ℕ) (hN : 6 ≤ N) : ∃ (f : BitString N → Bool), ∀ (d : CircDesc N (2 ^ N / (5 * N))), CircDesc.eval ⋯ 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).