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 accessible through Complexitylib.Circuits.LowerBound.

Core insensitivity lemma

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

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

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

Membership in coveredInputs: input i is covered by gate g iff some fan-in wire of g is the primary input wire i.

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

A gate covers at most fanIn-many primary inputs.

theorem Complexity.Circuit.card_coveredInputs_le_of_boundedAndOr {N G : ℕ} [NeZero N] {k : ℕ} (g : Gate (Basis.boundedAndOr k) (N + G)) : (coveredInputs g).card ≤ k

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

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

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

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

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