$P^*$ is non-decreasing for a continuous non-decreasing cost

Proved

MooreLateJobs.MaxDeferral.Pstar_monotone

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

generalized-inversep2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1scheduling

Let $f:\mathbb R\to\mathbb R$ be continuous and non-decreasing, and let $P^*$ be its generalized inverse (times $s\ge 0$ ; values in $\mathbb R\cup\{+\infty\}$ ). Then $P^*$ is non-decreasing:

y_1\le y_2 \implies P^*(y_1)\le P^*(y_2).

This is the step of Moore's argument that makes the feasibility of the due-date schedule $S_D(y)$ monotone in the cost level $y$ .

Formalization Note The paper's costs are also bounded; boundedness is not needed here and is not assumed (a stronger statement). Continuity is assumed, as in the paper; without it the claim can fail.

Preamble

import Mathlib
import Definitions.Def_MooreLateJobs_MaxDeferral_Pstar

Formal statement

namespace MooreLateJobs.MaxDeferral

theorem Pstar_monotone (f : ℝ → ℝ) (hcont : Continuous f) (hmono : Monotone f) :
    Monotone (Pstar f) := 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, p. 109, first paragraph ("Since the P_i's are monotonically non-decreasing, the P_i*'s are monotonically non-decreasing")

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

P∗P^*P∗ is non-decreasing for a continuous non-decreasing cost

$P^*$ is non-decreasing for a continuous non-decreasing cost