§3 Sequencing Algorithm, p. 545 — the backward rule always produces a complete sequence
ProvedLawlerPrec.MinMax.lawler_sequence_existsLet be a finite set of jobs with arbitrary processing times , cost functions and precedence constraints. If some sequence of observes the precedence constraints, then
In other words, the procedure "one simply finds a job which can be placed last … and so on" never stalls: at every stage the set of remaining jobs has a job required to precede none of the others, and among those a job of least cost at the remaining total processing time. This ensures that the optimality statement for the rule's sequences is not vacuous.
Formalization Note No assumption on processing times or costs is needed. "Produced by the rule" is the property IsLawlerSequence of a finished sequence, with arbitrary tie-breaking.
import Mathlib import Definitions.Def_LawlerPrec_MinMax_IsFeasible import Definitions.Def_LawlerPrec_MinMax_IsLawlerSequence
namespace LawlerPrec.MinMax
/-- §3 Sequencing Algorithm, p. 545, first paragraph: the procedure "one simply finds a job `k`
which can be placed last … and so on" never stalls. If some sequence of `J` observes the
precedence constraints, then some sequence of `J` is produced by the backward rule. No
assumption on processing times or costs is needed. -/
theorem lawler_sequence_exists {ι : Type*} [DecidableEq ι] (a : ι → ℝ) (c : ι → ℝ → ℝ)
(prec : ι → ι → Prop) (J : Finset ι) (hfeas : ∃ l : List ι, IsFeasible prec J l) :
∃ l : List ι, MooreLateJobs.Shared.IsSchedule J l ∧ IsLawlerSequence a c prec l := by sorry
end LawlerPrec.MinMax
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.