OAI/Combinatorics/IndependentSets/PCP/QueryIncidence.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.Verifier line 8
  2. abbrev OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.Label line 12
  3. abbrev OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.Vertex line 13
  4. abbrev OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.Dart line 14
  5. def OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.response line 18
  6. def OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.zeroSlot line 21
  7. def OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.decodeRight line 23
  8. def OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.encodeRight line 25
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.decode_encodeRight line 27
  10. def OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.canonicalSlot line 30
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.canonicalSlot_query line 33
  12. def OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.RepeatedConsistent line 37
  13. instance OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.repeatedConsistentDecidable line 40
  14. def OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.LeftValid line 46
  15. instance OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.leftValidDecidable line 49
  16. def OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.incidenceAccept line 55
  17. def OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.reverse line 60
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.reverse_involutive line 62
  19. def OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.reverseEquiv line 66
  20. def OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.tail line 72
  21. def OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.predicate line 76
  22. def OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.graph line 81
  23. theorem OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.edgeSatisfied_eq_incidence line 91
  24. def OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.honestLabeling line 99
  25. theorem OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.honest_leftValid line 103
  26. theorem OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.honest_incidence line 110
  27. theorem OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.perfect_completeness line 121
  28. theorem OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.satisfiable_of_verifier_satisfiable line 129
  29. def OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.decodedAssignment line 137
  30. theorem OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.incidenceAccept_true line 140
  31. theorem OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.all_incidences_imply_event line 149
  32. theorem OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.rejected_event_forces_slot line 164
  33. def OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.rejectedEvents line 182
  34. def OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.verifierRejectionCount line 185
  35. theorem OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.rejection_count_bound line 188
  36. theorem OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.card_label line 217
  37. theorem OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.card_vertex line 220
  38. theorem OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.card_dart line 224
  39. theorem OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.gap_transfer line 228
  40. theorem OAI.IndependentSetsGames.Foundations.PCP.QueryIncidence.six_query_alphabet line 243