OAI/Computability/Logspace/EstimatorInstructions.lean

GitHub source file

245 declarations, 0 contain sorry, 0 declared as axioms

Instruction encodings and resource parameters for the estimator.

From OpenAI, Exact Derandomization of Logarithmic Space: L = RL = BPL.

  1. abbrev OAI.ExactDerandomization.Helix.ID line 21

    Source comment

    Types used by the spine of the system.
    abbrev ID := ℕ × ℕ × ℕ×ℕ
  2. abbrev OAI.ExactDerandomization.Helix.ChoiceX line 22
  3. abbrev OAI.ExactDerandomization.Helix.Scout line 23
  4. abbrev OAI.ExactDerandomization.Helix.ClockH line 24
  5. abbrev OAI.ExactDerandomization.Helix.Crt line 25
  6. abbrev OAI.ExactDerandomization.Helix.Age.MV line 29
  7. abbrev OAI.ExactDerandomization.Helix.Age.g line 30
  8. abbrev OAI.ExactDerandomization.Helix.Age.styx line 31
  9. abbrev OAI.ExactDerandomization.Helix.Age.env line 32
  10. abbrev OAI.ExactDerandomization.Helix.Age.L line 33
  11. abbrev OAI.ExactDerandomization.Helix.Age.gap line 34
  12. def OAI.ExactDerandomization.Helix.Age.Brole line 35
  13. instance OAI.ExactDerandomization.Helix.Age.roleD line 36
  14. abbrev OAI.ExactDerandomization.Helix.Age.Period line 38
  15. abbrev OAI.ExactDerandomization.Helix.Age.slackT line 39
  16. def OAI.ExactDerandomization.Helix.Age.weight line 40
  17. def OAI.ExactDerandomization.Helix.Age.act line 41
  18. def OAI.ExactDerandomization.Helix.Age.due line 42
  19. lemma OAI.ExactDerandomization.Helix.Age.gap_pos line 43
  20. lemma OAI.ExactDerandomization.Helix.Age.gap_le line 44
  21. lemma OAI.ExactDerandomization.Helix.Age.pace line 50
  22. lemma OAI.ExactDerandomization.Helix.Age.weights line 54
  23. lemma OAI.ExactDerandomization.Helix.Age.well line 58
  24. lemma OAI.ExactDerandomization.Helix.Age.sooner line 63
  25. lemma OAI.ExactDerandomization.Helix.Age.gap_step line 70
  26. lemma OAI.ExactDerandomization.Helix.Age.oldpay line 72
  27. lemma OAI.ExactDerandomization.Helix.Age.renewal line 79
  28. lemma OAI.ExactDerandomization.Helix.Age.endbirth line 85
  29. lemma OAI.ExactDerandomization.Helix.Age.LB line 93
  30. lemma OAI.ExactDerandomization.Helix.Age.gapK line 94
  31. lemma OAI.ExactDerandomization.Helix.Age.slackK line 97
  32. lemma OAI.ExactDerandomization.Helix.Age.actK line 99
  33. def OAI.ExactDerandomization.Helix.Age.W line 104
  34. def OAI.ExactDerandomization.Helix.Age.D line 105
  35. lemma OAI.ExactDerandomization.Helix.Age.WK line 106
  36. lemma OAI.ExactDerandomization.Helix.Age.DK line 107
  37. lemma OAI.ExactDerandomization.Helix.Age.cpos line 110
  38. lemma OAI.ExactDerandomization.Helix.Age.WI line 111
  39. lemma OAI.ExactDerandomization.Helix.Age.DI line 112
  40. abbrev OAI.ExactDerandomization.Helix.Foil.kit line 124
  41. def OAI.ExactDerandomization.Helix.Foil.aspect line 125
  42. def OAI.ExactDerandomization.Helix.Foil.shaped line 128
  43. abbrev OAI.ExactDerandomization.Helix.Foil.dataR line 134
  44. def OAI.ExactDerandomization.Helix.Foil.claim line 135
  45. def OAI.ExactDerandomization.Helix.Foil.bitR line 138
  46. def OAI.ExactDerandomization.Helix.Foil.gaze line 141
  47. def OAI.ExactDerandomization.Helix.Foil.bitV line 143
  48. lemma OAI.ExactDerandomization.Helix.Foil.recovery line 145
  49. lemma OAI.ExactDerandomization.Helix.Foil.recovered line 147
  50. def OAI.ExactDerandomization.Helix.Foil.faceR line 150
  51. def OAI.ExactDerandomization.Helix.Foil.faceV line 151
  52. lemma OAI.ExactDerandomization.Helix.Foil.copyR line 153
  53. lemma OAI.ExactDerandomization.Helix.Foil.copyV line 157
  54. lemma OAI.ExactDerandomization.Helix.Foil.rightR line 161
  55. lemma OAI.ExactDerandomization.Helix.Foil.rightV line 167
  56. lemma OAI.ExactDerandomization.Helix.Foil.solely line 168
  57. def OAI.ExactDerandomization.Helix.Foil.testR line 172
  58. def OAI.ExactDerandomization.Helix.Foil.testV line 175
  59. def OAI.ExactDerandomization.Helix.Foil.operateR line 178
  60. def OAI.ExactDerandomization.Helix.Foil.operateV line 181
  61. def OAI.ExactDerandomization.Helix.Foil.delta0 line 185
  62. def OAI.ExactDerandomization.Helix.Foil.redV line 186
  63. def OAI.ExactDerandomization.Helix.Foil.Bob line 187
  64. def OAI.ExactDerandomization.Helix.Foil.rowUnit line 188
  65. def OAI.ExactDerandomization.Helix.Foil.vecUnit line 190
  66. def OAI.ExactDerandomization.Helix.Foil.permit line 191
  67. def OAI.ExactDerandomization.Helix.GK line 211
  68. lemma OAI.ExactDerandomization.Helix.GK.orG line 214
  69. lemma OAI.ExactDerandomization.Helix.GK.andG line 217
  70. lemma OAI.ExactDerandomization.Helix.GK.notG line 220
  71. lemma OAI.ExactDerandomization.Helix.GK.forth line 222
  72. lemma OAI.ExactDerandomization.Helix.GK.backG line 223
  73. lemma OAI.ExactDerandomization.Helix.GK.decideK line 225
  74. lemma OAI.ExactDerandomization.Helix.GK.ofdec line 227
  75. lemma OAI.ExactDerandomization.Helix.GK.eqG line 230
  76. lemma OAI.ExactDerandomization.Helix.GK.ltG line 231
  77. lemma OAI.ExactDerandomization.Helix.GK.leG line 232
  78. lemma OAI.ExactDerandomization.Helix.GK.ifG line 233
  79. lemma OAI.ExactDerandomization.Helix.Foil.faceRK line 243
  80. lemma OAI.ExactDerandomization.Helix.Foil.faceVK line 246
  81. lemma OAI.ExactDerandomization.Helix.Foil.testRK line 253
  82. lemma OAI.ExactDerandomization.Helix.Foil.testVK line 270
  83. lemma OAI.ExactDerandomization.Helix.Foil.coreK line 278
  84. lemma OAI.ExactDerandomization.Helix.Foil.heightK line 280
  85. theorem OAI.ExactDerandomization.Helix.Foil.XrankK line 300
  86. lemma OAI.ExactDerandomization.Helix.Foil.onRK line 304
  87. lemma OAI.ExactDerandomization.Helix.Foil.onVK line 307
  88. lemma OAI.ExactDerandomization.Helix.Foil.bobG line 312
  89. lemma OAI.ExactDerandomization.Helix.Foil.topK line 321
  90. lemma OAI.ExactDerandomization.Helix.Foil.roofK line 325
  91. lemma OAI.ExactDerandomization.Helix.Foil.permitted line 327
  92. structure OAI.ExactDerandomization.Helix.Moon.Tags line 355

    Source documentation

    Live structure prices and hyperparameters selected before running the program.

    structure Tags where
