OAI/Computability/Logspace/ContourTraversal.lean

GitHub source file

167 declarations, 0 contain sorry, 0 declared as axioms

Contour traversal of finite functional graphs with explicit predecessor enumeration.

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

  1. abbrev OAI.ExactDerandomization.Swirl.Dot line 23
  2. abbrev OAI.ExactDerandomization.Swirl.Gem line 24
  3. structure OAI.ExactDerandomization.Swirl.Fir line 26
  4. def OAI.ExactDerandomization.Swirl.Fir.broad line 38
  5. def OAI.ExactDerandomization.Swirl.Fir.finalx line 39
  6. def OAI.ExactDerandomization.Swirl.Fir.roll line 40
  7. def OAI.ExactDerandomization.Swirl.Fir.fold line 50
  8. def OAI.ExactDerandomization.Swirl.Fir.live line 61
  9. lemma OAI.ExactDerandomization.Swirl.Fir.forward line 63
  10. inductive OAI.ExactDerandomization.Swirl.Fir.Flight line 80
  11. lemma OAI.ExactDerandomization.Swirl.Fir.Flight.on line 85
  12. lemma OAI.ExactDerandomization.Swirl.Fir.Flight.unique line 86
  13. lemma OAI.ExactDerandomization.Swirl.Fir.quota line 92
  14. def OAI.ExactDerandomization.Swirl.Fir.nest line 111
  15. lemma OAI.ExactDerandomization.Swirl.Fir.rise line 112
  16. def OAI.ExactDerandomization.Swirl.lap line 133
  17. lemma OAI.ExactDerandomization.Swirl.laps line 139
  18. def OAI.ExactDerandomization.Swirl.Link line 142
  19. lemma OAI.ExactDerandomization.Swirl.Link.seq line 143
  20. lemma OAI.ExactDerandomization.Swirl.same line 145
  21. lemma OAI.ExactDerandomization.Swirl.ride line 146
  22. lemma OAI.ExactDerandomization.Swirl.Fir.between line 152
  23. lemma OAI.ExactDerandomization.Swirl.Fir.orbit line 187
  24. lemma OAI.ExactDerandomization.Swirl.Fir.whirl line 199
  25. inductive OAI.ExactDerandomization.Swirl.Stripe line 217

    Source documentation

    Linear link with internal points explicit; endpoints can coincide.

    inductive Stripe (r:α→α→Prop) : α→List α→α→Prop
  | run {x y} (h:r x y) : Stripe r x [] y
  | hook {x y z l} : r x y → Stripe r y l z → Stripe r x (y::l) z

