The frontier lower bound for nondeterministic circuits

A nondeterministic circuit has n ordinary inputs and k witness inputs. It decides a set S ⊆ U^n when an input x lies in S exactly if some witness y ∈ U^k makes the output on (x, y) accepting (Circuit.NondeterministicDecides). The number k of witness inputs is arbitrary. A circuit deciding S is a nondeterministic circuit without witness inputs (Circuit.Decides.nondeterministicDecides).

Hiding the witness inputs of the constraint network of a circuit (Compiler.hiddenNetwork) gives a network on the same graph that accepts exactly S and reads no more inputs. So the graph keeps its degree bound and its number of vertices, and its cycle rank and the number of ordinary inputs read still add up to at most (r - 1) s + 1. The support lemma and frontier demand apply to the hidden network as to any network, and the reduction theorem holds with the same bounds (exists_graph_of_nondeterministicDecides): only the n ordinary inputs are subtracted from the cycle rank. The frontier lower bound follows with the same coefficient as for deterministic circuits, uniformly in the number of witness inputs:

(r - 1) s > (1 + 1/A - ε) n

under the layout hypothesis LayoutBound (r + 1) A (eventually_lt_mul_innerSize_of_nondeterministicDecides), (r - 1) s > (2 - ε) n unconditionally (eventually_two_sub_mul_lt_mul_innerSize_of_nondeterministicDecides), and at fan-in two s > (L - ε) n with L = 1 + π / (3 arccos ((1 + 2√2)/4)) ≈ 4.5625 (eventually_gaussian_sub_mul_lt_innerSize_of_nondeterministicDecides).

Main definitions

• Cslib.Circuits.Circuit.NondeterministicDecides: a circuit with n + k inputs and one output decides a set of inputs on n coordinates, the last k inputs being witnesses.
• Cslib.Circuits.Frontier.Compiler.hiddenNetwork: the constraint network of a circuit with its last k inputs hidden.

Main results

• Cslib.Circuits.Frontier.Compiler.accepted_hiddenNetwork: exactness of the hidden network.
• Cslib.Circuits.Frontier.exists_graph_of_nondeterministicDecides: the reduction theorem for nondeterministic circuits.
• Cslib.Circuits.Frontier.eventually_lt_mul_innerSize_of_nondeterministicDecides: the frontier lower bound for nondeterministic circuits, conditional on the layout hypothesis.
• Cslib.Circuits.Frontier.eventually_two_sub_mul_lt_mul_innerSize_of_nondeterministicDecides: the unconditional frontier lower bound for nondeterministic circuits.
• Cslib.Circuits.Frontier.eventually_gaussian_sub_mul_lt_innerSize_of_nondeterministicDecides: the Gaussian (L - ε) n frontier lower bound for nondeterministic circuits of fan-in two.

def Cslib.Circuits.Circuit.NondeterministicDecides {σ : Signature} {U : Type u_1} {n k : ℕ} (c : Circuit σ (n + k) 1) (I : Interpretation σ U) (Acc : Set U) (S : Set (Fin n → U)) : Prop

A circuit with n + k inputs and one output decides S nondeterministically, accepting the values in Acc, when an input x on n coordinates lies in S exactly if for some witness y on the last k coordinates, the output of the circuit on (x, y) lies in Acc.

theorem Cslib.Circuits.Circuit.Decides.nondeterministicDecides {σ : Signature} {U : Type u_1} {n : ℕ} {c : Circuit σ n 1} {I : Interpretation σ U} {Acc : Set U} {S : Set (Fin n → U)} (h : c.Decides I Acc S) : c.NondeterministicDecides I Acc S

A circuit deciding a set decides it nondeterministically, with no witness inputs.

The hidden network of a circuit

noncomputable def Cslib.Circuits.Frontier.Compiler.hiddenNetwork {σ : Signature} {U : Type u_1} {n k m : ℕ} (c : Circuit σ (n + k) m) (I : Interpretation σ U) (Acc : Fin m → Set U) : Network U (Fin n) (Vertex c) (Edge c)

The hidden network of a circuit with n + k inputs: its constraint network, accepting at the output o the values in Acc o, with the last k inputs hidden.

@[simp]

theorem Cslib.Circuits.Frontier.Compiler.hiddenNetwork_toMultigraph {σ : Signature} {U : Type u_1} {n k m : ℕ} (c : Circuit σ (n + k) m) (I : Interpretation σ U) (Acc : Fin m → Set U) : (hiddenNetwork c I Acc).toMultigraph = graph c

