Circuit depth classes

This module defines nonuniform DEPTH, NC^i, AC^i, and TC^i classes using the library's total circuit-family convention. Every class therefore includes a specified answer on the empty input. NC i uses fan-in two, AC i uses unbounded AND/OR gates, TC i uses unbounded threshold gates, and all impose polynomial size.

The concrete polylogarithmic envelope is c * (Nat.log 2 n + 1) ^ i. Thus NC0 and AC0 are constant-depth classes, while NC1 is logarithmic depth with the same c * log₂ n + c convention as the Barrington formula-family development.

These definitions are explicitly nonuniform. Generator uniformity is an additional predicate and is not implicit in the names NC, AC, or TC.

theorem Complexity.polylogDepth_zero (c n : ℕ) : polylogDepth 0 c n = c

The exponent-zero polylogarithmic envelope is the constant c.

theorem Complexity.polylogDepth_one (c n : ℕ) : polylogDepth 1 c n = c * Nat.log 2 n + c

The exponent-one envelope agrees with the Barrington convention c * log₂ n + c.

theorem Complexity.polylogDepth_mono_constant {c c' : ℕ} (hcc' : c ≤ c') (i n : ℕ) : polylogDepth i c n ≤ polylogDepth i c' n

Increasing the multiplicative constant weakens a polylogarithmic depth bound.

theorem Complexity.polylogDepth_mono_exponent {i j : ℕ} (hij : i ≤ j) (c n : ℕ) : polylogDepth i c n ≤ polylogDepth j c n

Increasing the polylogarithmic exponent weakens the depth bound.

theorem Complexity.DEPTHWithBasis_mono (B : Basis) {d e : ℕ → ℕ} (hde : ∀ (n : ℕ), d n ≤ e n) : DEPTHWithBasis B d ⊆ DEPTHWithBasis B e

DEPTHWithBasis is monotone in its pointwise depth envelope.

theorem Complexity.NC_mono {i j : ℕ} (hij : i ≤ j) : NC i ⊆ NC j

The NC hierarchy is monotone in its polylogarithmic exponent.

theorem Complexity.AC_mono {i j : ℕ} (hij : i ≤ j) : AC i ⊆ AC j

The AC hierarchy is monotone in its polylogarithmic exponent.

theorem Complexity.TC_mono {i j : ℕ} (hij : i ≤ j) : TC i ⊆ TC j

The TC hierarchy is monotone in its polylogarithmic exponent.

theorem Complexity.AC_subset_TC (i : ℕ) : AC i ⊆ TC i

Exact gatewise simulation gives AC^i ⊆ TC^i without changing size or depth.

theorem Complexity.AC0_subset_TC0 : AC0 ⊆ TC0

In particular, nonuniform AC0 is contained in nonuniform TC0.

theorem Complexity.NC0_subset_NC1 : NC0 ⊆ NC1

In particular, constant-depth bounded-fan-in families are logarithmic depth.

theorem Complexity.mem_NC1_iff {f : BoolFunFamily} : f ∈ NC1 ↔ ∃ (F : CircuitFamily Basis.andOr2) (c : ℕ), F.Computes f ∧ F.PolynomialSize ∧ F.DepthBoundedBy fun (n : ℕ) => c * Nat.log 2 n + c

Membership in NC1 is exactly polynomial size and a c * log₂ n + c pointwise depth bound for one fan-in-two family.

theorem Complexity.mem_AC0_iff {f : BoolFunFamily} : f ∈ AC0 ↔ ∃ (F : CircuitFamily Basis.unboundedAndOr) (c : ℕ), F.Computes f ∧ F.PolynomialSize ∧ F.DepthBoundedBy fun (x : ℕ) => c

Membership in AC0 is exactly polynomial size and a constant pointwise depth bound for one total unbounded-fan-in circuit family.

theorem Complexity.mem_TC0_iff {f : BoolFunFamily} : f ∈ TC0 ↔ ∃ (F : CircuitFamily Basis.threshold) (c : ℕ), F.Computes f ∧ F.PolynomialSize ∧ F.DepthBoundedBy fun (x : ℕ) => c

Membership in TC0 is exactly polynomial size and a constant pointwise depth bound for one total threshold-circuit family.