OAI/Computability/MaxCut/Machines/PoweringMachineRotor.lean

GitHub source file

138 declarations, 0 contain sorry, 0 declared as axioms

A rotor step on the live unary port-table encoding. First read the reverse dart identifier; then read that dart's tail vertex. This uses no division or runtime graph data in finite control. Both positional selections are proved from the actual serialization.

  1. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRotor.Alphabet line 21
  2. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRotor.reverseRole line 23
  3. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRotor.endpointRole line 26
  4. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRotor.reverseRole_injective line 29
  5. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRotor.endpointRole_injective line 30
  6. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRotor.source_outside_reverse line 31
  7. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRotor.reverse_outside_endpoint line 32
  8. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRotor.reverseTapes line 34
  9. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRotor.endpointTapes line 35
  10. inductive OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRotor.Label line 37
  11. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRotor.instruction line 42
  12. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRotor.reverseId line 51
  13. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRotor.reverseAddress line 54
  14. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRotor.endpointAddress line 57
  15. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRotor.reverse_selected line 60
  16. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRotor.endpoint_selected line 70
  17. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRotor.afterReverse line 76
  18. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRotor.finalTapes line 81
  19. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRotor.steps line 87
  20. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRotor.rotorTrace line 91
  21. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRotor.finalTapes_endpoint line 141
  22. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRotor.finalTapes_other line 152
  23. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRotor.steps_le line 161
  24. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineRotor.machine line 180

    Source documentation

    Its finite description depends on the fixed degree and selected port; the vertex count and graph table are runtime tape data.

    def machine (degree port : Nat) : FinTM2 where
…
  25. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.Alphabet line 207
  26. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.Tape line 208
  27. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.first line 210
  28. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.shift line 212
  29. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.shift_injective line 214
  30. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.rotorRole line 218
  31. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.rotorRole_injective line 223
  32. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.Label line 227
  33. instance OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.labelFintype line 231
  34. instance OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.labelDecidableEq line 238
  35. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.entry line 245
  36. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.copyInstruction line 249
  37. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.instruction line 256
  38. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.steps line 269
  39. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.finalTapes line 275
  40. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.finalTapes_other line 284
  41. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.wordTrace line 305

    Source documentation

    Actual execution together with its endpoint word. No trace or running-time hypothesis is needed: the recursive proof composes the concrete instructions.

    theorem wordTrace (table : PortTables.Table n d) (t : Nat)
    (placement : Tape t → K) (distinct : Function.Injective placement)
    (vertex : Fin n) (ports : Fin t → Fin d)
    (labels : Label t → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.Tape, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.Label, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.Alphabet

  42. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.steps_le line 380
  43. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.machine line 394
  44. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.Tape line 413
  45. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.table line 415
  46. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.start line 416
  47. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.query line 417
  48. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.scan line 418
  49. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.reverse line 419
  50. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.scratch line 420
  51. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.leftEndpoint line 421
  52. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.rightEndpoint line 422
  53. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.leftCopy line 423
  54. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.rightCopy line 424
  55. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.rowOutput line 425
  56. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.endpoint line 427
  57. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.endpoint_false line 430
  58. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.endpoint_true line 431
  59. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.wordSharedRole line 434

    Source documentation

    Table, query, scan, reverse identifier, scratch, selected endpoint.

    def wordSharedRole (target : Bool) (i : Fin 6) : Fin 11 :=
…
  60. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.trajectoryPlacement line 440

    Source documentation

    Position zero is the caller's starting vertex; later positions are the separate physical trajectory tapes.

    def trajectoryPlacement {t max : Nat} (h : t ≤ max) : Fin (t + 1) → Tape max :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.Tape

  61. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement line 443
  62. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_zero line 448
  63. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_one line 450
  64. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_two line 452
  65. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_three line 454
  66. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_four line 456
  67. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_five line 458
  68. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_first line 460
  69. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_succ line 462
  70. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement line 465
  71. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_zero line 469
  72. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_one line 470
  73. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_two line 471
  74. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_three line 472
  75. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_four line 473
  76. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_five line 474
  77. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement line 476
  78. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_zero line 480
  79. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_one line 481
  80. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_two line 482
  81. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_three line 483
  82. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_four line 484
  83. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_five line 485
  84. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.wordSharedRole_injective line 487
  85. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.wordSharedRole_ne_start line 490
  86. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.wordSharedRole_ne_rowOutput line 494
  87. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.trajectoryPlacement_injective line 498
  88. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.wordShared_ne_trajectory line 519
  89. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_injective line 533

    Source documentation

    Every tape used by a bounded word is placed on its own physical tape.

    theorem wordPlacement_injective {t max : Nat} (ht : t ≤ max) (target : Bool) :
    Function.Injective (wordPlacement ht target) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement

  90. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_injective line 550
  91. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_injective line 554
  92. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_ne_rowOutput line 559

    Source documentation

    Word subroutines cannot use the row-output tape, even temporarily.

    theorem wordPlacement_ne_rowOutput {t max : Nat} (ht : t ≤ max) (target : Bool)
    (i : PoweringMachineWord.Tape t) : wordPlacement ht target i ≠ rowOutput max := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineWord.Tape, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.rowOutput

  93. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.shared_ne_wordPlacement_succ line 577

    Source documentation

    A shared role is disjoint from every trajectory tape. This supplies the position-frame premise of PoweringMachineWord.finalTapes_other.

    theorem shared_ne_wordPlacement_succ {t max : Nat} (ht : t ≤ max) (target : Bool)
    (role : Fin 11) (i : Fin t) :
    (Sum.inl role : Tape max) ≠ wordPlacement ht target (.inr i.succ) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.Tape, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement

  94. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.ExtraTape line 596
  95. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.GlobalTape line 597
  96. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.Label line 598
  97. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.finalOutput line 600
  98. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement line 603

    Source documentation

    The unary start vertex and outer counter occupy the same physical tape.

    def commonPlacement (max : Nat) (tape : PoweringMachineTapes.Tape max) : GlobalTape max :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.Tape, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.GlobalTape

  99. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_injective line 606
  100. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_start line 612
  101. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_table line 616
  102. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_scratch line 621
  103. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_rowOutput line 626
  104. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_ne_finalOutput line 631
  105. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_ne_header line 636
  106. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement line 644

    Source documentation

    Header writers use the common work tapes but emit on the final output. The relation producer continues to use commonPlacement rowOutput.

    def headerPlacement (max : Nat) (tape : PoweringMachineTapes.Tape max) : GlobalTape max :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.Tape, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.GlobalTape

  107. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_injective line 648
  108. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_rowOutput line 663
  109. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_eq_common line 667
  110. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_ne_data line 671
  111. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_ne_header line 679
  112. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.castTapes_inline_PoweringMachineInitialize line 691
  113. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.castStatement_inline_PoweringMachineInitialize line 694
  114. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.castConfiguration_inline_PoweringMachineInitialize line 697
  115. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.castTapes_apply_inline_PoweringMachineInitialize line 700
  116. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.castConfiguration_mk_inline_PoweringMachineInitialize line 706
  117. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.stepAux_cast_inline_PoweringMachineInitialize line 712
  118. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.boolAlphabet_eq_inline_PoweringMachineInitialize line 720
  119. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.mergeTapes line 726
  120. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.castTapes_embedding_inline_PoweringMachineInitialize line 731
  121. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.dropUnit_inline_PoweringMachineInitialize line 739
  122. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.headerStatement line 747

    Source documentation

    The native checked header statement is embedded and its inert extra register removed. All four native header tapes keep their identities.

    def headerStatement (max N B : Nat) (label : HeaderLabel) :
    TM2.Stmt (fun _ : GlobalTape max => Bool) Label (Master N) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.GlobalTape, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.Label

  123. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.headerConfiguration line 754
  124. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.headerConfiguration_eq_inline_PoweringMachineInitialize line 759
  125. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.stepAux_headerStatement line 773
  126. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.program line 786
  127. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.headerStep line 799
  128. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.headerTrace line 815
  129. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.initialGlobalTapes line 826
  130. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.copyFirstTrace line 829
  131. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.initializeTrace line 862

    Source documentation

    A concrete successful trace: copy the live input count, then execute the existing header machine on that copy. Runtime is exactly 3*vertices+5.

    theorem initializeTrace (max N B vertices : Nat) (extra : ExtraTape max → List Bool)
    (suffix : List Bool)
    (input : extra (.inl (PoweringMachineTapes.table max)) = encodeWord vertices ++ suffix)
    (scratch : extra (.inl (PoweringMachineTapes.scratch max)) = [])
    (state : Master N) :
    (MachineComposition.advance (TM2.step (program max N B)))^[3 * vertices + 5]
      (some ⟨some (.inr .seed), state, initialGlobalTapes extra⟩) =
      some ⟨none, (state.1, none), mergeTapes (finalTapes B vertices []) extra⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.ExtraTape, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.table, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineTapes.scratch, OAI.MaxCutGames.Foundations.Complexity.MachineComposition.advance, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.program, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.initialGlobalTapes, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.mergeTapes

  132. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.initializeInTime line 874
  133. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.instruction line 889

    Source documentation

    The five finite initialization labels can be placed in a caller's program. The native halt becomes its chosen continuation in the very same transition.

    def instruction {Λ : Type} (max N B : Nat) (labels : Label → Λ) (exit : Option Λ)
    (label : Label) : TM2.Stmt (fun _ : GlobalTape max => Bool) Λ (Master N) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.Label, OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.GlobalTape

  134. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.initializeAtInTime line 893
  135. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.final_counter line 908
  136. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.final_vertices line 913
  137. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.final_darts line 916
  138. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineInitialize.final_extra line 919