All missions

Motivation

In a flow shop every job passes through the same machines in the same order. Choosing the order in which jobs enter the shop so that the last job finishes as early as possible (minimizing the makespan) is one of the oldest problems of scheduling theory. For two machines Johnson (1954) gave an exact sorting rule; for three machines his rule is exact only in special cases, and the general problem was later shown to be NP-hard (Garey, Johnson and Sethi, 1976). Exact methods for three or more machines therefore enumerate sequences, and the question is how to enumerate as few of them as possible.

Ignall and Schrage (1965), at the same time as Lomnicki (Operational Research Quarterly, 1965), introduced branch and bound for the three-machine permutation flow shop. Their lower bound, which adds to the time each machine becomes free the work that remains on it and the least work that must follow on later machines, became the template for the machine-based bounds used in flow-shop branch and bound ever since.

Timeline. 1954: Johnson proves the two-machine rule and shows that for three machines a common job order on all machines loses nothing for the makespan. 1960: Land and Doig introduce branch and bound for integer programs. 1965: Ignall–Schrage and Lomnicki apply it to the three-machine flow shop. 1976: Garey, Johnson and Sethi prove the three-machine makespan problem NP-hard, so exact enumeration with good bounds remains the method for exact solutions.

Setting

There are $n\ge1$ jobs and three machines $A$, $B$, $C$. Job $i$ needs time $a_i$ on $A$, then $b_i$ on $B$, then $c_i$ on $C$. Following Johnson, only permutation schedules are considered: a full sequence is a permutation $\sigma$ of the jobs, processed in that order on all three machines, each operation starting as early as possible. Its makespan is the time machine $C$ finishes the last job.

A node $J_r$ is a partial sequence: an ordered list of $r$ distinct jobs. Its unscheduled set $\bar J_r$ is the set of the other $n-r$ jobs. The attributes $\mathrm{TIMEA}(J_r)$, $\mathrm{TIMEB}(J_r)$, $\mathrm{TIMEC}(J_r)$ are the times at which machines $A$, $B$, $C$ finish the jobs of $J_r$ processed in order. A full sequence begins with $J_r$ when its first $r$ positions are $J_r$. The lower bound of a node with $\bar J_r\neq\emptyset$ is

$$LB(J_r)=\max\Big[\mathrm{TIMEA}(J_r)+\sum_{\bar J_r}a_i+\min_{\bar J_r}(b_i+c_i),\ \mathrm{TIMEB}(J_r)+\sum_{\bar J_r}b_i+\min_{\bar J_r}c_i,\ \mathrm{TIMEC}(J_r)+\sum_{\bar J_r}c_i\Big].$$

The branch-and-bound procedure keeps a list of nodes ranked by $LB$, starting from the root (no job scheduled). At each step it removes the first node, creates one child per unscheduled job by appending that job, and inserts the children ranked into the list, a new node going before old nodes of equal bound. It stops when the first node of the list is terminal, i.e. has scheduled $n-1$ jobs, so that its last job is forced.

Formalization targets

Goal: the stopping rule certifies an optimal sequence

$$\exists k:\ \text{the first node of } \mathrm{run}(k) \text{ is terminal},\qquad\text{and}\qquad \text{first node } P \text{ terminal} \ \Longrightarrow\ \mathrm{makespan}(\sigma_P)\le\mathrm{makespan}(\sigma)\ \ \forall\sigma ,$$

where $\sigma_P$ is $P$ followed by its one unscheduled job. This is the paper's "the problem is solved: that node's sequence is an optimal one" (p. 402), for any real processing times.

Milestones

1. Validity of the bound (p. 401): $LB(J_r)\le\mathrm{makespan}(\sigma)$ for every $\sigma$ beginning with $J_r$, $r<n$.
2. Exactness at depth $n-1$ (general form of an observation on p. 403): for $r=n-1$, $LB(J_{n-1})$ equals the makespan of the completed sequence.
3. Node counts (p. 403): at least $\tfrac12n(n+1)$ nodes are created before stopping, at most $1+n+n(n-1)+\cdots+n!$ are ever created, and the list never holds more than $n!$ nodes.
4. Dominance (pp. 403–404): if $J_r$ and $I_r$ contain the same jobs, $\mathrm{TIMEA}(J_r)=\mathrm{TIMEA}(I_r)$; if also $\mathrm{TIMEB}(J_r)\le\mathrm{TIMEB}(I_r)$ and $\mathrm{TIMEC}(J_r)\le\mathrm{TIMEC}(I_r)$, replacing $I_r$ by $J_r$ at the beginning of any sequence does not increase its makespan, and $LB(J_r)\le LB(I_r)$ (p. 404).
5. The 4-job example (pp. 402–403): the run stops after 6 steps with node 231 first, whose bound 62 is the optimal makespan.
6. The refined bound (p. 409): the strengthened bound used in the paper's computations is still a lower bound.

Significance

The goal is the correctness theorem of the Ignall–Schrage algorithm: best-first search over partial sequences, with a machine-based bound, returns an optimal permutation. Milestone 1 is the bound's validity, which every later machine-based flow-shop bound generalizes; milestone 4 is the dominance rule that justifies discarding nodes; milestone 3 brackets the effort of the search between the best case $\tfrac12n(n+1)$ and full enumeration.

The paper's arguments are short and informal: validity of the bound is asserted with a one-line reason, and optimality at stopping is argued on the example. None of these results has a machine-checked proof. The formalization makes the procedure itself a precise object (list, insertion rule, stopping rule) and turns the paper's claims into statements about it, so that the correctness of the search is proved rather than illustrated.

Difficulty

Each inequality is elementary, but the goal is a statement about an iterated list-manipulating procedure. The obvious argument "the first node has the smallest bound and the bound is valid" needs an invariant that the paper does not state: at every step, every full sequence begins with some node on the list, and the list is sorted. Both must be proved to survive one step of removal and ranked insertion. Termination is likewise not stated: it needs a measure that strictly decreases, for instance the set of nodes that remain to be created, which requires showing that no node is created twice. A tempting shortcut, proving optimality only among the sequences whose nodes were created, is not the theorem.

Formalization scope

