Natural-valued circuit complexity on a support

Convenient forms of the support-complexity calculus over complete bases: an empty output family is free, and a bound obtained by synthesizing the output coordinates separately.

@[simp]

theorem Cslib.Circuits.complexityOn_empty {σ : Signature} {U : Type} {n : ℕ} {I : Interpretation σ U} [I.IsComplete] {s : Set (Fin n → U)} (f : (Fin n → U) → Fin 0 → U) : complexityOn I s f = 0

An empty output family needs no gates, on any support.

theorem Cslib.Circuits.complexityOn_le_sum {σ : Signature} {U : Type} {n m : ℕ} {I : Interpretation σ U} [I.IsComplete] {s : Set (Fin n → U)} (f : (Fin n → U) → Fin m → U) : complexityOn I s f ≤ ∑ j : Fin m, complexityOn I s fun (x : Fin n → U) (x_1 : Fin 1) => f x j

Separate scalar implementations can be combined without duplicating their inputs.