Lemma 4.11 — $C^m_{\mathrm{OPT}} \ge \sum_i w_i\kappa_i = C^\infty_{\mathrm{OPT}}$

Proved

AvgCompletionSched.DelayList.kappa_lower_bound

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

approximation-algorithmsp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1precedence-constraintsscheduling

Let an instance with release dates, positive weights and precedence constraints be given, and let $m$ be a number of machines. Then

every feasible $m$ -machine schedule $S^m$ satisfies

\sum_i w_i\kappa_i\le\sum_i w_iC^m_i ;

with unboundedly many machines the bound is attained: there is a feasible schedule on $n$ machines (one per job) whose sum of weighted completion times equals $\sum_i w_i\kappa_i$ .

Together, since part 1 holds for every number of machines, $\sum_i w_i\kappa_i=C^\infty_{\mathrm{OPT}}$ is the optimum with unboundedly many machines and a lower bound on $C^m_{\mathrm{OPT}}$ .

Formalization Note "Unboundedly many machines" is modelled by $n$ machines, which suffice because a schedule never runs more than $n$ jobs at a time.

Preamble

import Mathlib
import Definitions.Def_AvgCompletionSched_DelayList_Model

Formal statement

namespace AvgCompletionSched.DelayList

/-- Lemma 4.11 (p. 160): `C^m_opt ≥ ∑_i w_i κ_i = C^∞_opt`. Every feasible `m`-machine schedule
has sum of weighted completion times at least `∑_i w_i κ_i`, and with unboundedly many machines
(`n` machines suffice) there is a feasible schedule whose sum of weighted completion times equals
`∑_i w_i κ_i`. -/
theorem kappa_lower_bound {n m : ℕ} (I : Instance n) :
    (∀ N : Schedule I m, ∑ i, I.w i * kappa I i ≤ N.wct) ∧
    ∃ N : Schedule I n, N.wct = ∑ i, I.w i * kappa I i := by sorry

end AvgCompletionSched.DelayList

Source

Chekuri, Motwani, Natarajan, Stein, Approximation Techniques for Average Completion Time Scheduling, SIAM J. Comput. 31(1), 2001, p. 160, Lemma 4.11

Read-back

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

Hypotheses. Take any instance with $n$ jobs and any natural number $m$ (no lower bound).

Conclusion. Both of the following hold.

Every feasible schedule $N$ on $m$ machines satisfies

\sum_i w_i \kappa_i \;\le\; \sum_i w_i C^N_i.

There is a feasible schedule $N$ on exactly $n$ machines (one per job) with

\sum_i w_i C^N_i = \sum_i w_i \kappa_i.

Here $\kappa_i$ is defined recursively: $p_i + \max(\max_{h \prec i}\kappa_h, r_i)$ if $i$ has predecessors, and $p_i + r_i$ otherwise.

Degenerate cases.

If $m = 0$ and $n \ge 1$ , part 1 is vacuous (no schedule exists).
If $n = 0$ , both sums are $0$ and both parts are trivial.

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

Lemma 4.11 — COPTm≥∑iwiκi=COPT∞C^m_{\mathrm{OPT}} \ge \sum_i w_i\kappa_i = C^\infty_{\mathrm{OPT}}COPTm​≥∑i​wi​κi​=COPT∞​

Lemma 4.11 — $C^m_{\mathrm{OPT}} \ge \sum_i w_i\kappa_i = C^\infty_{\mathrm{OPT}}$