OAI/Computability/MaxCut/Machines/AlphabetRetraction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Pull a graph predicate back through a surjective label decoder. This preserves every rejection count after decoding. A concrete section embeds the initial eight-label graph into the fixed 64-label alphabet used throughout amplification.

  1. def OAI.MaxCutGames.Foundations.PCP.AlphabetRetraction.pullback line 17
  2. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetRetraction.edgeSatisfied_pullback line 24
  3. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetRetraction.rejectionCount_pullback line 29
  4. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetRetraction.satisfiable_pullback_iff line 34
  5. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetRetraction.Label64 line 46
  6. def OAI.MaxCutGames.Foundations.PCP.AlphabetRetraction.decode64 line 48
  7. def OAI.MaxCutGames.Foundations.PCP.AlphabetRetraction.encode64 line 50
  8. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetRetraction.decode_encode64 line 53
  9. def OAI.MaxCutGames.Foundations.PCP.AlphabetRetraction.initial64 line 58
  10. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetRetraction.initial64_satisfiable_iff line 62
  11. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetRetraction.initial64_alphabet line 67
  12. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetRetraction.initial64_inverse_size_gap line 70