Bounded costs give a level $y>0$ at which $S_D(y)$ has no late jobs

Proved

MooreLateJobs.MaxDeferral.bounded_exists_feasible_level

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

p2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1schedulingsingle-machine

Let $J$ be a finite set of jobs with processing times $t_j\ge 0$ and continuous, bounded, non-decreasing deferral costs $P_j$ . For each $y>0$ let $S_D(y)$ be a schedule of $J$ ordered by non-decreasing due-dates $D_j=P_j^*(y)$ (ties broken arbitrarily). Then

\exists\, y>0:\quad S_D(y) \text{ has no late jobs, i.e. } C_j\le P_j^*(y) \text{ for every job } j.

This supplies the feasible level from which the least feasible level $y^*$ is obtained.

Formalization Note The family $y\mapsto S_D(y)$ is an arbitrary one satisfying the ordering condition for every $y>0$ , so every tie-break is covered. $t_j\ge0$ is added (processing times are durations).

Preamble

import Mathlib
import Definitions.Def_MooreLateJobs_Shared_completionTime
import Definitions.Def_MooreLateJobs_MaxDeferral_NoLateAt

Formal statement

namespace MooreLateJobs.MaxDeferral

theorem bounded_exists_feasible_level {ι : Type*} [DecidableEq ι] (J : Finset ι) (t : ι → ℝ)
    (P : ι → ℝ → ℝ) (ht : ∀ i ∈ J, 0 ≤ t i)
    (hcont : ∀ i ∈ J, Continuous (P i)) (hbdd : ∀ i ∈ J, ∃ M, ∀ s, |P i s| ≤ M)
    (hmono : ∀ i ∈ J, Monotone (P i)) (SD : ℝ → List ι)
    (hSD : ∀ y, 0 < y →
      Shared.IsSchedule J (SD y) ∧ (SD y).Pairwise (fun a b => Pstar (P a) y ≤ Pstar (P b) y)) :
    ∃ y, 0 < y ∧ NoLateAt t P y (SD y) := by sorry

end MooreLateJobs.MaxDeferral

Source

Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1), 1968, pp. 108-109, "Minimizing the Maximum Deferral Cost" ("In that the P_i's are bounded, there always exists y > 0 such that S_D(y) has no "late" jobs")

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Bounded costs give a level y>0y>0y>0 at which SD(y)S_D(y)SD​(y) has no late jobs

Bounded costs give a level $y>0$ at which $S_D(y)$ has no late jobs