OAI/Combinatorics/KServer/AllocationCausality.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Hysteresis switch budget with signed filtering before every reset test. The only costs are actual rank drifts, actual flag changes, held-scale variation, and the new potential at literal wholesale resets.

  1. def OAI.KServer.RuleSchedule.S line 18
  2. def OAI.KServer.RuleSchedule.potential line 21
  3. def OAI.KServer.RuleSchedule.J line 25
  4. def OAI.KServer.RuleSchedule.expense line 30
  5. lemma OAI.KServer.RuleSchedule.S_nonneg line 35
  6. lemma OAI.KServer.RuleSchedule.editing line 38
  7. lemma OAI.KServer.RuleSchedule.run_adapted line 68
  8. lemma OAI.KServer.RuleSchedule.filtering_zero line 89
  9. lemma OAI.KServer.RuleSchedule.payment_step line 109
  10. lemma OAI.KServer.RuleSchedule.payment line 141
  11. lemma OAI.KServer.ActualOutput.key_adapted line 187
  12. lemma OAI.KServer.ActualOutput.b_adapted line 192
  13. lemma OAI.KServer.ActualOutput.schedule_prefix line 206
  14. lemma OAI.KServer.ActualOutput.mark_adapted line 212
  15. lemma OAI.KServer.ActualOutput.marked_adapted line 215
  16. lemma OAI.KServer.ActualOutput.reset_adapted line 217
  17. lemma OAI.KServer.ActualOutput.D_adapted line 222
  18. def OAI.KServer.ActualOutput.ruleFlags line 232
  19. lemma OAI.KServer.ActualOutput.rule_S line 233
  20. lemma OAI.KServer.ActualOutput.flags_adapted line 238
  21. lemma OAI.KServer.ActualOutput.rule_adapted line 243
  22. lemma OAI.KServer.SideProfile.B_bound line 271
  23. lemma OAI.KServer.SideProfile.coefficient_bound line 289
  24. lemma OAI.KServer.SideProfile.endpoint line 310
  25. def OAI.KServer.SideEdits.L line 363
  26. def OAI.KServer.SideEdits.Q line 364
  27. def OAI.KServer.SideEdits.K line 365
  28. lemma OAI.KServer.SideEdits.Q_nonneg line 367
  29. lemma OAI.KServer.SideEdits.pre_edit line 371
  30. lemma OAI.KServer.SideEdits.post_edit line 403
  31. lemma OAI.KServer.SideActualEdits.ordinary_key line 483
  32. lemma OAI.KServer.SideActualEdits.flags_supported line 488
  33. lemma OAI.KServer.SideActualEdits.flags_marked line 493
  34. lemma OAI.KServer.SideActualEdits.flags_change line 506
  35. lemma OAI.KServer.SideActualEdits.prepared_core_bound line 533
  36. lemma OAI.KServer.SideActualEdits.logs_charge line 551
  37. lemma OAI.KServer.SideActualEdits.theta_bound line 583
  38. def OAI.KServer.ActualOutput.capScale line 608
  39. lemma OAI.KServer.ActualOutput.capScale_range line 611
  40. lemma OAI.KServer.ActualOutput.cap_sum line 617
  41. lemma OAI.KServer.ActualOutput.cap_parameters_held line 623
  42. lemma OAI.KServer.ActualOutput.fine_step line 636
  43. lemma OAI.KServer.ActualOutput.fine_budget line 650
  44. lemma OAI.KServer.ActualOutput.d_adapted line 691
  45. lemma OAI.KServer.ActualOutput.α_adapted line 701
  46. lemma OAI.KServer.ActualOutput.side_adapted line 704
  47. lemma OAI.KServer.ActualOutput.out_adapted line 707
  48. lemma OAI.KServer.HierarchicalQuota.quota_adapted line 738