79 Communication Complexity — Balanced Simulation
79.1 Overview
This module establishes the balanced simulation theorem for deterministic two-party communication protocols: every protocol \(p\) on inputs \(X \times Y\) with output type \(\alpha \) admits a simulation \(q\) with identical run behavior satisfying \(3^{c(q)} \le 2^{c(q)} \cdot (\# \mathrm{leaves}(p))^{2}\), where \(c(q)\) is the communication complexity of \(q\). The proof proceeds by strong induction on the number of leaves, splitting the protocol tree at a balanced subprotocol at each step.
79.2 Declarations
For every deterministic protocol \(p : \mathrm{Protocol}\; X\; Y\; \alpha \), the number of leaves satisfies \(0 \lt \texttt{CommunicationComplexity.Deterministic.Protocol.numLeaves}\; p\). In particular, the leaf count of a protocol is always at least one.
If a protocol \(p\) has exactly one leaf (i.e. \(p.\mathrm{numLeaves} = 1\)), then its communication complexity satisfies \(p.\mathrm{complexity} = 0\). The only protocol with a single leaf is an immediate output node, which requires no communication.
Let \(m, n \in \mathbb {N}\) with \(3m \le 2n\) and \(3(n - m) \le 2n\). Then \(9 \cdot \max (m^2,\, (n-m)^2) \le 4n^2\). This arithmetic inequality captures the key quantitative gain obtained when a split is balanced: neither piece exceeds \(\tfrac {2}{3}\) of the total.
For every deterministic protocol \(p : \mathrm{Protocol}\; X\; Y\; \alpha \) there exists a protocol \(q\) such that \(q.\mathrm{run} = p.\mathrm{run}\) (i.e. \(q\) computes the same function as \(p\)) and
where \(c(q)\) denotes the communication complexity of \(q\).