A language outside P/poly

Shannon's counting argument gives, for every large n, a Boolean function on n bits whose circuit complexity exceeds 2 ^ n / n (Cslib.Circuits.Boolean.Shannon.lt_complexity). A language whose slices are such functions is not in P/poly, since 2 ^ n / n outgrows every polynomial Arora and Barak, Theorem 6.21.

Main results

• Cslib.Circuits.Boolean.PPoly.exists_not_mem: some language over Bool is not in P/poly.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 6.4
• C. E. Shannon, The synthesis of two-terminal switching circuits

theorem Cslib.Circuits.Boolean.PPoly.exists_not_mem : ∃ (L : Language Bool), L ∉ PPoly

P/poly is not every language. Some language over Bool has slices whose circuit complexity is not polynomially bounded.