namespace Stripe
variable {r w : α→α→Prop}
  26. lemma OAI.ExactDerandomization.Swirl.Stripe.joins line 224
  27. lemma OAI.ExactDerandomization.Swirl.Stripe.both line 229
  28. lemma OAI.ExactDerandomization.Swirl.Stripe.every line 237
  29. lemma OAI.ExactDerandomization.Swirl.Stripe.sever line 242
  30. inductive OAI.ExactDerandomization.Swirl.Flare line 253
  31. lemma OAI.ExactDerandomization.Swirl.stripes line 257
  32. def OAI.ExactDerandomization.Swirl.Rope.rope line 274
  33. lemma OAI.ExactDerandomization.Swirl.Rope.before line 278
  34. lemma OAI.ExactDerandomization.Swirl.Rope.paid line 281
  35. lemma OAI.ExactDerandomization.Swirl.Rope.sat line 290
  36. lemma OAI.ExactDerandomization.Swirl.Rope.repeatZ line 303
  37. lemma OAI.ExactDerandomization.Swirl.Rope.clean line 316
  38. lemma OAI.ExactDerandomization.Swirl.Rope.cutpoint line 329
  39. def OAI.ExactDerandomization.Swirl.Fir.march line 361
  40. lemma OAI.ExactDerandomization.Swirl.Fir.streak line 362
  41. def OAI.ExactDerandomization.Swirl.Fir.riseQ line 396
  42. def OAI.ExactDerandomization.Swirl.Fir.probe line 400
  43. abbrev OAI.ExactDerandomization.Swirl.Seat line 403
  44. abbrev OAI.ExactDerandomization.Swirl.Panel line 404
  45. structure OAI.ExactDerandomization.Swirl.Arena line 406
  46. abbrev OAI.ExactDerandomization.Swirl.Arena.acts line 417
  47. abbrev OAI.ExactDerandomization.Swirl.Arena.wait line 418
  48. abbrev OAI.ExactDerandomization.Swirl.Arena.tag line 419
  49. def OAI.ExactDerandomization.Swirl.Arena.touch line 421
  50. structure OAI.ExactDerandomization.Swirl.Shows line 428
  51. abbrev OAI.ExactDerandomization.Swirl.Shows.Chart line 435
  52. def OAI.ExactDerandomization.Swirl.Shows.ray line 437
  53. lemma OAI.ExactDerandomization.Swirl.Shows.rayK line 438
  54. def OAI.ExactDerandomization.Swirl.Shows.keep line 440
  55. lemma OAI.ExactDerandomization.Swirl.Shows.keepK line 442
  56. def OAI.ExactDerandomization.Swirl.Shows.upmov line 444
  57. lemma OAI.ExactDerandomization.Swirl.Shows.upK line 448
  58. def OAI.ExactDerandomization.Swirl.Shows.summit line 458
  59. lemma OAI.ExactDerandomization.Swirl.Shows.summitK line 461
  60. def OAI.ExactDerandomization.Swirl.Shows.topseat line 467
  61. lemma OAI.ExactDerandomization.Swirl.Shows.topK line 468
  62. def OAI.ExactDerandomization.Swirl.Shows.tryU line 470
  63. def OAI.ExactDerandomization.Swirl.Shows.chase line 471
  64. def OAI.ExactDerandomization.Swirl.Shows.rise line 472
  65. def OAI.ExactDerandomization.Swirl.Shows.downgrade line 474
  66. lemma OAI.ExactDerandomization.Swirl.Shows.downgrades line 475
  67. def OAI.ExactDerandomization.Swirl.Shows.dock line 477
  68. lemma OAI.ExactDerandomization.Swirl.Shows.dockK line 481
  69. def OAI.ExactDerandomization.Swirl.Shows.highp line 490
  70. lemma OAI.ExactDerandomization.Swirl.Shows.highK line 491
  71. def OAI.ExactDerandomization.Swirl.Shows.seeD line 492
  72. def OAI.ExactDerandomization.Swirl.Shows.step line 494
  73. def OAI.ExactDerandomization.Swirl.Shows.repeatQ line 498
  74. lemma OAI.ExactDerandomization.Swirl.Shows.repeatK line 499
  75. def OAI.ExactDerandomization.Swirl.Shows.spool line 500
  76. def OAI.ExactDerandomization.Swirl.Shows.away line 501
  77. def OAI.ExactDerandomization.Swirl.Shows.check line 502
  78. structure OAI.ExactDerandomization.Swirl.Shows.Covers line 504
  79. def OAI.ExactDerandomization.Swirl.Shows.promote line 522
  80. def OAI.ExactDerandomization.Swirl.Shows.counted line 524
  81. def OAI.ExactDerandomization.Swirl.Shows.rer line 529
  82. lemma OAI.ExactDerandomization.Swirl.Shows.Covers.stayst line 537
  83. lemma OAI.ExactDerandomization.Swirl.Shows.Covers.truekeep line 540
  84. lemma OAI.ExactDerandomization.Swirl.Shows.Covers.falsekeep line 543
  85. lemma OAI.ExactDerandomization.Swirl.Shows.Covers.stopkeep line 547
  86. lemma OAI.ExactDerandomization.Swirl.Shows.Covers.powered line 550
  87. lemma OAI.ExactDerandomization.Swirl.Shows.Covers.sought line 558
  88. lemma OAI.ExactDerandomization.Swirl.Shows.Covers.wished line 605
  89. def OAI.ExactDerandomization.Swirl.Shows.Covers.chosen line 621
  90. lemma OAI.ExactDerandomization.Swirl.Shows.Covers.child line 625
  91. lemma OAI.ExactDerandomization.Swirl.Shows.Covers.forwardx line 644
  92. lemma OAI.ExactDerandomization.Swirl.Shows.Covers.previousx line 657
  93. lemma OAI.ExactDerandomization.Swirl.Shows.Covers.turnx line 673
  94. lemma OAI.ExactDerandomization.Swirl.Shows.Covers.restNeon line 680
  95. lemma OAI.ExactDerandomization.Swirl.Shows.Covers.flash line 682
  96. lemma OAI.ExactDerandomization.Swirl.Stripe.twain line 707
  97. structure OAI.ExactDerandomization.Swirl.Rake line 715
  98. abbrev OAI.ExactDerandomization.Swirl.Rake.forth line 720
  99. abbrev OAI.ExactDerandomization.Swirl.Rake.back line 721
  100. abbrev OAI.ExactDerandomization.Swirl.Rake.root line 722
  101. abbrev OAI.ExactDerandomization.Swirl.Rake.pass line 723
  102. structure OAI.ExactDerandomization.Swirl.Rake.Circuit line 727
  103. lemma OAI.ExactDerandomization.Swirl.Rake.cable line 732
  104. def OAI.ExactDerandomization.Swirl.Rake.seek line 746
  105. inductive OAI.ExactDerandomization.Swirl.Rake.Alley line 749
  106. lemma OAI.ExactDerandomization.Swirl.Rake.Alley.ofStripe line 754
  107. lemma OAI.ExactDerandomization.Swirl.Rake.sounded line 760
  108. def OAI.ExactDerandomization.Swirl.Rake.gather line 773
  109. lemma OAI.ExactDerandomization.Swirl.Rake.attained line 776
  110. def OAI.ExactDerandomization.Swirl.Rake.ply line 798
  111. lemma OAI.ExactDerandomization.Swirl.Rake.follow line 801
  112. def OAI.ExactDerandomization.Swirl.Rake.surf line 809
  113. lemma OAI.ExactDerandomization.Swirl.Rake.climbed line 813
  114. def OAI.ExactDerandomization.Swirl.Rake.dune line 839
  115. lemma OAI.ExactDerandomization.Swirl.Rake.chose line 842
  116. structure OAI.ExactDerandomization.Swirl.Twig line 866
  117. def OAI.ExactDerandomization.Swirl.Twig.sole line 878
  118. lemma OAI.ExactDerandomization.Swirl.Twig.solely line 881
  119. def OAI.ExactDerandomization.Swirl.Twig.upward line 888
  120. def OAI.ExactDerandomization.Swirl.Twig.fromp line 889
  121. lemma OAI.ExactDerandomization.Swirl.Twig.atU line 891
  122. lemma OAI.ExactDerandomization.Swirl.Twig.atD line 892
  123. def OAI.ExactDerandomization.Swirl.Twig.tree line 895
  124. lemma OAI.ExactDerandomization.Swirl.Twig.probeU line 904
  125. lemma OAI.ExactDerandomization.Swirl.Twig.probeD line 921
  126. structure OAI.ExactDerandomization.Swirl.Bud line 929

    Source documentation

    The finite path-kernel: after q name val = next_raw_name + 1, zero for no edge. Modes 0 = static, 1 = opaque stationary, any other = mobile. Every operation-dependent guard is generated in LF before calling a lower query.

    structure Bud where