Jobs are Fin n (the paper's job $i$ is $i-1$), processing times are arbitrary reals with no sign condition, and full sequences are Equiv.Perm (Fin n). The makespan is the machine-$C$ completion time of Johnson's as-soon-as-possible schedule, taken from the published definition JohnsonFlowShop.ThreeStage.asapSchedule. Nodes are lists of jobs, and the node attributes are the same recursion folded over the list. Minima over $\bar J_r$ are Finset.inf'; on an empty set the auxiliary minimum returns a placeholder $0$ that no statement evaluates.

Explicit readings of the paper's phrases:

• "is a lower bound … for any node that emanates from node $P$" is "$\le$ the makespan of every permutation whose first $r$ positions are $J_r$";
• "a node that has scheduled all $n$ jobs" is read as a node with $n-1$ jobs, whose sequence is completed by the forced last job. The example (stop at node 231 of a 4-job problem), the node counts and the formula for $LB$ all require this reading;
• "the problem is solved: that node's sequence is an optimal one" is termination together with optimality over all $n!$ permutations;
• "cannot be hurt by replacing $I_r$ with $J_r$" compares the completions of $J_r$ and $I_r$ by the same ordering of the remaining jobs;
• children are inserted one at a time in increasing job index, each before every node with an equal bound; this reproduces the paper's LIST table;
• dominance discarding is not part of the procedure in the goal.

A formalization in which the optimality claim ranges only over sequences the run created, or one that asserts optimality without termination, would be trivial or vacuous and is ruled out by the goal's statement.

Not formalized: the reduction from general schedules to permutation schedules (Johnson's Lemma 3, proved on the platform as JohnsonFlowShop.ThreeStage.same_ordering_dominant), the dominance bookkeeping and its percentages, the two-machine mean-completion problem (a separate mission of this series), the computational tables, and the TIMEB/TIMEC columns of the example's LIST table. No platform item treats flow-shop lower bounds or branch and bound over sequences; the nearest branch-and-bound mission, BiconvexProg.BranchBound (Al-Khayyal and Falk), concerns biconvex programs and is unrelated.

The lemmas a solver will want (the invariant of the list, monotonicity of the completion recursion in its start times, validity of the bound) are reusable for the two-machine mission and for any other machine-based bound. Proofs of the milestones, and of the goal from them, are welcome in any order.

Selected references

• E. Ignall and L. Schrage, Application of the branch and bound technique to some flow-shop scheduling problems, Operations Research 13(3), 400–412, 1965. https://doi.org/10.1287/opre.13.3.400
• S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1), 61–68, 1954. https://doi.org/10.1002/nav.3800010110
• A. H. Land and A. G. Doig, An automatic method of solving discrete programming problems, Econometrica 28(3), 497–520, 1960. https://doi.org/10.2307/1910129
• M. R. Garey, D. S. Johnson and R. Sethi, The complexity of flowshop and jobshop scheduling, Mathematics of Operations Research 1(2), 117–129, 1976. https://doi.org/10.1287/moor.1.2.117

Motivation

The single-server queue with general independent interarrival and service times (the GI/G/1 queue) is the basic model of congestion in operations research: customers arrive at a service facility, wait if the server is busy, are served in order of arrival, and leave. The first question about any such system is whether it settles down. If customers keep arriving faster than they can be served, waiting times grow without bound; otherwise one expects an equilibrium distribution of waiting time that capacity planning, staffing and performance analysis can be based on.

D. V. Lindley's 1952 paper Lindley 1952 answered this question for the GI/G/1 queue in complete generality. It introduced the recursion for successive waiting times that now carries his name, connected the queue with a random walk, and proved that an equilibrium exists exactly when the mean service time is smaller than the mean interarrival time, with the degenerate deterministic case as the only exception. The paper is the starting point of the random-walk approach to queueing theory and of the later work of Kiefer and Wolfowitz, Spitzer, Loynes and Kingman.

Setting

Customers arrive in order at a single server; customer $r$ is served after all its predecessors. On a probability space $(\Omega, \mathcal F, P)$ let

• $t_r \ge 0$ be the interarrival time between customers $r$ and $r+1$,
• $s_r \ge 0$ be the service time of customer $r$.

Assumption 1: the $t_r$ are independent and identically distributed with finite mean $\mathscr{E}(t_r)$. Assumption 2: the $s_r$ are independent and identically distributed with finite mean $\mathscr{E}(s_r)$, and the families $\{s_r\}$ and $\{t_r\}$ are independent of each other.

Put $u_r = s_r - t_r$; the $u_r$ are i.i.d. and integrable, and $\mathscr{E}(u) = \mathscr{E}(s) - \mathscr{E}(t)$ denotes their common mean. The waiting time $w_r$ of customer $r$ (time from arrival to start of service) satisfies Lindley's recursion

$$w_1 = 0, \qquad w_{r+1} = \max(w_r + u_r,\ 0).$$

Write $F_r(x) = p(w_r \le x)$ for the waiting-time distribution function, $G$ for the law of $u_r$, and $U_n = u_1 + \dots + u_n$ for the associated random walk. Lindley shows that $F_r(x)$ converges for every $x$ to

$$F(x) = p(U_s \le x \text{ for all } s \ge 1) \quad (x \ge 0), \qquad F(x) = 0 \quad (x < 0).$$

Formalization targets

Goal: Lindley's theorem (§4, p. 281)

1. The waiting-time distribution $F_r$ converges to a proper (non-degenerate) limit distribution if and only if

$$\mathscr{E}(u) < 0 \quad \text{or} \quad u = 0 \text{ almost surely.}$$

2. If $\mathscr{E}(u) \ge 0$ and $u$ is not almost surely $0$, then $p(w_r \le x) \to 0$ for every $x$.

Milestones, in the order of the paper

• Eq. (2), the one-step convolution $F_{r+1}(x) = \int_{u \le x} F_r(x-u)\,dG(u)$ for $x \ge 0$ (an existing platform statement, referenced).
• Eq. (3), the duality with the random walk: $F_{r+1}(x) = p(U_s \le x \text{ for all } s \le r)$ for $x \ge 0$.
• The limit: $F_r(x) \to F(x)$ for every $x$.
• Eqs. (4)–(5), Lindley's integral equation $F(x) = \int_{u \le x} F(x-u)\,dG(u)$ for $x \ge 0$.
• Case (i): $\mathscr{E}(u) > 0 \Rightarrow F \equiv 0$. Case (ii): $\mathscr{E}(u) < 0 \Rightarrow F(x) \to 1$ as $x \to \infty$.
• Eq. (8), the theorem of Chung and Fuchs quoted by Lindley: a mean-zero, non-lattice random walk comes within $\epsilon$ of every point infinitely often.
• Case (iii): $\mathscr{E}(u) = 0$, $u \not\equiv 0 \Rightarrow F \equiv 0$.
• Companion: for $\mathscr{E}(u) < 0$, exactly one distribution on $[0,\infty)$ solves the integral equation.

Significance

The theorem is the stability criterion $\rho = \mathscr{E}(s)/\mathscr{E}(t) < 1$ for the GI/G/1 queue, and its proof identifies the equilibrium waiting time with the supremum of a random walk with negative drift. Every later result on the equilibrium waiting time (Pollaczek–Khinchine for M/G/1, Kingman's bounds, the Wiener–Hopf factorization, heavy-traffic limits) presupposes this existence statement. The critical case $\rho = 1$ is the part that goes beyond the law of large numbers: there is no equilibrium even though the queue has no drift.

The result has been proved since 1952 and appears in every queueing textbook. No machine-checked proof of it is known to exist. The platform already has related open statements in other frameworks: a law-level one-step identity and the stationary-delay equation from Gross et al. (QueueingFundamentals.GG1), and Loynes' theorem in a stationary ergodic Palm framework (PalmQueueing.Loynes.loynes_stability). None of them states convergence of the customer-indexed waiting-time distributions, and none treats the critical case. This mission produces the customer-indexed model, the random-walk duality, and the complete iff, including the Chung–Fuchs recurrence theorem for one-dimensional random walks, which is of independent use.

Difficulty

Cases (i) and (ii) follow from the strong law of large numbers, which Mathlib provides. The obstacle is the critical case $\mathscr{E}(u) = 0$: the strong law only gives $U_n/n \to 0$, which says nothing about whether $\sup_n U_n$ is finite. One needs the recurrence of mean-zero random walks (Chung–Fuchs), which is not in Mathlib. A second, smaller difficulty is eq. (3): it is an identity of probabilities, not of events, since the waiting time is built from sums taken in the reverse order of the walk's partial sums. Finally, the iff needs a careful passage from pointwise limits of distribution functions to convergence to a probability measure.

Formalization scope

All objects live in one definitions file, LindleyQueue.Stability.Model. The input is a structure Input Ω P holding measurable sequences s t : ℕ → Ω → ℝ with iIndepFun for each family, identical distribution, integrability, independence of the two families as random elements of $\mathbb R^{\mathbb N}$, and nonnegativity. Theorems assume IsProbabilityMeasure P. Committed conventions:

• Indexing from 0: w 0 is the paper's $w_1$, F r is $F_{r+1}$, U n $= \sum_{i<n}$ u i is the paper's $U_n$.
• Non-degenerate means proper: the limit is a probability measure $\nu$ on $\mathbb R$, and convergence is $F_r(x) \to \nu((-\infty,x])$ at every $x$ with $\nu\{x\} = 0$. When $u = 0$ a.s. the limit is the point mass at $0$, and the theorem counts it as convergent.
• "Certainly" means almost surely, for $u_1$; all $u_r$ share its law.
• $\mathscr{E}(u)$ is the Bochner integral of the integrable u 0; $G$ is the push-forward law of u 0, and Stieltjes integrals $\int_{u \le x} \cdots dG(u)$ are integrals over Set.Iic x.
• $F(x)$ is defined with the case split $x \ge 0$ / $x < 0$; eqs. (3), (4) are stated for $x \ge 0$, as on the page.
• Eq. (8) is stated for an arbitrary i.i.d. integrable mean-zero sequence (only the non-lattice half).

Trivializing formalizations are ruled out: the goal is about the queue's $F_r$, not the random walk's absorption probabilities; the limit must be a probability distribution, since "converges to some function" is already the limit milestone; and "$u = 0$" is almost-sure, not pointwise. A verification file builds an Input with $s_r = t_r = 1$, so the hypotheses are satisfiable.

Needed infrastructure: exchangeability of finite i.i.d. vectors, continuity of measure along decreasing events, the strong law (in Mathlib), recurrence of one-dimensional random walks, and convergence of distribution functions. The Chung–Fuchs theorem and the random-walk duality are reusable well beyond queueing; contributions of either are welcome.

Selected references

• D. V. Lindley, The theory of queues with a single server, Mathematical Proceedings of the Cambridge Philosophical Society 48(2), 277–289, 1952. https://doi.org/10.1017/S0305004100027638
• K. L. Chung and W. H. J. Fuchs, On the distribution of values of sums of random variables, Memoirs of the American Mathematical Society 6, 1951. https://doi.org/10.1090/memo/0006
• R. M. Loynes, The stability of a queue with non-independent inter-arrival and service times, Mathematical Proceedings of the Cambridge Philosophical Society 58(3), 497–520, 1962. https://doi.org/10.1017/S0305004100036781
• S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003, Ch. III and X. https://doi.org/10.1007/b97236

Motivation

A flow shop is the simplest model of a production line: every job passes through the same sequence of machines in the same order. Minimizing the time at which the last job leaves the last machine (the finish time, or makespan) is easy for two machines, where Johnson's rule gives an optimal schedule in time $O(n\log n)$ (Johnson 1954), and NP-hard from three machines on (Garey, Johnson, Sethi 1976; Gonzalez, Sahni 1978, §1, for preemptive schedules). For three or more machines the practical question is therefore how far a fast heuristic can be from the optimum in the worst case.

Gonzalez and Sahni (1978, §2) first show that any busy schedule, one that never leaves a processor idle while a task is available for it, has finish time at most $m$ times the optimum (their Lemma 10), and that the natural "longest job first" order does no better. They then give a heuristic, H, that uses Johnson's two-machine algorithm as a subroutine and has the better worst-case ratio $\lceil m/2\rceil$ (Lemma 11). This mission formalizes that bound.

Setting

A flow shop has $m$ processors $P_1,\dots,P_m$ and $n$ jobs. Job $i$ consists of $m$ tasks; task $j$ runs on processor $P_j$ and needs processing time $t_{j,i}\ge 0$ (zero is allowed). A non-preemptive schedule gives every task a start time $s_{j,i}$, and the task occupies $P_j$ during $[s_{j,i},s_{j,i}+t_{j,i})$. It is feasible when all start times are nonnegative, when task $j+1$ of a job starts only after task $j$ of that job has completed ($s_{j,i}+t_{j,i}\le s_{j+1,i}$), and when no processor runs two tasks of positive length at the same time. Its finish time $\mathrm{FT}(s)$ is the latest completion time $s_{j,i}+t_{j,i}$ (and $0$ if there is no task). An optimal finish time (OFT) schedule $S^*$ is a feasible schedule of least finish time.

Heuristic H (p. 48) divides the processors into $\lceil m/2\rceil$ groups: group $g$ consists of $P_{2g-1}$ and $P_{2g}$, and when $m$ is odd the last group is $P_m$ alone. The flow shop $F_g$ on group $g$ has the same jobs, with task times $t_{2g-1,i},t_{2g,i}$ only. For each group an OFT schedule $R(g)$ of $F_g$ is computed (by Johnson's algorithm), with finish time $f(R(g))$. The schedule $S$ generated by H runs these schedules one after another: every task of group $g$ starts at its time in $R(g)$ plus the offset $\sum_{h<g}f(R(h))$.

Formalization targets

Goal: Lemma 11 (p. 49)

For every flow shop with $m$ processors and $n$ jobs, every choice of OFT schedules $R(g)$ of the group flow shops, the schedule $S$ generated by H, and every feasible non-preemptive schedule $\tau$ of the flow shop (in particular an OFT schedule $S^*$),

$$\mathrm{FT}(S)\le\Big\lceil\frac m2\Big\rceil\,\mathrm{FT}(\tau).$$

The paper writes this as $\mathrm{FT}(S)/\mathrm{FT}(S^*)\le\lceil m/2\rceil$.

Milestones

1. Every group flow shop $F_g$ has an OFT schedule (p. 48; the paper obtains it with Johnson's algorithm).
2. The concatenation of feasible group schedules is a feasible schedule of the $m$-processor flow shop (p. 48).
3. $\mathrm{FT}(S^*)\ge\max_g f(R(g))$ (proof of Lemma 11, p. 49).
4. $\mathrm{FT}(S)\le\sum_g f(R(g))\le\lceil m/2\rceil\max_g f(R(g))$ (proof of Lemma 11, p. 49).

Significance

The result gives a polynomial-time heuristic, running in time $O(mn\log n)$, whose finish time is within a factor $\lceil m/2\rceil$ of the optimum on every instance, half the factor $m$ that every busy schedule already achieves. The paper's Example 4 (p. 49) shows that for $m=3$ the factor $2=\lceil 3/2\rceil$ is approached, so the analysis cannot be improved in general.

Formalizing it produces a reusable, machine-checked model of the $m$-processor flow shop with non-preemptive schedules, its restriction to blocks of consecutive processors, and the concatenation of schedules of disjoint blocks. Lemma 11 has a short paper proof; to our knowledge it has no machine-checked proof. The model's careful treatment of zero task times, of odd $m$, and of the restriction of a schedule to a processor group is itself part of the value: these are the points at which an informal argument is silent.

Difficulty

The arithmetic of the bound is short; the content lies in two structural facts about a precise model: that the concatenated object is a feasible schedule of the whole flow shop, including across the boundary between consecutive groups and for a final group of a single processor, and that the optimum of the whole flow shop is at least the optimum of each group flow shop, whose first processor has no predecessor. Informal arguments are silent on exactly these points. A naive formalization that leaves the offsets free, or that does not require the $R(g)$ to be optimal, makes the statement false; one that lets $S$ be any schedule with the right restrictions makes it witnessed by $S^*$ itself.

The existence of OFT schedules for the group flow shops (milestone 1) is a separate matter: the paper takes it from Johnson's algorithm, and proving it requires an optimality argument for two-machine flow shops (or a compactness argument over finitely many processing orders).

Formalization scope

• Representation. Processors are Fin m and jobs Fin n, both 0-based; times are real numbers. A flow shop is a matrix t : Fin m → Fin n → ℝ with t ≥ 0. A schedule is a matrix of start times. Group $g$ (0-based, g : Fin ((m + 1) / 2)) contains the processors $2g$ and $2g+1$ that exist, min 2 (m - 2g) of them.
• Finish time. A fold of max with baseline $0$ over all tasks; it is $0$ for $m=0$ or $n=0$. The maximum of the group finish times is also a fold of max with baseline $0$. No supremum over an unbounded or empty set is taken.
• Zero task times. A zero-length task occupies no processor time (it is exempt from the non-overlap condition) but still respects the job's task order and counts in the finish time when it is placed late; optimal schedules are unaffected.
• The optimum. "OFT schedule $S^*$" is replaced by a universally quantified feasible schedule $\tau$, which is stronger and needs no existence assumption for $S^*$. Optimality of $R(g)$ is the predicate "feasible, and finish time at most that of every feasible schedule of the same group flow shop".
• Constants. $\lceil m/2\rceil$ is (m + 1) / 2 in $\mathbb N$, cast to $\mathbb R$; the two agree for every $m\ge 0$. The ratio is multiplied out, so a zero optimum does not divide by zero.
• Not formalized. Johnson's algorithm and the running times $O(n\log n)$ and $O(mn\log n)$. The goal quantifies over every family of optimal group schedules, which includes the one Johnson's algorithm computes; the paper's proof uses only optimality. The preemptive comparison on p. 50 and the tightness examples are outside the mission.
• Trivialization ruled out. The schedule $S$ is a function of the $R(g)$ with the fixed offsets $\sum_{h<g}f(R(h))$, and each $R(g)$ must be optimal for its group flow shop; neither the offsets nor $S$ are free.
• Infrastructure. Elementary facts about Finset.fold max and sums over Fin; nothing beyond Mathlib. Contributions proving milestone 1 by formalizing Johnson's rule for this model are welcome and reusable.

Selected references

• T. Gonzalez, S. Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1), 36–52, 1978. https://doi.org/10.1287/opre.26.1.36
• S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1), 61–68, 1954. https://doi.org/10.1002/nav.3800010110
• M. R. Garey, D. S. Johnson, R. Sethi, The Complexity of Flowshop and Jobshop Scheduling, Mathematics of Operations Research 1(2), 117–129, 1976. https://doi.org/10.1287/moor.1.2.117

Motivation

Kingman's subadditive ergodic theorem (Theorem 1 of Kingman 1973, first proved in Kingman 1968) says that for a discrete-parameter subadditive process $x=(x_{st})$ the ratio $x_{0t}/t$ converges with probability one and in mean. Applications in first-passage percolation, products of random matrices and longest increasing subsequences often come with a continuous time parameter, so it is natural to ask whether the theorem holds with $t$ ranging over $[0,\infty)$.

Section 1.4 of the 1973 paper answers this question. Under separability alone, a continuous-parameter version would contain, as its additive special case, the claim that every separable process $(y_t;\,t\ge0)$ with stationary increments and finite expectations has a finite limit $\lim_{t\to\infty}y_t/t$ with probability one. Kingman remarks that no such theorem appears in the literature, "for the excellent reason that the conclusion is false, and in a very strong sense" (p. 888). Theorem 3 makes that sentence precise. It is the reason the continuous-parameter theorem of the paper (Theorem 4) carries an extra integrability hypothesis on the oscillation $\Omega_I=\sup_{s<t,\,s,t\in I}|x_{st}|$.

Setting

A real-time process is a family $(y_t;\,t\ge0)$ of real random variables on a probability space $(\Omega,\mathcal F,P)$. Its joint law is the law of the path $t\mapsto y_t$ on $\mathbb R^{[0,\infty)}$ with the product $\sigma$-algebra, that is, the collection of all finite-dimensional distributions.

• $(y_t)$ is stationary if for every $\tau\ge0$ the shifted process $(y_{t+\tau})_{t\ge0}$ has the same joint law as $(y_t)_{t\ge0}$.
• $(y_t)$ has stationary increments if for every $\tau\ge0$ the process $(y_{t+\tau}-y_\tau)_{t\ge0}$ has the same joint law as $(y_t-y_0)_{t\ge0}$.
• $(y_t)$ has finite expectations if $E|y_t|<\infty$ for every $t\ge0$.
• The sample function at $\omega\in\Omega$ is $t\mapsto y_t(\omega)$. It has derivatives of all orders if it is $C^\infty$ on $[0,\infty)$.

A growth bound is a function $\Gamma:(0,\infty)\to(0,\infty)$ that is increasing (non-decreasing). The event "$|y_t|\le\Gamma(t)$ for all sufficiently large $t$" is the set of $\omega$ for which some $T$ exists with $|y_t(\omega)|\le\Gamma(t)$ for every real $t\ge T$.

In the Lean development these notions are IsStationary, HasStationaryIncrements, Integrable (y t) P and ContDiffOn ℝ ∞ (fun t => y t ω) (Set.Ici 0), all in the namespace KingmanSubadditive.StationaryIncrements.

Formalization targets

Goal: Theorem 3 (p. 888)

For every positive non-decreasing $\Gamma$ on $(0,\infty)$ there are a probability space and a process $(y_t;\,t\ge0)$ with stationary increments, finite expectations and $C^\infty$ sample functions such that

$$P\{|y_t|\le\Gamma(t)\ \text{for all sufficiently large }t\}=0. \tag{1.4.4}$$

The quantifiers are "for every $\Gamma$ there exists $y$". Because $\Gamma$ may grow arbitrarily fast, no normalization $y_t/a(t)$ with a deterministic $a$ can converge to a finite limit almost surely.

Milestones

The milestones are the four steps of Kingman's proof, stated for the explicit process $y_t=Y_{t+\eta}$ of (1.4.5) built from a bump function $\psi$, a uniform $\eta$ and independent integer-valued $\nu_0,\nu_1,\dots$ with a law $m_\Gamma$ that depends on $\Gamma$:

1. $(y_t)$ is stationary, hence has stationary increments, and its sample functions are $C^\infty$ (p. 888).
2. $E(|y_t|)=E(y_0)=\int_0^1\psi(u)\,du<\infty$ (p. 888).
3. $\sum_{n\ge1}P\{\nu_n>\Gamma(n+\tfrac12)\}\ge\sum_{n\ge1}\sum_{r\ge n}\frac1{r(r+1)}=\infty$ (p. 889).
4. $P\{|y_t|\le\Gamma(t)\text{ eventually}\}\le P\{|y(n+\tfrac12\nu_n^{-1}-\eta)|\le\Gamma(n+\tfrac12\nu_n^{-1}-\eta)\text{ eventually}\}\le P\{\nu_n\le\Gamma(n+\tfrac12)\text{ eventually}\}=0$ (p. 889).

Significance

The result. Theorem 3 rules out any continuous-parameter subadditive ergodic theorem whose only hypotheses are separability, stationarity of the increments and finite means, and in fact any such theorem whose hypotheses are met by smooth stationary processes with finite means. The obstruction does not come from irregular paths: the counterexample is as regular as a path can be short of analyticity. Any continuous-time ergodic theorem therefore needs a hypothesis that controls the behaviour of the process inside unit intervals, such as $E(\Omega_I)<\infty$ in Theorem 4, or the integrability of $\int_I|y'|$ in the classical continuous-parameter ergodic theorem. The result also separates two kinds of time. Along the integers, a stationary-increment process with finite mean is an additive discrete process, so $y_n/n$ converges almost surely; Theorem 3 shows that the real-time path can still escape any envelope between the integers.

Formalizing it. The theorem is classical and its proof is complete in the paper. To our knowledge it has no machine-checked proof. A formalization requires the existence of a probability space carrying a uniform variable and an independent i.i.d. sequence with a prescribed law on the integers, the joint-law notion of stationarity for real-time processes, a stationarity argument for a randomly shifted process, an expectation computation with a change of variables, and the second Borel–Cantelli lemma. The definitions of stationarity and stationary increments for real-time processes on $[0,\infty)$ are reusable beyond this mission.

Difficulty

The natural first attempt is a process with linear or polynomial growth, such as $y_t=Zt$ with a heavy-tailed integrable $Z$. Every such attempt fails against a $\Gamma$ that grows faster, so the process must depend on $\Gamma$. A process that is large on a whole interval of length one cannot have finite mean when $\Gamma$ grows fast. The difficulty is to have excursions that are taller than any prescribed envelope infinitely often, and still keep finite expectation, stationarity in real time and smoothness. In the formal proof, the stationarity step is where most of the work sits: the shifted path must be identified in law with the original one for every real shift $\tau$, not only for integer shifts.

Formalization scope

• The process is y : ℝ → Ω → ℝ, with values at $t<0$ ignored; $\Omega$ lives in Type. Every $y_t$ with $t\ge0$ is measurable, and both stationarity definitions include almost-everywhere measurability, so Measure.map never takes its junk value.
• Joint laws are push-forwards to Set.Ici (0:ℝ) → ℝ with the product $\sigma$-algebra. Stationary increments compare the laws of $(y_{t+\tau}-y_\tau)_t$ and $(y_t-y_0)_t$ for every real $\tau\ge0$.
• "Increasing" is non-decreasing on $(0,\infty)$ (MonotoneOn Γ (Set.Ioi 0)), which gives the stronger theorem. $\Gamma$ is a total function on $\mathbb R$; its values at $t\le0$ are irrelevant.
• "Derivatives of all orders" is ContDiffOn ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) on $[0,\infty)$ for every $\omega$. This is $C^\infty$, not the analytic order.
• In (1.4.4) "sufficiently large $t$" ranges over real $t$. The event need not be measurable a priori; $P$ of a set is its outer measure.
• A statement with a fixed $\Gamma$, with $\exists\Gamma$, with "for some large $t$", or with $t$ restricted to the integers would be trivial or false and is not the theorem. The integer skeleton is precisely what does not fail.
• For the milestones, the random ingredients are hypotheses: any $\eta,\nu_0,\nu_1,\dots$ that are independent, with $\eta$ uniform on $(0,1)$ and each $\nu_r$ of law $m_\Gamma$. The existence of such a family is part of the goal's proof.

Contributions welcome: proofs of the milestones, a general lemma that a uniformly shifted process built from an i.i.d. sequence of unit blocks is stationary in real time, and a proof of the goal.

Selected references

• J. F. C. Kingman, Subadditive ergodic theory, The Annals of Probability 1(6):883–899, 1973. https://doi.org/10.1214/aop/1176996798
• J. F. C. Kingman, The ergodic theory of subadditive stochastic processes, Journal of the Royal Statistical Society, Series B 30(3):499–510, 1968. https://doi.org/10.1111/j.2517-6161.1968.tb00749.x

Motivation

Flow shops and job shops are the basic models of multi-stage production: every job passes through several machines, and each machine handles one task at a time. Gonzalez and Sahni (Operations Research 26(1), 1978) showed that minimizing the finish time of such shops is NP-complete even with preemption, and then asked how well simple heuristics do. One of the two objectives they study is the mean flow time, the average completion time of the jobs, which measures how long a job spends in the shop on average.

Their Lemma 9 analyses the most natural rule for that objective, shortest processing time first (SPT): process the jobs in order of nondecreasing total work. For a single machine SPT is optimal (Smith 1956; Conway, Maxwell and Miller, Theory of Scheduling, 1967, p. 76, which the paper cites). Lemma 9 shows that with $m$ processors the same rule loses at most a factor $m$, and the paper's Example 2 shows that the factor $m$ is attained in the limit.

Setting

A job shop has $m\ge1$ processors $P_1,\dots,P_m$ and $n$ jobs. Job $i$ is a finite sequence of tasks; each task names the processor that must process it and a processing time $p\ge0$. The tasks of a job are processed in their order: a task may start only after the job's previous task has completed. A flow shop is the special case in which every job has $m$ tasks and its $k$-th task runs on $P_k$.

A non-preemptive schedule gives every task a start time $s\ge0$; the task then occupies its processor during $[s,s+p)$, and two distinct tasks on one processor never overlap. The finish time $f_i(S)$ of job $i$ in schedule $S$ is the time at which all tasks of job $i$ have been completed, and the mean flow time is

$$\mathrm{MFT}(S)=\frac1n\sum_{i=1}^n f_i(S).$$

An OMFT schedule $S^*$ is a feasible schedule of least mean flow time.

Let $L_i$ be the sum of the task times of job $i$. An SPT order is a listing $\sigma(0),\dots,\sigma(n-1)$ of the jobs with $L_{\sigma(0)}\le\dots\le L_{\sigma(n-1)}$, ties broken arbitrarily. The SPT schedule processes the jobs in that order: each job in turn, each positive-time task starting at the later of the completion of the job's previous task and the latest completion of a task already placed on its processor. A zero-time task completes when its preceding task completes and leaves the processor available.

Formalization targets

Goal: Lemma 9

For every job shop, every SPT order $\sigma$ with SPT schedule $S$, and every feasible non-preemptive schedule $\tau$,

$$\mathrm{MFT}(S)\le m\cdot\mathrm{MFT}(\tau),$$

so that $\mathrm{MFT}(S)/\mathrm{MFT}(S^*)\le m$ for an OMFT schedule $S^*$. A separate item states the same bound for flow shops.

Milestones

The milestones follow the paper's proof of Lemma 9 on p. 47:

1. the SPT schedule is a feasible schedule;
2. the job in position $k$ of the SPT schedule finishes by $\sum_{j\le k}L_{\sigma(j)}$;
3. in any feasible schedule, if $i_1,\dots,i_n$ is the order in which the jobs finish, then $f_{i_k}\ge\sum_{j\le k}L_{i_j}/m$;
4. a prefix sum of any listing of the $L_i$ is at least the corresponding prefix sum of the sorted listing;
5. $\mathrm{MFT}(S^*)\ge\frac1n\sum_{k=1}^n\sum_{j=1}^k L_j/m$.

Significance

Lemma 9 is one of the earliest performance guarantees for a shop-scheduling heuristic under a sum objective. It shows that a rule computable by one sort, $O(n\log n)$ plus a linear pass, is within a factor equal to the number of machines, independently of the number of jobs. This is better than the factor $n$ that Lemma 8 of the same paper gives for an arbitrary busy schedule, whenever $m<n$. Example 2 of the paper shows that the factor cannot be improved for SPT. Lower bounds of the work-per-machine type used here recur in later approximation results for total completion time in shops and on parallel machines.

The result has been proved since 1978. As far as a search of the Prove2Me catalogue shows, it has not been machine-checked. This mission adds a machine-checked statement of the SPT schedule as an algorithm, not as an arbitrary schedule with a property. It also adds the guarantee for job shops with arbitrary task sequences, of which flow shops are a special case.

Difficulty

The arithmetic of the proof is short. The work is in two places. The SPT schedule is a concrete construction, a fold over jobs and tasks that updates processor availability, so the bound on its finish times has to be carried through an invariant of that construction. The lower bound on every feasible schedule needs a packing argument: tasks on one processor that complete by a given time have total length at most that time. That argument is not available in Mathlib in a form that applies here. The tempting shortcut of comparing the two schedules job by job fails: the optimal schedule need not finish jobs in SPT order, so the comparison must go through sums of sorted prefixes.

Formalization scope

• Instance and feasibility. The job data come from the published JobShopLTAS.Core.Instance (jobs Fin n, processors Fin m, tasks Fin (μ j), real processing times $\ge0$). The local IsPaperFeasibleSchedule requires nonnegative starts, in-job order, and no overlap of positive-time tasks on the same processor. Zero-time tasks occupy no processor interval. The paper assumes $m\ge1$, and the scheduling theorems carry that hypothesis.
• Finish time and MFT. $f_i$ is the maximum completion time over the tasks of job $i$, with baseline $0$; MFT divides by $n$, and for $n=0$ both sides are $0$.
• The SPT schedule is the list schedule constructed by the heuristic, for every SPT order, so ties are broken in every possible way. Zero-time tasks do not advance processor availability. It is not "any feasible schedule whose jobs finish in SPT order", a reading under which an optimal schedule would qualify and the goal would be trivial.
• The optimum. The paper's "Let $S^*$ be an OMFT schedule" is stated as "for every feasible non-preemptive schedule $\tau$". This is equivalent and does not assume that an optimum exists.
• Ratios multiplied out. $\mathrm{MFT}(S)/\mathrm{MFT}(S^*)\le m$ is stated as $\mathrm{MFT}(S)\le m\cdot\mathrm{MFT}(\tau)$, and the proof's bounds divided by $m$ are multiplied by $m$. No division by a possibly zero quantity occurs.
• Constants. The only constant is the factor $m$, the number of processors.
• Not formalized. The running time of SPT, the comparison with Lemma 8 and its remark "it is assumed that $m<n$" (not a hypothesis of Lemma 9), and the tightness Example 2.
• Milestones 2 and 4 are stated for every listing $\sigma$ and every pair of listings; they are combinatorial facts about list schedules and sorted sums that are reusable beyond this mission. Proofs of any milestone, and a reusable packing lemma for non-overlapping intervals, are welcome.

Selected references

• T. Gonzalez, S. Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1), 36–52, 1978. https://doi.org/10.1287/opre.26.1.36
• R. W. Conway, W. L. Maxwell, L. W. Miller, Theory of Scheduling, Addison-Wesley, 1967.
• W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3, 59–66, 1956. https://doi.org/10.1002/nav.3800030106
• K. Jansen, R. Solis-Oba, M. Sviridenko, Makespan Minimization in Job Shops: A Linear Time Approximation Scheme, SIAM J. Discrete Math. 16(2), 288–300, 2003 (source of the job-shop definition reused here). https://doi.org/10.1137/S0895480199363908

