The Extreme Values of the Fairness Parameter
Lax117284.ExtremeFairness · concepts/Lax117284/ExtremeFairness.lean · lax-117284
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Lemma
Three values of the fairness parameter are settled by inspection. For nothing is required of a schedule, so every instance is a yes-instance. For every client must be served on every day, which is possible exactly when no two jobs of a day conflict. For no client can be served often enough, so an instance with at least one client is a no-instance.
Concept map
Evidence
This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.
1 hasKFairSchedule_days_iff proven
2 hasKFairSchedule_zero proven
3 not_hasKFairSchedule_of_days_lt proven
Lean source view on GitHub
| 1 | import Lax117284.Scheduling |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: The Extreme Values of the Fairness Parameter |
| 6 | type: lemma |
| 7 | --- |
| 8 | Three values of the fairness parameter are settled by inspection. For nothing is |
| 9 | required of a schedule, so every instance is a yes-instance. For every client must |
| 10 | be served on every day, which is possible exactly when no two jobs of a day conflict. For |
| 11 | no client can be served often enough, so an instance with at least one client is a |
| 12 | no-instance. |
| 13 | |
| 14 | # Formalization Notes |
| 15 | |
| 16 | The case needs an instance with a client: an instance with none has nothing to |
| 17 | require and admits the empty schedule for every parameter. |
| 18 | -/ |
| 19 | |
| 20 | namespace Lax117284.ExtremeFairness |
| 21 | |
| 22 | open Lax117284.Scheduling |
| 23 | |
| 24 | /-- **A fairness parameter of `0` requires nothing.** -/ |
| 25 | axiom hasKFairSchedule_zero (I : Instance) : I.HasKFairSchedule 0 |
| 26 | |
| 27 | /-- **Serving every client on every day is possible exactly for conflict-free |
| 28 | instances.** -/ |
| 29 | axiom hasKFairSchedule_days_iff (I : Instance) : |
| 30 | I.HasKFairSchedule I.days ↔ I.ConflictFree |
| 31 | |
| 32 | /-- **A fairness parameter above the number of days is unattainable**, as soon as there is |
| 33 | a client of whom it is demanded. -/ |
| 34 | axiom not_hasKFairSchedule_of_days_lt {I : Instance} {k : ℕ} (hk : I.days < k) |
| 35 | (hn : 0 < I.clients) : ¬ I.HasKFairSchedule k |
| 36 | |
| 37 | end Lax117284.ExtremeFairness |
| 38 |
Formalization Notes
The case needs an instance with a client: an instance with none has nothing to require and admits the empty schedule for every parameter.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments