Shannon Bounds

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 (Circuit.size, which is G + 1 for a single-output circuit with G internal gates) at most ⌊2^N / (5N)⌋.

The proof proceeds by a counting (pigeonhole) argument: the number of distinct circuits of a given size is strictly less than the number of Boolean functions, so some function must be hard.

Main results

The main theorem is shannon_lower_bound_circuit:

theorem shannon_lower_bound_circuit (N : Nat) [NeZero N] (hN : 6 ≤ N) :
    ∃ f : BitString N → Bool,
      ∀ G (c : Circuit Basis.andOr2 N 1 G),
        c.size ≤ 2 ^ N / (5 * N) →
        (fun x => (c.eval x) 0) ≠ f

The statement uses the library's total Circuit.size; for a single-output circuit this is G + 1.

Since Basis.andOr2 is complete (the CompleteBasis Basis.andOr2 instance of Complexitylib.Circuits.AndOrNot, imported here), this yields a sizeComplexity bound via shannon_sizeComplexity.

• shannon_upper_bound — for N ≥ 16, every Boolean function on N inputs has sizeComplexity at most ⌊18 · 2^N / N⌋.

Together these establish that worst-case circuit complexity is Θ(2^N / N).

theorem Complexity.shannon_lower_bound_circuit (N : ℕ) [NeZero N] (hN : 6 ≤ N) : ∃ (f : BitString N → Bool), ∀ (G : ℕ) (c : Circuit Basis.andOr2 N 1 G), c.size ≤ 2 ^ N / (5 * N) → (fun (x : BitString N) => c.eval x 0) ≠ f

Shannon lower bound for circuits: for N ≥ 6, there exists a Boolean function on N inputs that cannot be computed by any fan-in-two AND/OR circuit of total size at most 2^N / (5N).

For a single-output circuit, c.size = G + 1.

theorem Complexity.shannon_sizeComplexity (N : ℕ) [NeZero N] (hN : 6 ≤ N) : ∃ (f : BitString N → Bool), Circuit.sizeComplexity Basis.andOr2 f > 2 ^ N / (5 * N)

Shannon lower bound in terms of sizeComplexity: for N ≥ 6, there exists a Boolean function whose fan-in-2 AND/OR circuit complexity exceeds 2^N / (5N).

theorem Complexity.shannon_upper_bound (N : ℕ) (hN : 16 ≤ N) [NeZero N] (f : BitString N → Bool) : Circuit.sizeComplexity Basis.andOr2 f ≤ 18 * 2 ^ N / N

Shannon upper bound: for N ≥ 16, every Boolean function on N inputs has fan-in-2 AND/OR circuit complexity at most 18 · 2^N / N.

Combined with shannon_sizeComplexity, this gives Θ(2^N / N).

This is the full-column-library variant (C = 18). The tighter (1 + o(1)) · 2^N / N bound due to Lupanov (1958) is Complexity.lupanov_sizeComplexity in Complexitylib.Interop.Cslib.Circuit, transferred from CSLib.