Coarse arity-only size bounds

These estimates trade the exact signature line count for a closed expression using only the number of primitive operations and their maximum arity.

def Cslib.Circuits.Signature.coarseBudget (σ : Signature) [Fintype σ.Op] (r n m G : ℕ) : ℕ

A simple closed budget depending only on signature size and maximum arity.

Equations

• σ.coarseBudget r n m G = (G + 1) * (1 + (n + G) + Fintype.card σ.Op * (n + G + 1) ^ r) ^ (G + m)

theorem Cslib.Circuits.Signature.sharpCount_le_coarseTerm (σ : Signature) [Fintype σ.Op] {r n m g G : ℕ} (arity : σ.ArityAtMost r) (bounded : g ≤ G) : σ.sharpCount n g m ≤ (1 + (n + G) + Fintype.card σ.Op * (n + G + 1) ^ r) ^ (G + m)

theorem Cslib.Circuits.Signature.sharpBudget_le_coarseBudget (σ : Signature) [Fintype σ.Op] {r n m G : ℕ} (arity : σ.ArityAtMost r) : σ.sharpBudget n m G ≤ σ.coarseBudget r n m G

theorem Cslib.Circuits.Circuit.card_functionsAtMost_le_coarseBudget {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) {r : ℕ} (arity : σ.ArityAtMost r) (n m G : ℕ) : (functionsAtMost interpretation n m G).card ≤ σ.coarseBudget r n m G

theorem Cslib.Circuits.Circuit.exists_hard_in_family_coarse {U : Type u_1} {σ : Signature} {n m G : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (family : Finset (Algebraic.Target U n m)) {r : ℕ} (arity : σ.ArityAtMost r) (large : σ.coarseBudget r n m G < family.card) : ∃ target ∈ family, GateHard interpretation G target