OAI/Computability/Logspace/QueryPrograms.lean

GitHub source file

196 declarations, 0 contain sorry, 0 declared as axioms

Bounded query programs with explicit scratch space and finite-margin guarantees.

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

  1. abbrev OAI.ExactDerandomization.Fret.unitB line 18
  2. abbrev OAI.ExactDerandomization.Fret.massB line 19
  3. lemma OAI.ExactDerandomization.Fret.unit1 line 20
  4. lemma OAI.ExactDerandomization.Fret.mass1 line 21
  5. lemma OAI.ExactDerandomization.Fret.mass0 line 22
  6. lemma OAI.ExactDerandomization.Fret.swellB line 23
  7. lemma OAI.ExactDerandomization.Fret.mass_mul line 28
  8. lemma OAI.ExactDerandomization.Fret.mass_mono line 29
  9. structure OAI.ExactDerandomization.Fret.Knob line 32
  10. def OAI.ExactDerandomization.Fret.Align line 37
  11. def OAI.ExactDerandomization.Fret.Live line 38
  12. def OAI.ExactDerandomization.Fret.Ears line 40
  13. lemma OAI.ExactDerandomization.Fret.amplitude line 42
  14. lemma OAI.ExactDerandomization.Fret.fewer line 47
  15. lemma OAI.ExactDerandomization.Fret.supply line 51
  16. def OAI.ExactDerandomization.Fret.amount line 56
  17. lemma OAI.ExactDerandomization.Fret.amountK line 57
  18. lemma OAI.ExactDerandomization.Fret.counted line 58
  19. def OAI.ExactDerandomization.Fret.scaleC line 61
  20. lemma OAI.ExactDerandomization.Fret.scaleK line 62
  21. lemma OAI.ExactDerandomization.Fret.scalen line 63
  22. structure OAI.ExactDerandomization.Fret.Bid line 66
  23. abbrev OAI.ExactDerandomization.Fret.Bid.arm line 74
  24. def OAI.ExactDerandomization.Fret.Bid.remote line 75
  25. lemma OAI.ExactDerandomization.Fret.Bid.remoteK line 79
  26. structure OAI.ExactDerandomization.Fret.Bid.Fit line 85
  27. def OAI.ExactDerandomization.Fret.Bid.uPair line 91
  28. lemma OAI.ExactDerandomization.Fret.Bid.behold line 98
  29. abbrev OAI.ExactDerandomization.Fret.Bid.joinCost line 132
  30. lemma OAI.ExactDerandomization.Fret.Bid.joint line 133
  31. inductive OAI.ExactDerandomization.Fret.Doop line 183
  32. def OAI.ExactDerandomization.Fret.Doop.gate line 189
  33. lemma OAI.ExactDerandomization.Fret.Doop.gateK line 197
  34. def OAI.ExactDerandomization.Fret.Doop.val line 206
  35. def OAI.ExactDerandomization.Fret.Doop.ration line 213
  36. def OAI.ExactDerandomization.Fret.Doop.fast line 214
  37. lemma OAI.ExactDerandomization.Fret.Doop.down_clip line 215
  38. lemma OAI.ExactDerandomization.Fret.Doop.legit line 225
  39. lemma OAI.ExactDerandomization.Fret.Doop.geom line 249
  40. abbrev OAI.ExactDerandomization.Fret.CoinQuery line 275
  41. def OAI.ExactDerandomization.Fret.Brick.center line 278
  42. lemma OAI.ExactDerandomization.Fret.Brick.centerK line 285
  43. def OAI.ExactDerandomization.Fret.Brick.solop line 291
  44. def OAI.ExactDerandomization.Fret.Brick.solo line 294
  45. def OAI.ExactDerandomization.Fret.Brick.tapeR line 295
  46. lemma OAI.ExactDerandomization.Fret.Brick.each0 line 298
  47. structure OAI.ExactDerandomization.Fret.Branch line 332
  48. def OAI.ExactDerandomization.Fret.Branch.port line 340
  49. abbrev OAI.ExactDerandomization.Fret.Branch.S line 341
  50. abbrev OAI.ExactDerandomization.Fret.Branch.key line 342
  51. def OAI.ExactDerandomization.Fret.Branch.bowl line 344
  52. structure OAI.ExactDerandomization.Fret.Branch.Trust line 346
  53. lemma OAI.ExactDerandomization.Fret.Branch.lease line 350
  54. def OAI.ExactDerandomization.Fret.Branch.collect line 372
  55. abbrev OAI.ExactDerandomization.Fret.Branch.reserve line 383
  56. abbrev OAI.ExactDerandomization.Fret.Branch.foldC line 384
  57. lemma OAI.ExactDerandomization.Fret.Branch.poem line 385
  58. inductive OAI.ExactDerandomization.Fret.Lyric line 455
  59. def OAI.ExactDerandomization.Fret.Lyric.weight line 462
  60. def OAI.ExactDerandomization.Fret.Lyric.pulse line 467
  61. def OAI.ExactDerandomization.Fret.Lyric.tail line 468
  62. def OAI.ExactDerandomization.Fret.Lyric.operate line 473
  63. def OAI.ExactDerandomization.Fret.Lyric.cost line 474
  64. lemma OAI.ExactDerandomization.Fret.Lyric.cost_hi line 482
  65. def OAI.ExactDerandomization.Fret.Lyric.choir line 490
  66. inductive OAI.ExactDerandomization.Fret.Lyric.Lethe line 501
  67. theorem OAI.ExactDerandomization.Fret.Lyric.song line 514
  68. lemma OAI.ExactDerandomization.Fret.Lyric.Lethe.bnd line 550
  69. abbrev OAI.ExactDerandomization.Fret.Lyric.bi line 571
  70. lemma OAI.ExactDerandomization.Fret.Lyric.Lethe.bundle line 572
  71. lemma OAI.ExactDerandomization.Fret.Bid.fixedjoint line 588
  72. structure OAI.ExactDerandomization.Fret.Branch.Faith line 630
  73. lemma OAI.ExactDerandomization.Fret.Branch.leased line 634
  74. lemma OAI.ExactDerandomization.Fret.Branch.poems line 649
  75. abbrev OAI.ExactDerandomization.Relay.Cog.repx line 720
  76. lemma OAI.ExactDerandomization.Relay.Cog.repK line 721
  77. def OAI.ExactDerandomization.Relay.Cog.stampT line 723
  78. def OAI.ExactDerandomization.Relay.Cog.outerQ line 725
  79. def OAI.ExactDerandomization.Relay.Cog.ren line 728
  80. lemma OAI.ExactDerandomization.Relay.Cog.renameR line 734
  81. lemma OAI.ExactDerandomization.Relay.Lot.Mane.rise line 756
  82. lemma OAI.ExactDerandomization.Relay.Lot.absorb line 772
  83. lemma OAI.ExactDerandomization.Relay.Lot.Mane.pause line 778
  84. abbrev OAI.ExactDerandomization.Fret.Punct line 806
  85. lemma OAI.ExactDerandomization.Fret.holdroom line 807
  86. lemma OAI.ExactDerandomization.Fret.punctspan line 813
  87. lemma OAI.ExactDerandomization.Fret.plight line 817
  88. lemma OAI.ExactDerandomization.Fret.punct0 line 821
  89. lemma OAI.ExactDerandomization.Fret.punct_up line 823
  90. def OAI.ExactDerandomization.Fret.Cargo.mint line 829
  91. lemma OAI.ExactDerandomization.Fret.Cargo.mintK line 833
  92. def OAI.ExactDerandomization.Fret.Cargo.openx line 836
  93. lemma OAI.ExactDerandomization.Fret.Cargo.openK line 837
  94. def OAI.ExactDerandomization.Fret.Cargo.encase line 838
  95. def OAI.ExactDerandomization.Fret.Cargo.transit line 841
  96. lemma OAI.ExactDerandomization.Fret.Cargo.aboard line 842
  97. def OAI.ExactDerandomization.Fret.Cargo.switch line 853
  98. lemma OAI.ExactDerandomization.Fret.Cargo.switchK line 856
  99. def OAI.ExactDerandomization.Fret.Cargo.strip line 860
  100. lemma OAI.ExactDerandomization.Fret.Cargo.stripK line 861
  101. abbrev OAI.ExactDerandomization.Fret.Cargo.only0 line 863
  102. def OAI.ExactDerandomization.Fret.Cargo.flag0 line 864
  103. def OAI.ExactDerandomization.Fret.Cargo.knock line 865
  104. def OAI.ExactDerandomization.Fret.Cargo.choose line 867
  105. lemma OAI.ExactDerandomization.Fret.Cargo.expands line 870
  106. lemma OAI.ExactDerandomization.Fret.Cargo.flavor line 874
  107. def OAI.ExactDerandomization.Fret.Cargo.combine line 889
  108. lemma OAI.ExactDerandomization.Fret.Cargo.restores line 894
  109. structure OAI.ExactDerandomization.Fret.Camp line 917

    Source documentation

    transparent query/list iteration

    structure Camp where
