Wire accounting and shared gates

For a circuit with no unused gates, let w count original input occurrences and let e sum each gate's uses beyond its first. Double counting gives w + e + size = totalFanIn + outputCount. Thus a binary single-output circuit satisfies w + e = size + 1. Every shared gate contributes at least one to e, so w + sharedGates.card ≤ size + 1 as well.

Uses include designated outputs and count repeated gate arguments separately. No assumption of distinct arguments, Boolean values, positive input count, or gated outputs is needed. The no-unused-gates hypothesis is essential to the balance equation: an unused gate has no first use to subtract.

These generic extensions of CSLib's circuit model are candidates for upstreaming. They count structural sharing, without assigning a semantic or communication cost to a shared gate.

theorem Cslib.Circuits.Circuit.wire_use_balance {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (used : c.NoUnusedGates) : c.inputUses + c.excessFanout + c.size = c.totalFanIn + m

Exact wire-use accounting for a circuit without unused gates.

theorem Cslib.Circuits.Circuit.card_sharedGates_le_excessFanout {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : c.sharedGates.card ≤ c.excessFanout

Each shared gate contributes at least one use beyond its first.

theorem Cslib.Circuits.Circuit.inputUses_add_excessFanout_eq {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (used : c.NoUnusedGates) (binary : ∀ (j : Fin c.size), σ.Arity (c.program.lines j).op = 2) : c.inputUses + c.excessFanout = c.size + m

Exact binary fan-in turns wire accounting into w + e = size + outputCount.

theorem Cslib.Circuits.Circuit.inputUses_add_excessFanout_le {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (used : c.NoUnusedGates) (bounded : c.FanInAtMost 2) : c.inputUses + c.excessFanout ≤ c.size + m

Fan-in at most two bounds input occurrences plus excess gate uses.

theorem Cslib.Circuits.Circuit.inputUses_add_card_sharedGates_le {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (used : c.NoUnusedGates) (bounded : c.FanInAtMost 2) : c.inputUses + c.sharedGates.card ≤ c.size + m

In fan-in-two circuits, shared gates consume the same budget as input occurrences.