The circuit size hierarchy

Changing one value of a Boolean function on n inputs changes its circuit complexity by at most 2 n + 3 (complexity_update_le). Walking from a constant function, which costs exactly one gate (complexity_const), to a hard one, one value at a time, the complexity therefore takes every value up to the complexity of the hard function, up to 2 n + 3 (exists_complexity_mem_Ioc). With Shannon's lower bound [Sha49], every size below 2 ^ n / n is the complexity of some function, up to 2 n + 3, and so more gates allow strictly more languages (SIZE_ssubset). Walking from a constant function to any function f shows that f costs at most 2 ^ n (2 n + 3) + 1 gates (complexity_le_two_pow_mul_add_one).

Main results

• Cslib.Circuits.Boolean.complexity_const: a constant costs exactly one gate.
• Cslib.Circuits.Boolean.complexity_update_le: changing one value costs 2 n + 3 gates.
• Cslib.Circuits.Boolean.complexity_le_two_pow_mul_add_one, Cslib.Circuits.Boolean.complexity_le_of_dependsOn: the truth-table bound, for all functions and for functions depending on few inputs.
• Cslib.Circuits.Boolean.exists_complexity_mem_Ioc: complexities below that of a given function are attained, up to 2 n + 3.
• Cslib.Circuits.Boolean.SIZE_ssubset: the size hierarchy.
• Cslib.Circuits.Boolean.SIZE_pow_ssubset: SIZE ((n + 1) ^ k) ⊂ SIZE ((n + 1) ^ (k + 1)).

References

• C. E. Shannon, The synthesis of two-terminal switching circuits

theorem Cslib.Circuits.Boolean.complexity_update_le {n : ℕ} (f : BooleanFunction n) (a : Fin n → Bool) (b : Bool) : complexity interpretation (single (Function.update f a b)) ≤ complexity interpretation (single f) + (2 * n + 3)

Changing one value of a Boolean function costs at most 2 n + 3 gates.

theorem Cslib.Circuits.Boolean.complexity_le_two_pow_mul_add_one {n : ℕ} (f : BooleanFunction n) : complexity interpretation (single f) ≤ 2 ^ n * (2 * n + 3) + 1

The truth-table bound. A Boolean function on n inputs costs at most 2 ^ n * (2 * n + 3) + 1 gates: start from a constant and change one value at a time.

theorem Cslib.Circuits.Boolean.complexity_le_of_dependsOn {n : ℕ} {f : BooleanFunction n} {s : Finset (Fin n)} (hf : DependsOn f ↑s) : complexity interpretation (single f) ≤ 2 ^ s.card * (2 * s.card + 3) + 1

A Boolean function that depends only on the inputs in s costs at most 2 ^ #s * (2 * #s + 3) + 1 gates.

theorem Cslib.Circuits.Boolean.complexity_const {n : ℕ} (b : Bool) : complexity interpretation (single fun (x : BitString n) => b) = 1

A constant function costs exactly one gate: a circuit without gates outputs an input.

theorem Cslib.Circuits.Boolean.exists_lt_le_add_of_update_le {ι : Type u_1} {α : Type u_2} [Finite ι] [DecidableEq ι] (μ : (ι → α) → ℕ) {B t : ℕ} (hμ : ∀ (w : ι → α) (i : ι) (a : α), μ (Function.update w i a) ≤ μ w + B) {u v : ι → α} (hu : μ u ≤ t) (hv : t < μ v) : ∃ (w : ι → α), t < μ w ∧ μ w ≤ t + B

Discrete intermediate values. If changing one coordinate raises a measure by at most B, and the measure is at most t at u and above t at v, then it lies in (t, t + B] somewhere.

theorem Cslib.Circuits.Boolean.exists_complexity_mem_Ioc {n t : ℕ} (g : BooleanFunction n) (hg : t < complexity interpretation (single g)) : ∃ (f : BooleanFunction n), t < complexity interpretation (single f) ∧ complexity interpretation (single f) ≤ t + (2 * n + 3)

Every complexity below that of a given function is exceeded by at most 2 n + 3 by the complexity of some function.

theorem Cslib.Circuits.Boolean.SIZE_ssubset {s t : ℕ → ℕ} (hst : s ≤ t) (ht : ∀ (n : ℕ), 1 ≤ t n) (hgap : ∀ᶠ (n : ℕ) in Filter.atTop, s n + (2 * n + 3) ≤ t n) (hs : ∃ᶠ (n : ℕ) in Filter.atTop, ↑(s n) < 2 ^ n / ↑n) : SIZE s ⊂ SIZE t

The circuit size hierarchy. If s ≤ t, t is positive, eventually s n + 2 n + 3 ≤ t n, and infinitely often s n < 2 ^ n / n, then some language has circuits of size t but not of size s.

theorem Cslib.Circuits.Boolean.SIZE_pow_ssubset {k : ℕ} (hk : 1 ≤ k) : (SIZE fun (n : ℕ) => (n + 1) ^ k) ⊂ SIZE fun (n : ℕ) => (n + 1) ^ (k + 1)

The polynomial size hierarchy. For k ≥ 1, circuits of size (n + 1) ^ (k + 1) decide strictly more languages than circuits of size (n + 1) ^ k.