…
  110. abbrev OAI.ExactDerandomization.Fret.Camp.Info line 925
  111. def OAI.ExactDerandomization.Fret.Camp.cond0 line 926
  112. lemma OAI.ExactDerandomization.Fret.Camp.condK line 927
  113. def OAI.ExactDerandomization.Fret.Camp.work0 line 929
  114. lemma OAI.ExactDerandomization.Fret.Camp.workK line 930
  115. def OAI.ExactDerandomization.Fret.Camp.solve line 933
  116. def OAI.ExactDerandomization.Fret.Camp.walk0 line 934
  117. def OAI.ExactDerandomization.Fret.Camp.n0 line 938
  118. def OAI.ExactDerandomization.Fret.Camp.poster line 939
  119. lemma OAI.ExactDerandomization.Fret.Camp.round line 941
  120. structure OAI.ExactDerandomization.Fret.Badge line 986

    Source documentation

    Probe an actual finite-margin numerical question.

    structure Badge where
…
  121. def OAI.ExactDerandomization.Fret.Badge.one line 995
  122. def OAI.ExactDerandomization.Fret.Badge.dispatch line 998
  123. lemma OAI.ExactDerandomization.Fret.Badge.dispatchK line 1001
  124. abbrev OAI.ExactDerandomization.Fret.Badge.cell line 1005
  125. def OAI.ExactDerandomization.Fret.Badge.valuep line 1007
  126. lemma OAI.ExactDerandomization.Fret.Badge.valueK line 1010
  127. def OAI.ExactDerandomization.Fret.Badge.check line 1016
  128. def OAI.ExactDerandomization.Fret.Badge.plan line 1019
  129. def OAI.ExactDerandomization.Fret.Badge.tariffStart line 1020
  130. def OAI.ExactDerandomization.Fret.Badge.tariff line 1021
  131. lemma OAI.ExactDerandomization.Fret.Badge.query line 1022
  132. lemma OAI.ExactDerandomization.Fret.Badge.accuracy line 1057
  133. structure OAI.ExactDerandomization.Fret.Seats line 1082
  134. abbrev OAI.ExactDerandomization.Fret.Seats.d line 1089
  135. abbrev OAI.ExactDerandomization.Fret.Seats.l line 1090
  136. abbrev OAI.ExactDerandomization.Fret.Seats.info line 1091
  137. abbrev OAI.ExactDerandomization.Fret.Seats.seat line 1092
  138. def OAI.ExactDerandomization.Fret.Seats.hasOK line 1093
  139. def OAI.ExactDerandomization.Fret.Seats.stable line 1094
  140. abbrev OAI.ExactDerandomization.Fret.Seats.panelx line 1095
  141. abbrev OAI.ExactDerandomization.Fret.Seats.bench line 1096
  142. lemma OAI.ExactDerandomization.Fret.Seats.home line 1098
  143. lemma OAI.ExactDerandomization.Fret.Seats.stable_home line 1099
  144. lemma OAI.ExactDerandomization.Fret.Seats.has_home line 1100
  145. lemma OAI.ExactDerandomization.Fret.Seats.rocks line 1101
  146. def OAI.ExactDerandomization.Fret.Seats.loud line 1103
  147. def OAI.ExactDerandomization.Fret.Seats.band line 1104
  148. lemma OAI.ExactDerandomization.Fret.Seats.maxv line 1105
  149. lemma OAI.ExactDerandomization.Fret.Seats.flex line 1107
  150. abbrev OAI.ExactDerandomization.Fret.Seats.freq line 1109
  151. def OAI.ExactDerandomization.Fret.Seats.full line 1110
  152. lemma OAI.ExactDerandomization.Fret.Seats.located line 1112
  153. lemma OAI.ExactDerandomization.Fret.Seats.leasedD line 1121
  154. lemma OAI.ExactDerandomization.Fret.Seats.rhymeD line 1126
  155. lemma OAI.ExactDerandomization.Fret.Seats.duetD line 1130
  156. def OAI.ExactDerandomization.Fret.Seats.hear line 1138
  157. abbrev OAI.ExactDerandomization.Fret.Seats.rite line 1139
  158. lemma OAI.ExactDerandomization.Fret.Seats.avis line 1141
  159. abbrev OAI.ExactDerandomization.Fret.Seats.berth line 1162
  160. lemma OAI.ExactDerandomization.Fret.Seats.advises line 1164
  161. inductive OAI.ExactDerandomization.Fret.Lyric.Chor line 1182
  162. lemma OAI.ExactDerandomization.Fret.Lyric.sing line 1196
  163. lemma OAI.ExactDerandomization.Fret.Lyric.Chor.nominal line 1238
  164. lemma OAI.ExactDerandomization.Fret.Lyric.Chor.minuet line 1247
  165. lemma OAI.ExactDerandomization.Fret.Seats.higher line 1262
  166. lemma OAI.ExactDerandomization.Fret.Seats.pointed0 line 1264
  167. abbrev OAI.ExactDerandomization.Fret.Seats.nothingX line 1267
  168. lemma OAI.ExactDerandomization.Fret.Seats.blankD line 1268
  169. lemma OAI.ExactDerandomization.Fret.Seats.steer line 1271
  170. abbrev OAI.ExactDerandomization.Fret.Seats.transformed line 1283
  171. lemma OAI.ExactDerandomization.Fret.Seats.importD line 1284
  172. lemma OAI.ExactDerandomization.Fret.Seats.transportD line 1290
  173. structure OAI.ExactDerandomization.Fret.Seek line 1302

    Source documentation

    Pick the zero-based kth nonzero answer; the pair of index and answer is positive, or 0 if none.

    structure Seek where
