Combinatorics

Motivation

An integer program in standard form, $\max c\cdot x$ subject to $Ax=b$, $x\ge 0$, $x$ integer, is easy to state and hard to solve. Its linear programming relaxation is solved by the simplex method, which ends at an optimal basis $B$. The difference between the two problems is the integrality of $x$, and R. E. Gomory's 1969 paper Some polyhedra related to combinatorial problems (Linear Algebra Appl. 2, 451–558, doi:10.1016/0024-3795(69)90017-2) measures that difference with a finite Abelian group. Dropping only the nonnegativity of the basic variables leaves a problem whose feasible set has a simple structure: its convex hull is the corner polyhedron, and its integer points are the solutions of an equation in the group $\mathbb Z^m/B\mathbb Z^m$.

The first section of the paper uses this to explain when the integer program reduces to the group problem. Its asymptotic theorem says that if $b$ lies far enough inside the cone where $B$ is LP-optimal, then an optimal solution of the group problem gives an optimal integer solution. Gomory first proved this in 1965 (On the relation between integer and noninteger solutions to linear programs, PNAS 53, 260–265, doi:10.1073/pnas.53.2.260) by a counting argument on group solutions. The 1969 paper proves it again through the geometry of the corner polyhedron. The vertices of that polyhedron are irreducible, and an irreducible point is small. This is the version formalized here.

Setting

Let $A=(B,N)$ be an integer $m\times(m+n)$ matrix, with $B$ a nonsingular $m\times m$ matrix (the first $m$ columns) and $N$ the $m\times n$ matrix of the remaining columns $N_1,\dots,N_n$. As on p. 452 of the paper, $A$ contains an $m\times m$ unit matrix. Let $b\in\mathbb Z^m$ and $c=(c_B,c_N)\in\mathbb R^{m+n}$. The integer program (2) is

$$\max\ c\cdot x\quad\text{subject to}\quad Ax=b,\ x\ge 0,\ x\ \text{integer}.$$

The relative prices are $c_N^*=-c_N+c_BB^{-1}N$, with components $c^*_{m+i}$. $B$ is an optimal LP basis when $B^{-1}b\ge0$ and every $c^*_{m+i}\ge0$.

The group is $\mathcal G=M(I)/M(B)$, where $M(I)=\mathbb Z^m$ and $M(B)$ is the lattice of integer combinations of the columns of $B$. Let $f$ be the quotient map. $\mathcal G$ is finite of order $D=|\det B|$. Let $\mathcal N$ be the set of nonzero elements among $fN_1,\dots,fN_n$, and put $g_0=fb$. The group equation is

$$\sum_{g\in\mathcal N}t(g)\cdot g=g_0,\qquad t(g)\in\mathbb Z_{\ge0},$$

and $P(\mathcal G,\mathcal N,g_0)$ is the convex hull of its solutions in $\mathbb R^{\mathcal N}$. A nonnegative integer $t$ is irreducible if any two integer vectors $s,r$ with $0\le s,r\le t$ and $\sum s(g)\cdot g=\sum r(g)\cdot g$ are equal.

The group costs are $c^*(g)=\min_{i:\,fN_i=g}c^*_{m+i}$. Problem (8) minimizes $\sum_g c^*(g)t(g)$ over the solutions of the group equation. A corresponding vertex of a point $t^*$ (Remark 1) is a nonnegative integer $x_N^*$ with three properties: $t^*(g)=\sum_{i:\,fN_i=g}x^*_{m+i}$; at most one positive $x^*_{m+i}$ per group element; and $x^*_{m+i}=0$ when $fN_i=\bar0$. It uses only least cost columns when $x^*_{m+i}>0$ only if $c^*_{m+i}=c^*(fN_i)$.

The cone $K_B=\{y\in\mathbb R^m:B^{-1}y\ge0\}$ is where $B$ is LP-optimal. $K_B(d)$ is the set of its points at Euclidean distance at least $d$ from its frontier, and $l_{\max}$ is the largest Euclidean length of a column $N_i$.

Formalization targets

Goal: THEOREM 4 (p. 462)

If $b\in K_B\bigl(l_{\max}(D-1)\bigr)$, $t^*$ is a vertex of $P(\mathcal G,\mathcal N,fb)$ minimizing (8), and $x_N^*$ is a corresponding vertex using only least cost columns, then

$$x^*=\bigl(B^{-1}(b-Nx_N^*),\ x_N^*\bigr)\ \text{is an optimal integer solution of (2)}.$$

Milestones

1. THEOREM 1 (p. 459): an irreducible $t$ satisfies $\prod_{g\in\mathcal N}(1+t(g))\le|\mathcal G|$.
2. p. 459: $|M(I)/M(B)|=|\det B|$.
3. THEOREM 2 (p. 460): every vertex of $P(\mathcal G,\mathcal N,g_0)$ is an irreducible integer point.
4. Proof of THEOREM 4 (p. 462): an irreducible $t$ has $\sum_g t(g)\le|\mathcal G|-1$.
5. THEOREM 3 (p. 461): a corresponding vertex of a minimizing vertex is optimal for (2) whenever $B^{-1}(b-Nx_N^*)\ge0$.
6. Proof of THEOREM 4: $\|Nx_N^*\|\le l_{\max}(D-1)$.
7. Proof of THEOREM 4: $y\in K_B(d)$ and $\|v\|\le d$ imply $y-v\in K_B$.
8. Display (10), p. 464: the optimal $x^*$ of THEOREM 4 satisfies $\prod_{i=1}^n(1+x^*_{m+i})\le D$.

Significance

THEOREM 4 explains why integer programs with large right-hand sides are often easy. For $b$ outside a band of width $l_{\max}(D-1)$ along the boundary of the cone $K_B$, the integer optimum is the LP solution $B^{-1}b$ plus a correction that depends only on the class of $b$ modulo the lattice of $B$. That correction is periodic in $b$ and can be tabulated once for the $D$ group elements. The vertex form adds a structural statement: the correction can be read off a vertex of the corner polyhedron, so the faces and vertices of corner polyhedra (the subject of the rest of the paper) bear directly on integer programming. Display (10) shows such optimal solutions are small: their nonbasic parts satisfy $\prod(1+x_{m+i})\le D$.

All results here are proved in the paper. None of them is formalized yet. The 1965 version of the asymptotic theorem, posed as THEOREM 1 of the mission on Gomory (1965), is in the same family of statements. Its hypothesis is that the group solution is optimal; here the hypothesis is that it is a vertex of $P(\mathcal G,\mathcal N,g_0)$. Its counting lemma (a short optimal group solution) and its bound $\|Ny\|\le(D-1)l$ have counterparts in milestones 4 and 6.

Difficulty

An optimal solution of the group problem need not be short. Group solutions can be made longer without changing their cost (add a zero-cost cycle), and a long nonbasic part $x_N$ can push $b-Nx_N$ out of the cone $K_B$, making $x_B$ negative. The goal must therefore use the vertex hypothesis. Vertices are irreducible (THEOREM 2), and irreducibility bounds their size through a pigeonhole count in the finite group (THEOREM 1). The formal work is spread across three settings: the convex geometry of the hull of an infinite integer set, the arithmetic of the quotient $\mathbb Z^m/B\mathbb Z^m$ and its order, and the linear algebra connecting $B^{-1}$, the cone $K_B$ and its frontier.

Formalization scope

Vectors on $\mathcal N$ are functions on the subtype of a Finset of the group. Integer solutions are $\mathbb N$-valued, and $P(\mathcal G,\mathcal N,g_0)$ is convexHull ℝ of their real images. THEOREMS 1 and 2 are stated for an arbitrary finite Abelian group and any finite $\mathcal N$ not containing $0$, as in the paper. The integer program uses the basis as the first $m$ columns, Fin m ⊕ Fin n. $B^{-1}$ is the real matrix inverse, and every statement assumes $\det B\ne0$. Optimality of $x$ means feasibility plus $c\cdot y\le c\cdot x$ for every feasible integer $y$; no supremum is taken. The loose phrases of the paper are read as follows.

• "Vertex" means an extreme point.
• "Every vertex is irreducible" means every vertex is the image of an integer solution, and that solution is irreducible.
• "Optimal linear programming basis" means $B^{-1}b\ge0$ and $c^*\ge0$.
• "Corresponding vertex $x^*$ of $P_x(B,N,b)$" means conditions (i)–(iii) of Remark 1, which the paper calls easily verified, taken as the definition.
• "Minimizing (8)" means minimizing over the integer solutions of the group equation.
• "Euclidean distance from the frontier" is explicit: $\sqrt{\sum_k v_k^2}$, frontier in the usual topology, so $K_B(0)=K_B$.

