UniqueGamesTheorem
DefinitionThis block sets up the formal target of a Unique Games reduction from 3-SAT. A PermutationTable on alphabet size q stores a forward and an inverse table of Fin q values that are mutually inverse, so it is a bijection of labels. A Constraint on n vertices has a source vertex, a target vertex and such a permutation, and a labeling Fin n → Fin q satisfies it when the permutation maps the source's label to the target's label. An Instance is a vertex count together with a nonempty list of constraints, so parallel constraints keep their multiplicity, and countSatisfied counts the satisfied list entries. On the formula side, a literal is a natural-number variable name with a sign, a clause is exactly three literals evaluated as their disjunction, a Formula is a list of clauses (repeated names and literals are allowed), and it is satisfiable when some Boolean assignment of names makes every clause true. A bit-string decoder reads a formula as a sequence of records, each a true bit followed by three literals (a sign bit and a name), ended by a false bit with nothing left over. Names are written as little-endian binary digits, each digit preceded by a true bit and the list closed by a false bit, and non-canonical padded digit lists are rejected. The language consists of the bit strings that decode to a satisfiable formula. Over F2 = ZMod 2, an instance is a translation instance relative to a bijection between the q labels and F2^s when every constraint permutation acts, in those coordinates, as adding some constraint-specific shift vector. The encoding of a game is a unary encoding of its list of vertex count, alphabet size, constraint count, and then each constraint's source, target and permutation images. SimpleBipartite says an instance has a Boolean side assignment with every constraint going from a false vertex to a true vertex, and no two distinct constraint occurrences sharing the same (source, target) pair. For real ε and δ, a BinaryGapReduction fixes an alphabet size q ≥ 2, a dimension s ≥ 1, a bijection from labels to F2^s, and a map from bit strings to instances. Every output must be simple bipartite and a translation instance. The map must be computed by a multi-tape Turing machine in polynomial time, measured in the raw input length, with the game encoding as the output format, and every tape alphabet must be finite. Completeness requires that an input in the language gives some labeling satisfying at least a 1 − ε fraction of the constraints. Soundness requires that an input outside the language gives every labeling a satisfied fraction of at most δ. This is a structure of data and assumed properties, and no existence of such a reduction is asserted.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/UniqueGamesTheorem.lean; bytes 16..8310
-- Kind: block; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.
import Mathlib
namespace OAI
namespace UniqueGamesTheorem.Foundations.Target
/-- Finite forward and inverse tables make totality and invertibility explicit.
An eventual external encoding only needs to serialize the forward table. -/
structure PermutationTable (alphabet : Nat) where
images : Vector (Fin alphabet) alphabet
inverseImages : Vector (Fin alphabet) alphabet
leftInverse : ∀ label : Fin alphabet, inverseImages[images[label]] = label
rightInverse : ∀ label : Fin alphabet, images[inverseImages[label]] = label
structure Constraint (vertices alphabet : Nat) where
source : Fin vertices
target : Fin vertices
permutation : PermutationTable alphabet
def Constraint.satisfied {n q : Nat} (constraint : Constraint n q)
(labeling : Fin n → Fin q) : Bool :=
decide (constraint.permutation.images[labeling constraint.source] = labeling constraint.target)
/-- Constraint occurrences are list entries, so repeated parallel edges retain
their multiplicity. No weights are hidden in this representation. -/
structure Instance (alphabet : Nat) where
vertices : Nat
constraints : List (Constraint vertices alphabet)
nonempty : constraints ≠ []
def countSatisfied {n q : Nat} (labeling : Fin n → Fin q) :
List (Constraint n q) → Nat
| [] => 0
| constraint :: rest =>
(if constraint.satisfied labeling then 1 else 0) + countSatisfied labeling rest
end UniqueGamesTheorem.Foundations.Target
namespace UniqueGamesTheorem.BinaryFormula
open UniqueGamesTheorem.Foundations
structure Literal where
name : Nat
positive : Bool
deriving DecidableEq
def Literal.eval (literal : Literal) (assignment : Nat → Bool) : Bool :=
if literal.positive then assignment literal.name else !(assignment literal.name)
abbrev Clause := Vector Literal 3
def Clause.eval (clause : Clause) (assignment : Nat → Bool) : Bool :=
(clause[0].eval assignment || clause[1].eval assignment) || clause[2].eval assignment
/-- An ordinary conjunction of three-slot clauses with sparse variable names.
Repeated names and repeated literals are permitted in every clause. -/
structure Formula where
clauses : List Clause
def Formula.Satisfiable (F : Formula) : Prop :=
∃ assignment : Nat → Bool, ∀ clause ∈ F.clauses, clause.eval assignment = true
end UniqueGamesTheorem.BinaryFormula
namespace UniqueGamesTheorem.BinaryEncoding
open BinaryFormula
def bitsValue : List Bool → Nat
| [] => 0
| b :: bits => Nat.bit b (bitsValue bits)
def parseFrame : List Bool → Option (List Bool × List Bool)
| false :: rest => some ([], rest)
| true :: b :: rest => do
let (bits, trailing) ← parseFrame rest
return (b :: bits, trailing)
| _ => none
/-- Equality with the canonical digits rejects alternate padded encodings. -/
def parseName (input : List Bool) : Option (Nat × List Bool) := do
let (digits, rest) ← parseFrame input
let name := bitsValue digits
if digits = name.bits then some (name, rest) else none
def parseLiteral : List Bool → Option (Literal × List Bool)
| sign :: input => do
let (name, rest) ← parseName input
return (⟨name, sign⟩, rest)
| [] => none
def parseClause (input : List Bool) : Option (Clause × List Bool) := do
let (a, input) ← parseLiteral input
let (b, input) ← parseLiteral input
let (c, rest) ← parseLiteral input
return (#v[a, b, c], rest)
/-- Fuel bounds the number of clause iterations, not the size of any name. -/
def parseClauses : Nat → List Bool → Option (List Clause × List Bool)
| 0, _ => none
| _ + 1, false :: rest => some ([], rest)
| fuel + 1, true :: input => do
let (clause, input) ← parseClause input
let (clauses, rest) ← parseClauses fuel input
return (clause :: clauses, rest)
| _ + 1, [] => none
def decodeFormula (input : List Bool) : Option Formula := do
let (clauses, rest) ← parseClauses (input.length + 1) input
if rest = [] then some ⟨clauses⟩ else none
end UniqueGamesTheorem.BinaryEncoding
namespace UniqueGamesTheorem.BinaryLanguage
open UniqueGamesTheorem.Foundations
def language (input : List Bool) : Prop :=
∃ formula, BinaryEncoding.decodeFormula input = some formula ∧ formula.Satisfiable
end UniqueGamesTheorem.BinaryLanguage
namespace UniqueGamesTheorem.Integration.BinaryLinear
abbrev F2 := ZMod 2
abbrev Vector (n : Nat) := Fin n → F2
end UniqueGamesTheorem.Integration.BinaryLinear
namespace UniqueGamesTheorem.Integration.TranslationTarget
open UniqueGamesTheorem.Foundations
open Target
def IsTranslationInstance {q s : Nat} (coordinates : Fin q ≃ BinaryLinear.Vector s)
(g : Instance q) : Prop :=
∀ constraint ∈ g.constraints, ∃ shift : BinaryLinear.Vector s,
∀ label : Fin q,
coordinates (constraint.permutation.images[label]) = coordinates label + shift
end UniqueGamesTheorem.Integration.TranslationTarget
namespace UniqueGamesTheorem.Foundations.Complexity
def encodeWord (n : Nat) : List Bool := List.replicate n true ++ [false]
def encodeWords : List Nat → List Bool
| [] => []
| n :: ns => encodeWord n ++ encodeWords ns
end UniqueGamesTheorem.Foundations.Complexity
namespace UniqueGamesTheorem.Foundations.Complexity
open Target
def tableWords {q : Nat} (table : PermutationTable q) : List Nat :=
table.images.toList.map Fin.val
def constraintWords {n q : Nat} (constraint : Constraint n q) : List Nat :=
[constraint.source.val, constraint.target.val] ++ tableWords constraint.permutation
def gameWords {q : Nat} (game : Instance q) : List Nat :=
[game.vertices, q, game.constraints.length] ++ game.constraints.flatMap constraintWords
def gameBits {q : Nat} (game : Instance q) : List Bool := encodeWords (gameWords game)
end UniqueGamesTheorem.Foundations.Complexity
namespace UniqueGamesTheorem.Foundations.Complexity.MachineFiniteAlphabet
open Turing
/-- Every physical tape has a finite alphabet. Together with `M.kFin`, this
also makes the disjoint union of all physical tape alphabets finite. -/
def FiniteAlphabet (M : FinTM2) : Prop := ∀ k, Finite (M.Γ k)
end UniqueGamesTheorem.Foundations.Complexity.MachineFiniteAlphabet
namespace UniqueGamesTheorem.Explicit.MachineOutputContract
open UniqueGamesTheorem.Foundations
open Target
open scoped BigOperators
/-- A canonical orientation from the false side to the true side. Injectivity
is on occurrence indices, so two distinct list entries cannot be parallel even
when their constraint tables are different. -/
structure SimpleBipartite {q : Nat} (game : Instance q) where
side : Fin game.vertices → Bool
sourceSide : ∀ i : Fin game.constraints.length,
side game.constraints[i].source = false
targetSide : ∀ i : Fin game.constraints.length,
side game.constraints[i].target = true
endpoints_injective : Function.Injective (fun i : Fin game.constraints.length =>
(game.constraints[i].source, game.constraints[i].target))
/-- Every parameter, coordinate identification, program, and polynomial is
fixed before the input quantifier. The identity input encoding measures runtime
in the original raw bit length, including sparse binary variable names. -/
structure BinaryGapReduction (ε δ : ℝ) where
alphabet : Nat
alphabetAtLeastTwo : 2 ≤ alphabet
dimension : Nat
dimensionPositive : 1 ≤ dimension
coordinates : Fin alphabet ≃ Integration.BinaryLinear.Vector dimension
construct : List Bool → Instance alphabet
simpleBipartite : ∀ input, SimpleBipartite (construct input)
translations : ∀ input,
Integration.TranslationTarget.IsTranslationInstance coordinates (construct input)
computation : Turing.TM2ComputableInPolyTime (id : List Bool → List Bool)
Complexity.gameBits construct
finiteAlphabet : Complexity.MachineFiniteAlphabet.FiniteAlphabet computation.tm
completeness : ∀ input, BinaryLanguage.language input →
∃ labeling, 1 - ε ≤
(countSatisfied labeling (construct input).constraints : ℝ) /
(construct input).constraints.length
soundness : ∀ input, ¬BinaryLanguage.language input →
∀ labeling, (countSatisfied labeling (construct input).constraints : ℝ) /
(construct input).constraints.length ≤ δ
end UniqueGamesTheorem.Explicit.MachineOutputContract
namespace UniqueGamesTheorem
end UniqueGamesTheorem
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.