Circuit size classes and CSLib circuits

This module lifts the per-function bridge of Complexitylib.Interop.Cslib.Circuit to the language classes SIZE s. The key device is sliceSizeComplexity L, the fan-in-two AND/OR size complexity of each length slice of L: a language lies in SIZE s exactly when these slice complexities are pointwise below s.

Main results

• Complexity.mem_SIZE_iff_sliceSizeComplexity_le — SIZE s membership is a pointwise bound on slice size complexity
• Complexity.exists_cslib_of_mem_SIZE, Complexity.mem_SIZE_of_cslib — SIZE in CSLib's De Morgan circuit model
• Complexity.lupanov_sliceSizeComplexity, Complexity.exists_mem_SIZE_bigO_two_pow_div — every language has circuits of size (1 + ε) 2ⁿ / n for large n, hence of size O(2ⁿ / n)
• Complexity.exists_language_not_mem_SIZE — some language is outside SIZE s whenever n + 2 s(n) ≤ 2ⁿ / n eventually; in particular (Complexity.exists_language_not_mem_SIZE_littleO) whenever s = o(2ⁿ / n)
• Complexity.SIZE_subset_cslib_SIZE, Complexity.cslib_SIZE_subset_SIZE — our SIZE classes versus CSLib's De Morgan classes Cslib.Circuits.Boolean.SIZE
• Complexity.PPoly_eq_cslib_PPoly — our PPoly is CSLib's Cslib.Circuits.Boolean.PPoly; hence (Complexity.exists_not_mem_PPoly) some language lies outside PPoly

Relation to CSLib's family-level results

CSLib states Lupanov's and Shannon's bounds for De Morgan circuit families (Cslib.Circuits.Boolean.exists_decides_size_le, Cslib.Circuits.Boolean.exists_language_lt_size) and derives Cslib.Circuits.Boolean.exists_not_mem_PPoly. Our hard language (Complexity.exists_language_sliceSizeComplexity_gt) is CSLib's, and our exists_not_mem_PPoly is CSLib's through PPoly_eq_cslib_PPoly. The Lupanov results here are the fan-in-two AND/OR slice form of CSLib's family bound; they come from the per-function transfer Complexity.lupanov_sizeComplexity, which absorbs the extra output gate of Circuit.ofCslib.

Provenance of CSLib's family-level classes