Motivation

In a job shop, each job has an ordered list of tasks, and each task must use a specified machine. A production planner may be able to interrupt a task and resume it later, yet still be unable to find a short schedule efficiently. Gonzalez and Sahni studied how the ability to preempt changes the difficulty of minimizing the time at which all jobs are complete. Their 1978 paper establishes complexity results for flow shops and job shops and then examines approximation schedules when exact optimization is difficult (Gonzalez and Sahni, 1978).

This mission concerns the paper's two-machine construction from 3-PARTITION. It is the reduction used for their claim that finding an optimal preemptive or non-preemptive finish-time schedule remains NP-complete when input size is measured by the sum of task lengths. The formal target isolates the decision equivalence proved for the constructed instance. It gives solvers a precise schedule statement to establish without conflating the scheduling theorem with the separate complexity-class argument.

Setting

A 3-PARTITION input $C$ comprises an integer $t\ge0$, a positive integer target $B$, and $s=3t$ positive integer sizes $a_1,\ldots,a_s$. A valid input satisfies

$$\sum_{i=1}^{s}a_i=tB,\qquad B/4<a_i<B/2\quad(1\le i\le s).$$

It has a 3-partition when the $s$ indices can be assigned to $t$ disjoint groups, each containing exactly three indices and having total size $B$. The strict bounds rule out groups of other cardinalities at that sum and are part of the source problem, not a convenience added for formalization. When $t=0$, the input has no sizes or groups and the empty grouping is a solution.

