§2, proof of the Theorem, p. 544 — moving a job of $S$ to the end keeps the precedence constraints

Proved

LawlerPrec.MinMax.move_last_feasible

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

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

Let $\pi'$ be a sequence of the job set $J$ that observes the precedence constraints, and let $k \in S(J)$ be a job that is not required to precede any other job of $J$ . Let $\pi$ be obtained from $\pi'$ by removing $k$ and appending it at the end. Then

\pi' \text{ observes the precedence constraints} \;\Longrightarrow\; \pi \text{ observes them.}

In Lawler's proof $\pi' = (A, k, B, k')$ and $\pi = (A, B, k', k)$ ; this is the first of the three steps showing that moving $k$ to the last position never hurts.

Formalization Note $\pi$ is written l.erase k ++ [k] for $\pi' =$ l, which is the page's $(A, B, k', k)$ whenever l = A ++ [k] ++ B ++ [k'], and covers also the case where $k$ is already last.

Preamble

import Mathlib
import Definitions.Def_LawlerPrec_MinMax_IsFeasible
import Definitions.Def_LawlerPrec_MinMax_lastEligible

Formal statement

namespace LawlerPrec.MinMax

/-- §2, proof of the Theorem, p. 544, third paragraph: moving a job `k ∈ S` to the last position
of a sequence `π′ = l` that observes the precedence constraints gives a sequence
`π = l.erase k ++ [k]` that observes them too. When `l = A ++ [k] ++ B ++ [k′]` this `π` is the
page's `A ++ B ++ [k′] ++ [k]`. -/
theorem move_last_feasible {ι : Type*} [DecidableEq ι] (prec : ι → ι → Prop) (J : Finset ι)
    (l : List ι) (k : ι) (hl : IsFeasible prec J l) (hk : k ∈ lastEligible prec J) :
    IsFeasible prec J (l.erase k ++ [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, PROOF, third paragraph

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

§2, proof of the Theorem, p. 544 — moving a job of SSS to the end keeps the precedence constraints

§2, proof of the Theorem, p. 544 — moving a job of $S$ to the end keeps the precedence constraints