OAI/Computability/UniqueGames/Machines/MachineRegularOriginalBodyBounds.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Polynomial runtime for the actual original-vertex body. The size parameter includes the already accumulated output, so no output-prefix premise is used.

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBodyBounds.wide line 16
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBodyBounds.rowPolynomial line 17
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBodyBounds.outputPolynomial line 19
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBodyBounds.corePolynomial line 21
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBodyBounds.blockPolynomial line 25
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBodyBounds.cleanupPolynomial line 28
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBodyBounds.timePolynomial line 29
  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBodyBounds.bodySize line 33
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBodyBounds.blockPolynomial_eval line 36
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBodyBounds.originalTimeBound_le line 51
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBodyBounds.wide_le line 62
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBodyBounds.vertexSteps_le line 72
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBodyBounds.clearSteps_frame line 98
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBodyBounds.cleanupSteps_le line 105
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBodyBounds.totalSteps_le line 136
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBodyBounds.originalInTime line 154