80 Communication Complexity — Bit String

80.1 Overview

This module introduces \(n\)-bit strings as Boolean-valued functions on \(\mathrm{Fin}\, n\) and develops the signed inner product of two such strings under the standard \(\{ 0,1\} \to \{ \pm 1\} \) correspondence. The main results relate the signed inner product to the Hamming distance: it equals \(n - 2\, \mathrm{hammingDist}(x,y)\), and it is additive under concatenation and multiplicative under repetition.

80.2 Declarations

Definition 80.1 Bit string

✓

An \(n\)-bit string is a function \(x : \mathrm{Fin}\, n \to \mathrm{Bool}\). The type \(\texttt{CommunicationComplexity.BitString}\, n\) is an abbreviation for \(\mathrm{Fin}\, n \to \mathrm{Bool}\).

Definition 80.2 Signed inner product

✓

Given two \(n\)-bit strings \(x, y : \mathrm{Fin}\, n \to \mathrm{Bool}\), their signed inner product is the integer

\[ \mathrm{signedInner}(x, y) \; =\; \sum _{i=0}^{n-1} \begin{cases} 1 & \text{if } x_i = y_i,\\ -1 & \text{if } x_i \neq y_i.\end{cases} \]

Each coordinate where \(x\) and \(y\) agree contributes \(+1\), and each disagreeing coordinate contributes \(-1\).

Definition 80.3 Agreement count

✓

The agreement count of two \(n\)-bit strings \(x\) and \(y\) is the number of coordinates \(i \in \mathrm{Fin}\, n\) on which \(x_i = y_i\), i.e., \(\# \{ i : x_i = y_i\} \) as a natural number.

Theorem 80.4 Agreement count plus Hamming distance equals length

✓

For any two \(n\)-bit strings \(x\) and \(y\),

\[ \mathrm{agreementCount}(x, y) + \mathrm{hammingDist}(x, y) = n. \]

The agreeing and disagreeing coordinates partition \(\{ 0, \ldots , n-1\} \).

Theorem 80.5 Agreement count as complement of Hamming distance

✓

For any two \(n\)-bit strings \(x\) and \(y\), the agreement count satisfies

\[ \mathrm{agreementCount}(x, y) = n - \mathrm{hammingDist}(x, y) \]

as an equality of integers (after casting the natural numbers to \(\mathbb {Z}\)).

Theorem 80.6 Signed inner product via Hamming distance

✓

For any two \(n\)-bit strings \(x\) and \(y\),

\[ \mathrm{signedInner}(x, y) \; =\; n - 2\, \mathrm{hammingDist}(x, y). \]

Theorem 80.7 Signed inner product via agreement and disagreement counts

✓

For any two \(n\)-bit strings \(x\) and \(y\),

\[ \mathrm{signedInner}(x, y) \; =\; \mathrm{agreementCount}(x, y) - \mathrm{hammingDist}(x, y). \]

That is, the signed inner product equals the number of agreeing coordinates minus the number of disagreeing coordinates.

Theorem 80.8 Signed inner product is additive under concatenation

✓

For strings \(x_1, y_1 : \mathrm{Fin}\, m \to \mathrm{Bool}\) and \(x_2, y_2 : \mathrm{Fin}\, n \to \mathrm{Bool}\),

\[ \mathrm{signedInner}(\mathrm{append}(x_1, x_2),\, \mathrm{append}(y_1, y_2)) \; =\; \mathrm{signedInner}(x_1, y_1) + \mathrm{signedInner}(x_2, y_2). \]

Concatenating both pairs of bit strings adds their signed inner products.

Theorem 80.9 Signed inner product is invariant under index recast

✓

If \(m = n\) and \(x, y : \mathrm{Fin}\, n \to \mathrm{Bool}\), then

\[ \mathrm{signedInner}(x \circ \mathrm{Fin.cast}\, h,\; y \circ \mathrm{Fin.cast}\, h) \; =\; \mathrm{signedInner}(x, y). \]

Reindexing both inputs along a \(\mathrm{Fin.cast}\) does not change the signed inner product.

Theorem 80.10 Signed inner product scales under repetition

✓

For any \(n\)-bit strings \(x\) and \(y\) and any \(a : \mathbb {N}\),

\[ \mathrm{signedInner}(\mathrm{Fin.repeat}\, a\, x,\; \mathrm{Fin.repeat}\, a\, y) \; =\; a \cdot \mathrm{signedInner}(x, y). \]

Repeating both inputs \(a\) times multiplies the signed inner product by \(a\).