The monotone Karchmer--Wigderson correspondence

The protocol model tracks its zero-input and one-input rectangles in the type. Alice partitions the one-input side, Bob partitions the zero-input side, and a leaf supplies one coordinate separating the whole remaining rectangle.

The translations are depth-exact:

• Alice nodes become disjunctions and Bob nodes become conjunctions.
• A monotone formula recursively gives a protocol of the same depth.

Consequently a Boolean function has a depth-d monotone formula exactly when its root Karchmer--Wigderson relation has a depth-d protocol in this model. No uniformity condition is present.

theorem Complexity.KarchmerWigderson.Protocol.eval_toFormula_eq_false {N : ℕ} {zeroInputs oneInputs : Set (BitString N)} (protocol : Protocol N zeroInputs oneInputs) {input : BitString N} (hinput : input ∈ zeroInputs) : MonotoneFormula.eval input protocol.toFormula = false

A protocol's formula is false throughout its zero-input rectangle.

theorem Complexity.KarchmerWigderson.Protocol.eval_toFormula_eq_true {N : ℕ} {zeroInputs oneInputs : Set (BitString N)} (protocol : Protocol N zeroInputs oneInputs) {input : BitString N} (hinput : input ∈ oneInputs) : MonotoneFormula.eval input protocol.toFormula = true

A protocol's formula is true throughout its one-input rectangle.

theorem Complexity.KarchmerWigderson.Protocol.depth_toFormula {N : ℕ} {zeroInputs oneInputs : Set (BitString N)} (protocol : Protocol N zeroInputs oneInputs) : protocol.toFormula.depth = protocol.depth

Protocol-to-formula translation preserves depth exactly.

theorem Complexity.KarchmerWigderson.Protocol.toFormula_computes {N : ℕ} (function : BitString N → Bool) (protocol : RootProtocol function) : (toFormula protocol).Computes function

The formula extracted from a root protocol computes the underlying function.

theorem Complexity.KarchmerWigderson.Protocol.exists_protocol_of_formula {N : ℕ} (formula : MonotoneFormula N) (function : BitString N → Bool) (computes : formula.Computes function) : ∃ (protocol : RootProtocol function), depth protocol = formula.depth

Every monotone formula computing function yields a root protocol of exactly the same depth.

theorem Complexity.KarchmerWigderson.Protocol.exists_formula_of_protocol {N : ℕ} (function : BitString N → Bool) (protocol : RootProtocol function) : ∃ (formula : MonotoneFormula N), formula.Computes function ∧ formula.depth = depth protocol

Every root protocol yields a monotone formula of exactly the same depth.

theorem Complexity.KarchmerWigderson.Protocol.exists_protocol_depth_iff_formula_depth {N : ℕ} (function : BitString N → Bool) (depthBound : ℕ) : (∃ (protocol : RootProtocol function), depth protocol ≤ depthBound) ↔ ∃ (formula : MonotoneFormula N), formula.Computes function ∧ formula.depth ≤ depthBound

Monotone Karchmer--Wigderson correspondence. A root protocol of depth at most depthBound exists exactly when a monotone formula of that depth exists.