OAI.UniqueGamesTheorem.theorem11

The theorem states that, for any real numbers ε and δ with 0<ε<1/2 and 0<δ<1/2, there exists a BinaryGapReduction ε δ, a polynomial-time reduction from satisfiability of binary-encoded 3-clause formulas to translation Unique Games. The source language consists of bit-strings that decode, under a canonical self-delimiting encoding with sparse variable names, to a conjunction of clauses of three literals (repeats allowed) that has a satisfying assignment. A reduction consists of the following data, all fixed before any input is chosen. There is an alphabet size q≥2, a dimension s≥1, and an equivalence between the q labels and the vectors in F₂^s. There is a map construct sending each input bit-list to a Unique Games instance over q labels, whose constraints form a nonempty list (so multiplicities are kept), each given by a source vertex, a target vertex and a permutation of the labels with explicit inverse table. Every constructed instance is simple bipartite: vertices are split into two sides, every constraint goes from the false side to the true side, and no two distinct constraint entries share the same (source, target) pair. Every constraint permutation is a translation, meaning it adds some fixed vector in F₂^s to the coordinates of each label. The map construct is computed by a Mathlib Turing machine (TM2) in polynomial time on the raw input bit length, with output the bit encoding of the instance, and every tape alphabet of that machine is finite. Completeness: if the input formula is satisfiable, some labeling of the vertices satisfies at least a 1−ε fraction of the constraints. Soundness: if the input is not a satisfiable formula (including any string that fails to decode), every labeling satisfies at most a δ fraction of the constraints. The alphabet and machine depend only on ε and δ. The theorem is stated with its proof admitted (sorry).