Counting functions computed by finite circuits over a complete basis

This module provides the complexity characterization of Cslib.Circuits.computableFunctions over a complete gate basis, complementing Cslib.Circuits.mem_computableFunctions_iff_ecomplexity_le.

Main results

• Cslib.Circuits.mem_computableFunctions_iff_complexity_le: over a complete basis, the scalar functions computable with at most s gates are those of complexity at most s.

theorem Cslib.Circuits.mem_computableFunctions_iff_complexity_le {σ : Signature} [Finite σ.Op] {U : Type u} {I : Interpretation σ U} [I.IsComplete] {n s : ℕ} {f : (Fin n → U) → U} : f ∈ computableFunctions I n s ↔ complexity I (single f) ≤ s

Over a complete basis, the functions computable with at most s gates are those of complexity at most s.