OAI/Computability/UniqueGames/Machines/MachineRegularTableBoundsLemmas.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

A polynomial cap for the actual two regularization loops, their header, and all seven final drain loops. Per-call sizes include the complete stored output prefix.

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.oldLoopPolynomial line 19
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.ownerLoopPolynomial line 24
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.timePolynomial line 29
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.oldElapsed_prefix_le line 35
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.oldElapsed_le line 57
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.ownerElapsed_prefix_le line 65
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.ownerElapsed_le line 89
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.totalTime_le line 98
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.machineInTime line 114
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTableRuntime.rawProgram line 136
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTableRuntime.sourceMachine_eq line 144
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTableRuntime.cleanupTapes line 148
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTableRuntime.cleanup_complete line 151
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTableRuntime.terminalRun line 155
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTableRuntime.computableInPolyTime line 175

    Source documentation

    The literal canonical output configuration computes the shared regular preprocessing map, with the actual complete raw execution as its witness.

    noncomputable def computableInPolyTime (H : PreprocessingRegularTables.BaseTable) :
    TM2ComputableInPolyTime GraphTables.tableBits
      (PortTables.inputBits (ports := PreprocessingRegularTables.internalDegree + 1))
…
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTableRuntime.finite_alphabet line 184

    Source documentation

    Finiteness refers to the exact machine in the preceding certificate.

    theorem finite_alphabet (H : PreprocessingRegularTables.BaseTable) :
    ∀ k, Finite ((computableInPolyTime H).tm.Γ k) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTableRuntime.computableInPolyTime