theorem Cslib.Circuits.Frontier.Compiler.accepted_hiddenNetwork {σ : Signature} {U : Type u_1} {n k m : ℕ} (c : Circuit σ (n + k) m) (I : Interpretation σ U) (Acc : Fin m → Set U) [Nonempty U] : (hiddenNetwork c I Acc).accepted = {x : Fin n → U | ∃ (y : Fin k → U), ∀ (o : Fin m), c.eval I (Fin.append x y) o ∈ Acc o}

Exactness of the hidden network. It accepts an input x exactly when some values y of the last k inputs make every output o of the circuit on (x, y) lie in Acc o.

theorem Cslib.Circuits.Frontier.Compiler.ncard_readAt_hiddenNetwork_le {σ : Signature} {U : Type u_1} {n k m : ℕ} (c : Circuit σ (n + k) m) (I : Interpretation σ U) (Acc : Fin m → Set U) (v : Vertex c) : ((hiddenNetwork c I Acc).readAt v).ncard ≤ 1

Each vertex of the hidden network reads at most one input.

theorem Cslib.Circuits.Frontier.Compiler.ncard_read_hiddenNetwork_le {σ : Signature} {U : Type u_1} {n k m : ℕ} (c : Circuit σ (n + k) m) (I : Interpretation σ U) (Acc : Fin m → Set U) : (hiddenNetwork c I Acc).read.ncard ≤ (network c I Acc).read.ncard

The hidden network reads no more inputs than the network of the circuit.

theorem Cslib.Circuits.Frontier.Compiler.cycleRank_add_ncard_read_hiddenNetwork_le {σ : Signature} {U : Type u_1} {n k m : ℕ} (c : Circuit σ (n + k) m) (I : Interpretation σ U) (Acc : Fin m → Set U) {r : ℕ} (hfan : c.FanInAtMost r) (hconn : (graph c).toSimpleGraph.Connected) : (graph c).cycleRank + (hiddenNetwork c I Acc).read.ncard ≤ (r - 1) * c.innerSize + 1

The cycle rank. For fan-in at most r, if the graph of the circuit is connected, its cycle rank and the number of ordinary inputs read by the hidden network add up to at most (r - 1) s + 1, where s counts the inner gates.

The reduction theorem for nondeterministic circuits

theorem Cslib.Circuits.Frontier.accepted_hiddenNetwork_of_nondeterministicDecides {σ : Signature} {U : Type u_1} {n k : ℕ} {I : Interpretation σ U} {Acc : Set U} {c : Circuit σ (n + k) 1} {S : Set (Fin n → U)} [Nonempty U] (hS : c.NondeterministicDecides I Acc S) : (Compiler.hiddenNetwork c I fun (x : Fin 1) => Acc).accepted = S

The hidden network of a circuit deciding S nondeterministically accepts exactly S.

theorem Cslib.Circuits.Frontier.cycleRank_le_of_nondeterministicDecides {σ : Signature} {U : Type u_1} {n k : ℕ} {I : Interpretation σ U} {Acc : Set U} {c : Circuit σ (n + k) 1} {S : Set (Fin n → U)} {K r : ℕ} [Finite U] [Nontrivial U] (hfan : c.FanInAtMost r) (hS : c.NondeterministicDecides I Acc S) (hfree : RectangleFree S K) (hbig : Nat.card U * K ^ 2 ≤ S.ncard) : ↑(Compiler.graph c).cycleRank ≤ (↑r - 1) * ↑c.innerSize - ↑n + Real.logb ↑(Nat.card U) ↑K + 1

The cycle rank of the graph of a nondeterministic circuit deciding a large K-rectangle-free set S ⊆ U^n is at most (r - 1) s - n + log_q K + 1 for fan-in at most r, where s counts the inner gates. Only the n ordinary inputs are subtracted.

theorem Cslib.Circuits.Frontier.logb_ncard_le_width_of_nondeterministicDecides {σ : Signature} {U : Type u_1} {n k : ℕ} {I : Interpretation σ U} {Acc : Set U} {c : Circuit σ (n + k) 1} {S : Set (Fin n → U)} {K r : ℕ} [Finite U] [Nontrivial U] (hr : 2 ≤ r) (hfan : c.FanInAtMost r) (hS : c.NondeterministicDecides I Acc S) (hfree : RectangleFree S K) (hbig : Nat.card U * K ^ 2 ≤ S.ncard) (π : Layout (Compiler.Vertex c)) : Real.logb ↑(Nat.card U) ↑S.ncard ≤ ↑((Compiler.graph c).width π) + (↑r + 2) + 3 * Real.logb ↑(Nat.card U) ↑K + Real.logb (↑(Nat.card U)) (↑(Nat.card (Compiler.Vertex c)) + 1)

