OAI/Computability/UniqueGames/Machines/MachineRegularOwnerBody.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Actual execution and exact runtime of the fixed dummy-owner program.

  1. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.joinTrace line 13
  2. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.oneStep line 17
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.metadataPlacement line 21
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.metadataTrace line 32

    Source documentation

    Actual cloud metadata, with every outer register and tape preserved.

    theorem metadataTrace (H : BaseTable) (t : GraphTables.Table) (v : Fin t.vertices)
    (output : List Bool) :
    (advance (TM2.step (program H)))^[MachineCloudPadding.totalTime t v]
      (some (cfg H (some entry) (initialData t v output))) =
      some (cfg H (some (.copyCount .seed)) (metadataData t v output)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.BaseTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.totalTime, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.entry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.initialData, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.metadataData

  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.working_update_local line 49
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.working_update_fuel line 63
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.working_update_global line 70
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.working_update_output line 84
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.copyCountTrace line 99

    Source documentation

    The local rank starts at the actual cloud size, copied from its physical tape.

    theorem copyCountTrace (H : BaseTable) (t : GraphTables.Table) (v : Fin t.vertices)
    (output : List Bool) :
    (advance (TM2.step (program H)))^[2 * (cloudSize t v + 1) + 1]
      (some (cfg H (some (.copyCount .seed)) (metadataData t v output))) =
      some (cfg H (some (.copyFuel .seed)) (seededData t v output)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.BaseTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.metadataData, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.seededData

  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.copyFuelTrace line 116

    Source documentation

    Padding fuel is another preserved unary copy; it is never a control parameter.

    theorem copyFuelTrace (H : BaseTable) (t : GraphTables.Table) (v : Fin t.vertices)
    (output : List Bool) :
    (advance (TM2.step (program H)))^[2 * (padding t v + 1) + 1]
      (some (cfg H (some (.copyFuel .seed)) (seededData t v output))) =
      some ⟨some .guard, readyState H,
        working (seededData t v output) (encodeWord (padding t v)) []⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.BaseTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.seededData, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.readyState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.working, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.guardZeroStep line 133
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.guardPositiveStep line 139
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.dummyBits line 148
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.vertexData line 152
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.loopData line 159
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.loopFrame line 163
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.preSteps line 167
  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.loopSteps line 171
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.cleanupCost line 178
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.ownerTime line 184
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.familyPlacement line 190
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.familyResultPlacement line 199
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.familyExecution line 210
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.familySteps line 216
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.familyTrace line 220
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.coreFrame_eq line 240
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.vertexPlacement line 258
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.vertexTrace line 274

    Source documentation

    A complete actual dummy vertex block, with the owner's fuel left untouched.

    theorem vertexTrace (H : BaseTable) (t : GraphTables.Table) (v : Fin t.vertices)
    (j : Fin (padding t v)) (output fuel : List Bool) :
    (advance (TM2.step (program H)))^[
        MachineRegularVertexBlock.dummySteps t (padding t) (familyCloudTable H t) v j output.length]
      (some ⟨some (.vertex (MachineRegularVertexBlock.dummyEntry internalDegree
        MachineRegularOriginalBody.degree_positive)), readyState H,
        working (vertexData H t v j.val output) fuel []⟩) =
      some ⟨some .bump, readyState H,
        working (vertexData H t v j.val (output ++ dummyBits H t v j)) fuel []⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.BaseTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.dummySteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.dummyEntry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.degree_positive, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.readyState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.working, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.vertexData, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.dummyBits

  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.working_fuel line 298
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.working_scratch line 301
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.loopPositiveStep line 304
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.loopZeroStep line 315
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.bumpStep line 320
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.loopPrefixTrace line 330
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.preparationTrace line 358
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.cleanupFrame line 367
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.ownerBits_zero line 408
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.cleanupZeroFrame line 415
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.cleanupLoopFrame line 425
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.cleanupZeroTrace line 436
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.cleanupLoopTrace line 450
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.loopTrace line 464
  43. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.ownerInTime line 482

    Source documentation

    Actual complete owner execution, including the genuinely empty padding case. The bound is assembled from proven component bounds; its family term is not used as an exact number of transitions.

    noncomputable def ownerInTime (H : BaseTable) (t : GraphTables.Table)
    (v : Fin t.vertices) (output : List Bool) :
    StateTransition.EvalsToInTime (TM2.step (program H))
      (cfg H (some entry) (initialData t v output))
      (some (cfg H none (finalData H t v output))) (ownerTime H t v output) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.BaseTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.entry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.initialData, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.finalData, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.ownerTime

  44. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.totalSteps line 514
  45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.ownerTrace line 517
  46. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOwnerBody.totalSteps_le line 523