Lax Lean Archive

Lemma 5

Lax496464.Lemma5 · concepts/Lax496464/Lemma5.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 a proper instance the jobs alive at any one instant form a consecutive block of the earliest-start-time order, so the constraint matrix of Section 6.2 has the consecutive ones property: the first family of rows is a family of prefixes, and the second is a family of blocks.

    With the theorem of Fulkerson and Gross this makes the matrix totally unimodular, which is what lets the integer program be solved as a linear program.

    The correspondence the section asserts — that the feasible solutions of the program are exactly the feasible sets — is stated here too. It holds on every instance with equal, positive preprocessing times and nonnegative start times, proper or not.

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

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

    1 ilp_correct proven

    2 ilp_optimum proven

    3 lemma5 proven

    4 matrix_isTotallyUnimodular proven

    In the paper

    • page 6 of this submission's paper

    Lean source view on GitHub

    1import Lax496464.ConsecutiveOnes
    2import Lax496464.IntegerProgram
    3
    4/-!
    5---
    6title: Lemma 5
    7type: theorem
    8---
    9On a proper instance the jobs alive at any one instant form a consecutive block of the
    10earliest-start-time order, so the constraint matrix of Section 6.2 has the consecutive
    11ones property: the first family of rows is a family of prefixes, and the second is a
    12family of blocks.
    13
    14With the theorem of Fulkerson and Gross this makes the matrix totally unimodular, which
    15is what lets the integer program be solved as a linear program.
    16
    17The correspondence the section asserts — that the feasible solutions of the program are
    18exactly the feasible sets — is stated here too. It holds on every instance with equal,
    19positive preprocessing times and nonnegative start times, proper or not.
    20
    21# Formalization Notes
    22
    23Three statements: that the program describes the problem, that its matrix has the
    24consecutive ones property, and that the matrix is therefore totally unimodular.
    25
    26The first is asserted in the paper and not proved there. It is the statement that turns a
    27program on paper into an algorithm for the shop, and both directions are needed: a
    28feasible set gives a feasible vector, and a feasible vector gives a feasible set.
    29
    30Properness enters only in the second. What it buys is that the order by start time and
    31the order by due date agree, which is what makes a set of intervals containing a common
    32point an interval of the order.
    33-/
    34
    35namespace Lax496464.Lemma5
    36
    37open Lax496464.FlowShop Lax496464.FlowShop.Instance
    38open Lax496464.EstOrder Lax496464.ProperInstances
    39open Lax496464.ConsecutiveOnes Lax496464.IntegerProgram
    40open Matrix
    41
    42variable (I : Instance)
    43
    44/-- **The program is the problem.** With equal positive preprocessing times and
    45nonnegative start times, a set of jobs is feasible exactly when its indicator vector
    46satisfies both families of constraints. -/
    47axiom ilp_correct (hest : EstOrdered I) {p : ℕ} (hp : ∀ i : I.Job, I.p i = p) (hp0 : 0 < p)
    48 (hq : ∀ i : I.Job, 0 < I.q i) (hs : ∀ j : I.Job, 0 ≤ s j) (Z : Finset I.Job) :
    49 Feasible I Z ↔ ∀ r, (matrix I *ᵥ indicator I Z) r ≤ rhs I p r
    50
    51/-- **The optimum is the optimum.** A `0/1` vector satisfying the constraints with
    52objective value `W` is exactly a feasible set of weight `W`. -/
    53axiom ilp_optimum (hest : EstOrdered I) {p : ℕ} (hp : ∀ i : I.Job, I.p i = p) (hp0 : 0 < p)
    54 (hq : ∀ i : I.Job, 0 < I.q i) (hs : ∀ j : I.Job, 0 ≤ s j) (W : ℕ) :
    55 (∃ x : I.Job → ℤ, (∀ i, x i = 0 ∨ x i = 1) ∧
    56 (∀ r, (matrix I *ᵥ x) r ≤ rhs I p r) ∧ ∑ i, (I.w i : ℤ) * x i = W) ↔
    57 ∃ Z : Finset I.Job, Feasible I Z ∧ weight I Z = W
    58
    59/-- **Lemma 5.** On a proper instance the constraint matrix has the consecutive ones
    60property. -/
    61axiom lemma5 (hest : EstOrdered I) (h : Proper I) : HasConsecutiveOnes (matrix I)
    62
    63/-- The constraint matrix of a proper instance is totally unimodular. -/
    64axiom matrix_isTotallyUnimodular (hest : EstOrdered I) (h : Proper I) :
    65 (matrix I).IsTotallyUnimodular
    66
    67end Lax496464.Lemma5
    68
    Show ProofShow ProofShow ProofShow Proof
    Formalization Notes

    Three statements: that the program describes the problem, that its matrix has the consecutive ones property, and that the matrix is therefore totally unimodular.

    The first is asserted in the paper and not proved there. It is the statement that turns a program on paper into an algorithm for the shop, and both directions are needed: a feasible set gives a feasible vector, and a feasible vector gives a feasible set.

    Properness enters only in the second. What it buys is that the order by start time and the order by due date agree, which is what makes a set of intervals containing a common point an interval of the order.

    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…