Gate Elimination Lower Bound

For every circuit, the number of essential input variables is at most its total fan-in. For a bounded fan-in k AND/OR basis (Basis.boundedAndOr k), this is at most k times circuit size.

The key insight: if no gate directly reads a primary input wire, then that input cannot influence the circuit's output. By contrapositive, every essential variable must be "covered" by at least one gate. Since each gate reads at most k inputs, the circuit needs at least ⌈n'/k⌉ gates.

Definitions (from Complexitylib.Circuits.EssentialInput)

• IsEssentialInput f i — function f depends on input variable i (flipping bit i can change some output)
• essentialInputs f — the Finset of all essential input variables

Main results

The generic theorem is Circuit.card_essentialInputs_le_totalFanIn; its bounded-fan-in corollary is Circuit.card_essentialInputs_le_mul_size:

theorem Circuit.card_essentialInputs_le_mul_size {k : Nat}
    (c : Circuit (Basis.boundedAndOr k) N M G)
    (f : BitString N → BitString M)
    (hf : c.eval = f) :
    (essentialInputs f).card ≤ k * c.size

And its corollary for functions that depend on all inputs:

theorem Circuit.le_mul_size_of_forall_isEssentialInput {k : Nat}
    (c : Circuit (Basis.boundedAndOr k) N M G)
    (f : BitString N → BitString M)
    (hf : c.eval = f)
    (hall : ∀ i : Fin N, IsEssentialInput f i) :
    N ≤ k * c.size

theorem Complexity.Circuit.card_essentialInputs_le_totalFanIn {N M G : ℕ} [NeZero N] [NeZero M] {B : Basis} (c : Circuit B N M G) (f : BitString N → BitString M) (hf : c.eval = f) : (essentialInputs f).card ≤ c.totalFanIn

Over any basis, the number of essential variables of a computed function is at most the circuit's total number of gate-input occurrences.

theorem Complexity.Circuit.le_totalFanIn_of_forall_isEssentialInput {N M G : ℕ} [NeZero N] [NeZero M] {B : Basis} (c : Circuit B N M G) (f : BitString N → BitString M) (hf : c.eval = f) (hall : ∀ (i : Fin N), IsEssentialInput f i) : N ≤ c.totalFanIn

If a function depends on every input, every circuit computing it has total fan-in at least N.

theorem Complexity.Circuit.card_essentialInputs_le_mul_size {N M G : ℕ} [NeZero N] [NeZero M] {k : ℕ} (c : Circuit (Basis.boundedAndOr k) N M G) (f : BitString N → BitString M) (hf : c.eval = f) : (essentialInputs f).card ≤ k * c.size

For bounded fan-in k, the number of essential variables of a computed function is at most k times the circuit's total gate count.

theorem Complexity.Circuit.le_mul_size_of_forall_isEssentialInput {N M G : ℕ} [NeZero N] [NeZero M] {k : ℕ} (c : Circuit (Basis.boundedAndOr k) N M G) (f : BitString N → BitString M) (hf : c.eval = f) (hall : ∀ (i : Fin N), IsEssentialInput f i) : N ≤ k * c.size

If a function computed by a bounded fan-in k circuit depends on every input, then N ≤ k * c.size.