Complexitylib circuits and CSLib circuits

CSLib's circuit model counts every gate of its De Morgan basis (constants, negation, binary conjunction and disjunction) toward size. Our fan-in-two AND/OR circuits (Basis.andOr2) make negation free and count their output gates. The two sizes agree up to a factor of two and an additive N:

• Circuit.ofCslib turns a CSLib circuit of size g with M outputs into one of ours of size g + M (Circuit.eval_ofCslib, Circuit.size_ofCslib);
• Circuit.exists_cslib turns one of ours with G internal gates into a CSLib circuit of size at most N + 2G + M.

CSLib proves the sharp counting bounds for its model, and they transfer here with different losses. Lupanov's upper bound, previously missing from this library, transfers sharply: Circuit.sizeComplexity is at most (1 + ε) 2ⁿ / n for large n. Shannon's lower bound pays the factor of two of Circuit.exists_cslib: some function has 2ⁿ / n < n + 2 · sizeComplexity, that is, size complexity above (2ⁿ / n - n) / 2, about half the sharp bound 2ⁿ / n.

Main results

• Complexity.Circuit.sizeComplexity_le_of_cslib, Complexity.Circuit.exists_cslib_of_sizeComplexity — size complexity versus CSLib gate counts
• Complexity.lupanov_sizeComplexity — every function on n bits has size complexity at most (1 + ε) 2ⁿ / n for large n
• Complexity.exists_sizeComplexity_gt_cslib — some function on n bits has size complexity above (2ⁿ / n - n) / 2 for large n
• Complexity.mem_PPoly_iff_cslib — P/poly is exactly the class of languages with polynomial-size CSLib De Morgan circuits at every input length; see Complexity.PPoly_eq_cslib_PPoly for the equality with CSLib's own class

theorem Complexity.Circuit.cslib_computes_iff {σ : Cslib.Circuits.Signature} {U : Type u_1} {I : Cslib.Circuits.Interpretation σ U} {N : ℕ} {c : Cslib.Circuits.Circuit σ N 1} {f : (Fin N → U) → U} : (c.Computes I fun (x : Fin N → U) (x_1 : Fin 1) => f x) ↔ ∀ (x : Fin N → U), c.eval I x 0 = f x

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

theorem Complexity.Circuit.eval_ofCslib {N M : ℕ} [NeZero N] [NeZero M] (c : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature N M) (x : BitString N) : (ofCslib c).eval x = c.eval Cslib.Circuits.Boolean.interpretation x

CSLib circuits run as ours. The translation computes what the CSLib circuit computes.

theorem Complexity.Circuit.size_ofCslib {N M : ℕ} [NeZero N] [NeZero M] (c : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature N M) : (ofCslib c).size = c.size + M

The translation of a CSLib circuit of size g with M outputs has size g + M.

theorem Complexity.Circuit.exists_cslib {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.andOr2 N M G) : ∃ (c' : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature N M), c'.size ≤ N + 2 * G + M ∧ ∀ (x : Fin N → Bool) (j : Fin M), c'.eval Cslib.Circuits.Boolean.interpretation x j = c.eval x j

Our circuits run as CSLib's. A fan-in-two AND/OR circuit with G internal gates and M outputs has a CSLib De Morgan circuit of size at most N + 2G + M computing the same outputs.

theorem Complexity.Circuit.sizeComplexity_le_of_cslib {N : ℕ} [NeZero N] (c : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature N 1) {f : BitString N → Bool} (hc : c.Computes Cslib.Circuits.Boolean.interpretation fun (x : Fin N → Bool) (x_1 : Fin 1) => f x) : sizeComplexity Basis.andOr2 f ≤ c.size + 1

A CSLib De Morgan circuit computing f bounds its fan-in-two AND/OR size complexity by its size plus one.

theorem Complexity.Circuit.exists_cslib_of_sizeComplexity {N : ℕ} [NeZero N] (f : BitString N → Bool) : ∃ (c : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature N 1), c.size ≤ N + 2 * sizeComplexity Basis.andOr2 f ∧ c.Computes Cslib.Circuits.Boolean.interpretation fun (x : Fin N → Bool) (x_1 : Fin 1) => f x

Every function has a CSLib De Morgan circuit of size at most N + 2 · sizeComplexity f.

theorem Complexity.lupanov_sizeComplexity {ε : ℝ} (hε : 0 < ε) : ∃ (N₀ : ℕ), ∀ (n : ℕ) [inst : NeZero n], N₀ ≤ n → ∀ (f : BitString n → Bool), ↑(Circuit.sizeComplexity Basis.andOr2 f) ≤ (1 + ε) * 2 ^ n / ↑n

Lupanov's upper bound. For every ε > 0 and all sufficiently large n, every Boolean function on n bits has fan-in-two AND/OR size complexity at most (1 + ε) 2ⁿ / n. Transferred from CSLib's De Morgan bound.

theorem Complexity.exists_sizeComplexity_gt_cslib : ∃ (N₀ : ℕ), ∀ (n : ℕ) [inst : NeZero n], N₀ ≤ n → ∃ (f : BitString n → Bool), 2 ^ n / ↑n < ↑n + 2 * ↑(Circuit.sizeComplexity Basis.andOr2 f)

Shannon's lower bound, transferred from CSLib. For all sufficiently large n, some Boolean function on n bits has fan-in-two AND/OR size complexity above (2ⁿ / n - n) / 2.

theorem Complexity.mem_PPoly_iff_cslib {L : Language} : L ∈ PPoly ↔ ∃ (p : Polynomial ℕ), ∀ (n : ℕ), ∃ (c : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature n 1), c.size ≤ Polynomial.eval n p ∧ c.Computes Cslib.Circuits.Boolean.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => decide (List.ofFn x ∈ L)

P/poly in CSLib's circuit model. A language is in P/poly exactly when, for some polynomial p and every input length n, a CSLib De Morgan circuit of size at most p(n) decides its length-n slice.