OAI/Computability/MaxCut/Machines/MachineRegularOwnerProgram.lean

GitHub source file

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

    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.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.BaseTable, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.program, OAI.MaxCutGames.Foundations.Complexity.MachineCloudPadding.totalTime, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.cfg, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.entry, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.initialData, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.metadataData

  46. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.working_update_local line 238
  47. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.working_update_fuel line 252
  48. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.working_update_global line 259
  49. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.working_update_output line 273
  50. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.copyCountTrace line 288

    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.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.BaseTable, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.cfg, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.metadataData, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.seededData

  51. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.copyFuelTrace line 305

    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.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.BaseTable, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.cfg, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.seededData, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.readyState, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.working, OAI.MaxCutGames.Foundations.Complexity.encodeWord

  52. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.guardZeroStep line 322
  53. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.guardPositiveStep line 328
  54. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.dummyBits line 337
  55. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.vertexData line 341
  56. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.loopData line 348
  57. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.loopFrame line 352
  58. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.preSteps line 356
  59. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.loopSteps line 360
  60. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupCost line 367
  61. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.ownerTime line 373
  62. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.familyPlacement line 379
  63. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.familyResultPlacement line 388
  64. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.familyExecution line 399
  65. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.familySteps line 405
  66. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.familyTrace line 409
  67. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.coreFrame_eq line 429
  68. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.vertexPlacement line 447
  69. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.vertexTrace line 463

    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.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.BaseTable, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.dummySteps, OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyEntry, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.degree_positive, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.readyState, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.working, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.vertexData, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.dummyBits

  70. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.working_fuel line 487
  71. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.working_scratch line 490
  72. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.loopPositiveStep line 493
  73. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.loopZeroStep line 504
  74. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.bumpStep line 509
  75. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.loopPrefixTrace line 519
  76. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.preparationTrace line 547
  77. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupFrame line 556
  78. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.ownerBits_zero line 597
  79. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupZeroFrame line 604
  80. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupLoopFrame line 614
  81. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupZeroTrace line 625
  82. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupLoopTrace line 639
  83. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.loopTrace line 653
  84. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.ownerInTime line 671

    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.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.BaseTable, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.cfg, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.entry, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.initialData, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.finalData, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.ownerTime

  85. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.totalSteps line 703
  86. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.ownerTrace line 706
  87. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOwnerBody.totalSteps_le line 712
  88. def OAI.MaxCutGames.Foundations.PCP.PreprocessingMachineBounds.inputLength line 725
  89. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingMachineBounds.cloudSize_le_input line 727
  90. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingMachineBounds.cloudTotal_le_input line 731
  91. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingMachineBounds.level_le_input line 737
  92. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingMachineBounds.regularVertices_le_input line 741
  93. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingMachineBounds.offset_le_sum line 746
  94. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingMachineBounds.prefix_le_input line 757
  95. def OAI.MaxCutGames.Foundations.PCP.PreprocessingMachineBounds.tablePolynomial line 766

    Source documentation

    A two-parameter bound for the complete unary graph codec.

    noncomputable def tablePolynomial (a b : Nat) : Polynomial Nat :=
…
  96. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingMachineBounds.tableBits_le_of_counts line 771
  97. def OAI.MaxCutGames.Foundations.PCP.PreprocessingMachineBounds.regularPolynomial line 781
  98. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingMachineBounds.regularBits_le line 784
  99. def OAI.MaxCutGames.Foundations.PCP.PreprocessingMachineBounds.rotorPolynomial line 798
  100. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingMachineBounds.cloudRotorBits_le line 802