Circuit depth and wires bound KW rounds and message alphabets #
This is the general Karchmer--Wigderson translation for the library's
unbounded-fan-in AND/OR circuits, including free negation flags on gate inputs.
totalFanIn counts every gate-input occurrence, including output gates and
repeated wires. The protocol has no more rounds than the circuit has layers.
theorem
Complexity.Circuit.exists_roundProtocol
{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
A depth-d unbounded AND/OR circuit gives a general KW protocol with
at most d messages, each drawn from an alphabet of size totalFanIn.
This holds for each output, including constants and negated internal wires.
theorem
Complexity.Circuit.exists_roundProtocol_of_gates
{N M G : ℕ}
[NeZero N]
[NeZero M]
(c : Circuit Basis.unboundedAndOr N M G)
(d : ℕ)
(hd : c.depth ≤ d)
(j : Fin M)
:
A depth-d unbounded AND/OR circuit with N inputs and G internal gates
gives a general KW protocol with at most d messages, each drawn from an
alphabet of size 2 * (N + G) encoding a wire and its negation flag.