OAI/Combinatorics/KServer/MetricService.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Common complete keys have controlled anchors. Only common moving heavy labels incur chronological travel; tiers and singleton fallback are fixed.

  1. lemma OAI.KServer.LevelKeys.inl_key line 19
  2. def OAI.KServer.LevelKeys.motion line 31
  3. lemma OAI.KServer.LevelKeys.motion_nonneg line 38
  4. lemma OAI.KServer.LevelKeys.motion_le line 48
  5. lemma OAI.KServer.LevelKeys.common_anchor_motion line 57
  6. lemma OAI.KServer.LevelKeys.common_anchor_distance line 91
  7. abbrev OAI.KServer.JointMetric.Node line 113
  8. def OAI.KServer.JointMetric.motion line 114
  9. lemma OAI.KServer.JointMetric.motion_nonneg line 117
  10. lemma OAI.KServer.JointMetric.anchor_close line 124
  11. lemma OAI.KServer.JointMetric.anchor_move line 130
  12. lemma OAI.KServer.JointMetric.anchor_move_bound line 137
  13. lemma OAI.KServer.JointMetric.count_witness line 147
  14. lemma OAI.KServer.JointMetric.motion_sum line 159
  15. lemma OAI.KServer.JointMetric.count_matching line 184
  16. abbrev OAI.KServer.JointService.Node line 216
  17. def OAI.KServer.JointService.leaf line 218
  18. lemma OAI.KServer.JointService.leaf_number line 222
  19. lemma OAI.KServer.JointService.leaf_quota line 227
  20. lemma OAI.KServer.JointService.leaf_park line 239
  21. lemma OAI.KServer.JointService.leaf_anchor line 251
  22. lemma OAI.KServer.JointService.count_serves line 269