Scheduling Theory

Motivation

Single-machine scheduling with precedence constraints, written $1|\mathrm{prec}|\sum w_jC_j$ in the notation of Graham et al., asks for an order of $n$ weighted jobs on one machine that respects a given partial order and minimizes the weighted sum of completion times. The problem is strongly NP-hard (Lawler 1978; Lenstra and Rinnooy Kan 1978), and closing its approximability gap is listed by Schuurman and Woeginger among ten outstanding open problems in scheduling theory. Several 2-approximation algorithms are known (Schulz 1996; Hall et al. 1997; Chudak and Hochbaum 1999; Chekuri and Motwani 1999; Margot et al. 2003).

A line of work by Chudak and Hochbaum, Correa and Schulz, and Ambühl and Mastrolilli showed that the problem is a special case of minimum weighted vertex cover in a graph built from the precedence order. Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) observed that this graph is the graph of incomparable pairs of dimension theory, and used that identification to obtain $(2-2/f)$-approximations for orders of fractional dimension at most $f$. This mission formalizes that framework: the identification of the two graphs and the rounding guarantee of the paper's Theorem 5.1.

Setting

An instance $S$ consists of a finite set $N$ of jobs, a partial order $P$ on $N$ (reflexive, antisymmetric, transitive; $(i,j)\in P$ with $i\ne j$ means job $i$ finishes before job $j$ starts), processing times $p_j\ge 0$ and weights $w_j\ge 0$.

Two jobs $x,y$ are incomparable, $x\parallel y$, when neither $(x,y)$ nor $(y,x)$ lies in $P$. The set $\operatorname{inc}(P)$ of incomparable pairs consists of ordered pairs and is closed under swapping. A linear extension of $P$ is a linear order $L\supseteq P$ on $N$; it reverses $(x,y)\in\operatorname{inc}(P)$ when $y<x$ in $L$. A nonempty multiset $L_1,\dots,L_t$ of linear extensions is a $k:t$-realizer if every incomparable pair is reversed by at least $k$ of them. The fractional dimension $\operatorname{fdim}(P)$ is the least ratio $t/k$ over all $k:t$-realizers.

The vertex cover graph $G^S_P$ has the incomparable pairs as nodes; nodes $(i,j)$ and $(k,\ell)$ are adjacent if $j=k$ and $i=\ell$, or $j=k$ and $(i,\ell)\in P$, or $(i,\ell),(k,j)\in P$ (symmetrically closed). Node $(i,j)$ has weight $w_{(i,j)}=p_iw_j$, and $w(C)=\sum_{u\in C}w_u$. $\mathrm{OPT}$ is the minimum weight of a vertex cover of $G^S_P$. The LP relaxation [CS-LP] asks for $x\in[0,1]^{\operatorname{inc}(P)}$ with $x_u+x_v\ge1$ on every edge, minimizing $\sum_u w_ux_u$. For a solution $x$ write $V_a=\{u: x_u=a\}$, and for a linear extension $L$ let $I_{1/2}(L)$ be the pairs of $V_{1/2}$ reversed in $L$.

The graph of incomparable pairs $G_P$ (Felsner and Trotter 2000) also has the incomparable pairs as vertices; two of them are adjacent when the pair of them is a minimal set of incomparable pairs that no linear extension reverses entirely.

Formalization targets

Goal: Theorem 5.1 (p. 658)

For an instance $S$, a $k:t$-realizer $L_1,\dots,L_t$ of $P$, and a half-integral optimal solution $x$ of [CS-LP], put $C_i=V_1\cup\bigl(V_{1/2}\setminus I_{1/2}(L_i)\bigr)$. Then every $C_i$ is a vertex cover of $G^S_P$, and

$$\frac1t\sum_{i=1}^t w(C_i)\;\le\;\Bigl(2-\frac{2}{t/k}\Bigr)\mathrm{OPT}.$$

Milestones

• Proposition 3.2 (p. 657): $G^S_P=G_P$.
• Footnote 4 (p. 659): the pairs reversed by a linear extension are independent in $G^S_P$.
• Eq. (4): $\frac1t|\{i: L_i\text{ reverses }u\}|\ge k/t$ for every incomparable pair $u$.
• Eq. (5): $\frac1t\sum_i w(I_{1/2}(L_i))\ge \frac kt\,w(V_{1/2})$.
• Hochbaum's observation (§5, p. 659): for half-integral feasible $x$, $V_1\cup C$ covers $G^S_P$ whenever $C$ covers $G^S_P[V_{1/2}]$.
• Eqs. (6)–(8): $\frac1t\sum_iw(C_i)\le w(V_1)+(1-\frac kt)w(V_{1/2})\le 2(1-\frac kt)(w(V_1)+\frac12w(V_{1/2}))\le(2-\frac2{t/k})\mathrm{OPT}$ when $P$ is not a linear order.

Significance

The result. Combined with the cited Theorem 2.1 (Ambühl–Mastrolilli 2009; Correa–Schulz 2005), which turns an $\alpha$-approximate vertex cover of $G^S_P$ into an $\alpha$-approximate schedule, Theorem 5.1 gives a $(2-2/f)$-approximation for $1|\mathrm{prec}|\sum w_jC_j$ whenever the precedence order has an efficiently samplable realizer with $t/k\le f$. The paper applies it to interval orders ($3/2$), convex bipartite orders and semiorders ($4/3$), orders of bounded degree and orders of interval dimension two; for the earlier special classes it matched or improved the best known ratios, and for the last two it gave the first results. Proposition 3.2 makes the dimension theory of posets (realizers, critical pairs, fractional dimension) directly available to the vertex cover approach.

Formalizing it. The results are proved in the paper; to the best of current knowledge none of them has a machine-checked proof. The mission produces a Lean development of incomparable pairs, linear extensions, $k$-fold realizers and the hypergraph of incomparable pairs, which other dimension-theory missions can reuse, and a verified LP-rounding argument for half-integral vertex cover solutions under a distribution of independent sets.

Difficulty

Most of the rounding argument is arithmetic over finite sums. The central nontrivial step is the inclusion $G_P\subseteq G^S_P$ in Proposition 3.2: for two incomparable pairs that are not adjacent under the three-case rule, one must construct a single linear extension reversing both. This needs an extension of $P$ by two new comparabilities whose transitive closure is still antisymmetric, followed by Szpilrajn's theorem; checking that every potential cycle is excluded by the three cases is the actual content. The opposite inclusion, and footnote 4, follow from transitivity and antisymmetry of linear orders. A second point of care is the inequality $t\ge 2k$ used in step (7): it is not part of the definition of a realizer, and follows from each linear extension reversing exactly one of $(x,y)$ and $(y,x)$.

Formalization scope