The printed slip on p. 462 ($\sum(1+t^*(g))$ for THEOREM 1's product) is corrected in the Lean. Dropping the vertex hypothesis from the goal is not a valid formalization (the statement becomes false in general), and neither is defining irreducibility with real $r,s$ (THEOREM 1 then fails). The existence of a minimizing vertex, which the paper takes for granted, is not posed.

A complete development needs the finiteness and order of $\mathbb Z^m/B\mathbb Z^m$ (Mathlib's AddSubgroup.index_eq_natAbs_det), extreme points of convex hulls (extremePoints_convexHull_subset), and an argument that a closed cone with $y$ deep inside it contains the ball around $y$. The group-polyhedron definitions and THEOREMS 1–2 apply to any finite Abelian group and are reusable beyond this mission. Proofs of any milestone are welcome independently.

Selected references

• R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra and Its Applications 2 (1969), 451–558. https://doi.org/10.1016/0024-3795(69)90017-2
• R. E. Gomory, On the relation between integer and noninteger solutions to linear programs, Proc. Nat. Acad. Sci. USA 53 (1965), 260–265. https://doi.org/10.1073/pnas.53.2.260
• R. E. Gomory, Faces of an integer polyhedron, Proc. Nat. Acad. Sci. USA 57 (1967), 16–18. https://doi.org/10.1073/pnas.57.1.16
• B. L. van der Waerden, Modern Algebra, English translation of the 2nd German edition, Ungar, New York, 1949–1950 (computation of $f$, cited p. 456).

Motivation

Scheduling work on several identical processors creates a plausible expectation: completing tasks sooner, removing constraints, or adding a processor should not delay the overall finish. A fixed priority-list rule defeats that expectation. When a task becomes ready earlier, it can occupy a processor that would otherwise have run another task; that decision changes later availability. Graham gives explicit schedules in which changing only the list raises the finishing time from 12 to 14, removing two precedence constraints raises it to 16, shortening every task raises it to 13, or adding one processor raises it to 15. These examples establish that the effect is a property of the scheduling rule, rather than of a change in the total set of tasks. See Graham, §2, pp. 417–419.

This mission concerns the upper limit of that effect. An operations researcher comparing a list schedule before and after a change in available processors or task data needs a bound that survives all four changes at once. The result is also a compact benchmark for formalizing algorithms whose behavior depends on changing availability: the model must describe when tasks become ready, when processors are idle, and which ready task a processor takes next. Graham's Theorem 1, proved in the 1969 paper, supplies the bound.

Setting

There are $r$ tasks $T_1,\ldots,T_r$ and $n$ identical processors. Each task $T_j$ has a positive processing time $\mu(T_j)$. A strict precedence order $\prec$ specifies tasks that must be completed first: $T_i\prec T_j$ means $T_j$ cannot start before $T_i$ ends. A priority list $L$ orders all tasks once each. It may place a successor before a predecessor, because the processor skips any task that is not ready. These conventions are those of Graham's system in §2, p. 416.

A schedule gives each task a processor and a start time $S_j\ge0$. Once started, the task occupies that processor continuously on $[S_j,S_j+\mu(T_j))$. Two tasks on one processor cannot overlap, while tasks may meet at an endpoint. Precedence means $S_i+\mu(T_i)\le S_j$ whenever $T_i\prec T_j$. The finishing time $\omega$ is the largest completion time $S_j+\mu(T_j)$. The paper's list rule starts the first currently ready task in $L$ whenever a processor can take a task. A ready task that has not started cannot coexist with an idle processor. If one task starts while another ready task waits, the started task is earlier in $L$.

The same task set is run a second time, with processing times $\mu'$, order $\prec'$, list $L'$, processor count $n'$, and finishing time $\omega'$. The data satisfy $\mu'(T_j)\le\mu(T_j)$ for every $j$ and $\prec'\subseteq\prec$. Thus the second run may have shorter tasks and fewer precedence relations; both lists may differ arbitrarily. Both runs obey the same list-scheduling rule Graham, §3, p. 419.

Formalization targets

General anomaly bound

For $r,n,n'\ge1$, positive processing times in both runs, and the two list schedules just described, the target is Graham's Theorem 1:

$$\frac{\omega'}{\omega}\le 1+\frac{n-1}{n'}.$$

The numerator and denominator refer to the actual runs, with potentially different lists and processor counts. The conclusion does not require the new schedule to finish earlier. Its factor permits the anomalies shown in §2 while preventing an arbitrarily large increase for fixed $n,n'$. The supporting targets follow the proof's numbered displays: a precedence chain covering idle times in the second run (1), an idle-time estimate for that chain (2), a comparison of its length with the first run (3)–(4), and the work-volume bound used in (5) Graham, pp. 419–420.

Significance

The theorem places a quantitative limit on the damage caused by a list rule after simultaneous changes in task durations, precedence, ordering, and capacity. When $n'=n$, the factor is $2-1/n$; when the first run has one processor, it is $1$. The statement applies to every finite task set and every pair of lists, so it can be reused when a scheduling method produces a list without additional structural guarantees. Graham states that the bound is best possible, citing earlier examples; this mission formalizes the inequality in this paper and does not claim to formalize those external examples Graham, p. 420.

The result is proved in the source paper. The work here is to give its objects precise Lean definitions and to supply machine-checked proofs of the bound and its supporting claims. A formal development needs to account for continuous real start times, processor assignments, half-open execution intervals, and the behavior of the list rule when several tasks or processors become available together. The resulting model of a nonpreemptive list schedule and the basic volume and chain estimates can serve later formalizations of parallel scheduling. The present proposal contains statements and definitions; its theorem bodies are open proof obligations.

Difficulty

Total work alone does not control the anomaly: processors can be idle while precedence keeps available work from starting, and changing precedence can alter which tasks occupy the processors later. A direct comparison of corresponding task completion times between the two runs also fails in Graham's §2 examples. The central difficulty is expressing the second run's idle periods through work on a single precedence chain and then relating that chain to the first run's finishing time. In Lean, the chain and the time intervals must be represented without silently changing endpoint conventions or treating a ready but unstarted task as running.

Formalization scope

Tasks are Fin r and processors are Fin n, with zero-based Lean indices corresponding to Graham's one-based subscripts. Processing times and start times are real. A priority list is a bijection between positions and tasks, so it contains every task exactly once and need not respect precedence. The order is strict. Feasible schedules are nonpreemptive and use half-open running intervals. The finishing time is a finite maximum of completion times; for no tasks it is defined as zero, while the ratio theorem assumes $r>0$ so its denominator is positive. Both processor counts are positive. The strict positivity of both time functions is inherited from the paper's $\mu:T\to(0,\infty)$ convention.

The model captures Graham's rule by no unforced idleness and list priority. It does not encode the smaller-index tie rule for identical processors, since the tie affects only processor labels and not start times or $\omega$. The covering-chain milestone represents Graham's set $B$ as times before $\omega'$ when not all processors are busy; all-idle times before the finish cannot occur under the list rule. The idle-time milestone writes the total duration of empty tasks as $n'\omega'-\sum_j\mu'(T_j)$ using display (5). Natural-number subtraction is not used in the constants: $n-1$ and $n'-1$ are real differences. The companion existence statement and a concrete two-task sanity check rule out a vacuous list-schedule predicate. Contributions can address that existence theorem, the chain construction, interval accounting, the volume bound, and the final ratio.

Selected references

• R. L. Graham, Bounds on Multiprocessing Timing Anomalies, SIAM Journal on Applied Mathematics 17(2), 416–429, 1969. DOI: 10.1137/0117039.

Motivation

Shop scheduling asks how to sequence jobs that each need processing on several machines. In an open shop, a job's operations may be executed in any order, as in testing stations, repair bays, or classroom and examination timetables, where the order in which a candidate visits the stations is irrelevant. The objective studied here is the makespan $C_{\max}$, the time at which the last operation finishes.

The survey of Graham, Lawler, Lenstra and Rinnooy Kan (Ann. Discrete Math. 5, 1979) introduced the three-field notation $\alpha|\beta|\gamma$ that the scheduling literature still uses, and classified the complexity of the problems it names. For the open shop, its §5.2.1 presents a simplified exposition of the result of Gonzalez and Sahni (J. ACM 23, 1976): with two machines and no preemption, the obvious lower bound on the makespan is always achieved. The same page records that the three-machine case $O3\|C_{\max}$ is binary NP-hard, so two machines is exactly where the problem is easy.

Timeline. Gonzalez and Sahni (1976) gave the linear-time algorithm for $O2\|C_{\max}$, proved NP-hardness for $O3\|C_{\max}$, and gave a polynomial algorithm for the preemptive problem $O|pmtn|C_{\max}$. Graham et al. (1979, §5.2.1) gave the shorter construction formalized here, and observed (§5.2.2) that it implies preemption brings no advantage for $m = 2$. Lenstra (cited as forthcoming in the survey) showed $O2|r_j|C_{\max}$, $O2|tree|C_{\max}$ and $O\|C_{\max}$ unary NP-hard.

Setting

There are $n$ jobs $J_1, \dots, J_n$ and two machines $M_1$, $M_2$. Job $J_j$ has an operation on $M_1$ of length $a_j \ge 0$ and an operation on $M_2$ of length $b_j \ge 0$. There is no preemption, and every job is available at time $0$. A schedule assigns start times $s_1(j)$ and $s_2(j)$ to the two operations of $J_j$, which then occupy $[s_1(j), s_1(j)+a_j)$ on $M_1$ and $[s_2(j), s_2(j)+b_j)$ on $M_2$.

A schedule is feasible if

1. all start times are nonnegative;
2. each machine processes at most one job at a time: the intervals of distinct jobs on the same machine do not overlap;
3. each job is processed on at most one machine at a time: the two intervals of the same job do not overlap, in either order.

Write $T_1 = \sum_j a_j$ and $T_2 = \sum_j b_j$ for the two machine loads. The survey's construction uses the sets

$$A = \{J_j \mid a_j \ge b_j\}, \qquad B = \{J_j \mid a_j < b_j\},$$

two distinct jobs $J_r$, $J_l$ with $a_r \ge \max_{J_j \in A} b_j$ and $b_l \ge \max_{J_j \in B} a_j$, and $A' = A - \{J_r, J_l\}$, $B' = B - \{J_r, J_l\}$.

Formalization targets

Goal: the optimal makespan

$$C^*_{\max} = \max\Big\{T_1,\ T_2,\ \max_j\,(a_j + b_j)\Big\},$$

and the optimum is attained. Formally, for every $T \ge 0$: a feasible schedule completing every operation by $T$ exists if and only if $T_1 \le T$, $T_2 \le T$ and $a_j + b_j \le T$ for all $j$. The goal mentions neither $A$, $B$, $J_r$, $J_l$ nor the case analysis; those are the milestones.

Milestones (in the order of the argument)

1. Two distinct jobs $J_r$, $J_l$ with the required bounds exist when $n \ge 2$.
2. Fig. 5.1: the blocks $B' \cup \{J_l\}$ and $A' \cup \{J_r\}$, with $A'$ and $B'$ in arbitrary order, have feasible staircase schedules without idle time.
3. Fig. 5.2: if $T_1 - a_l \ge T_2 - b_r$, the blocks combine into a feasible schedule of all jobs ending by $T_1 + b_r$.
4. Case (1): if moreover $a_r \le T_2 - b_r$, some feasible schedule has length at most $\max\{T_1, T_2\}$.
5. Case (2): if moreover $a_r > T_2 - b_r$, some feasible schedule has length at most $\max\{T_1, a_r + b_r\}$.
6. The symmetric case $T_1 - a_l < T_2 - b_r$: some feasible schedule has length at most $\max\{T_1, T_2, a_l + b_l\}$.
7. The lower bound: every feasible schedule has $C_{\max} \ge \max\{T_1, T_2, \max_j(a_j + b_j)\}$.

Significance

The result. The theorem gives a closed form for the optimal makespan of a two-machine open shop, together with a linear-time construction of an optimal schedule. The survey uses it immediately: since the bound is also a lower bound for preemptive schedules, $O2|pmtn|C_{\max}$ is solved by the same schedules, so preemption gives no advantage on two machines (§5.2.2). It is the standard example of a shop problem whose trivial lower bound is tight, and the contrast with the binary NP-hard $O3\|C_{\max}$ marks the complexity boundary for nonpreemptive open shops.

Formalizing it. The result is classical and proved on paper; no machine-checked proof is known to exist on this platform. The mission produces a reusable model of nonpreemptive two-machine open-shop schedules with real processing times, a verified lower bound, and a verified constructive argument. Unlike many existence-of-schedule results, the survey's construction is explicit (orders and start times), so it can be formalized directly rather than through an abstract existence argument.

Difficulty

The lower bound is the easy half. The difficulty is the construction: a schedule must meet the bound simultaneously on both machines and for every job. The natural first idea, running every job on $M_1$ then $M_2$ in some order (a flow-shop schedule), fails: Johnson's rule then gives a makespan that can exceed $\max\{T_1, T_2, \max_j(a_j+b_j)\}$, because the open shop needs some job to visit $M_2$ first. The survey's construction moves exactly one job, $J_r$, to the front of $M_2$, and its correctness depends on the choice of $J_r$ and $J_l$ and on the case split on $T_1 - a_l$ versus $T_2 - b_r$. Figures 5.3 and 5.4 are drawn for $T_1 \ge T_2$; in the other subcases the start times shown in the figures need adjustment, and the formal statements of the cases assert lengths rather than the figures' exact start times.

Formalization scope

All declarations live in the namespace SchedSurvey.O2. Jobs are Fin n, 0-based ($J_j$ is index $j-1$). Processing times and start times are real numbers with $a_j, b_j \ge 0$; the survey's integer data are a special case, and every claim of §5.2.1 holds over the reals. A schedule is a pair of start-time functions s₁ s₂ : Fin n → ℝ. Interval non-overlap is s + p ≤ s' ∨ s' + p' ≤ s, so touching intervals are allowed and a zero-length operation occupies nothing. Feasibility (IsFeasible) contains both disjointness constraints of §2.1, the machine constraint and the job constraint, with the two operations of a job in either order. The job constraint is essential: without it the optimum would be $\max\{T_1, T_2\}$ and the goal false.

"Length at most $L$" is CompletesBy a b S L: every operation ends by $L$. Optimality is stated in threshold form, which avoids taking a supremum or infimum over a possibly empty set and is equivalent to "$C^*_{\max}$ equals the maximum and is attained". A maximum over $A$ or $B$ appears as a bound on every member, which is also correct for empty $A$ or $B$. The orders of $A'$ and $B'$ are duplicate-free lists whose members are exactly those sets; back-to-back start times are given by contigStart.

The milestone on the choice of $J_r$, $J_l$ assumes $n \ge 2$, which the page presupposes; the goal does not, and covers $n \le 1$ as well. The lower bound assumes $T \ge 0$, which matters only for $n = 0$.

A trivializing formalization is ruled out: feasibility includes both disjointness constraints and nonnegative start times, the threshold is quantified over all $T \ge 0$, and no constant is fixed.

Contributions welcome: proofs of the lower bound (a sum of disjoint intervals inside $[0, T]$), of the list-based block lemmas, of the case lemmas, and of the goal from them. The interval and back-to-back-schedule lemmas are reusable for other shop problems.

Selected references

• R.L. Graham, E.L. Lawler, J.K. Lenstra, A.H.G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
• T. Gonzalez, S. Sahni, Open shop scheduling to minimize finish time, Journal of the ACM 23(4) (1976) 665–679. https://doi.org/10.1145/321978.321985
• S.M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1 (1954) 61–68. https://doi.org/10.1002/nav.3800010110

Motivation

Parallel processing poses a basic allocation question: given tasks of known lengths and several identical processors, how much time is lost when tasks are assigned by a simple list rule instead of an optimal allocation? The finishing time is the moment the last processor completes its work. For independent tasks, a list rule starts each next task on a processor that becomes free first. Such a rule is easy to execute, but the resulting allocation can be worse than the best partition of tasks among processors. Graham's 1969 paper studies precise worst-case ratios for this model. Its Theorem 3 asks what guarantee follows when the first $k$ tasks of the list are chosen among the longest and scheduled optimally before the remaining tasks are appended.

The paper also notes two endpoints of this family. With $k=0$, the rule is ordinary list scheduling and has ratio at most $2-1/n$. With $k=n$, the $n$ longest tasks can start one per processor, giving ratio at most $3/2-1/(2n)$. Theorem 3 expresses these as instances of one bound, including the integer jump at each multiple of $n$ Graham, pp. 427–428.

Setting

There are $r>0$ independent tasks, indexed by $jin\{0,\ldots,r-1\}$, and $n>0$ identical processors, indexed by $p\in\{0,\ldots,n-1\}$. Task $j$ takes a strictly positive time $\mu_j$. A priority list $L$ contains every task exactly once. Its first $k$ tasks are $k$ of the longest tasks; equal lengths may be ordered either way. As a processor becomes available, it takes the next task in the list. Once started, a task runs without interruption. With no precedence constraints, every unstarted task is ready, so a processor runs its assigned tasks consecutively from time zero.

An assignment $\sigma$ records the processor that executes each task. The load $\ell_p(\sigma)$ of processor $p$ is the sum of its assigned task lengths. The finishing time is the largest load, $\omega(k)=\max_p\ell_p(\sigma)$. For a list assignment, each task is assigned to a processor whose load from earlier list tasks is smallest at that step. If two processors are tied, either can be selected without changing the finishing time. For any assignment $\tau$, let $\omega_k(\tau)$ be the largest load contributed by only the first $k$ list tasks. The algorithm requires its own first $k$ assignments to minimize $\omega_k(\tau)$ over all assignments $\tau$; the remaining tasks may occur in any list order.

Write $\omega_0$ for the smallest finishing time achievable for all $r$ tasks. The paper introduces it as the minimum over possible lists and later describes the same problem as minimizing the largest part sum over partitions of the task lengths Graham, pp. 421, 428. The formalization uses the partition or assignment form of $\omega_0$.

Formalization targets

Theorem 3

For $0\le k\le r$, when the first $k$ longest tasks have an optimal prefix schedule, Graham's bound is

$$\frac{\omega(k)}{\omega_0} \le 1+\frac{1-1/n}{1+\lfloor k/n\rfloor}.$$

Here $\lfloor k/n\rfloor$ is the greatest integer at most $k/n$. The theorem also says the bound is best possible when $k$ is divisible by $n$ Graham, Theorem 3, p. 427. The equality examples are a separate companion statement in this mission.

Source milestones

The milestones state the finite-volume lower bound on $\omega_0$, the case in which completing all tasks takes no longer than completing the first $k$, and the paper's numbered inequalities (14), (15), and (16). They use $\alpha^*$ for the greatest task length after the first $k$ positions. These are individual mathematical claims from the proof on p. 427, with their original wording and formulas recorded alongside the formal statements.

Significance

The theorem gives a quantitative tradeoff between work spent optimizing a prefix and the worst-case finishing time of the full list. Its denominator is $1+\lfloor k/n\rfloor$, so the guarantee improves when the optimized prefix contains another full processor's worth of long tasks. The example at multiples of $n$ shows that the stated coefficient cannot be uniformly reduced for the algorithm as specified Graham, p. 427.

The result is proved in the paper. This mission's remaining work is a machine-checked proof of its exact statement and the source's intermediate inequalities. The published identical-machine makespan definition is reused, while the list-assignment rule, optimal prefix, and longest-remaining-task quantity are made explicit here. Those definitions can also support later work on list scheduling without precedence constraints. No machine-checked proof of Theorem 3 is claimed by this proposal.

Difficulty

An optimal schedule for the first $k$ long tasks does not make the entire list optimal: short tasks appended later can affect which processor finishes last. A bound based only on average total work ignores this final imbalance; a bound based only on the largest remaining task ignores how many long tasks every assignment must place together. The proof must relate both constraints to one finishing time while preserving the floor $\lfloor k/n\rfloor$. Replacing that floor with the real quotient changes the claim, and allowing an arbitrary prefix arrangement loses the algorithm's required optimality.

Formalization scope

Tasks and processors are finite indexed sets Fin r and Fin n; their zero-based indices correspond to the paper's one-based $T_j$ and $P_i$. Task lengths are positive real numbers, and both $r$ and $n$ are positive. The list is a permutation, not merely a sequence that might omit or repeat a task. The condition $k\le r$ is explicit because choosing $k$ tasks from $r$ requires it; the paper treats $r>k$ inside the proof and the case $k=r$ is covered by the theorem. There is no precedence relation in this mission.

The list rule is a predicate on assignments: each next task goes to a processor with least current load. It omits the paper's smaller-index tie convention, since tied identical processors can be interchanged without changing the finishing time. The first $k$ positions must contain $k$ longest tasks, and their assignment must minimize the prefix finishing time among all assignments of those tasks. Those conditions are part of the goal; the inequalities (14)–(16) are conclusions to establish, not assumptions of the goal. A separate existence statement and a checked concrete instance ensure the list predicate is satisfiable.

All maxima and minima range over finite nonempty processor or assignment sets. The optimum is a minimum over assignments, equivalent to the paper's minimum over lists in the independent-task model. The quantity $\alpha^*$ is the largest duration outside the prefix when $k<r$, and is defined as zero when none remains; statements using it require $k<r$. Division is by $n>0$ and by $\omega_0>0$. Lean's natural-number quotient represents $\lfloor k/n\rfloor$; real subtraction is used for coefficients such as $n-1$. Contributions toward the finite load identities, the optimum-over-lists equivalence, and proofs of the listed bounds are within scope.

Selected references

• R. L. Graham, Bounds on Multiprocessing Timing Anomalies, SIAM Journal on Applied Mathematics 17(2), 416–429, 1969. DOI: 10.1137/0117039.

Motivation

The cutting stock problem asks how to cut standard stock rolls of length $L$ into pieces of demanded lengths $l_1,\dots,l_m$ so that the demands are met at least cost. Gilmore and Gomory solved its linear programming relaxation by column generation (Part I, Opns. Res. 9 (1961)): every cutting pattern is a column, and the column to bring into the basis is found by solving an integer knapsack problem whose objective is given by the current dual prices. In Part II (Opns. Res. 11 (1963)) they replaced the dynamic-programming knapsack solver of Part I by a lexicographic enumeration with a bound test, the Knapsack Method, and reported it to be about five times as fast as dynamic programming on their problem set (p. 866). The method is an early enumeration-with-bounds (branch-and-bound type) procedure for the integer knapsack, and the same pricing problem remains the inner loop of column generation for cutting stock, bin packing and their many variants.

Setting

There are $m$ demanded lengths $l_1,\dots,l_m>0$ with linear programming prices $b_1,\dots,b_m\ge0$, and $k$ standard stock lengths $L_1,\dots,L_k$ with costs $c_1,\dots,c_k$. A column for $L_j$ is a vector $(\alpha)_m=(a_1,\dots,a_m)$ of nonnegative integers with $\sum_i l_ia_i\le L_j$. The knapsack problem (1) for $L_j$ is

$$\bar M_j=\max\Big\{\sum_{i=1}^m b_ia_i : a_i\in\mathbb Z_{\ge0},\ \sum_{i=1}^m l_ia_i\le L_j\Big\},$$

and the quantity to compute is $M_j=\max(c_j,\bar M_j)$: a column improves the linear program exactly when $\bar M_j>c_j$.

For a prefix $(\alpha)_s=(a_1,\dots,a_s)$ write $\lambda\cdot(\alpha)_s=\sum_{i\le s}l_ia_i$ and $\beta\cdot(\alpha)_s=\sum_{i\le s}b_ia_i$. Step (1) sorts the data, $b_1/l_1\ge\dots\ge b_m/l_m$ and $L_1>\dots>L_k$, and appends a slack item $a_{m+1}$ with $b_{m+1}=0$, $l_{m+1}=1$. The method then generates vectors in decreasing lexicographic order:

• Steps (2) and (7) fill the coefficients after a prefix greedily, $a_i=[(L-\text{used})/l_i]$, for $L=L_1$ at the start and $L=L_t$ later.
• Step (3) records $\beta\cdot(\alpha)_m$ as the new $M_j$ for each $j\ge t$ with $L_j\ge\lambda\cdot(\alpha)_m$ and $\beta\cdot(\alpha)_m>M_j$.
• Step (4) finds the last nonzero coefficient $a_s$.
• Step (5) lowers $a_s$ by one and looks for the smallest $j$ with $L_j\ge\lambda\cdot(\alpha)_s$ and $(L_j-\lambda\cdot(\alpha)_s)b_{s+1}>(M_j-\beta\cdot(\alpha)_s)l_{s+1}$. This is the bound obtained by relaxing the integrality of $a_{s+1}$.
• Step (6) backs up to the previous nonzero coefficient when no such $j$ exists, and stops when there is none.

In Lean the method is a transition system Step on states (a, s, t, M, phase). Reachable means reachable from the start state of Step (2).

Formalization targets

Goal: the method terminates and computes $M_1$

Under Step (1)'s ordering, with $l_i>0$ and $b_i\ge0$:

$$\text{every run is finite},\quad \text{a non-final state has a successor},\quad M_1^{\text{final}}=\max\big(c_1,\bar M_1\big),$$

and at the end every $M_j$ is $c_j$ or the price of a column for $L_j$, with $c_j\le M_j$. With one stock length ($k=1$) this is the paper's correctness claim in full: the method solves the knapsack problem (1).

Milestones

1. Steps (2)/(7): the greedy completion is the lexicographically largest extension of a prefix that fits the capacity.
2. Step (4): the lexicographic predecessor of a fitting vector extends $(\alpha^1)_s$.
3. The relaxation bound $\beta\cdot(\alpha')_m\le\beta\cdot(\alpha)_s+b_{s+1}(L-\lambda\cdot(\alpha)_s)/l_{s+1}$ for every fitting extension.
4. After the inequality of Step (5)'s test fails, no vector between $(\alpha)_s$ and the successor of Step (6) improves $M$.
5. The vectors tested in Step (3) strictly decrease lexicographically.
6. The invariant on entry to Step (3).
7. Identical prices: among lengths with equal prices only the shortest is needed (p. 869).

Significance

The goal certifies the pricing oracle of the Gilmore–Gomory column-generation method: the knapsack solver it calls returns the true optimum. The pricing step is exact only if that holds, and so is the conclusion "no improving column exists, the LP is solved". Milestones 1–4 are reusable on their own. They are the textbook ingredients of lexicographic and depth-first branch-and-bound for the integer knapsack: the greedy completion, the density-ordered LP bound, and the pruning rule.

The paper's argument is a short paragraph, "clear from the order in which the $m$-vectors are generated". Writing it out shows that the claim is false for several stock lengths as the steps are printed. With $m=1$, $l_1=b_1=1$, $L=(5,2)$ and $c=(0,0)$, the method tests $(5)$. The test of Step (5) at $(4)$ then fails for $j=2$ only because $4>L_2$, Step (6) stops, and the run ends with $M_2=0$ while the column $(2)$ has price 2. This mission therefore states what the printed algorithm does achieve. The result is the full claim for $k=1$ and for the longest stock length in general. A sorry-free Lean proof of the counterexample run accompanies the mission. No part of the method or its correctness has been formalized before, as far as a search of the platform shows.

Difficulty

The method skips large parts of the lexicographic order in three ways:

• Step (7) jumps to the greedy completion for $L_t$ rather than $L_1$.
• Step (6) jumps past every smaller value of $a_s$ once one test fails.
• Step (3) updates only $j\ge t$.

Each skip has to be justified by a bound that holds for every vector skipped, and the justifications interact. A skipped vector may fit a longer stock length but not $L_t$, and the bound for $L_1$ must cover exactly those vectors. The invariant that survives all three moves is not the naive "every vector above the current one has been examined": the vectors are not examined, only bounded. Termination needs the lexicographic decrease together with finiteness of the fitting vectors, and progress needs the reachability invariants $1\le s\le m$ and $a_s\ne0$ that make Step (5) meaningful.

Formalization scope

• Items are Fin m from 0. The paper's level $s$ is a natural number, and the prefix $(\alpha)_s$ is the coordinates with index < s. Stock lengths are Fin k, and $L_1$ is index 0. The slack item enters only through $b_{s+1}$ and $l_{s+1}$ at $s=m$. The lexicographic order is Mathlib's Pi.Lex, and $[x]$ is Nat.floor.

• $M_j=\max(c_j,\bar M_j)$ is the predicate IsKnapsackMax, never a real supremum, which would be 0 on an empty set. The algorithm's output is never defined as the maximum. The goal includes termination and progress, so its correctness clause is not vacuous. Every invariant is stated for reachable states only.

• The goal adds two disclosed hypotheses:

  • $l_i>0$: demanded lengths.
  • $b_i\ge0$: with a negative price the method is wrong, and the paper applies it to cutting-stock prices, which are nonnegative.

  Step (1) is a hypothesis on the data, not a step.

• The goal also makes these corrections:

  • The claim is narrowed. For every $j$ it states $c_j\le M_j$ and attainment, and the upper bound for $L_1$ only (see Significance).
  • The lexicographic order is repaired. The page's definition misses vectors that differ in their first coefficient.
  • Step (7) reads λ·(α)_m. The page's "satisfies $L_t\ge\lambda\cdot(\alpha)_s$" is read as $\lambda\cdot(\alpha)_m$.
  • Step (4) gets a stopping case. On the zero vector, where the page has no case, the method stops.
  • Milestone 4 is stated for the failed inequality, not for a failed test, because the failed test is what makes the page's successor claim false.

• Not formalized:

  • Step (3′), the variant computing $\max_j(M_j-c_j)$.
  • The record of patterns.
  • The dynamic-programming recursion and the timing estimates.

Contributions welcome: proofs of the milestones, and a corrected multi-length variant of the method with a proof that it computes every $M_j$.

Selected references

• P. C. Gilmore, R. E. Gomory, A linear programming approach to the cutting stock problem—Part II, Operations Research 11(6) (1963), 863–888. https://doi.org/10.1287/opre.11.6.863
• P. C. Gilmore, R. E. Gomory, A linear programming approach to the cutting-stock problem, Operations Research 9(6) (1961), 849–859. https://doi.org/10.1287/opre.9.6.849
• G. B. Dantzig, Discrete-variable extremum problems, Operations Research 5(2) (1957), 266–288. https://doi.org/10.1287/opre.5.2.266

Motivation

In just-in-time scheduling each job has a preferred time, and finishing it early is as undesirable as finishing it late. Garey, Tarjan and Wilfong (Math. Oper. Res. 13 (1988), 330–348) study the one-processor version in which task $T_i$ has a length $l_i \ge 0$ and a preferred starting time $a_i \ge 0$, and the discrepancy of a task started at time $s_i$ is $|s_i - a_i|$. The penalty is symmetric: earliness and tardiness cost the same. The paper shows that minimizing the total discrepancy is NP-complete, gives an $O(N \log N)$ algorithm for a fixed task order, and, in §3, gives an efficient algorithm for minimizing the maximum discrepancy $\max_i |s_i - a_i|$: a linear-time test for a given bound $\gamma$ after an $O(N \log N)$ sort, combined with a search over $\gamma$.

This mission formalizes the structural core of §3: the normal-form theorems (Theorem 4, Corollaries 1 and 2) on which the paper's algorithm for maximum discrepancy is built. The two companion missions of the series cover the NP-completeness result (THEOREM 1) and the fixed-order algorithm (THEOREMS 2 and 3).

Setting

Fix a bound $\gamma \ge 0$. A schedule has maximum discrepancy at most $\gamma$ exactly when every task starts no earlier than its release time $r_i = \max\{0, a_i - \gamma\}$ and finishes no later than its deadline $d_i = a_i + l_i + \gamma$ (p. 342). These release times and deadlines are in special form: with $\alpha = 2\gamma$, for every task

$$d_i - r_i = l_i + \alpha \quad\text{or}\quad \big(r_i = 0 \text{ and } d_i < l_i + \alpha\big).$$

From here on the data are arbitrary reals $l_i \ge 0$, $r_i \ge 0$, $d_i$ in special form for some $\alpha \ge 0$.

A schedule is an execution order $\sigma$ ($\sigma(p)$ is the task in position $p$) with starting times $s_i$, such that a task finishes no later than any later-positioned task starts: $s_{\sigma(p)} + l_{\sigma(p)} \le s_{\sigma(q)}$ for $p < q$. It is feasible if $r_i \le s_i$ and $s_i + l_i \le d_i$ for every $i$. Its makespan is $\max_i (s_i + l_i)$, and it is optimum if it is feasible and no feasible schedule has a smaller makespan.

Let $T_N$ be a task of largest deadline. A schedule has the release time property if every task executed after $T_N$ has release time strictly later than the starting time of $T_N$. When the tasks are indexed with $d_1 \le \dots \le d_N$, a schedule is in standard form with split index $j$, $0 \le j \le N-1$, if it begins with an optimum schedule of $T_1, \dots, T_j$, followed by $T_N$ started at the maximum of $r_N$ and the completion time of that first part, followed by $T_{j+1}, \dots, T_{N-1}$ in this order without idle time.

Formalization targets

Goal: Corollary 2 (p. 344)

$$\exists\ \text{a feasible schedule} \;\Longrightarrow\; \exists\ \text{an optimum schedule that is in standard form and has the release time property.}$$

Milestones

1. Theorem 4 (pp. 342–343): if a feasible schedule exists, some optimum schedule has the release time property with respect to any task of largest deadline.
2. The deadline split (proof of Corollary 1, p. 344): in every feasible schedule with the release time property, a task $T_i \neq T_N$ precedes $T_N$ if and only if $d_i \le s_N + \alpha$.
3. Corollary 1 (p. 344): some optimum schedule executes before $T_N$ exactly the tasks of deadline at most $\beta$, for some $\beta \ge 0$.
4. Release before finish (p. 344): every task executed after $T_N$ has $r_i \le s_N + l_N$.
5. Normalization after $T_N$ (p. 344): an optimum schedule with the release time property can be changed, without moving $T_N$ later and without touching the tasks before it, so that there is no idle time from the start of $T_N$ on and the later tasks run in deadline order.

Two companion items state the reformulation of the maximum-discrepancy bound as release times and deadlines, and the special form with $\alpha = 2\gamma$.

Significance

Corollary 2 reduces the search for an optimum schedule of $T_1, \dots, T_n$ to $n$ candidates, one per split index, each assembled from an optimum schedule of a shorter prefix. This is the dynamic program of §3.2, which the paper implements in $O(N)$ time after an $O(N \log N)$ sort; combined with a search over $\gamma$ it minimizes the maximum discrepancy. Without the special form, deciding whether one processor can meet arbitrary release times and deadlines is NP-complete (reference [4] of the paper, Garey and Johnson 1979), so the normal form is what separates the tractable case from the general one.

The results are proved in the paper; no machine-checked proof of them is known on Prove2Me. A formal proof of Corollary 2 would certify the correctness of the split-index recursion and, together with the companions, of the reduction from maximum discrepancy to this release-time/deadline problem.

Difficulty

The obvious argument fails in Theorem 4. Exchanging a straggler (a task after $T_N$ released no later than $T_N$ starts) with $T_N$ shifts the tasks between them, and for general release times and deadlines those tasks can become infeasible. The paper's argument uses the special form at every step: a task released after $T_N$ starts has $r_i > 0$, hence $d_i - r_i = l_i + \alpha$ exactly, and this equality is what bounds how far tasks may move. It also needs an extremal choice of the optimum schedule (fewest tasks after $T_N$, then fewest tasks between $T_N$ and the first straggler), which requires showing that optimum schedules exist over the reals. The passage to standard form then combines this with an earliest-deadline exchange for the tasks after $T_N$ and the replacement of the first part by an optimum sub-schedule without losing feasibility of the later tasks.

Formalization scope

Tasks are indexed by Fin N (0-based: the paper's $T_1, \dots, T_N$ are $0, \dots, N-1$; the paper's $T_N$ in Corollary 2 is the index $N-1$). All data are real. A schedule is a permutation σ : Fin N ≃ Fin N with starting times s : Fin N → ℝ; "executed before/after" refers to σ, not to a comparison of starting times, because zero-length tasks may share a starting time. Execution intervals meet at most at endpoints. The makespan is a supremum over Fin N; "optimum" quantifies over all feasible schedules, not only standard-form ones.

The standing hypotheses on every structural item are $\alpha \ge 0$, $r_i \ge 0$, $l_i \ge 0$ (from $\gamma \ge 0$, the $\max\{0, \cdot\}$ in $r_i$, and nonnegative lengths); since $s_i \ge r_i$, start times are nonnegative, as the paper assumes throughout. The special form is a hypothesis of every structural item and cannot be dropped. The paper's dummy task $T_0$ ($r_0 = d_0 = l_0 = 0$) is not a task; an empty first part completes at time $0$. Corollary 1's "the set of all tasks with deadline $\beta$ or less" is read as excluding $T_N$, the only reading under which it is true. The page's "(which can be assumed optimum)" is part of the standard form. The deadline-split and release-before-finish milestones are stated for every feasible schedule, as their arguments allow.

A trivializing formalization is excluded: the standard form pins $T_N$'s start to $\max(r_N, C)$ and the later tasks to consecutive positions in index order, so the goal is not Corollary 1 restated with an unconstrained split.

Running times ($O(N \log N)$, $O(N)$) and the algorithm of §3.2 are out of scope. The development needs only finite permutations, finite suprema and the exchange arguments of §3.1; the existence of an optimum schedule (minimum makespan over finitely many orders, earliest-start schedules) is reusable for other single-machine problems with release times and deadlines. Proofs of any milestone, and a sorry-free proof of the existence of optimum schedules, are welcome.

Selected references

• M. R. Garey, R. E. Tarjan, G. T. Wilfong, One-Processor Scheduling with Symmetric Earliness and Tardiness Penalties, Mathematics of Operations Research 13(2):330–348, 1988. https://doi.org/10.1287/moor.13.2.330
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979 (reference [4] of the paper, cited on p. 342 for the NP-completeness of one-processor scheduling with release times and deadlines). ISBN 0-7167-1045-5

Motivation

A task may have a preferred execution time because a material delivery, external event, or downstream operation is timed to it. Starting early can be as costly as starting late. Garey, Tarjan, and Wilfong study this situation on one processor, where tasks cannot overlap but idle time between tasks is permitted. Their total-discrepancy problem is hard when the execution order is free; fixing the order leaves a substantial timing problem because each start can still move and can force changes to earlier starts. The paper gives an explicit scheduling procedure for that case and proves that it minimizes the sum of deviations from preferred starts (Garey, Tarjan, and Wilfong, 1988, §§1–2).

This mission targets that procedure and its correctness theorem. It also records the paper's equal-length result: when task lengths are identical, a minimum-cost schedule exists in preferred-start order, so the fixed-order procedure applies after sorting. These are two precise claims about total discrepancy, distinct from the paper's separate maximum-discrepancy problem.

Setting

There are $n$ tasks, indexed $i=0,\ldots,n-1$. Task $i$ has a nonnegative length $l_i$, a nonnegative preferred starting time $a_i$, and an actual starting time $s_i$. Once started, it occupies the one processor until $s_i+l_i$. Each start must be nonnegative. For the fixed-order problem, task $i$ must finish before task $i+1$ starts, so $s_i+l_i\le s_{i+1}$. This permits idle time when the inequality is strict. The task's discrepancy is $|s_i-a_i|$; because its preferred completion is $a_i+l_i$, this is also its absolute completion-time discrepancy. The total discrepancy is

$$\operatorname{cost}_n(s)=\sum_{i=0}^{n-1}|s_i-a_i|.$$

A block is a maximal consecutive set of tasks with no idle time between neighboring tasks. Within a block, Decrease counts tasks whose actual starts are later than preferred, and Increase counts tasks whose actual starts are no later than preferred. These names describe the effect of moving the entire block earlier: the discrepancy of a Decrease task falls initially, whereas that of an Increase task rises. The algorithm's state is a schedule $S_n$ for the first $n$ tasks. It inserts the next task at its preferred start when the previous task has finished, and at that finish time otherwise. In the latter case it may move the final block earlier until one of the paper's stopping events occurs: the block reaches time zero, a late task reaches its preferred start, or the block meets its predecessor (§2.2, p. 337).

For the equal-length result, schedules may execute tasks in any order. Two distinct tasks are feasible together when one completes before the other starts; meeting at endpoints is allowed. The objective remains the same sum of absolute discrepancies.

Formalization targets

Fixed-order optimality

The main target is the paper's Theorem 2. For all nonnegative task data and every $n$, the actual schedule $S_n$ produced by the block-shifting algorithm is feasible and satisfies

$$\operatorname{cost}_n(S_n)\le\operatorname{cost}_n(s) \qquad\text{for every feasible fixed-order schedule }s.$$

This includes the empty schedule and schedules with idle time. The milestone list follows the paper's own assertions: a balanced final block can move earlier without changing cost; every block of $S_n$ has more Increase tasks than Decrease tasks or begins at zero (Lemma 7); and the two claims in Case 2 of the proof record the cost of adding a late task and the comparison with schedules that place it earlier (Theorem 2 and Lemma 7, p. 338).

Equal-length schedules

The companion target is Theorem 3. If every task has a common length $L\ge0$ and the preferred starts are indexed so that $a_i\le a_{i+1}$, then among all feasible schedules, including those with another task order, at least one minimum-cost schedule starts the tasks in index order:

$$\exists s\;\bigl[ \operatorname{cost}_n(s)\le\operatorname{cost}_n(t) \text{ for every feasible }t \bigr] \quad\text{with }s_i\le s_{i+1}\text{ whenever }i+1<n.$$

The paper uses this statement to connect free-order equal-length scheduling to its fixed-order procedure (Theorem 3, p. 340).

Significance

Theorem 2 certifies an explicit schedule, not just the existence of an optimum. It fixes the objective value for a prescribed execution order and gives a baseline against which any other legal timing of the same tasks can be compared. Theorem 3 supplies the ordering fact needed to use that result when all lengths agree. Together they explain why a problem that is difficult for unrestricted task lengths still has these structured solvable cases (Garey, Tarjan, and Wilfong, 1988, abstract and §2.5).

The paper proves both theorems on paper. The work here is to formalize its schedule construction, cost, block boundaries, and comparison classes in Lean, then obtain machine-checked proofs of the stated targets. The draft theorem declarations compile with proof placeholders; this proposal does not claim that they are already machine-checked results. A completed development would make the model and the algorithm available for later formal work on scheduling with idle time and symmetric earliness and tardiness penalties.

Difficulty

Moving a task closer to its preferred start can move neighboring tasks farther from theirs. A simple task-by-task choice therefore does not establish global optimality. Nor does a count of late and early tasks in one block, by itself, justify arbitrary earlier movements of individual tasks. The difficult comparison in the paper is between the algorithm's schedule and a competing feasible schedule whose new task starts earlier: the whole final block and its constrained relative movements matter. The proof also has to account for the boundary at time zero and for blocks that merge when shifted. These are the reasons the explicit procedure and its block invariant need careful statements (§§2.2–2.3, pp. 337–338).

Formalization scope

The Lean development represents task data and starts as functions from natural-number indices to real numbers; only indices below $n$ count. Task $i$ in Lean is the paper's $T_{i+1}$. Preferred times, lengths, and legal starting times are nonnegative. The start-time condition is a standing convention used by the paper's algorithm, especially its zero-boundary stopping rule. Fixed-order feasibility requires successive tasks to be separated by at least the earlier task's length; unrestricted feasibility uses pairwise nonoverlap. An empty schedule is legal and has cost zero. The representation allows zero-length tasks, as does the paper's $l_i\ge0$ model.

The algorithm is defined by its stated insertion and single-block-shift operations. Defining $S_n$ as a chosen minimizer would erase the content of Theorem 2; the goal also explicitly asserts feasibility so that an illegal low-cost function cannot qualify. Theorem 3 compares with every feasible unrestricted-order schedule, not just schedules already in preferred-start order. The core definitions, the block invariant, and the cost comparisons are useful beyond this particular proof. Formalizing the paper's running-time bounds and heap implementation is outside this mission.

Selected references

• Michael R. Garey, Robert E. Tarjan, and Gordon T. Wilfong, One-Processor Scheduling with Symmetric Earliness and Tardiness Penalties, Mathematics of Operations Research 13(2), 330–348, 1988. DOI: 10.1287/moor.13.2.330.

3SUM asks whether three distinct positions in a list of integers contain values summing to zero. It is a central problem in fine-grained complexity.

This mission formalizes a deterministic $O(n^{1.9992})$ algorithm for 3SUM on $n$ polynomially bounded integers, on a word RAM with $O(\log n)$-bit words. Alman and Vassilevska Williams's 2026 breakthrough gives a truly subquadratic bound, refuting the integer 3SUM hypothesis in this model.

The mission uses the accompanying Lean specification and shares the Exact Triangle milestone with Truly Subcubic APSP on a Word RAM.

References

1. Josh Alman and Virginia Vassilevska Williams, Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs, 2026, Theorem 22.
2. Anthropic, formal-math / 3sum-apsp: accompanying Lean formalization, Theorem_22_3SUM.

Why priority queues with cheap decrease key matter

Many network optimization algorithms spend most of their time in a heap (priority queue): a set of items with real keys that supports inserting an item, finding and deleting an item of minimum key, melding two heaps, decreasing the key of an item, and deleting an arbitrary item. Dijkstra's shortest-path algorithm performs at most one delete min per vertex and may perform a decrease key for each edge, so on a graph with $n$ vertices and $m$ edges its running time is governed by how cheap decrease key is. Binomial queues support the heap operations in $O(\log n)$ worst-case time.

Fredman and Tarjan (J. ACM 34 (1987)) introduced Fibonacci heaps (F-heaps), in which delete min and delete take $O(\log n)$ amortized time and every other operation, decrease key included, takes $O(1)$ amortized time. This brings Dijkstra's algorithm to $O(n \log n + m)$ and improves the best bounds then known for all-pairs shortest paths, weighted bipartite matching (the assignment problem) and minimum spanning trees. F-heaps descend from the binomial queues of Vuillemin (1978) and use the potential technique of amortized analysis of Sleator and Tarjan. This mission formalizes the paper's §2 analysis, culminating in THEOREM 1 on p. 604.

Setting

An F-heap is a list of heap-ordered rooted trees: every child's key is at least its parent's key. Each node holds an item, the item's real key and a mark bit; the children of a node are kept in the order in which they were linked to it, earliest first. The rank $r(x)$ of a node is its number of children. A collection is a list of heaps, named by position; a run starts with no heaps.

Linking two trees with roots $x$ and $y$ makes $y$ the last child of $x$ if the key of $x$ is smaller, and otherwise makes $x$ the last child of $y$; the root that becomes a child is unmarked. The operations act as follows:

• make heap adds an empty heap; find min acts on a nonempty heap and returns a root of minimum key; insert adds a one-node tree for a new item; meld concatenates two root lists.
• delete min removes a root $x$ of minimum key, adds the children of $x$ to the roots, then repeats the linking step, "find any two trees whose roots have the same rank, and link them", in any order, until all root ranks are distinct.
• decrease key $(\Delta, i, h)$, $\Delta \ge 0$, lowers the key of $i$ and, if the node $x$ of $i$ is not a root, cuts $x$ from its parent, making its subtree a new tree. delete $(i, h)$ cuts $x$ the same way, destroys it and adds its children to the roots; a minimum root is deleted as in delete min.
• After every cut of a child of $p$, if $p$ is not a root it is marked if unmarked and cut from its own parent if marked: a cascading cut, which may repeat upwards.

The actual time of an operation is one unit, plus one per linking step, plus one per cut, plus for delete min the scan of the rank array (the largest rank involved). The potential $\Phi$ of a collection is the number of trees plus twice the number of marked nonroot nodes, and the amortized time of an operation is its actual time plus the increase of $\Phi$.

Formalization targets

Goal: THEOREM 1 (p. 604)

There is an absolute constant $C > 0$ such that for every sequence of $T$ operations started from no heaps, with $n_t$ the number of items in the heap that operation $t$ acts on, just before it acts,

$$\sum_{t<T} \mathrm{cost}_t \;\le\; \sum_{t<T} b_t, \qquad b_t = \begin{cases} C(\log_2 n_t + 1) & \text{delete min or delete},\\ C & \text{otherwise.}\end{cases}$$

The paper's wording is "the total time is at most the total amortized time, where the amortized time is $O(\log n)$ for each delete min or delete operation and $O(1)$ for each of the other operations"; the goal pins the $O(\cdot)$ to one constant and does not name the potential.

Milestones

1. LEMMA 1: the $i$th child of a node, in linking order, has rank at least $i - 2$.
2. $F_{k+2} \ge \varphi^k$, with $F_k$ the Fibonacci numbers and $\varphi = (1+\sqrt5)/2$.
3. COROLLARY 1: a node of rank $k$ has at least $F_{k+2} \ge \varphi^k$ descendants, itself included.
4. A node of rank $k$ in an $n$-item heap has $\varphi^k \le n$, hence $k \le \log n / \log\varphi$.
5. make heap, find min and meld leave $\Phi$ unchanged; insert raises it by one.
6. delete min raises $\Phi$ by at most $\log n / \log \varphi$ minus the number of linking steps.
7. decrease key raises $\Phi$ by at most three minus the number of cascading cuts.
8. From no heaps, the total amortized time bounds the total actual time.

Significance

THEOREM 1 is the data-structure fact behind the paper's algorithmic results: Dijkstra's algorithm in $O(n\log n + m)$, all-pairs shortest paths and the assignment problem in $O(n^2 \log n + nm)$, and minimum spanning trees in $O(m\,\beta(m,n))$.

The result has been proved since 1987. What the mission adds is a machine-checked version of the paper's own analysis on an operational model with arbitrary linking order, unmarking on link, marking or cascading on every cut, and the paper's unit costs. The proposal states the theorem and its supporting claims; their proofs remain to be formalized.

Difficulty

The obvious argument, that every tree is a binomial tree and so every rank is at most $\log_2 n$, fails as soon as cuts are allowed: decrease key and delete remove subtrees arbitrarily, and the trees of an F-heap need not be binomial. The rank bound has to come from an invariant of the whole history (LEMMA 1), which only holds because a node loses at most one child before it is cut itself; without cascading cuts a node of rank $k$ can be left with only $k+1$ descendants, and no logarithmic rank bound holds. A second difficulty is that the actual cost of one decrease key is unbounded, since a single operation may trigger arbitrarily many cascading cuts; a per-operation worst-case argument cannot give THEOREM 1, and the bound holds only for whole sequences started from no heaps.

Formalization scope

All declarations sit in the namespace FibHeap.Amort. Trees are a nested inductive FTree with item ℕ, key ℝ, a mark bit and a list of children in linking order; a heap is List FTree (its roots) and a collection is List Heap. Operations are a step relation Step s op s' d whose data d records linking steps, cuts, cascading cuts and the scan, so that cost d = 1 + links + cuts + scan is determined by what the operation did. The linking loop allows every order of linking; a link tie makes the first root a child of the second, while delete min may choose any minimum-key root. Runs start from no heaps; reachable collections consist of heap-ordered trees with each item in at most one heap. LEMMA 1, COROLLARY 1 and the delete-min bound are stated for reachable collections only, as the paper's "a node in an F-heap" intends. The paper's standing assumption that an item is in only one heap at a time is enforced by the precondition of insert and is not a hypothesis. The minimum pointer and returned items are not stored in the step relation; find min is a state-preserving step charged one unit. A heap destroyed by meld remains as an empty heap at its index.

Logarithms in the goal are base 2 (footnote 1, p. 600), with a $+1$ so that one-item heaps have positive budget. The paper's constant "$\le 1.4404 \log n$" on p. 604 is a rounding slip ($1/\log_2 \varphi = 1.44042\ldots$); milestones use the exact $\log_\varphi n$.

The goal is not trivialized: the cost counts every linking step and every cut as fixed by the step relation, $C$ is quantified before the run, and a companion theorem (step_exists) shows that every valid operation can be performed, so runs containing delete min, decrease key and cascading cuts exist. A further supporting statement gives an explicit form of the delete potential bound. A complete development needs facts about the nested inductive (sizes, subtree lists, marked counts under list edits), an invariant for LEMMA 1 recording when each child was linked, and the Fibonacci inequality; contributions of any of these as separate lemmas are welcome.

Selected references

• M. L. Fredman and R. E. Tarjan, Fibonacci heaps and their uses in improved network optimization algorithms, J. ACM 34(3):596–615, 1987. https://doi.org/10.1145/28869.28874
• J. Vuillemin, A data structure for manipulating priority queues, Comm. ACM 21(4):309–315, 1978. https://doi.org/10.1145/359460.359478
• R. E. Tarjan, Amortized computational complexity, SIAM J. Algebraic Discrete Methods 6(2):306–318, 1985. https://doi.org/10.1137/0606031
• E. W. Dijkstra, A note on two problems in connexion with graphs, Numer. Math. 1:269–271, 1959. https://doi.org/10.1007/BF01386390

Motivation

A postal route that must traverse every street and return to its starting point is a Chinese postman tour. In a street network, crossings are nodes, streets are edges, and the cost of a route is the sum of the lengths of the streets it traverses, counted with repetition. The practical question is which streets must be repeated, and how often. Edmonds and Johnson's 1973 paper separates that question from constructing the resulting tour: choose the repeated edges first, then find an Euler tour of the resulting multigraph. This mission concerns their reduction of the first question to a minimum-weight matching of the odd-degree nodes.

The reduction matters because it turns a route problem with arbitrary repeated edge traversals into a finite pairing problem. The graph of odd nodes is complete, with the weight of a pair given by its shortest-path distance in the original network. A matching chooses which odd nodes to pair, and paths realizing those pairs identify edges to repeat. The paper also explains why overlapping paths can be replaced so that no edge needs to be repeated by this construction more than once (§3, pp. 92–93).

Setting

A graph $G=(N,E)$ has finite node and edge sets. Each edge has two distinct endpoints. Different edges may join the same pair of nodes, so parallel streets remain distinct. The graph is connected when every pair of nodes is joined by an edge-labelled walk. A walk records both its node sequence and its edge sequence; a tour is a closed walk. An Euler tour uses each edge exactly once, while a postman tour uses each edge at least once. Edge lengths $c_e$ are real and nonnegative, as in §2, p. 89.

The degree of $v$ is the number of named edges meeting it. Let $T$ be the set of nodes of odd degree. For every edge $e$, let $x_e\in\mathbb N$ be the number of additional traversals. The parity equations require a nonnegative integer $w_v$ at each node such that

$$\sum_{e\ni v}x_e=2w_v+b_v,\qquad b_v=\begin{cases}1&v\in T,\\0&v\notin T.\end{cases}$$

Their objective is $z(x)=\sum_{e\in E}c_ex_e$. These are the paper's (3.1)–(3.4), with natural-number values encoding integrality and nonnegativity (§3, pp. 90–91). The equations express the even-degree condition after adding $x_e$ copies of each original edge.

For nodes $u,v$, write $d(u,v)$ for the length of a shortest path in $G$. This distance is backed by an attaining edge-simple path and is a lower bound on the length of every walk from $u$ to $v$. Connectivity and nonnegative edge lengths make that specification meaningful. Let $G_p$ be the complete graph on $T$, with edge $\{u,v\}$ of weight $d(u,v)$. A 1-matching $M$ pairs every node of $T$ with exactly one distinct node. Its length is $L(M)=\sum_{\{u,v\}\in M}d(u,v)$, equivalently half the sum of $d(v,f(v))$ over $v\in T$ for the pairing involution $f$ (§3, p. 92).

Formalization targets

Odd-node matching reduction

The goal asserts the existence of a 1-matching of the odd nodes and both directions of the cost comparison:

$$\forall M\;\exists x\text{ satisfying the parity equations}:\quad x_e\in\{0,1\},\ z(x)\le L(M),$$ $$\forall x\text{ satisfying the parity equations}\;\exists M:\quad L(M)\le z(x).$$

The existence conclusion and these comparisons identify the two attained minimum values. The goal does not prescribe a particular matching algorithm. Its supporting targets are the paper's uncrossing of overlapping shortest paths, parity of their union, reduction of multiplicities to zero or one, and decomposition of a parity solution into paths between odd nodes (§3, pp. 92–93).

Postman-tour reduction

The companion target relates a tour's edge counts to the parity equations. A postman tour traverses edge $e$ exactly $1+x_e$ times, and its length is

$$\sum_{e\in E}c_e(1+x_e) =\sum_{e\in E}c_e+z(x).$$

Conversely, positive integer edge counts with even incidence at every node can be ordered into a postman tour of a connected graph. The supporting Euler theorem handles a connected even multigraph (§2, p. 89).

Significance

The matching result characterizes the optimal additional cost of an undirected postman route. It says that the parity correction can be chosen from paths pairing odd nodes, and that no feasible choice of repeated traversals can beat the best such pairing. The companion identifies how that correction becomes an actual tour. The distinction is useful when one wants to change the matching method while retaining the mathematical guarantee on route length.

A formal development would provide a reusable account of finite multigraph walks whose edge names distinguish parallel edges, of shortest-path distances with explicit attainment, and of parity subgraphs decomposed into odd-to-odd paths and even-degree residual tours. These pieces support later formal work on route inspection, $T$-joins, and matching-based graph algorithms. The paper proves the mathematical result. The exact multigraph and cost statements drafted here are open formalization targets; the local prior-art search found related results for simple graphs and metric traveling-salesman models, but no published statement with this paper's objects and conclusion.

Difficulty

A direct shortest-path construction can assign the same original edge to two matching pairs. Simply setting $x_e=1$ for the union then loses the additivity of path lengths, and setting $x_e=2$ loses the promised zero-or-one form. The uncrossing claim must control both the matching cost and the number of times each original edge appears. In the converse direction, an arbitrary feasible $x$ may contain repeated edges and cycles; the argument must account for these without assuming that every supported edge belongs to a path between odd nodes (§3, pp. 92–93).

Formalization scope

Lean uses the published EdmondsMatching65.Polyhedron.Graph for $G$: finite node and edge types and an endpoint map into unordered node pairs. A proof field excludes loops; distinct edge names may have identical endpoints. Walks use lists of nodes and named edges with zero-based indices, and the one-node, zero-edge walk is allowed. Edge multiplicities and parity witnesses are natural numbers. Costs and shortest-path lengths are real. The distance relation requires both an attaining edge-simple path and a bound against all walks; no real infimum over a possibly empty family is used. The matching is a fixed-point-free involution on the odd nodes, extended by the identity elsewhere, and each pair contributes half of its two directed distance terms.

The goal assumes a connected graph and nonnegative edge lengths, exactly as the section does. The tour-only results require a nonempty node type because a list-based tour must have a starting node; without it an edgeless graph on no nodes would satisfy connectivity and even degree vacuously. The path-decomposition statement permits unused even-degree cycles. No independent set of “odd nodes” is accepted as input: it is computed from the degree of $G$.

The development needs finite multigraph incidence, edge-labelled walks, shortest paths, finite matchings, parity arithmetic, path uncrossing, and Euler tours. Proofs or useful intermediate results for these objects are welcome, including results applicable to multigraphs beyond the postman setting.

Selected references

• Jack Edmonds and Ellis L. Johnson, Matching, Euler tours and the Chinese postman, Mathematical Programming 5 (1973), 88–124. DOI: 10.1007/BF01580113.