Counting hard sparse functions

The graphs of all maps from p bits to p bits have exactly 2 ^ p points and give 2 ^ (p * 2 ^ p) distinct scalar functions on 2 * p bits. Even the circuit count without its factorial saving proves that some graph needs more than 2 ^ (p - 4) gates, for every p ≥ 4.

noncomputable def Complexity.CircuitSparseSynthesis.Internal.graphSupport {p : ℕ} (f : (Fin p → Bool) → Fin p → Bool) : Finset (Fin (p + p) → Bool)

A graph, viewed as a sparse set of inputs on two equal blocks.

Equations

• Complexity.CircuitSparseSynthesis.Internal.graphSupport f = Finset.image (fun (x : Fin p → Bool) => Fin.append x (f x)) Finset.univ

def Complexity.CircuitSparseSynthesis.Internal.graphFunction {p : ℕ} (f : (Fin p → Bool) → Fin p → Bool) : Cslib.BooleanFunction (p + p)

Membership in the graph of a map on bit strings.

Equations

• Complexity.CircuitSparseSynthesis.Internal.graphFunction f x = decide ((fun (j : Fin p) => x (Fin.natAdd p j)) = f fun (j : Fin p) => x (Fin.castAdd p j))

theorem Complexity.CircuitSparseSynthesis.Internal.card_graphSupport {p : ℕ} (f : (Fin p → Bool) → Fin p → Bool) : (graphSupport f).card = 2 ^ p

theorem Complexity.CircuitSparseSynthesis.Internal.indicator_graphSupport {p : ℕ} (f : (Fin p → Bool) → Fin p → Bool) : Cslib.Circuits.Boolean.Correction.indicator ↑(graphSupport f) = fun (x : Cslib.BitString (p + p)) (x_1 : Fin 1) => graphFunction f x

theorem Complexity.CircuitSparseSynthesis.Internal.graphFunction_injective (p : ℕ) : Function.Injective graphFunction

theorem Complexity.CircuitSparseSynthesis.Internal.circuit_count_lt_graph_count {p : ℕ} (large : 4 ≤ p) : (Cslib.Circuits.Boolean.computableFunctions (p + p) (2 ^ (p - 4))).card < 2 ^ (p * 2 ^ p)

theorem Complexity.CircuitSparseSynthesis.Internal.exists_hard_graph {p : ℕ} (large : 4 ≤ p) : ∃ (domain : Finset (Fin (p + p) → Bool)), domain.card = 2 ^ p ∧ 2 ^ (p - 4) < Cslib.Circuits.complexity Cslib.Circuits.Boolean.interpretation (Cslib.Circuits.Boolean.Correction.indicator ↑domain)