• Jobs form a finite type N; the precedence order is a relation P : N → N → Prop with IsPartialOrder, carried by the structure Instance. Processing times and weights are nonnegative reals.
• $\operatorname{inc}(P)$ is the subtype IncPair P of N × N; a linear extension is a relation with IsLinearOrder containing P; a $k:t$-realizer is a family Fin t → LinearExtension P with $t>0$. Reversal of $(x,y)$ means $y<x$ in $L$ throughout; the page's "$y>x$" in Eq. (4) and "$\mathrm{Prob}[j>i]$" in Eq. (5) are the same family of inequalities because $\operatorname{inc}(P)$ is symmetric.
• $G^S_P$ is the symmetric closure of the printed three-case rule on distinct nodes. $G_P$ is defined through linear extensions and hyperedge minimality, never through the three-case rule, so Proposition 3.2 is a genuine statement and not a definitional equality.
• [CS-LP] drops the constant term $\sum_jp_jw_j+\sum_{(i,j)\in P}p_iw_j$ of [CS-IP], which does not affect optimality. $\mathrm{OPT}$ is the minimum weight of a vertex cover of $G^S_P$, taken over a finite nonempty family.
• Not formalized: "efficiently samplable", "polynomial time" and "randomized algorithm". The expectation over a uniformly sampled $L_i$ is stated as the average $\frac1t\sum_{i=1}^t$, which is equivalent to it and stronger than the existence of one good index. The existence of a half-integral optimal [CS-LP] solution (Nemhauser–Trotter, cited) is a hypothesis on $x$. The conversion of a vertex cover into a schedule (Theorem 2.1, cited) is not formalized; the goal is stated for vertex covers of $G^S_P$.
• Constants: $2-2/(t/k)$ in real arithmetic; it equals $2-2k/t$, and equals $2$ when $k=0$.
• The paper assumes $\operatorname{fdim}(P)\ge2$, i.e. $P$ is not a linear order. Eqs. (6)–(8) carry that hypothesis as the paper does; the goal omits it because for a linear order both sides are $0$.
• Conclusion (a), that each $C_i$ is a vertex cover, is part of the goal and is not assumed.

Contributions welcome: proofs of the milestones in any order, and a reusable Szpilrajn-style lemma producing a linear extension that reverses a prescribed set of compatible incomparable pairs.

Selected references

• C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the approximability of single-machine scheduling with precedence constraints, Math. Oper. Res. 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
• C. Ambühl, M. Mastrolilli, Single machine precedence constrained scheduling is a vertex cover problem, Algorithmica 53(4), 2009 (reference [2] of the paper).
• J. R. Correa, A. S. Schulz, Single-machine scheduling with precedence constraints, Math. Oper. Res. 30(4):1005–1021, 2005. https://doi.org/10.1287/moor.1050.0158
• G. R. Brightwell, E. R. Scheinerman, Fractional dimension of partial orders, Order 9(2):139–158, 1992 (reference [7]).
• S. Felsner, W. T. Trotter, Dimension, graph and hypergraph coloring, Order 17(2):167–177, 2000 (reference [13]).
• D. S. Hochbaum, Efficient bounds for the stable set, vertex cover and set packing problems, Discrete Appl. Math. 6(3):243–254, 1983 (reference [20]).
• G. L. Nemhauser, L. E. Trotter, Vertex packings: structural properties and algorithms, Math. Programming 8(1):232–248, 1975 (reference [29]).

Motivation

The problem $1\,|\,\mathrm{prec}\,|\,\sum w_jC_j$ asks for a single-machine sequence of jobs, respecting precedence constraints, that minimizes the weighted sum of completion times. It has been known to be strongly NP-hard since Lawler (1978) and Lenstra and Rinnooy Kan (1978), several different 2-approximation algorithms are known, and closing the approximability gap is listed by Schuurman and Woeginger (1999) as one of ten outstanding open problems in scheduling theory. Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) give the first inapproximability result for this problem: under a widely believed complexity assumption it has no polynomial-time approximation scheme (PTAS). The bridge to that result is a quantitative link, Lemma 9.1, between the optimal value of a special bipartite scheduling instance and the maximum edge biclique of a bipartite graph, a problem whose hardness of approximation was established by Ambühl, Mastrolilli and Svensson (FOCS 2007). This mission formalizes that link.

Setting

A schedule of a finite job set is a sequence $\sigma$ listing every job once; the machine processes the jobs in that order from time $0$ without idle time or pre-emption. Job $j$ has a processing time $p_j$ and a weight $w_j$; its completion time $C_j$ is the sum of the processing times of the jobs up to and including $j$, and the value of $\sigma$ is $\mathrm{val}(\sigma)=\sum_j w_jC_j$. Precedence constraints are a relation $P$ on jobs: $(i,j)\in P$ with $i\ne j$ means job $i$ must be completed before job $j$ starts. A schedule respecting all of them is feasible, and a feasible schedule $\sigma^*$ of least value is optimal.

Let $G=(U,V,E)$ be an $n$-by-$n$ bipartite graph: $|U|=|V|=n$ and $E\subseteq U\times V$. An edge biclique is a pair $A\subseteq U$, $B\subseteq V$ with $A\times B\subseteq E$, of value $|A|\cdot|B|$; the maximum edge biclique problem (Definition 9.1) asks for one of largest value. The bipartite scheduling instance $S_G$ has jobs $U\cup V$ and precedence constraints

$$P=(U\times V)\setminus E,$$

so $u\in U$ must precede $v\in V$ exactly when $(u,v)$ is not an edge. Jobs of $U$ have $p=1$, $w=0$; jobs of $V$ have $p=0$, $w=1$. Thus $\mathrm{val}(\sigma)=\sum_{v\in V}C_v$, where $C_v$ is the number of $U$-jobs scheduled before $v$. For $i\ge1$, $\sigma(i)$ denotes the number of $V$-jobs scheduled before $i$ jobs of $U$ have been scheduled.

In the Lean development these are weightedCompletion, IsOptimalSchedule, IsEdgeBiclique, maxBicliqueValue, precSG, procSG, weightSG, valSG, IsOptimalSG and vBefore in the namespace SingleMachinePrec.Biclique.

Formalization targets

Goal: Lemma 9.1 (p. 666)

If a maximum edge biclique of $G$ has value $an^2$ with $a\in(0,1]$, then $S_G$ has an optimal schedule and every optimal schedule $\sigma^*$ satisfies

$$n^2-an^2\Bigl(\ln\frac1a+2\Bigr)\le\mathrm{val}(\sigma^*)\le n^2-an^2 .$$

Milestones (proof of Lemma 9.1, §9, p. 666)

1. For every edge biclique $(A,B)$, a schedule in the block order $U\setminus A\to B\to A\to V\setminus B$ exists, and every such schedule is feasible with

$$\mathrm{val}(\sigma)=n^2-|A|\cdot|B| .$$

