OAI/Computability/UniqueGames/Machines/MachineOverlayTable.lean

GitHub source file

134 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.Tape line 17
2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.Ambient line 18
3. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.State line 19
4. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.graphArchive line 21
5. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.graphStream line 22
6. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.scratch line 23
7. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.vertexCount line 24
8. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.dartCount line 25
9. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.expanderArchive line 26
10. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.expanderStream line 27
11. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.fuel line 28
12. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.vertex line 29
13. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.tail line 30
14. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.oldReverse line 31
15. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.relation line 32
16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.dividedCopy line 33
17. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.quotient line 34
18. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.newReverse line 35
19. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.rowBuffer line 36
20. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.output line 37
21. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.oldTapes line 39
22. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.expanderTapes line 43
23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.oldTapes_injective line 47
24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.expanderTapes_injective line 53
25. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.clean line 59
26. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.expanderState line 62
27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.expanderState_clean line 71
28. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.MainLabel line 76
29. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.Label line 88
30. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.next line 90
31. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.mainInstruction line 94

    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 AmbientState 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.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.MainLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.State, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.loopAt, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.expanderArchive, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.scratch, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.next, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.forkLoop, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.expanderStream, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.seed, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.output, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryAffineAt.scan, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.vertexCount

32. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.program line 136

    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 AmbientState 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.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.next, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.mainInstruction

33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.program_main line 142
34. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.extraTapes line 145
35. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.splitView line 148
36. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.combine line 152
37. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.initialTapes line 156
38. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.splitTapes line 159
39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.placedTapes line 162
40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.splitTrace line 168

    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 : AmbientState) :
        (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.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.exactSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableSplit.rowsBits, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.clean, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.initialTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.next, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.splitTapes

41. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.memory line 189

    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.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.Tape

42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.memory_graphArchive line 193
43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.memory_graphStream line 195
44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.memory_scratch line 197
45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.memory_vertexCount line 199
46. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.memory_dartCount line 201
47. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.memory_expanderArchive line 203
48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.memory_expanderStream line 205
49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.memory_fuel line 207
50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.memory_vertex line 209
51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.memory_tail line 211
52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.memory_oldReverse line 213
53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.memory_relation line 215
54. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.memory_dividedCopy line 217
55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.memory_quotient line 219
56. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.memory_newReverse line 221
57. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.memory_rowBuffer line 223
58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.memory_output line 225
59. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.update_output line 228
60. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.update_expanderStream line 231
61. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.update_graphStream line 235
62. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.update_fuel line 239
63. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.update_vertex line 242
64. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.update_tail line 245
65. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.update_vertexCount line 248
66. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.update_dartCount line 251
67. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.joinTrace line 255
68. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.initialTapes_memory line 259
69. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.splitTapes_memory line 266
70. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.preparationSteps line 274
71. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.preparationTrace line 278

    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 : AmbientState) :
        (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.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.preparationSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.next, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.clean, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.memory, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords

72. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.encodeWords_flatMap line 346
73. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.encodeWords_flatten line 352
74. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.encodeWords_flatten_flatMap line 358
75. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.oldRows line 367
76. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.expanderValues line 368
77. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.oldBlock line 371
78. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.expanderBlock line 373
79. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.oldOutput line 376
80. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.expanderOutput line 378
81. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.outputBlock line 380
82. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.oldOutput_eq line 383
83. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.expanderOutput_eq line 397
84. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.outputBlock_eq line 401
85. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.graphRows_blocks line 407
86. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.expanderRows_blocks line 416
87. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.tableBits_blocks line 421
88. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.remaining line 432
89. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.emittedPrefix line 434
90. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.remaining_step line 437
91. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.prefix_step line 445
92. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.remaining_zero line 452
93. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.remaining_end line 454
94. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.prefix_zero line 458
95. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.prefix_end line 460
96. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.oldFrame line 467
97. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.expanderFrame line 476
98. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.oldVertexTrace line 484
99. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.expanderVertexTrace line 503
100. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.tailCopyTrace line 535
101. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.tailFinishTrace line 552
102. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.pairSteps line 581
103. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.pairTrace line 589

     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 : AmbientState) :
         (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.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.pairSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.next, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.clean, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.memory, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.oldBlock, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.expanderBlock, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.outputBlock

104. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.cleanupSteps line 609
105. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.cleanupTrace line 611
106. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.rawExpander line 640
107. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.outputPrefix line 643
108. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.outputPrefix_step line 646
109. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.loopBase line 651
110. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.loopCost line 657
111. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.loopBodyTraces line 665

     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 : AmbientState) :
         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.UniqueGamesTheorem.Foundations.Complexity.MachineCountedLoop.BodyTraces, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.fuel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.clean, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.loopBase, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.loopCost

112. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.loopTrace line 701
113. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.tableSteps line 735
114. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.tableTrace line 740
115. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.flatMap_length_le line 768
116. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.flatten_length_le line 780
117. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.oldSize line 784
118. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.expanderSize line 785
119. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.blockSize line 786
120. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.oldOutput_length_le line 788
121. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.expanderOutput_length_le line 795
122. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.outputBlock_length_le line 808
123. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.outputCapacity line 816
124. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.outputPrefix_length_le line 818
125. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.pairBudget line 835
126. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.pairSteps_le line 842
127. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.loopSteps_le line 879
128. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.phasePolynomial line 888

     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.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.phasePolynomial_eval line 904
130. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.timePolynomial line 912
131. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.tableSteps_le line 915
132. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.tableInTime line 932
133. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.machine line 945
134. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.machine_alphabet_finite line 956