Internal: Gate Elimination Lower Bound

This internal module proves the gate elimination lower bound: for any circuit over a bounded fan-in k AND/OR basis, if the computed function depends on n' essential variables, the circuit has size at least ⌈n'/k⌉.

The public definitions (IsEssentialInput, essentialInputs) are in Complexitylib.Circuits.EssentialInput. The public theorems (card_essentialInputs_le_mul_size, le_mul_size_of_forall_isEssentialInput) are stated in Complexitylib.Circuits.LowerBound.

Core insensitivity lemma

Essential variables must be read

Counting argument

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

Generic counting bound: every essential variable consumes at least one gate-input occurrence, so their number is bounded by total fan-in.

theorem Complexity.Circuit.le_totalFanIn_of_forall_isEssentialInput_internal {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (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 every input is essential, total fan-in is at least the input arity.

theorem Complexity.Circuit.card_essentialInputs_le_mul_size_internal {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

Bounded-fan-in corollary: the number of essential variables is at most k times circuit size.

theorem Complexity.Circuit.le_mul_size_of_forall_isEssentialInput_internal {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 every input is essential in the bounded-fan-in setting, then N ≤ k * size.