Boolean circuit families — definitions

This module lifts the finite Circuit model to one circuit at every positive input length. Because Circuit deliberately requires a nonzero input arity, the answer on the unique empty input is stored separately as emptyOutput.

The first component of circuits n is the number of internal gates. Family size counts internal and output gates, but not primary-input vertices or the free per-edge negation flags.

def Complexity.Circuit.Computes {B : Basis} {N G : ℕ} [NeZero N] (c : Circuit B N 1 G) (f : BitString N → Bool) : Prop

A single-output circuit computes f when its output agrees with f on every input.

Equations

• c.Computes f = ((fun (x : Complexity.BitString N) => c.eval x 0) = f)

def Complexity.Circuit.ComputesOnLength {B : Basis} {N G : ℕ} [NeZero N] (c : Circuit B N 1 G) (f : BoolFunFamily) : Prop

A circuit computes the length-N member of a Boolean function family.

Equations

• c.ComputesOnLength f = c.Computes (f N)

structure Complexity.CircuitFamily (B : Basis) : Type

A nonuniform family of single-output circuits over B.

At each positive length n, the dependent pair contains an internal-gate count G and a circuit Circuit B n 1 G. The unique length-zero input is handled by emptyOutput, since the base circuit model deliberately requires at least one input wire.

• emptyOutput : Bool

  The family's answer on the unique length-zero input, stored directly because Circuit requires a positive input arity.

• circuits (n : ℕ) [NeZero n] : (G : ℕ) × Circuit B n 1 G

  For each positive length n, an internal-gate count G paired with a single-output circuit on n inputs and G internal gates.

def Complexity.CircuitFamily.internalGateCount {B : Basis} (F : CircuitFamily B) (n : ℕ) [NeZero n] : ℕ

Number of internal gates in the positive-length circuit.

Equations

• F.internalGateCount n = (F.circuits n).fst

def Complexity.CircuitFamily.circuit {B : Basis} (F : CircuitFamily B) (n : ℕ) [NeZero n] : Circuit B n 1 (F.internalGateCount n)

The circuit selected by the family at positive input length n.

Equations

• F.circuit n = (F.circuits n).snd

def Complexity.CircuitFamily.function {B : Basis} (F : CircuitFamily B) : BoolFunFamily

The Boolean function family computed by F, including its explicit length-zero answer.

Equations

• F.function 0 x_2 = F.emptyOutput
• F.function n.succ x_2 = (F.circuit (n + 1)).eval x_2 0

def Complexity.CircuitFamily.evalList {B : Basis} (F : CircuitFamily B) (x : List Bool) : Bool

Evaluate a circuit family on the list representation used by languages.

Equations

• F.evalList x = F.function x.length x.get

def Complexity.CircuitFamily.size {B : Basis} (F : CircuitFamily B) : ℕ → ℕ

Total circuit size at each length. The separate empty-input answer is a finite exception and is assigned size zero.

Equations

• F.size 0 = 0
• F.size n.succ = (F.circuit (n + 1)).size

def Complexity.CircuitFamily.depth {B : Basis} (F : CircuitFamily B) : ℕ → ℕ

Circuit depth at each length, with depth zero on the empty input.

Equations

• F.depth 0 = 0
• F.depth n.succ = (F.circuit (n + 1)).depth

def Complexity.CircuitFamily.SizeBoundedBy {B : Basis} (F : CircuitFamily B) (s : ℕ → ℕ) : Prop

A pointwise size bound for a circuit family.

Equations

• F.SizeBoundedBy s = ∀ (n : ℕ), F.size n ≤ s n

def Complexity.CircuitFamily.DepthBoundedBy {B : Basis} (F : CircuitFamily B) (d : ℕ → ℕ) : Prop

A pointwise depth bound for a circuit family.

Equations

• F.DepthBoundedBy d = ∀ (n : ℕ), F.depth n ≤ d n

def Complexity.CircuitFamily.PolynomialSize {B : Basis} (F : CircuitFamily B) : Prop

A family has polynomial size when one natural-coefficient polynomial bounds its size at every input length.

Equations

• F.PolynomialSize = ∃ (p : Polynomial ℕ), F.SizeBoundedBy fun (n : ℕ) => Polynomial.eval n p

def Complexity.CircuitFamily.Computes {B : Basis} (F : CircuitFamily B) (f : BoolFunFamily) : Prop

F computes the Boolean function family f at every length.

Equations

• F.Computes f = (F.function = f)