OAI/Computability/Logspace/EstimatorInterfaces.lean

GitHub source file

209 declarations, 0 contain sorry, 0 declared as axioms

Typed estimator requests, traversal interfaces, and terminal configurations.

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

  1. structure OAI.ExactDerandomization.Chime.Scheme line 21

    Source documentation

    Each statistical unit offers several opaque services.

    structure Scheme where
…
  2. def OAI.ExactDerandomization.Chime.Scheme.hole line 31
  3. def OAI.ExactDerandomization.Chime.Scheme.bell line 32
  4. def OAI.ExactDerandomization.Chime.Scheme.token line 33
  5. def OAI.ExactDerandomization.Chime.Scheme.cell line 34
  6. def OAI.ExactDerandomization.Chime.Scheme.inside line 35
  7. def OAI.ExactDerandomization.Chime.Scheme.unitK line 36
  8. def OAI.ExactDerandomization.Chime.Scheme.which line 37
  9. def OAI.ExactDerandomization.Chime.Scheme.date line 38
  10. lemma OAI.ExactDerandomization.Chime.Scheme.tokenK line 39
  11. lemma OAI.ExactDerandomization.Chime.Scheme.cellK line 40
  12. lemma OAI.ExactDerandomization.Chime.Scheme.unitK0 line 41
  13. lemma OAI.ExactDerandomization.Chime.Scheme.markB line 43
  14. lemma OAI.ExactDerandomization.Chime.Scheme.bellU line 44
  15. lemma OAI.ExactDerandomization.Chime.Scheme.bellT line 45
  16. lemma OAI.ExactDerandomization.Chime.Scheme.bellV line 46
  17. def OAI.ExactDerandomization.Chime.Scheme.ofclock line 48
  18. def OAI.ExactDerandomization.Chime.Scheme.ofword line 49
  19. def OAI.ExactDerandomization.Chime.Scheme.based line 50
  20. def OAI.ExactDerandomization.Chime.Scheme.before line 51
  21. lemma OAI.ExactDerandomization.Chime.Scheme.beforeK line 52
  22. def OAI.ExactDerandomization.Chime.Scheme.vent line 55
  23. lemma OAI.ExactDerandomization.Chime.Scheme.born line 59
  24. structure OAI.ExactDerandomization.Chime.Dome line 65
  25. abbrev OAI.ExactDerandomization.Chime.Dome.s line 73
  26. abbrev OAI.ExactDerandomization.Chime.Dome.F line 74
  27. abbrev OAI.ExactDerandomization.Chime.Dome.x line 75
  28. abbrev OAI.ExactDerandomization.Chime.Dome.r line 76
  29. abbrev OAI.ExactDerandomization.Chime.Dome.P line 77
  30. abbrev OAI.ExactDerandomization.Chime.Dome.active line 78
  31. abbrev OAI.ExactDerandomization.Chime.Dome.W line 79
  32. abbrev OAI.ExactDerandomization.Chime.Dome.D line 80
  33. abbrev OAI.ExactDerandomization.Chime.Dome.loadC line 81
  34. abbrev OAI.ExactDerandomization.Chime.Dome.won line 82
  35. abbrev OAI.ExactDerandomization.Chime.Dome.high line 83
  36. lemma OAI.ExactDerandomization.Chime.Dome.till line 85
  37. lemma OAI.ExactDerandomization.Chime.Dome.hiwon line 86
  38. lemma OAI.ExactDerandomization.Chime.Dome.future line 87
  39. abbrev OAI.ExactDerandomization.Chime.Dome.glove line 90
  40. abbrev OAI.ExactDerandomization.Chime.Dome.clearG line 91
  41. lemma OAI.ExactDerandomization.Chime.Dome.cleared line 92
  42. abbrev OAI.ExactDerandomization.Chime.Dome.audible line 97
  43. abbrev OAI.ExactDerandomization.Chime.Dome.dual line 98
  44. structure OAI.ExactDerandomization.Chime.Dome.Shape line 101

    Source documentation

    analytic clocks and polynomial choices are separated from the running program.

    structure Shape : Prop where
