OAI/Computability/Logspace/EstimatorMachine.lean

GitHub source file

205 declarations, 0 contain sorry, 0 declared as axioms

The finite estimator program and its instruction-level resource contracts.

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

  1. structure OAI.ExactDerandomization.SiteX.Line line 22
  2. abbrev OAI.ExactDerandomization.SiteX.Line.prog line 30
  3. abbrev OAI.ExactDerandomization.SiteX.Line.D line 31
  4. abbrev OAI.ExactDerandomization.SiteX.Line.eye line 32
  5. abbrev OAI.ExactDerandomization.SiteX.Line.torch line 33
  6. abbrev OAI.ExactDerandomization.SiteX.Line.wick0 line 34
  7. abbrev OAI.ExactDerandomization.SiteX.Line.n line 35
  8. abbrev OAI.ExactDerandomization.SiteX.Line.w0 line 36
  9. abbrev OAI.ExactDerandomization.SiteX.Line.B line 37
  10. abbrev OAI.ExactDerandomization.SiteX.Line.m line 38
  11. abbrev OAI.ExactDerandomization.SiteX.Line.plotM line 39
  12. abbrev OAI.ExactDerandomization.SiteX.Line.limitM line 40
  13. lemma OAI.ExactDerandomization.SiteX.Line.poss line 42
  14. def OAI.ExactDerandomization.SiteX.Line.clr line 44
  15. def OAI.ExactDerandomization.SiteX.Line.rowL line 46
  16. def OAI.ExactDerandomization.SiteX.Line.vecL line 47
  17. structure OAI.ExactDerandomization.SiteX.Line.Chart line 49
  18. lemma OAI.ExactDerandomization.SiteX.Line.Chart.sc line 56
  19. lemma OAI.ExactDerandomization.SiteX.Line.Chart.above6 line 57
  20. lemma OAI.ExactDerandomization.SiteX.Line.Chart.draft line 58
  21. lemma OAI.ExactDerandomization.SiteX.Line.Chart.rent line 60
  22. lemma OAI.ExactDerandomization.SiteX.Line.Chart.e0 line 61
  23. lemma OAI.ExactDerandomization.SiteX.Line.Chart.auth line 63
  24. lemma OAI.ExactDerandomization.SiteX.Line.Chart.cred line 65
  25. lemma OAI.ExactDerandomization.SiteX.Line.Chart.courseR line 70
  26. lemma OAI.ExactDerandomization.SiteX.Line.Chart.courseV line 79
  27. lemma OAI.ExactDerandomization.SiteX.Line.Chart.parse line 88
  28. lemma OAI.ExactDerandomization.SiteX.Line.Chart.walls line 105
  29. lemma OAI.ExactDerandomization.SiteX.Line.Chart.assigned line 114
  30. lemma OAI.ExactDerandomization.SiteX.Line.Chart.chamber line 118
  31. def OAI.ExactDerandomization.SiteX.Line.smallQ line 160
  32. lemma OAI.ExactDerandomization.SiteX.Line.Launch line 161
  33. lemma OAI.ExactDerandomization.SiteX.Line.Voices line 163
  34. lemma OAI.ExactDerandomization.SiteX.Line.spokenC line 169
  35. structure OAI.ExactDerandomization.SiteX.Line.CageQ line 179

    Source comment

    reusable request-origin signature. all indices in the allotted range, incl holes.
    structure CageQ where
…
  36. structure OAI.ExactDerandomization.SiteX.Line.CageQ.Front line 186
  37. lemma OAI.ExactDerandomization.SiteX.Line.CageQ.Front.awake line 200
  38. lemma OAI.ExactDerandomization.SiteX.Line.CageQ.Front.back0 line 203
  39. lemma OAI.ExactDerandomization.SiteX.Line.CageQ.Front.point0 line 207
  40. structure OAI.ExactDerandomization.SiteX.Line.CageQ.Trace line 218
  41. structure OAI.ExactDerandomization.SiteX.Line.CageQ.Offer line 225
  42. lemma OAI.ExactDerandomization.SiteX.Line.CageQ.Trace.distinct_path line 229
  43. lemma OAI.ExactDerandomization.SiteX.Line.CageQ.Trace.caseM line 231
  44. lemma OAI.ExactDerandomization.SiteX.Line.CageQ.Trace.places line 235
  45. abbrev OAI.ExactDerandomization.SiteX.Line.atom0 line 243

    Source documentation

    Cocoon. Universal micromoves on alpha 0.

    abbrev atom0 := Was.atom 0
