ComparatorChallenges/UniqueGamesTheorem.lean

GitHub source file

32 declarations, 1 contain sorry, 0 declared as axioms

1. structure OAI.UniqueGamesTheorem.Foundations.Target.PermutationTable A finite permutation table with a certified inverse line 9

   Source documentation

   Finite forward and inverse tables make totality and invertibility explicit. An eventual external encoding only needs to serialize the forward table.

   L4DEL explanation

   including the table of each permutation.

   fixing a label to v uniquely fixes the label to w and vice versa

   A PermutationTable alphabet stores both directions of a permutation of Fin alphabet: images is the forward table and inverseImages is its proposed inverse.

   1. Both vectors have exactly alphabet entries, so every label has a forward image and an inverse image without a partial lookup.
   2. leftInverse and rightInverse prove the two tables undo each other in both orders. Those fields are what make this data a permutation rather than merely two arrays.
   3. The later output encoding serializes only images; the inverse table and proofs certify the Lean object but do not add duplicate words to gameBits. The manuscript supports explicit permutation tables, while this two-table certification is the Lean implementation.

   Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games, OpenAI, The Unique Games Theorem (2026), p. 2, Subhash Khot, On the Unique Games Conjecture (2010), p. 5

   Also declared: OAI/Computability/UniqueGames/Model.lean:9 (same declaration text).

   structure PermutationTable (alphabet : Nat) where
   …

2. structure OAI.UniqueGamesTheorem.Foundations.Target.Constraint One oriented permutation constraint line 15

   L4DEL explanation

   where πe is a permutation of K.

   A Constraint vertices alphabet selects a source vertex, a target vertex, and the permutation table that tells which target label matches each source label.

   1. Both endpoints inhabit Fin vertices, so they are valid indices into the same finite vertex set.
   2. Orientation matters: satisfaction applies the stored permutation to the source label and compares the result with the target label.
   3. This structure is one occurrence's mathematical data. Multiplicity and nonemptiness belong to Instance, not to an individual constraint.

   Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games, OpenAI, The Unique Games Theorem (2026), p. 2

   Also declared: OAI/Computability/UniqueGames/Model.lean:15 (same declaration text).

   structure Constraint (vertices alphabet : Nat) where
   …

3. def OAI.UniqueGamesTheorem.Foundations.Target.Constraint.satisfied Test whether one labeling satisfies one constraint line 20

   L4DEL explanation

   A labeling a satisfies e when a(ve ) = πe (a(ue )).

   constraint.satisfied labeling is the Boolean decision that the target vertex's label equals the forward image of the source vertex's label.

   1. Read labeling constraint.source, apply constraint.permutation.images, and compare with labeling constraint.target.
   2. decide converts that decidable equality into true or false; it does not search for a labeling.
   3. Because the table has a certified inverse, fixing either endpoint label uniquely determines the satisfying label at the other endpoint.

   Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games, OpenAI, The Unique Games Theorem (2026), p. 2

   Also declared: OAI/Computability/UniqueGames/Model.lean:20 (same declaration text).

   def Constraint.satisfied {n q : Nat} (constraint : Constraint n q)
       (labeling : Fin n → Fin q) : Bool :=
   …

   Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Constraint

4. structure OAI.UniqueGamesTheorem.Foundations.Target.Instance An explicit, unweighted list of Unique Games constraints line 26

   Source documentation

   Constraint occurrences are list entries, so repeated parallel edges retain their multiplicity. No weights are hidden in this representation.

   L4DEL explanation

   a finite vertex set, a finite alphabet K, and a nonempty list of oriented constraints

   An Instance alphabet records a finite number of vertices and a nonempty list of permutation constraints over that fixed alphabet.

   1. Each constraint carries endpoints in Fin vertices, so malformed vertex indices cannot inhabit the structure.
   2. Constraints are list occurrences rather than a set: identical or parallel entries remain separate and are counted with multiplicity by countSatisfied.
   3. There is no weight field. Thus the ratio used later is the ordinary number of satisfied list entries divided by the nonzero list length.

   Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games, OpenAI, The Unique Games Theorem (2026), p. 2

   Also declared: OAI/Computability/UniqueGames/Model.lean:26 (same declaration text).

   structure Instance (alphabet : Nat) where
   …