The paper builds a job shop $JS(C)$ with machines $P_1,P_2$ and $s+1$ jobs. For $1\le i\le s$, job $i$ has a task of length $a_i$ on $P_1$, followed by a task of length $a_i$ on $P_2$. The last job, $s+1$, has $2t$ tasks, each of length $B$. Its tasks alternate between the machines, starting on $P_2$. This last order matters: reversing it would produce a different construction. The source gives the decision threshold $\tau=2tB$ (Lemma 7, p. 44).

A non-preemptive schedule gives each task one continuous processing interval. A preemptive schedule may divide an operation into finitely many positive-length intervals. In either case, jobs obey their task order, distinct pieces on the same machine do not overlap, and processing starts at or after time zero. Write $FT(S)$ for the time at which all tasks of schedule $S$ have finished. The paper allows the same job to revisit a machine, as the final job does here.

Formalization targets

Lemma 7: the constructed instance

For every valid $C$, the main goal states both the paper's preemptive equivalence and the non-preemptive form established by its two directions:

$$\begin{aligned} \exists S\text{ preemptive for }JS(C): FT(S)\le2tB &\iff C\text{ has a 3-partition},\\ \exists S\text{ non-preemptive for }JS(C): FT(S)\le2tB &\iff C\text{ has a 3-partition}. \end{aligned}$$