CSLib's circuit families and the classes Cslib.Circuits.Boolean.SIZE and Cslib.Circuits.Boolean.PPoly (with their family-level Lupanov and Shannon bounds and Cslib.Circuits.Boolean.exists_not_mem_PPoly), together with Language.slice, are not yet in upstream CSLib. They are pending CSLib work by this library's author, pinned here from the integration branch of the SamuelSchlesinger/cslib fork. The comparisons with them in this file are therefore consistency checks against those definitions, not corroboration by independently reviewed ones, and they may need revisiting if the definitions change before merging. The counting argument behind the hard language, Cslib.Circuits.Boolean.Shannon.exists_hard_function, is merged upstream (CSLib PR #891), but the pinned version restates it for the bundled circuit size Circuit.size of the pending CSLib PR #949, so the statement used here is itself part of the pending work.

noncomputable def Complexity.sliceSizeComplexity (L : Language) : ℕ → ℕ

The fan-in-two AND/OR size complexity of the length-n slice of L, with value 0 on the empty length (which circuit families answer by a stored bit).

Equations

• Complexity.sliceSizeComplexity L 0 = 0
• Complexity.sliceSizeComplexity L n.succ = Complexity.Circuit.sizeComplexity Complexity.Basis.andOr2 fun (x : Complexity.BitString (n + 1)) => decide (List.ofFn x ∈ L)

theorem Complexity.sliceSizeComplexity_succ (L : Language) (m : ℕ) : sliceSizeComplexity L (m + 1) = Circuit.sizeComplexity Basis.andOr2 fun (x : BitString (m + 1)) => decide (List.ofFn x ∈ L)

At a positive length, sliceSizeComplexity is the size complexity of the slice.

theorem Complexity.mem_SIZE_iff_sliceSizeComplexity_le {L : Language} {s : ℕ → ℕ} : L ∈ SIZE s ↔ ∀ (n : ℕ), sliceSizeComplexity L n ≤ s n

SIZE via slice complexity. A language lies in SIZE s exactly when every length slice has fan-in-two AND/OR size complexity at most s n.

theorem Complexity.mem_SIZE_sliceSizeComplexity (L : Language) : L ∈ SIZE (sliceSizeComplexity L)

Every language lies in SIZE of its own slice complexity, the least size bound it admits.

theorem Complexity.exists_cslib_of_mem_SIZE {L : Language} {s : ℕ → ℕ} (hL : L ∈ SIZE s) (n : ℕ) : ∃ (c : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature n 1), c.size ≤ n + 2 * s n + 1 ∧ c.Computes Cslib.Circuits.Boolean.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => decide (List.ofFn x ∈ L)

SIZE in CSLib terms, forward. If L ∈ SIZE s, then at every length n some CSLib De Morgan circuit of size at most n + 2 s(n) + 1 decides the length-n slice of L.

theorem Complexity.mem_SIZE_of_cslib {L : Language} {s : ℕ → ℕ} (h : ∀ (n : ℕ) [NeZero n], ∃ (c : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature n 1), c.size ≤ s n ∧ c.Computes Cslib.Circuits.Boolean.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => decide (List.ofFn x ∈ L)) : L ∈ SIZE fun (n : ℕ) => s n + 1

SIZE in CSLib terms, backward. If at every positive length n some CSLib De Morgan circuit of size at most s(n) decides the length-n slice of L, then L ∈ SIZE (s + 1).

theorem Complexity.slice_eq_decide (L : Language) (n : ℕ) : Language.slice L n = fun (x : Fin n → Bool) => decide (List.ofFn x ∈ L)

CSLib's length-n slice of a language is its classical characteristic function on words of length n.

theorem Complexity.SIZE_subset_cslib_SIZE (s : ℕ → ℕ) : SIZE s ⊆ Cslib.Circuits.Boolean.SIZE fun (n : ℕ) => n + 2 * s n + 1

Our SIZE inside CSLib's. A language with fan-in-two AND/OR circuits of size s(n) has De Morgan circuits of size n + 2 s(n) + 1.

Cslib.Circuits.Boolean.SIZE comes from the author's pending CSLib work, pinned from the integration branch of the SamuelSchlesinger/cslib fork, so this inclusion is a consistency check with that definition (see the module docstring).

theorem Complexity.cslib_SIZE_subset_SIZE (s : ℕ → ℕ) : Cslib.Circuits.Boolean.SIZE s ⊆ SIZE fun (n : ℕ) => s n + 1

CSLib's SIZE inside ours. A language with De Morgan circuits of size s(n) has fan-in-two AND/OR circuits of size s(n) + 1.

Cslib.Circuits.Boolean.SIZE comes from the author's pending CSLib work, pinned from the integration branch of the SamuelSchlesinger/cslib fork, so this inclusion is a consistency check with that definition (see the module docstring).

theorem Complexity.PPoly_eq_cslib_PPoly : PPoly = Cslib.Circuits.Boolean.PPoly

Our P/poly is CSLib's. Fan-in-two AND/OR circuits with free negations and De Morgan circuits counting every gate define the same class P/poly: the two size measures agree up to n + 2s + 1, and CSLib's bounds n ^ k + k are cofinal among polynomials.

Cslib.Circuits.Boolean.PPoly and the Cslib.Circuits.Boolean.SIZE classes it is built from come from the author's pending CSLib work, pinned from the integration branch of the SamuelSchlesinger/cslib fork and not yet reviewed upstream. The equality is therefore a consistency check between this library's PPoly and those definitions (see the module docstring).

theorem Complexity.exists_not_mem_PPoly : ∃ (L : Language), L ∉ PPoly

Some language is not in P/poly. This is CSLib's Cslib.Circuits.Boolean.exists_not_mem_PPoly, through PPoly_eq_cslib_PPoly.

That theorem and Cslib.Circuits.Boolean.PPoly come from the author's pending CSLib work, pinned from the integration branch of the SamuelSchlesinger/cslib fork. The counting argument underneath, Cslib.Circuits.Boolean.Shannon.exists_hard_function, is merged upstream, but the pinned version is restated for the bundled circuit size of the pending CSLib PR #949 (see the module docstring).

theorem Complexity.lupanov_sliceSizeComplexity {ε : ℝ} (hε : 0 < ε) : ∃ (N₀ : ℕ), ∀ (L : Language) (n : ℕ), N₀ ≤ n → ↑(sliceSizeComplexity L n) ≤ (1 + ε) * 2 ^ n / ↑n

Lupanov's bound for languages. For every ε > 0 there is N₀ such that every language's slices of length n ≥ N₀ have fan-in-two AND/OR size complexity at most (1 + ε) 2ⁿ / n. This is the fan-in-two AND/OR form of CSLib's family bound Cslib.Circuits.Boolean.exists_decides_size_le.

theorem Complexity.exists_mem_SIZE_lupanov {ε : ℝ} (hε : 0 < ε) (L : Language) : ∃ (s : ℕ → ℕ), (∀ᶠ (n : ℕ) in Filter.atTop, ↑(s n) ≤ (1 + ε) * 2 ^ n / ↑n) ∧ L ∈ SIZE s

Every language has near-optimal circuits. For every ε > 0, every language lies in SIZE s for some s with s(n) ≤ (1 + ε) 2ⁿ / n for all large n.

theorem Complexity.exists_mem_SIZE_bigO_two_pow_div (L : Language) : ∃ (s : ℕ → ℕ), (BigO s fun (n : ℕ) => 2 ^ n / n) ∧ L ∈ SIZE s

Every language has circuits of size O(2ⁿ / n) (with 2ⁿ / n the natural-number quotient).

theorem Complexity.exists_language_sliceSizeComplexity_gt : ∃ (L : Language), ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ n / ↑n < ↑n + 2 * ↑(sliceSizeComplexity L n)

A hard language. Some language has slice size complexity above (2ⁿ / n - n) / 2 at every large length n. The language is the one of CSLib's family-level Shannon bound Cslib.Circuits.Boolean.exists_language_lt_size.

theorem Complexity.exists_language_not_mem_SIZE : ∃ (L : Language), ∀ (s : ℕ → ℕ), (∀ᶠ (n : ℕ) in Filter.atTop, ↑n + 2 * ↑(s n) ≤ 2 ^ n / ↑n) → L ∉ SIZE s

Hard languages outside small SIZE classes. Some language lies outside SIZE s for every s with n + 2 s(n) ≤ 2ⁿ / n for all large n.

theorem Complexity.exists_language_not_mem_SIZE_littleO : ∃ (L : Language), ∀ (s : ℕ → ℕ), (LittleO s fun (n : ℕ) => 2 ^ n / n) → L ∉ SIZE s

SIZE(o(2ⁿ / n)) misses a language. Some language lies outside SIZE s for every s = o(2ⁿ / n) (with 2ⁿ / n the natural-number quotient).