5. def OAI.UniqueGamesTheorem.Foundations.Target.countSatisfied Count satisfied constraint occurrences line 31

   L4DEL explanation

   Its value is the fraction of satisfied constraints

   countSatisfied labeling constraints recursively counts how many entries in the constraint list evaluate to true under one labeling.

   1. The empty list contributes zero.
   2. For a head constraint, add one when constraint.satisfied labeling is true and zero otherwise, then recurse on the tail.
   3. This is an occurrence count: repeated equal constraints are counted repeatedly. The later game value divides this natural number by the nonempty list length.

   Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games, OpenAI, The Unique Games Theorem (2026), p. 2

   Also declared: OAI/Computability/UniqueGames/Model.lean:31 (same declaration text).

   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

   Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Constraint

6. structure OAI.UniqueGamesTheorem.BinaryFormula.Literal A signed Boolean variable occurrence line 43

   L4DEL explanation

   A Literal pairs an arbitrary natural-number variable name with a Boolean sign.

   1. positive = true represents the variable itself; positive = false represents its Boolean negation.
   2. Names are natural numbers rather than a dense finite type, so an encoded formula may use sparse indices.
   3. DecidableEq lets the surrounding syntax compare literals mechanically; it adds no well-formedness restriction.

   Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games

   Also declared: OAI/Computability/UniqueGames/Model.lean:43 (same declaration text).

   structure Literal where
   …

7. def OAI.UniqueGamesTheorem.BinaryFormula.Literal.eval Evaluate a signed literal under a Boolean assignment line 48

   L4DEL explanation

   Given assignment : Nat → Bool, a positive literal returns the assigned bit and a negative literal returns its Boolean complement.

   1. Look up the variable by literal.name.
   2. If literal.positive is true, keep the value; otherwise apply Boolean !.
   3. The assignment is total on all natural names, so sparse or previously unseen indices still have a defined value.

   Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games

   Also declared: OAI/Computability/UniqueGames/Model.lean:48 (same declaration text).

   def Literal.eval (literal : Literal) (assignment : Nat → Bool) : Bool :=
   …

   Mentions: OAI.UniqueGamesTheorem.BinaryFormula.Literal

8. abbrev OAI.UniqueGamesTheorem.BinaryFormula.Clause Exactly three literal slots line 51

   L4DEL explanation

   Clause abbreviates Vector Literal 3, so its arity is fixed by the type rather than checked at runtime.

   1. Positions 0, 1, and 2 are all available by finite indexing.
   2. The vector may repeat a literal or variable name; this alias imposes no distinctness condition.
   3. Being an abbreviation, Clause unfolds directly to the vector type in later definitions.

   Sources and attribution: Pinned OpenAI Lean source for Unique Games

   Also declared: OAI/Computability/UniqueGames/Model.lean:51 (same declaration text).

   abbrev Clause := Vector Literal 3

   Mentions: OAI.UniqueGamesTheorem.BinaryFormula.Literal

9. def OAI.UniqueGamesTheorem.BinaryFormula.Clause.eval Evaluate a 3SAT clause by disjunction line 53

   L4DEL explanation

   A clause is true when at least one of its three signed literals evaluates to true under the assignment.

   1. Evaluate positions zero and one and combine them with Boolean ||.
   2. Disjoin that result with the evaluation at position two.
   3. This is ordinary three-literal OR; no exactly-one or parity interpretation is introduced.

   Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games

   Also declared: OAI/Computability/UniqueGames/Model.lean:53 (same declaration text).

   def Clause.eval (clause : Clause) (assignment : Nat → Bool) : Bool :=
   …

   Mentions: OAI.UniqueGamesTheorem.BinaryFormula.Clause