The milestones follow the source's proof text: the schedule supplied by a solution in Lemma 7(a), the timing forced on the final job, the exclusion of short preemptive schedules in Lemma 7(b), and the preemptive equivalence stated in the proof. The final-job milestone describes the occupied time slots of the paper's Figure 4, independently of how many adjacent pieces a formal schedule uses.

Significance

The equivalence transfers the distinction between solvable and unsolvable 3-PARTITION inputs to an exact finish-time threshold in a job shop with only two machines. It also establishes the non-preemptive decision equivalence for this construction, because a solution yields a non-preemptive schedule while an unsolvable input rules out even the more permissive preemptive schedules. These facts supply the scheduling part of the paper's strong NP-completeness claim; membership in NP is handled separately by Lemma 6 (pp. 44–45).

The result is proved in the source paper. The work proposed here is a machine-checked development of its explicit reduction equivalence and the finite-piece scheduling model needed to state it. The milestone theorems expose statements that can be reused when formalizing other preemptive scheduling reductions. The shared job-shop instance and 3-PARTITION input are already published definitions; the particular reduction instance and preemptive schedule predicate are new local definitions.

Difficulty

Preemption makes a task's processing time distributable across intervals. Merely checking that each machine has enough total capacity does not characterize feasible schedules: every job's operations must still occur in order, and pieces of different jobs must avoid one another on each machine. The converse direction must constrain every preemptive schedule that meets the threshold, not only a schedule having the visual pattern in Figure 4. A schedule can also represent one uninterrupted interval as several adjacent pieces, so piece count alone cannot express the source's timing claim.

