Prove2Me

(4.2) — if ∑jpj>α∑jCj∗\sum_j p_j>\alpha\sum_j C^*_j then ∑jrj≤(1−α)∑jCj∗\sum_j r_j\le(1-\alpha)\sum_j C^*_j

Proved
AvgCompletionSched.ParallelRelease.release_sum_bound

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

approximation-algorithmsp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1scheduling

Let N∗N^* be a feasible nonpreemptive schedule of an instance on mm machines with release dates, with completion times Cj∗C^*_j, and let α\alpha be a real number. If

∑jpj>α∑jCj∗,then∑jrj≤(1−α)∑jCj∗.\sum_j p_j>\alpha\sum_j C^*_j,\qquad\text{then}\qquad\sum_j r_j\le(1-\alpha)\sum_j C^*_j.

This is inequality (4.2). It follows from the simple bound ∑jCj∗≥∑j(pj+rj)\sum_j C^*_j\ge\sum_j(p_j+r_j) and is the case split that lets the analysis of Lemma 4.19 balance list scheduling against Delay List: when the processing times are small relative to the optimum, list scheduling is good; otherwise the release dates are small, which is what Delay List needs.

Preamble
import Mathlib
import Definitions.Def_AvgCompletionSched_ParallelRelease_Model
Formal statement
namespace AvgCompletionSched.ParallelRelease

/-- (4.2): if `∑ p_j > α ∑ C*_j`, then `∑ r_j ≤ (1 - α) ∑ C*_j`. -/
theorem release_sum_bound {n m : ℕ} (I : Instance n m) (Nstar : Schedule I) (α : ℝ)
    (hα : α * ∑ j, Nstar.C j < ∑ j, I.p j) :
    ∑ j, I.r j ≤ (1 - α) * ∑ j, Nstar.C j := by sorry

end AvgCompletionSched.ParallelRelease
Source
Chekuri, Motwani, Natarajan, Stein, Approximation Techniques for Average Completion Time Scheduling, SIAM J. Comput. 31(1), 2001, p. 163, proof of Lemma 4.19, eq. (4.2)
Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let II be an instance with nn jobs, m≥1m\ge1 machines, pj>0p_j>0 and rj≥0r_j\ge0. Let N∗N^* be any feasible nonpreemptive schedule: start times Sj≥rjS_j\ge r_j, and distinct jobs on the same machine do not overlap. Write Cj∗=Sj+pjC^*_j=S_j+p_j.

Let α\alpha be any real number, with no sign or size restriction, such that

α∑jCj∗<∑jpj.\alpha\sum_jC^*_j<\sum_j p_j.

The theorem asserts

∑jrj≤(1−α)∑jCj∗.\sum_j r_j\le(1-\alpha)\sum_j C^*_j.

Degenerate cases.

  • If n=0n=0, the hypothesis reads 0<00<0, which is false, so the statement is vacuous.
  • For n≥1n\ge1 with α≤1\alpha\le 1, the hypothesis can be satisfied. For example, any α≤0\alpha\le0 satisfies it, since ∑jCj∗>0\sum_j C^*_j>0.
  • α\alpha may be negative, in which case the factor 1−α1-\alpha exceeds 11.
Human review

  • Endorsed by Shuze Chen · Sep 27, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Sep 27, 2026

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

View graph