10. structure OAI.UniqueGamesTheorem.BinaryFormula.Formula Binary 3SAT as a finite list of three-literal clauses line 58

    Source documentation

    An ordinary conjunction of three-slot clauses with sparse variable names. Repeated names and repeated literals are permitted in every clause.

    L4DEL explanation

    Given a 3SAT formula, apply Theorem 4.1 and Lemma 4.2

    A Formula is exactly a list of Clauses, and each clause is a length-three vector of signed literals whose variable names are natural numbers.

    1. Variable names may be sparse, and neither repeated names nor repeated literals are forbidden. This is a syntax container, not a promise that the input has been simplified.
    2. Satisfaction is defined separately: one Boolean assignment must make every listed clause evaluate to true.
    3. The manuscript starts its final construction from a 3SAT formula. The particular framed bit serialization below is a Lean comparator interface and is not attributed to the paper.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games, OpenAI, The Unique Games Theorem (2026), p. 38

    Also declared: OAI/Computability/UniqueGames/Model.lean:58 (same declaration text).

    structure Formula where
    …

11. def OAI.UniqueGamesTheorem.BinaryFormula.Formula.Satisfiable One assignment satisfies every listed clause line 61

    L4DEL explanation

    F.Satisfiable means there exists a total Boolean assignment making each clause occurring in F.clauses evaluate to true.

    1. The existential assignment maps every natural-number variable name to a Boolean value.
    2. The universal condition ranges over list membership, so repeated clauses create repeated obligations with the same truth value.
    3. An empty formula is satisfiable because the all-clauses condition is vacuous.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games

    Also declared: OAI/Computability/UniqueGames/Model.lean:61 (same declaration text).

    def Formula.Satisfiable (F : Formula) : Prop :=
    …

    Mentions: OAI.UniqueGamesTheorem.BinaryFormula.Formula

12. def OAI.UniqueGamesTheorem.BinaryEncoding.bitsValue Interpret a least-significant-bit-first Boolean list line 70

    L4DEL explanation

    bitsValue converts Lean's canonical Boolean digit list back to a natural number.

    1. The empty list denotes zero.
    2. A head bit b and recursive tail value n become Nat.bit b n, placing b at the low-order end.
    3. parseName later checks the decoded number's Nat.bits against the original digits, which supplies canonicality rather than this fold alone.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games

    Also declared: OAI/Computability/UniqueGames/Model.lean:70 (same declaration text).

    def bitsValue : List Bool → Nat
      | [] => 0
      | b :: bits => Nat.bit b (bitsValue bits)

13. def OAI.UniqueGamesTheorem.BinaryEncoding.parseFrame Parse one self-delimiting frame of bits line 74

    L4DEL explanation

    parseFrame reads zero or more data bits, each introduced by true, until a false terminator, then returns the digits and untouched suffix.

    1. A leading false means the framed digit list is empty.
    2. A leading true requires one following data bit and then recursively parses the rest of the frame.
    3. End of input before a terminator, or true without a following bit, returns none.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games

    Also declared: OAI/Computability/UniqueGames/Model.lean:74 (same declaration text).

    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. -/

14. def OAI.UniqueGamesTheorem.BinaryEncoding.parseName Decode one canonically framed natural-number name line 82

    Source documentation

    Equality with the canonical digits rejects alternate padded encodings.

    L4DEL explanation

    parseName reads one framed list of bits, converts it to a natural number, and returns that number together with the unconsumed suffix only when the digits are canonical.

    1. parseFrame uses false as the end marker and true followed by a bit as one framed digit.
    2. bitsValue reconstructs the natural number; comparing the parsed digits with name.bits rejects padded or otherwise alternate encodings of the same number.
    3. This parser is a comparator-level serialization choice. The manuscript asserts a deterministic polynomial-time reduction but does not specify this framing, so no manuscript quotation is attached to the encoding detail.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games, Pinned OpenAI formalization note 102

    Also declared: OAI/Computability/UniqueGames/Model.lean:82 (same declaration text).

    def parseName (input : List Bool) : Option (Nat × List Bool) := do
    …