…
  46. lemma OAI.ExactDerandomization.SiteX.Line.Chart.bootsBasic line 247
  47. lemma OAI.ExactDerandomization.SiteX.Line.Chart.voteRoot line 256
  48. lemma OAI.ExactDerandomization.SiteX.Line.Chart.basic0 line 260
  49. lemma OAI.ExactDerandomization.SiteX.Line.Chart.holdX line 268
  50. lemma OAI.ExactDerandomization.SiteX.Line.Chart.Rope line 271
  51. structure OAI.ExactDerandomization.SiteX.MintV line 331

    Source comment

    Scalar prices determined before unfolding predecessor calls.
    structure MintV where
…
  52. def OAI.ExactDerandomization.SiteX.MintV.prism line 337
  53. abbrev OAI.ExactDerandomization.SiteX.MintV.tokenH line 338
  54. abbrev OAI.ExactDerandomization.SiteX.MintV.inputH line 339
  55. def OAI.ExactDerandomization.SiteX.MintV.rangeN line 340
  56. abbrev OAI.ExactDerandomization.SiteX.MintV.roofX line 341
  57. def OAI.ExactDerandomization.SiteX.MintV.shellQ line 343
  58. lemma OAI.ExactDerandomization.SiteX.MintV.shore line 344
  59. lemma OAI.ExactDerandomization.SiteX.MintV.shorn line 345
  60. def OAI.ExactDerandomization.SiteX.MintV.fine line 349
  61. lemma OAI.ExactDerandomization.SiteX.MintV.fluc line 350
  62. lemma OAI.ExactDerandomization.SiteX.MintV.decor line 355
  63. lemma OAI.ExactDerandomization.SiteX.Line.rolff line 372
  64. lemma OAI.ExactDerandomization.SiteX.Line.rolfe line 374
  65. structure OAI.ExactDerandomization.SiteX.Line.Fabric line 376
  66. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.roll line 383
  67. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.frame line 384
  68. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.c line 385
  69. def OAI.ExactDerandomization.SiteX.Line.Fabric.activeR line 386
  70. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.world line 387
  71. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.S0 line 388
  72. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.S1 line 389
  73. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.S2 line 390
  74. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.marathon line 391
  75. lemma OAI.ExactDerandomization.SiteX.Line.Fabric.leg line 392
  76. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.tagged line 393
  77. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.govern line 394
  78. def OAI.ExactDerandomization.SiteX.Line.Fabric.Good line 395
  79. lemma OAI.ExactDerandomization.SiteX.Line.Fabric.workR line 397
  80. lemma OAI.ExactDerandomization.SiteX.Line.Fabric.Good.booked line 402
  81. lemma OAI.ExactDerandomization.SiteX.Line.Fabric.Good.encs line 404
  82. lemma OAI.ExactDerandomization.SiteX.Line.Fabric.Good.n0 line 405
  83. lemma OAI.ExactDerandomization.SiteX.Line.Fabric.Good.n1 line 406
  84. structure OAI.ExactDerandomization.SiteX.Line.Fabric.HistoryC line 409
  85. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.HistoryC.R line 413
  86. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.HistoryC.actual line 414
  87. structure OAI.ExactDerandomization.SiteX.Line.Fabric.HistoryC.Compared line 415
  88. lemma OAI.ExactDerandomization.SiteX.Line.Fabric.HistoryC.Compared.set line 419
  89. structure OAI.ExactDerandomization.SiteX.Line.Producer line 460
  90. abbrev OAI.ExactDerandomization.SiteX.Line.Producer.awake line 465
  91. def OAI.ExactDerandomization.SiteX.Line.Producer.coversF line 466
  92. def OAI.ExactDerandomization.SiteX.Line.Producer.scoreF line 467
  93. structure OAI.ExactDerandomization.SiteX.Line.Producer.Light line 468
  94. structure OAI.ExactDerandomization.SiteX.Line.Producer.Quote line 472
  95. structure OAI.ExactDerandomization.SiteX.Line.Producer.Certified line 477
  96. lemma OAI.ExactDerandomization.SiteX.Line.Producer.Quote.orbit line 484
  97. lemma OAI.ExactDerandomization.SiteX.Line.Producer.Quote.lacks line 490
  98. lemma OAI.ExactDerandomization.SiteX.Line.Producer.Certified.supply line 495
  99. lemma OAI.ExactDerandomization.SiteX.Line.Producer.Certified.pixels line 510
  100. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.α line 523
  101. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.Rslots line 524
  102. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.Snum line 525
  103. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.β line 526
  104. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.terminal line 527
  105. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.leaveE line 528
  106. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.final0 line 529
  107. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.finalE line 530
  108. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.grid line 531
  109. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.trio line 532
  110. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.grains line 533
  111. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.aimE line 534
  112. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.heated line 535
  113. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.Tscale line 536
  114. def OAI.ExactDerandomization.SiteX.Line.Fabric.slotWord line 538
  115. structure OAI.ExactDerandomization.SiteX.Line.Fabric.Yolk line 540
  116. structure OAI.ExactDerandomization.SiteX.Line.Fabric.YFine line 543
  117. structure OAI.ExactDerandomization.SiteX.Line.Fabric.Hinge line 556
  118. structure OAI.ExactDerandomization.SiteX.Line.Fabric.HFine line 559
  119. structure OAI.ExactDerandomization.SiteX.Line.Fabric.Tgood line 570
  120. structure OAI.ExactDerandomization.SiteX.Line.Fabric.Profession line 575

    Source documentation

    mating on the pre-cap main ports. Captures baseline order by specifying only its needed invariants.

    structure Profession (f:Producer)(tb:ℕ→ℕ→ℕ) :Prop where