…
  45. lemma OAI.ExactDerandomization.Chime.Dome.Shape.bookB line 109
  46. lemma OAI.ExactDerandomization.Chime.Dome.Shape.migrate line 111
  47. abbrev OAI.ExactDerandomization.Chime.Dome.talk line 122
  48. lemma OAI.ExactDerandomization.Chime.Dome.aon line 124
  49. def OAI.ExactDerandomization.Chime.Dome.cand line 126
  50. lemma OAI.ExactDerandomization.Chime.Dome.grab line 129
  51. def OAI.ExactDerandomization.Chime.Dome.echo line 134
  52. def OAI.ExactDerandomization.Chime.Dome.swears line 135
  53. lemma OAI.ExactDerandomization.Chime.Dome.identity line 136
  54. abbrev OAI.ExactDerandomization.Chime.Dome.pulseQ line 150
  55. lemma OAI.ExactDerandomization.Chime.Dome.pulseB line 151
  56. lemma OAI.ExactDerandomization.Chime.Dome.day line 152
  57. abbrev OAI.ExactDerandomization.Chime.Dome.Tide line 156
  58. def OAI.ExactDerandomization.Chime.Dome.pour line 157
  59. def OAI.ExactDerandomization.Chime.Dome.curve line 162
  60. lemma OAI.ExactDerandomization.Chime.Dome.uniquely line 165
  61. def OAI.ExactDerandomization.Chime.Dome.AtM line 169
  62. structure OAI.ExactDerandomization.Chime.Dome.Streams line 174
  63. lemma OAI.ExactDerandomization.Chime.Dome.Streams.throve line 183
  64. lemma OAI.ExactDerandomization.Chime.Dome.Streams.lines line 187
  65. lemma OAI.ExactDerandomization.Chime.Dome.Streams.canonicalS line 201
  66. def OAI.ExactDerandomization.Chime.Dome.fuel line 209
  67. structure OAI.ExactDerandomization.Chime.Dome.Ears0 line 212
  68. def OAI.ExactDerandomization.Chime.Dome.Heard line 217

    Source documentation

    Artificial terminal configurations get only replies already covered by the W induction.

    def Heard (u:ℕ): Prop:= ∀ v:ℕ,p.active v→p.W v<p.W u→p.won v 0→p.Ears0 v
  69. lemma OAI.ExactDerandomization.Chime.Dome.ascent line 218
  70. lemma OAI.ExactDerandomization.Chime.Dome.fires line 226
  71. def OAI.ExactDerandomization.Chime.Dome.chord line 259
  72. abbrev OAI.ExactDerandomization.Chime.Dome.orch line 263
  73. structure OAI.ExactDerandomization.Chime.Dome.Suite line 264
  74. structure OAI.ExactDerandomization.Chime.Dome.Sings line 270
  75. structure OAI.ExactDerandomization.Chime.Dome.StageW line 274
  76. abbrev OAI.ExactDerandomization.Chime.Dome.Voice line 277
  77. lemma OAI.ExactDerandomization.Chime.Dome.Suite.pit line 282
  78. lemma OAI.ExactDerandomization.Chime.Dome.Suite.hired line 286

    Source documentation

    Issue after inserting a command in the main program.

    lemma hired (f:ℕ)(t:ℕ)(hl:bell u f t ≤ p.F.limit){i b c}
    (he:1  ≤  c)(hh:c ≤ p.slope)
    (hg:Lot.Mane p.l c ⟨p.W u,t⟩ (p.D u) (bell u f t) p.l.P (0,i) b):
    p.talk (bell u f t) i b:= by
