A circuit gives a bounded-round general KW protocol #
The standard Karchmer--Wigderson translation, as used in Section 1.1 of Oliver Korten, Top-Down Lower Bounds for All Depths, ECCC TR26-221 (2026), https://eccc.weizmann.ac.il/report/2026/221/.
Descend through a gate input selected by the appropriate player. Every gate has fan-in at most the circuit's total input-wire count. Negated wires swap the players without an extra message. Empty gates have constant value and therefore an empty KW relation; an arbitrary coordinate is a valid answer.
theorem
Complexity.KarchmerWigderson.RoundProtocol.exists_negated_internal
{ι : Type u_1}
{M : Type u_2}
{d : ℕ}
{P : RoundProtocol ι M d}
{f : (ι → Bool) → Bool}
(h : P.SolvesKW f)
(b : Bool)
:
∃ (Q : RoundProtocol ι M d), Q.SolvesKW fun (x : ι → Bool) => b ^^ f x
theorem
Complexity.KarchmerWigderson.RoundProtocol.exists_or_protocol_internal
{ι : Type u_1}
(i0 : ι)
{W a d : ℕ}
(ha : a ≤ W)
(f : Fin a → (ι → Bool) → Bool)
(child : Fin a → RoundProtocol ι (Fin W) d)
(hchild : ∀ (j : Fin a), (child j).SolvesKW (f j))
:
∃ (P : RoundProtocol ι (Fin W) (d + 1)), P.SolvesKW fun (x : ι → Bool) => AndOrOp.or.eval a fun (j : Fin a) => f j x
theorem
Complexity.KarchmerWigderson.RoundProtocol.exists_and_protocol_internal
{ι : Type u_1}
(i0 : ι)
{W a d : ℕ}
(ha : a ≤ W)
(f : Fin a → (ι → Bool) → Bool)
(child : Fin a → RoundProtocol ι (Fin W) d)
(hchild : ∀ (j : Fin a), (child j).SolvesKW (f j))
:
∃ (P : RoundProtocol ι (Fin W) (d + 1)), P.SolvesKW fun (x : ι → Bool) => AndOrOp.and.eval a fun (j : Fin a) => f j x
theorem
Complexity.KarchmerWigderson.RoundProtocol.exists_coded_or_protocol_internal
{ι : Type u_1}
{α : Type u_2}
(i0 : ι)
{a d : ℕ}
(code : Fin a → α)
(F : α → (ι → Bool) → Bool)
(child : α → RoundProtocol ι α d)
(hchild : ∀ (j : Fin a), (child (code j)).SolvesKW (F (code j)))
:
∃ (P : RoundProtocol ι α (d + 1)), P.SolvesKW fun (x : ι → Bool) => AndOrOp.or.eval a fun (j : Fin a) => F (code j) x
theorem
Complexity.KarchmerWigderson.RoundProtocol.exists_coded_and_protocol_internal
{ι : Type u_1}
{α : Type u_2}
(i0 : ι)
{a d : ℕ}
(code : Fin a → α)
(F : α → (ι → Bool) → Bool)
(child : α → RoundProtocol ι α d)
(hchild : ∀ (j : Fin a), (child (code j)).SolvesKW (F (code j)))
:
∃ (P : RoundProtocol ι α (d + 1)), P.SolvesKW fun (x : ι → Bool) => AndOrOp.and.eval a fun (j : Fin a) => F (code j) x
theorem
Complexity.Circuit.gate_fanIn_le_total_internal
{N M G : ℕ}
[NeZero N]
[NeZero M]
(c : Circuit Basis.unboundedAndOr N M G)
(i : Fin G)
:
theorem
Complexity.Circuit.output_fanIn_le_total_internal
{N M G : ℕ}
[NeZero N]
[NeZero M]
(c : Circuit Basis.unboundedAndOr N M G)
(i : Fin M)
:
theorem
Complexity.Circuit.exists_input_protocol_internal
{N M G : ℕ}
[NeZero N]
[NeZero M]
(c : Circuit Basis.unboundedAndOr N M G)
(d : ℕ)
(w : Fin (N + G))
(hw : ↑w < N)
:
∃ (P : KarchmerWigderson.RoundProtocol (Fin N) (Fin c.totalFanIn) d),
P.SolvesKW fun (x : Fin N → Bool) => c.wireValue x w
theorem
Complexity.Circuit.exists_wire_protocol_internal
{N M G : ℕ}
[NeZero N]
[NeZero M]
(c : Circuit Basis.unboundedAndOr N M G)
(d : ℕ)
(w : Fin (N + G))
(hw : c.wireDepth w ≤ d)
:
∃ (P : KarchmerWigderson.RoundProtocol (Fin N) (Fin c.totalFanIn) d),
P.SolvesKW fun (x : Fin N → Bool) => c.wireValue x w
theorem
Complexity.Circuit.exists_roundProtocol_internal
{N M G : ℕ}
[NeZero N]
[NeZero M]
(c : Circuit Basis.unboundedAndOr N M G)
(d : ℕ)
(hd : c.depth ≤ d)
(j : Fin M)
:
∃ (P : KarchmerWigderson.RoundProtocol (Fin N) (Fin c.totalFanIn) d), P.SolvesKW fun (x : Fin N → Bool) => c.eval x j
theorem
Complexity.Circuit.exists_input_protocol_of_gates_internal
{N M G : ℕ}
[NeZero N]
[NeZero M]
(c : Circuit Basis.unboundedAndOr N M G)
(d : ℕ)
(w : Fin (N + G))
(hw : ↑w < N)
: