OAI/Computability/Logspace/SparseRows.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

Sparse row encodings, slot selection, and virtual baselines.

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

  1. structure OAI.ExactDerandomization.Stem.Depot line 20

    Source documentation

    A row with bounded ports and virtual baseline.

    structure Depot where
…
  2. abbrev OAI.ExactDerandomization.Stem.Depot.live line 29
  3. def OAI.ExactDerandomization.Stem.Depot.space line 30
  4. def OAI.ExactDerandomization.Stem.Depot.qpoint line 31
  5. structure OAI.ExactDerandomization.Stem.Depot.Trust line 32
  6. lemma OAI.ExactDerandomization.Stem.Depot.Trust.seen line 41
  7. lemma OAI.ExactDerandomization.Stem.Depot.Trust.snatch line 44
  8. abbrev OAI.ExactDerandomization.Stem.Depot.Trust.coast line 48
  9. lemma OAI.ExactDerandomization.Stem.Depot.Trust.coast_true line 50
  10. structure OAI.ExactDerandomization.Stem.Depot.Trust.ColorF line 89
  11. def OAI.ExactDerandomization.Stem.Depot.Trust.ColorF.mapG line 95
  12. def OAI.ExactDerandomization.Stem.Depot.Trust.GoodS line 98
  13. def OAI.ExactDerandomization.Stem.Depot.Trust.ColorF.hoot line 99
  14. lemma OAI.ExactDerandomization.Stem.Depot.Trust.restates line 103
  15. lemma OAI.ExactDerandomization.Stem.Depot.Trust.region line 108
  16. lemma OAI.ExactDerandomization.Stem.Depot.Trust.onward line 120
  17. lemma OAI.ExactDerandomization.Stem.Depot.Trust.amount0 line 140
  18. structure OAI.ExactDerandomization.Stem.Cage line 162

    Source comment

    main (b=false) weight argument o. b=true witness uses score I, not the upper guarding score.
    structure Cage where
…
  19. abbrev OAI.ExactDerandomization.Stem.Cage.firstC line 177
  20. abbrev OAI.ExactDerandomization.Stem.Cage.fellow line 178
  21. abbrev OAI.ExactDerandomization.Stem.Cage.relay0 line 179
  22. abbrev OAI.ExactDerandomization.Stem.Cage.crown line 180
  23. abbrev OAI.ExactDerandomization.Stem.Cage.figure line 181
  24. structure OAI.ExactDerandomization.Stem.Cage.Ink line 185

    Source documentation

    birth chamber precondition

    structure Ink : Prop where
…
  25. abbrev OAI.ExactDerandomization.Stem.Cage.ratioX line 205
  26. def OAI.ExactDerandomization.Stem.Cage.probeX line 208
  27. lemma OAI.ExactDerandomization.Stem.Cage.probeK line 211
  28. abbrev OAI.ExactDerandomization.Stem.Cage.realkey line 218
  29. abbrev OAI.ExactDerandomization.Stem.Cage.pin line 219
  30. def OAI.ExactDerandomization.Stem.Cage.badge0 line 220
  31. lemma OAI.ExactDerandomization.Stem.Cage.Ink.crew line 228
  32. lemma OAI.ExactDerandomization.Stem.Cage.Ink.fix0 line 232
  33. lemma OAI.ExactDerandomization.Stem.Cage.Ink.crowny line 234
  34. lemma OAI.ExactDerandomization.Stem.Cage.Ink.sculpt line 250
  35. abbrev OAI.ExactDerandomization.Stem.Cage.Peer line 259
  36. abbrev OAI.ExactDerandomization.Stem.Cage.gauge line 260
  37. abbrev OAI.ExactDerandomization.Stem.Cage.goodz line 261
  38. abbrev OAI.ExactDerandomization.Stem.Cage.tolls line 262
  39. abbrev OAI.ExactDerandomization.Stem.Cage.OutC line 263
  40. def OAI.ExactDerandomization.Stem.Cage.voice line 265
  41. lemma OAI.ExactDerandomization.Stem.Cage.Ink.probeB line 272
  42. lemma OAI.ExactDerandomization.Stem.Cage.Ink.orb line 274
  43. lemma OAI.ExactDerandomization.Stem.Cage.Ink.asks line 300
  44. structure OAI.ExactDerandomization.Stem.Cage.Ballot line 321
  45. def OAI.ExactDerandomization.Stem.Cage.Game line 323
  46. def OAI.ExactDerandomization.Stem.Cage.shaft line 324
  47. abbrev OAI.ExactDerandomization.Stem.Cage.belt line 325
  48. abbrev OAI.ExactDerandomization.Stem.Cage.valN line 326
  49. structure OAI.ExactDerandomization.Stem.Cage.Style line 328
  50. lemma OAI.ExactDerandomization.Stem.Cage.Ink.ht0 line 337
  51. lemma OAI.ExactDerandomization.Stem.Cage.Ink.colorBlock line 340
  52. lemma OAI.ExactDerandomization.Stem.Cage.Ink.cost_vol line 353
  53. abbrev OAI.ExactDerandomization.Stem.Cage.Ink.prepare line 357
  54. lemma OAI.ExactDerandomization.Stem.Cage.Ink.chose line 358
  55. abbrev OAI.ExactDerandomization.Stem.Cage.Ink.voteC line 394
  56. lemma OAI.ExactDerandomization.Stem.Cage.Ink.shoots line 395
  57. lemma OAI.ExactDerandomization.Stem.Cage.Style.markers line 422
  58. lemma OAI.ExactDerandomization.Stem.Cage.Style.ck line 429
  59. abbrev OAI.ExactDerandomization.Stem.Cage.Style.child line 432
  60. def OAI.ExactDerandomization.Stem.Cage.Style.listed line 433
  61. lemma OAI.ExactDerandomization.Stem.Cage.Style.park line 435
  62. lemma OAI.ExactDerandomization.Stem.Cage.Style.many line 446
  63. lemma OAI.ExactDerandomization.Stem.Cage.Style.hears line 450
  64. lemma OAI.ExactDerandomization.Stem.Cage.Style.lonely line 458
  65. abbrev OAI.ExactDerandomization.Stem.Cage.zbase line 478
  66. abbrev OAI.ExactDerandomization.Stem.Cage.rearmM line 479
  67. lemma OAI.ExactDerandomization.Stem.Cage.rearmK line 480
  68. abbrev OAI.ExactDerandomization.Stem.Cage.fruit line 481
  69. abbrev OAI.ExactDerandomization.Stem.Cage.exitP line 485
  70. abbrev OAI.ExactDerandomization.Stem.Cage.lastP line 486
  71. abbrev OAI.ExactDerandomization.Stem.Cage.totalG line 487
  72. abbrev OAI.ExactDerandomization.Stem.Cage.skyG line 488
  73. abbrev OAI.ExactDerandomization.Stem.Cage.spice line 490
  74. lemma OAI.ExactDerandomization.Stem.Cage.Ink.spaceG line 496
  75. theorem OAI.ExactDerandomization.Stem.Cage.Ink.fruitage line 498
  76. structure OAI.ExactDerandomization.Stem.Cage.Harvest line 533
  77. lemma OAI.ExactDerandomization.Stem.Cage.bloom line 541