OAI/Computability/MaxCut/Machines/AlphabetReduction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The explicit assignment tester applied to the encoded satisfying pairs of an actual finite edge predicate. The resulting soundness loss is independent of the alphabet size. Uniform padding of the finite sample space and assembly of the global incidence graph are separate constructions.

  1. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetReduction.LegalPair line 22
  2. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetReduction.InputCoordinate line 25
  3. def OAI.MaxCutGames.Foundations.PCP.AlphabetReduction.pairEncoding line 27
  4. def OAI.MaxCutGames.Foundations.PCP.AlphabetReduction.edgeTesterReject line 31
  5. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetReduction.rejected_edge_tester_bound line 35
  6. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetReduction.honest_edge_tester line 51