15. def OAI.UniqueGamesTheorem.BinaryEncoding.parseLiteral Parse a sign bit followed by one canonical name line 87

    L4DEL explanation

    parseLiteral consumes the first bit as polarity, delegates the remaining input to parseName, and returns one Literal plus the suffix.

    1. With a leading bit sign, successful name parsing yields ⟨name, sign⟩.
    2. Failure of the nested canonical-name parser propagates through the Option computation.
    3. Empty input fails because a literal must contain a sign even before its framed name.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games

    Also declared: OAI/Computability/UniqueGames/Model.lean:87 (same declaration text).

    def parseLiteral : List Bool → Option (Literal × List Bool)
      | sign :: input => do
          let (name, rest) ← parseName input
          return (⟨name, sign⟩, rest)
      | [] => none

    Mentions: OAI.UniqueGamesTheorem.BinaryEncoding.parseName

16. def OAI.UniqueGamesTheorem.BinaryEncoding.parseClause Parse three literals in sequence line 93

    L4DEL explanation

    parseClause runs parseLiteral three times and packages the results as the length-three vector #v[a,b,c].

    1. Each successful parser passes its unconsumed suffix to the next literal parser.
    2. Failure at any of the three positions makes the whole Option computation fail.
    3. No delimiter is needed between literals because each variable name carries its own frame terminator.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games

    Also declared: OAI/Computability/UniqueGames/Model.lean:93 (same declaration text).

    def parseClause (input : List Bool) : Option (Clause × List Bool) := do
    …

17. def OAI.UniqueGamesTheorem.BinaryEncoding.parseClauses Decode a terminated clause list with structural fuel line 100

    Source documentation

    Fuel bounds the number of clause iterations, not the size of any name.

    L4DEL explanation

    parseClauses fuel input parses a list in which false ends the list and true announces one three-literal clause followed by the rest.

    1. Zero fuel always fails; positive fuel plus false succeeds with the empty clause list; positive fuel plus true parses one clause and recurses with one less unit.
    2. An empty input without a terminator fails. decodeFormula supplies input.length + 1 fuel, enough to bound clause iterations while each framed variable name may consume several bits.
    3. This is termination and canonical-input machinery for the Lean interface, not a proof step quoted from the mathematical manuscript.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games, Pinned OpenAI formalization note 102

    Also declared: OAI/Computability/UniqueGames/Model.lean:100 (same declaration text).

    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

    Mentions: OAI.UniqueGamesTheorem.BinaryEncoding.parseClause

18. def OAI.UniqueGamesTheorem.BinaryEncoding.decodeFormula Accept exactly one complete canonical formula encoding line 109

    L4DEL explanation

    decodeFormula input parses the clause list with enough fuel and succeeds only when no trailing bits remain.

    1. The fuel is input.length + 1, so recursive clause parsing cannot exhaust it before consuming a finite input.
    2. parseClauses returns both clauses and a suffix; decodeFormula rejects every nonempty suffix.
    3. On exact consumption it wraps the clause list in Formula; malformed, unterminated, noncanonical, or trailing encodings return none.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games

    Also declared: OAI/Computability/UniqueGames/Model.lean:109 (same declaration text).

    def decodeFormula (input : List Bool) : Option Formula := do
    …

19. def OAI.UniqueGamesTheorem.BinaryLanguage.language The encoded language of satisfiable binary 3SAT formulas line 119

    L4DEL explanation

    language input holds exactly when the entire bit list decodes to some formula and that formula has a satisfying Boolean assignment.

    1. The existential formula is tied to the input by decodeFormula input = some formula.
    2. The second conjunct applies Formula.Satisfiable to that same decoded syntax tree.
    3. Parser failure, trailing bits, or a well-formed unsatisfiable formula all place the input outside the language, for different reasons.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games, Pinned OpenAI formalization note 102

    Also declared: OAI/Computability/UniqueGames/Model.lean:119 (same declaration text).

    def language (input : List Bool) : Prop :=
    …

20. abbrev OAI.UniqueGamesTheorem.Integration.BinaryLinear.F2 The two-element coefficient field line 126

    L4DEL explanation

    F2 abbreviates ZMod 2, the field whose two elements encode binary addition and translation.

    1. Arithmetic is modulo two, so every element is its own additive inverse.
    2. The abbreviation introduces no new structure or proof; it shortens the types used by the translation contract.
    3. This is the scalar field for the label coordinate space, not the Boolean type used by formula encodings and graph sides.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games

    Also declared: OAI/Computability/UniqueGames/Model.lean:126 (same declaration text).

    abbrev F2 := ZMod 2

