Day-Independent Due Dates and Processing Times
Lax117284.Theorem13 · concepts/Lax117284/Theorem13.lean · lax-117284
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Theorem 13. Let be an instance whose due dates and processing times are both day-independent, so that all days have the same conflict graph . Then admits a -fair schedule if and only if , where is the chromatic number of .
A feasible schedule meets a clique of in at most one client per day, so a clique of vertices whose clients are each served times needs days; this gives the condition with the clique number in place of the chromatic number. Conversely a proper colouring of with colours partitions the clients into independent sets, and serving the classes in rotation serves every client on days. Both bounds meet because is an interval graph, and its chromatic number therefore equals its clique number.
Concept map
Evidence
This concept declares 4 statements. Each proof establishes one of them relative to its assumptions.
1 chromaticNumber_dayGraph proven
2 dayGraph_eq_of_dayIndep proven
3 hasKFairSchedule_iff_mul_chromaticNumber_le proven
4 hasKFairSchedule_iff_mul_cliqueNum_le proven
In the paper
- page 3 of this submission's paper
Lean source view on GitHub
| 1 | import Lax117284.ConflictGraph |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Day-Independent Due Dates and Processing Times |
| 6 | type: theorem |
| 7 | --- |
| 8 | **Theorem 13.** Let be an instance whose due dates and processing times are both |
| 9 | day-independent, so that all days have the same conflict graph . Then admits a |
| 10 | -fair schedule if and only if , where is the chromatic |
| 11 | number of . |
| 12 | |
| 13 | A feasible schedule meets a clique of in at most one client per day, so a clique of |
| 14 | vertices whose clients are each served times needs days; this gives the |
| 15 | condition with the clique number in place of the chromatic number. Conversely a proper |
| 16 | colouring of with colours partitions the clients into independent |
| 17 | sets, and serving the classes in rotation serves every client on |
| 18 | days. Both bounds meet because is an interval graph, |
| 19 | and its chromatic number therefore equals its clique number. |
| 20 | |
| 21 | # Formalization Notes |
| 22 | |
| 23 | The two extreme values of the source's chain of inequalities are stated separately: that |
| 24 | the problem is equivalent to the condition on the clique number, and that the chromatic |
| 25 | number of a day's conflict graph is its clique number. The second is the only property of |
| 26 | interval graphs the results use — a paper cites it, and here it is proved for these graphs. |
| 27 | |
| 28 | The chromatic number is mathlib's, with values in the extended naturals, so the condition |
| 29 | is stated there; with the clique number, a natural number, the condition is an inequality |
| 30 | of natural numbers. |
| 31 | -/ |
| 32 | |
| 33 | namespace Lax117284.Theorem13 |
| 34 | |
| 35 | open Lax117284.Scheduling Lax117284.ConflictGraph |
| 36 | |
| 37 | variable {I : Instance} |
| 38 | |
| 39 | /-- **Day-independent instances have one conflict graph.** -/ |
| 40 | axiom dayGraph_eq_of_dayIndep (hd : I.DayIndepD) (hp : I.DayIndepP) (i i' : Fin I.days) : |
| 41 | dayGraph I i = dayGraph I i' |
| 42 | |
| 43 | /-- **A day's conflict graph is an interval graph, so its chromatic number is its clique |
| 44 | number.** -/ |
| 45 | axiom chromaticNumber_dayGraph (I : Instance) (i : Fin I.days) : |
| 46 | (dayGraph I i).chromaticNumber = (dayGraph I i).cliqueNum |
| 47 | |
| 48 | /-- **Theorem 13, with the clique number.** -/ |
| 49 | axiom hasKFairSchedule_iff_mul_cliqueNum_le (hd : I.DayIndepD) (hp : I.DayIndepP) |
| 50 | (i₀ : Fin I.days) (k : ℕ) : |
| 51 | I.HasKFairSchedule k ↔ k * (dayGraph I i₀).cliqueNum ≤ I.days |
| 52 | |
| 53 | /-- **Theorem 13.** With day-independent due dates and processing times, a `k`-fair |
| 54 | schedule exists exactly when `k` times the chromatic number of the conflict graph is at |
| 55 | most the number of days. -/ |
| 56 | axiom hasKFairSchedule_iff_mul_chromaticNumber_le (hd : I.DayIndepD) (hp : I.DayIndepP) |
| 57 | (i₀ : Fin I.days) (k : ℕ) : |
| 58 | I.HasKFairSchedule k ↔ (k : ℕ∞) * (dayGraph I i₀).chromaticNumber ≤ I.days |
| 59 | |
| 60 | end Lax117284.Theorem13 |
| 61 |
Formalization Notes
The two extreme values of the source's chain of inequalities are stated separately: that the problem is equivalent to the condition on the clique number, and that the chromatic number of a day's conflict graph is its clique number. The second is the only property of interval graphs the results use — a paper cites it, and here it is proved for these graphs.
The chromatic number is mathlib's, with values in the extended naturals, so the condition is stated there; with the clique number, a natural number, the condition is an inequality of natural numbers.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments