Nonuniform circuit families

Circuit lower bounds are finite statements about one input width, while complexity classes quantify over a sequence of circuits. This module supplies that missing bridge without fixing a gate basis.

A Circuit.Family sigma m chooses one m-output circuit for every input width. Its gate count at each width is the member circuit's size, so size agrees definitionally with the finite circuit model. Polynomial size and constant depth are expressed by exact natural-number bounds. The factor (n + 1) ^ degree makes the definition well behaved at input width zero and avoids burying finite-prefix adjustments inside asymptotic notation.

@[reducible, inline]

abbrev Algebraic.Target.Family (U : Type u) (m : ℕ) : Type u

An m-output target at every input width.

Equations

• Algebraic.Target.Family U m = ((n : ℕ) → Algebraic.Target U n m)

def Algebraic.Target.scalarFamily {U : Type u_1} (family : (n : ℕ) → ScalarFunction U n) : Family U 1

Regard a family of scalar functions as a one-output target family.

Equations

• Algebraic.Target.scalarFamily family n input x✝ = family n input

@[simp]

theorem Algebraic.Target.scalarFamily_apply {U : Type u_1} {n : ℕ} (family : (n : ℕ) → ScalarFunction U n) (input : Fin n → U) (output : Fin 1) : scalarFamily family n input output = family n input

def Cslib.Circuits.Circuit.Resource.PolynomiallyBounded (resource : ℕ → ℕ) : Prop

A natural-valued resource is bounded by one fixed polynomial.

The coefficient and degree do not depend on the input width. Using n + 1 gives an exact all-width statement equivalent to the usual eventual polynomial bound for natural-valued resources.

Equations

• Cslib.Circuits.Circuit.Resource.PolynomiallyBounded resource = ∃ (coefficient : ℕ) (degree : ℕ), ∀ (n : ℕ), resource n ≤ coefficient * (n + 1) ^ degree

def Cslib.Circuits.Circuit.Resource.ConstantlyBounded (resource : ℕ → ℕ) : Prop

A natural-valued resource is bounded by one constant at every width.

Equations

• Cslib.Circuits.Circuit.Resource.ConstantlyBounded resource = ∃ (bound : ℕ), ∀ (n : ℕ), resource n ≤ bound

def Cslib.Circuits.Circuit.Resource.EventuallyExceedsEveryPolynomial (resource : ℕ → ℕ) : Prop

A resource eventually strictly exceeds every fixed natural polynomial.

Equations

