OAI/Computability/UniqueGames/Machines/PoweringMachineVertex.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.Command line 13
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.ports line 15
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.direction line 18
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.commands line 21
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.commands_length line 23
  6. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.LocalLabel line 27
  7. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.SequenceLabel line 28
  8. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.Label line 29
  9. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.State line 30
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.sequenceEntry line 32
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.entry line 37
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.sequenceInstruction line 40
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.instruction line 49
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.result line 55
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.sequenceTapes line 61
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.finalTapes line 67
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.sequenceSteps line 72
  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.costSum line 78
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.sequenceSteps_eq line 84
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.steps line 97
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.budget line 100
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.costSum_le line 103
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.steps_le line 116
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.sequenceTrace line 120
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.vertexTrace line 150
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.sequenceTapes_ready line 168
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.finalTapes_ready line 182
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.sequenceTapes_other line 191
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.finalTapes_other line 205
  30. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.rowBits line 212
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.blockIndex_eq_encodeDart line 217

    Source documentation

    Decoding a command gives exactly its existing vertex-block row index.

    theorem blockIndex_eq_encodeDart (n : Nat) (vertex : Fin vertices) (j : Command d n) :
    PoweringTableLayout.blockIndex d n vertex j =
      PoweringEnumeration.encodeDart vertices d n (direction j, vertex, ports j) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.Command, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.direction, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.ports

  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.rowBits_eq line 225
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.encodeWords_flatMap line 232
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.rows_eq_vertexRowBits line 238
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.sequenceTapes_output line 261
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.finalTapes_output line 281
  37. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineVertex.vertexInTime line 292