OAI/Computability/PerfectCompleteness/Machines/WitnessEncodingLemmas.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.Bits line 15
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.selector line 17
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.payload line 20
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.pack line 23
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.selector_pack line 28
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.payload_pack line 33
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.Valid line 39
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.valid_iff_local line 42
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.selectedLength line 63
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.selectedLength_eq line 66
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.decode line 71
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.decode_length_le line 74
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.decode_length_eq line 77
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.encode line 82
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.selector_encode line 86
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.payload_encode line 92
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.encode_valid line 97
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.selectedLength_encode line 101
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.decode_encode line 105
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.exists_valid_iff line 116
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.present line 125
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.present_eq line 128
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.witnessCell line 133
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.witnessCell_eq_getElem? line 138
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.witnessCell_end line 145
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.inputPrefix line 149
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.inputPrefix_length line 151
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.pairCell line 156
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.pairCell_eq_getElem? line 160
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.pairBits_decode_length_le line 168
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.pairCells_eq_stackEncoding line 175
  32. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.freeInputPolynomial line 182
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.freeInputPolynomial_eval line 184
  34. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.localConstraintSites line 188
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.localConstraintSites_le line 190
  36. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.localConstraintPolynomial line 194
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.localConstraintSites_le_eval line 196
  38. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.initial line 203
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.initial_control line 208
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.initial_state line 211
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.initial_input_stack line 214
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.initial_other_stack line 219
  43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.initial_input_cell line 224
  44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.initial_input_end line 230
  45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.initial_stack_length_le line 237
  46. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.initial_encode line 248
  47. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessEncoding.accepts_iff_valid_assignment line 255
  48. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierBounds.initializationPolynomial line 270
  49. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierBounds.validationPolynomial line 273
  50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierBounds.initializationPolynomial_eval line 276
  51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierBounds.validationPolynomial_eval line 280
  52. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierBounds.gatesPolynomial line 284
  53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierBounds.gatesPolynomial_eval line 292
  54. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierBounds.bitsPolynomial line 304
  55. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierBounds.machineGatesPolynomial line 310
  56. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierBounds.machineBitsPolynomial line 315
  57. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierBounds.machineGatesPolynomial_eval line 320
  58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierBounds.toFormula_bits_le line 332
  59. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierBounds.toFormula_bits_le_machinePolynomial line 349