• Cslib.Circuits.Circuit.Resource.EventuallyExceedsEveryPolynomial resource = ∀ (coefficient degree : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, coefficient * (n + 1) ^ degree < resource n

theorem Cslib.Circuits.Circuit.Resource.PolynomiallyBounded.of_le {smaller larger : ℕ → ℕ} (bounded : PolynomiallyBounded larger) (comparison : ∀ (n : ℕ), smaller n ≤ larger n) : PolynomiallyBounded smaller

A pointwise smaller resource inherits a polynomial upper bound.

theorem Cslib.Circuits.Circuit.Resource.ConstantlyBounded.polynomiallyBounded {resource : ℕ → ℕ} (bounded : ConstantlyBounded resource) : PolynomiallyBounded resource

Every constant resource bound is a degree-zero polynomial bound.

theorem Cslib.Circuits.Circuit.Resource.EventuallyExceedsEveryPolynomial.not_polynomiallyBounded {resource : ℕ → ℕ} (dominates : EventuallyExceedsEveryPolynomial resource) : ¬PolynomiallyBounded resource

Eventual domination of every polynomial rules out a polynomial bound.

structure Cslib.Circuits.Circuit.Family (sigma : Signature) (m : ℕ) : Type u_1

A nonuniform family chooses one finite circuit at each input width.

• circuit (n : ℕ) : Circuit sigma n m

  The circuit chosen nonuniformly at each input width.

def Cslib.Circuits.Circuit.Family.gateCount {sigma : Signature} {m : ℕ} (family : Family sigma m) (n : ℕ) : ℕ

Number of internal gates at each input width.

Equations

• family.gateCount n = (family.circuit n).size

def Cslib.Circuits.Circuit.Family.size {sigma : Signature} {m : ℕ} (family : Family sigma m) (n : ℕ) : ℕ

Gate-count size of every member of a circuit family.

Equations

• family.size n = (family.circuit n).size

@[simp]

theorem Cslib.Circuits.Circuit.Family.size_eq_gateCount {sigma : Signature} {m : ℕ} (family : Family sigma m) (n : ℕ) : family.size n = family.gateCount n

def Cslib.Circuits.Circuit.Family.depth {sigma : Signature} {m : ℕ} (family : Family sigma m) (n : ℕ) : ℕ

Designated-output depth of every member of a circuit family.

Equations

• family.depth n = (family.circuit n).depth

def Cslib.Circuits.Circuit.Family.cost {sigma : Signature} {m : ℕ} (family : Family sigma m) (operationCost : Algebraic.OperationCost sigma) (n : ℕ) : ℕ

Weighted gate cost of every member of a circuit family.

Equations

• family.cost operationCost n = (family.circuit n).cost operationCost

def Cslib.Circuits.Circuit.Family.Computes {sigma : Signature} {m : ℕ} {U : Type u_2} (family : Family sigma m) (interpretation : Interpretation sigma U) (target : Algebraic.Target.Family U m) : Prop

Pointwise exact computation of a target family.

Equations

• family.Computes interpretation target = ∀ (n : ℕ), (family.circuit n).ComputesWith interpretation (target n)

def Cslib.Circuits.Circuit.Family.HasSizeAtMost {sigma : Signature} {m : ℕ} (family : Family sigma m) (bound : ℕ → ℕ) : Prop

The family has a specified all-width size bound.

Equations

• family.HasSizeAtMost bound = ∀ (n : ℕ), family.size n ≤ bound n

def Cslib.Circuits.Circuit.Family.HasDepthAtMost {sigma : Signature} {m : ℕ} (family : Family sigma m) (bound : ℕ → ℕ) : Prop

The family has a specified all-width depth bound.

Equations

• family.HasDepthAtMost bound = ∀ (n : ℕ), family.depth n ≤ bound n

def Cslib.Circuits.Circuit.Family.HasPolynomialSize {sigma : Signature} {m : ℕ} (family : Family sigma m) : Prop

The family has polynomially bounded gate-count size.

Equations

• family.HasPolynomialSize = Cslib.Circuits.Circuit.Resource.PolynomiallyBounded family.size

def Cslib.Circuits.Circuit.Family.HasPolynomialCost {sigma : Signature} {m : ℕ} (family : Family sigma m) (operationCost : Algebraic.OperationCost sigma) : Prop

The family has polynomially bounded weighted cost.

Equations

• family.HasPolynomialCost operationCost = Cslib.Circuits.Circuit.Resource.PolynomiallyBounded (family.cost operationCost)

def Cslib.Circuits.Circuit.Family.HasConstantDepth {sigma : Signature} {m : ℕ} (family : Family sigma m) : Prop

The family has one depth bound independent of the input width.

Equations

• family.HasConstantDepth = Cslib.Circuits.Circuit.Resource.ConstantlyBounded family.depth

theorem Cslib.Circuits.Circuit.Family.HasSizeAtMost.polynomialSize {sigma : Signature} {m : ℕ} {family : Family sigma m} {bound : ℕ → ℕ} (bounded : family.HasSizeAtMost bound) (polynomial : Resource.PolynomiallyBounded bound) : family.HasPolynomialSize

A pointwise size budget yields polynomial size when the budget is polynomially bounded.

theorem Cslib.Circuits.Circuit.Family.HasDepthAtMost.constantDepth {sigma : Signature} {m : ℕ} {family : Family sigma m} {bound : ℕ → ℕ} (bounded : family.HasDepthAtMost bound) (constant : Resource.ConstantlyBounded bound) : family.HasConstantDepth

A pointwise depth budget yields constant depth when the budget is constantly bounded.