OAI/Combinatorics/UniformKServer/LevelMap.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

The literal level key: heavy precedence, then chronological tiers in their fixed order, then singleton fallback. Its alphabet is fixed by the instance, not by the finite law or horizon used to analyze the independent tape.

  1. structure OAI.UniformKServer.LevelMap.Data line 23
  2. abbrev OAI.UniformKServer.LevelMap.HeavySlot line 33
  3. abbrev OAI.UniformKServer.LevelMap.Label line 34
  4. abbrev OAI.UniformKServer.LevelMap.HeavyTape line 35
  5. abbrev OAI.UniformKServer.LevelMap.TierTape line 36
  6. abbrev OAI.UniformKServer.LevelMap.Tape line 38
  7. theorem OAI.UniformKServer.LevelMap.Data.quota line 42
  8. def OAI.UniformKServer.LevelMap.Data.point line 48
  9. def OAI.UniformKServer.LevelMap.Data.heavyFlag line 49
  10. def OAI.UniformKServer.LevelMap.Data.heavyState line 51
  11. def OAI.UniformKServer.LevelMap.Data.heavyKey line 55
  12. def OAI.UniformKServer.LevelMap.Data.tierKey line 58
  13. def OAI.UniformKServer.LevelMap.Data.key line 62
  14. def OAI.UniformKServer.LevelMap.Data.anchor line 65
  15. def OAI.UniformKServer.LevelMap.Data.tierLaw line 70
  16. def OAI.UniformKServer.LevelMap.Data.law line 74
  17. theorem OAI.UniformKServer.LevelMap.Data.first_witness line 77
  18. theorem OAI.UniformKServer.LevelMap.Data.heavy_covers line 91
  19. theorem OAI.UniformKServer.LevelMap.Data.tier_covers line 99
  20. theorem OAI.UniformKServer.LevelMap.Data.covers line 105
  21. theorem OAI.UniformKServer.LevelMap.Data.diameter line 119