2. For every schedule, $\sigma(n+1)=n$ and

$$\mathrm{val}(\sigma)=\sum_{i=1}^n\bigl(\sigma(i+1)-\sigma(i)\bigr)i=n^2-\sum_{i=1}^n\sigma(i).$$

3. For every feasible schedule and $i=1,\dots,n$,

$$\sigma(i)(n-i+1)\le an^2,\qquad \sigma(i)\le n .$$

Significance

Lemma 9.1 shows that the optimal value of $S_G$ determines the maximum edge biclique of $G$ up to a factor of order $\ln(1/a)$ in the "area above the work line" $n^2-\mathrm{val}(\sigma^*)$. Combined with the hardness of approximating maximum edge biclique (Theorem 9.1, cited from Ambühl, Mastrolilli and Svensson 2007) it yields Theorem 9.2: $1\,|\,\mathrm{prec}\,|\,\sum w_jC_j$ has no PTAS unless SAT can be decided by a probabilistic algorithm in time $2^{N^\epsilon}$ for every $\epsilon>0$. It also makes precise the two-dimensional Gantt chart picture of Eastman, Even and Isaacs (1964) and of Goemans and Williamson (2000), in which every point on the work line of a schedule defines an edge biclique.

The lemma is proved in the paper; it is not formalized anywhere to our knowledge. A formal proof certifies the combinatorial core of the no-PTAS result independently of the complexity-theoretic layer, and its definitions (the bipartite instance $S_G$, edge bicliques, the profile $\sigma(i)$) are reusable for the gap inequality behind Theorem 9.2.

Difficulty

The upper bound is a direct computation on one explicit schedule. The lower bound is a statement about every feasible schedule, of which there are exponentially many, and it must hold with the explicit constant $2$ and the factor $\ln(1/a)$ for every $a\in(0,1]$. The printed argument splits the sum at $i=(1-a)n$ and uses $\lfloor an\rfloor$, treating $an$ as an integer; for general $a$ (for example $n=3$, value $2$, $an=2/3$) the split point is not an integer, so the printed estimate does not apply verbatim and the constant $2$ has to be re-checked for non-integral $an$. On the formal side, the value identity requires relating completion times in a list to counting $U$-jobs before each $V$-job, with ties among zero-length jobs.

Formalization scope

Jobs are the disjoint union U ⊕ V of two finite types with Fintype.card U = Fintype.card V = n; $E$ is a relation U → V → Prop. A schedule is a duplicate-free list containing every job; feasibility is the published LawlerPrec.MinMax.IsFeasible and completion times are the published MooreLateJobs.Shared.completionTime (time $0$ start, no idle time). Processing times and weights are reals, here in $\{0,1\}$. The maximum edge biclique value is the maximum of $|A|\cdot|B|$ over all edge bicliques, the empty ones included, so the hypothesis $a>0$ means $E\ne\emptyset$. The logarithm is natural (Real.log).

Conventions and readings committed to:

• The goal is stated for every optimal schedule, and the existence of an optimal schedule is a separate conclusion, so the bounds cannot hold vacuously. Proving the bounds for one particular schedule, or for an optimal value defined as an infimum that could be a junk default, would not be this lemma.
• No integrality hypothesis on $an$ is added.
• Milestones 2 and 3 are stated for every schedule (respectively every feasible schedule), not only for $\sigma^*$; milestone 1 states the value of the block-order schedule as an equality, where the paper writes "$\le\cdots=$".
• The paper's $P=(U\times V)\setminus E$ is irreflexive; feasibility only constrains distinct jobs, so it agrees with the reflexive partial order of §1.

Not formalized: Theorem 9.1 (cited hardness of maximum edge biclique) and Theorem 9.2 (no PTAS under a complexity assumption); no polynomial-time or complexity-theoretic statement appears in the mission. Contributions welcome: proofs of the three milestones and of the goal; Mathlib's bounds on harmonic numbers (Mathlib/NumberTheory/Harmonic/Bounds.lean) are the relevant library.

Selected references

• C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the Approximability of Single-Machine Scheduling with Precedence Constraints, Mathematics of Operations Research 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
• C. Ambühl, M. Mastrolilli, O. Svensson, Inapproximability results for sparsest cut, optimal linear arrangement, and precedence constraint scheduling, Proc. 48th IEEE FOCS, 329–337, 2007 (reference [4] of the paper).
• W. L. Eastman, S. Even, I. M. Isaacs, Bounds for the optimal scheduling of n jobs on m processors, Management Science 11(2):268–279, 1964 (reference [11]).
• M. X. Goemans, D. P. Williamson, Two-dimensional Gantt charts and a scheduling algorithm of Lawler, SIAM J. Discrete Math. 13(3):281–294, 2000 (reference [15]).
• P. Schuurman, G. J. Woeginger, Polynomial time approximation algorithms for machine scheduling: ten open problems, J. Scheduling 2(5):203–213, 1999 (reference [36]).

Scheduling precedence-constrained jobs on machines of different speeds

Graham (1966) showed that list scheduling finds a schedule within a factor $2$ of optimal for precedence-constrained jobs on identical parallel machines, the first performance guarantee for an approximation algorithm. When the machines run at different speeds (uniformly related machines), the same analysis breaks down, and for two decades the problem $Q|prec|C_{\max}$ resisted a guarantee independent of the speeds better than $O(\sqrt m)$.

Timeline:

• 1974, Liu and Liu: list scheduling on machines of different speeds, with a guarantee that depends on the speeds and can be arbitrarily large even for a fixed number of machines.
• 1980, Jaffe: list scheduling on the machines whose speed is within a factor $\sqrt m$ of the fastest gives an $O(\sqrt m)$-approximation.
• 1978, Lenstra and Rinnooy Kan: with precedence constraints, no $\rho$-approximation with $\rho < 4/3$ exists unless P = NP. This bound already holds for identical machines.
• 1997–1999, Chudak and Shmoys: an LP-guided variant of list scheduling achieves $O(\log m)$, and $K + 2\sqrt K + 1$ when there are only $K$ distinct speeds (J. Algorithms 30 (1999) 323–343; conference version SODA 1997).

The mission formalizes the makespan half of that paper, up to its Theorem 3.7.

Setting

An instance has $n$ jobs and $m \ge 1$ machines. Job $j$ requires $p_j > 0$ units of processing, and machine $i$ runs at speed $s_i > 0$, so job $j$ takes $p_j/s_i$ time units on machine $i$. A strict partial order $\prec$ on the jobs gives precedence constraints: $j \prec k$ means that job $k$ may not start until job $j$ has completed.

A schedule runs each job $j$ without interruption on one machine $\mu(j)$, from a start time $S_j \ge 0$ to its completion time $C_j = S_j + p_j/s_{\mu(j)}$. A machine processes at most one job at a time, and $j \prec k$ forces $C_j \le S_k$. Its length is $C_{\max} = \max_j C_j$. $C^*_{\max}$ is the length of an optimal schedule.