…
  79. lemma OAI.ExactDerandomization.Chime.Dome.Suite.concert line 293
  80. lemma OAI.ExactDerandomization.Chime.Dome.Suite.dance line 299
  81. lemma OAI.ExactDerandomization.Chime.Dome.Suite.descend line 306
  82. lemma OAI.ExactDerandomization.Chime.Dome.Suite.pull_shot line 313
  83. def OAI.ExactDerandomization.Chime.Dome.Bullet.lookup line 323
  84. lemma OAI.ExactDerandomization.Chime.Dome.Bullet.lookupK line 326
  85. def OAI.ExactDerandomization.Chime.Dome.Bullet.snap line 329
  86. lemma OAI.ExactDerandomization.Chime.Dome.Bullet.past line 330
  87. lemma OAI.ExactDerandomization.Chime.Dome.Bullet.copy line 347
  88. abbrev OAI.ExactDerandomization.Chime.Dome.Bullet.roomS line 355
  89. lemma OAI.ExactDerandomization.Chime.Dome.Bullet.clef line 356
  90. structure OAI.ExactDerandomization.Chime.Cone line 384

    Source documentation

    Shared interface of the instructions at a pointer. alpha is the unit ultimately offering the visit (test tag offered by another unit). Knot is a pure capped append on designated paths.

    structure Cone where
