OAI/Computability/UniqueGames/PCP/TableGapReductionLemmas.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Both semantic implications for the actual stored-table 3SAT gap map. The positive clause gap follows from the full actual repeated transformation. The full map admits a polynomial-time machine.

  1. theorem OAI.UniqueGamesTheorem.Foundations.PCP.TableGapReduction.run_gap line 25
  2. theorem OAI.UniqueGamesTheorem.Foundations.PCP.TableGapReduction.output_gap line 30
  3. theorem OAI.UniqueGamesTheorem.Foundations.PCP.TableGapReduction.output_satisfiable_iff line 38
  4. theorem OAI.UniqueGamesTheorem.Foundations.PCP.TableGapReduction.gapMap_satisfiable_iff line 48
  5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.TableGapReduction.output_count_gap line 52
  6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.TableGapReduction.gapMap_clauseGap line 72
  7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.TableGapReduction.finalClauseGap_le_one line 78
  8. def OAI.UniqueGamesTheorem.Outer.HastadSource.success line 96
  9. def OAI.UniqueGamesTheorem.Outer.HastadSource.asSource line 100
  10. theorem OAI.UniqueGamesTheorem.Outer.HastadSource.failure_add_success line 103
  11. def OAI.UniqueGamesTheorem.Outer.HastadSource.gapInput line 111
  12. def OAI.UniqueGamesTheorem.Outer.HastadSource.sourceMap line 115
  13. def OAI.UniqueGamesTheorem.Outer.HastadSource.output line 119
  14. theorem OAI.UniqueGamesTheorem.Outer.HastadSource.complete line 123
  15. theorem OAI.UniqueGamesTheorem.Outer.HastadSource.sound line 130
  16. def OAI.UniqueGamesTheorem.Outer.HastadSource.roundMachine line 139
  17. theorem OAI.UniqueGamesTheorem.Outer.HastadSource.roundMachine_finite line 142
  18. def OAI.UniqueGamesTheorem.Outer.HastadSource.gapMachine line 147
  19. def OAI.UniqueGamesTheorem.Outer.HastadSource.sourceMachine line 155
  20. def OAI.UniqueGamesTheorem.Outer.HastadSource.computation line 161
  21. theorem OAI.UniqueGamesTheorem.Outer.HastadSource.finiteAlphabet line 166
  22. structure OAI.UniqueGamesTheorem.Outer.HastadSource.Reduction line 173
  23. theorem OAI.UniqueGamesTheorem.Outer.HastadSource.exists_reduction line 180