OAI/Computability/Logspace/DyadicArithmetic.lean

GitHub source file

243 declarations, 0 contain sorry, 0 declared as axioms

Redundant dyadic digits, signed arithmetic, and bounded-precision numerical queries.

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

  1. def OAI.ExactDerandomization.Relay.slate line 20
  2. def OAI.ExactDerandomization.Relay.stone line 21
  3. def OAI.ExactDerandomization.Relay.scree line 22
  4. lemma OAI.ExactDerandomization.Relay.screenp line 24
  5. lemma OAI.ExactDerandomization.Relay.slate_stone line 26
  6. instance OAI.ExactDerandomization.Relay.(instance at line 28) line 28
  7. def OAI.ExactDerandomization.Relay.pairInt line 39
  8. lemma OAI.ExactDerandomization.Relay.Kn.splitZ line 42
  9. lemma OAI.ExactDerandomization.Relay.Kn.topNat line 46
  10. lemma OAI.ExactDerandomization.Relay.Kn.negNat line 48
  11. lemma OAI.ExactDerandomization.Relay.Kn.ZofN line 51
  12. lemma OAI.ExactDerandomization.Relay.Kn.rock line 58
  13. lemma OAI.ExactDerandomization.Relay.Kn.plusZ line 65
  14. lemma OAI.ExactDerandomization.Relay.Kn.negZ line 68
  15. lemma OAI.ExactDerandomization.Relay.Kn.absN line 71
  16. lemma OAI.ExactDerandomization.Relay.Kn.leZ line 74
  17. lemma OAI.ExactDerandomization.Relay.Kn.prodZ line 78
  18. lemma OAI.ExactDerandomization.Relay.Kn.minZ line 90
  19. lemma OAI.ExactDerandomization.Relay.Kn.maxZ line 92
  20. lemma OAI.ExactDerandomization.Relay.Kn.down_eq line 95
  21. lemma OAI.ExactDerandomization.Relay.Kn.chop line 111
  22. lemma OAI.ExactDerandomization.Relay.Kn.modulus line 126
  23. lemma OAI.ExactDerandomization.Relay.Zbound line 134
  24. abbrev OAI.ExactDerandomization.Rill.Tape line 151
  25. def OAI.ExactDerandomization.Rill.dsign line 152
  26. def OAI.ExactDerandomization.Rill.Checked line 154
  27. lemma OAI.ExactDerandomization.Rill.safe_d line 156
  28. lemma OAI.ExactDerandomization.Rill.slate_le line 170
  29. abbrev OAI.ExactDerandomization.Rill.capD line 172
  30. abbrev OAI.ExactDerandomization.Rill.History line 174
  31. def OAI.ExactDerandomization.Rill.postcard line 175
  32. abbrev OAI.ExactDerandomization.Rill.clockK line 176
  33. structure OAI.ExactDerandomization.Rill.Port line 178
  34. def OAI.ExactDerandomization.Rill.Port.OK line 187
  35. abbrev OAI.ExactDerandomization.Rill.Port.comp line 188
  36. abbrev OAI.ExactDerandomization.Rill.Port.s line 189
  37. structure OAI.ExactDerandomization.Rill.Port.Uses line 191
  38. def OAI.ExactDerandomization.Rill.Port.Feeds line 193
  39. abbrev OAI.ExactDerandomization.Rill.Port.Tells line 194
  40. lemma OAI.ExactDerandomization.Rill.Port.alone line 196
  41. lemma OAI.ExactDerandomization.Rill.Port.stale line 202
  42. lemma OAI.ExactDerandomization.Rill.sumsign line 207
  43. lemma OAI.ExactDerandomization.Rill.suffixes line 221
  44. abbrev OAI.ExactDerandomization.Rill.Wgt line 239
  45. abbrev OAI.ExactDerandomization.Rill.Comb line 240
  46. abbrev OAI.ExactDerandomization.Rill.Ream line 241
  47. abbrev OAI.ExactDerandomization.Rill.DW line 242
  48. abbrev OAI.ExactDerandomization.Rill.EV line 243
  49. structure OAI.ExactDerandomization.Rill.Oven line 244
  50. def OAI.ExactDerandomization.Rill.Oven.era line 252
  51. lemma OAI.ExactDerandomization.Rill.Oven.eraK line 254
  52. def OAI.ExactDerandomization.Rill.Oven.still line 257
  53. lemma OAI.ExactDerandomization.Rill.Oven.stillK line 258
  54. def OAI.ExactDerandomization.Rill.Oven.test line 259
  55. lemma OAI.ExactDerandomization.Rill.Oven.testK line 261
  56. def OAI.ExactDerandomization.Rill.Oven.pointer line 264
  57. lemma OAI.ExactDerandomization.Rill.Oven.pointerK line 268
  58. def OAI.ExactDerandomization.Rill.Oven.inflate line 274
  59. lemma OAI.ExactDerandomization.Rill.Oven.inflateK line 275
  60. def OAI.ExactDerandomization.Rill.Oven.plusone line 277
  61. def OAI.ExactDerandomization.Rill.Oven.score line 278
  62. def OAI.ExactDerandomization.Rill.Oven.backq line 281
  63. lemma OAI.ExactDerandomization.Rill.Oven.backK line 283
  64. def OAI.ExactDerandomization.Rill.Oven.march line 295
  65. lemma OAI.ExactDerandomization.Rill.Oven.marchK line 298
  66. def OAI.ExactDerandomization.Rill.Oven.hoop line 301
  67. lemma OAI.ExactDerandomization.Rill.Oven.hoopK line 302
  68. def OAI.ExactDerandomization.Rill.Oven.per line 305
  69. def OAI.ExactDerandomization.Rill.Oven.throughout line 307
  70. def OAI.ExactDerandomization.Rill.Oven.coal line 308
  71. abbrev OAI.ExactDerandomization.Rill.Oven.start line 310
  72. def OAI.ExactDerandomization.Rill.Oven.cold line 311
  73. def OAI.ExactDerandomization.Rill.Oven.astir line 312
  74. abbrev OAI.ExactDerandomization.Rill.Oven.ext line 326
  75. abbrev OAI.ExactDerandomization.Rill.Oven.labels line 327
  76. def OAI.ExactDerandomization.Rill.Oven.rel line 328
  77. structure OAI.ExactDerandomization.Rill.Oven.Thaw line 329
  78. def OAI.ExactDerandomization.Rill.Oven.bank line 337
  79. def OAI.ExactDerandomization.Rill.Oven.sums line 339
  80. def OAI.ExactDerandomization.Rill.Oven.evenH line 341
  81. def OAI.ExactDerandomization.Rill.Oven.chart line 343
  82. def OAI.ExactDerandomization.Rill.Oven.chT line 348
  83. def OAI.ExactDerandomization.Rill.Oven.chF line 351
  84. def OAI.ExactDerandomization.Rill.Oven.perch line 353
  85. lemma OAI.ExactDerandomization.Rill.Oven.bank_step line 355
  86. lemma OAI.ExactDerandomization.Rill.Oven.ave line 358
  87. lemma OAI.ExactDerandomization.Rill.Oven.enrol line 362
  88. lemma OAI.ExactDerandomization.Rill.Oven.progress line 364
  89. lemma OAI.ExactDerandomization.Rill.Oven.sum_data line 367
  90. lemma OAI.ExactDerandomization.Rill.Oven.finished line 372
  91. lemma OAI.ExactDerandomization.Rill.Oven.Thaw.windy line 380
  92. lemma OAI.ExactDerandomization.Rill.Oven.Thaw.timed line 395
  93. lemma OAI.ExactDerandomization.Rill.Oven.Thaw.cutL line 406
  94. lemma OAI.ExactDerandomization.Rill.Oven.Thaw.seed_size line 427
  95. def OAI.ExactDerandomization.Rill.Oven.bill line 461
  96. abbrev OAI.ExactDerandomization.Rill.Oven.price line 462
  97. lemma OAI.ExactDerandomization.Rill.Oven.Thaw.age line 468
  98. lemma OAI.ExactDerandomization.Rill.Oven.Thaw.mounted line 470
  99. lemma OAI.ExactDerandomization.Rill.Oven.Thaw.admits line 484
  100. lemma OAI.ExactDerandomization.Rill.Oven.Thaw.postcardQ line 496
  101. lemma OAI.ExactDerandomization.Rill.Oven.Thaw.frameon line 498
  102. lemma OAI.ExactDerandomization.Rill.Oven.Thaw.frequent line 501
  103. lemma OAI.ExactDerandomization.Rill.Oven.Thaw.testH line 527
  104. lemma OAI.ExactDerandomization.Rill.Oven.Thaw.throughoutH line 532
  105. lemma OAI.ExactDerandomization.Rill.Oven.Thaw.followQ line 541
  106. lemma OAI.ExactDerandomization.Rill.Oven.Thaw.icy line 551
  107. lemma OAI.ExactDerandomization.Rill.Oven.Thaw.gloveQ line 556
  108. lemma OAI.ExactDerandomization.Rill.Oven.Thaw.finds line 564
  109. def OAI.ExactDerandomization.Rill.codeQ line 582
  110. def OAI.ExactDerandomization.Rill.diffd line 583
  111. lemma OAI.ExactDerandomization.Rill.rangeQ line 585
  112. lemma OAI.ExactDerandomization.Rill.resolve line 586
  113. lemma OAI.ExactDerandomization.Rill.codeK line 589
  114. lemma OAI.ExactDerandomization.Rill.sandK line 592
  115. def OAI.ExactDerandomization.Rill.earlier line 599
  116. lemma OAI.ExactDerandomization.Rill.earlyK line 601
  117. def OAI.ExactDerandomization.Rill.highZ line 605
  118. lemma OAI.ExactDerandomization.Rill.highK line 606
  119. abbrev OAI.ExactDerandomization.Rill.fromQ line 608
  120. lemma OAI.ExactDerandomization.Rill.fromK line 609
  121. def OAI.ExactDerandomization.Rill.aheadQ line 610
  122. lemma OAI.ExactDerandomization.Rill.prev0K line 611
  123. def OAI.ExactDerandomization.Rill.liftarm line 613
  124. def OAI.ExactDerandomization.Rill.Raised line 618
  125. def OAI.ExactDerandomization.Rill.powder line 620
  126. lemma OAI.ExactDerandomization.Rill.lifting line 621
  127. abbrev OAI.ExactDerandomization.Rill.Coin line 675
  128. def OAI.ExactDerandomization.Rill.Coin.v line 677
  129. def OAI.ExactDerandomization.Rill.Coin.ofZ line 678
  130. def OAI.ExactDerandomization.Rill.Coin.place line 679
  131. def OAI.ExactDerandomization.Rill.Coin.neg line 680
  132. def OAI.ExactDerandomization.Rill.Coin.join line 681
  133. def OAI.ExactDerandomization.Rill.Coin.mult line 683
  134. def OAI.ExactDerandomization.Rill.Coin.inv line 684
  135. def OAI.ExactDerandomization.Rill.Coin.low line 687
  136. def OAI.ExactDerandomization.Rill.Coin.minimum line 688
  137. def OAI.ExactDerandomization.Rill.Coin.maximum line 689
  138. theorem OAI.ExactDerandomization.Rill.Coin.place0 line 691
  139. lemma OAI.ExactDerandomization.Rill.Coin.ofv line 692
  140. lemma OAI.ExactDerandomization.Rill.Coin.neg0 line 693
  141. lemma OAI.ExactDerandomization.Rill.Coin.mul0 line 694
  142. lemma OAI.ExactDerandomization.Rill.Coin.add0 line 696
  143. lemma OAI.ExactDerandomization.Rill.Coin.inv0 line 698
  144. lemma OAI.ExactDerandomization.Rill.Coin.low_eq line 714
  145. lemma OAI.ExactDerandomization.Rill.Coin.min0 line 718
  146. lemma OAI.ExactDerandomization.Rill.Coin.max0 line 722
  147. def OAI.ExactDerandomization.Rill.Coin.floor0 line 725
  148. lemma OAI.ExactDerandomization.Rill.Coin.floorok line 726
  149. lemma OAI.ExactDerandomization.Rill.Coin.ofK line 737
  150. lemma OAI.ExactDerandomization.Rill.Coin.placeK line 738
  151. lemma OAI.ExactDerandomization.Rill.Coin.negK line 740
  152. lemma OAI.ExactDerandomization.Rill.Coin.addaK line 741
  153. lemma OAI.ExactDerandomization.Rill.Coin.multK line 744
  154. lemma OAI.ExactDerandomization.Rill.Coin.lowerK line 746
  155. lemma OAI.ExactDerandomization.Rill.Coin.minK line 748
  156. lemma OAI.ExactDerandomization.Rill.Coin.maxK line 749
  157. lemma OAI.ExactDerandomization.Rill.Coin.floorK line 750
  158. lemma OAI.ExactDerandomization.Rill.Coin.invK line 751
  159. structure OAI.ExactDerandomization.Rill.Meld line 766
  160. def OAI.ExactDerandomization.Rill.Meld.result line 773
  161. lemma OAI.ExactDerandomization.Rill.Meld.resultK line 780
  162. def OAI.ExactDerandomization.Rill.Meld.word line 789
  163. lemma OAI.ExactDerandomization.Rill.Meld.wordK line 790
  164. def OAI.ExactDerandomization.Rill.Meld.ran0 line 791
  165. def OAI.ExactDerandomization.Rill.Meld.cooked line 792
  166. def OAI.ExactDerandomization.Rill.Meld.tally line 795
  167. def OAI.ExactDerandomization.Rill.Meld.fp line 797
  168. abbrev OAI.ExactDerandomization.Rill.Meld.plug line 799
  169. abbrev OAI.ExactDerandomization.Rill.Meld.out line 801
  170. structure OAI.ExactDerandomization.Rill.Meld.Lip line 803
  171. lemma OAI.ExactDerandomization.Rill.Meld.profile line 812
  172. lemma OAI.ExactDerandomization.Rill.Meld.plugv line 827
  173. theorem OAI.ExactDerandomization.Rill.Meld.recipe line 839
  174. theorem OAI.ExactDerandomization.Rill.Meld.stream line 888
  175. abbrev OAI.ExactDerandomization.Rill.countgt line 910
  176. abbrev OAI.ExactDerandomization.Rill.countge line 911
  177. def OAI.ExactDerandomization.Rill.emin line 913
  178. lemma OAI.ExactDerandomization.Rill.existsN line 916
  179. def OAI.ExactDerandomization.Rill.rankN line 925
  180. lemma OAI.ExactDerandomization.Rill.rankN_v line 927
  181. lemma OAI.ExactDerandomization.Rill.aboveN line 930
  182. lemma OAI.ExactDerandomization.Rill.topN line 936
  183. lemma OAI.ExactDerandomization.Rill.earns line 943
  184. lemma OAI.ExactDerandomization.Rill.excels line 948
  185. lemma OAI.ExactDerandomization.Rill.scaled_rank line 962
  186. lemma OAI.ExactDerandomization.Rill.clipped_rank line 984
  187. lemma OAI.ExactDerandomization.Rill.sweepV line 1002
  188. abbrev OAI.ExactDerandomization.Rill.Exam line 1032
  189. abbrev OAI.ExactDerandomization.Rill.Hoard line 1033
  190. structure OAI.ExactDerandomization.Rill.Survey line 1034
  191. def OAI.ExactDerandomization.Rill.Survey.scrutiny line 1042
  192. lemma OAI.ExactDerandomization.Rill.Survey.scrK line 1044
  193. abbrev OAI.ExactDerandomization.Rill.Survey.Fuse line 1049
  194. def OAI.ExactDerandomization.Rill.Survey.startP line 1050
  195. lemma OAI.ExactDerandomization.Rill.Survey.originK line 1053
  196. def OAI.ExactDerandomization.Rill.Survey.light line 1058
  197. def OAI.ExactDerandomization.Rill.Survey.asses line 1059
  198. lemma OAI.ExactDerandomization.Rill.Survey.assesK line 1062
  199. def OAI.ExactDerandomization.Rill.Survey.fetchOne line 1064
  200. def OAI.ExactDerandomization.Rill.Survey.passQ line 1066
  201. lemma OAI.ExactDerandomization.Rill.Survey.passK line 1070
  202. def OAI.ExactDerandomization.Rill.Survey.held0 line 1074
  203. lemma OAI.ExactDerandomization.Rill.Survey.held0K line 1075
  204. def OAI.ExactDerandomization.Rill.Survey.chargeQ line 1077
  205. def OAI.ExactDerandomization.Rill.Survey.regain line 1080
  206. lemma OAI.ExactDerandomization.Rill.Survey.regainK line 1081
  207. def OAI.ExactDerandomization.Rill.Survey.moreB line 1088
  208. lemma OAI.ExactDerandomization.Rill.Survey.moreK line 1090
  209. def OAI.ExactDerandomization.Rill.Survey.totalize line 1096
  210. lemma OAI.ExactDerandomization.Rill.Survey.totalK line 1100
  211. def OAI.ExactDerandomization.Rill.Survey.per line 1108
  212. def OAI.ExactDerandomization.Rill.Survey.pane line 1109
  213. def OAI.ExactDerandomization.Rill.Survey.bulb line 1110
  214. abbrev OAI.ExactDerandomization.Rill.Survey.zeroQ line 1111
  215. def OAI.ExactDerandomization.Rill.Survey.rtest line 1112
  216. def OAI.ExactDerandomization.Rill.Survey.poll line 1114
  217. abbrev OAI.ExactDerandomization.Rill.Survey.topC line 1126
  218. abbrev OAI.ExactDerandomization.Rill.Survey.targetK line 1127
  219. def OAI.ExactDerandomization.Rill.Survey.oper line 1128
  220. def OAI.ExactDerandomization.Rill.Survey.nest line 1129
  221. def OAI.ExactDerandomization.Rill.Survey.priceB line 1130
  222. structure OAI.ExactDerandomization.Rill.Survey.Clue line 1131
  223. lemma OAI.ExactDerandomization.Rill.Survey.Clue.coal line 1140
  224. lemma OAI.ExactDerandomization.Rill.Survey.Clue.tight_exam line 1153
  225. lemma OAI.ExactDerandomization.Rill.Survey.Clue.bite line 1165
  226. lemma OAI.ExactDerandomization.Rill.Survey.Clue.license0 line 1180
  227. lemma OAI.ExactDerandomization.Rill.Survey.Clue.good0 line 1201
  228. def OAI.ExactDerandomization.Rill.Survey.residue line 1222
  229. def OAI.ExactDerandomization.Rill.Survey.sec line 1223
  230. lemma OAI.ExactDerandomization.Rill.Survey.swing line 1225
  231. lemma OAI.ExactDerandomization.Rill.Survey.volley line 1231
  232. lemma OAI.ExactDerandomization.Rill.Survey.sec0 line 1235
  233. lemma OAI.ExactDerandomization.Rill.Survey.secb line 1236
  234. abbrev OAI.ExactDerandomization.Rill.Survey.Clue.N line 1248
  235. lemma OAI.ExactDerandomization.Rill.Survey.Clue.rootP line 1250
  236. lemma OAI.ExactDerandomization.Rill.Survey.Clue.pollen line 1255
  237. lemma OAI.ExactDerandomization.Rill.Survey.Clue.checkplane line 1274
  238. lemma OAI.ExactDerandomization.Rill.Survey.Clue.field0 line 1278
  239. def OAI.ExactDerandomization.Rill.Survey.Clue.car line 1284
  240. lemma OAI.ExactDerandomization.Rill.Survey.Clue.carr line 1289
  241. lemma OAI.ExactDerandomization.Rill.Survey.Clue.intensity line 1292
  242. lemma OAI.ExactDerandomization.Rill.Survey.Clue.stream0 line 1316
  243. lemma OAI.ExactDerandomization.Rill.Survey.Clue.tasked line 1326