49 Communication Complexity — Helper
49.1 Overview
This module provides Boolean helper definitions used throughout the communication complexity library: the type of \(n\)-bit Boolean inputs, the \(\pm 1\) sign encoding of Boolean values, and coordinate-flipping operations, together with their basic algebraic identities.
49.2 Declarations
\(\texttt{BoolInput}(n)\) is the type of \(n\)-bit Boolean inputs, defined as the function type \(\mathrm{Fin}\, n \to \mathrm{Bool}\).
\(\texttt{zeroInput}(n) : \texttt{BoolInput}(n)\) is the constant \(\mathrm{false}\) function, i.e. the \(n\)-bit string consisting entirely of zeros.
If \(x : \texttt{BoolInput}(n)\) satisfies \(x \ne \texttt{zeroInput}(n)\), then there exists some index \(i \in \mathrm{Fin}\, n\) such that \(x\, i = \mathrm{true}\).
\(\texttt{boolSign} : \mathrm{Bool} \to \mathbb {R}\) assigns the real value \(1\) to \(\mathrm{false}\) and \(-1\) to \(\mathrm{true}\), embedding Boolean values into the multiplicative group \(\{ \pm 1\} \subset \mathbb {R}\).
For all \(a, b : \mathrm{Bool}\),
That is, \(\texttt{boolSign}\) is a group homomorphism from \((\mathrm{Bool}, \oplus )\) to \((\{ \pm 1\} , \cdot )\).
For a finite type \(\alpha \), a finite set \(s : \mathrm{Finset}\, \alpha \), and a function \(f : \alpha \to \mathrm{Bool}\),
For all \(a, b : \mathrm{Bool}\),
In other words, the product of two \(\pm 1\) signs equals \(1\) when the bits agree and \(-1\) when they disagree.
Given \(i : \mathrm{Fin}\, n\) and \(x : \texttt{BoolInput}(n)\), \(\texttt{flipAt}\, i\, x\) is the Boolean input obtained from \(x\) by negating the \(i\)-th coordinate and leaving all other coordinates unchanged.
For \(i : \mathrm{Fin}\, n\) and \(x : \texttt{BoolInput}(n)\), \((\texttt{flipAt}\, i\, x)\, i = \neg (x\, i)\).
For \(i, j : \mathrm{Fin}\, n\) with \(j \ne i\) and \(x : \texttt{BoolInput}(n)\), \((\texttt{flipAt}\, i\, x)\, j = x\, j\).
For \(i : \mathrm{Fin}\, n\) and \(x : \texttt{BoolInput}(n)\), \(\texttt{flipAt}\, i\, (\texttt{flipAt}\, i\, x) = x\). That is, applying \(\texttt{flipAt}\, i\) twice recovers the original input.
For every \(i : \mathrm{Fin}\, n\), the map \(\texttt{flipAt}\, i : \texttt{BoolInput}(n) \to \texttt{BoolInput}(n)\) is bijective; its two-sided inverse is itself.