185 Communication Complexity — Hard Sample
185.1 Overview
This module builds the explicit finite sample space carrying Razborov’s hard distribution for set disjointness, used in the information-complexity proof of the linear randomized lower bound: a uniformly random special coordinate \(T\), two independent uniform bits at \(T\), and at every other coordinate a uniformly random pair from \(\{ 00, 01, 10\} \). It also provides the uniform laws on the factors, the accessors reading off Alice’s and Bob’s inputs, and the basic events and conditioning variables used downstream.
185.2 Declarations
The inductive type with three constructors neither, leftOnly, rightOnly, encoding the three disjoint coordinate pairs \((A_i, B_i) \in \{ (0,0), (1,0), (0,1)\} \) placed at every coordinate \(i\) other than the special coordinate \(T\) in the hard distribution for disjointness.
For any type \(\alpha \) and element \(a \in \alpha \), the subtype \(\{ x : \alpha \mid x \in \{ a\} \} \) has cardinality exactly \(1\), for any Fintype instance on that subtype.