…
  93. abbrev OAI.ExactDerandomization.Helix.Moon.M line 363
  94. abbrev OAI.ExactDerandomization.Helix.Moon.planets line 364
  95. abbrev OAI.ExactDerandomization.Helix.Moon.T line 365
  96. lemma OAI.ExactDerandomization.Helix.Moon.Mk line 366
  97. lemma OAI.ExactDerandomization.Helix.Moon.TKn line 367
  98. abbrev OAI.ExactDerandomization.Helix.Moon.roof line 369
  99. lemma OAI.ExactDerandomization.Helix.Moon.crowX line 370
  100. abbrev OAI.ExactDerandomization.Helix.Moon.WaresCap line 371
  101. abbrev OAI.ExactDerandomization.Helix.Moon.hill0 line 373
  102. abbrev OAI.ExactDerandomization.Helix.Moon.hill line 374
  103. abbrev OAI.ExactDerandomization.Helix.Moon.fillA line 375
  104. def OAI.ExactDerandomization.Helix.Moon.topo line 376
  105. lemma OAI.ExactDerandomization.Helix.Moon.hillKn line 380
  106. lemma OAI.ExactDerandomization.Helix.Moon.maxK line 383
  107. lemma OAI.ExactDerandomization.Helix.Moon.upclock line 389
  108. lemma OAI.ExactDerandomization.Helix.Moon.stationK line 397
  109. lemma OAI.ExactDerandomization.Helix.Moon.storageK line 401
  110. abbrev OAI.ExactDerandomization.Helix.Moon.Candle line 405
  111. def OAI.ExactDerandomization.Helix.Moon.capAX line 406
  112. def OAI.ExactDerandomization.Helix.Moon.wax line 408
  113. lemma OAI.ExactDerandomization.Helix.Moon.waxK line 409
  114. lemma OAI.ExactDerandomization.Helix.Moon.craned line 414
  115. lemma OAI.ExactDerandomization.Helix.Moon.scouttop line 421
  116. def OAI.ExactDerandomization.Helix.Orbit.licensed line 484
  117. abbrev OAI.ExactDerandomization.Helix.Orbit.post line 485
  118. def OAI.ExactDerandomization.Helix.Orbit.opt line 486
  119. def OAI.ExactDerandomization.Helix.Orbit.posn line 487
  120. lemma OAI.ExactDerandomization.Helix.Orbit.optionX line 488
  121. lemma OAI.ExactDerandomization.Helix.Orbit.targetX line 489
  122. def OAI.ExactDerandomization.Helix.Orbit.omegaQ line 490
  123. def OAI.ExactDerandomization.Helix.Orbit.colorQ line 491
  124. def OAI.ExactDerandomization.Helix.Orbit.taps line 492
  125. def OAI.ExactDerandomization.Helix.Orbit.entitled line 495
  126. def OAI.ExactDerandomization.Helix.Orbit.paired line 500
  127. abbrev OAI.ExactDerandomization.Helix.Orbit.idx line 506
  128. def OAI.ExactDerandomization.Helix.Orbit.location line 507
  129. lemma OAI.ExactDerandomization.Helix.Orbit.licensedK line 512
  130. lemma OAI.ExactDerandomization.Helix.Orbit.entitlementK line 515
  131. lemma OAI.ExactDerandomization.Helix.Orbit.pledgeK line 533
  132. def OAI.ExactDerandomization.Helix.Orbit.schedule line 545
  133. lemma OAI.ExactDerandomization.Helix.Orbit.licensedW line 551
  134. lemma OAI.ExactDerandomization.Helix.Orbit.licensedD line 557
  135. abbrev OAI.ExactDerandomization.Helix.Night.pigmentA line 576
  136. abbrev OAI.ExactDerandomization.Helix.Night.qlim line 577
  137. abbrev OAI.ExactDerandomization.Helix.Night.tiny line 578
  138. def OAI.ExactDerandomization.Helix.Night.billQ line 579
  139. def OAI.ExactDerandomization.Helix.Night.fRock line 585
  140. lemma OAI.ExactDerandomization.Helix.Night.billK line 592
  141. lemma OAI.ExactDerandomization.Helix.Night.fRockK line 597
  142. def OAI.ExactDerandomization.Helix.Night.stageC line 605
  143. def OAI.ExactDerandomization.Helix.Night.field line 610
  144. def OAI.ExactDerandomization.Helix.Night.wick line 611
  145. lemma OAI.ExactDerandomization.Helix.Night.scenic line 612
  146. lemma OAI.ExactDerandomization.Helix.Night.topo_hi line 629
  147. lemma OAI.ExactDerandomization.Helix.Night.dawn line 634
  148. lemma OAI.ExactDerandomization.Helix.Night.cap_time line 641
  149. lemma OAI.ExactDerandomization.Helix.Night.Orchestra line 643
  150. lemma OAI.ExactDerandomization.Helix.Night.town line 651
  151. lemma OAI.ExactDerandomization.Helix.Night.launch line 652
  152. lemma OAI.ExactDerandomization.Helix.Night.localC line 656
  153. lemma OAI.ExactDerandomization.Helix.Night.chask line 663
  154. lemma OAI.ExactDerandomization.Helix.Night.pairbill line 672
  155. abbrev OAI.ExactDerandomization.Helix.Torch.innate line 702
  156. abbrev OAI.ExactDerandomization.Helix.Torch.denote line 707
  157. abbrev OAI.ExactDerandomization.Helix.Torch.Part line 708
  158. def OAI.ExactDerandomization.Helix.Torch.ray line 710
  159. lemma OAI.ExactDerandomization.Helix.Torch.decorK line 718
  160. def OAI.ExactDerandomization.Helix.Torch.lamp line 748
  161. lemma OAI.ExactDerandomization.Helix.Torch.lampK line 749
  162. def OAI.ExactDerandomization.Helix.Torch.harp line 750
  163. lemma OAI.ExactDerandomization.Helix.Torch.tints line 752
  164. lemma OAI.ExactDerandomization.Helix.Torch.life line 765
  165. abbrev OAI.ExactDerandomization.Helix.Torch.charm line 769
  166. abbrev OAI.ExactDerandomization.Helix.Torch.trail line 770
  167. abbrev OAI.ExactDerandomization.Helix.Torch.measureL line 771
  168. abbrev OAI.ExactDerandomization.Helix.Torch.waxy line 772
  169. lemma OAI.ExactDerandomization.Helix.Torch.housed line 773
  170. lemma OAI.ExactDerandomization.Helix.Torch.litwax line 778
  171. lemma OAI.ExactDerandomization.Helix.Torch.litmode line 781
  172. def OAI.ExactDerandomization.Helix.Was.air line 801
  173. lemma OAI.ExactDerandomization.Helix.Was.atm line 802
  174. lemma OAI.ExactDerandomization.Helix.Was.birth line 804
  175. def OAI.ExactDerandomization.Helix.Was.moon0 line 809
  176. def OAI.ExactDerandomization.Helix.Was.bin0 line 810
  177. abbrev OAI.ExactDerandomization.Helix.Was.bright line 811
  178. lemma OAI.ExactDerandomization.Helix.Was.lower0 line 812
  179. lemma OAI.ExactDerandomization.Helix.Was.equal0 line 819
  180. abbrev OAI.ExactDerandomization.Helix.Was.Kpre line 826
  181. lemma OAI.ExactDerandomization.Helix.Was.passage line 827
  182. abbrev OAI.ExactDerandomization.Helix.Was.atom line 838
  183. abbrev OAI.ExactDerandomization.Helix.Was.radixG line 839
  184. abbrev OAI.ExactDerandomization.Helix.Was.fan line 840
  185. abbrev OAI.ExactDerandomization.Helix.Was.downX line 841
  186. abbrev OAI.ExactDerandomization.Helix.Was.avails line 842
  187. def OAI.ExactDerandomization.Helix.Was.Flight line 844
  188. lemma OAI.ExactDerandomization.Helix.Was.fly_pair line 851
  189. lemma OAI.ExactDerandomization.Helix.Was.fly_one line 870
  190. lemma OAI.ExactDerandomization.Helix.Was.edgeK line 890
  191. lemma OAI.ExactDerandomization.Helix.Was.moonG line 891
  192. lemma OAI.ExactDerandomization.Helix.Was.brightK line 895
  193. lemma OAI.ExactDerandomization.Helix.Was.faf line 907
  194. def OAI.ExactDerandomization.Helix.Was.map0 line 939
  195. abbrev OAI.ExactDerandomization.Helix.Was.Clasp line 940
  196. def OAI.ExactDerandomization.Helix.Was.lastP line 941
  197. def OAI.ExactDerandomization.Helix.Was.unitN line 942
  198. lemma OAI.ExactDerandomization.Helix.Was.unitKN line 943
  199. abbrev OAI.ExactDerandomization.Helix.Was.walkq line 954
  200. def OAI.ExactDerandomization.Helix.Was.stopped line 955
  201. lemma OAI.ExactDerandomization.Helix.Was.travel line 959
  202. abbrev OAI.ExactDerandomization.Helix.Was.Cube line 981
  203. def OAI.ExactDerandomization.Helix.Was.wrapP line 982
  204. lemma OAI.ExactDerandomization.Helix.Was.wrapK line 987
  205. def OAI.ExactDerandomization.Helix.Was.basic line 994
  206. abbrev OAI.ExactDerandomization.Helix.Was.packB line 996
  207. lemma OAI.ExactDerandomization.Helix.Was.decideWay line 997
  208. theorem OAI.ExactDerandomization.Helix.Was.motion line 1002
  209. abbrev OAI.ExactDerandomization.Helix.Mold.Crux line 1053
  210. abbrev OAI.ExactDerandomization.Helix.Mold.Aide line 1055
  211. abbrev OAI.ExactDerandomization.Helix.Mold.Croft line 1056
  212. abbrev OAI.ExactDerandomization.Helix.Mold.lips line 1057
  213. abbrev OAI.ExactDerandomization.Helix.Mold.stint line 1058
  214. abbrev OAI.ExactDerandomization.Helix.Mold.pointer line 1059
  215. abbrev OAI.ExactDerandomization.Helix.Mold.uphold line 1060
  216. def OAI.ExactDerandomization.Helix.Mold.visitX line 1061
  217. lemma OAI.ExactDerandomization.Helix.Mold.visitXK line 1063
  218. abbrev OAI.ExactDerandomization.Helix.Mold.assignT line 1069
  219. abbrev OAI.ExactDerandomization.Helix.Mold.selop line 1070
  220. def OAI.ExactDerandomization.Helix.Mold.send line 1071
  221. lemma OAI.ExactDerandomization.Helix.Mold.sendK line 1074
  222. def OAI.ExactDerandomization.Helix.Mold.rope line 1081
  223. lemma OAI.ExactDerandomization.Helix.Mold.ropeK line 1083
  224. def OAI.ExactDerandomization.Helix.Mold.tailR line 1085
  225. lemma OAI.ExactDerandomization.Helix.Mold.tailRK line 1086
  226. abbrev OAI.ExactDerandomization.Helix.Mold.Pose line 1090
  227. def OAI.ExactDerandomization.Helix.Mold.offer line 1091
  228. lemma OAI.ExactDerandomization.Helix.Mold.offerK line 1098
  229. def OAI.ExactDerandomization.Helix.Mold.flexQ line 1107
  230. lemma OAI.ExactDerandomization.Helix.Mold.flexK line 1108
  231. def OAI.ExactDerandomization.Helix.Mold.coneX line 1111
  232. def OAI.ExactDerandomization.Helix.Mold.knob line 1118
  233. lemma OAI.ExactDerandomization.Helix.Mold.highflex line 1120
  234. abbrev OAI.ExactDerandomization.Helix.Mold.bandD line 1123
  235. lemma OAI.ExactDerandomization.Helix.Mold.knows line 1124
  236. structure OAI.ExactDerandomization.Helix.Mold.Stash line 1128
  237. def OAI.ExactDerandomization.Helix.Mold.codeRank line 1132
  238. def OAI.ExactDerandomization.Helix.Mold.who line 1135
  239. lemma OAI.ExactDerandomization.Helix.Mold.whoK line 1136
  240. def OAI.ExactDerandomization.Helix.Mold.dust line 1138
  241. def OAI.ExactDerandomization.Helix.Mold.visitMain line 1139
  242. abbrev OAI.ExactDerandomization.Helix.Mold.woven line 1142
  243. lemma OAI.ExactDerandomization.Helix.Mold.seated line 1145
  244. abbrev OAI.ExactDerandomization.Helix.Mold.unitV line 1155
  245. lemma OAI.ExactDerandomization.Helix.Mold.sizeR line 1156