Nondeterministic circuit lower bounds

A verifier has n ordinary inputs and k existential witness inputs, with no restriction on k. Hiding the witnesses preserves the compiler graph and its degree and size bounds. The cycle count still subtracts every reachable ordinary input. The same dense rectangle-free families therefore have the same lower bound, uniformly in the number of witness inputs.

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

A verifier accepts an ordinary input exactly when some witness makes its output accepting.

Equations

• Complexity.Frontier.NondeterministicDecides c I Acc S = ∀ (x : Fin n → U), x ∈ S ↔ ∃ (y : Fin k → U), c.eval I (Fin.append x y) 0 ∈ Acc

theorem Complexity.Frontier.exists_graph_of_nondeterministic_decides {U : Type u} {σ : Cslib.Circuits.Signature} {n k : ℕ} [Finite U] [Nontrivial U] {I : Cslib.Circuits.Interpretation σ U} {Acc : Set U} {c : Cslib.Circuits.Circuit σ (n + k) 1} {S : Set (Fin n → U)} {K r : ℕ} (hr : 2 ≤ r) (hfan : c.FanInAtMost r) (hS : NondeterministicDecides c I Acc S) (hfree : RectangleFree S K) (hbig : Nat.card U * K ^ 2 ≤ S.ncard) : ∃ (V : Type) (E : Type) (_ : Finite V) (_ : Finite E) (G : Multigraph V E), G.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) (w : ℕ), (∀ (t : ℕ), (G.cut (π.initial t)).ncard ≤ w) → Real.logb ↑(Nat.card U) ↑S.ncard ≤ ↑w + (↑r + 2) + 3 * Real.logb ↑(Nat.card U) ↑K + Real.logb (↑(Nat.card U)) (↑(Nat.card V) + 1)

The compiler graph of a verifier, after hiding witnesses, has the same reduction bounds as an ordinary circuit. The subtraction counts only ordinary inputs.

theorem Complexity.Frontier.lowerBound_nondeterministic {U : Type u} [Finite U] [Nontrivial U] {r : ℕ} (hr : 2 ≤ r) {A : ℝ} (hA : 0 < A) (hlayout : LayoutBound (r + 1) A) (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 : ℕ) (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ U) (Acc : Set U) (c : Cslib.Circuits.Circuit σ (n + k) 1), c.FanInAtMost r → NondeterministicDecides c I Acc (S n) → (1 + 1 / A - ε) * ↑n < (↑r - 1) * ↑c.innerSize

The frontier lower bound for verifiers, uniformly in the number of existential inputs.

theorem Complexity.Frontier.lowerBound_nondeterministic_gaussian {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 : ℕ) (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ U) (Acc : Set U) (c : Cslib.Circuits.Circuit σ (n + k) 1), c.FanInAtMost 2 → NondeterministicDecides c I Acc (S n) → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑n < ↑c.innerSize

The Gaussian coefficient also holds for nondeterministic circuits of fan-in two.