Boolean circuit families

This module provides the public API for circuit-family semantics, concrete size/depth bounds, and the equivalence between pointwise polynomial bounds and the power big-O convention used by complexity classes.

theorem Complexity.Circuit.computes_congr {B : Basis} {N G : ℕ} [NeZero N] (c : Circuit B N 1 G) {f g : BitString N → Bool} (h : f = g) : c.Computes f ↔ c.Computes g

Computes respects equality of the target function.

theorem Complexity.Circuit.computesOnLength_congr {B : Basis} {N G : ℕ} [NeZero N] (c : Circuit B N 1 G) {f g : BoolFunFamily} (h : f N = g N) : c.ComputesOnLength f ↔ c.ComputesOnLength g

ComputesOnLength depends only on the family's component at length N.

theorem Complexity.Circuit.Computes.apply {B : Basis} {N G : ℕ} [NeZero N] {c : Circuit B N 1 G} {f : BitString N → Bool} (h : c.Computes f) (x : BitString N) : c.eval x 0 = f x

A circuit computing f evaluates to f x on each input x.

theorem Complexity.Circuit.ComputesOnLength.apply {B : Basis} {N G : ℕ} [NeZero N] {c : Circuit B N 1 G} {f : BoolFunFamily} (h : c.ComputesOnLength f) (x : BitString N) : c.eval x 0 = f N x

A circuit computing a family at length N evaluates to f N x on each input x.

theorem Complexity.Circuit.Computes.sizeComplexity_le {B : Basis} {N G : ℕ} [NeZero N] {c : Circuit B N 1 G} {f : BitString N → Bool} (h : c.Computes f) : sizeComplexity B f ≤ c.size

Any circuit computing f witnesses an upper bound on the size complexity of f.

@[simp]

theorem Complexity.CircuitFamily.function_zero {B : Basis} (F : CircuitFamily B) (x : BitString 0) : F.function 0 x = F.emptyOutput

At length 0 the family's function is the designated empty-input output.

@[simp]

theorem Complexity.CircuitFamily.function_succ {B : Basis} (F : CircuitFamily B) (n : ℕ) (x : BitString (n + 1)) : F.function (n + 1) x = (F.circuit (n + 1)).eval x 0

At positive lengths the family's function is evaluation of the length-n + 1 circuit.

@[simp]

theorem Complexity.CircuitFamily.size_zero {B : Basis} (F : CircuitFamily B) : F.size 0 = 0

The size of a circuit family at length 0 is 0.

@[simp]

theorem Complexity.CircuitFamily.size_succ {B : Basis} (F : CircuitFamily B) (n : ℕ) : F.size (n + 1) = (F.circuit (n + 1)).size

At positive lengths the family's size is the size of the length-n + 1 circuit.

@[simp]

theorem Complexity.CircuitFamily.depth_zero {B : Basis} (F : CircuitFamily B) : F.depth 0 = 0

The depth of a circuit family at length 0 is 0.

@[simp]

theorem Complexity.CircuitFamily.depth_succ {B : Basis} (F : CircuitFamily B) (n : ℕ) : F.depth (n + 1) = (F.circuit (n + 1)).depth

At positive lengths the family's depth is the depth of the length-n + 1 circuit.

theorem Complexity.CircuitFamily.sizeBoundedBy_mono {B : Basis} (F : CircuitFamily B) {s t : ℕ → ℕ} (hF : F.SizeBoundedBy s) (hst : ∀ (n : ℕ), s n ≤ t n) : F.SizeBoundedBy t

A size bound may be weakened to any pointwise larger bound.

theorem Complexity.CircuitFamily.depthBoundedBy_mono {B : Basis} (F : CircuitFamily B) {d e : ℕ → ℕ} (hF : F.DepthBoundedBy d) (hde : ∀ (n : ℕ), d n ≤ e n) : F.DepthBoundedBy e

A depth bound may be weakened to any pointwise larger bound.

theorem Complexity.CircuitFamily.SizeBoundedBy.bigO {B : Basis} {F : CircuitFamily B} {s : ℕ → ℕ} (h : F.SizeBoundedBy s) : BigO F.size s

A pointwise size bound yields a big-O size bound.

theorem Complexity.CircuitFamily.polynomialSize_iff_bigO {B : Basis} (F : CircuitFamily B) : F.PolynomialSize ↔ ∃ (k : ℕ), BigO F.size fun (x : ℕ) => x ^ k

Pointwise polynomial size is equivalent to a big-O power bound.

theorem Complexity.CircuitFamily.computes_congr {B : Basis} (F : CircuitFamily B) {f g : BoolFunFamily} (h : f = g) : F.Computes f ↔ F.Computes g

Computes respects equality of the target function family.

theorem Complexity.CircuitFamily.computes_unique {B : Basis} (F : CircuitFamily B) {f g : BoolFunFamily} (hf : F.Computes f) (hg : F.Computes g) : f = g

A circuit family computes at most one function family.

@[simp]

theorem Complexity.CircuitFamily.evalList_ofFn {B : Basis} (F : CircuitFamily B) {n : ℕ} (x : BitString n) : F.evalList (List.ofFn x) = F.function n x

Evaluating the serialized fixed-length input agrees with family evaluation at that length.

@[simp]

theorem Complexity.CircuitFamily.evalList_toList {B : Basis} (F : CircuitFamily B) {n : ℕ} (x : BitString n) : F.evalList x.toList = F.function n x

Evaluating the list form of a fixed-length input agrees with family evaluation at that length.

@[simp]

theorem Complexity.CircuitFamily.evalList_nil {B : Basis} (F : CircuitFamily B) : F.evalList [] = F.emptyOutput

Evaluating the empty list yields the designated empty-input output.

theorem Complexity.CircuitFamily.Computes.apply {B : Basis} {F : CircuitFamily B} {f : BoolFunFamily} (h : F.Computes f) (n : ℕ) (x : BitString n) : F.function n x = f n x

A family computing f agrees with f at every length and input.

theorem Complexity.CircuitFamily.Computes.evalList {B : Basis} {F : CircuitFamily B} {f : BoolFunFamily} (h : F.Computes f) (x : List Bool) : F.evalList x = f x.length x.get

A family computing f evaluates any list input to f at the list's length.