46 Communication Complexity — Det Rectangle
46.1 Overview
This module establishes that every deterministic communication protocol induces a monochromatic rectangle partition of the input space \(X \times Y\) into at most \(2^c\) rectangles, where \(c\) is the protocol’s communication complexity. It also derives the fooling-set lower-bound method, showing that the size of any fooling set bounds \(\mathrm{CC}(g)\) from below via \(\lceil \log _2 |S| \rceil \leq \mathrm{CC}(g)\).
46.2 Declarations
Given a set \(R \subseteq X \times Y\), \(\texttt{swapInputSet}(R)\) is the set \(\{ (y, x) \mid (x, y) \in R\} \subseteq Y \times X\) obtained by swapping the two coordinates of every element.
For any set \(R \subseteq X \times Y\) and pair \((y, x) \in Y \times X\), \((y, x) \in \texttt{swapInputSet}(R)\) if and only if \((x, y) \in R\).
For any set \(R \subseteq X \times Y\), applying \(\texttt{swapInputSet}\) twice recovers \(R\): \(\texttt{swapInputSet}(\texttt{swapInputSet}(R)) = R\).
Given maps \(f_X : X' \to X\) and \(f_Y : Y' \to Y\) and a set \(R \subseteq X \times Y\), \(\texttt{preimageInputSet}(f_X, f_Y, R)\) is the set \(\{ (x', y') \in X' \times Y' \mid (f_X(x'), f_Y(y')) \in R\} \), the pullback of \(R\) along the product map \(f_X \times f_Y\).
For maps \(f_X : X' \to X\), \(f_Y : Y' \to Y\), a set \(R \subseteq X \times Y\), and a pair \((x', y') \in X' \times Y'\), we have \((x', y') \in \texttt{preimageInputSet}(f_X, f_Y, R)\) if and only if \((f_X(x'), f_Y(y')) \in R\).
For a protocol \(p\) and sets \(A \subseteq X\), \(B \subseteq Y\), \(\texttt{leafRectanglesAux}(p, A, B)\) is the collection of rectangles induced by the leaves of \(p\) when the reachable inputs are constrained to \(A \times B\). It is defined by structural recursion: an output node yields \(\{ A \times B\} \), while Alice (resp. Bob) nodes split \(A\) (resp. \(B\)) according to the branching function and recurse.
The leaf rectangles of a protocol \(p : \texttt{Protocol}\, X\, Y\, \alpha \) form the collection \(\texttt{leafRectangles}(p) = \texttt{leafRectanglesAux}(p, X, Y)\), i.e. the set of input rectangles induced by the leaves of \(p\) over the full input space \(X \times Y\).
If \(R \in \texttt{leafRectanglesAux}(p, A, B)\), then \(\texttt{swapInputSet}(R) \in \texttt{leafRectanglesAux}(p.\texttt{swap}, B, A)\). This is an internal auxiliary result proved by structural induction on the protocol.
If \(R\) is a leaf rectangle of \(p\), then \(\texttt{swapInputSet}(R)\) is a leaf rectangle of \(p.\texttt{swap}\), the protocol with Alice and Bob’s roles exchanged.
If \(R \in \texttt{leafRectanglesAux}(p, A, B)\) and \(f_X : X' \to X\), \(f_Y : Y' \to Y\), then \(\texttt{preimageInputSet}(f_X, f_Y, R) \in \texttt{leafRectanglesAux}(p.\texttt{comap}(f_X, f_Y),\, f_X^{-1}(A),\, f_Y^{-1}(B))\). This is an internal auxiliary result proved by structural induction.
If \(R\) is a leaf rectangle of \(p\) and \(f_X : X' \to X\), \(f_Y : Y' \to Y\), then \(\texttt{preimageInputSet}(f_X, f_Y, R)\) is a leaf rectangle of \(p.\texttt{comap}(f_X, f_Y)\).
Every element of \(\texttt{leafRectanglesAux}(p, A, B)\) is a combinatorial rectangle, i.e. a set of the form \(A' \times B'\) for some \(A' \subseteq X\), \(B' \subseteq Y\).
For any protocol \(p\) and any \(R \in \texttt{leafRectangles}(p)\), the set \(R\) is a combinatorial rectangle, i.e. \(\texttt{Rectangle.IsRectangle}(R)\) holds.
Every element \(R\) of \(\texttt{leafRectanglesAux}(p, A, B)\) satisfies \(R \subseteq A \times B\).
The union of \(\texttt{leafRectanglesAux}(p, A, B)\) contains \(A \times B\): \(A \times B \subseteq \bigcup \texttt{leafRectanglesAux}(p, A, B)\).
If \(R, S \in \texttt{leafRectanglesAux}(p, A, B)\) and \(R \neq S\), then \(R\) and \(S\) are disjoint subsets of \(X \times Y\).
For any protocol \(p\), the union of all leaf rectangles equals the entire input space: \(\bigcup \texttt{leafRectangles}(p) = X \times Y\).
For any protocol \(p\), if \(R, S \in \texttt{leafRectangles}(p)\) and \(R \neq S\), then \(R\) and \(S\) are disjoint.
If \(R \in \texttt{leafRectanglesAux}(p, A, B)\) and both \((x, y) \in R\) and \((x', y') \in R\), then \(p.\texttt{run}(x, y) = p.\texttt{run}(x', y')\): the protocol outputs the same value at every input in \(R\).
If \(p\) computes \(g : X \to Y \to \alpha \) and \(R \in \texttt{leafRectangles}(p)\), then \(R\) is \(g\)-monochromatic: all inputs in \(R\) receive the same value of \(g\).
For any protocol \(p\) and constraint sets \(A, B\), the number of elements in \(\texttt{leafRectanglesAux}(p, A, B)\) is at most \(2^{p.\texttt{complexity}}\).
For any protocol \(p\) and constraint sets \(A, B\), the collection \(\texttt{leafRectanglesAux}(p, A, B)\) is a finite set.
For any protocol \(p\) with communication complexity \(c = p.\texttt{complexity}\), the number of leaf rectangles satisfies \(|\texttt{leafRectangles}(p)| \leq 2^c\).
For any protocol \(p\), the set \(\texttt{leafRectangles}(p)\) is finite.
If \(p\) computes \(g : X \to Y \to \alpha \), then the collection \(\texttt{leafRectangles}(p)\) is a monochromatic rectangle partition of \(X \times Y\) with respect to \(g\): every element is a rectangle, the elements are pairwise disjoint, their union is all of \(X \times Y\), and each element is \(g\)-monochromatic.
If \(p\) computes \(g : X \to Y \to \alpha \) with communication complexity \(c\), then \(\texttt{leafRectangles}(p)\) is a monochromatic rectangle partition of \(X \times Y\) with respect to \(g\) and has at most \(2^c\) parts.
Given a subprotocol path \(\texttt{hsp} : \texttt{SubprotocolPath}\, s\, p\), the set of input pairs \((x, y) \in X \times Y\) that reach \(s\) along that path is a combinatorial rectangle \(\texttt{reachXPath}(\texttt{hsp}) \times \texttt{reachYPath}(\texttt{hsp})\).
Given a subprotocol witness \(\texttt{hsp} : \texttt{IsSubprotocol}\, s\, p\), the set of input pairs \((x, y) \in X \times Y\) that reach \(s\) (via the canonical path choice) is a combinatorial rectangle.
If \(\mathrm{CC}(g) \leq n\), then there exists a monochromatic rectangle partition of \(X \times Y\) with respect to \(g\) having at most \(2^n\) parts.
To prove \(\mathrm{CC}(g) \geq n + 1\), it suffices to show that every monochromatic rectangle partition of \(g\) has more than \(2^n\) parts: if every \(\texttt{IsMonoPartition}\, P\, g\) satisfies \(2^n \lt |P|\), then \((n+1) \leq \mathrm{CC}(g)\).
If \(\mathrm{CC}(g) \leq n\) and \(S \subseteq X \times Y\) is a fooling set for \(g\), then \(|S| \leq 2^n\).
For any fooling set \(S\) for \(g\), the deterministic communication complexity satisfies \(\lceil \log _2 |S| \rceil \leq \mathrm{CC}(g)\) (as extended naturals).