OAI/Combinatorics/UniformKServer/CooldownLabels.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Fixed finite label pools with a full preceding-step cooldown. No historical label is globally reserved: only current and preceding record sets are excluded.

  1. abbrev OAI.UniformKServer.CooldownLabels.Slot line 17
  2. def OAI.UniformKServer.CooldownLabels.chooseSlot line 19
  3. theorem OAI.UniformKServer.CooldownLabels.chooseSlot_not_mem line 22
  4. structure OAI.UniformKServer.CooldownLabels.State line 31
  5. def OAI.UniformKServer.CooldownLabels.step line 35
  6. def OAI.UniformKServer.CooldownLabels.run line 41
  7. theorem OAI.UniformKServer.CooldownLabels.previous_card line 45
  8. theorem OAI.UniformKServer.CooldownLabels.chosen_fresh line 51
  9. theorem OAI.UniformKServer.CooldownLabels.label_none line 61
  10. theorem OAI.UniformKServer.CooldownLabels.label_old line 65
  11. theorem OAI.UniformKServer.CooldownLabels.label_new_fresh line 70
  12. theorem OAI.UniformKServer.CooldownLabels.injective line 76
  13. theorem OAI.UniformKServer.CooldownLabels.common_anchor line 111
  14. theorem OAI.UniformKServer.CooldownLabels.one_step_cooldown line 132

    Source documentation

    A new label is absent not only now, but from the whole preceding map.

    theorem one_step_cooldown (M : ℕ) (S : ℕ → Finset I) (birth : ℕ → Option I)
    (hS : ∀ t, (S t).card≤M) (t : ℕ) (n : I) (hb : birth (t+1)=some n) :
    (run M S birth (t+2)).label n∉(S t).image (run M S birth t).label := by
…

    Mentions: OAI.UniformKServer.CooldownLabels.run