Lax Lean Archive

Earliest-Start-Time Order, and Distinct Endpoints

Lax496464.EstOrder · concepts/Lax496464/EstOrder.lean · lax-496464

definition

Loading review…

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

    Definition

    Two standing conventions of the paper's algorithmic sections, and the rescaling that establishes the second.

    An instance is in earliest-start-time order when its jobs are numbered so that the start times s1≤⋯≤sns_1 \le \dots \le s_n are nondecreasing. Every algorithm of the paper begins by sorting the jobs this way, and its tables are indexed by the resulting order.

    The endpoints of an instance are the 2n2n numbers sjs_j and djd_j. They are distinct when no two of them coincide. Section 4 assumes this, and obtains it by the rescaling

    dj′=(n+1)dj+j,qj′=(n+1)qj,pj′=(n+1)pj,d'_j = (n+1)d_j + j, \qquad q'_j = (n+1)q_j, \qquad p'_j = (n+1)p_j ,

    which leaves the weights alone.

    Concept map
    2 concepts; 12 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 2 of this submission's paper

    Lean source view on GitHub

    1import Lax496464.FlowShop
    2
    3/-!
    4---
    5title: Earliest-Start-Time Order, and Distinct Endpoints
    6type: definition
    7---
    8Two standing conventions of the paper's algorithmic sections, and the rescaling that
    9establishes the second.
    10
    11An instance is *in earliest-start-time order* when its jobs are numbered so that the
    12start times s1≤⋯≤sns_1 \le \dots \le s_n are nondecreasing. Every algorithm of the paper
    13begins by sorting the jobs this way, and its tables are indexed by the resulting order.
    14
    15The *endpoints* of an instance are the 2n2n numbers sjs_j and djd_j. They are *distinct*
    16when no two of them coincide. Section 4 assumes this, and obtains it by the rescaling
    17dj′=(n+1)dj+j,qj′=(n+1)qj,pj′=(n+1)pj,d'_j = (n+1)d_j + j, \qquad q'_j = (n+1)q_j, \qquad p'_j = (n+1)p_j ,
    18which leaves the weights alone.
    19
    20# Formalization Notes
    21
    22Earliest-start-time order is a property of an instance rather than a separate kind of
    23object, so that every result about instances applies to one in that order without
    24transport.
    25
    26The rescaling shifts the *whole* interval of job jj by jj, not only its right endpoint,
    27since sj′=dj′−qj′=(n+1)sj+js'_j = d'_j - q'_j = (n+1)s_j + j. That is what makes it sound, and also what
    28makes it depend on the numbering: two intervals that merely touch, si=djs_i = d_j with no
    29conflict between them, would begin to overlap if the later-starting job had the smaller
    30index. Under earliest-start-time order that cannot happen, because si=dj>sjs_i = d_j > s_j
    31forces j<ij < i. So the assumption is not about the size of the multiplier alone, and the
    32statements about the rescaling carry the order as a hypothesis.
    33
    34The rescaled instance has the same number of jobs, so a set of jobs of one is a set of
    35jobs of the other with no coercion.
    36-/
    37
    38namespace Lax496464.EstOrder
    39
    40open Lax496464.FlowShop Lax496464.FlowShop.Instance
    41
    42/-- The jobs are numbered in nondecreasing order of their start times. -/
    43def EstOrdered (I : Instance) : Prop := ∀ i j : I.Job, i ≤ j → s i ≤ s j
    44
    45/-- No two of the `2n` endpoints `s j` and `d j` coincide. -/
    46structure DistinctEndpoints (I : Instance) : Prop where
    47 /-- Distinct jobs have distinct start times. -/
    48 start_inj : ∀ i j : I.Job, s i = s j → i = j
    49 /-- Distinct jobs have distinct due dates. -/
    50 due_inj : ∀ i j : I.Job, (I.d i : ℤ) = (I.d j : ℤ) → i = j
    51 /-- No start time is a due date. -/
    52 start_ne_due : ∀ i j : I.Job, s i ≠ (I.d j : ℤ)
    53
    54/-- The rescaled instance `d' j = (n+1) d j + j`, `q' j = (n+1) q j`, `p' j = (n+1) p j`,
    55with the weights unchanged. -/
    56def scale (I : Instance) : Instance where
    57 jobs := I.jobs
    58 machines := I.machines
    59 p j := (I.jobs + 1) * I.p j
    60 q j := (I.jobs + 1) * I.q j
    61 d j := (I.jobs + 1) * I.d j + (j : ℕ)
    62 w j := I.w j
    63
    64end Lax496464.EstOrder
    65
    Formalization Notes

    Earliest-start-time order is a property of an instance rather than a separate kind of object, so that every result about instances applies to one in that order without transport.

    The rescaling shifts the whole interval of job jj by jj, not only its right endpoint, since sj′=dj′−qj′=(n+1)sj+js'_j = d'_j - q'_j = (n+1)s_j + j. That is what makes it sound, and also what makes it depend on the numbering: two intervals that merely touch, si=djs_i = d_j with no conflict between them, would begin to overlap if the later-starting job had the smaller index. Under earliest-start-time order that cannot happen, because si=dj>sjs_i = d_j > s_j forces j<ij < i. So the assumption is not about the size of the multiplier alone, and the statements about the rescaling carry the order as a hypothesis.

    The rescaled instance has the same number of jobs, so a set of jobs of one is a set of jobs of the other with no coercion.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…