21. abbrev OAI.UniqueGamesTheorem.Integration.BinaryLinear.Vector A finite binary coordinate vector line 128

    L4DEL explanation

    Vector n abbreviates the function type Fin n → F2, so a vector is one modulo-two coordinate for each of n positions.

    1. Pointwise addition supplies the translation operation used in every constraint.
    2. Fin n makes the dimension part of the type and rules out out-of-range coordinates.
    3. When n is positive this type has 2^n elements; the reduction record separately identifies it with the finite label type.

    Sources and attribution: Pinned OpenAI Lean source for Unique Games

    Also declared: OAI/Computability/UniqueGames/Model.lean:128 (same declaration text).

    abbrev Vector (n : Nat) := Fin n → F2
    …

    Mentions: OAI.UniqueGamesTheorem.Integration.BinaryLinear.F2

22. def OAI.UniqueGamesTheorem.Integration.TranslationTarget.IsTranslationInstance Every permutation constraint is addition by one binary shift line 137

    L4DEL explanation

    every constraint is a translation

    After identifying labels with a binary vector space, IsTranslationInstance coordinates g requires each listed permutation to act as x ↦ x+shift for some shift depending on that constraint.

    1. The property quantifies over every constraint occurrence in g.constraints.
    2. For one occurrence it chooses one vector shift, then requires the coordinate equation for every possible label.
    3. The same coordinate equivalence is fixed for the whole game; only the additive shift may vary between constraints.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games, OpenAI, The Unique Games Theorem (2026), p. 2

    Also declared: OAI/Computability/UniqueGames/Model.lean:137 (same declaration text).

    def IsTranslationInstance {q s : Nat} (coordinates : Fin q ≃ BinaryLinear.Vector s)
        (g : Instance q) : Prop :=
    …

    Mentions: OAI.UniqueGamesTheorem.Integration.BinaryLinear.Vector

23. def OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord Encode one natural number in unary with a zero terminator line 147

    L4DEL explanation

    encodeWord n is n copies of true followed by one false.

    1. The count of leading true bits recovers the natural number.
    2. The false terminator makes concatenations of several words uniquely separable.
    3. This output representation is unary, unlike the canonical binary variable-name framing used for the input formula and the logarithmic endpoint encoding discussed in the manuscript.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games

    Also declared: ComparatorChallenges/PerfectCompleteness.lean:7 (same declaration text), OAI/Computability/UniqueGames/Model.lean:147 (same declaration text).

    def encodeWord (n : Nat) : List Bool := List.replicate n true ++ [false]

24. def OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords Concatenate a list of unary natural-number words line 149

    L4DEL explanation

    encodeWords maps each natural to encodeWord and joins the framed words in list order.

    1. An empty word list becomes an empty bit list.
    2. For n :: ns, output the frame for n followed by the recursive encoding of ns.
    3. Because each word ends in false, adjacent frames remain decodable without a separate length field.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games

    Also declared: ComparatorChallenges/PerfectCompleteness.lean:9 (same declaration text), OAI/Computability/UniqueGames/Model.lean:149 (same declaration text).

    def encodeWords : List Nat → List Bool
      | [] => []
      | n :: ns => encodeWord n ++ encodeWords ns
    
    end UniqueGamesTheorem.Foundations.Complexity
    
    namespace UniqueGamesTheorem.Foundations.Complexity
    
    open Target

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

25. def OAI.UniqueGamesTheorem.Foundations.Complexity.tableWords Serialize the forward half of a permutation table line 159

    L4DEL explanation

    tableWords table lists the natural values of table.images in label order.

    1. toList preserves the vector's alphabet entries.
    2. Mapping Fin.val removes the bounded-index wrapper and produces natural-number words.
    3. The inverse table and inverse-law proofs are omitted because the certified forward permutation determines them mathematically.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games

    Also declared: OAI/Computability/UniqueGames/Model.lean:159 (same declaration text).

    def tableWords {q : Nat} (table : PermutationTable q) : List Nat :=
    …

