Lax Lean Archive

The Endpoint Sweep of Section 4, and Its Table

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

    The algorithm behind the first half of the third theorem. The time axis is swept from left to right through the 2n2n endpoints — the start times and the due dates — and the state carried at an instant tt is the set XX of selected jobs alive then, together with the weight selected so far and the preprocessing time spent. The table entry

    Tt[X,W′]T_t[X, W']

    records whether a feasible selection of weight W′W', all of whose jobs have started by tt, is alive at tt in exactly XX and costs at most P′P' to preprocess.

    Between two consecutive endpoints nothing happens, and at an endpoint exactly one thing does: a job becomes due, or a job starts. The two recursions of Section 4 say what each does to the table.

    Since XX is a set of jobs alive at one instant, it has at most ω\omega members, so the table has 2ω2^\omega columns — which is where the running time comes from.

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

    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: The Endpoint Sweep of Section 4, and Its Table
    7type: definition
    8---
    9The algorithm behind the first half of the third theorem. The time axis is swept from
    10left to right through the 2n2n *endpoints* — the start times and the due dates — and the
    11state carried at an instant tt is the set XX of selected jobs alive then, together with
    12the weight selected so far and the preprocessing time spent. The table entry
    13Tt[X,W′]T_t[X, W']
    14records whether a feasible selection of weight W′W', all of whose jobs have started by
    15tt, is alive at tt in exactly XX and costs at most P′P' to preprocess.
    16
    17Between two consecutive endpoints nothing happens, and at an endpoint exactly one thing
    18does: a job becomes due, or a job starts. The two recursions of Section 4 say what each
    19does to the table.
    20
    21Since XX is a set of jobs alive at one instant, it has at most ω\omega members, so the
    22table has 2ω2^\omega columns — which is where the running time comes from.
    23
    24# Formalization Notes
    25
    26The table is again a predicate rather than a value, downward closed in the preprocessing
    27budget, for the reason given for the table of Section 3.
    28
    29The state is the set of *selected* jobs alive at tt, not a set of machines: which machine
    30runs which job never matters, because at most mm jobs alive at once is the whole of
    31Condition 2. That is the depth characterization, and it is what makes a subset of the
    32alive jobs the right index.
    33
    34The preprocessing budget runs forwards here and backwards in Section 3, so the two
    35programs carry the same information in opposite directions. Nothing is claimed about
    36their relationship; each is proved against the definition of a feasible set.
    37
    38The endpoints are collected as a finite set of integers, with no order imposed. The
    39sweep's step needs consecutive endpoints, and that two consecutive ones enclose exactly
    40one event is where the distinctness of the endpoints is used.
    41-/
    42
    43namespace Lax496464.Sweep
    44
    45open Lax496464.FlowShop Lax496464.FlowShop.Instance
    46
    47variable (I : Instance)
    48
    49/-- The total preprocessing time of `Z`. -/
    50def pload (Z : Finset I.Job) : ℤ := ∑ i ∈ Z, (I.p i : ℤ)
    51
    52/-- The table: a feasible set of weight `W'`, all of whose jobs have started by `t`, is
    53alive at `t` in exactly `X` and costs at most `P'` to preprocess. -/
    54def Reachable (t : ℤ) (X : Finset I.Job) (W' : ℕ) (P' : ℤ) : Prop :=
    55 ∃ Z : Finset I.Job, Feasible I Z ∧ (∀ k ∈ Z, s k ≤ t) ∧
    56 running I Z t = X ∧ weight I Z = W' ∧ pload I Z ≤ P'
    57
    58/-- The `2n` endpoints: the start times and the due dates. -/
    59def endpoints : Finset ℤ :=
    60 (Finset.univ.image fun k : I.Job => s k) ∪
    61 (Finset.univ.image fun k : I.Job => (I.d k : ℤ))
    62
    63end Lax496464.Sweep
    64
    Formalization Notes

    The table is again a predicate rather than a value, downward closed in the preprocessing budget, for the reason given for the table of Section 3.

    The state is the set of selected jobs alive at tt, not a set of machines: which machine runs which job never matters, because at most mm jobs alive at once is the whole of Condition 2. That is the depth characterization, and it is what makes a subset of the alive jobs the right index.

    The preprocessing budget runs forwards here and backwards in Section 3, so the two programs carry the same information in opposite directions. Nothing is claimed about their relationship; each is proved against the definition of a feasible set.

    The endpoints are collected as a finite set of integers, with no order imposed. The sweep's step needs consecutive endpoints, and that two consecutive ones enclose exactly one event is where the distinctness of the endpoints is used.

    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…