Double counting wire uses

theorem Cslib.Circuits.Circuit.card_wireUse {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : Fintype.card c.WireUse = c.totalFanIn + m

The number of wire-use occurrences is the total fan-in plus the output count.

theorem Cslib.Circuits.Circuit.sum_wireUses {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : ∑ w : Wire n c.size, c.wireUses w = c.totalFanIn + m

Every wire-use occurrence reads exactly one wire.

theorem Cslib.Circuits.Circuit.inputUses_add_sum_gate_uses {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : c.inputUses + ∑ j : Fin c.size, c.wireUses (Wire.gate j) = c.totalFanIn + m

Splitting the wires into inputs and gates preserves the total number of uses.

theorem Cslib.Circuits.Circuit.sum_gate_uses_eq {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (used : c.NoUnusedGates) : ∑ j : Fin c.size, c.wireUses (Wire.gate j) = c.excessFanout + c.size

Without unused gates, the first use of each gate accounts for exactly size uses.

theorem Cslib.Circuits.Circuit.totalFanIn_le_of_fanInAtMost {σ : Signature} {n m : ℕ} (c : Circuit σ n m) {r : ℕ} (bounded : c.FanInAtMost r) : c.totalFanIn ≤ r * c.size

Bounded fan-in bounds the total number of gate argument slots.