OAI/Computability/PerfectCompleteness/Machines/ProducerTimeLemmas.lean

GitHub source file

89 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.bootstrapPolynomial line 32
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.validityPolynomial line 35
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.loweringPolynomial line 38
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.transitionEmissionPolynomial line 41
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.acceptanceEmissionPolynomial line 46
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.finishPolynomial line 50
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.iterationPolynomial line 53
  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.knownPhasePolynomial line 57
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.producerPolynomial line 62
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.bootstrapPolynomial_eval line 65
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.validity_steps_le line 69
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.front_steps_le line 74
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.loweringPolynomial_eval line 79
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.transitionEmissionPolynomial_eval line 85
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.acceptanceEmissionPolynomial_eval line 92
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.forestSteps line 100
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.forestSteps_le line 106
  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.initialForestSteps line 125
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.initialForestSteps_le line 129
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.transitionForestSteps line 143
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.transitionForestSteps_le line 147
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.acceptanceForestSteps line 153
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.acceptanceForestSteps_le line 158
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.frameInput line 174
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.frameInput_dataSize_le line 177
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.transitionEmissionSteps line 186
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.transitionEmissionSteps_le line 190
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.acceptanceEmissionSteps line 214
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.acceptanceEmissionSteps_le line 218
  30. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.finishSteps line 236
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.finishSteps_le line 240
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.iterationPolynomial_eval line 262
  33. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.iterationSteps line 268
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.iterationSteps_le line 272
  35. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.knownPhaseSteps line 289
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.knownPhaseSteps_le line 296
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTime.producerPolynomial_eval line 310
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.loweringSteps_eq_forestSteps line 335
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.verifier_steps_eq line 347
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.verifier_steps_le line 354
  41. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.verifierInPolynomialTime line 362
  42. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceStage.verifierPlacedInPolynomialTime line 376
  43. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.verifierInitialTapes line 406
  44. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.verifierFinalTapes line 410
  45. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.verifierInPolynomialTime line 413
  46. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.verifierInPolynomialTime_steps line 425
  47. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.verifierPlacedInPolynomialTime line 430
  48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.verifierFinal_output line 444
  49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.verifierFinal_clean line 448
  50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.verifierPlaced_output line 452
  51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.verifierPlaced_clean line 458
  52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitFinish.verifierPlaced_other line 463
  53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionIteration.steps_eq_sum line 483
  54. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionIteration.tokens_frame_eq_forest line 497
  55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionIteration.lowerSteps_eq_forestSteps line 513
  56. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionIteration.stageSteps_verifier line 536
  57. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionIteration.verifier_steps_eq line 543
  58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionIteration.verifier_steps_le line 557
  59. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionIteration.verifierInPolynomialTime line 564
  60. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionIteration.verifierPlacedInPolynomialTime line 581
  61. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTailStage.IterateLabel line 622
  62. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTailStage.Label line 624
  63. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTailStage.entry line 627
  64. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTailStage.statement line 630
  65. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTailStage.initial line 641
  66. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTailStage.afterIteration line 644
  67. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTailStage.afterAcceptance line 647
  68. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTailStage.terminal line 650
  69. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTailStage.timePolynomial line 654
  70. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTailStage.finish_entry line 659
  71. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTailStage.inTime line 667
  72. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTailStage.program line 704
  73. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTailStage.programInTime line 707
  74. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerTailStage.terminal_output line 714
  75. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerMachine.Label line 734
  76. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerMachine.initPorts line 737
  77. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerMachine.initLabels line 743
  78. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerMachine.entry line 746
  79. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerMachine.program line 748
  80. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerMachine.timePolynomial line 755
  81. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerMachine.initializerReady line 759
  82. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerMachine.inTime line 764
  83. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerMachine.rawProgram line 791
  84. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerMachine.initialCfg line 798
  85. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerMachine.terminalRun line 809
  86. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerMachine.cleanupTapes line 820
  87. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerMachine.cleanup_complete line 823
  88. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerMachine.computableInPolyTime line 827
  89. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerMachine.finiteAlphabet line 833