Lax Lean Archive

Every Instance May Be Assumed to Have Distinct Endpoints

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

proven

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

    Theorem

    On an instance in earliest-start-time order, the rescaling of Section 4 changes neither which sets of jobs are feasible nor what they weigh, and it makes the 2n2n endpoints pairwise distinct. So an algorithm may assume distinct endpoints, which is what the sweeps of Sections 4 and 5 do when they step from one endpoint to the next and treat each step as carrying a single event.

    Concept map
    4 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.

    1 scale_distinctEndpoints proven

    2 scale_feasible_iff proven

    3 scale_weight proven

    In the paper

    • page 4 of this submission's paper

    Lean source view on GitHub

    1import Lax496464.Conditions
    2import Lax496464.EstOrder
    3
    4/-!
    5---
    6title: Every Instance May Be Assumed to Have Distinct Endpoints
    7type: theorem
    8---
    9On an instance in earliest-start-time order, the rescaling of Section 4 changes neither
    10which sets of jobs are feasible nor what they weigh, and it makes the 2n2n endpoints
    11pairwise distinct. So an algorithm may assume distinct endpoints, which is what the
    12sweeps of Sections 4 and 5 do when they step from one endpoint to the next and treat each
    13step as carrying a single event.
    14
    15# Formalization Notes
    16
    17Three statements, because the rescaling has three things to deliver: it preserves the
    18feasible sets, it preserves their weights, and it separates the endpoints. The first is
    19the one with content — a conflict must be created by the rescaling neither where there
    20was none nor destroyed where there was one — and it is where the hypothesis of
    21earliest-start-time order is used.
    22
    23The order is preserved as well, so the rescaled instance is again an admissible input for
    24every algorithm. That is stated too, since an assumption discharged by a transformation
    25is of no use if the transformation breaks another.
    26
    27Positive processing times are assumed, and the rescaling needs them: with qj=0q_j = 0 the
    28window [sj,dj)[s_j, d_j) is empty, the scaled instance has sj=djs_j = d_j for that job, and the
    29endpoints are not separated after all. The paper's algorithms carry the same assumption
    30wherever they count jobs alive at an instant.
    31-/
    32
    33namespace Lax496464.Normalization
    34
    35open Lax496464.FlowShop Lax496464.FlowShop.Instance Lax496464.EstOrder
    36
    37/-- **Section 4.** The rescaling preserves feasibility. -/
    38axiom scale_feasible_iff (I : Instance) (h : EstOrdered I) (hq : ∀ i : I.Job, 0 < I.q i)
    39 (Z : Finset I.Job) :
    40 Feasible (scale I) Z ↔ Feasible I Z
    41
    42/-- The rescaling preserves weights. -/
    43axiom scale_weight (I : Instance) (Z : Finset I.Job) :
    44 weight (scale I) Z = weight I Z
    45
    46/-- The rescaling separates the endpoints, and keeps the jobs in earliest-start-time
    47order. -/
    48axiom scale_distinctEndpoints (I : Instance) (h : EstOrdered I) (hq : ∀ i : I.Job, 0 < I.q i) :
    49 DistinctEndpoints (scale I) ∧ EstOrdered (scale I)
    50
    51end Lax496464.Normalization
    52
    Show ProofShow ProofShow Proof
    Formalization Notes

    Three statements, because the rescaling has three things to deliver: it preserves the feasible sets, it preserves their weights, and it separates the endpoints. The first is the one with content — a conflict must be created by the rescaling neither where there was none nor destroyed where there was one — and it is where the hypothesis of earliest-start-time order is used.

    The order is preserved as well, so the rescaled instance is again an admissible input for every algorithm. That is stated too, since an assumption discharged by a transformation is of no use if the transformation breaks another.

    Positive processing times are assumed, and the rescaling needs them: with qj=0q_j = 0 the window [sj,dj)[s_j, d_j) is empty, the scaled instance has sj=djs_j = d_j for that job, and the endpoints are not separated after all. The paper's algorithms carry the same assumption wherever they count jobs alive at an instant.

    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…