Lax Lean Archive

Observation 1

Lax496464.Observation1 · concepts/Lax496464/Observation1.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

    A feasible set of jobs admits a just-in-time schedule whose first stage runs the jobs in nondecreasing order of their start times sjs_j — earliest start time first. So nothing is lost by looking only at schedules that preprocess in that order, and an algorithm that decides which jobs to select need not also decide in which order to preprocess them.

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

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 2 of this submission's paper

    Lean source view on GitHub

    1import Lax496464.Conditions
    2
    3/-!
    4---
    5title: Observation 1
    6type: theorem
    7---
    8A feasible set of jobs admits a just-in-time schedule whose first stage runs the jobs in
    9nondecreasing order of their start times sjs_j — earliest start time first. So nothing is
    10lost by looking only at schedules that preprocess in that order, and an algorithm that
    11decides which jobs to select need not also decide in which order to preprocess them.
    12
    13# Formalization Notes
    14
    15The conclusion is stated as a property of one schedule of the given set rather than as a
    16claim about an optimal schedule of the instance. The two are the same: an optimal
    17solution is a feasible set of largest weight, and the statement replaces any schedule of
    18a feasible set by one in earliest-start-time order without changing the set. Phrased this
    19way the statement needs no notion of optimality and applies to every feasible set, which
    20is how the paper's algorithms use it.
    21
    22The order is on start times rather than on indices, and jobs with equal start times are
    23left unordered: the exchange argument produces a schedule in which si<sjs_i < s_j forces
    24ii's first operation to finish before jj's begins, and says nothing about ties.
    25-/
    26
    27namespace Lax496464.Observation1
    28
    29open Lax496464.FlowShop Lax496464.FlowShop.Instance
    30
    31/-- **Observation 1.** Every feasible set has a just-in-time schedule that preprocesses
    32in nondecreasing order of start times. -/
    33axiom exists_est_schedule (I : Instance) (Z : Finset I.Job) (h : Feasible I Z) :
    34 ∃ σ : JITSchedule Z, ∀ i ∈ Z, ∀ j ∈ Z, s i < s j → σ.pre i + I.p i ≤ σ.pre j
    35
    36end Lax496464.Observation1
    37
    Show Proof
    Formalization Notes

    The conclusion is stated as a property of one schedule of the given set rather than as a claim about an optimal schedule of the instance. The two are the same: an optimal solution is a feasible set of largest weight, and the statement replaces any schedule of a feasible set by one in earliest-start-time order without changing the set. Phrased this way the statement needs no notion of optimality and applies to every feasible set, which is how the paper's algorithms use it.

    The order is on start times rather than on indices, and jobs with equal start times are left unordered: the exchange argument produces a schedule in which si<sjs_i < s_j forces ii's first operation to finish before jj's begins, and says nothing about ties.

    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…