Let $\bar s_1 > \bar s_2 > \cdots > \bar s_K$ be the distinct speeds and $m_k$ the number of machines of speed $\bar s_k$. An assignment $k(j)$ names the speed class at which job $j$ is to run. Its loads are $D_k = \frac{1}{m_k}\sum_{j:k(j)=k} p_j/\bar s_k$, and its chain bound $C$ is the largest value of $\sum_{j\in\mathcal C} p_j/\bar s_{k(j)}$ over chains $\mathcal C$ of $\prec$. Speed-based list scheduling is Graham's rule restricted by the assignment: whenever a machine of speed $\bar s_k$ is idle, it starts the first available job $j$ on the list with $k(j) = k$.

The linear program LP has variables $x_{kj} \ge 0$, $C_j$ and $D$. It minimizes $D$ subject to the following constraints:

• $\sum_k x_{kj} = 1$;
• $\frac{1}{m_k\bar s_k}\sum_j p_j x_{kj} \le D$;
• $\sum_k (p_j/\bar s_k)x_{kj} \le C_j$, and $\sum_k (p_j/\bar s_k)x_{kj} \le C_j - C_{j'}$ whenever $j' \prec j$;
• $C_j \le D$.

From a solution, with $\bar p_j = \sum_k (p_j/\bar s_k)x_{kj}$, the assignment algorithm gives each job $j$ the speed class $k \notin B_j = \{k : p_j/\bar s_k > \gamma\bar p_j\}$ of largest capacity $\bar s_k m_k$.

Formalization targets

Goal: Theorem 3.7 (p. 10)

There is an absolute constant $c$ such that for every instance with $m \ge 2$ machines and $K$ distinct speeds, the better of the two schedules below has length at most

$$\min\bigl\{K + 2\sqrt K + 1,\ 1.89\log_2 m + c\sqrt{\log_2 m}\bigr\}\cdot C^*_{\max}.$$

• (A) An optimal LP solution, the assignment algorithm with $\gamma = \sqrt K + 1$, and speed-based list scheduling.
• (B) The same algorithm run on speeds rounded down to powers of $e$, with machines slower than $\bar s_1/(m\log_2 m)$ dropped, and read back on the original machines.

Milestones, in proof order

• Existence of speed-based list schedules (p. 4).
• Theorem 2.1: $C_{\max} \le C + \sum_k D_k$.
• The LP lower bound $\bar D \le C^*_{\max}$ (p. 6).
• Lemmas 3.1–3.4: chain bounds $2\bar D$ and $(\sqrt K + 1)\bar D$, and load bounds $2K\bar D$ and $(K + \sqrt K)\bar D$.
• Theorem 3.5 and Corollary 3.6: the factor $K + 2\sqrt K + 1$ against $C^*_{\max}$ and against $\bar D$.
• Rounded schedules serve the original instance (p. 9).
• The speed rounding: at most $\lfloor\log_\beta(\alpha m)\rfloor + 1$ speeds, and the LP value grows by a factor of at most $\beta(1 + 1/\alpha)$ (p. 10).
• The "In fact" form of the guarantee, relative to any feasible LP solution (p. 10).

Significance

The result gives the first $O(\log m)$ guarantee for $Q|prec|C_{\max}$, independent of the speeds, and a guarantee depending only on the number of distinct speeds. Through the batching technique of Shmoys, Wein and Williamson it extends to release dates (Corollary 3.8). Since LP also relaxes the preemptive problem, it gives an $O(\log m)$ bound on the ratio between the nonpreemptive and preemptive optima (Corollaries 3.9, 3.10). The "In fact" form, relative to an arbitrary feasible LP solution, drives the paper's $\sum w_jC_j$ algorithm in §4.

The result is proved in the literature but, as far as is known, not formalized. A formal proof requires machine-checking the following:

• the continuous-time list-scheduling argument for different speeds;
• the filtering argument of Lin and Vitter;
• the reduction to logarithmically many speeds, including the off-by-one count of rounded speeds that the page leaves implicit.

Later work gave a combinatorial $O(\log m)$-approximation (Chekuri and Bender, 2001) and an $O(\log m/\log\log m)$-approximation (Li, 2017). These are not part of this mission.

Difficulty

Graham's argument has two lower bounds:

1. the total processing along a chain;
2. the time during which every machine is busy.

With different speeds, the first bound fails: a chain may have been run on slow machines, and its length then says nothing about $C^*_{\max}$. Forcing every job onto a fast machine repairs chains but can leave most machines idle, so the second bound fails. The paper only guarantees that all machines of one speed are busy at each moment of an idle period. Making this pay off requires an assignment that controls chain lengths and per-class loads simultaneously. That assignment is the delicate part: Theorem 2.1 is the bookkeeping, while Lemmas 3.2 and 3.4 rely on the LP. Two of the formal steps are routine on paper but fiddly in Lean: time-interval accounting over a continuous-time schedule, and the counting of rounded speed classes.

Formalization scope

• Representation. Jobs are Fin n and machines Fin m with $m \ge 1$. $p_j > 0$ and $s_i > 0$. $\prec$ is a strict partial order, and a chain is a finite set of pairwise comparable jobs. $C_{\max}$ is the maximum completion time, or $0$ with no jobs.
• Speed classes. The classes are computed from the speeds, so $m_k \ge 1$ and $\bar s_k > 0$ by construction. The Lean index $0$ is the paper's fastest class $\bar s_1$.
• The algorithm as predicates. Speed-based list scheduling is the predicate the proof of Theorem 2.1 uses: jobs run at their assigned speed, and no machine of a job's speed idles while that job is available and unstarted. Every list order and every order of idle machines satisfies it. The assignment algorithm is a predicate allowing every maximizer, since the page does not break ties. Theorems 3.5 and 3.7 quantify over all optimal LP solutions, all such assignments and all such schedules. Existence is supplied by the milestones.
• Comparator. The bound is stated against every feasible schedule of the same instance, never against the LP value or a best schedule of the rounded instance. A statement asserting only that some good schedule exists would be trivially true (the optimum witnesses it); the goal bounds the schedule the algorithm returns.
• Constants and logarithms. $\log m$ is $\log_2 m$, as the paper specifies. $m \ge 2$ is assumed in Theorem 3.7 and in the "In fact" remark, which are asymptotic in $m$. The $O(\sqrt{\log m})$ term is one absolute constant $c$, quantified before the instance, and $1.89$ is the page's number.
• Generalizations and corrections. Lemmas 3.1–3.4 are stated for every feasible LP solution, since their proofs use only feasibility. The speed rounding is relative to $\bar s_1$, with no normalization. The count of rounded speeds is $\lfloor\log_\beta(\alpha m)\rfloor + 1$; the page writes $\log_\beta(\alpha m)$.
• Not formalized. Polynomial running time is not formalized.
• Out of scope. Corollaries 3.8–3.10, Theorem 3.11 and §4 are excluded.

Proofs of any milestone are welcome. Reusable beyond this mission are the following: the model of nonpreemptive schedules on uniformly related machines with precedence, the speed-based list-scheduling predicate with Theorem 2.1, and the LP.

Selected references

• F. A. Chudak and D. B. Shmoys, Approximation algorithms for precedence-constrained scheduling problems on parallel machines that run at different speeds, J. Algorithms 30 (1999) 323–343 (authors' manuscript used here). https://doi.org/10.1006/jagm.1998.0987
• R. L. Graham, Bounds for certain multiprocessing anomalies, Bell System Technical Journal 45 (1966) 1563–1581. https://doi.org/10.1002/j.1538-7305.1966.tb01709.x
• J. M. Jaffe, Efficient scheduling of tasks without full use of processor resources, Theoretical Computer Science 12 (1980) 1–17. https://doi.org/10.1016/0304-3975(80)90002-4
• J.-H. Lin and J. S. Vitter, ε-approximations with minimum packing constraint violation, STOC 1992, 771–782. https://doi.org/10.1145/129712.129787
• D. B. Shmoys, J. Wein and D. P. Williamson, Scheduling parallel machines on-line, SIAM J. Computing 24 (1995) 1313–1331. https://doi.org/10.1137/S0097539793248317
• C. Chekuri and M. A. Bender, An efficient approximation algorithm for minimizing makespan on uniformly related machines, J. Algorithms 41 (2001) 212–224. https://doi.org/10.1006/jagm.2001.1184
• S. Li, Scheduling to minimize total weighted completion time via time-indexed linear programming relaxations, SIAM J. Computing 46 (2017) 409–440. https://doi.org/10.1137/15M1053163

Motivation

Single-machine scheduling with precedence constraints asks for an order in which one machine processes jobs while respecting prescribed comparisons between them. For the objective of minimizing total weighted completion time, the structure of the precedence order can influence the quality of approximation algorithms. Ambühl, Mastrolilli, Mutsanas, and Svensson connect one such approach to coloring a graph built from the order's incomparable pairs. A bounded number of colors would make a certain class of coloring-based guarantees uniform over the class of precedence orders. Their Theorem 4.3 shows that canonical interval orders have no such uniform bound for this particular graph. Ambühl et al., §4.2, p. 658

An interval order is a partial order whose elements can be represented by closed real intervals, with one element strictly before another when the first interval ends before the second begins. Interval orders are a familiar restriction of general precedence systems. The paper distinguishes them from semiorders, represented by intervals of equal length, for which it reports a three-element realizer bound and a corresponding scheduling guarantee. The chromatic obstruction here explains why that particular bounded-color route cannot be extended uniformly from semiorders to all interval orders. It does not assert that every scheduling approach to interval orders fails. Ambühl et al., §§3–4.2, pp. 656–658

Setting

For an integer $n\ge2$, let $[n]$ be a linearly ordered set with $n$ points. The canonical interval order $I_n$ has one element for every pair of distinct points $a<b$ in $[n]$, viewed as the closed interval $[a,b]$. For two such intervals, write $S\le_{I_n}T$ when $S=T$ or the right endpoint of $S$ is strictly less than the left endpoint of $T$. Thus intervals that touch at an endpoint remain incomparable. The formalization represents each interval by its two-element endpoint set, and its order relation is equivalent to this endpoint rule. Ambühl et al., §4.2, p. 658

For any partial order $P$ on a ground set $N$, an ordered incomparable pair is $(x,y)$ with neither $x\le_P y$ nor $y\le_P x$. Both $(x,y)$ and $(y,x)$ are vertices when $x$ and $y$ are incomparable. A linear extension of $P$ is a linear order on the same elements that contains all comparisons of $P$. It reverses $(x,y)$ if it places $y$ before $x$. The graph $G_P$ has the ordered incomparable pairs as vertices. Two distinct vertices form an edge when no linear extension reverses both, while each singleton can be reversed by some linear extension. This singleton condition is the minimality clause in the paper's definition through its hypergraph of incomparable pairs. Ambühl et al., §2.1, p. 655, §3, p. 656

A proper $k$-coloring assigns one of $k$ colors to every vertex of $G_P$ so that endpoints of an edge have different colors. The graph's chromatic number $\chi(G_P)$ is the least positive number of colors that works, when the graph is nonempty. The mission uses the equivalent predicate that no proper map into a fixed $k$-element color set exists once $n$ is large enough. This also gives a clear interpretation at $k=0$.

Formalization targets

The goal is Theorem 4.3: for each fixed integer $k$, all sufficiently large canonical interval orders have incomparable-pairs graphs with chromatic number greater than $k$. With $k\ge0$, the Lean target is

$$\forall k\in\mathbb N,\ \exists n_0\ge2,\ \forall n\ge n_0,\quad G_{I_n}\text{ is not $k$-colorable}.$$

The paper states $k$ as an integer. Its negative cases are immediate from nonnegativity of chromatic numbers; the target states the substantive range. The threshold $n_0$ may depend on $k$, while $I_n$ and $G_{I_n}$ are constructed from $n$ rather than supplied as arbitrary objects. Ambühl et al., Theorem 4.3, p. 658

Two assertions from the theorem's proof serve as milestones. First, $\chi(G_{I_n})$ is nondecreasing as $n$ increases. Second, for four endpoints $i<j<\ell<m$, the vertices $(\{i,j\},\{j,\ell\})$ and $(\{j,\ell\},\{\ell,m\})$ are adjacent in $G_{I_n}$. They are recorded with their wording and provenance from §4.2. A separately published theorem on hypergraph Ramsey numbers is included as a reference because the source uses that theorem in its large-$n$ argument. Ambühl et al., proof of Theorem 4.3, p. 658

Significance

The result provides a precise structural limitation: across the canonical interval orders, the chromatic numbers of $G_{I_n}$ cannot be bounded by one constant. The graph $G_P$ is a specific graph of ordered incomparable pairs, distinct from other graphs that can be associated with a scheduling instance. Thus the conclusion addresses the bounded-color approach attached to this graph, without asserting an algorithmic impossibility for interval-order scheduling. The paper contrasts this limitation with the bounded-realizer situation for semiorders. Ambühl et al., §§3–4.2, pp. 656–658

The theorem is proved in the 2011 paper. The remaining work in this mission is a machine-checked development of its definition layer, its two stated supporting assertions, and the unbounded-color conclusion. The partial-order property of $I_n$ is already proved in the definition file; the three theorem statements are open proof targets in the proposal. A completed formalization would also give reusable components for finite interval orders, ordered incomparable pairs, and coloring arguments in dimension theory.

Difficulty

A pair of intervals overlapping or touching is easy to recognize as incomparable, but graph adjacency has a stronger meaning: it quantifies over every linear extension of the entire partial order. A local test based only on the four displayed intervals would silently change the graph. Likewise, the fact that two vertices have different endpoint descriptions does not by itself make them adjacent. The formal argument must connect the canonical interval representation to the global extension-based edge condition, then show that a bounded coloring cannot persist as the endpoint set grows. Ambühl et al., proof of Theorem 4.3, p. 658

Formalization scope

The endpoint set is Fin n, hence indexed $0,\ldots,n-1$ rather than the paper's $1,\ldots,n$; the shift preserves order. Elements of $I_n$ are exactly two-element subsets of this set. The order relation includes equality and strict separation of endpoint sets and is proved to be a partial order. The graph is defined for an arbitrary binary relation so it can be reused, but every target here applies it to the concrete partial order $I_n$. Vertices are ordered incomparable pairs, and adjacency retains both singleton reversibility and failure of simultaneous reversibility. Defining adjacency directly from the desired four-point pattern would trivialize the target and is excluded.

Colorable n k means existence of a proper function from all vertices of $G_{I_n}$ to Fin k. For an empty graph, zero-colorability is allowed by this representation. The theorem therefore includes a threshold $n_0\ge2$ and quantifies over every $n\ge n_0$; the assertion itself forces the threshold past any empty-graph exceptions. The formal target uses natural $k$; the paper's negative integer values need no separate theorem. No asymptotic notation or unspecified constants occur. The source's Ramsey number $R(3:4,\ldots,4)$ is not hard-coded into the goal, because the source asserts existence of a suitable threshold, not that the least threshold equals that value.

The printed adjacency justification names an alternating-cycle pair set different from the two adjacent vertices in the preceding sentence. The milestone formalizes the adjacency assertion itself and records the printed explanation verbatim for review; it does not turn the mismatched pair set into a hypothesis. The mission needs finite order embeddings, linear extensions, graph colorings, and a finite Ramsey theorem. The existing published Ramsey theorem is referenced as a reusable result. No scheduling approximation algorithm, polynomial-time statement, or numerical scheduling guarantee is formalized in this mission.

Selected references

• Christoph Ambühl, Monaldo Mastrolilli, Nikolaos Mutsanas, and Ola Svensson, On the Approximability of Single-Machine Scheduling with Precedence Constraints, Mathematics of Operations Research 36(4), 653–669, 2011. DOI: 10.1287/moor.1110.0512

Motivation

In classical single-machine stochastic scheduling, $N$ jobs with independent random processing requirements $X_i$ are processed one after another, and the makespan (the completion time of the last job) is the same for every schedule that never idles: it is $X_1+\dots+X_N$. Research therefore concentrated on weighted flow times and rewards. Browne and Yechiali (Operations Research 38(3), 1990, 495–498) studied jobs that deteriorate while they wait: the longer a job is delayed, the more processing it needs. Such models arose in the control of queueing and communication systems (Browne 1988; Browne and Yechiali 1989) and in inventory issuing, where stored items lose quality at item-specific rates. Under deterioration the actual processing times depend on the order, so the makespan, and its expectation, become functions of the schedule, and the basic question is which order minimizes the expected makespan.

Setting

There are $N$ jobs, all available at time $0$, and a single processor. Job $i$ has an initial processing requirement $X_i$, a random variable on a probability space $(\Omega,\mathcal F,P)$: the time needed to complete job $i$ if it is processed first. Under linear deterioration, a job whose processing is delayed until time $t$ needs

$$Y_i(t) = X_i + \alpha_i t,$$

where $\alpha_i>0$ is its deterministic growth rate. A job stops deteriorating once it is put on the processor.

Only nonpreemptive strategies without idling are allowed, so a policy is a permutation $\pi$ of $\{1,\dots,N\}$, with $\pi(i)=j$ meaning that job $j$ is the $i$-th processed. The completion times follow the model: $S_0(\pi)=0$, and the job in position $k$ starts at $S_{k-1}(\pi)$ and takes $Y_{\pi(k)}(S_{k-1}(\pi))$, so

$$S_k(\pi) = S_{k-1}(\pi) + X_{\pi(k)} + \alpha_{\pi(k)} S_{k-1}(\pi), \qquad k = 1,\dots,N.$$

The makespan is $S_N(\pi)$ and the expected makespan is $\mathrm E\,S_N(\pi)$. In Lean these are completionTime X α π k ω, makespan X α π ω and expectedMakespan P X α π in the namespace DeterioratingJobs.Makespan.

The paper's Lemma 1 concerns, for real numbers $\mu_i$ and $\gamma_i$, the sum (1)

$$F_{\mu,\gamma}(\pi) = \sum_{i=1}^{N} \mu_{\pi(i)} \prod_{r=i+1}^{N} \gamma_{\pi(r)},$$

the Lean lemma1Sum μ γ π (empty product $=1$).

Formalization targets

Goal: the expected-makespan index rule (§1, p. 496)

If the $X_i$ are integrable, $\alpha_i>0$, and $\pi$ schedules the jobs by increasing values of $\mathrm E(X_i)/\alpha_i$, then

$$\mathrm E\,S_N(\pi) \le \mathrm E\,S_N(\sigma) \qquad\text{for every permutation } \sigma .$$

Milestones

1. Lemma 1 (p. 495). If $\gamma_i>1$ for all $i$, the sum (1) is minimized over all permutations by any permutation ordered by increasing $\mu_i/[\gamma_i-1]$, and maximized by any permutation ordered by decreasing values.
2. Eq. (2) (p. 496). For every $\pi$ and $j\le N$,

$$S_j(\pi) = \sum_{i=1}^{j} X_{\pi(i)} \prod_{r=i+1}^{j} \bigl(1+\alpha_{\pi(r)}\bigr).$$

3. The expected makespan in the form (1) (p. 496, after (2)).

$$\mathrm E\,S_N(\pi) = \sum_{i=1}^{N} \mathrm E(X_{\pi(i)}) \prod_{r=i+1}^{N}\bigl(1+\alpha_{\pi(r)}\bigr) = F_{\mathrm E X,\,1+\alpha}(\pi).$$

Significance

The result is an index rule: each job receives a number computed from its own data, $\mathrm E(X_i)/\alpha_i$, and sorting by that number is optimal. It needs only the means of the initial requirements, not their distributions, and it holds without independence. The same reduction to Lemma 1 gives the paper's other index rules: the variance of the makespan under independent requirements, the Poisson-shock model (5), Lévy-type growth (6) and setup/detach times (7). In inventory issuing, it says which stored item to issue first when items lose value at item-specific linear rates. Lemma 1 itself, which the paper attributes to Rau (1971) and relates to optimal search, is a general statement about ordering products of factors along a sequence.

The result is proved in the paper by an appeal to Lemma 1, whose proof is given there as one sentence ("direct upon an interchange argument"). None of these statements has a machine-checked proof on Prove2Me or in Mathlib. This mission produces a formal model of linear deterioration on a single machine, a formal proof of the interchange lemma with ties handled, and the formal index rule.

Difficulty

The algebra of one adjacent interchange is short. The work is in passing from that local comparison to optimality over all $N!$ permutations, with ties allowed: the paper speaks of "the permutation ordered by increasing values", but with equal indices several permutations qualify, and each of them must be shown optimal. The natural route, "an optimal permutation exists and must be sorted", needs care, because a sorted permutation is not unique and the swap that improves an unsorted permutation may only weakly improve it. On the probabilistic side, the expectation of the makespan must be reduced to the expectations of the $X_i$; the makespan is a polynomial in the $X_i$ with deterministic coefficients, so this is linearity of the integral, but integrability has to be carried through the recursion.

Formalization scope

• Jobs are Fin N (0-based: Lean job i is the paper's job $i+1$); a policy is π : Equiv.Perm (Fin N) with π k the job in position k, as in the paper's $\pi(i)=j$. $N=0$ is allowed.
• The probability space is (Ω, P) with [IsProbabilityMeasure P]; $X_i$ is Ω → ℝ; expectations are Bochner integrals, and every theorem about them assumes each $X_i$ integrable. The growth rates are deterministic reals.
• Completion times are defined by the model recursion $S_{k}=S_{k-1}+Y_{\pi(k)}(S_{k-1})$, never by the closed form (2), so that (2) is a theorem about the model.
• Explicit readings of loose phrases: "the permutation ordered by increasing values of $v_i$" means any permutation with $k\mapsto v_{\pi(k)}$ non-strictly increasing (Monotone), and "decreasing" means Antitone; "is minimized" means $\le$ against every permutation; "expected" means the integral of an integrable random variable.
• Added hypotheses: $\alpha_i>0$ in the goal (the paper divides by $\alpha_i$ without stating it) and $\gamma_i>1$ in Lemma 1 (the paper applies it only with $\gamma_i = 1+\alpha_i$ or $(1+\alpha_i)^2$; for $\gamma_i<1$ the ordering reverses).
• Omitted assumptions: positivity of the $X_i$ and their independence. The goal holds without them, so the formal statement is slightly more general than the paper's.
• Trivializing formalizations are excluded: defining $S$ by formula (2) would make milestone 2 a definition unfolding; a strictly increasing ordering would make the goal vacuous whenever two indices tie; ordering $\pi^{-1}$ instead of $\pi$ states a different theorem; dropping integrability makes all expectations $0$; allowing $\alpha_i=0$ makes $\mathrm E(X_i)/\alpha_i=0$ a meaningless index.
• Not formalized here: the variance result (3), the Poisson model (5), the Lévy model (6), Proposition 1, setup times (7), exponential growth (9), and the NP-hardness conjecture. Proposition 2 (weighted expected completion time) is the companion mission Scheduling Deteriorating Jobs on a Single Processor II.
• Related platform items, none of which states these results: PalmQueueing.Ordering.interchange_permutations (interchange permutations of a GI/GI/1 queue) and the additive, non-deteriorating completion-time models MooreLateJobs.Shared.completionTime and NumStochOpt.ListScheduling.Makespan.

Contributions welcome: proofs of the milestones, a reusable "sorted permutation minimizes a sum of products" lemma, and the variance index (3) as an extension.

Selected references

• S. Browne, U. Yechiali, Scheduling Deteriorating Jobs on a Single Processor, Operations Research 38(3), 1990, 495–498. https://doi.org/10.1287/opre.38.3.495
• J. G. Rau, Minimizing a Function of Permutations of n Integers, Operations Research 19(1), 1971, 237–240. https://doi.org/10.1287/opre.19.1.237
• F. P. Kelly, A Remark on Search and Sequencing Problems, Mathematics of Operations Research 7(1), 1982, 154–157. https://doi.org/10.1287/moor.7.1.154
• R. W. Conway, W. L. Maxwell, L. W. Miller, Theory of Scheduling, Addison-Wesley, 1967.

Motivation

Deterministic machine scheduling asks how to process a set of jobs on a set of machines so that an overall criterion, such as the time at which the last job finishes, is as small as possible. In the early 1970s many such problems had efficient algorithms (Johnson's rule for the two-machine flow shop, Smith's ratio rule for a single machine, Lawler's rule under precedence constraints), while others resisted every attempt. The report of Brucker, Lenstra and Rinnooy Kan (Mathematisch Centrum, 1975; journal version in Annals of Discrete Mathematics 1, 1977) drew the line between the two groups systematically. It fixed the four-field notation $n|m|\ell,\lambda|k$ that the scheduling literature still uses, and it proved NP-completeness of the "easiest" hard problems by explicit reductions in the sense of Karp.

The first family of reductions in the report, Theorem 3, concerns the simplest machine environment beyond a single machine: two identical machines. It shows that already there, minimizing the makespan and minimizing the total weighted completion time are as hard as PARTITION. These two reductions are simplified versions of reductions given by Bruno, Coffman and Sethi (1974), reference [3] of the report.

Setting

PARTITION. Given positive integers $a_1,\dots,a_t$, decide whether there is a subset $S$ of $T=\{1,\dots,t\}$ with

$$\sum_{j\in S}a_j=\sum_{j\in T-S}a_j .$$

Write $A=\sum_{j\in T}a_j$ for the total.

Two identical machines. There are $n$ jobs $J_1,\dots,J_n$ and two machines $M_1,M_2$. Job $J_j$ has a processing time $p_j\in\mathbb N$ and a weight $w_j\in\mathbb N$, and must be processed without interruption on one machine of its choice; all jobs are available at time $0$. A schedule assigns to every job a machine and a starting time $B_j\in\mathbb N$; its completion time is $C_j=B_j+p_j$. A schedule is feasible if no two jobs on the same machine are processed at the same time, i.e. the intervals $[B_j,B_j+p_j)$ on each machine are pairwise disjoint. Idle time is allowed. Two criteria are considered:

$$C_{\max}=\max_j C_j,\qquad \sum_j w_jC_j .$$

The problems $n|2|I|C_{\max}$ and $n|2|I|\sum w_jC_j$ ask for a feasible schedule minimizing the respective criterion.

Reducibility. Following Section 2 of the report, each problem is replaced by its recognition version: given an instance and a threshold $y$, is there a feasible schedule with value $\le y$? A problem $P'$ is reducible to $P$, written $P'\propto P$, if every instance of $P'$ can be transformed in polynomial time into an instance of $P$ with the same answer. Instances are written as words over a finite alphabet, with every number in binary.

Formalization targets

Goal: Theorem 3

$$\text{PARTITION}\propto n|2|I|C_{\max}\qquad\text{and}\qquad \text{PARTITION}\propto n|2|I|\textstyle\sum w_jC_j .$$

Both reductions use the same instance shape: $n=t$ jobs with $p_j=a_j$.

Milestones

1. Theorem 3(a), equivalence. With $p_j=a_j$ and $y=\tfrac12A$: PARTITION has a solution iff some feasible schedule has $C_{\max}\le y$.
2. Ordering independence. With $p_j=w_j=a_j$, if $S$ is the set of jobs on $M_1$ and each machine works without idle time from $0$, then $\sum w_jC_j=k(S)$ for every order of the jobs, where

$$k(S)=\sum_{j,k\in S,\,j\le k}a_ja_k+\sum_{j,k\in T-S,\,j\le k}a_ja_k ;$$

every feasible schedule with this assignment has value at least $k(S)$. 3. The identity for $k(S)$. With $c=\sum_{j\in S}a_j-\tfrac12A$,

$$k(S)=k(T)-\Big(\sum_{j\in S}a_j\Big)\Big(\sum_{j\in T-S}a_j\Big)=\sum_{j,k\in T,\,j\le k}a_ja_k-\big(\tfrac12A+c\big)\big(\tfrac12A-c\big)=y+c^2 .$$

4. Theorem 3(b), equivalence. With $p_j=w_j=a_j$ and $y=\sum_{j,k\in T,\,j\le k}a_ja_k-\tfrac14A^2$: PARTITION has a solution iff some feasible schedule has $\sum w_jC_j\le y$.

Significance

The result. Since PARTITION is NP-complete (Karp 1972), Theorem 3 shows that both problems are NP-hard with only two machines and a single operation per job; their recognition versions are NP-complete. Together with the single-machine and shop results in the rest of the report, it places the boundary of tractability in deterministic scheduling. The makespan problem $P2\|C_{\max}$ became a standard source problem for later hardness proofs and a standard target for pseudo-polynomial algorithms and approximation schemes. The weighted completion time result contrasts with the single-machine case, which Smith's ratio rule solves in polynomial time.

Formalizing it. The theorem is classical and fully proved on paper; the report prints the constructions and, for (b), a short calculation. To our knowledge no machine-checked proof exists. The mission produces (i) a precise model of nonpreemptive schedules on two identical machines with integer start times and idle time allowed, (ii) the two yes-instance equivalences with the paper's rational thresholds, (iii) the ordering-independence statement for $p_j=w_j$ behind part (b), and (iv) the polynomial-time computability of the reductions in a Turing machine model. Part (iv) is the formal content of "reducible" and is missing from the paper.

Difficulty

For part (a) the mathematics is short. The paper treats it as evident; a formal proof must still handle schedules with idle time and the case of odd $A$, where $\tfrac12A$ is not an integer.

Part (b) rests on the claim that, when $p_j=w_j$, the value $\sum w_jC_j$ does not depend on the order of the jobs on a machine. For a single machine without idle time this is a symmetric double sum. A recognition-problem proof also needs the converse direction: no schedule with idle time beats the non-idle one, so every feasible schedule with assignment $S$ has value at least $k(S)$. The paper cites this rather than proving it.

The step the paper leaves out entirely is polynomiality. The constructions copy the input and compute $\tfrac12A$ or $\sum_{j\le k}a_ja_k-\tfrac14A^2$, and in a one-tape Turing machine model with an explicit polynomial time bound this needs binary arithmetic (sums, products, a floor) carried out on the tape. It also needs a decoder that rejects malformed words and lists containing a zero. This is routine in principle but long in practice.

Formalization scope

• Model. Jobs are Fin n and machines Fin 2 (machine 0 is $M_1$). Starting times are natural numbers. Section 3 of the report computes them from processing orders on nonnegative integer data, and both criteria are regular, so real starting times would give the same yes-instances. Processing times may be zero; a zero-length job occupies the empty interval. Schedules may contain idle time.
• Criteria. "$C_{\max}\le y$" is stated as $C_j\le y$ for every job, which equals $\max_jC_j\le y$ for $n\ge1$ and avoids a supremum. $\sum w_jC_j$ is a finite sum in $\mathbb N$.
• Languages. PARTITION is the set of binary codes of lists of positive integers that admit a partition; a code of a list with a zero entry is not in the language. A target word codes $n$, the processing times (and weights, job by job), and a threshold $y\in\mathbb N$. The number of machines is fixed by the class and not coded. Every coded instance is in the class, so the language admits nothing outside it.
• Reducibility is CookPvsNP.PolyReducible from the published definition CookPvsNP_defs (Cook's one-tape Turing machines, polynomial-time many-one reductions). The alphabet BSym and the binary code encNats are reused from the published ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann). Its PARTITION language is not reused, because it allows zero sizes.
• Thresholds. The milestones state the paper's thresholds $\tfrac12A$ and $\sum_{j\le k}a_ja_k-\tfrac14A^2$ as real numbers, exactly as printed. The goal's reduction must write a natural-number threshold; all schedule values are integers, so the floor of the printed threshold gives the same yes-instances.
• Explicit readings. The equivalence of (a) is not printed; the report says on p. 14 that such equivalences are "trivial or clear" where not proved. "Only depends on the choice of $S$" is stated as two facts: equality for non-idle schedules and a lower bound for all feasible schedules. "It is easily seen (cf. Figure 1)" is the three-step identity, one equality per printed step. $k(S)$ is defined by its closed form, and its link to schedules is a milestone.
• Ruled out. A target language whose yes-instances are defined through PARTITION, an equivalence for some instance rather than the paper's construction, and a goal that drops polynomial-time computability would all make the goal vacuous or different. The statements here use the constructions as printed and Cook's reducibility.
• Welcome contributions. Proofs of the four milestones; a library of polynomial-time Turing machine programs for binary arithmetic and list decoding over BSym, which every mission of this series needs and which is reusable for other reductions on the platform.

Selected references

• P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum Report BW 43/75, Amsterdam, 1975. https://ir.cwi.nl/pub/9725/9725D.pdf
• J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Complexity of machine scheduling problems, Annals of Discrete Mathematics 1 (1977) 343–362. https://doi.org/10.1016/S0167-5060(08)70743-X
• J. Bruno, E. G. Coffman Jr., R. Sethi, Scheduling independent tasks to reduce mean finishing time, Communications of the ACM 17 (1974) 382–387. https://doi.org/10.1145/361011.361064
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
• S. A. Cook, The complexity of theorem-proving procedures, STOC 1971, 151–158. https://doi.org/10.1145/800157.805047
• W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3 (1956) 59–66. https://doi.org/10.1002/nav.3800030106