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.Program.card_biUnion_wireSupport_le_cost: supporting inputs are bounded by the frontier size plus the program cost under any weight bounding arities by 1 + w op.
• 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.
• Cslib.Circuits.Program.FanInAtMost.mono, Cslib.Circuits.Circuit.FanInAtMost.mono: fan-in bounds are monotone in the bound.
• Cslib.Circuits.Program.FanInAtMost.append, Cslib.Circuits.Circuit.FanInAtMost.comp, Cslib.Circuits.Circuit.FanInAtMost.append: fan-in bounds of composed programs and circuits.
• Cslib.Circuits.Circuit.fanInAtMost_pi: single-output circuits side by side keep a common fan-in bound.

theorem Cslib.Circuits.Wire.castSucc_injective {n g : ℕ} : Function.Injective castSucc

Embedding a wire into a widened program by Wire.castSucc is injective.

theorem Cslib.Circuits.Program.card_biUnion_wireSupport_le_cost {σ : Signature} {n g : ℕ} (program : Program σ n g) (w : σ.Op → ℕ) (hw : ∀ (op : σ.Op), σ.Arity op ≤ 1 + w op) (frontier : Finset (Wire n g)) : (frontier.biUnion program.wireSupport).card ≤ frontier.card + program.cost w

The inputs supporting a frontier of wires in a program are bounded by the size of the frontier plus the cost of the program, for any weight function that bounds gate arities by 1 + w op.

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.

Composition

theorem Cslib.Circuits.Program.FanInAtMost.mono {σ : Signature} {n g : ℕ} {p : Program σ n g} {r s : ℕ} (h : p.FanInAtMost r) (hrs : r ≤ s) : p.FanInAtMost s

A fan-in bound holds for every larger bound.

theorem Cslib.Circuits.Program.FanInAtMost.append {σ : Signature} {n k g₁ g₂ r : ℕ} {p : Program σ n g₁} {feed : Fin k → Wire n g₁} {q : Program σ k g₂} (hp : p.FanInAtMost r) (hq : q.FanInAtMost r) : (p.append feed q).FanInAtMost r

Continuing a program by another keeps a common fan-in bound.

theorem Cslib.Circuits.Circuit.FanInAtMost.mono {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {r s : ℕ} (h : c.FanInAtMost r) (hrs : r ≤ s) : c.FanInAtMost s

A fan-in bound of a circuit holds for every larger bound.

theorem Cslib.Circuits.Circuit.FanInAtMost.comp {σ : Signature} {n m p : ℕ} {d : Circuit σ m p} {c : Circuit σ n m} {r : ℕ} (hd : d.FanInAtMost r) (hc : c.FanInAtMost r) : (d.comp c).FanInAtMost r

Sequential composition keeps a common fan-in bound.

theorem Cslib.Circuits.Circuit.FanInAtMost.append {σ : Signature} {n m p : ℕ} {c : Circuit σ n m} {d : Circuit σ n p} {r : ℕ} (hc : c.FanInAtMost r) (hd : d.FanInAtMost r) : (c.append d).FanInAtMost r

Parallel composition keeps a common fan-in bound.

theorem Cslib.Circuits.Circuit.fanInAtMost_pi {σ : Signature} {n m r : ℕ} {cs : Fin m → Circuit σ n 1} (h : ∀ (j : Fin m), (cs j).FanInAtMost r) : (pi cs).FanInAtMost r

Single-output circuits side by side keep a common fan-in bound.