Karchmer--Wigderson protocols -- proof internals

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

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

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

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

def Complexity.KarchmerWigderson.Protocol.ofFormulaInternal {N : ℕ} (formula : MonotoneFormula N) {zeroInputs oneInputs : Set (BitString N)} (zeroInvariant : ∀ input ∈ zeroInputs, MonotoneFormula.eval input formula = false) (oneInvariant : ∀ input ∈ oneInputs, MonotoneFormula.eval input formula = true) : Protocol N zeroInputs oneInputs

Internal formula-to-protocol construction under arbitrary rectangle invariants.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.KarchmerWigderson.Protocol.depth_ofFormulaInternal {N : ℕ} (formula : MonotoneFormula N) {zeroInputs oneInputs : Set (BitString N)} (zeroInvariant : ∀ input ∈ zeroInputs, MonotoneFormula.eval input formula = false) (oneInvariant : ∀ input ∈ oneInputs, MonotoneFormula.eval input formula = true) : (ofFormulaInternal formula zeroInvariant oneInvariant).depth = formula.depth

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

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

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