Lax Lean Archive

Uniform Preprocessing Times, and Proper Instances

Lax496464.ProperInstances · concepts/Lax496464/ProperInstances.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 restrictions on an instance, both from Section 6 of the paper.

    An instance has uniform preprocessing times when all pjp_j are equal. It is proper when no job's second-operation interval [sj,dj)[s_j, d_j) contains another's.

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

    In the paper

    • page 6 of this submission's paper

    Lean source view on GitHub

    1import Lax496464.FlowShop
    2
    3/-!
    4---
    5title: Uniform Preprocessing Times, and Proper Instances
    6type: definition
    7---
    8Two restrictions on an instance, both from Section 6 of the paper.
    9
    10An instance has *uniform preprocessing times* when all pjp_j are equal. It is *proper*
    11when no job's second-operation interval [sj,dj)[s_j, d_j) contains another's.
    12
    13# Formalization Notes
    14
    15Uniformity is stated as the existence of a common value rather than as a constant carried
    16by the instance, so that it is a property of an instance and not a different kind of
    17object.
    18
    19Properness is stated as the impossibility of containment, with the degenerate case
    20excluded by the hypothesis that the two jobs are distinct: two jobs with the same
    21interval would otherwise make every instance improper. Containment is the wide reading —
    22sj≤sis_j \le s_i and di≤djd_i \le d_j, allowing either endpoint to coincide — which is the one
    23the paper's argument uses: on a proper instance the order by start time and the order by
    24due date agree, and that needs the non-strict form.
    25-/
    26
    27namespace Lax496464.ProperInstances
    28
    29open Lax496464.FlowShop Lax496464.FlowShop.Instance
    30
    31/-- All preprocessing times are equal. -/
    32def Uniform (I : Instance) : Prop := ∃ p : ℕ, ∀ j : I.Job, I.p j = p
    33
    34/-- No job's second-operation interval contains another's. -/
    35def Proper (I : Instance) : Prop :=
    36 ∀ i j : I.Job, i ≠ j → ¬ (s j ≤ s i ∧ (I.d i : ℤ) ≤ (I.d j : ℤ))
    37
    38end Lax496464.ProperInstances
    39
    Formalization Notes

    Uniformity is stated as the existence of a common value rather than as a constant carried by the instance, so that it is a property of an instance and not a different kind of object.

    Properness is stated as the impossibility of containment, with the degenerate case excluded by the hypothesis that the two jobs are distinct: two jobs with the same interval would otherwise make every instance improper. Containment is the wide reading — sj≤sis_j \le s_i and di≤djd_i \le d_j, allowing either endpoint to coincide — which is the one the paper's argument uses: on a proper instance the order by start time and the order by due date agree, and that needs the non-strict form.

    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…