General bounded-round Karchmer--Wigderson protocols

RoundProtocol ι M d sends at most d messages from the alphabet M. Its output names a differing coordinate, with no monotonicity restriction. TopDown develops the density-rectangle adversary for this model.

theorem Complexity.KarchmerWigderson.RoundProtocol.run_swapPlayers {ι : Type u_1} {M : Type u_2} {d : ℕ} (P : RoundProtocol ι M d) (x y : ι → Bool) : P.swapPlayers.run x y = P.run y x

Swapping all speakers swaps the input arguments to the protocol's run.

theorem Complexity.KarchmerWigderson.RoundProtocol.SolvesKW.swapPlayers {ι : Type u_1} {M : Type u_2} {d : ℕ} {P : RoundProtocol ι M d} {f : (ι → Bool) → Bool} (h : P.SolvesKW f) : P.swapPlayers.SolvesKW fun (x : ι → Bool) => !f x

Player swapping gives a protocol for the complemented function.