Nondeterministic Circuit Complexity Bounds

Upper bounds on the circuit complexity of existentially quantified Boolean functions.

Given f : BitString (k + m) → Bool, the existential quantification existQuantify f : BitString m → Bool is defined by g(y) = ∃ x ∈ {0,1}^k, f(x ++ y). This models a nondeterministic circuit that guesses the first k input bits.

Definitions (from Circ.Nondeterminism.Defs)

• existQuantify — existential quantification over first k inputs
• forallQuantify — universal quantification over first k inputs
• restrictFirst — fix the first input to a constant

Main results

• restrict_size_complexity_le — hardwiring one input does not increase circuit complexity.

• or_size_complexity_le — the OR of two functions has complexity at most the sum of their complexities plus one.

• existQuantify_complexity_le — naive upper bound: sizeComplexity(existQuantify f) ≤ 2^k · (sizeComplexity(f) + 1). Proof by induction on k using existQuantify_succ, restriction, and OR combination.

• existQuantify_complexity_shannon — Shannon upper bound: sizeComplexity(existQuantify f) ≤ 18 · 2^m / m. Unconditional (the quantified function has only m inputs).

• existQuantify_complexity_min — the minimum of the two bounds above.

The naive bound is tighter when k is small and f has low complexity; the Shannon bound wins when k is large, regardless of f's complexity.

instance CircuitComplexity.instNeZeroAddLeft {k m : ℕ} [NeZero m] : NeZero (k + m)

k + m ≥ 1 whenever m ≥ 1. Enables sizeComplexity on BitString (k + m).

Building-block bounds

theorem CircuitComplexity.restrict_size_complexity_le {k m : ℕ} [CompleteBasis Basis.andOr2] [NeZero m] (f : BitString (k + 1 + m) → Bool) (b : Bool) : Circuit.sizeComplexity Basis.andOr2 (restrictFirst f b) ≤ Circuit.sizeComplexity Basis.andOr2 f

Hardwiring one input does not increase fan-in-2 AND/OR circuit complexity.

Given a circuit of size s computing f, we modify each gate in-place (via restrictGateP): any input that referenced the hardwired variable is redirected using the gate's negation flags to produce the correct constant, without adding extra gates. See Circ.Internal.Nondeterminism for the construction.

theorem CircuitComplexity.or_size_complexity_le {N : ℕ} [CompleteBasis Basis.andOr2] [NeZero N] (g₁ g₂ : BitString N → Bool) : (Circuit.sizeComplexity Basis.andOr2 fun (x : BitString N) => g₁ x || g₂ x) ≤ Circuit.sizeComplexity Basis.andOr2 g₁ + Circuit.sizeComplexity Basis.andOr2 g₂ + 1

The OR of two Boolean functions has circuit complexity bounded by the sum of their individual complexities plus one (for the OR output gate).

Uses ShannonUpper.binopCircuit to compose two circuits side-by-side.

Transport lemma for the base case

Main results

theorem CircuitComplexity.existQuantify_complexity_le {k m : ℕ} [CompleteBasis Basis.andOr2] (f : BitString (k + m) → Bool) [NeZero m] : Circuit.sizeComplexity Basis.andOr2 (existQuantify f) ≤ 2 ^ k * (Circuit.sizeComplexity Basis.andOr2 f + 1)

Naive upper bound for existential quantification.

If f : BitString (k + m) → Bool has fan-in-2 AND/OR circuit complexity s, then existQuantify f : BitString m → Bool has circuit complexity at most 2^k · (s + 1).

Proof. By induction on k. We prove the tighter statement sizeComplexity + 1 ≤ 2^k · (s + 1), which absorbs the OR-gate overhead at each step.

• Base case (k = 0): existQuantify is the identity (up to a transport along 0 + m = m), so complexity is preserved.

• Inductive step (k → k + 1): existQuantify (k+1) f factors as (existQuantify k (f|₀)) OR (existQuantify k (f|₁)) via existQuantify_succ. Restriction preserves complexity; the OR adds one gate; and the inductive hypothesis bounds each branch by 2^k · (s + 1) − 1. After the "+1 trick": (size₁ + size₂ + 1) + 1 = (size₁ + 1) + (size₂ + 1) ≤ 2^(k+1) · (s + 1).

theorem CircuitComplexity.existQuantify_complexity_shannon {k m : ℕ} [CompleteBasis Basis.andOr2] (f : BitString (k + m) → Bool) [NeZero m] (hm : 16 ≤ m) : Circuit.sizeComplexity Basis.andOr2 (existQuantify f) ≤ 18 * 2 ^ m / m

Shannon upper bound for existential quantification.

The quantified function existQuantify f : BitString m → Bool is just an m-input Boolean function, so the Shannon upper bound applies unconditionally. Even if f has exponential circuit complexity, existQuantify f has complexity at most O(2^m / m), which decreases exponentially as more variables are quantified away.

theorem CircuitComplexity.existQuantify_complexity_min {k m : ℕ} [CompleteBasis Basis.andOr2] (f : BitString (k + m) → Bool) [NeZero m] (hm : 16 ≤ m) : Circuit.sizeComplexity Basis.andOr2 (existQuantify f) ≤ min (2 ^ k * (Circuit.sizeComplexity Basis.andOr2 f + 1)) (18 * 2 ^ m / m)

Combined upper bound: the minimum of the naive and Shannon bounds.

When sizeComplexity(f) ≈ 2^(k+m)/2, the Shannon bound 18 · 2^m / m is exponentially better than the naive 2^k · (s + 1), especially for large k.