# Perfect completeness for 2-to-1 games

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Perfect completeness for 2-to-1 games](../../preprints/Perfect-completeness-for-2-to-1-games-September-23-2026/paper.pdf)

## Scope

The formalized result establishes perfect-completeness hardness for 2-to-1 games. For every fixed rational $0<\delta<1$, a deterministic polynomial-time reduction from binary 3SAT produces a nonempty unweighted game of value exactly $1$ on satisfiable inputs and at most $\delta$ on unsatisfiable inputs. Each constraint projection has exactly two preimages for each output label. The alphabet depends only on $\delta$, and the runtime is measured in the original input bit length.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Perfect-completeness reduction for 2-to-1 games | [PerfectCompleteness.lean](../ComparatorChallenges/PerfectCompleteness.lean) |