Natural-valued circuit complexity on a support

Convenient forms of the support-complexity calculus over complete bases, including a bound obtained by synthesizing the output coordinates separately.

theorem Cslib.Circuits.complexityOn_le_of_computesOn {σ : Signature} {U : Type} {n m : ℕ} {I : Interpretation σ U} [I.IsComplete] {s : Set (Fin n → U)} {f : (Fin n → U) → Fin m → U} (c : Circuit σ n m) (hc : c.ComputesOn I s f) : complexityOn I s f ≤ c.size

A circuit correct on the support bounds its natural-valued complexity.

theorem Cslib.Circuits.exists_computesOn_size_eq_complexityOn {σ : Signature} {U : Type} {n m : ℕ} {I : Interpretation σ U} [I.IsComplete] {s : Set (Fin n → U)} {f : (Fin n → U) → Fin m → U} : ∃ (c : Circuit σ n m), c.ComputesOn I s f ∧ c.size = complexityOn I s f

The minimum size of a circuit correct on a support is attained.

theorem Cslib.Circuits.complexityOn_congr {σ : Signature} {U : Type} {n m : ℕ} {I : Interpretation σ U} [I.IsComplete] {s : Set (Fin n → U)} {f g : (Fin n → U) → Fin m → U} (h : Set.EqOn f g s) : complexityOn I s f = complexityOn I s g

Equal targets on the required support have equal complexity.

@[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.