67 Communication Complexity — Public Coin Approximation
67.1 Overview
This module provides the bridge between public-coin protocols over arbitrary finite probability spaces and those using the canonical CoinTape randomness source. The key result is that any finite-message public-coin protocol can be approximated by a CommunicationComplexity.CoinTape-based protocol of equal complexity, with the approximation error degrading by at most the chosen slack \(\delta \gt 0\).
67.2 Declarations
Given a public-coin finite-message protocol \(p\) over an arbitrary finite probability space \(\Omega \) and a slack \(\delta \gt 0\), this definition produces a natural number \(n\) together with a finite-message protocol over \(\mathrm{CoinTape}(n)\) that approximates \(p\). The construction works by pulling back \(p\) along a measure-approximating map \(\varphi : \mathrm{CoinTape}(n) \to \Omega \) provided by CommunicationComplexity.Internal.single_coin_approx.
For any finite-message protocol \(p\) over a finite probability space \(\Omega \) and any \(\delta \gt 0\), the complexity of the CoinTape approximation \((p.\mathrm{toCoinTape}\; \delta ).2\) equals the complexity of the original protocol \(p\).
Let \(p\) be a public-coin finite-message protocol over a finite probability space \(\Omega \), let \(Q : X \to Y \to \alpha \to \mathrm{Prop}\) be a correctness predicate, and let \(\varepsilon , \delta \gt 0\). If \(p\) approximately satisfies \(Q\) with error at most \(\varepsilon \) (i.e. \(p.\mathrm{ApproxSatisfies}\; Q\; \varepsilon \) holds), then the CoinTape approximation \((p.\mathrm{toCoinTape}\; \delta ).2\) approximately satisfies \(Q\) with error at most \(\varepsilon + \delta \).