Theorem.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.MaxCutGames.Theorem.exists_binaryGapReduction line 8
theorem OAI.MaxCutGames.theorem11 line 23
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.
```
theorem theorem11 (ε δ : ℝ)
    (hε : 0 < ε) (hεhalf : ε < 1 / 2)
    (hδ : 0 < δ) (hδhalf : δ < 1 / 2) :
    Nonempty (Explicit.MachineOutputContract.BinaryGapReduction ε δ) :=
…
```
Mentions: OAI.MaxCutGames.Explicit.MachineOutputContract.BinaryGapReduction