circuit_depth_conjecture
Provedanalysiscomputational-complexitygraph-theory
Monotone circuit depth conjecture: The minimum depth of a monotone circuit for computing certain monotone functions. Karchmer-Wigderson (1988) connected depth to communication complexity. Exact lower bounds for specific functions (clique) are open.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem circuit_depth_conjecture (n : ℕ) (hn : 1 ≤ n)
(f : (Fin n → Bool) → Bool)
(hmono : ∀ x y : Fin n → Bool, (∀ i, x i = false → y i = false) →
(f x = true → f y = true)) :
∃ (depth : ℕ), depth ≤ 2 * n + 1 ∧
∃ (circuit : (Fin n → Bool) → Bool),
(∀ x, circuit x = f x) := by
sorrySource