…
  91. structure OAI.ExactDerandomization.Chime.Road line 396
  92. def OAI.ExactDerandomization.Chime.Cone.bow line 405
  93. structure OAI.ExactDerandomization.Chime.Cone.ConeX line 407
  94. abbrev OAI.ExactDerandomization.Chime.Cone.ConeX.ear line 413
  95. abbrev OAI.ExactDerandomization.Chime.Cone.ConeX.stem line 414
  96. abbrev OAI.ExactDerandomization.Chime.Cone.ConeX.h0 line 415
  97. abbrev OAI.ExactDerandomization.Chime.Cone.ConeX.f0 line 416
  98. abbrev OAI.ExactDerandomization.Chime.Cone.ConeX.s1 line 417
  99. abbrev OAI.ExactDerandomization.Chime.Cone.ConeX.i1 line 418
  100. abbrev OAI.ExactDerandomization.Chime.Cone.ConeX.b1 line 419
  101. abbrev OAI.ExactDerandomization.Chime.Cone.ConeX.ip line 420
  102. abbrev OAI.ExactDerandomization.Chime.Cone.ConeX.n line 421
  103. def OAI.ExactDerandomization.Chime.Cone.ConeX.GoodX line 422
  104. abbrev OAI.ExactDerandomization.Chime.Cone.ConeX.less line 423
  105. abbrev OAI.ExactDerandomization.Chime.Cone.ConeX.wideQ line 424
  106. structure OAI.ExactDerandomization.Chime.Cone.ConeX.BaseX line 426
  107. def OAI.ExactDerandomization.Chime.Cone.ConeX.Allow line 435
  108. structure OAI.ExactDerandomization.Chime.Cone.ConeX.Point line 437
  109. inductive OAI.ExactDerandomization.Chime.Cone.ConeX.Pond line 453
  110. def OAI.ExactDerandomization.Chime.Cone.ConeX.dry line 459
  111. inductive OAI.ExactDerandomization.Chime.Cone.ConeX.Flora line 460
  112. def OAI.ExactDerandomization.Chime.Cone.ConeX.pen line 464
  113. abbrev OAI.ExactDerandomization.Chime.Cone.ConeX.ambient line 465
  114. lemma OAI.ExactDerandomization.Chime.Cone.ConeX.little line 467
  115. lemma OAI.ExactDerandomization.Chime.Cone.ConeX.award line 487
  116. lemma OAI.ExactDerandomization.Chime.Cone.ConeX.orderly line 492
  117. lemma OAI.ExactDerandomization.Chime.Cone.ConeX.targeted line 498
  118. lemma OAI.ExactDerandomization.Chime.Cone.ConeX.archway line 507
  119. lemma OAI.ExactDerandomization.Chime.Cone.ConeX.coronet line 513
  120. abbrev OAI.ExactDerandomization.Chime.Arch line 534
  121. abbrev OAI.ExactDerandomization.Chime.NoteM line 535
  122. abbrev OAI.ExactDerandomization.Chime.Face line 536
  123. abbrev OAI.ExactDerandomization.Chime.Pr line 537
  124. def OAI.ExactDerandomization.Chime.ray0 line 538
  125. def OAI.ExactDerandomization.Chime.concatJ line 539
  126. lemma OAI.ExactDerandomization.Chime.sofJ line 540
  127. structure OAI.ExactDerandomization.Chime.Harp line 554
  128. abbrev OAI.ExactDerandomization.Chime.Harp.quoteQ line 562
  129. def OAI.ExactDerandomization.Chime.Harp.keys line 563
  130. lemma OAI.ExactDerandomization.Chime.Harp.keysK line 564
  131. def OAI.ExactDerandomization.Chime.Harp.rim0 line 565
  132. lemma OAI.ExactDerandomization.Chime.Harp.rimK line 566
  133. def OAI.ExactDerandomization.Chime.Harp.fillQ line 567
  134. lemma OAI.ExactDerandomization.Chime.Harp.fillK line 568
  135. def OAI.ExactDerandomization.Chime.Harp.roads line 569
  136. lemma OAI.ExactDerandomization.Chime.Harp.roadsK line 570
  137. def OAI.ExactDerandomization.Chime.Harp.hopX line 571
  138. lemma OAI.ExactDerandomization.Chime.Harp.hopK line 572
  139. lemma OAI.ExactDerandomization.Chime.Harp.rayK line 575
  140. lemma OAI.ExactDerandomization.Chime.Harp.concatK line 577
  141. def OAI.ExactDerandomization.Chime.Harp.port line 579
  142. lemma OAI.ExactDerandomization.Chime.Harp.portK line 580
  143. def OAI.ExactDerandomization.Chime.Harp.thru line 581
  144. def OAI.ExactDerandomization.Chime.Harp.mapJ line 582
  145. lemma OAI.ExactDerandomization.Chime.Harp.mapK line 583
  146. def OAI.ExactDerandomization.Chime.Harp.pen0 line 586
  147. lemma OAI.ExactDerandomization.Chime.Harp.penK line 587
  148. def OAI.ExactDerandomization.Chime.Harp.lit line 591
  149. def OAI.ExactDerandomization.Chime.Harp.handle line 592
  150. lemma OAI.ExactDerandomization.Chime.Harp.handleK line 597
  151. def OAI.ExactDerandomization.Chime.Harp.cueV line 603
  152. lemma OAI.ExactDerandomization.Chime.Harp.keyp line 606
  153. lemma OAI.ExactDerandomization.Chime.Harp.path0 line 607
  154. lemma OAI.ExactDerandomization.Chime.Harp.again line 608
  155. structure OAI.ExactDerandomization.Chime.Harp.Wick line 623
  156. abbrev OAI.ExactDerandomization.Chime.Harp.Wick.d line 628
  157. def OAI.ExactDerandomization.Chime.Harp.Wick.Ok line 629
  158. def OAI.ExactDerandomization.Chime.Harp.Wick.state line 630
  159. def OAI.ExactDerandomization.Chime.Harp.Wick.Veil line 636
  160. abbrev OAI.ExactDerandomization.Chime.Harp.Wick.den0 line 638
  161. structure OAI.ExactDerandomization.Chime.Harp.Wick.Life line 640
  162. lemma OAI.ExactDerandomization.Chime.Harp.Wick.Life.den_good line 651
  163. lemma OAI.ExactDerandomization.Chime.Harp.Wick.Life.lower0 line 655
  164. lemma OAI.ExactDerandomization.Chime.Harp.Wick.Life.announce line 658
  165. lemma OAI.ExactDerandomization.Chime.Harp.Wick.Life.emerges line 674
  166. theorem OAI.ExactDerandomization.Chime.Harp.Wick.Life.offers line 737
  167. lemma OAI.ExactDerandomization.Chime.Harp.Wick.Life.veiled line 767
  168. structure OAI.ExactDerandomization.Chime.Ember line 797
  169. abbrev OAI.ExactDerandomization.Chime.Ember.D line 810
  170. abbrev OAI.ExactDerandomization.Chime.Ember.Q line 811
  171. abbrev OAI.ExactDerandomization.Chime.Ember.q line 812
  172. abbrev OAI.ExactDerandomization.Chime.Ember.fav line 813
  173. structure OAI.ExactDerandomization.Chime.Ember.Trust line 816

    Source documentation

    Input ring geometry.

    structure Trust : Prop where
