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 Circ.EssentialInput. The public theorems (gate_elimination_lower_bound, lower_bound_all_inputs) are accessible through Circ.LowerBound.

Core insensitivity lemma

theorem CircuitComplexity.Circuit.wireValue_eq_of_unreferenced {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) (i : Fin N) (b : Bool) (hno : ∀ (g : Fin G) (k : Fin (c.gates g).fanIn), ↑((c.gates g).inputs k) ≠ ↑i) (x : BitString N) (w : Fin (N + G)) (hw : ↑w ≠ ↑i) : c.wireValue x w = c.wireValue (Function.update x i b) w

If no internal gate reads primary input i, wire values at wires other than i are unchanged when input i is modified.

theorem CircuitComplexity.Circuit.eval_eq_of_unreferenced {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) (i : Fin N) (b : Bool) (hno_gates : ∀ (g : Fin G) (k : Fin (c.gates g).fanIn), ↑((c.gates g).inputs k) ≠ ↑i) (hno_outputs : ∀ (j : Fin M) (k : Fin (c.outputs j).fanIn), ↑((c.outputs j).inputs k) ≠ ↑i) (x : BitString N) : c.eval x = c.eval (Function.update x i b)

If no gate (internal or output) reads primary input i, the circuit output is unchanged when input i is modified.

Essential variables must be read

theorem CircuitComplexity.Circuit.exists_gate_reads_input {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) (f : BitString N → BitString M) (hf : c.eval = f) (i : Fin N) (hdep : IsEssentialInput f i) : (∃ (g : Fin G) (k : Fin (c.gates g).fanIn), ↑((c.gates g).inputs k) = ↑i) ∨ ∃ (j : Fin M) (k : Fin (c.outputs j).fanIn), ↑((c.outputs j).inputs k) = ↑i

If c computes f and f depends on variable i, some gate (internal or output) directly reads input wire i.

Counting argument

def CircuitComplexity.Circuit.coveredInputs {B : Basis} {N G : ℕ} (g : Gate B (N + G)) : Finset (Fin N)

The set of primary inputs directly wired into a gate.

Equations

• CircuitComplexity.Circuit.coveredInputs g = {i : Fin N | ∃ (k : Fin g.fanIn), ↑(g.inputs k) = ↑i}

theorem CircuitComplexity.Circuit.mem_coveredInputs {B : Basis} {N G : ℕ} (g : Gate B (N + G)) (i : Fin N) : i ∈ coveredInputs g ↔ ∃ (k : Fin g.fanIn), ↑(g.inputs k) = ↑i

theorem CircuitComplexity.Circuit.card_coveredInputs_le {B : Basis} {N G : ℕ} [NeZero N] (g : Gate B (N + G)) : (coveredInputs g).card ≤ g.fanIn

theorem CircuitComplexity.Circuit.boundedAON_coveredInputs_card_le {N G : ℕ} [NeZero N] {k : ℕ} (g : Gate (Basis.boundedAON k) (N + G)) : (coveredInputs g).card ≤ k

For a gate over bounded fan-in k AON basis, covered inputs has card ≤ k.

theorem CircuitComplexity.Circuit.essential_inputs_le_mul_size {N M G : ℕ} [NeZero N] [NeZero M] {k : ℕ} (c : Circuit (Basis.boundedAON k) N M G) (f : BitString N → BitString M) (hf : c.eval = f) : (EssentialInputs f).card ≤ k * c.size

Counting bound: for bounded fan-in k, the number of essential variables is at most k times the circuit size.

theorem CircuitComplexity.Circuit.gate_elimination_lower_bound {N M G : ℕ} [NeZero N] [NeZero M] {k : ℕ} (c : Circuit (Basis.boundedAON k) N M G) (f : BitString N → BitString M) (hf : c.eval = f) : (EssentialInputs f).card ≤ k * c.size

Gate elimination lower bound: for fan-in k, circuit size is at least ⌈n'/k⌉ where n' is the number of essential variables.

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

Corollary: if f depends on all N inputs, then N ≤ k · size.