Lemma 2.2 — $C^P_i = T_i + \sum_{0<\beta\le1}\beta S^P_i(\beta)$

Proved

AvgCompletionSched.BestAlpha.preemptive_completion_decomposition

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

p2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1scheduling

Let $P$ be any preemptive one-machine schedule of an instance with processing times $p_j>0$ and release dates $r_j\ge0$ . Fix a job $J_i$ . Let $T_i$ be the total idle time of $P$ before $C^P_i$ , and let $x_{ij}$ be the fraction of job $J_j$ processed before $C^P_i$ . Then

C^P_i=T_i+\sum_{j} x_{ij}\,p_j .

In the paper's notation, $S^P_i(\beta)$ is the set of jobs $J_j$ with $x_{ij}=\beta$ (and also the sum of their processing times), and the identity reads $C^P_i=T_i+\sum_{0<\beta\le1}\beta S^P_i(\beta)$ : the interval $[0,C^P_i)$ splits into idle time and the pieces of the jobs processed in it.

Formalization Note The sum over $\beta$ is reindexed as a sum over jobs; jobs with $x_{ij}=0$ contribute $0$ . $T_i$ is defined as the Lebesgue measure of the idle times in $[0,C^P_i)$ , not as $C^P_i$ minus the processed amount, so that the identity is not true by definition.

Preamble

import Mathlib
import Definitions.Def_AvgCompletionSched_BestAlpha_Model

Formal statement

namespace AvgCompletionSched.BestAlpha
theorem preemptive_completion_decomposition {n : ℕ} {I : Instance n}
    (P : PreemptiveSchedule I) (i : Fin n) :
    P.CP i = P.idle i + ∑ j, P.frac i j * I.p j := by sorry
end AvgCompletionSched.BestAlpha

Source

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

Read-back

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

Take any number of jobs $n$ and any instance $I$ (processing times $p_j > 0$ , release dates $r_j \ge 0$ ). Take any preemptive schedule $P$ of $I$ and any job $i$ .

The statement asserts that the completion time of $i$ in $P$ splits exactly into idle time plus processing done before it:

C^P_i \;=\; T_i + \sum_{j} x_{ij}\, p_j.

The symbols mean:

$C^P_i$ is the first time by which $p_i$ units of job $i$ have been processed. Formally it is $\inf\{t : \mathrm{done}_i(t)\ge p_i\}$ , where $\mathrm{done}_j(t)$ is the Lebesgue measure of the set of times in $[0,t)$ at which $j$ runs.
$T_i$ is the Lebesgue measure of the set of times in $[0, C^P_i)$ at which the machine is idle.
$x_{ij} = \mathrm{done}_j(C^P_i)/p_j$ is the fraction of job $j$ processed before $C^P_i$ . Hence $x_{ij}\,p_j = \mathrm{done}_j(C^P_i)$ .

The sum runs over all jobs $j$ , including $j = i$ itself.

Degenerate cases. Since a job $i$ is required, $n \ge 1$ . With a single job, the claim reads $C^P_i = T_i + \mathrm{done}_i(C^P_i)$ . No division by zero occurs, because $p_j > 0$ .

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 2.2 — CiP=Ti+∑0<β≤1βSiP(β)C^P_i = T_i + \sum_{0<\beta\le1}\beta S^P_i(\beta)CiP​=Ti​+∑0<β≤1​βSiP​(β)

Lemma 2.2 — $C^P_i = T_i + \sum_{0<\beta\le1}\beta S^P_i(\beta)$