…
  174. structure OAI.ExactDerandomization.Chime.Ember.Bridge line 828
  175. lemma OAI.ExactDerandomization.Chime.Ember.Bridge.lit line 839
  176. lemma OAI.ExactDerandomization.Chime.Ember.Bridge.grove line 856
  177. structure OAI.ExactDerandomization.Chime.Ember.Quilt line 877
  178. def OAI.ExactDerandomization.Chime.Ember.pie line 882
  179. lemma OAI.ExactDerandomization.Chime.Ember.Quilt.lotc line 886
  180. theorem OAI.ExactDerandomization.Chime.Ember.Quilt.quilted line 905
  181. abbrev OAI.ExactDerandomization.Chime.Ember.stepC line 919
  182. structure OAI.ExactDerandomization.Chime.Ember.Mouth line 921
  183. abbrev OAI.ExactDerandomization.Chime.Ember.cutWay line 923
  184. def OAI.ExactDerandomization.Chime.Ember.pathOp line 927
  185. def OAI.ExactDerandomization.Chime.Ember.valueOf line 930
  186. lemma OAI.ExactDerandomization.Chime.Ember.Mouth.disp line 935
  187. lemma OAI.ExactDerandomization.Chime.Ember.Mouth.sole line 950
  188. lemma OAI.ExactDerandomization.Chime.Ember.Mouth.pointIn line 955
  189. lemma OAI.ExactDerandomization.Chime.Ember.Mouth.exchange0 line 965
  190. lemma OAI.ExactDerandomization.Chime.Ember.Mouth.unique0 line 966
  191. theorem OAI.ExactDerandomization.Chime.Ember.Mouth.clearsWay line 971
  192. structure OAI.ExactDerandomization.Chime.Ember.Forest line 1006
  193. abbrev OAI.ExactDerandomization.Chime.Ember.Forest.q line 1015
  194. structure OAI.ExactDerandomization.Chime.Ember.Forest.Archive line 1016
  195. abbrev OAI.ExactDerandomization.Chime.Ember.Forest.S line 1029
  196. def OAI.ExactDerandomization.Chime.Ember.Forest.teaN line 1031
  197. abbrev OAI.ExactDerandomization.Chime.Ember.Forest.V0 line 1032
  198. abbrev OAI.ExactDerandomization.Chime.Ember.Forest.scoreRank line 1033
  199. abbrev OAI.ExactDerandomization.Chime.Ember.Forest.scoreTape line 1034
  200. lemma OAI.ExactDerandomization.Chime.Ember.Forest.Archive.stage0 line 1039
  201. lemma OAI.ExactDerandomization.Chime.Ember.Forest.Archive.gears line 1052
  202. lemma OAI.ExactDerandomization.Chime.Ember.Forest.Archive.unsealed line 1078
  203. lemma OAI.ExactDerandomization.Chime.Ember.Forest.Archive.estimated line 1086
  204. lemma OAI.ExactDerandomization.Chime.Ember.Forest.Archive.counted line 1100
  205. abbrev OAI.ExactDerandomization.Chime.Ember.Forest.Bcost line 1130
  206. abbrev OAI.ExactDerandomization.Chime.Ember.Forest.trackG line 1131
  207. abbrev OAI.ExactDerandomization.Chime.Ember.Forest.engine line 1133
  208. lemma OAI.ExactDerandomization.Chime.Ember.Forest.Archive.digit line 1138
  209. lemma OAI.ExactDerandomization.Chime.Ember.Forest.Archive.fullplan line 1163