OAI/Computability/Logspace/UniformEstimator.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous correctness of one uniform estimator program on all inputs.

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

  1. def OAI.ExactDerandomization.Umbra.Codex.atlas line 30
  2. abbrev OAI.ExactDerandomization.Umbra.Codex.mdi line 31
  3. abbrev OAI.ExactDerandomization.Umbra.Codex.boxI0 line 33
  4. abbrev OAI.ExactDerandomization.Umbra.Codex.boxI1 line 34
  5. abbrev OAI.ExactDerandomization.Umbra.Codex.boxT line 35
  6. abbrev OAI.ExactDerandomization.Umbra.Codex.boxE line 36
  7. abbrev OAI.ExactDerandomization.Umbra.Codex.capT line 37
  8. abbrev OAI.ExactDerandomization.Umbra.Codex.rankT1 line 38
  9. abbrev OAI.ExactDerandomization.Umbra.Codex.rankE1 line 39
  10. abbrev OAI.ExactDerandomization.Umbra.Codex.VI line 40
  11. abbrev OAI.ExactDerandomization.Umbra.Codex.VF line 41
  12. def OAI.ExactDerandomization.Umbra.Codex.produce line 43
  13. abbrev OAI.ExactDerandomization.Umbra.Codex.pages line 55
  14. abbrev OAI.ExactDerandomization.Umbra.Codex.hcap line 57
  15. abbrev OAI.ExactDerandomization.Umbra.Codex.compass line 58
  16. abbrev OAI.ExactDerandomization.Umbra.Codex.coins3 line 59
  17. abbrev OAI.ExactDerandomization.Umbra.Codex.debit3 line 60
  18. structure OAI.ExactDerandomization.Umbra.Codex.Paying line 62
  19. def OAI.ExactDerandomization.Umbra.Codex.sump line 73
  20. lemma OAI.ExactDerandomization.Umbra.Codex.liable line 77
  21. structure OAI.ExactDerandomization.Umbra.Codex.Fortune line 81
  22. lemma OAI.ExactDerandomization.Umbra.Codex.enacted line 90
  23. structure OAI.ExactDerandomization.Umbra.TrustQ line 108
  24. lemma OAI.ExactDerandomization.Umbra.TrustQ.owns line 115
  25. lemma OAI.ExactDerandomization.Umbra.TrustQ.ownsV line 116
  26. lemma OAI.ExactDerandomization.Umbra.TrustQ.grants line 117
  27. lemma OAI.ExactDerandomization.Umbra.TrustQ.scripted line 122
  28. lemma OAI.ExactDerandomization.Umbra.TrustQ.stock line 123
  29. lemma OAI.ExactDerandomization.Umbra.TrustQ.capdraw line 124
  30. lemma OAI.ExactDerandomization.Umbra.TrustQ.pearls line 126
  31. lemma OAI.ExactDerandomization.Umbra.TrustQ.pearlR line 135
  32. lemma OAI.ExactDerandomization.Umbra.TrustQ.pearlV line 138
  33. lemma OAI.ExactDerandomization.Umbra.TrustQ.insures line 142
  34. abbrev OAI.ExactDerandomization.Umbra.Elect.Birth line 168
  35. abbrev OAI.ExactDerandomization.Umbra.Elect.Mark line 170
  36. abbrev OAI.ExactDerandomization.Umbra.Elect.CeilingR line 172
  37. structure OAI.ExactDerandomization.Umbra.Elect.Covenant line 176

    Source documentation

    Specific contract per version, Good row assumed.Pulse.EI at any m scoreboard. If inactive potential, no TC or T services. End serves zeros.

    structure Covenant (u:Line (q:=q) (w:=w) (h:=h))(p:MintV)(a:ℕ):Prop where
