Lax Lean Archive

Lemma 2

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

    The two recursions of Section 4 are correct.

    At an instant tt at which job jj becomes due and nothing else happens, the entries at tt are those at the previous endpoint with jj either present or absent: jj is no longer alive, so it has left the state, and whether it was selected is what the two cases record. Equation (4).

    At an instant tt at which job jj starts and nothing else happens, either jj is not selected and the state is unchanged, or jj is selected, in which case it joins the state, the state must still be small enough to fit on the machines, and the first-stage machine must be able to finish jj by tt. Equation (3).

    Past the last start time the table answers the question: some state carries weight W′W' exactly when a feasible set of weight W′W' exists.

    Concept map
    5 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 exists_reachable_iff proven

    2 reachable_due proven

    3 reachable_start proven

    In the paper

    • page 4 of this submission's paper

    Lean source view on GitHub

    1import Lax496464.Sweep
    2
    3/-!
    4---
    5title: Lemma 2
    6type: theorem
    7---
    8The two recursions of Section 4 are correct.
    9
    10At an instant tt at which job jj becomes due and nothing else happens, the entries at
    11tt are those at the previous endpoint with jj either present or absent: jj is no
    12longer alive, so it has left the state, and whether it was selected is what the two cases
    13record. Equation (4).
    14
    15At an instant tt at which job jj starts and nothing else happens, either jj is not
    16selected and the state is unchanged, or jj is selected, in which case it joins the
    17state, the state must still be small enough to fit on the machines, and the first-stage
    18machine must be able to finish jj by tt. Equation (3).
    19
    20Past the last start time the table answers the question: some state carries weight W′W'
    21exactly when a feasible set of weight W′W' exists.
    22
    23# Formalization Notes
    24
    25Both equations are stated as equivalences, so each says at once that the recursion
    26invents no entry and loses none.
    27
    28The hypotheses spell out what "nothing else happens" means: no other start time and no
    29other due date lies in the half-open interval between the two endpoints. On an instance
    30with distinct endpoints, consecutive endpoints satisfy exactly one of the two patterns,
    31which is what turns the two equations into a sweep.
    32
    33Positive processing times are assumed, as everywhere in the paper. Here they are what
    34makes a job alive at its own start time, so that selecting a job really does put it into
    35the state.
    36-/
    37
    38namespace Lax496464.Lemma2
    39
    40open Lax496464.FlowShop Lax496464.FlowShop.Instance Lax496464.Sweep
    41
    42variable (I : Instance)
    43
    44/-- **Equation (4).** The step across an instant at which job `j` becomes due. -/
    45axiom reachable_due (hq : ∀ i : I.Job, 0 < I.q i) {t' t : ℤ} {j : I.Job}
    46 {X : Finset I.Job} {W' : ℕ} {P' : ℤ}
    47 (htt : t' < t) (hdj : (I.d j : ℤ) = t)
    48 (hnos : ∀ k : I.Job, ¬ (t' < s k ∧ s k ≤ t))
    49 (hnod : ∀ k : I.Job, k ≠ j → ¬ (t' < (I.d k : ℤ) ∧ (I.d k : ℤ) ≤ t)) :
    50 Reachable I t X W' P' ↔
    51 j ∉ X ∧ (Reachable I t' X W' P' ∨ Reachable I t' (insert j X) W' P')
    52
    53/-- **Equation (3).** The step across an instant at which job `j` starts. -/
    54axiom reachable_start (hq : ∀ i : I.Job, 0 < I.q i) {t' t : ℤ} {j : I.Job}
    55 {X : Finset I.Job} {W' : ℕ} {P' : ℤ}
    56 (htt : t' < t) (hsj : s j = t)
    57 (hnos : ∀ k : I.Job, k ≠ j → ¬ (t' < s k ∧ s k ≤ t))
    58 (hnod : ∀ k : I.Job, ¬ (t' < (I.d k : ℤ) ∧ (I.d k : ℤ) ≤ t)) :
    59 Reachable I t X W' P' ↔
    60 (j ∉ X ∧ Reachable I t' X W' P') ∨
    61 (j ∈ X ∧ (X.erase j).card < I.machines ∧
    62 ∃ (W'' : ℕ) (P'' : ℤ), W'' + I.w j = W' ∧ Reachable I t' (X.erase j) W'' P'' ∧
    63 P'' + I.p j ≤ s j ∧ P'' + I.p j ≤ P')
    64
    65/-- **The read-off.** Past the last start time, a state of weight `W'` is exactly a
    66feasible set of weight `W'`. -/
    67axiom exists_reachable_iff {t : ℤ} (ht : ∀ k : I.Job, s k ≤ t) (W' : ℕ) :
    68 (∃ (X : Finset I.Job) (P' : ℤ), Reachable I t X W' P') ↔
    69 ∃ Z : Finset I.Job, Feasible I Z ∧ weight I Z = W'
    70
    71end Lax496464.Lemma2
    72
    Show ProofShow ProofShow Proof
    Formalization Notes

    Both equations are stated as equivalences, so each says at once that the recursion invents no entry and loses none.

    The hypotheses spell out what "nothing else happens" means: no other start time and no other due date lies in the half-open interval between the two endpoints. On an instance with distinct endpoints, consecutive endpoints satisfy exactly one of the two patterns, which is what turns the two equations into a sweep.

    Positive processing times are assumed, as everywhere in the paper. Here they are what makes a job alive at its own start time, so that selecting a job really does put it into the state.

    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…