…
  174. abbrev OAI.ExactDerandomization.Fret.Seek.bin line 1308
  175. lemma OAI.ExactDerandomization.Fret.Seek.binpos line 1309
  176. abbrev OAI.ExactDerandomization.Fret.Seek.SeqN line 1310
  177. def OAI.ExactDerandomization.Fret.Seek.transfer line 1311
  178. def OAI.ExactDerandomization.Fret.Seek.relief line 1314
  179. def OAI.ExactDerandomization.Fret.Seek.part line 1317
  180. lemma OAI.ExactDerandomization.Fret.Seek.heightp line 1319
  181. lemma OAI.ExactDerandomization.Fret.Seek.countle line 1329
  182. lemma OAI.ExactDerandomization.Fret.Seek.catalogs line 1330
  183. lemma OAI.ExactDerandomization.Fret.Seek.ticket line 1331
  184. lemma OAI.ExactDerandomization.Fret.Seek.order line 1337
  185. lemma OAI.ExactDerandomization.Fret.Seek.found_min line 1345
  186. lemma OAI.ExactDerandomization.Fret.Seek.missed line 1359
  187. lemma OAI.ExactDerandomization.Fret.Seek.casebook line 1375
  188. abbrev OAI.ExactDerandomization.Fret.Seek.grainK line 1382
  189. def OAI.ExactDerandomization.Fret.Seek.fill line 1389
  190. lemma OAI.ExactDerandomization.Fret.Seek.fillK line 1393
  191. def OAI.ExactDerandomization.Fret.Seek.road line 1397
  192. lemma OAI.ExactDerandomization.Fret.Seek.roadK line 1398
  193. def OAI.ExactDerandomization.Fret.Seek.tent line 1401
  194. def OAI.ExactDerandomization.Fret.Seek.latch line 1402
  195. abbrev OAI.ExactDerandomization.Fret.Seek.N line 1405
  196. lemma OAI.ExactDerandomization.Fret.Seek.earns line 1407