The Shannon window of MCSP

Every Boolean function on n inputs has a circuit with about 2 ^ n / n gates, and most of them need about that many [Sha49], [Lup58]. So for uniformly random truth tables the answer to MCSP changes near threshold 2 ^ n / n: above it every truth table is a yes-instance, and below it almost every truth table is a no-instance. This is a statement about the distribution of circuit complexities, not about the difficulty of deciding MCSP: at lower thresholds the rare yes-instances must still be recognized exactly, and that regime is the one studied by hardness magnification [OPS19]. This file states the window with explicit constants and explicit arities:

• for n ≥ 64, every truth table is a yes-instance at threshold 12 · 2 ^ n / n (MCSP.mem_of_twelve_mul_le), by Lupanov's construction with explicit parameters;
• for n ≥ 16, at most 2 ^ (2 ^ n / 4) of the 2 ^ (2 ^ n) truth tables are yes-instances at threshold 2 ^ n / (5 n) (MCSP.ncard_setOf_mem_le), by counting circuits.

It also states the asymptotically sharp window, from cslib's Lupanov and Shannon bounds: for every ε > 0 and all large n, every truth table is a yes-instance at threshold (1 + ε) 2 ^ n / n (MCSP.eventually_mem), and some truth table is a no-instance at threshold 2 ^ n / n (MCSP.eventually_exists_not_mem).

Sizes count every AND, OR, NOT and constant gate.

Main results

• Cslib.MCSP.mem_of_twelve_mul_le, Cslib.MCSP.ncard_setOf_mem_le, Cslib.MCSP.exists_not_mem: the explicit window.
• Cslib.MCSP.eventually_mem, Cslib.MCSP.eventually_exists_not_mem: the sharp window.

References

• C. E. Shannon, The Synthesis of Two-Terminal Switching Circuits
• O. B. Lupanov, On a Method of Circuit Synthesis
• Stasys Jukna, Boolean Function Complexity: Advances and Frontiers, Theorems 1.14 and 1.15.
• I. C. Oliveira, J. Pich, R. Santhanam, Hardness magnification near state-of-the-art lower bounds

Elementary estimates

Every function has a circuit with 12 · 2 ^ n / n gates

Few functions have a circuit with 2 ^ n / (5 n) gates

The explicit window

theorem Cslib.MCSP.mem_of_twelve_mul_le {n s : ℕ} (hn : 64 ≤ n) (T : BitString (2 ^ n)) (hs : 12 * 2 ^ n / n ≤ s) : { arity := n, table := T, threshold := s } ∈ MCSP

Above the window. For n ≥ 64, every truth table of a function on n inputs is a yes-instance of MCSP at every threshold of at least 12 · 2 ^ n / n.

theorem Cslib.MCSP.ncard_setOf_mem_le {n : ℕ} (hn : 16 ≤ n) : {T : BitString (2 ^ n) | { arity := n, table := T, threshold := 2 ^ n / (5 * n) } ∈ MCSP}.ncard ≤ 2 ^ (2 ^ n / 4)

Below the window. For n ≥ 16, at most 2 ^ (2 ^ n / 4) of the 2 ^ (2 ^ n) truth tables of functions on n inputs are yes-instances of MCSP at threshold 2 ^ n / (5 n).

theorem Cslib.MCSP.exists_not_mem {n : ℕ} (hn : 16 ≤ n) : ∃ (T : BitString (2 ^ n)), { arity := n, table := T, threshold := 2 ^ n / (5 * n) } ∉ MCSP

For n ≥ 16, some truth table of a function on n inputs is a no-instance of MCSP at threshold 2 ^ n / (5 n).

The sharp window

theorem Cslib.MCSP.eventually_mem (ε : ℝ) (hε : 0 < ε) : ∃ (N : ℕ), ∀ n ≥ N, ∀ (T : BitString (2 ^ n)) (s : ℕ), (1 + ε) * 2 ^ n / ↑n ≤ ↑s → { arity := n, table := T, threshold := s } ∈ MCSP

Above the sharp window [Lup58]. For every ε > 0 and all large n, every truth table of a function on n inputs is a yes-instance of MCSP at every threshold of at least (1 + ε) 2 ^ n / n.

theorem Cslib.MCSP.eventually_exists_not_mem : ∃ (N : ℕ), ∀ n ≥ N, ∃ (T : BitString (2 ^ n)), { arity := n, table := T, threshold := 2 ^ n / n } ∉ MCSP

Below the sharp window [Sha49]. For all large n, some truth table of a function on n inputs is a no-instance of MCSP at threshold 2 ^ n / n.