…

    Mentions: OAI.ExactDerandomization.SiteX.Line.Producer

  121. structure OAI.ExactDerandomization.SiteX.Line.Fabric.Efine line 586

    Source documentation

    Final matrix port operations, including paired information for echoes.

    structure Efine (p:MintV)(f:Producer):Prop where
…

    Mentions: OAI.ExactDerandomization.SiteX.MintV, OAI.ExactDerandomization.SiteX.Line.Producer

  122. abbrev OAI.ExactDerandomization.SiteX.Label.gob line 610
  123. lemma OAI.ExactDerandomization.SiteX.Label.gobK line 611
  124. abbrev OAI.ExactDerandomization.SiteX.Label.PURE line 614
  125. def OAI.ExactDerandomization.SiteX.Label.put line 617
  126. lemma OAI.ExactDerandomization.SiteX.Label.putK line 618
  127. def OAI.ExactDerandomization.SiteX.Label.followP line 622
  128. lemma OAI.ExactDerandomization.SiteX.Label.followK line 624
  129. def OAI.ExactDerandomization.SiteX.Label.roadX line 628
  130. lemma OAI.ExactDerandomization.SiteX.Line.Fabric.pointerot line 639
  131. lemma OAI.ExactDerandomization.SiteX.Line.Fabric.awayT line 641
  132. def OAI.ExactDerandomization.SiteX.Line.Fabric.diva line 644
  133. lemma OAI.ExactDerandomization.SiteX.Line.Fabric.weightEnd line 647
  134. lemma OAI.ExactDerandomization.SiteX.Line.Fabric.ageEnd line 651
  135. lemma OAI.ExactDerandomization.SiteX.Line.Fabric.parentL line 654
  136. structure OAI.ExactDerandomization.SiteX.Line.Fabric.Mantle line 659
  137. lemma OAI.ExactDerandomization.SiteX.Line.Fabric.Mantle.ties line 671
  138. lemma OAI.ExactDerandomization.SiteX.Line.Fabric.Mantle.bridge line 679
  139. def OAI.ExactDerandomization.SiteX.Studio.stacc line 716

    Source documentation

    allocate main's body by operation tags.

    def stacc (q:ℕ)(u:ℕ):ℕ:=enc ((q,u,0):Reed.Stool)

    Mentions: OAI.ExactDerandomization.Reed.Stool

  140. def OAI.ExactDerandomization.SiteX.Studio.collapse line 717
  141. lemma OAI.ExactDerandomization.SiteX.Studio.lidK line 718
  142. lemma OAI.ExactDerandomization.SiteX.Studio.oK line 719
  143. lemma OAI.ExactDerandomization.SiteX.Studio.collapseK line 720
  144. def OAI.ExactDerandomization.SiteX.Studio.erode line 722
  145. def OAI.ExactDerandomization.SiteX.Studio.enter line 723
  146. def OAI.ExactDerandomization.SiteX.Studio.arrange line 724
  147. lemma OAI.ExactDerandomization.SiteX.Studio.arr line 728
  148. abbrev OAI.ExactDerandomization.SiteX.Studio.dockA line 742
  149. abbrev OAI.ExactDerandomization.SiteX.Studio.stk line 743
  150. lemma OAI.ExactDerandomization.SiteX.Studio.stalk line 744
  151. def OAI.ExactDerandomization.SiteX.Studio.Parcel line 746

    Source documentation

    direct untransformed data-station program assigned at one valid card.

    def Parcel (u:Line (q:=q) (w:=w) (h:=h))(a:ℕ)(p:Cog):Prop:=