…
  127. structure OAI.ExactDerandomization.Swirl.Clay line 941

    Source documentation

    Root kernel proof data. hand maps addresses to the shared register carrying that address and a catalyst, not to local pc states. Different hand embeddings of the same addresses during different invocations are allowed.

    structure Clay where
…
  128. abbrev OAI.ExactDerandomization.Swirl.Bud.pk line 956
  129. abbrev OAI.ExactDerandomization.Swirl.Bud.ready line 957
  130. abbrev OAI.ExactDerandomization.Swirl.Bud.entry line 959
  131. abbrev OAI.ExactDerandomization.Swirl.Bud.nextx line 960
  132. abbrev OAI.ExactDerandomization.Swirl.Bud.code line 961
  133. abbrev OAI.ExactDerandomization.Swirl.Bud.range0 line 962
  134. def OAI.ExactDerandomization.Swirl.Bud.earth line 964
  135. lemma OAI.ExactDerandomization.Swirl.Bud.walled line 965
  136. def OAI.ExactDerandomization.Swirl.Bud.Hill line 967
  137. abbrev OAI.ExactDerandomization.Swirl.Bud.poke line 975

    Source documentation

    Canonical toss calls for stationary/moving candidates

    abbrev poke (b:Bool) (i j:ℕ) := p.stem b |>.f s.l.x (pk s i j)

    Mentions: OAI.ExactDerandomization.Swirl.Bud.pk

  138. def OAI.ExactDerandomization.Swirl.Bud.motorout line 976
  139. def OAI.ExactDerandomization.Swirl.Bud.bed line 981
  140. structure OAI.ExactDerandomization.Swirl.Bud.Wall line 983
  141. def OAI.ExactDerandomization.Swirl.Bud.Wall.twig line 1003
  142. def OAI.ExactDerandomization.Swirl.Bud.arena line 1038
  143. def OAI.ExactDerandomization.Swirl.Bud.invert line 1053
  144. lemma OAI.ExactDerandomization.Swirl.Bud.invert2 line 1054
  145. def OAI.ExactDerandomization.Swirl.Bud.lit line 1056
  146. lemma OAI.ExactDerandomization.Swirl.Bud.Wall.alive line 1069
  147. lemma OAI.ExactDerandomization.Swirl.Bud.Wall.hover line 1089
  148. lemma OAI.ExactDerandomization.Swirl.Bud.Wall.auth line 1109
  149. lemma OAI.ExactDerandomization.Swirl.Bud.Wall.again line 1132
  150. lemma OAI.ExactDerandomization.Swirl.Bud.Wall.dusk line 1138
  151. def OAI.ExactDerandomization.Swirl.Bud.putter line 1162
  152. lemma OAI.ExactDerandomization.Swirl.Bud.putK line 1164
  153. def OAI.ExactDerandomization.Swirl.Bud.gate line 1168
  154. def OAI.ExactDerandomization.Swirl.Bud.chk line 1169
  155. lemma OAI.ExactDerandomization.Swirl.Bud.chkK line 1172
  156. def OAI.ExactDerandomization.Swirl.Bud.printx line 1174
  157. lemma OAI.ExactDerandomization.Swirl.Bud.printK line 1180
  158. def OAI.ExactDerandomization.Swirl.Bud.pureq line 1185
  159. lemma OAI.ExactDerandomization.Swirl.Bud.pureK line 1186
  160. def OAI.ExactDerandomization.Swirl.Bud.script line 1188
  161. lemma OAI.ExactDerandomization.Swirl.Bud.scriptK line 1189
  162. def OAI.ExactDerandomization.Swirl.Bud.heedx line 1192
  163. lemma OAI.ExactDerandomization.Swirl.Bud.heedK line 1194
  164. def OAI.ExactDerandomization.Swirl.Bud.tackle line 1197
  165. def OAI.ExactDerandomization.Swirl.Bud.showall line 1204
  166. lemma OAI.ExactDerandomization.Swirl.Bud.Wall.handle line 1210
  167. theorem OAI.ExactDerandomization.Swirl.Bud.Wall.yields line 1307