Every layout of the graph of a nondeterministic circuit is wide. For a circuit of fan-in at most r ≥ 2 deciding a large K-rectangle-free set S nondeterministically, every layout π of its graph satisfies log_q |S| ≤ width π + (r + 2) + 3 log_q K + log_q (|V| + 1).

theorem Cslib.Circuits.Frontier.exists_graph_of_nondeterministicDecides {σ : Signature} {U : Type u_1} {n k : ℕ} {I : Interpretation σ U} {Acc : Set U} {c : Circuit σ (n + k) 1} {S : Set (Fin n → U)} {K r : ℕ} [Finite U] [Nontrivial U] (hr : 2 ≤ r) (hfan : c.FanInAtMost r) (hS : c.NondeterministicDecides I Acc S) (hfree : RectangleFree S K) (hbig : Nat.card U * K ^ 2 ≤ S.ncard) : ∃ (V : Type) (E : Type) (_ : Finite V) (x : Finite E) (G : Multigraph V E), G.toSimpleGraph.Connected ∧ G.Loopless ∧ G.MaxDegreeLE (r + 1) ∧ Nat.card V ≤ 2 * r * c.innerSize + 3 ∧ ↑G.cycleRank ≤ (↑r - 1) * ↑c.innerSize - ↑n + Real.logb ↑(Nat.card U) ↑K + 1 ∧ ∀ (π : Layout V), Real.logb ↑(Nat.card U) ↑S.ncard ≤ ↑(G.width π) + (↑r + 2) + 3 * Real.logb ↑(Nat.card U) ↑K + Real.logb (↑(Nat.card U)) (↑(Nat.card V) + 1)

The reduction theorem for nondeterministic circuits. A circuit with s inner gates of fan-in at most r ≥ 2, over any basis on U, with n ordinary and any number of witness inputs, deciding a K-rectangle-free set S ⊆ U^n nondeterministically with |S| ≥ q K ^ 2, where q = |U| ≥ 2, yields a connected, loopless multigraph of maximum degree r + 1 with at most 2 r s + 3 vertices and cycle rank at most (r - 1) s - n + log_q K + 1, every layout of which has width at least log_q |S| - 3 log_q K - log_q (|V| + 1) - (r + 2).

The lower bounds