Formalization scope

Machines are Fin 2, with $P_1$ numbered $0$ and $P_2$ numbered $1$. Jobs are Fin (3t+1); the final job is index $3t$. Its zero-based operation $i$ uses machine $1$ for even $i$ and machine $0$ for odd $i$. The definition uses the published JobShopLTAS.Core.Instance for ordered operations, machines, real processing times, and non-preemptive feasibility. It uses the published ResourceScheduling.Chain.ThreePartition for $t,B,a_i$, validity, and solutions. Those objects have the same conventions as the paper here. The local preemptive model uses finitely many positive-length pieces per task, whose durations sum exactly to that task's processing time. The threshold is the explicit real cast of $2tB$; no real infimum or division by a possibly zero optimum appears.

The goal is specific to the instance the paper constructs from each valid input. A free job-shop instance, a freely chosen schedule, or an extra hypothesis that the input has a solution would erase the reduction's content. Validity carries $B>0$, total $tB$, and both strict bounds on each $a_i$. The case $t=0$ remains in scope: the constructed job has no tasks and its finish-time threshold is zero. All existing tasks have positive length whenever the input is valid, so the published non-preemptive predicate's treatment of zero-length tasks does not affect this mission.

The paper states “3-Partition $\alpha$ preemptive JOFT with $m=2$” and connects it to NP-completeness for preemptive and non-preemptive scheduling when complexity is measured by the sum of task lengths. The Lean theorem states the proof's two decision equivalences with constant $2tB$ and machine count $2$. It does not formalize $\alpha$ as a polynomial-time many-one reduction, the unary task-length measure, NP-completeness, or Lemma 6's NP-membership argument. Contributions that establish the reduction statements, the schedule construction, or general finite-piece scheduling facts are within scope.

Selected references

• Teofilo Gonzalez and Sartaj Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1), 1978, pp. 36–52. DOI: 10.1287/opre.26.1.36.

Motivation

Shop scheduling asks how to process a set of jobs, each a sequence of tasks on prescribed machines, so that all work is completed as early as possible. The flow shop, in which every job visits the machines in the same order, is the most studied of these models in operations research. For two machines, Johnson's rule (1954) computes a schedule of minimum finish time in $O(n\log n)$ time, and for two machines allowing interruptions (preemption) does not help. Garey, Johnson and Sethi (Math. Oper. Res. 1976) and Brucker, Lenstra and Rinnooy Kan (Mathematisch Centrum report BW 43/75, 1975; Ann. Discrete Math. 1977) showed that the non-preemptive problem becomes NP-complete with three machines.

Gonzalez and Sahni (Operations Research, 1978) extended this picture to preemptive schedules. Their Theorem 1 shows that minimizing the finish time of a three-machine flow shop is NP-complete with or without preemption, even when every job has at most two tasks of nonzero length. When every job has only one task the problem is trivial, so this is the simplest NP-complete case of the flow-shop finish-time problem. The result explains why no exact polynomial algorithm is expected and motivates the approximation results in the second half of the same paper.

Timeline:

• 1954: Johnson, two-machine flow shop, optimal non-preemptive rule.
• 1975: Brucker, Lenstra, Rinnooy Kan: non-preemptive three-machine flow shop NP-complete, including the case of two nonzero tasks per job (the paper's Corollary 1, which it says "is also obtained in [1]").
• 1976: Garey, Johnson, Sethi: non-preemptive three-machine flow shop NP-complete even when the problem size is the sum of the task lengths.
• 1978: Gonzalez, Sahni: the preemptive three-machine flow shop is NP-complete, by a reduction from PARTITION that also covers the non-preemptive case with two nonzero tasks per job.

Setting

A flow shop has $m\ge1$ processors $P_1,\dots,P_m$ and a finite set of jobs. Task $j$ of job $i$ must be processed on $P_j$ for $t_{j,i}\ge 0$ time units, and it can start only after task $j-1$ of the same job is completed. Task times may be zero. The schedule starts at time $0$.

A preemptive schedule gives every task a finite set of pieces $(s,f)$ with $0\le s<f$: the task is processed on its processor during $[s,f)$. Pieces on the same processor do not overlap, the pieces of a task have total length $t_{j,i}$, and every piece of a task starts after every piece of the earlier tasks of the same job has ended. A non-preemptive schedule processes every task in at most one piece. For a schedule $S$, $f_i(S)$ is the time at which job $i$ is completed and the finish time is $\mathrm{FT}(S)=\max_i f_i(S)$.

PARTITION. A multiset $S=\{a_1,\dots,a_n\}$ of nonnegative integers has a partition if some set $u$ of indices satisfies $\sum_{i\in u}a_i=\tfrac12\sum_{i=1}^n a_i$.

The instance FS. With $T=\sum_i a_i$, the flow shop $\mathrm{FS}$ has $m=3$ processors and $n+2$ jobs:

$$t_{\cdot,i}=(a_i,0,a_i)\ (1\le i\le n),\qquad t_{\cdot,n+1}=(T/2,\,T,\,0),\qquad t_{\cdot,n+2}=(0,\,T,\,T/2),$$

and the threshold is $\tau=2T$. Every job has at most two nonzero tasks.

Formalization targets

Goal: Theorem 1 (p. 38)

For every $n$ and every $a_1,\dots,a_n\in\mathbb N$:

$$\mathrm{FS}\ \text{has at most two nonzero tasks per job},$$ $$\big(\exists\,S'\ \text{preemptive},\ \mathrm{FT}(S')\le 2T\big)\iff S\ \text{has a partition},$$ $$\big(\exists\,S'\ \text{non-preemptive},\ \mathrm{FT}(S')\le 2T\big)\iff S\ \text{has a partition}.$$

Milestones

• Lemma 1(a) (p. 39): a partition of $S$ yields a non-preemptive schedule of FS with $\mathrm{FT}=2T$ (Figure 1).
• Observations (i)–(ii) (p. 39): in any preemptive schedule with $\mathrm{FT}\le 2T$, task $t_{1,n+1}$ ends by $T$ and task $t_{3,n+2}$ starts no earlier than $T$.
• Lemma 1(b) (p. 39): if $S$ has no partition, every preemptive schedule of FS has $\mathrm{FT}>2T$.
• Lemma 1 (p. 38): the preemptive equivalence.
• Corollary 1 (p. 39): the non-preemptive equivalence.

Significance

The result. The equivalence shows that a polynomial-time algorithm deciding whether a three-machine flow shop (with two nonzero tasks per job) has a schedule of finish time at most $\tau$, preemptive or not, would decide PARTITION in polynomial time. With membership in NP (the paper's Lemma 2) it gives NP-completeness of both versions. It also marks the boundary with the polynomial cases: $m=2$ (Johnson's rule), and jobs with a single task.

Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge no machine-checked proof of this reduction exists, and the platform has no formal model of preemptive shop schedules. The mission produces one: a piece-based preemptive schedule with zero task times, which subsumes the non-preemptive case, together with the first formal NP-hardness reduction for preemptive flow shops on the platform.

Difficulty

Direction (a) asks for one explicit schedule. Direction (b) must rule out every preemptive schedule of FS, and preemption is exactly what makes this delicate: a task may be split into any finite number of pieces placed anywhere on its processor, so the naive intuition that a failed partition leaves "unusable gaps" is no longer evident, since pieces of different jobs can be interleaved to fill gaps. A correct argument must therefore be an accounting of processor time over the pieces, valid for any number and position of pieces, and it must treat zero-length tasks, which occupy no processor time but still delay the next task of their job. Finally, the non-preemptive equivalence is not a formal consequence of the preemptive one alone: it uses that (a) produces a non-preemptive schedule and that (b) holds for all preemptive schedules, which include the non-preemptive ones.

Formalization scope

• Processors are Fin 3 ($P_1,P_2,P_3$ = 0, 1, 2), jobs of FS are Fin n ⊕ Fin 2 (Sum.inr 0 is job $n+1$, Sum.inr 1 is job $n+2$). Task times are real numbers; the PARTITION data are a : Fin n → ℕ, and "has a partition" is $2\sum_{i\in u}a_i=\sum_i a_i$ in $\mathbb N$.
• A schedule is a Finset of pieces $(s,f)$ per task with the four conditions of the Setting. Non-preemptive means at most one piece per task. Zero tasks have no pieces and occupy no processor time. $f_i(S)$ and $\mathrm{FT}(S)$ are maxima with baseline $0$.
• Explicit constants: $T=\sum_i a_i$, the times $T/2$ and $T$ of jobs $n+1,n+2$, and the threshold $\tau=2T$, as on p. 39. Lemma 1(a) states finish time exactly $2T$, as the paper does.
• Not formalized: "NP-complete", the reducibility relation "$\alpha$", membership in NP (Lemma 2, p. 40) and the polynomial computability of FS from $S$. The paper states Theorem 1, Lemma 1 and Corollary 1 as complexity claims. Their proofs establish the equivalences above for the constructed instance, and those equivalences are what is formalized.
• No trivializing reading is admitted: the statements concern the specific instance FS built from $a$, not an arbitrary flow shop, and the schedule model rules out overlapping pieces and out-of-order tasks while still allowing zero tasks. A sorry-free check confirms that Figure 1 is a valid non-preemptive schedule of FS for $S=\{1,1\}$.
• Reusable beyond this mission: the flow-shop model with preemptive pieces, and PARTITION. Proofs of the milestones and a proof of the goal from them are welcome.

