OAI/Computability/UniqueGames/Machines/MachineRegularOriginalBody.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

One actual original-vertex body of regularization

The finite code composes physical metadata preparation, expander-family materialization, all vertex rows, and seven metadata drain loops. The outer loop owns the global vertex counter and keeps it unchanged during this body.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.Tape line 23
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.Alphabet line 24
  3. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.CoreState line 25
  4. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.MetaState line 26
  5. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.FamilyState line 27
  6. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.State line 28
  7. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.Data line 29
  8. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.BaseTable line 30
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.degree_positive line 32
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.readyState line 35
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.metadataTape line 39
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.metadataView line 43
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.familyTape line 48
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.familyView line 52
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.vertexView line 57
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.metadataView_left line 61
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.metadataView_right line 64
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.familyView_left line 72
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.familyView_right line 75
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.vertexView_left line 83
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.vertexView_right line 85
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.metadataStates line 91
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.familyStates line 97
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.vertexStates line 98
  25. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.Label line 101
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.entry line 108
  27. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.clearTape line 110
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.clearEntry line 114
  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.clearSource line 117
  30. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.vertexSource line 120
  31. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.program line 124
  32. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.frame line 135
  33. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.coreFrame line 140
  34. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.cfg line 143
  35. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.initialData line 146
  36. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.metadataData line 159
  37. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.familyData line 162
  38. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.emittedBits line 167
  39. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.emittedData line 170
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.joinTrace line 174
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.metadataPlacement line 178
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.metadataTrace line 188

    Source documentation

    Genuine metadata trace transported with all other finite registers and private family tapes preserved.

    theorem metadataTrace (H : BaseTable) (t : GraphTables.Table) (e : Fin t.darts)
    (output : List Bool) :
    (advance (TM2.step (program H)))^[MachineRegularMetadata.totalTime t e]
      (some (cfg H (some entry) (initialData t e output))) =
      some (cfg H (some (.family .start)) (metadataData t e output)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.BaseTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.totalTime, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.entry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.initialData, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.metadataData

  43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.familyPlacement line 204
  44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.familyResultPlacement line 212
  45. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.familyExecution line 225
  46. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.familySteps line 230
  47. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.familyTrace line 236

    Source documentation

    Family work is performed on its physical tapes and produces the rotor from the previously computed unary cloud size.

    theorem familyTrace (H : BaseTable) (t : GraphTables.Table) (e : Fin t.darts)
    (output : List Bool) :
    (advance (TM2.step (program H)))^[familySteps H t e output]
      (some (cfg H (some (.family .start)) (metadataData t e output))) =
      some (cfg H (some (.vertex (MachineRegularVertexBlock.originalEntry
        internalDegree degree_positive))) (familyData H t e output)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.BaseTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.familySteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.metadataData, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalEntry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.degree_positive, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.familyData

  48. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.clearMemory line 254

    Source documentation

    Seven real drain loops, including the complete materialized rotor.

    def clearMemory (base : Tape → List Bool) : Nat → Tape → List Bool
  | 0 => base
  | k + 1 => if h : k < 7 then
      Function.update (clearMemory base k) (clearTape ⟨k, h⟩) [] else clearMemory base k

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.clearTape

  49. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.clearSteps line 259
  50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.identityPlacement line 264
  51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.drainTrace line 267
  52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.clearPrefixTrace line 283
  53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.clearTrace line 298
  54. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.clearFrame line 304
  55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.coreFrame_eq line 322
  56. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.emittedData_eq line 342
  57. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.vertexPlacement line 346
  58. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.vertexSteps line 357
  59. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.vertexTrace line 363

    Source documentation

    Every internal port and the inherited original row are emitted by their actual checked row machines, using the rotor just materialized on tape 7.

    theorem vertexTrace (H : BaseTable) (t : GraphTables.Table) (e : Fin t.darts)
    (output : List Bool) :
    (advance (TM2.step (program H)))^[vertexSteps H t e output]
      (some (cfg H (some (.vertex (MachineRegularVertexBlock.originalEntry
        internalDegree degree_positive))) (familyData H t e output))) =
      some (cfg H (clearEntry 0) (emittedData H t e output)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.BaseTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.vertexSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalEntry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.degree_positive, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.familyData, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.clearEntry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.emittedData

  60. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.totalSteps line 382
  61. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.originalTrace line 389

    Source documentation

    Complete execution of one original-vertex iteration, including physical cleanup of all seven retained metadata fields. The global index is preserved.

    theorem originalTrace (H : BaseTable) (t : GraphTables.Table) (e : Fin t.darts)
    (output : List Bool) :
    (advance (TM2.step (program H)))^[totalSteps H t e output]
      (some (cfg H (some entry) (initialData t e output))) =
      some (cfg H none (initialData t e (output ++ emittedBits H t e))) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.BaseTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.totalSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.entry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.initialData, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.emittedBits

  62. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.originalExecution line 407

    Source documentation

    Exact execution witness. Its stored count is derived from the four actual phases; a polynomial estimate is supplied separately.

    noncomputable def originalExecution (H : BaseTable) (t : GraphTables.Table) (e : Fin t.darts)
    (output : List Bool) :
    StateTransition.EvalsToInTime (TM2.step (program H))
      (cfg H (some entry) (initialData t e output))
      (some (cfg H none (initialData t e (output ++ emittedBits H t e))))
      (totalSteps H t e output) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.BaseTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.entry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.initialData, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.emittedBits, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.totalSteps