…
  38. structure OAI.ExactDerandomization.Umbra.Elect.FullV line 187
  39. def OAI.ExactDerandomization.Umbra.Elect.Promised line 191
  40. lemma OAI.ExactDerandomization.Umbra.Elect.glacial line 194
  41. lemma OAI.ExactDerandomization.Umbra.Elect.ruddy line 199
  42. lemma OAI.ExactDerandomization.Umbra.Elect.haze line 201
  43. lemma OAI.ExactDerandomization.Umbra.Elect.Covenant.mute line 208
  44. lemma OAI.ExactDerandomization.Umbra.Elect.Covenant.fandom line 212
  45. lemma OAI.ExactDerandomization.Umbra.Elect.Covenant.orchard line 263
  46. lemma OAI.ExactDerandomization.Umbra.Elect.Promised.seeking line 276
  47. lemma OAI.ExactDerandomization.Umbra.Elect.Promised.sooner line 277
  48. lemma OAI.ExactDerandomization.Umbra.TrustQ.stara line 303
  49. lemma OAI.ExactDerandomization.Umbra.TrustQ.starb line 335
  50. lemma OAI.ExactDerandomization.Umbra.TrustQ.stard line 352
  51. lemma OAI.ExactDerandomization.Umbra.TrustQ.promiseE line 393
  52. lemma OAI.ExactDerandomization.Umbra.TrustQ.earlierT line 396
  53. lemma OAI.ExactDerandomization.Umbra.TrustQ.crownC line 401
  54. lemma OAI.ExactDerandomization.Umbra.TrustQ.deputed line 404
  55. lemma OAI.ExactDerandomization.Umbra.TrustQ.starR line 411
  56. lemma OAI.ExactDerandomization.Umbra.TrustQ.staE line 417
  57. abbrev OAI.ExactDerandomization.Umbra.TrustQ.pr line 427
  58. lemma OAI.ExactDerandomization.Umbra.TrustQ.upK line 428
  59. lemma OAI.ExactDerandomization.Umbra.TrustQ.sovereign line 434
  60. lemma OAI.ExactDerandomization.Umbra.TrustQ.hstep line 447
  61. lemma OAI.ExactDerandomization.Umbra.TrustQ.umbrella line 455
  62. lemma OAI.ExactDerandomization.Umbra.TrustQ.terrarium line 480
  63. abbrev OAI.ExactDerandomization.Umbra.TrustQ.bread line 519
  64. lemma OAI.ExactDerandomization.Umbra.TrustQ.sunken line 520
  65. lemma OAI.ExactDerandomization.Umbra.TrustQ.relicV line 532
  66. lemma OAI.ExactDerandomization.Umbra.TrustQ.treasuryV line 554
  67. lemma OAI.ExactDerandomization.Umbra.TrustQ.auraV line 568
  68. lemma OAI.ExactDerandomization.Umbra.TrustQ.earned line 581
  69. theorem OAI.ExactDerandomization.Umbra.TrustQ.coverage line 593

    Source documentation

    full version closure.

    theorem coverage (u0:ℕ) (hx:u.D.active u0):
    FullV u p u0:=by
…
  70. abbrev OAI.ExactDerandomization.Umbra.Scope.selfS line 625
  71. abbrev OAI.ExactDerandomization.Umbra.Scope.Dscope line 626
  72. abbrev OAI.ExactDerandomization.Umbra.Scope.prog0 line 627
  73. def OAI.ExactDerandomization.Umbra.Scope.cosmos line 628
  74. abbrev OAI.ExactDerandomization.Umbra.Scope.request line 630
  75. abbrev OAI.ExactDerandomization.Umbra.Scope.U line 631
  76. abbrev OAI.ExactDerandomization.Umbra.Scope.shield line 632
  77. def OAI.ExactDerandomization.Umbra.Scope.study line 633
  78. def OAI.ExactDerandomization.Umbra.Scope.chop0 line 634
  79. def OAI.ExactDerandomization.Umbra.Scope.dustF line 635
  80. abbrev OAI.ExactDerandomization.Umbra.Scope.solve line 637
  81. lemma OAI.ExactDerandomization.Umbra.Scope.cosmosK line 639
  82. lemma OAI.ExactDerandomization.Umbra.Scope.UK line 643
  83. lemma OAI.ExactDerandomization.Umbra.Scope.studyK line 648
  84. lemma OAI.ExactDerandomization.Umbra.Scope.shake line 653
  85. structure OAI.ExactDerandomization.Umbra.Scope.Sane line 664
  86. abbrev OAI.ExactDerandomization.Umbra.Scope.Page line 669
  87. lemma OAI.ExactDerandomization.Umbra.Scope.Sane.stableQ line 675
  88. lemma OAI.ExactDerandomization.Umbra.Scope.Sane.swept line 681
  89. lemma OAI.ExactDerandomization.Umbra.Scope.Sane.date0 line 683
  90. abbrev OAI.ExactDerandomization.Umbra.Scope.Sane.stalkC line 685
  91. lemma OAI.ExactDerandomization.Umbra.Scope.Sane.suiteV line 686
  92. lemma OAI.ExactDerandomization.Umbra.Scope.Sane.calend line 690
  93. lemma OAI.ExactDerandomization.Umbra.Scope.Sane.money0 line 703
  94. def OAI.ExactDerandomization.Umbra.Scope.Sane.Agent line 718
  95. lemma OAI.ExactDerandomization.Umbra.Scope.Sane.bells0 line 722