26. def OAI.UniqueGamesTheorem.Foundations.Complexity.constraintWords Serialize one constraint as endpoints plus a permutation table line 162

    L4DEL explanation

    constraintWords emits the source index, target index, and every forward permutation image as natural numbers.

    1. The first two words fix the oriented endpoints.
    2. tableWords appends exactly one image for each alphabet label.
    3. The alphabet size is fixed outside the input, so each constraint contributes a fixed number of natural-number fields once the error parameters are fixed.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games

    Also declared: OAI/Computability/UniqueGames/Model.lean:162 (same declaration text).

    def constraintWords {n q : Nat} (constraint : Constraint n q) : List Nat :=
    …

27. def OAI.UniqueGamesTheorem.Foundations.Complexity.gameWords Flatten an explicit game into natural-number fields line 165

    L4DEL explanation

    gameWords game places a three-word header before the serialization of every constraint occurrence.

    1. The header records the vertex count, fixed alphabet size, and number of list occurrences.
    2. flatMap constraintWords preserves occurrence order and multiplicity while concatenating endpoints and forward tables.
    3. The explicit occurrence count and fixed table width delimit the remaining fields without serializing proofs or inverse tables.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games

    Also declared: OAI/Computability/UniqueGames/Model.lean:165 (same declaration text).

    def gameWords {q : Nat} (game : Instance q) : List Nat :=
    …

28. def OAI.UniqueGamesTheorem.Foundations.Complexity.gameBits The comparator's concrete output bit string line 168

    L4DEL explanation

    gameBits game applies the unary encodeWords representation to the complete natural-number field list from gameWords.

    1. This is the exact output function named in BinaryGapReduction.computation, so the polynomial-time machine contract concerns these bytes, not an unspecified abstract graph.
    2. The representation is explicit and prefix-decodable, but it uses unary natural-number words. It is not the logarithmic endpoint encoding described in the paper's polynomial-encoding paragraph.
    3. The theorem's formal contract therefore stands on the Lean proof that this concrete output function is computed in polynomial time; the manuscript is not cited as specifying this encoding.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games, Pinned OpenAI formalization note 102

    Also declared: OAI/Computability/UniqueGames/Model.lean:168 (same declaration text).

    def gameBits {q : Nat} (game : Instance q) : List Bool := encodeWords (gameWords game)
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.gameWords

29. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteAlphabet.FiniteAlphabet Every physical tape of the reduction machine has a finite alphabet line 178

    Source documentation

    Every physical tape has a finite alphabet. Together with M.kFin, this also makes the disjoint union of all physical tape alphabets finite.

    L4DEL explanation

    FiniteAlphabet M means Finite (M.Γ k) for every physical tape index k of the two-tape-style finite Turing-machine model.

    1. The quantifier ranges over tape indices, not game labels. Together with the machine's finite number of tapes, it rules out hiding an infinite symbol type inside the polynomial-time computation.
    2. This condition does not give one numeric bound on every alphabet and does not itself prove polynomial time; BinaryGapReduction.computation carries the separate runtime contract.
    3. The paper's fixed finite game alphabet and this machine-alphabet condition are related explicitness requirements but are not the same proposition.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games, Pinned OpenAI formalization note 102

    Also declared: ComparatorChallenges/PerfectCompleteness.lean:19 (same declaration text), OAI/Computability/UniqueGames/Model.lean:178 (same declaration text).

    def FiniteAlphabet (M : FinTM2) : Prop := ∀ k, Finite (M.Γ k)
    …

30. structure OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.SimpleBipartite A certificate that the output graph is simple and bipartite line 191

    Source documentation

    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.

    L4DEL explanation

    A simple bipartite instance has two disjoint vertex sets and at most one constraint on each pair of opposite vertices.

    SimpleBipartite game assigns every vertex a Boolean side, orients every constraint from the false side to the true side, and forbids two occurrence indices from sharing the same ordered endpoints.

    1. sourceSide and targetSide certify the bipartition for every list occurrence rather than merely asserting that some partition exists.
    2. endpoints_injective is injectivity on occurrence indices. Because all constraints use the same left-to-right orientation, it gives at most one constraint for each opposite-side vertex pair.
    3. The certificate permits isolated vertices; simplicity and bipartiteness do not require connectivity or positive degree.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games, OpenAI, The Unique Games Theorem (2026), p. 2

    Also declared: OAI/Computability/UniqueGames/Model.lean:191 (same declaration text).

    structure SimpleBipartite {q : Nat} (game : Instance q) where
    …

