OAI/Computability/UniqueGames/Machines/MachineRegularOwnerProgram.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Actual dummy-owner body of regularization

The owner is a physically stored unary index. The code computes its cloud metadata, initializes local index and fuel, skips the family computation when padding is zero, and otherwise generates one rotor for all dummy vertices of this owner. Each vertex iteration consumes one fuel bit and increments both physical vertex indices. The final checked addition and cleanup leave only the updated global index, prefix, and accumulated output.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.Tape line 25
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.Alphabet line 26
  3. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.State line 27
  4. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.Data line 28
  5. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.CoreState line 29
  6. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.MetaState line 30
  7. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.FamilyState line 31
  8. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.BaseTable line 32
  9. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.(instance at line 34) line 34
  10. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.(instance at line 35) line 35
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.core line 37
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.paddingTape line 38
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.levelTape line 39
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.dummyFuel line 40
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.scratch line 41
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.readyState line 43
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.metadataTape line 45
  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.metadataView line 48
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.familyTape line 52
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.familyView line 55
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.vertexView line 59
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.metadataView_left line 63
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.metadataView_right line 66
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.familyView_left line 72
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.familyView_right line 75
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.vertexView_left line 81
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.vertexView_right line 83
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.metadataStates line 89
  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.familyStates line 95
  30. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.vertexStates line 101
  31. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.Label line 107
  32. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.entry line 119
  33. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.program line 121
  34. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.working line 154
  35. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.frame line 158
  36. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.cfg line 160
  37. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.initialData line 163
  38. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.metadataData line 176
  39. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.seededData line 179
  40. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.ownerBits line 182
  41. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.finalData line 185