OAI/Computability/UniqueGames/Theorem.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniqueGamesTheorem.Theorem.exists_binaryGapReduction line 10
2. theorem OAI.UniqueGamesTheorem.theorem11 line 26

   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.

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

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

   Mentions: OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.BinaryGapReduction