OAI/Computability/Logspace/FiniteFieldPrograms.lean

GitHub source file

179 declarations, 0 contain sorry, 0 declared as axioms

Uniform prime-field enumeration and finite arithmetic for deterministic probability decisions.

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

  1. def OAI.ExactDerandomization.Grain.Prime.tube line 24
  2. lemma OAI.ExactDerandomization.Grain.Prime.tube_hi line 26
  3. lemma OAI.ExactDerandomization.Grain.Prime.unique_small line 31
  4. lemma OAI.ExactDerandomization.Grain.Prime.uniquely line 45
  5. lemma OAI.ExactDerandomization.Grain.Prime.tubeK line 56
  6. def OAI.ExactDerandomization.Grain.Prime.test line 62
  7. def OAI.ExactDerandomization.Grain.Prime.primex line 65
  8. lemma OAI.ExactDerandomization.Grain.Prime.divK line 68
  9. lemma OAI.ExactDerandomization.Grain.Prime.pxK line 69
  10. lemma OAI.ExactDerandomization.Grain.Prime.px_eq line 72
  11. def OAI.ExactDerandomization.Grain.Prime.atp line 96
  12. def OAI.ExactDerandomization.Grain.Prime.last line 98
  13. lemma OAI.ExactDerandomization.Grain.Prime.last_prime line 99
  14. lemma OAI.ExactDerandomization.Grain.Prime.lastK line 112
  15. structure OAI.ExactDerandomization.Grain.Rock line 124
  16. def OAI.ExactDerandomization.Grain.Rock.B line 131
  17. def OAI.ExactDerandomization.Grain.Rock.lamp line 132
  18. def OAI.ExactDerandomization.Grain.Rock.n line 133
  19. instance OAI.ExactDerandomization.Grain.Rock.primed line 134
  20. lemma OAI.ExactDerandomization.Grain.Rock.nf line 136
  21. def OAI.ExactDerandomization.Grain.Rock.matter0 line 139
  22. lemma OAI.ExactDerandomization.Grain.Rock.prompts line 140
  23. lemma OAI.ExactDerandomization.Grain.Rock.sizeE line 146
  24. lemma OAI.ExactDerandomization.Grain.Rock.codeE line 148
  25. lemma OAI.ExactDerandomization.Grain.Rock.BKn line 155
  26. lemma OAI.ExactDerandomization.Grain.Rock.codeKn line 156
  27. abbrev OAI.ExactDerandomization.Grain.Rock.linE line 158
  28. lemma OAI.ExactDerandomization.Grain.Rock.exprKn line 159
  29. lemma OAI.ExactDerandomization.Grain.Rock.affine line 162
  30. lemma OAI.ExactDerandomization.Grain.Rock.lampK line 167
  31. lemma OAI.ExactDerandomization.Grain.Rock.nKn line 171
  32. abbrev OAI.ExactDerandomization.Grain.Page line 184
  33. abbrev OAI.ExactDerandomization.Grain.Stamp line 185
  34. abbrev OAI.ExactDerandomization.Grain.Issue line 186
  35. def OAI.ExactDerandomization.Grain.Print.ncard line 193
  36. def OAI.ExactDerandomization.Grain.Print.den line 194
  37. def OAI.ExactDerandomization.Grain.Print.badge line 195
  38. def OAI.ExactDerandomization.Grain.Print.issued line 196
  39. lemma OAI.ExactDerandomization.Grain.Print.nr line 197
  40. lemma OAI.ExactDerandomization.Grain.Print.xi line 198
  41. instance OAI.ExactDerandomization.Grain.Print.(instance at line 203) line 203
  42. lemma OAI.ExactDerandomization.Grain.Print.xu line 204
  43. def OAI.ExactDerandomization.Grain.Print.barr line 209
  44. def OAI.ExactDerandomization.Grain.Print.brief line 210
  45. def OAI.ExactDerandomization.Grain.Print.on line 211
  46. def OAI.ExactDerandomization.Grain.Print.revealed line 212
  47. instance OAI.ExactDerandomization.Grain.Print.(instance at line 213) line 213
  48. instance OAI.ExactDerandomization.Grain.Print.(instance at line 214) line 214
  49. instance OAI.ExactDerandomization.Grain.Print.(instance at line 215) line 215
  50. lemma OAI.ExactDerandomization.Grain.Print.nsmall line 216
  51. lemma OAI.ExactDerandomization.Grain.Print.rn line 218
  52. lemma OAI.ExactDerandomization.Grain.Print.valid line 221
  53. lemma OAI.ExactDerandomization.Grain.Print.built line 227
  54. lemma OAI.ExactDerandomization.Grain.Print.constit line 232
  55. lemma OAI.ExactDerandomization.Grain.Print.fill line 233
  56. def OAI.ExactDerandomization.Grain.Print.wallP line 240
  57. def OAI.ExactDerandomization.Grain.Print.ink line 241
  58. def OAI.ExactDerandomization.Grain.Print.pages line 242
  59. lemma OAI.ExactDerandomization.Grain.Print.boxbound line 243
  60. def OAI.ExactDerandomization.Grain.Print.publish line 250
  61. def OAI.ExactDerandomization.Grain.Print.spine line 251
  62. lemma OAI.ExactDerandomization.Grain.Print.entry line 252
  63. lemma OAI.ExactDerandomization.Grain.Print.owner line 255
  64. lemma OAI.ExactDerandomization.Grain.Print.columns line 260
  65. lemma OAI.ExactDerandomization.Grain.Print.both line 271
  66. lemma OAI.ExactDerandomization.Grain.Print.bytesK line 274
  67. lemma OAI.ExactDerandomization.Grain.Print.onK line 282
  68. lemma OAI.ExactDerandomization.Grain.Print.pagesK line 294
  69. lemma OAI.ExactDerandomization.Grain.Print.pubK line 298
  70. def OAI.ExactDerandomization.Grain.Print.ms line 320
  71. def OAI.ExactDerandomization.Grain.Print.zi line 321
  72. def OAI.ExactDerandomization.Grain.Print.mix line 322
  73. lemma OAI.ExactDerandomization.Grain.Print.valms line 325
  74. lemma OAI.ExactDerandomization.Grain.Print.nadd line 328
  75. def OAI.ExactDerandomization.Grain.Print.shoot line 331
  76. lemma OAI.ExactDerandomization.Grain.Print.shoots line 332
  77. def OAI.ExactDerandomization.Grain.Print.stretch line 336
  78. lemma OAI.ExactDerandomization.Grain.Print.stretchy line 337
  79. lemma OAI.ExactDerandomization.Grain.Print.asideK line 350
  80. lemma OAI.ExactDerandomization.Grain.Print.msK line 357
  81. lemma OAI.ExactDerandomization.Grain.Print.ziK line 359
  82. lemma OAI.ExactDerandomization.Grain.Print.mixK line 362
  83. lemma OAI.ExactDerandomization.Grain.Print.shootK line 365
  84. lemma OAI.ExactDerandomization.Grain.Print.stretchK line 367
  85. def OAI.ExactDerandomization.Grain.Rock.camp line 385
  86. lemma OAI.ExactDerandomization.Grain.Rock.camps line 386
  87. lemma OAI.ExactDerandomization.Grain.Rock.campK line 395
  88. def OAI.ExactDerandomization.Grain.Rock.qualify line 405
  89. abbrev OAI.ExactDerandomization.Grain.Rock.printid line 408
  90. lemma OAI.ExactDerandomization.Grain.Rock.verified line 409
  91. lemma OAI.ExactDerandomization.Grain.Rock.qualifyK line 420
  92. lemma OAI.ExactDerandomization.Grain.Rock.numbers line 423
  93. def OAI.ExactDerandomization.Grain.Rock.sumtop line 446
  94. lemma OAI.ExactDerandomization.Grain.Rock.totalK line 448
  95. def OAI.ExactDerandomization.Grain.Rock.census line 466
  96. lemma OAI.ExactDerandomization.Grain.Rock.witness0 line 467
  97. lemma OAI.ExactDerandomization.Grain.Rock.positive0 line 469
  98. def OAI.ExactDerandomization.Grain.Rock.survey line 476
  99. lemma OAI.ExactDerandomization.Grain.Rock.countok line 477
  100. def OAI.ExactDerandomization.Grain.Rock.answer line 487
  101. lemma OAI.ExactDerandomization.Grain.Rock.zenK line 489
  102. lemma OAI.ExactDerandomization.Grain.Rock.censusK line 493
  103. lemma OAI.ExactDerandomization.Grain.Rock.tallyK line 495
  104. lemma OAI.ExactDerandomization.Grain.Rock.annK line 497
  105. lemma OAI.ExactDerandomization.Grain.Rock.scale_cnv line 500
  106. lemma OAI.ExactDerandomization.Grain.Rock.certificate line 506
  107. theorem OAI.ExactDerandomization.Grain.Rock.convince line 519
  108. abbrev OAI.ExactDerandomization.Grain.Print.Z4 line 559
  109. def OAI.ExactDerandomization.Grain.Print.zd line 561
  110. def OAI.ExactDerandomization.Grain.Print.red line 562
  111. def OAI.ExactDerandomization.Grain.Print.change0 line 564
  112. def OAI.ExactDerandomization.Grain.Print.change1 line 565
  113. def OAI.ExactDerandomization.Grain.Print.bare line 567
  114. def OAI.ExactDerandomization.Grain.Print.walkstep line 568
  115. def OAI.ExactDerandomization.Grain.Print.reducep line 571
  116. def OAI.ExactDerandomization.Grain.Print.fetch line 572
  117. lemma OAI.ExactDerandomization.Grain.Print.readout line 577
  118. lemma OAI.ExactDerandomization.Grain.Print.redCast line 578
  119. lemma OAI.ExactDerandomization.Grain.Print.reducePol_any line 583
  120. lemma OAI.ExactDerandomization.Grain.Print.prints_any line 596
  121. lemma OAI.ExactDerandomization.Grain.Print.recast line 598
  122. lemma OAI.ExactDerandomization.Grain.Print.zoom line 602
  123. lemma OAI.ExactDerandomization.Grain.Print.fetching line 609
  124. lemma OAI.ExactDerandomization.Grain.Print.quads line 619
  125. lemma OAI.ExactDerandomization.Grain.Print.zdK line 625
  126. lemma OAI.ExactDerandomization.Grain.Print.holeK line 627
  127. lemma OAI.ExactDerandomization.Grain.Print.redK line 634
  128. lemma OAI.ExactDerandomization.Grain.Print.plow line 637
  129. lemma OAI.ExactDerandomization.Grain.Print.polK line 659
  130. lemma OAI.ExactDerandomization.Grain.Print.plusK line 664
  131. lemma OAI.ExactDerandomization.Grain.Print.addK line 668
  132. lemma OAI.ExactDerandomization.Grain.Print.bareK line 672
  133. lemma OAI.ExactDerandomization.Grain.Print.zoomK line 675
  134. lemma OAI.ExactDerandomization.Grain.Print.downK line 680
  135. lemma OAI.ExactDerandomization.Grain.Print.dropK line 681
  136. lemma OAI.ExactDerandomization.Grain.Print.pickK line 686
  137. lemma OAI.ExactDerandomization.Grain.Print.fetchK0 line 692
  138. lemma OAI.ExactDerandomization.Grain.Print.fetchK line 700
  139. abbrev OAI.ExactDerandomization.Grain.Print.Token line 727
  140. def OAI.ExactDerandomization.Grain.Print.checkS line 729
  141. def OAI.ExactDerandomization.Grain.Print.checkD line 735
  142. def OAI.ExactDerandomization.Grain.Print.arch line 740
  143. abbrev OAI.ExactDerandomization.Grain.Print.Bundle line 747
  144. def OAI.ExactDerandomization.Grain.Print.tossR line 748
  145. lemma OAI.ExactDerandomization.Grain.Print.rose line 754
  146. lemma OAI.ExactDerandomization.Grain.Print.landlord line 759
  147. lemma OAI.ExactDerandomization.Grain.Print.S_K line 765
  148. lemma OAI.ExactDerandomization.Grain.Print.D_K line 770
  149. lemma OAI.ExactDerandomization.Grain.Print.A_K line 775
  150. lemma OAI.ExactDerandomization.Grain.Print.tossed line 788
  151. abbrev OAI.ExactDerandomization.Grain.Print.rad line 793
  152. lemma OAI.ExactDerandomization.Grain.Print.rad_pos line 794
  153. def OAI.ExactDerandomization.Grain.Print.number line 795
  154. def OAI.ExactDerandomization.Grain.Print.mark line 796
  155. lemma OAI.ExactDerandomization.Grain.Print.mintK line 798
  156. def OAI.ExactDerandomization.Grain.Print.queue line 827
  157. lemma OAI.ExactDerandomization.Grain.Print.width line 834
  158. lemma OAI.ExactDerandomization.Grain.Print.emblem line 844
  159. lemma OAI.ExactDerandomization.Grain.Print.touring line 851
  160. abbrev OAI.ExactDerandomization.Grain.Print.Guide line 883
  161. abbrev OAI.ExactDerandomization.Grain.Print.MapState line 884
  162. def OAI.ExactDerandomization.Grain.Print.goon line 886
  163. lemma OAI.ExactDerandomization.Grain.Print.goonK line 890
  164. abbrev OAI.ExactDerandomization.Grain.Print.Lap line 898
  165. def OAI.ExactDerandomization.Grain.Print.capz line 899
  166. lemma OAI.ExactDerandomization.Grain.Print.capzK line 901
  167. def OAI.ExactDerandomization.Grain.Print.spin line 906
  168. lemma OAI.ExactDerandomization.Grain.Print.spinK line 911
  169. lemma OAI.ExactDerandomization.Grain.Print.limits line 922
  170. def OAI.ExactDerandomization.Grain.Print.scoreQ line 926
  171. lemma OAI.ExactDerandomization.Grain.Print.wellQ line 933
  172. theorem OAI.ExactDerandomization.Grain.Print.flowed line 950
  173. def OAI.ExactDerandomization.Grain.Print.stepout line 986
  174. def OAI.ExactDerandomization.Grain.Print.touched line 987
  175. lemma OAI.ExactDerandomization.Grain.Print.spin_null line 990
  176. lemma OAI.ExactDerandomization.Grain.Print.stepK line 992
  177. lemma OAI.ExactDerandomization.Grain.Print.touchedK line 997
  178. lemma OAI.ExactDerandomization.Grain.Print.unpacked line 1003
  179. lemma OAI.ExactDerandomization.Grain.Print.exactHit line 1007