Selected references

• T. Gonzalez, S. Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1), 36–52, 1978. https://doi.org/10.1287/opre.26.1.36
• M. R. Garey, D. S. Johnson, R. Sethi, The Complexity of Flowshop and Jobshop Scheduling, Mathematics of Operations Research 1(2), 117–129, 1976. https://doi.org/10.1287/moor.1.2.117
• S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1), 61–68, 1954. https://doi.org/10.1002/nav.3800010110
• P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum report BW 43/75, 1975; Annals of Discrete Mathematics 1, 343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
• R. M. Karp, Reducibility among Combinatorial Problems, in Complexity of Computer Computations, Plenum, 85–103, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9

Motivation

A finite Markov decision system asks how to choose actions while a changing state controls which actions are available. The choice can affect both the reward now and the distribution of future states. In a total-reward problem, the process can continue indefinitely; if transitions are substochastic, it can also terminate. Kallenberg's treatment of positive dynamic programming connects this control problem to a finite linear program and uses an optimal flow to identify a policy that is optimal from every initial state Kallenberg, Chapter 3.

The connection matters when an optimizer is easier to compute as state-action frequencies than as an infinite sequence of decisions. A policy may depend on the entire observed history and may randomize at every decision. The theorem under study says that, when the dual linear program has an extreme optimal solution, its positive coordinates identify a pure stationary policy as good as every such general policy. This assertion includes models in which the selected policy is not transient Kallenberg, Theorem 3.5.2 and Example 3.5.1.

Setting

Let $E=\{1,\ldots,N\}$ be a nonempty finite state space. At state $i$, one chooses an action from the nonempty finite set $A(i)$. Action $a\in A(i)$ earns a real reward $r_{ia}$ and moves to state $j$ with probability $p_{iaj}\ge0$. The sum $\sum_jp_{iaj}$ is at most one; any missing probability represents termination. Positive dynamic programming imposes $r_{ia}\ge0$ for every admissible state-action pair Kallenberg, Section 2.2 and Assumption 3.5.1.

A policy $R=(\pi^1,\pi^2,\ldots)$ assigns an action distribution after each finite history. The history records the initial state and all states and actions observed so far. Write $C$ for this full policy class. A pure stationary policy $f^\infty$ always chooses one fixed admissible action $f(i)$ whenever it visits $i$.

Starting from state $i$, let $v_i(R)$ be the expected total reward of $R$, and let $v_i=\sup_{R\in C}v_i(R)$. Because the rewards are nonnegative, the finite-horizon expected totals increase to $v_i(R)$; both policy and optimal values may be $+\infty$. A real vector $w=(w_i)$ is TMD superharmonic if $w_i\ge r_{ia}+\sum_jp_{iaj}w_j$ for each $i$ and $a\in A(i)$ Kallenberg, Definition 3.3.1.

For given weights $\beta_j>0$, equation (3.5.2) is a linear program over nonnegative state-action flows $x_{ia}$. It maximizes $\sum_{i,a}r_{ia}x_{ia}$ subject to

$$\sum_{a\in A(j)}x_{ja}-\sum_{i\in E}\sum_{a\in A(i)}p_{iaj}x_{ia}\le\beta_j\qquad(j\in E).$$

The set $E_x=\{i:\sum_{a\in A(i)}x_{ia}>0\}$ records the states with positive flow Kallenberg, Notation 3.1.1 and equation (3.5.2).

Formalization targets

Superharmonic value

Theorem 3.5.1 identifies $v$ as the smallest nonnegative TMD-superharmonic vector. The original superharmonic definition ranges over real vectors; the value must also be allowed to take $+\infty$. The formal statement gives both the extended superharmonic inequalities for $v$ and its componentwise bound by every nonnegative real superharmonic vector:

$$0\le v_i,\qquad v_i\ge r_{ia}+\sum_jp_{iaj}v_j,\qquad v_i\le w_i\quad\text{for every nonnegative real superharmonic }w.$$

This is the numbered milestone of the mission Kallenberg, Theorem 3.5.1.

Policy from an extreme optimal dual flow

The main goal is Theorem 3.5.2. Suppose $x^*$ is an extreme point of the feasible region of (3.5.2) and has objective at least as large as every feasible flow. Then every pure stationary rule $f$ choosing $x^*_{i,f(i)}>0$ on $E_{x^*}$, with arbitrary admissible actions outside $E_{x^*}$, is total optimal:

$$v_i(f^\infty)=v_i=\sup_{R\in C}v_i(R)\qquad(i\in E).$$

The goal records the finite-optimum case by requiring an actual optimal solution $x^*$; it makes no extra assumption that every policy is transient Kallenberg, Theorem 3.5.2.

Significance

The theorem converts an extreme optimal state-action flow into one decision rule that is optimal simultaneously for all starting states. Since $C$ includes policies that change with time, use full histories or randomize, it establishes that those freedoms cannot improve the total-reward value when the stated dual optimizer exists. The positive model also reveals when extended values matter: outside the finite-optimum case, the dual objective may be unbounded and an optimal total reward may be infinite Kallenberg, pp. 78–83.

A formal development of this result must keep the policy class and the linear program in the same model. It provides reusable definitions of a finite substochastic control system, finite-history probabilities, extended total rewards, state-action flows and superharmonic vectors. The result is proved in the book; the mission asks for a machine-checked proof of its statement, not for a new optimization theorem. The draft statements are open goals until such proofs are supplied.

Difficulty

A finite linear program has finitely many variables, while the value compares a flow-derived rule with every infinite, history dependent policy. A comparison restricted to stationary or transient policies would miss the main assertion. The proof also has to treat zero-flow states: the dual solution does not prescribe an action there, yet the theorem permits every admissible choice. Finally, the superharmonic milestone permits an infinite value, while the linear program itself uses real coordinates. A development must connect those representations without turning an infinite reward into an arbitrary default real value.

Formalization scope

Lean represents states as Fin N with $N>0$, and each $A(i)$ as a nonempty finite subset of a finite action type. The transition rows sum to at most one. Histories carry past states and actions, and the first action has internal index zero, corresponding to the book's time one. Policy probabilities are nonnegative, vanish outside $A(i)$ and sum to one. The expected reward of a finite horizon is a finite sum over histories; nonnegative total reward is its supremum in EReal. The value takes the supremum over the full policy type, not over a restricted policy subclass.

Dual flow coordinates exist only for admissible state-action pairs. Extreme points are taken in the feasible set of (3.5.2) in those coordinates, and its balance constraints retain the source's $\le\beta_j$ direction. The goal quantifies over every admissible pure rule satisfying the positive-flow condition. These choices exclude the vacuous shortcut of defining the value using only pure stationary policies or assuming optimality as a hypothesis.

The mathematical infrastructure includes finite policy histories, state-action occupancy probabilities, extended nonnegative reward limits, the real flow polyhedron and its extreme points. The history and flow definitions can support later work on other finite decision models. Contributions to those foundational results and to the full comparison with history dependent policies are within the mission's scope. The negative-reward regime of Section 3.6, whose claims involve average optimality and recurrent classes in an extended stochastic model, requires its own representation and is outside this positive-reward target.

Selected references

• L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983. Publisher repository.

Motivation

Every pure integer program, once its linear programming relaxation has been solved, can be relaxed further to a problem over a finite Abelian group: the nonbasic variables must satisfy a single congruence in the group of the optimal basis. R. E. Gomory introduced this relaxation in 1965 and studied the convex hull of its solutions in Some polyhedra related to combinatorial problems (Linear Algebra Appl. 2 (1969), 451–558, doi:10.1016/0024-3795(69)90017-2). The facets of these group polyhedra are valid inequalities for every integer program whose basis produces the same group, and they became the source of cutting planes for integer programming: Gomory's mixed-integer cut and the later theory of corner polyhedra and subadditive valid inequalities descend from them.

The number of facets grows fast with the order of the group, so a list of facets for each group is not a usable description. Section 3D of the paper, "Lifting up Faces", gives a structural tool instead: facets of the polyhedron of a small group produce facets of the polyhedron of every larger group that maps onto it. This mission formalizes that construction (THEOREM 19) and its converse (THEOREM 20).

Setting

Let $\mathcal G$ be a finite Abelian group, written additively, with zero $\bar 0$ and order $D=|\mathcal G|$, and let $\mathcal G^+=\mathcal G-\{\bar 0\}$. For a right-hand side $g_0\in\mathcal G$, the group equation asks for nonnegative integers $t(g)$, $g\in\mathcal G^+$, with

