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.

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} {n m : ℕ} {U : Type u_2} (c : Circuit σ n m) {interpretation : Interpretation σ U} {target : (Fin n → U) → Fin m → U} {selected : Finset (Fin n)} {r : ℕ} (computes : c.ComputesWith interpretation target) (essential : ∀ k ∈ selected, Algebraic.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.