Arity profiles for circuit counting

This file records the basis information used by closed-form counting bounds. The exact counting theorems remain independent of these estimates.

def Cslib.Circuits.Signature.ArityAtMost (σ : Signature) (r : ℕ) : Prop

Every symbol in a signature has arity at most r.

Equations

• σ.ArityAtMost r = ∀ (op : σ.Op), σ.Arity op ≤ r

structure Cslib.Circuits.Signature.HasMaximumArity (σ : Signature) (r : ℕ) : Prop

The finite signature has maximum arity exactly r. Packaging the upper bound and an operation attaining it gives the closed Shannon theorem a natural basis-level hypothesis.

• arity_le : σ.ArityAtMost r

  No primitive operation has arity greater than r.

• attained : ∃ (op : σ.Op), σ.Arity op = r

  Some primitive operation has arity r.

theorem Cslib.Circuits.Signature.lineCount_le_card_mul_pow (σ : Signature) [Fintype σ.Op] {r : ℕ} (arity : σ.ArityAtMost r) (w : ℕ) : σ.lineCount w ≤ Fintype.card σ.Op * (w + 1) ^ r

Arity-only upper bound for the number of lines. The successor on w handles zero wires and nullary operations uniformly.

theorem Cslib.Circuits.Signature.lineCount_mono (σ : Signature) [Fintype σ.Op] : Monotone σ.lineCount

The number of available lines is monotone in the number of wires.

theorem Cslib.Circuits.Signature.HasMaximumArity.wires_le_lineCount {σ : Signature} [Fintype σ.Op] {r : ℕ} (maximum : σ.HasMaximumArity r) (positive : 0 < r) (w : ℕ) : w ≤ σ.lineCount w

A signature with a positive maximum arity has at least as many possible lines as available wires.