Size lower bounds from bounded fan-in

Unfolding a frontier through a bounded-fan-in program controls how many original inputs can reach the outputs. Essential inputs therefore give a lower bound on circuit size.

Main results

• Cslib.Circuits.Circuit.card_inputSupport_le_size: a circuit of fan-in r with m outputs has at most m + (r - 1) size supporting inputs.
• Cslib.Circuits.Circuit.essential_le_size: the same bound for essential inputs of the computed function.
• Cslib.Circuits.Circuit.card_inputSupport_le_depth, Cslib.Circuits.Circuit.essential_le_depth: at depth d, an output of a circuit of fan-in r depends on at most r ^ d inputs.

theorem Cslib.Circuits.Circuit.card_inputSupport_le_size {σ : Signature} {n m : ℕ} (c : Circuit σ n m) {r : ℕ} (bounded : c.FanInAtMost r) : c.inputSupport.card ≤ m + (r - 1) * c.size

A fan-in-r circuit has at most m + (r - 1) * c.size supporting inputs.

theorem Cslib.Circuits.Circuit.essential_le_size {σ : Signature} {U : Type u_1} {n m : ℕ} (c : Circuit σ n m) {interpretation : Interpretation σ U} {target : (Fin n → U) → Fin m → U} {selected : Finset (Fin n)} {r : ℕ} (computes : c.Computes interpretation target) (essential : ∀ k ∈ selected, EssentialAt target k) (bounded : c.FanInAtMost r) : selected.card ≤ m + (r - 1) * c.size

If a circuit has fan-in at most r, computes target, and every input in selected is essential to target, then selected has at most m + (r - 1) * c.size elements.

Depth

theorem Cslib.Circuits.Program.card_wireSupport_le_pow {σ : Signature} {n r g : ℕ} {p : Program σ n g} : p.FanInAtMost r → ∀ (w : Wire n g), (p.wireSupport w).card ≤ max 1 r ^ p.wireDepths w

In a program of fan-in r, a wire of depth d is supported by at most max 1 r ^ d inputs.

theorem Cslib.Circuits.Circuit.card_inputSupport_le_depth {σ : Signature} {n m : ℕ} (c : Circuit σ n m) {r : ℕ} (hc : c.FanInAtMost r) : c.inputSupport.card ≤ m * max 1 r ^ c.depth

A circuit of fan-in r with m outputs and depth d has at most m (max 1 r) ^ d supporting inputs.

theorem Cslib.Circuits.Circuit.essential_le_depth {σ : Signature} {U : Type u_1} {n m : ℕ} (c : Circuit σ n m) {I : Interpretation σ U} {target : (Fin n → U) → Fin m → U} {selected : Finset (Fin n)} {r : ℕ} (hc : c.Computes I target) (h : ∀ k ∈ selected, EssentialAt target k) (hr : c.FanInAtMost r) : selected.card ≤ m * max 1 r ^ c.depth

If a circuit of fan-in r and depth d computes target, and every input in selected is essential to target, then selected has at most m (max 1 r) ^ d elements.