theorem Cslib.Circuits.Frontier.eventually_lt_mul_innerSize_of_nondeterministicDecides {U : Type u} [Finite U] [Nontrivial U] {S : (n : ℕ) → Set (Fin n → U)} {K : ℕ → ℕ} {r : ℕ} (hr : 2 ≤ r) {A : ℝ} (hA : 0 < A) (hlayout : LayoutBound (r + 1) A) (hfree : ∀ᶠ (n : ℕ) in Filter.atTop, RectangleFree (S n) (K n)) (hK : (fun (n : ℕ) => Real.log ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hdense : (fun (n : ℕ) => ↑n * Real.log ↑(Nat.card U) - Real.log ↑(S n).ncard) =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (k : ℕ) (σ : Signature) (I : Interpretation σ U) (Acc : Set U) (c : Circuit σ (n + k) 1), c.FanInAtMost r → c.NondeterministicDecides I Acc (S n) → (1 + 1 / A - ε) * ↑n < (↑r - 1) * ↑c.innerSize

The frontier lower bound for nondeterministic circuits. Let r ≥ 2 and assume the layout hypothesis for maximum degree r + 1 with coefficient A > 0. Let S_n ⊆ U^n be K_n-rectangle-free sets over a finite alphabet U with at least two symbols, with log K_n = o(n) and n log |U| - log |S_n| = o(n). Then for every ε > 0 and all large n, every circuit of fan-in at most r with any number k of witness inputs deciding S_n nondeterministically, over any basis and interpretation on U, has s inner gates with (r - 1) s > (1 + 1/A - ε) n.

theorem Cslib.Circuits.Frontier.eventually_lt_innerSize_of_nondeterministicDecides {U : Type u} [Finite U] [Nontrivial U] {S : (n : ℕ) → Set (Fin n → U)} {K : ℕ → ℕ} {A : ℝ} (hA : 0 < A) (hlayout : LayoutBound 3 A) (hfree : ∀ᶠ (n : ℕ) in Filter.atTop, RectangleFree (S n) (K n)) (hK : (fun (n : ℕ) => Real.log ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hdense : (fun (n : ℕ) => ↑n * Real.log ↑(Nat.card U) - Real.log ↑(S n).ncard) =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (k : ℕ) (σ : Signature) (I : Interpretation σ U) (Acc : Set U) (c : Circuit σ (n + k) 1), c.FanInAtMost 2 → c.NondeterministicDecides I Acc (S n) → (1 + 1 / A - ε) * ↑n < ↑c.innerSize

The frontier lower bound for nondeterministic circuits of fan-in two. Assume the layout hypothesis for subcubic graphs with coefficient A > 0. Under the hypotheses of eventually_lt_mul_innerSize_of_nondeterministicDecides, for every ε > 0 and all large n, every circuit of fan-in at most two with any number of witness inputs deciding S_n nondeterministically, over any basis and interpretation on U, has more than (1 + 1/A - ε) n inner gates.

theorem Cslib.Circuits.Frontier.eventually_two_sub_mul_lt_mul_innerSize_of_nondeterministicDecides {U : Type u} [Finite U] [Nontrivial U] {S : (n : ℕ) → Set (Fin n → U)} {K : ℕ → ℕ} {r : ℕ} (hr : 2 ≤ r) (hfree : ∀ᶠ (n : ℕ) in Filter.atTop, RectangleFree (S n) (K n)) (hK : (fun (n : ℕ) => Real.log ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hdense : (fun (n : ℕ) => ↑n * Real.log ↑(Nat.card U) - Real.log ↑(S n).ncard) =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (k : ℕ) (σ : Signature) (I : Interpretation σ U) (Acc : Set U) (c : Circuit σ (n + k) 1), c.FanInAtMost r → c.NondeterministicDecides I Acc (S n) → (2 - ε) * ↑n < (↑r - 1) * ↑c.innerSize

The unconditional frontier lower bound for nondeterministic circuits. Let r ≥ 2, and let S_n ⊆ U^n be K_n-rectangle-free sets over a finite alphabet U with at least two symbols, with log K_n = o(n) and n log |U| - log |S_n| = o(n). Then for every ε > 0 and all large n, every circuit of fan-in at most r with any number of witness inputs deciding S_n nondeterministically, over any basis and interpretation on U, has s inner gates with (r - 1) s > (2 - ε) n.

theorem Cslib.Circuits.Frontier.eventually_two_sub_mul_lt_innerSize_of_nondeterministicDecides {U : Type u} [Finite U] [Nontrivial U] {S : (n : ℕ) → Set (Fin n → U)} {K : ℕ → ℕ} (hfree : ∀ᶠ (n : ℕ) in Filter.atTop, RectangleFree (S n) (K n)) (hK : (fun (n : ℕ) => Real.log ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hdense : (fun (n : ℕ) => ↑n * Real.log ↑(Nat.card U) - Real.log ↑(S n).ncard) =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (k : ℕ) (σ : Signature) (I : Interpretation σ U) (Acc : Set U) (c : Circuit σ (n + k) 1), c.FanInAtMost 2 → c.NondeterministicDecides I Acc (S n) → (2 - ε) * ↑n < ↑c.innerSize

The unconditional frontier lower bound for nondeterministic circuits of fan-in two. Under the hypotheses of eventually_two_sub_mul_lt_mul_innerSize_of_nondeterministicDecides, for every ε > 0 and all large n, every circuit of fan-in at most two with any number of witness inputs deciding S_n nondeterministically, over any basis and interpretation on U, has more than (2 - ε) n inner gates.

theorem Cslib.Circuits.Frontier.eventually_gaussian_sub_mul_lt_innerSize_of_nondeterministicDecides {U : Type u} [Finite U] [Nontrivial U] {S : (n : ℕ) → Set (Fin n → U)} {K : ℕ → ℕ} (hfree : ∀ᶠ (n : ℕ) in Filter.atTop, RectangleFree (S n) (K n)) (hK : (fun (n : ℕ) => Real.log ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hdense : (fun (n : ℕ) => ↑n * Real.log ↑(Nat.card U) - Real.log ↑(S n).ncard) =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (k : ℕ) (σ : Signature) (I : Interpretation σ U) (Acc : Set U) (c : Circuit σ (n + k) 1), c.FanInAtMost 2 → c.NondeterministicDecides I Acc (S n) → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑n < ↑c.innerSize

The Gaussian frontier lower bound for nondeterministic circuits of fan-in two. Under the hypotheses of eventually_two_sub_mul_lt_innerSize_of_nondeterministicDecides, for every ε > 0 and all large n, every circuit of fan-in at most two with any number of witness inputs deciding S_n nondeterministically, over any basis and interpretation on U, has more than (L - ε) n inner gates, where L = 1 + π / (3 arccos ((1 + 2√2)/4)) ≈ 4.5625.