OAI/Computability/MaxCut/Main.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.OptimalMaxCut.LongCode.InstanceAdapter.bits_eq_gameBits line 19
2. theorem OAI.OptimalMaxCut.LongCode.InstanceAdapter.exists_encoded_gridComputer line 30
3. theorem OAI.OptimalMaxCut.main line 53

   Source documentation

   Optimal Max-Cut approximation hardness: for EVERY fixed real alpha above the exact Goemans--Williamson constant, an ordinary binary polynomial reduction prints a full finite SIMPLE UNWEIGHTED graph and a strict YES/NO optimum gap. The construction uses an analytic inequality, rational long-code construction, integer rounding, finite-field derandomization and a graph-printer TM.

   Distinct definitions of this name: ComparatorChallenges/OptimalMaxCut.lean:153 (different declaration text). Qualify references as OAI.OptimalMaxCut.main@path.

   theorem main : MainStatement := by
   …

   Mentions: OAI.OptimalMaxCut.MainStatement

4. example OAI.(example at line 81) line 81