$$\sum_{g\in\mathcal G^+}t(g)\cdot g=g_0 .$$

Its solution set is $T(\mathcal G,g_0)$; when $g_0=\bar 0$, the zero solution is excluded, as stipulated on p. 474. Each solution is a point of $\mathbb R^{\mathcal G^+}$, a space of dimension $n'=D-1$, and the master polyhedron $P(\mathcal G,g_0)$ is the convex hull of $T(\mathcal G,g_0)$. Gomory reads a solution $t$ as a path from $\bar 0$ to $g_0$ that uses the element $g$ exactly $t(g)$ times; with arc lengths $\pi(g)$ its length is $\pi\cdot t=\sum_g\pi(g)t(g)$.

An inequality $\pi\cdot t\ge\pi_0$, written $(\pi,\pi_0)$, is a face of $P(\mathcal G,g_0)$ when $\pi\ne0$, every $t\in T(\mathcal G,g_0)$ satisfies it, and the solutions on the hyperplane $\pi\cdot t=\pi_0$ generate that hyperplane: every point of it is a weighted sum, with total weight 1, of such solutions. A face is therefore a facet; Gomory says "face" throughout, and so does this mission. The solutions with $\pi\cdot t=\pi_0$ are the minimal paths.

Let $\psi$ be a homomorphism of $\mathcal G$ onto a second finite Abelian group $\mathcal H$, with kernel $\mathcal K=\psi^{-1}(\bar 0)$. A coefficient vector $\pi'$ on $\mathcal H^+$ is lifted to $\mathcal G^+$ by

$$\pi(g)=\pi'(\psi g),\qquad \pi'(\bar 0)=0,$$

so that every element of the kernel gets coefficient $0$.

Formalization targets

Goal: THEOREM 19 (p. 486)

If $\psi g_0\ne\bar 0$ and $(\pi',\pi_0)$ is a face of $P(\mathcal H,\psi g_0)$ with $\pi_0>0$, then

$$\Big(\pi,\pi_0\Big),\quad \pi(g)=\pi'(\psi g),\quad\text{is a face of } P(\mathcal G,g_0).$$

For instance, the face $t_1\ge1$ of $P(\mathcal G_2,(1))$ lifts through reduction mod 2 to the face $t_1+0t_2+t_3+0t_4+t_5\ge1$ of $P(\mathcal G_6,(5))$ (p. 488).

Milestones

1. Face criterion (p. 469, proof of THEOREM 7). For $\pi_0>0$, $(\pi,\pi_0)$ is a face iff it is valid on $T$ and $n'$ linearly independent solutions satisfy $\pi\cdot t=\pi_0$.
2. Pushing paths forward (p. 486). A solution $t$ for $\mathcal G$ maps to the solution $\tau(h)=\sum_{g\in\psi^{-1}h}t(g)$ for $\mathcal H$ of the same length; hence the lifted inequality is valid.
3. Lifted minimal paths (p. 487). From a minimal path $\tau$ for $\mathcal H$ and a kernel element $k$, the path $T_k(\tau)$ is a minimal path for $\mathcal G$.
4. Rank $D-1$ (pp. 487–488). The lifted inequality has $D-1$ linearly independent minimal paths.

Further result: THEOREM 20 (p. 489)

Conversely, a face $(\pi,\pi_0)$ of $P(\mathcal G,g_0)$ with $\pi_0>0$ and $\pi(g)=0$ for some $g\ne\bar0$ is the lift of a face of $P(\mathcal H,\psi g_0)$ for some $\psi$ of $\mathcal G$ onto a group $\mathcal H$ with $\psi g=\bar 0$.

Significance

THEOREMS 19 and 20 together say that the faces of $P(\mathcal G,g_0)$ with $\pi_0>0$ and a zero coefficient are exactly the faces lifted from proper quotients of $\mathcal G$. A catalogue of these positive-right-hand-side faces therefore only needs the faces with all coefficients positive; the rest come from smaller groups. Gomory uses this to explain the tables of Appendix 5: for $\mathcal G_{2,2}$ and $\mathcal G_{2,2,2}$ every such face is a lift of the single nontrivial face of $P(\mathcal G_2,(1))$, and for a direct sum $\mathcal G=\mathcal K_1\oplus\mathcal K_2$ every face of the polyhedron of a summand not containing $g_0$ extends to a face for $\mathcal G$ (p. 489). The same idea, sending facets of one group problem to facets of another by a homomorphism, recurs in the later theory of group relaxations and infinite group problems.

Both theorems are proved in the paper. To the knowledge of this mission, neither the group polyhedra, their faces nor the lifting theorem has a machine-checked formalization; the platform's other "lifting" results (lifted cover facets of the knapsack polytope, cone lifts of convex sets) are different notions. The mission produces a reusable definition layer for master group polyhedra and their faces, stated once for an arbitrary finite Abelian group, and a formal version of the passage between faces of a group and of its quotients.

Difficulty

Validity of the lifted inequality is a one-line computation (milestone 2). The content is that the lift is a facet: one must exhibit $D-1$ affinely independent solutions on the hyperplane, while the quotient face only supplies $|\mathcal H|-1$ of them. A solution of the quotient problem does not determine a solution for $\mathcal G$; coset representatives must be chosen and the path closed by a kernel element, and the kernel coordinates, which all have coefficient zero, must still be filled to full rank.

The obvious reduction, "a facet pulls back to a facet under a surjective map", fails here because the map from $\mathcal G$-paths to $\mathcal H$-paths is a linear projection from dimension $D-1$ to $|\mathcal H|-1$ and does not lift independence by itself. It also fails at $\pi_0=0$: with $\mathcal G=\mathbb Z_6$, $\mathcal H=\mathbb Z_3$, $g_0=1$, the face $t(1)\ge0$ of $P(\mathbb Z_3,(1))$ lifts to $t(1)+t(4)\ge0$, which is valid but not a face of $P(\mathbb Z_6,(1))$.

Formalization scope

The formalization uses one definition file for an arbitrary finite Abelian group ([AddCommGroup G] [Fintype G] [DecidableEq G]), instantiated at both $\mathcal G$ and $\mathcal H$. It commits to the following readings:

• Vectors are indexed by the subtype $\{g\mid g\ne\bar0\}$, so $\bar0$ has no coordinate and the dimension of T-space is $|\mathcal G|-1$ for each group separately; solutions are $\mathbb N$-valued, nonzero, and cast to $\mathbb R$. When $g_0\ne\bar0$, the group equation already excludes the zero vector.
• "Generated by the points on the hyperplane" means that the affine span of the tight solutions equals the hyperplane $\{x:\pi\cdot x=\pi_0\}$; $\pi\ne0$ is part of the definition and $\pi_0\ge0$ is not (THEOREM 6 proves it).
• Paths are vectors and "minimal path" means a solution with $\pi\cdot t=\pi_0$.
• $\pi'(\bar0)=0$ is built into the lift; "onto" is Function.Surjective ψ, and $g_0\notin\mathcal K$ is $\psi g_0\ne\bar0$.
• Added hypothesis $\pi_0>0$ in THEOREM 19 and the rank milestone: the page omits it, and the $\mathbb Z_6\to\mathbb Z_3$ example above shows the statement is false without it.
• The face criterion is THEOREM 7's "basic feasible solution" unfolded into $n'$ linearly independent tight solutions, stated for the master polyhedron only and for nontrivial groups, where $n'>0$.
• Pushing a path forward uses $\psi g_0\ne\bar0$, the standing hypothesis of THEOREM 19, so the pushed path cannot become the excluded zero solution.
• The lifted path $T_k(\tau)$ puts its closing $1$ on the kernel element $g_0-\sum_{g\notin\mathcal K}t_k(g)\cdot g$ itself, and adds nothing when that element is $\bar0$.
• In THEOREM 20, "nontrivial" is $\pi_0>0$, the printed $(\pi_1,\pi_0)$ is read as $(\pi,\pi_0)$, and the conclusion requires $\psi g=\bar0$ for the given zero coefficient: without it the identity map would satisfy the statement.

A formalization that proves only validity of the lift, or that defines faces without the generation condition (so that every valid inequality is a "face"), would be trivial and is ruled out by the definition of IsFace.

The development needs finite sums over fibres of $\psi$, a choice of coset representatives, and a rank argument for a block matrix with full-rank diagonal blocks. The definitions of $T$, $P(\mathcal G,g_0)$ and face are reusable for any further result on master group polyhedra. Proofs of the milestones in any order, alternative proofs of the face criterion, and a proof of THEOREM 20 are welcome.

Selected references

• R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra and Its Applications 2 (1969), 451–558. doi:10.1016/0024-3795(69)90017-2
• R. E. Gomory, On the relation between integer and noninteger solutions to linear programs, Proceedings of the National Academy of Sciences 53 (1965), 260–265. doi:10.1073/pnas.53.2.260
• R. E. Gomory and E. L. Johnson, Some continuous functions related to corner polyhedra, Mathematical Programming 3 (1972), 23–85. doi:10.1007/BF01584976