OAI/Computability/UniqueGames/PCP/MachineRawInitialTable.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual finite machine computing the initial graph's full serialized table. The runtime bound counts every parse, row, cleanup and output reversal.

  1. theorem OAI.UniqueGamesTheorem.Foundations.PCP.MachineRawInitialTable.trace_trans line 16
  2. def OAI.UniqueGamesTheorem.Foundations.PCP.MachineRawInitialTable.prefixBits line 20
  3. theorem OAI.UniqueGamesTheorem.Foundations.PCP.MachineRawInitialTable.outputBits line 24
  4. theorem OAI.UniqueGamesTheorem.Foundations.PCP.MachineRawInitialTable.machineTrace line 31
  5. def OAI.UniqueGamesTheorem.Foundations.PCP.MachineRawInitialTable.outputsInTime line 57
  6. def OAI.UniqueGamesTheorem.Foundations.PCP.MachineRawInitialTable.computableInPolyTime line 65