Prove2Me

THEOREM (§2 Sequencing Theorem), p. 544 — some minmax optimal sequence has a least-cost job of SS last

Proved
LawlerPrec.MinMax.sequencing_theorem

by mikedeng1 · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

minmaxp2o-batch-pfp1ap2o-gran-per-chapterp2o-plan-paperp2o-v1precedence-constraintsschedulingsingle-machine

Let JJ be a nonempty finite set of jobs with non-negative processing times aja_j, monotone nondecreasing cost functions cjc_j, and arbitrary precedence constraints, and suppose some sequence of JJ observes the constraints. Let SS be the set of jobs of JJ not required to precede any others, T=∑j∈JajT = \sum_{j \in J} a_j, and let k∈Sk \in S satisfy

ck(T)  =  min⁡j∈Scj(T).c_k(T) \;=\; \min_{j \in S} c_j(T).

Then there exists a minmax optimal sequence in which job kk is last.

This is the paper's only labelled result. It reduces the choice of the last job of an optimal sequence to a comparison of the eligible jobs' costs at the fixed time TT, independently of how the other jobs are ordered.

Formalization Note Two hypotheses are added and disclosed: non-negative processing times (durations; the paper's proof uses them) and the existence of a feasible sequence, which "there exists a minmax optimal sequence" presupposes (with a cycle in the constraints, no sequence observes them, while SS can still be nonempty). The minimum is encoded as k∈Sk \in S and ck(T)≤cj(T)c_k(T) \le c_j(T) for all j∈Sj \in S; ties are allowed.

Preamble
import Mathlib
import Definitions.Def_LawlerPrec_MinMax_IsMinmaxOptimal
import Definitions.Def_LawlerPrec_MinMax_lastEligible
Formal statement
namespace LawlerPrec.MinMax

/-- THEOREM (§2 Sequencing Theorem, Lawler 1973, p. 544). Let `S = lastEligible prec J` be the jobs
not required to precede any others, `T = ∑_{j ∈ J} a_j`, and `k ∈ S` with
`c_k(T) = min_{j ∈ S} c_j(T)`. If some sequence of `J` observes the precedence constraints, then
there is a minmax optimal sequence in which job `k` is last. -/
theorem sequencing_theorem {ι : Type*} [DecidableEq ι] (a : ι → ℝ) (c : ι → ℝ → ℝ)
    (prec : ι → ι → Prop) (J : Finset ι) (hJ : J.Nonempty) (ha : ∀ j ∈ J, 0 ≤ a j)
    (hc : ∀ j ∈ J, Monotone (c j)) (hfeas : ∃ l : List ι, IsFeasible prec J l) (k : ι)
    (hk : k ∈ lastEligible prec J)
    (hmin : ∀ j ∈ lastEligible prec J, c k (∑ i ∈ J, a i) ≤ c j (∑ i ∈ J, a i)) :
    ∃ l : List ι, IsMinmaxOptimal a c prec J hJ l ∧ l.getLast? = some k := by sorry

end LawlerPrec.MinMax
Source
Lawler, Optimal Sequencing of a Single Machine Subject to Precedence Constraints, Management Science 19(5), 1973, p. 544, §2 Sequencing Theorem, THEOREM
Human review

  • Endorsed by Shuze Chen · Oct 5, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 5, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph