While this submission is a draft, it cannot be used by other submissions.

Day-Independent Due Dates and Processing Times

Lax117284.Theorem13 · concepts/Lax117284/Theorem13.lean · lax-117284

proven

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Theorem 13. Let II be an instance whose due dates and processing times are both day-independent, so that all mm days have the same conflict graph GG. Then II admits a kk-fair schedule if and only if k⋅χ(G)≤mk \cdot \chi(G) \le m, where χ(G)\chi(G) is the chromatic number of GG.

    A feasible schedule meets a clique of GG in at most one client per day, so a clique of cc vertices whose clients are each served kk times needs kc≤mk c \le m days; this gives the condition with the clique number in place of the chromatic number. Conversely a proper colouring of GG with χ(G)\chi(G) colours partitions the clients into χ(G)\chi(G) independent sets, and serving the classes in rotation serves every client on ⌊m/χ(G)⌋≥k\lfloor m / \chi(G)\rfloor \ge k days. Both bounds meet because GG is an interval graph, and its chromatic number therefore equals its clique number.

    Concept map
    4 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    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

    1import Lax117284.ConflictGraph
    2
    3/-!
    4---
    5title: Day-Independent Due Dates and Processing Times
    6type: theorem
    7---
    8**Theorem 13.** Let II be an instance whose due dates and processing times are both
    9day-independent, so that all mm days have the same conflict graph GG. Then II admits a
    10kk-fair schedule if and only if k⋅χ(G)≤mk \cdot \chi(G) \le m, where χ(G)\chi(G) is the chromatic
    11number of GG.
    12
    13A feasible schedule meets a clique of GG in at most one client per day, so a clique of cc
    14vertices whose clients are each served kk times needs kc≤mk c \le m days; this gives the
    15condition with the clique number in place of the chromatic number. Conversely a proper
    16colouring of GG with χ(G)\chi(G) colours partitions the clients into χ(G)\chi(G) independent
    17sets, and serving the classes in rotation serves every client on
    18⌊m/χ(G)⌋≥k\lfloor m / \chi(G)\rfloor \ge k days. Both bounds meet because GG is an interval graph,
    19and its chromatic number therefore equals its clique number.
    20
    21# Formalization Notes
    22
    23The two extreme values of the source's chain of inequalities are stated separately: that
    24the problem is equivalent to the condition on the clique number, and that the chromatic
    25number of a day's conflict graph is its clique number. The second is the only property of
    26interval graphs the results use — a paper cites it, and here it is proved for these graphs.
    27
    28The chromatic number is mathlib's, with values in the extended naturals, so the condition
    29is stated there; with the clique number, a natural number, the condition is an inequality
    30of natural numbers.
    31-/
    32
    33namespace Lax117284.Theorem13
    34
    35open Lax117284.Scheduling Lax117284.ConflictGraph
    36
    37variable {I : Instance}
    38
    39/-- **Day-independent instances have one conflict graph.** -/
    40axiom 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
    44number.** -/
    45axiom 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.** -/
    49axiom 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
    54schedule exists exactly when `k` times the chromatic number of the conflict graph is at
    55most the number of days. -/
    56axiom 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
    60end Lax117284.Theorem13
    61
    Show ProofShow ProofShow ProofShow Proof
    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.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…