OAI/Computability/MaxCut/Machines/MachineOverlayTable.lean

GitHub source file

134 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.Tape line 15
2. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.Ambient line 16
3. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.State line 17
4. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.graphArchive line 19
5. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.graphStream line 20
6. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.scratch line 21
7. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.vertexCount line 22
8. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.dartCount line 23
9. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.expanderArchive line 24
10. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.expanderStream line 25
11. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.fuel line 26
12. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.vertex line 27
13. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.tail line 28
14. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.oldReverse line 29
15. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.relation line 30
16. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.dividedCopy line 31
17. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.quotient line 32
18. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.newReverse line 33
19. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.rowBuffer line 34
20. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.output line 35
21. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.oldTapes line 37
22. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.expanderTapes line 41
23. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.oldTapes_injective line 45
24. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.expanderTapes_injective line 51
25. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.clean line 57
26. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.expanderState line 60
27. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.expanderState_clean line 69
28. inductive OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.MainLabel line 74
29. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.Label line 86
30. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.next line 88
31. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.mainInstruction line 91

    Source documentation

    Fixed degree control, including two actual independent working streams.

    def mainInstruction (d e : Nat) (hd : 0 < d) (he : 0 < e) :
        MainLabel d e → TM2.Stmt (fun _ : Tape => Bool) (Label d e) (State A d e)
      | .copyHFirst => Reduction.MachineTransfer.loopAt expanderArchive scratch id false
          (.inr .copyHFirst) (next .copyHSecond)
      | .copyHSecond => MachineCopy.forkLoop scratch expanderArchive expanderStream false
          (.inr .copyHSecond) (next .countSeed)
      | .countSeed => MachineUnaryAffineAt.seed output 0 (.inr .countScan)
      | .countScan => MachineUnaryAffineAt.scan vertexCount scratch output (d + e)
          (.inr .countScan) (.inr .countRestore)
      | .countRestore => Reduction.MachineTransfer.loopAt scratch vertexCount id false
          (.inr .countRestore) (next .headerSeed)
      | .headerSeed => MachineUnaryAffineAt.seed output 0 (.inr .headerScan)
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.MainLabel, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.Label, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.State, OAI.MaxCutGames.Reduction.MachineTransfer.loopAt, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.expanderArchive, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.scratch, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.next, OAI.MaxCutGames.Foundations.Complexity.MachineCopy.forkLoop, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.expanderStream, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.seed, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.output, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.scan, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.vertexCount

32. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.program line 133

    Source documentation

    The checked splitter is placed directly in five homogeneous Boolean stacks, with its actual halt replaced by the next preparation label.

    def program (d e : Nat) (hd : 0 < d) (he : 0 < e) :
        Label d e → TM2.Stmt (fun _ : Tape => Bool) (Label d e) (State A d e)
      | .inl l => Placement.statement Sum.inl Sum.inl (next .copyHFirst)
          (MachineTableSplit.program l)
      | .inr l => mainInstruction d e hd he l

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.Label, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.State, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.next, OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.program, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.mainInstruction

33. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.program_main line 139
34. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.extraTapes line 142
35. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.splitView line 145
36. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.combine line 149
37. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.initialTapes line 153
38. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.splitTapes line 156
39. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.placedTapes line 159
40. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.splitTrace line 165

    Source documentation

    The complete existing splitter is executed, retaining both archives.

    theorem splitTrace (d e : Nat) (hd : 0 < d) (he : 0 < e)
        (table : GraphTables.Table) (rawH : List Bool) (a : A) :
        (advance (TM2.step (program d e hd he)))^[MachineTableSplit.exactSteps
          table.vertices table.darts (MachineTableSplit.rowsBits table)]
          (some ⟨some (.inl .copyFirst), clean d e hd he a,
            initialTapes (GraphTables.tableBits table) rawH⟩) =
          some ⟨next .copyHFirst, clean d e hd he a,
            splitTapes table.vertices table.darts (MachineTableSplit.rowsBits table) rawH⟩ := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.program, OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.exactSteps, OAI.MaxCutGames.Foundations.Complexity.MachineTableSplit.rowsBits, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.clean, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.initialTapes, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.next, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.splitTapes

41. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.memory line 186

    Source documentation

    Every unnamed work tape is empty at these phase boundaries.

    def memory (g h gs hs n m f v t out : List Bool) : Tape → List Bool
      | .inl i => ![g, gs, [], n, m] i
      | .inr i => ![h, hs, f, v, t, [], [], [], [], [], [], out] i

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

42. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.memory_graphArchive line 190
43. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.memory_graphStream line 192
44. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.memory_scratch line 194
45. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.memory_vertexCount line 196
46. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.memory_dartCount line 198
47. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.memory_expanderArchive line 200
48. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.memory_expanderStream line 202
49. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.memory_fuel line 204
50. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.memory_vertex line 206
51. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.memory_tail line 208
52. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.memory_oldReverse line 210
53. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.memory_relation line 212
54. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.memory_dividedCopy line 214
55. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.memory_quotient line 216
56. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.memory_newReverse line 218
57. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.memory_rowBuffer line 220
58. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.memory_output line 222
59. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.update_output line 225
60. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.update_expanderStream line 228
61. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.update_graphStream line 232
62. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.update_fuel line 236
63. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.update_vertex line 239
64. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.update_tail line 242
65. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.update_vertexCount line 245
66. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.update_dartCount line 248
67. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.joinTrace_inline_MachineOverlayTable line 252
68. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.initialTapes_memory line 256
69. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.splitTapes_memory line 263
70. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.preparationSteps line 271
71. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.preparationTrace line 275

    Source documentation

    Preserve and copy raw H, emit both output headers from the parsed unary vertex count, copy the actual fuel field, and initialize the physical counter.

    theorem preparationTrace (d e : Nat) (hd : 0 < d) (he : 0 < e)
        (g h gs : List Bool) (n m : Nat) (a : A) :
        (advance (TM2.step (program d e hd he)))^[preparationSteps n h]
          (some ⟨next .copyHFirst, clean d e hd he a,
            memory g h gs [] (encodeWord n) (encodeWord m) [] [] [] []⟩) =
          some ⟨next .guard, clean d e hd he a,
            memory g h gs h (encodeWord n) (encodeWord m) (encodeWord n) (encodeWord 0) []
              (encodeWords [n, n * (d + e)])⟩ := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.program, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.preparationSteps, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.next, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.clean, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.memory, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.encodeWords

72. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.encodeWords_flatMap_inline_MachineOverlayTable line 343
73. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.encodeWords_flatten_inline_MachineOverlayTable line 349
74. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.encodeWords_flatten_flatMap_inline_MachineOverlayTable line 355
75. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.oldRows line 364
76. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.expanderValues line 365
77. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.oldBlock line 368
78. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.expanderBlock line 370
79. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.oldOutput line 373
80. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.expanderOutput line 375
81. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.outputBlock line 377
82. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.oldOutput_eq line 380
83. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.expanderOutput_eq line 394
84. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.outputBlock_eq line 398
85. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.graphRows_blocks line 404
86. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.expanderRows_blocks line 413
87. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.tableBits_blocks line 418
88. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.remaining line 429
89. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.emittedPrefix line 431
90. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.remaining_step line 434
91. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.prefix_step line 442
92. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.remaining_zero line 449
93. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.remaining_end line 451
94. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.prefix_zero line 455
95. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.prefix_end line 457
96. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.oldFrame line 464
97. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.expanderFrame line 473
98. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.oldVertexTrace line 481
99. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.expanderVertexTrace line 499
100. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.tailCopyTrace line 530
101. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.tailFinishTrace line 547
102. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.pairSteps line 576
103. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.pairTrace line 584

     Source documentation

     The complete old/expander pair for one actual vertex, with both physical stream suffixes and the unchanged unary fuel accounted for.

     theorem pairTrace {n : Nat} (d e : Nat) (hd : 0 < d) (he : 0 < e)
         (G : PortTables.Table n d) (H : ExpanderTables.Table n e) (v : Fin n)
         (g h gs hs nv mv f out : List Bool) (a : A) :
         (advance (TM2.step (program d e hd he)))^[pairSteps G H v out]
           (some ⟨next (.old (0, none)), clean d e hd he a,
             memory g h (oldBlock G v ++ gs) (expanderBlock H v ++ hs)
               nv mv f (encodeWord v.val) [] out⟩) =
           some ⟨next .guard, clean d e hd he a,
             memory g h gs hs nv mv f (encodeWord (v.val + 1)) [] (out ++ outputBlock G H v)⟩ := by
     …

     Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.program, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.pairSteps, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.next, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.clean, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.memory, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.oldBlock, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.expanderBlock, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.outputBlock

104. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.cleanupSteps line 604
105. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.cleanupTrace line 606
106. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.rawExpander line 635
107. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.outputPrefix line 638
108. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.outputPrefix_step line 641
109. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.loopBase line 646
110. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.loopCost line 652
111. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.loopBodyTraces line 660

     Source documentation

     Each body premise needed by the generic unary counted-loop theorem is constructed from the actual old/expander pair execution.

     theorem loopBodyTraces {n : Nat} (d e : Nat) (hd : 0 < d) (he : 0 < e)
         (G : PortTables.Table n d) (H : ExpanderTables.Table n e) (a : A) :
         MachineCountedLoop.BodyTraces fuel (.inr .guard) (.inr (.old (0, none)))
           (program d e hd he) [] (fun _ => (clean d e hd he a).1) (fun _ => none)
           (loopBase G H) (loopCost G H) n := by
     …

     Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCountedLoop.BodyTraces, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.fuel, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.program, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.clean, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.loopBase, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.loopCost

112. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.loopTrace line 696
113. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.tableSteps line 730
114. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.tableTrace line 735
115. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.flatMap_length_le_inline_MachineOverlayTable line 763
116. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.flatten_length_le_inline_MachineOverlayTable line 775
117. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.oldSize line 779
118. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.expanderSize line 780
119. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.blockSize line 781
120. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.oldOutput_length_le line 783
121. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.expanderOutput_length_le line 790
122. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.outputBlock_length_le line 803
123. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.outputCapacity line 811
124. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.outputPrefix_length_le line 813
125. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.pairBudget line 830
126. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.pairSteps_le line 837
127. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.loopSteps_le line 875
128. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.phasePolynomial line 884

     Source documentation

     Polynomial formed from the actual per-row and counted-loop transition budgets. Fixed degree parameters determine its coefficients.

     noncomputable def phasePolynomial (d e : Nat) : Polynomial Nat :=
     …

129. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.phasePolynomial_eval line 900
130. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.timePolynomial line 908
131. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.tableSteps_le line 911
132. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.tableInTime line 928
133. def OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.machine line 941
134. theorem OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.machine_alphabet_finite line 952