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

Proved

AvgCompletionSched.InTree.kappa_lower_bound

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

lower-boundsp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1scheduling

Let an in-tree instance without release dates be given, and let $\kappa_i$ be the critical-path length of job $i$ (Definition 4.1). Then:

for every number $m$ of machines, every feasible nonpreemptive $m$ -machine schedule $N$ satisfies

\sum_i w_i\kappa_i\le \sum_i w_i C^N_i ,

so $C^m_{\mathrm{OPT}}\ge\sum_i w_i\kappa_i$ ; 2. with unboundedly many machines the value $\sum_i w_i\kappa_i$ is attained: some feasible schedule on $n$ machines (as many machines as jobs, which is as good as unboundedly many) has $\sum_i w_i C^N_i=\sum_i w_i\kappa_i$ . Together with part 1 this is the equality $\sum_i w_i\kappa_i=C^\infty_{\mathrm{OPT}}$ .

Part 1 is the second lower bound used in Theorem 4.17.

Formalization Note The optimum is not formed as an infimum: part 1 is stated against every feasible schedule, and $C^\infty_{\mathrm{OPT}}$ is rendered as "attained on $n$ machines" (no schedule on any number of machines does better, by part 1).

Preamble

import Mathlib
import Definitions.Def_AvgCompletionSched_InTree_Model

Formal statement

namespace AvgCompletionSched.InTree

/-- Lemma 4.11 (p. 160): `C^m_opt ≥ ∑_i w_i κ_i = C^∞_opt`. First part: every feasible schedule
on any number `m` of machines has value at least `∑_i w_i κ_i`. Second part (the equality with
`C^∞_opt`): with unboundedly many machines (`n` machines suffice for `n` jobs) the value
`∑_i w_i κ_i` is attained, so together with the first part it is the optimum. -/
theorem kappa_lower_bound {n : ℕ} (I : Instance n) :
    (∀ (m : ℕ) (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.InTree

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

Undefined names. The statement uses four names from the imported module Definitions.Def_AvgCompletionSched_InTree_Model, and their definitions are not shown here:

$\mathrm{Instance}(n)$ , a type of problem instances indexed by a natural number $n$ ;
$\mathrm{Schedule}(I, m)$ , a type of objects built from an instance $I$ and a natural number $m$ ;
$\kappa_I(i)$ , a quantity attached to each index $i$ of an instance $I$ ;
$\mathrm{wct}(N)$ , a numerical value attached to each schedule $N$ .

This read-back therefore cannot say what an instance or a schedule is, what makes a schedule feasible, how $\kappa$ is computed, or what number type the values live in. Everything below holds only as far as those hidden definitions give it meaning.

The names suggest a reading: $n$ jobs forming an in-tree, $m$ machines, weights $w_i$ , and weighted total completion time. The documentation comment also describes the theorem as "Lemma 4.11 (p. 160)", with $\sum_i w_i\kappa_i = C^\infty_{\mathrm{opt}}$ . Both are suggestions only. The comment is not part of the formal assertion, and the code itself never defines or mentions an optimum $C^m_{\mathrm{opt}}$ or $C^\infty_{\mathrm{opt}}$ .

Setting. Fix:

a natural number $n$ ;
an instance $I$ of type $\mathrm{Instance}(n)$ .

The instance provides a weight $w_i$ for each index $i$ , and the sum runs over every index $i$ of that index type. Judging by the sums, the index type is finite, presumably with $n$ elements, but the code does not show this. Write

K(I) \;=\; \sum_{i} w_i \,\kappa_I(i).

Claim. The theorem asserts both of the following.

Lower bound. For every natural number $m$ and every schedule $N$ of type $\mathrm{Schedule}(I, m)$ ,

K(I) \;\le\; \mathrm{wct}(N).

The inequality is non-strict.

Attainment with exactly $n$ machines. There exists a schedule $N$ of type $\mathrm{Schedule}(I, n)$ , where the second parameter is the same $n$ that indexes the instance, such that

\mathrm{wct}(N) \;=\; K(I).

The statement makes no other claim. In particular:

It does not say that schedules with fewer than $n$ machines can reach $K(I)$ .
It does not say that the schedule in part 2 is unique.
It does not name $K(I)$ as the minimum of anything. That follows only by combining the two parts: over all schedules of type $\mathrm{Schedule}(I, n)$ , the least value of $\mathrm{wct}$ exists and equals $K(I)$ .

Degenerate cases.

$n = 0$ . If the index type is then empty, $K(I)$ is the empty sum $0$ . Part 1 becomes $0 \le \mathrm{wct}(N)$ for every schedule on any number of machines. Part 2 then requires a schedule with $0$ machines whose value is exactly $0$ . Whether such a schedule exists depends on the hidden definition of $\mathrm{Schedule}$ . If none exists, the theorem is false for $n = 0$ rather than vacuous.
$m = 0$ in part 1. The claim covers schedules with zero machines. If $\mathrm{Schedule}(I, 0)$ has no elements (for $n \ge 1$ , say), that instance of part 1 is vacuous. If it does have elements, each one must satisfy the bound.
Empty schedule types in general. If $\mathrm{Schedule}(I, m)$ is empty for some $m$ , part 1 says nothing about that $m$ .
Other effects of the hidden definitions. Nothing here can be judged from the code shown: whether $w_i$ may be zero or negative, and whether $\kappa$ or $\mathrm{wct}$ involve subtraction in $\mathbb{N}$ , division, or other operations that return a default value on bad inputs.

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}}$