…

    Mentions: OAI.ExactDerandomization.SiteX.Line

  152. lemma OAI.ExactDerandomization.SiteX.Studio.stationed line 749
  153. lemma OAI.ExactDerandomization.SiteX.Studio.echoTicket line 759
  154. lemma OAI.ExactDerandomization.SiteX.Studio.scoreTicket line 769
  155. lemma OAI.ExactDerandomization.SiteX.Studio.positioned line 781
  156. lemma OAI.ExactDerandomization.SiteX.Studio.vital line 787
  157. lemma OAI.ExactDerandomization.SiteX.Studio.stayedC line 791
  158. lemma OAI.ExactDerandomization.SiteX.Studio.soonerC line 796
  159. def OAI.ExactDerandomization.SiteX.Label.substitute line 816

    Source comment

    cap invocation program uses a common graph virtual q.
    def substitute (_:Word)(q:ℕ):ℕ:=post (unitK q) Label.PURE 0 (date q)

    Mentions: OAI.ExactDerandomization.Word, OAI.ExactDerandomization.SiteX.Label.PURE

  160. lemma OAI.ExactDerandomization.SiteX.Label.substituteK line 817
  161. def OAI.ExactDerandomization.SiteX.Label.renbody line 818
  162. lemma OAI.ExactDerandomization.SiteX.Label.reprise line 819
  163. abbrev OAI.ExactDerandomization.SiteX.Label.Ticket line 822
  164. def OAI.ExactDerandomization.SiteX.Label.match0 line 823
  165. lemma OAI.ExactDerandomization.SiteX.Label.match0K line 827
  166. def OAI.ExactDerandomization.SiteX.Label.outwardP line 835
  167. lemma OAI.ExactDerandomization.SiteX.Label.outwardK line 836
  168. abbrev OAI.ExactDerandomization.SiteX.Label.placeholder line 840
  169. def OAI.ExactDerandomization.SiteX.Label.motionR line 842
  170. def OAI.ExactDerandomization.SiteX.Label.fold0 line 846
  171. abbrev OAI.ExactDerandomization.SiteX.Label.neighbors line 849
  172. abbrev OAI.ExactDerandomization.SiteX.Label.fullB line 850
  173. lemma OAI.ExactDerandomization.SiteX.Label.came line 851
  174. lemma OAI.ExactDerandomization.SiteX.Label.pickout line 853
  175. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.alongE line 888
  176. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.core12 line 889
  177. lemma OAI.ExactDerandomization.SiteX.Line.Fabric.cap_dual line 891
  178. lemma OAI.ExactDerandomization.SiteX.Line.Fabric.adding line 901
  179. structure OAI.ExactDerandomization.SiteX.Line.Fabric.Bloom12 line 905
  180. lemma OAI.ExactDerandomization.SiteX.Line.Fabric.Bloom12.funded line 912
  181. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.Bloom12.flood line 948
  182. lemma OAI.ExactDerandomization.SiteX.Line.Fabric.Bloom12.swell line 950
  183. structure OAI.ExactDerandomization.SiteX.Line.Fabric.Stand line 1002

    Source comment

    B rank roles station.
    structure Stand where
…
  184. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.Stand.cage line 1010
  185. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.Stand.beacon line 1011
  186. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.Stand.H line 1012
  187. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.Stand.bank line 1015
  188. structure OAI.ExactDerandomization.SiteX.Line.Fabric.Stand.Law line 1018
  189. lemma OAI.ExactDerandomization.SiteX.Line.Fabric.Stand.Law.promoted line 1032
  190. lemma OAI.ExactDerandomization.SiteX.Line.Fabric.Stand.Law.identityN line 1080
  191. theorem OAI.ExactDerandomization.SiteX.Line.Fabric.Bloom12.charm line 1167
  192. def OAI.ExactDerandomization.SiteX.Line.Fabric.startsP line 1232
  193. lemma OAI.ExactDerandomization.SiteX.Line.Fabric.startsK line 1235
  194. def OAI.ExactDerandomization.SiteX.Line.Fabric.quiet line 1238
  195. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.capprog line 1240
  196. lemma OAI.ExactDerandomization.SiteX.Line.Fabric.vocal line 1242
  197. lemma OAI.ExactDerandomization.SiteX.Line.Fabric.rankName line 1246
  198. theorem OAI.ExactDerandomization.SiteX.Line.Fabric.tribunal line 1250
  199. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.EmptyT line 1267
  200. lemma OAI.ExactDerandomization.SiteX.Line.Fabric.desert12 line 1268
  201. def OAI.ExactDerandomization.SiteX.Line.Fabric.Stand.score0 line 1313
  202. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.Stand.tollD line 1318
  203. theorem OAI.ExactDerandomization.SiteX.Line.Fabric.Stand.Law.ardent line 1324
  204. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.Stand.TDef line 1366
  205. abbrev OAI.ExactDerandomization.SiteX.Line.Fabric.Stand.IDef line 1367