31. structure OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.BinaryGapReduction The complete machine-checkable contract for the gap reduction line 203

    Source documentation

    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.

    L4DEL explanation

    The alphabet, the degree of the running-time polynomial, and its constants depend only on ε, δ.

    A BinaryGapReduction ε δ packages one alphabet, binary-vector-space coordinate system, constructor, machine computation, and the two gap guarantees before any encoded formula is supplied.

    1. alphabetAtLeastTwo, dimensionPositive, and coordinates identify the fixed labels with Fin dimension → ZMod 2; translations then requires every output constraint to add one fixed binary shift.
    2. construct returns a nonempty unweighted instance, while simpleBipartite certifies its graph shape. computation and finiteAlphabet expose the exact output-bit function as a finite-alphabet polynomial-time Turing computation.
    3. Completeness says a satisfiable decoded input has some labeling satisfying at least 1-ε of the occurrences. Soundness says an unsatisfiable decoded input makes every labeling satisfy at most δ of them.
    4. The record contains the theorem's output contract; it is not itself the existence proof. theorem11 is the declaration that states such a record is nonempty for every allowed pair of errors.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games, OpenAI, The Unique Games Theorem (2026), p. 2

    Also declared: OAI/Computability/UniqueGames/Model.lean:203 (same declaration text).

    structure BinaryGapReduction (ε δ : ℝ) where
    …

32. theorem OAI.UniqueGamesTheorem.theorem11 Challenge statement: A polynomial-time binary-3SAT reduction proving the Unique Games gap sorry line 231

    Source documentation

    For every fixed pair of errors in (0, 1/2), binary 3SAT reduces in polynomial time to translation Unique Games with completeness at least 1 - ε and soundness at most δ. The alphabet and machine depend only on the errors.

    L4DEL explanation

    We prove the Unique Games Conjecture.

    The author conjectured that the problem is computationally hard.

    For any fixed completeness error ε and soundness bound δ between 0 and 1/2, there exists a concrete polynomial-time reduction from encoded binary 3SAT to a nonempty simple bipartite Unique Games instance. Satisfiable inputs admit a labeling of value at least 1-ε; unsatisfiable inputs give every labeling value at most δ.

    1. BinaryGapReduction ε δ fixes an alphabet of size at least two, a positive dimension, and an identification of its labels with a finite vector space over F₂ before quantifying over inputs.
    2. Its output instances are nonempty, unweighted, simple and bipartite; every constraint permutation is translation by a fixed vector in those coordinates, and the encoded output is computed by a finite-alphabet Turing machine in polynomial time.
    3. The Lean conclusion is Nonempty (BinaryGapReduction ε δ). This declaration concerns only the Unique Games theorem, not the four separate Max-Cut, Vertex Cover, Min-UnCut, and directed-feedback results documented in the same note; its challenge proof is sorry and the paired solution is OAI.Computability.UniqueGames.Main.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), Pinned OpenAI Lean source for Unique Games, OpenAI Unique Games manuscript (abstract), Pinned OpenAI formalization note 102, Subhash Khot, On the Unique Games Conjecture (2010), p. 5

    Distinct definitions of this name: OAI/Computability/UniqueGames/Theorem.lean:26 (same statement text; different proof or body). Qualify references as OAI.UniqueGamesTheorem.theorem11@path.

    Unique Game: a constraint-satisfaction instance in which each edge constraint is a permutation, so either endpoint's label uniquely determines the satisfying label at the other endpoint

    theorem theorem11 (ε δ : ℝ)
        (hε : 0 < ε) (hεhalf : ε < 1 / 2)
        (hδ : 0 < δ) (hδhalf : δ < 1 / 2) :
        Nonempty (Explicit.MachineOutputContract.BinaryGapReduction ε δ) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.BinaryGapReduction