Optimization

Motivation

The dynamic lot size model asks when, and how much, to order of a single item over a planning horizon of $n$ periods with known, time-varying demands, setup costs, unit order costs and holding costs. It is the textbook model of production planning and the building block of material requirements planning, multi-item scheduling and many decomposition schemes for larger supply-chain problems.

Wagner and Whitin (1958) showed that some optimal policy orders only when inventory is zero, which turns the problem into a shortest-path recursion with $O(n^2)$ running time. For more than thirty years this was the standard algorithm. In 1991 three groups independently reduced the complexity: Federgruen and Tzur (Management Science 37(8), 1991), Wagelmans, van Hoesel and Kolen (Operations Research 40, 1992) and Aggarwal and Park (Operations Research 41, 1993). Each obtained $O(n \log n)$ in general and $O(n)$ under special cost structures. The Federgruen–Tzur algorithm is a forward algorithm: at iteration $j$ it keeps a short list of periods that could still be the best last setup period for some future horizon, and updates it by local tests on neighbouring entries. This mission formalizes the theorem that justifies those tests.

Setting

For periods $i = 1, 2, \dots$ let $d_i$ be the demand, $K_i$ the setup cost, $c_i$ the variable per unit order cost and $h_i$ the cost of carrying a unit of inventory at the end of period $i$. Write $D(i) = \sum_{k=1}^{i} d_k$ and $H(i) = \sum_{k=1}^{i} h_k$, so $D(0) = H(0) = 0$. For $i < j$ let $c_{ij} = c_i + h_i + \dots + h_{j-1}$, let $\tilde C(i) = c_i - H(i-1)$, and let

$$S(i, j) = \sum_{r=i}^{j-1} h_r\,\bigl(D(j) - D(r)\bigr)$$

be the carrying cost of an order placed in period $i$ that covers the demands of periods $i, \dots, j$.

The costs are given by the zero-inventory recursion (2): $F(0) = 0$ and, for $1 \le l \le t$,

$$F(l, t) = F(l-1) + K_l + S(l, t) + c_l\,[D(t) - D(l-1)], \qquad F(t) = \min_{1 \le l \le t} F(l, t).$$

$F(l, t)$ is the cost of the first $t$ periods when the last setup is in period $l$.

For two periods $k < l$ the difference $\Delta_{k,l}(t) = F(k,t) - F(l,t)$ is affine in $D(t)$, with intercept $A(k,l)$ given by (4) and slope $c_{k,l} - c_l = \tilde C(k) - \tilde C(l)$. Its root $G(k,l)$ is defined by (5): $A(k,l)/(\tilde C(l) - \tilde C(k))$ when the slopes differ, and $+\infty$ or $-\infty$ according to the sign of $A(k,l)$ when they agree. It is extended symmetrically, $G(l,k) = G(k,l)$.

At iteration $j$ the future demands are unknown, so a future horizon has a potential cumulative demand $x \ge D(j)$. The $j$th Minimal Optimal Predecessors list $\Omega(j)$ is the set of periods $l \le j$ that are the lowest-index optimal last setup period, among $\{1, \dots, j\}$, for every potential cumulative demand in some open interval above $D(j)$.

Formalization targets

Goal: Theorem 1(a)

Let $j \ge 1$ and let $S = \{i_1, \dots, i_r\}$ with $\Omega(j) \subseteq S \subseteq \{1, \dots, j\}$, ranked so that $\tilde C(i_1) \ge \dots \ge \tilde C(i_r)$, with equal $\tilde C$-values in ascending order of index. Put $g(1) = D(j)$ and $g(l) = G(i_l, i_{l-1})$ for $l = 2, \dots, r$. Then

$$S = \Omega(j) \iff g(1) < g(2) < \dots < g(r) < \infty. \tag{6}$$

Milestones

In attack order:

• identity (1a) for the carrying costs;
• Lemma 2(a)–(d), the linearity of $\Delta_{k,l}$ and the sign test against its root $G(k,l)$;
• the claim that $\Omega(j)$ contains an optimal last setup period for the horizon $j$;
• the strict chains (7)–(8) of the Appendix;
• Theorem 1(b), that under (6) the first entry $i_1$ is an optimal last setup period $l(j)$;
• Theorem 1(c)(i)–(iii), the three elimination rules: $g(2) \le D(j)$ removes $i_1$, $g(k+1) \le g(k)$ removes $i_k$, and $g(r) = \infty$ removes $i_r$.

A supporting item potCost_spec certifies that the potential costs used to define $\Omega(j)$ agree with the paper's $F(l,t)$, up to a term that does not depend on $l$.

Significance

Theorem 1 is what makes the forward algorithm correct. Part (a) reduces the minimality of a candidate list to a condition on consecutive pairs of a sorted list. Part (c) says which entry to delete when the condition fails. Part (b) says where to read off the optimal last setup period. With these, $\Omega(j)$ is maintained by deletions at the ends and in the interior of a list ordered by $\tilde C$, and each period is inserted and deleted at most once; the $O(n \log n)$ bound, and the $O(n)$ bound under the paper's special cost structures, follow from this bookkeeping. The same lower-envelope reasoning appears in the other 1991–1993 algorithms and in later extensions to backlogging and capacitated variants.

The result has a complete published proof. To our knowledge there is no machine-checked development of the Wagner–Whitin recursion or of any of the fast lot-sizing algorithms. This mission produces the model, the breakpoints and the Minimal Optimal Predecessors lists as reusable definitions, and a checked proof of the characterization. It also records two small corrections that a formal reading forces on the printed text (see Formalization scope).

Difficulty

Each piece in isolation is elementary algebra on affine functions. The difficulty is in the combinatorics of the lower envelope with ties. The natural argument "consecutive breakpoints increase, so each line owns an interval" must handle three things:

• equal slopes, where $G = \pm\infty$;
• several lines meeting at one point;
• the lowest-index tie-breaking that makes $\Omega(j)$ minimal.

The "only if" direction needs every failure of (6) to be traced to an element that is never the unique lowest-index optimum on an interval. Ties are exactly where the printed definition of $\Omega(j)$, read literally at a single demand value, breaks the theorem. A proof that ignores ties proves a statement that is false.

Formalization scope

• Data and costs. The data are four functions $\mathbb N \to \mathbb R$ bundled in a structure; values at index $0$ are unused, and no sign conditions are imposed. $F$ is defined by the recursion (2) with $F(0) = 0$. Its identification with the minimum cost over all feasible policies is the paper's Lemma 1 (Wagner–Whitin), which is not part of this mission. The horizon $n$ is not a parameter.
• Breakpoints. $G$ and the critical values $g(\cdot)$ take values in EReal, so $\pm\infty$ are kept distinct from every real number. The final "$< \infty$" of (6) is part of the condition.
• Ranked lists. A ranked set is a duplicate-free List ℕ. Lean lists are 0-based, so the paper's $i_{m+1}$ and $g(m+1)$ are entry $m$ and gval j L m.
• Disclosed change 1, $\Omega(j)$. The page asks for a single potential cumulative demand $D \ge D(j)$ at which $l$ is the lowest-index optimum. With that reading, Theorem 1(a) "only if" and Theorem 1(c) fail when two lines tie exactly at a breakpoint (an explicit five-period instance is in the definition's note). The formalization requires $l$ to be the lowest-index optimum on a nondegenerate open interval of potential demands above $D(j)$. This is the paper's own description of the list on p. 915: "the unique optimal last setup period for any horizon … with potential cumulative demand $g(k) < D < g(k+1)$".
• Disclosed change 2, Lemma 2(d). The printed hypothesis "$c_{k,l} < c_l$" duplicates part (c) and is read as "$c_{k,l} = c_l$". The equivalence "$\Delta_{k,l} \ge 0$ iff $D(t) \ge G(k,l)$" is stated under $A(k,l) \ne 0$, since $A(k,l) = 0$ gives $G = +\infty$ by (5).
• Ruling out trivial formalizations. The hypotheses of the goal are satisfiable for every $j \ge 1$: rank $\{1, \dots, j\}$ itself. $\Omega(j)$ is nonempty (a milestone). $F(t)$ for $t \ge 1$ is a minimum over the nonempty set $\{1, \dots, t\}$, never a default value. $G$ is never replaced by a real-valued junk value at equal slopes.
• Out of scope. Lemma 1, Lemma 3, Corollaries 1–5, Theorem 2, the Algorithm's pseudo-code and its complexity analysis, and the submodularity discussion of §5.
• Reusable infrastructure. The model, the recursion (2), $A$, $G$ and $\Omega(j)$ can be reused for the paper's algorithmic results and for related lot-sizing papers. Proofs of the milestones, in any order, are welcome.

Selected references

• A. Federgruen and M. Tzur, A Simple Forward Algorithm to Solve General Dynamic Lot Sizing Models with n Periods in O(n log n) or O(n) Time, Management Science 37(8):909–925, 1991. https://doi.org/10.1287/mnsc.37.8.909
• H. M. Wagner and T. M. Whitin, Dynamic Version of the Economic Lot Size Model, Management Science 5(1):89–96, 1958. https://doi.org/10.1287/mnsc.5.1.89
• A. Wagelmans, S. van Hoesel and A. Kolen, Economic Lot-Sizing: An O(n log n) Algorithm That Runs in Linear Time in the Wagner-Whitin Case, Operations Research 40(1-supplement-1):S145–S156, 1992. https://doi.org/10.1287/opre.40.1.S145
• A. Aggarwal and J. K. Park, Improved Algorithms for Economic Lot Size Problems, Operations Research 41(3):549–571, 1993. https://doi.org/10.1287/opre.41.3.549

Motivation

(r, Q) policies are the standard replenishment rule for a single item under continuous review: whenever the inventory position (stock on hand plus on order minus backorders) drops to the reorder point $r$, an order of size $Q$ is placed. They are known to be optimal in the classical models with Poisson or compound renewal demand, constant or exogenous lead times and full backlogging, and they are used widely in practice and in multi-item and multi-echelon systems where they are applied item by item.

For decades, computing an optimal pair $(r, Q)$ exactly was not routine. The textbook treatment of Hadley and Whitin (1963) gives approximations; as Browne and Zipkin (1991) put it, "until recently, there was no reliable, straightforward method for computing an optimal (r, Q) policy, even in the simple case of Poisson demand processes." Many heuristics were proposed (surveyed by Lee and Nahmias, 1989); the only exact procedure in circulation was in Zipkin's classnotes, based on a result of Sahin (1982).

Federgruen and Zheng (1992) give a short exact algorithm, Algorithm OPT, whose work is linear in the optimal order quantity $Q^*$. It rests only on the form of the cost, not on a particular demand model.

Setting

Inventory positions are integers (demand arrives unit by unit). A fixed cost $\kappa>0$ is charged per order, and $G:\mathbb Z\to\mathbb R$ is the expected holding and backlogging cost rate as a function of the inventory position $y$. In all the models of the paper the long-run average cost of the $(r,Q)$ policy, for an integer $r$ and an integer $Q\ge1$, has the form

$$C(r,Q)=\Big[\kappa+\sum_{y=r+1}^{r+Q}G(y)\Big]\Big/Q. \tag{1}$$

The paper's standing assumptions on $G$ are:

1. $-G$ is unimodal: there is an integer $m$ with $G$ nonincreasing on $\{y\le m\}$ and nondecreasing on $\{y\ge m\}$ (flat stretches allowed);
2. $\lim_{|y|\to\infty}G(y)=\infty$.

The sequence $y_Q$. Let $y_1$ be an integer minimizing $G$. Given $y_1,\dots,y_Q$, let $L(Q)=\min\{y_1,\dots,y_Q\}$ and $R(Q)=\max\{y_1,\dots,y_Q\}$, and set

$$y_{Q+1}=\begin{cases}L(Q)-1 & \text{if } G(L(Q)-1)\le G(R(Q)+1),\\ R(Q)+1 & \text{otherwise.}\end{cases}$$

So the window $[L(Q),R(Q)]$ grows by one point at a time towards the smaller neighbouring value, ties going left. Write $r^*(Q)$ for an optimal reorder point for a given $Q$, and

$$C^*(Q)=\Big[\kappa+\sum_{i=1}^{Q}G(y_i)\Big]\Big/Q .$$

Algorithm OPT, Step 1. Variables $S,Q,C^*,r,R$ start at $S=\kappa+G(y_1)$, $Q=1$, $C^*=S$, $r=y_1-1$, $R=y_1+1$. Each pass compares $G(r)$ and $G(R)$; on the smaller side (left on ties) it stops if $C^*$ is at most that value, and otherwise adds the value to $S$ and moves $r$ one step left or $R$ one step right; then $Q:=Q+1$ and $C^*:=S/Q$. The output is the final $(r,Q)$.

Formalization targets

Goal: Theorem 1

Under the standing assumptions, Step 1 of Algorithm OPT, started from any global minimizer $y_1$ of $G$, stops after finitely many passes, and its output $(r,Q)$ satisfies $Q\ge1$ and

$$C(r,Q)\le C(r',Q')\qquad\text{for all integers } r' \text{ and all integers } Q'\ge 1 .$$

The goal fixes no constants and no demand model: it is a statement about every $G$ satisfying the standing assumptions.

Milestones, in proof order

• §2, p. 811: $\{y_1,\dots,y_Q\}$ is the contiguous block $[L(Q),R(Q)]$ of $Q$ integers and carries the $Q$ smallest values of $G$.
• Figure 1 (p. 809): $y_{Q+1}$ has the least $G$-value outside the window; in particular $G(y_1)\le G(y_2)\le\cdots$.
• Lemma 1: $L(Q)-1$ is an optimal reorder point for $Q$.
• Corollary 1: $r^*(Q)-1\le r^*(Q+1)\le r^*(Q)$.
• Display before (6): $\min_r C(r,Q)=C^*(Q)$.
• (6): $C^*(Q+1)=[QC^*(Q)+G(y_{Q+1})]/(Q+1)$, and $C^*(Q+1)<C^*(Q)$ iff $G(y_{Q+1})<C^*(Q)$.
• Lemma 2: the smallest $q$ with $C^*(q)\le G(y_{q+1})$ exists and is an optimal order size.
• Step 1 tracks the sequence: from the state $(\kappa+\sum_{i\le Q}G(y_i),\,Q,\,C^*(Q),\,L(Q)-1,\,R(Q)+1)$ one pass stops with $(L(Q)-1,Q)$ exactly when $C^*(Q)\le G(y_{Q+1})$ and otherwise moves to the same state for $Q+1$.

Significance

The result turns the joint minimization of (1) over $(r,Q)\in\mathbb Z\times\mathbb Z_{\ge1}$, an unbounded two-dimensional integer problem, into a single scan whose length is $Q^*$ plus the distance to the minimizer of $G$. Because it uses only the form (1) and the unimodality of $-G$, it applies at once to Poisson and compound Poisson demand, to stochastic lead times with an equilibrium lead-time demand, and to cost structures with stockout penalties; the paper also notes extensions to $(r,nQ)$ policies. Lemma 1 and Corollary 1 additionally give the structure of the optimal reorder point as a function of $Q$.

The result has been proved on paper since 1992. What this mission adds is a machine-checked proof of the algorithm's correctness for general $G$ under exactly the paper's hypotheses. The platform already has the linear-cost special case of the underlying lemmas for one discrete demand model (InventoryControl.rq_discrete_recursion, rq_discrete_joint_optimal), but with $C(Q)$ and $Q^*$ given as hypotheses and no algorithm; nothing on the platform states the algorithm or treats general unimodal $-G$.

Difficulty

The obvious argument says: for fixed $Q$ the sum in (1) should cover the $Q$ smallest values of $G$, and the greedy window collects exactly those. Both halves need care on the integers with flat stretches of $G$: "the $Q$ smallest values" is ambiguous under ties, and the claim that a greedy window holds them relies on $y_1$ being a global minimizer together with the unimodality of $-G$, not on convexity.

The stopping rule is the second point. Lemma 2 looks like a first-order condition, but $C^*(\cdot)$ need not be convex; optimality of the first stopping $q$ for all larger $Q$ uses that the values $G(y_i)$ are nondecreasing along the sequence, which the paper uses without stating. Termination of the algorithm is not discussed on the page; it needs $G\to\infty$, and fails for constant $G$.

Finally, the goal is about an imperative loop. Connecting its five variables to $y_Q$, $C^*(Q)$ and $L(Q)$ is an invariant argument that has to match the tie-breaking and the non-strict stopping tests exactly.

Formalization scope

• Types. $G:\mathbb Z\to\mathbb R$, $\kappa\in\mathbb R$ with $\kappa>0$, reorder points in $\mathbb Z$, order quantities in $\mathbb N$ with $Q\ge1$ required wherever a cost appears. Lean's $x/0=0$ makes $C(r,0)=0$, so optimality is always quantified over $Q'\ge1$ and the goal asserts that the returned $Q$ is $\ge1$.
• Assumptions. "$-G$ unimodal" is NegUnimodal G: $\exists m$, $G$ antitone on $(-\infty,m]$ and monotone on $[m,\infty)$. "$\lim_{|y|\to\infty}G=\infty$" is Coercive G: $G\to+\infty$ along atBot and atTop. Mathlib's QuasiconvexOn ℤ is not used: over $\mathbb Z$-weights it holds for every function.
• The sequence. $L(Q),R(Q)$ are defined by recursion on the window, and $y$ is 1-based with an unused value at index 0; that $L,R$ are the minimum and maximum of $\{y_1,\dots,y_Q\}$, as the paper defines them, is the first milestone.
• The algorithm. Step 1 is transcribed literally, including $G(r)\le G(R)$ → left and the non-strict tests $C^*\le G(r)$, $C^*\le G(R)$; $G$ is evaluated directly instead of through the $\Delta G$ bookkeeping. The loop runs with a pass budget and returns nothing when the budget runs out; the goal states that for every large enough budget it returns an optimal pair.
• Step 0 is not formalized. It scans $L=0,1,\dots$ for the first $L$ with $\Delta G(L)\ge0$, under the paper's simplification $y_1>0$; under unimodality alone it can stop on a plateau before the minimum. The goal starts Step 1 from a given global minimizer $y_1$, which is the paper's own §2 setup and matches its p. 812 remark that Step 0 may be replaced by a bisection search.
• Not formalized: Theorem 1's second sentence (the operation count), the derivations of (1) for specific demand models, and (5).
• Corrected slips. The printed proof of Lemma 2 writes $C(Q)-C(Q^*)$ with $C^*(Q)$ inside the bracket; the correct identity has $C^*(Q)-C^*(Q^*)$ and $C^*(Q^*)$. Lemma 2's "$Q^*$" is formalized as existence of the smallest $q$ with the property plus its optimality, since minimizers need not be unique; likewise "$r^*(Q)=L(Q)-1$" means $L(Q)-1$ is an optimal reorder point.
• Ruled out. Defining the algorithm's output as an argmin of $C$, or by searching for Lemma 2's $q$, would make the goal trivial; the algorithm is defined by its steps. A statement of the form "if the run returns a pair, it is optimal" would be vacuous for a loop that never stops; termination is part of the goal.

Proofs of any milestone are welcome, as are general lemmas on windows of unimodal integer sequences, which are reusable beyond this mission.

Selected references

• A. Federgruen and Y.-S. Zheng, An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4):808–813, 1992. https://doi.org/10.1287/opre.40.4.808
• G. Hadley and T. M. Whitin, Analysis of Inventory Systems, Prentice-Hall, 1963.
• S. Browne and P. Zipkin, Inventory Models with Continuous, Stochastic Demands, Annals of Applied Probability 1(3):419–435, 1991. https://doi.org/10.1214/aoap/1177005875
• H. L. Lee and S. Nahmias, Single-Product, Single-Location Models, in Handbooks in OR & MS vol. 4, 1993 (cited by the paper as a 1989 working paper).
• I. Sahin, On the Objective Function Behavior in (s, S) Inventory Models, Operations Research 30(4):709–724, 1982. https://doi.org/10.1287/opre.30.4.709

Why total tardiness on one machine

A shop that promises delivery dates is judged by how late its orders are, not by how early. For a single machine processing $n$ jobs that are all available at time $0$, the total tardiness of a processing order,

$$T=\sum_{i\in J}\max(0,\,C_i-d_i),$$

charges each job the amount by which its completion time $C_i$ exceeds its due date $d_i$, and nothing for finishing early. It is one of the basic criteria of deterministic scheduling (Conway, Maxwell and Miller, Theory of Scheduling, 1967), and the single-machine problem of minimizing it is the core subproblem of many dispatching and decomposition methods.

Two contrasting rules are classical. Sequencing in order of shortest processing time (SPT) minimizes total lateness $\sum_i (C_i-d_i)$ and total completion time (Smith, 1956), and it minimizes total tardiness when every job is tardy under it. Sequencing by earliest due date (EDD) minimizes total tardiness when at most one job is tardy under it. Between these extremes no simple rule is optimal, and before 1969 the proposed exact methods (Held and Karp, 1962; Lawler, 1964; Elmaghraby, 1968) searched subsets of schedules.

Timeline.

• 1956: Smith's ratio rule for weighted completion time; SPT for flow time and lateness.
• 1965: Root notes that SPT is optimal for total tardiness when all due dates are equal.
• 1969: Emmons (Operations Research 17(4)) proves dominance theorems that fix the relative order of pairs of jobs in some optimal schedule, and derives from them general sufficient conditions for SPT and EDD optimality.
• 1977: Lawler gives a pseudopolynomial algorithm, built on Emmons's dominance results (Annals of Discrete Mathematics 1).
• 1990: Du and Leung prove the problem NP-hard (Mathematics of Operations Research 15(3)), so sufficient conditions of Emmons's kind are the most one can expect from a simple rule.

This mission formalizes Emmons's SPT side: the pairwise dominance theorem for a shorter job before a longer one, and its corollary that the SPT schedule is optimal under a condition far weaker than "every job is tardy".

Setting

A finite set $J$ of jobs is processed on one machine. Job $i$ has a processing time $p_i\ge 0$ and a due date $d_i\in\mathbb R$. A schedule of $J$ is an ordering of the jobs of $J$; the machine starts at time $0$, never idles, and processes the jobs in that order, so a job's completion time $C_i$ is the sum of the processing times of the jobs up to and including it. Its tardiness is $T_i=\max(0, C_i-d_i)$, and the schedule's total tardiness is $T=\sum_{i\in J}T_i$. A schedule is optimal if no schedule of $J$ has smaller total tardiness.

Following Emmons, jobs are SPT-indexed: $J_1,\dots,J_n$ are numbered so that $j<k$ implies $p_j<p_k$, or $p_j=p_k$ and $d_j\le d_k$. The SPT schedule processes $J_1,J_2,\dots,J_n$ in this order.

Emmons's notation $j\leftarrow k$ ("$J_j$ precedes $J_k$ in an optimal schedule") means that there exists an optimal schedule having all properties already established and in which $J_j$ comes before $J_k$. The set $B_k$ collects the jobs already known to precede $J_k$.

Formalization targets

Goal: Corollary 1.4 (p. 705)

$$d_j+p_j\le\sum_{i=1}^{j+1}p_i\quad(j=1,\dots,n-1)\quad\Longrightarrow\quad\text{the SPT schedule minimizes } \sum_{i\in J}\max(0,C_i-d_i).$$

The condition can be read as $d_j\le C_j+(p_{j+1}-p_j)$ with $C_j$ the SPT completion time of $J_j$, so it allows jobs to be early. It is the paper's sufficient condition for SPT optimality, and the conclusion is optimality against every schedule of $J$.

Milestones

1. Interchange claim (proof of Theorem 1, p. 703): in a schedule where all of $B$ precede $J_k$ and $J_k$ precedes $J_j$, with $j<k$ and $d_j\le\max(\sum_{B}p_i+p_k,\,d_k)$, interchanging $J_j$ and $J_k$ does not increase total tardiness.
2. Theorem 1 (p. 703): if some optimal schedule has all of $B$ before $J_k$ and $d_j\le\max(\sum_{B}p_i+p_k,\,d_k)$, then some optimal schedule has all of $B$ before $J_k$ and also $J_j$ before $J_k$.
3. Corollary 1.1 (p. 704): if $d_1\le\max(p_i,d_i)$ for all $i>1$, then $J_1$ is first in an optimal schedule.
4. Time re-referencing (p. 705): processing $J_k$ first leaves the problem on $J\setminus\{J_k\}$ with due dates $d_i-p_k$.
5. First-job reduction (p. 705): $J_k$ followed by an optimal schedule of that reduced problem is optimal, whenever some optimal schedule starts with $J_k$.

Two further results are included as supporting statements: Corollary 1.2 (p. 705, $J_n$ last) and Corollary 2.3 (p. 707, the adjacent-pair rule $j\leftarrow k$ iff $d_j\le\max(W+p_k,d_k)$ after a waiting time $W$).

Significance

Corollary 1.4 turns an NP-hard problem into a closed-form answer on a recognizable class of instances: one pass over the SPT order checks the condition, and if it holds no search is needed. Theorem 1 is the more general tool. It orders pairs of jobs in an optimal schedule, and together with Emmons's companion theorems it underlies later exact methods for total tardiness, including Lawler's decomposition and the branch-and-bound algorithms that use Emmons's dominance rules for pruning.

The results are proved in the paper. What a formalization adds is a checked account of the step that the paper treats informally: dominance statements are existential ("some optimal schedule has $J_j$ before $J_k$"), and the paper argues on p. 702 that such statements can be accumulated. Each statement here makes explicit which previously established properties the new optimal schedule keeps. No machine-checked proof of these results was found on Prove2Me or in Mathlib at the time of drafting.

Difficulty

The obvious argument is a pairwise interchange, but the interchanged jobs are not adjacent. Moving $J_k$ from before $J_j$ to $J_j$'s position shifts every job in between, changes two tardiness terms in different directions, and the comparison depends on where the due dates fall relative to the start of $J_k$ and the end of $J_j$. The hypothesis involving $\sum_{B_k}p_i$ only controls the start time of $J_k$ through the information that $B_k$ precedes it, so the existence statement must carry that information along.

The goal is not a direct consequence of Theorem 1 applied pairwise: existential conclusions for different pairs need not hold in a common optimal schedule. Optimality of one fixed order requires all the pairwise decisions to be realized simultaneously, and the problem changes (due dates shift) once a job is fixed in place.

Formalization scope

Jobs are elements of a type $\iota$ with a linear order that plays the role of the paper's index, and the job set is a Finset ι; this lets the reduction remove a job and keep the remaining labels. Schedules and completion times are the published definitions MooreLateJobs.Shared.IsSchedule and MooreLateJobs.Shared.completionTime (duplicate-free lists containing exactly the jobs of $J$; prefix sums of processing times from time $0$). Tardiness, total tardiness, optimality (against every schedule of $J$), "precedes" (comparison of positions), the SPT indexing convention and the SPT schedule (the jobs sorted by index) are defined in EmmonsTardiness.SPT.Model. Processing times and due dates are real.

Conventions and deviations from the page:

• Added: processing times are nonnegative, $p_i\ge0$ for $i\in J$. They are durations; the proof of Theorem 1 uses that the start time of $J_k$ is at least $\sum_{B_k}p_i$, and Corollary 2.3's second direction is false without it.
• Not imposed: the reduction $d_i<\sum_J p_i$ of p. 703. It is a without-loss-of-generality preprocessing step that no statement needs, so dropping it makes the statements stronger.
• Kept: the SPT indexing convention of p. 703 is a hypothesis of every statement that refers to job indices.
• $j\leftarrow k$: the "properties already established" are the precedences named in hypothesis (1); the broader cumulative reading of p. 702 is not formalized.

A formalization of the goal as "some optimal schedule starts with $J_1$", or of Theorem 1 with an arbitrary set $B$ unrelated to optimal schedules, would be a different and weaker (or false) statement; the targets above state optimality of the SPT schedule itself and tie $B$ to an optimal schedule.

Needed infrastructure: lemmas on prefix sums of lists, on the effect of a transposition on positions in a duplicate-free list, on removing the head of a schedule, and existence of an optimal schedule among the finitely many permutations of $J$. These list-scheduling lemmas are reusable for other single-machine results (Moore 1968, and the EDD mission of this series). Proofs of the milestones, alternative arguments, and general interchange lemmas are all welcome.

Selected references

• H. Emmons, One-Machine Sequencing to Minimize Certain Functions of Job Tardiness, Operations Research 17(4):701–715, 1969. https://doi.org/10.1287/opre.17.4.701
• 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
• J. G. Root, Scheduling with Deadlines and Loss Functions on k Parallel Machines, Management Science 11:460–475, 1965. https://doi.org/10.1287/mnsc.11.4.460
• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1):102–109, 1968. https://doi.org/10.1287/mnsc.15.1.102
• E. L. Lawler, A "Pseudopolynomial" Algorithm for Sequencing Jobs to Minimize Total Tardiness, Annals of Discrete Mathematics 1:331–342, 1977. https://doi.org/10.1016/S0167-5060(08)70742-8
• J. Du, J. Y.-T. Leung, Minimizing Total Tardiness on One Machine is NP-Hard, Mathematics of Operations Research 15(3):483–495, 1990. https://doi.org/10.1287/moor.15.3.483

Motivation

A function that is bounded below need not attain its infimum: $e^x$ on $\mathbb{R}$ has infimum $0$ and no minimizer. The classical "variational principle" says that at a minimizer $\bar u$ of a differentiable functional, $F'(\bar u)=0$. Without compactness there may be no minimizer, and the principle has nothing to say. In 1974 Ivar Ekeland showed that a weaker statement survives in every complete metric space: next to any approximate minimizer lies a point that is the exact, strict minimizer of a slightly perturbed function (Ekeland 1974).

The result is now a standard tool in nonlinear analysis, optimization and the calculus of variations. It yields approximate first-order conditions ($\|F'(v)\|_*\le\varepsilon$) without existence of minimizers, approximate Lagrange multiplier rules, and approximate maximum principles in optimal control; Ekeland's survey (Ekeland 1979) collects many of these uses.

Timeline. Bishop and Phelps introduced the partial order on a Banach space times $\mathbb{R}$ that underlies the proof, in their study of support functionals of convex sets (Bishop–Phelps, The support functional of a convex set, Proc. Symp. Pure Math. 7, AMS, 1963). Brøndsted and Rockafellar used it in 1965 to obtain subdifferentiability properties of convex functions on Banach spaces (Brøndsted–Rockafellar 1965), and Browder applied it to nonconvex subsets of Banach spaces (Bull. AMS 79, 1973). Ekeland's 1974 article, formalized here, isolates the device as a principle valid in every complete metric space for lower semicontinuous functions with values in $\mathbb{R}\cup\{+\infty\}$, and applies it to Gâteaux-differentiable functions, constrained optimization, Plateau's problem, geodesics and optimal control.

Setting

Let $(V,d)$ be a complete metric space. Let $F:V\to\mathbb{R}\cup\{+\infty\}$ be lower semicontinuous (for every $c$ the set $\{F\le c\}$ is closed), not identically $+\infty$, and bounded from below:

$$\inf F > -\infty. \tag{1.1}$$

For $\varepsilon>0$, a point $u\in V$ is an $\varepsilon$-minimizer if

$$\inf F \le F(u) \le \inf F + \varepsilon. \tag{1.2}$$

For $\alpha>0$, the Bishop–Phelps order on $V\times\mathbb{R}$ is

$$(v_1,a_1)\prec(v_2,a_2)\iff (a_2-a_1)+\alpha\,d(v_1,v_2)\le 0. \tag{1.6}$$

In Lean it is EkelandVP.General.bpLE α p q, read $p\prec q$. The epigraph of $F$ is $S=\{(v,a)\mid a\ge F(v)\}\subseteq V\times\mathbb{R}$ (1.15).

In §2, $V$ is a real Banach space with dual $V^*$, and $F$ is Gâteaux-differentiable with derivative $F':V\to V^*$ (EkelandVP.General.IsGateauxDiff F F'): at every $u_0$ with $F(u_0)<+\infty$, $\frac{d}{dt}F(u_0+tv)|_{t=0}=\langle F'(u_0),v\rangle$ for every $v$ (2.1).

Formalization targets

Goal: Theorem 1.1 (p. 324)

For every $u$ satisfying (1.2) and every $\lambda>0$ there is $v\in V$ with

$$F(v)\le F(u),\qquad d(u,v)\le\lambda,\qquad \forall w\ne v:\ F(w)>F(v)-\frac{\varepsilon}{\lambda}\,d(v,w). \tag{1.3–1.5}$$

The parameters $\varepsilon$ and $\lambda$ are free; the trade-off between closeness to $u$ and the size of the perturbation is the content of the theorem.

Milestones (§1)

1. For $\alpha>0$, $\prec$ is reflexive, antisymmetric and transitive (p. 325).
2. For every $(v_1,a_1)$, the set $\{(v,a)\mid (v_1,a_1)\prec(v,a)\}$ is closed in $V\times\mathbb{R}$ (p. 325).
3. Lemma 1.2 (p. 325): if $S\subseteq V\times\mathbb{R}$ is closed and $a\ge m$ on $S$ for some $m$ (1.7), then every $(v_1,a_1)\in S$ lies below a $\prec$-maximal element of $S$.

Consequences (§2)

• Corollary 2.3 (p. 328): for $V$ Banach, $F$ l.s.c. and Gâteaux-differentiable with $-\infty<\inf F<+\infty$, and every $\varepsilon>0$, there is $v_\varepsilon$ with $F(v_\varepsilon)-\inf F\le\varepsilon^2$ and $\|F'(v_\varepsilon)\|_*\le\varepsilon$.
• Corollary 2.4 (p. 328): if moreover $F(v)\ge k\|v\|+c$ with $k>0$, then $F'(V)$ is dense in $kB^*$.
• Corollary 2.5 (p. 329): if $F(v)\ge\Phi(\|v\|)$ with $\Phi$ continuous and $\Phi(t)/t\to\infty$, then $F'(V)$ is dense in $V^*$.

Significance

The result. Theorem 1.1 replaces "a minimizer exists" by "a strict minimizer of a Lipschitz perturbation exists nearby", with explicit control of both the distance and the perturbation. With $\lambda=\sqrt{\varepsilon}$ this gives a point that is $\varepsilon$-optimal, $\sqrt{\varepsilon}$-close to $u$, and $\sqrt{\varepsilon}$-stationary in the metric sense. Corollary 2.3 is the form announced in the paper's abstract: a differentiable function with a finite lower bound has points where $F$ is almost minimal and $\|F'\|_*$ is arbitrarily small. Later sections of the same paper use Theorem 1.1 for approximate Lagrange multiplier rules (§3) and an approximate Pontryagin maximum principle (§7), which are the subjects of missions II and III of this series.

Formalizing it. The theorem is proved; this mission formalizes the paper's own route (the order (1.6), Lemma 1.2, then Theorem 1.1) and its first applications in §2. The pinned Mathlib has no statement of Ekeland's principle, of the Caristi fixed point theorem, or of the Bishop–Phelps order, and the platform has none either. A machine-checked Theorem 1.1 for extended-real-valued functions would be directly reusable by every later mission that needs approximate optimality without compactness.

Difficulty

The obvious argument — take a minimizing sequence and pass to a limit — fails because nothing makes a minimizing sequence converge: $V$ is not compact, and a minimizing sequence of $e^x$ escapes to $-\infty$. Completeness only helps for Cauchy sequences, so one must construct a sequence that is Cauchy. The limit must moreover be maximal for the order (1.6), not merely a limit point, and that maximality is what produces the strict inequality (1.5). Lemma 1.2 is where this difficulty sits. In §2, the passage from the metric statement (1.5) to a bound on $\|F'(v)\|_*$ requires $F$ to be finite near $v$ along every line, which the Gâteaux hypothesis supplies.

Formalization scope

• $V$ is a MetricSpace with CompleteSpace; $d(u,v)$ is dist u v. $V\times\mathbb{R}$ carries the product topology; only closedness of subsets of it is used.
• $F:V\to$ EReal. "Bounded from below" (1.1) is $\bot<\inf_v F(v)$; it also excludes the value $-\infty$, which the paper's codomain does not contain. "Not identically $+\infty$" is $\exists v_0,\ F(v_0)\ne\top$. Lower semicontinuity is Mathlib's LowerSemicontinuous.
• (1.2) is assumed in the form $F(u)\le\inf F+\varepsilon$ with $\varepsilon>0$ real (the left half is automatic). $\lambda$ is named lam.
• (1.5) is $F(v)-\frac{\varepsilon}{\lambda}d(v,w)<F(w)$ for all $w\ne v$, strict, with the paper's argument order $d(v,w)$. Since $F(v)$ is finite under the hypotheses, the EReal subtraction is ordinary.
• A trivializing formalization is ruled out: $F$ is not real-valued (the value $+\infty$ is what lets §3 apply the theorem to $F$ plus the indicator of a closed set), (1.5) is strict and quantified over all $w\ne v$, and the conclusion is not weakened to $d(u,v)<\infty$ or $\le$ in (1.5).
• In §2, $V$ is a real NormedSpace with CompleteSpace, $F'$ is a function $V\to(V\to_L\mathbb{R})$, and Gâteaux differentiability requires $t\mapsto F(u_0+tv)$ to be finite near $t=0$ before taking a real derivative; without this, EReal.toReal $(\pm\infty)=0$ would let an infinite function have a junk derivative. Density of $F'(V)$ is stated for derivatives taken at points where $F<+\infty$.
• Theorem 2.2 is not part of this mission: its conclusion (2.4) is printed as the strict $\|v-u\|<\lambda$, while its one-line proof from Theorem 1.1 gives only $\le\lambda$. Corollaries 2.3–2.5 do not depend on the strict form.

Contributions welcome: proofs of the milestones (the first two are short; Lemma 1.2 is the core), of Theorem 1.1, and of the §2 corollaries; a reusable Caristi fixed point theorem built on the same order would be a natural addition.

Selected references

• I. Ekeland, On the Variational Principle, J. Math. Anal. Appl. 47 (1974), 324–353. https://doi.org/10.1016/0022-247X(74)90025-0
• I. Ekeland, Nonconvex minimization problems, Bull. Amer. Math. Soc. (N.S.) 1 (1979), 443–474. https://doi.org/10.1090/S0273-0979-1979-14595-6
• E. Bishop, R. R. Phelps, The support functional of a convex set, in Convexity (V. Klee, ed.), Proc. Symp. Pure Math. 7, Amer. Math. Soc., 1963, 27–35. (Reference [4] of Ekeland 1974.)
• A. Brøndsted, R. T. Rockafellar, On the subdifferentiability of convex functions, Proc. Amer. Math. Soc. 16 (1965), 605–611. https://doi.org/10.1090/S0002-9939-1965-0178103-8
• F. E. Browder, Normal solvability for nonlinear mappings into Banach spaces, Bull. Amer. Math. Soc. 79 (1973), 328–350. https://doi.org/10.1090/S0002-9904-1973-13152-9

Motivation

Two-stage stochastic linear programs model decisions taken before uncertainty is resolved (first stage) and corrected afterwards at a cost (second stage, the recourse). The standard solution method for problems with finitely many scenarios is the L-shaped method of Van Slyke and Wets (1969), an outer linearization in the style of Benders decomposition: a master program approximates the expected recourse function by cutting planes, one cut per iteration. Birge and Louveaux (1988) proposed the multicut variant, which approximates the recourse function of each realization separately and can add several cuts per iteration, and compared the two methods by worst-case counts of major iterations.

The paper's §5 treats the special case of simple recourse, where the second stage only penalizes shortage and surplus of each component of the first-stage output against a random target. Simple recourse arises in production planning, inventory and capacity models, and is the case in which the recourse function separates into one-dimensional pieces. There the paper derives an explicit LP (25) equivalent to the problem, a dedicated multicut algorithm for it, and the bound of $Jm_2+1$ iterations quoted below. This mission formalizes that section.

Setting

First-stage data are $c\in\mathbb R^{n_1}$, $A\in\mathbb R^{m_1\times n_1}$, $b\in\mathbb R^{m_1}$, and the first-stage feasible set is $K_1=\{x\mid Ax=b,\ x\ge0\}$. A deterministic technology matrix $T\in\mathbb R^{m_2\times n_1}$, with rows $T_i$, maps $x$ to the tender $\chi=Tx\in\mathbb R^{m_2}$. Problem (3) of the paper is

$$\min\ z(x)=cx+\Psi(Tx)\quad\text{s.t. } x\in K_1 .$$

For each row $i=1,\dots,m_2$ the random vector $\xi_i=(q_i^+,q_i^-,h_i)$ takes $J$ values $\xi_{ij}=(q^+_{ij},q^-_{ij},h_{ij})$ with probabilities $p_{ij}$. The simple recourse cost (20) of row $i$ is the optimal value of a one-row LP,

$$\psi_i(\chi_i,\xi_{ij})=\min\{q^+_{ij}y^+ + q^-_{ij}y^- \mid y^+-y^-=h_{ij}-\chi_i,\ y^+,y^-\ge0\},$$

and by separability (19) the expected recourse function is $\Psi(\chi)=\sum_i\Psi_i(\chi_i)$ with $\Psi_i(\chi_i)=\sum_j p_{ij}\psi_i(\chi_i,\xi_{ij})$. Write $q_{ij}=q^+_{ij}+q^-_{ij}$.

The multicut algorithm for simple recourse problems (p. 389) keeps a set $I$ of identified pairs $l=(i,j)$, initially empty. Step 1 solves the master program (26),

$$\min\ cx+\sum_{i,j}p_{ij}q^-_{ij}(T_ix)+\sum_{l\in I}u_l\quad\text{s.t. } Ax=b,\ x\ge0,\ u_l\ge e_l-E_lx,\ u_l\ge0\ (l\in I),$$

with $E_l=p_{ij}q_{ij}T_i$ and $e_l=p_{ij}q_{ij}h_{ij}$. Step 2 adds to $I$ every pair for which the constraint $0\ge p_{ij}q_{ij}(h_{ij}-T_ix^\nu)$ (27) is violated at the master's solution $x^\nu$, and returns to Step 1; when no pair is added the algorithm stops.

Formalization targets

Goal: the $Jm_2+1$ bound, with correctness

The paper states (p. 389): "The initial problem (26) involves $m_1$ constraints and $n_1$ variables. For this problem, the worst-case situation is when at each iteration, only one constraint (27) is violated in Step 2. Then, the maximal number of iterations is $Jm_2+1$." The goal asserts, for every run of the algorithm (any optimal solution of (26) may be used at each Step 1):

$$\nu\text{-th solve of Step 1 takes place}\ \Longrightarrow\ \nu\le Jm_2+1,$$

and, when the algorithm stops at $x^\nu$, $x^\nu\in K_1$ and $cx^\nu+\Psi(Tx^\nu)\le cx+\Psi(Tx)$ for all $x\in K_1$.

Milestones

1. (22)–(23): for $q^++q^-\ge0$ the LP (20) attains its minimum $\max\{q^-(\chi-h),q^+(h-\chi)\}$, so each $\theta_{ij}$ has only two cuts.
2. (24)–(25): the simple recourse problem is equivalent to the LP (25): same optimal $x$, and the value of (25) at $x$ with the best slacks is $z(x)$.
3. Relaxation and stopping: (26) is a relaxation of (25), and if no unidentified pair violates (27) at an optimum of (26), that optimum (extended by zero slacks) is optimal for (25).
4. Facets: each $\Psi_i$ is a maximum of $J+1$ affine functions, so $\Psi$ is a maximum of at most $(J+1)^{m_2}$ affine functions.

Significance

The bound is linear in $m_2$ and $J$, while the L-shaped method may need as many iterations as $\Psi$ has facets, up to $(J+1)^{m_2}$ (milestone 4). This is the paper's clearest instance of the multicut method's worst-case advantage, and the equivalence (25) shows that simple recourse problems are LPs of size linear in $m_2J$, a fact used throughout the later literature on simple and integrated recourse.

The results are proved in the paper, briefly. To our knowledge none has a machine-checked proof. Formalizing them produces a checked reduction of simple recourse to an explicit LP, a checked correctness proof of a constraint-generation algorithm with an explicit iteration bound, and the piece count of a sum of one-dimensional convex piecewise linear functions.

Difficulty

The counting argument is short once the algorithm is pinned down; the difficulty lies in the rest. Correctness at stopping requires relating three optimization problems (3), (25) and (26) whose objectives differ by a constant and by slack variables that are only present for identified pairs, and doing so for an arbitrary optimal solution of the master. The step from (20) to (22)–(23) requires solving an LP in closed form, as an infimum that must first be shown finite. The facet count requires showing that a sum of $J$ convex functions, each with one breakpoint, is a maximum of exactly $J+1$ affine functions, which is not a consequence of convexity alone.

Formalization scope

All vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, realizations are indexed by Fin J, and pairs $(i,j)$ by Fin m2 × Fin J. The second-stage value $\psi$ is the EReal infimum of the LP (20), not its closed form; expectations are finite sums weighted by $p_{ij}\ge0$ with $\sum_jp_{ij}=1$.

Readings pinned down, each recorded in the item statements:

• $q_{ij}\ge0$. The paper never states it, but without it (20) is unbounded below and (25) is not equivalent to (3). It is a field of the model.
• $x\ge0$ belongs to (3) and is omitted in the displays of (25) and (26); it is kept in both.
• Step 2 ranges over unidentified pairs. The paper writes "for each $i$ and $j$"; read literally, an identified pair whose $u_l$ already covers it could be re-added forever. The paper's remark that (27) "identifies any constraints in (25) that are not met" fixes the reading. The state of the algorithm is the set of identified pairs; the order of identification, and so the index $t$, is immaterial.
• Stopping rule. It is implicit in the paper: stop when (27) is violated for no pair.
• Counting. The paper writes "the maximal number of iterations is $Jm_2+1$"; we count solves of Step 1, the stopping solve included, which is what its argument counts.
• Constant. The objective of (26) omits the constant $-\sum p_{ij}q^-_{ij}h_{ij}$ of (25), as printed.
• Facets. "$\Psi_i$ contains $J+1$ facets" is read as "is a maximum of $J+1$ (not necessarily distinct) affine functions".

A formalization in which the master step could fire without a violated, unidentified pair, or in which the algorithm's optimal solutions were fixed in advance, would make the bound either false or empty; the definitions exclude both. The goal includes optimality at stopping so that it is not only a statement about a set growing inside a finite set.

Needed infrastructure: elementary LP feasibility and optimality, finite sums in EReal, and piecewise linear convex functions on $\mathbb R$. Contributions of any of the milestones, in any order, are welcome; milestone 1 is the natural first step.

Selected references

• J.R. Birge and F.V. Louveaux, A multicut algorithm for two-stage stochastic linear programs, European Journal of Operational Research 34 (1988) 384–392. https://doi.org/10.1016/0377-2217(88)90159-2
• R.M. Van Slyke and R. Wets, L-shaped linear programs with applications to optimal control and stochastic programming, SIAM Journal on Applied Mathematics 17 (1969) 638–663. https://doi.org/10.1137/0117061
• J.R. Birge and F.V. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4

Motivation

Two-stage stochastic linear programs with recourse are a standard model for planning under uncertainty: a first-stage decision $x$ is taken before a random outcome $\xi$ is observed, and a second-stage (recourse) decision $y$ corrects for it afterwards at a cost. When $\xi$ has finitely many realizations, the problem is a large but structured linear program, and the classical way to solve it is the L-shaped method of Van Slyke and Wets (1969), a Benders-type outer linearization of the expected recourse cost.

Birge and Louveaux (1988) proposed the multicut L-shaped algorithm: instead of one cut on the expected recourse function per iteration, it adds one cut per realization. They compared the two methods by worst-case counts of major iterations (the operations between two returns to the master problem), and showed that the multicut count grows linearly in the number $K$ of realizations, while their bound for the single-cut method grows like $K^{m_2}$. The multicut idea is now part of every textbook treatment of decomposition for stochastic programming (Birge and Louveaux, Introduction to Stochastic Programming, Ch. 5) and of most production implementations of Benders decomposition.

Setting

The data are a matrix $A\in\mathbb R^{m_1\times n_1}$, vectors $b$, $c$, a fixed recourse matrix $W\in\mathbb R^{m_2\times n_2}$, and $K$ realizations $k=1,\dots,K$, each with a cost $q_k\in\mathbb R^{n_2}$, a right-hand side $h_k\in\mathbb R^{m_2}$, a technology matrix $T_k\in\mathbb R^{m_2\times n_1}$ and a probability $p_k$. Row vectors are written without transposes, as in the paper. The second-stage value of realization $k$ is

$$Q_k(x)=\min\{\,q_k y\mid Wy=h_k-T_kx,\ y\ge 0\,\}\in\mathbb R\cup\{\pm\infty\},$$

the expected recourse is $\Omega(x)=\sum_k p_kQ_k(x)$, and the deterministic equivalent (2) minimizes $cx+\Omega(x)$ over $K_1\cap K_2$, where $K_1=\{x\mid Ax=b,\ x\ge 0\}$ and $K_2$ is the set of $x$ for which every second-stage problem is feasible.

The multicut algorithm keeps feasibility cuts $(D_l,d_l)$ and, for each $k$, optimality cuts $(E_{l(k)},e_{l(k)})$. Step 1 solves the master

$$\min\ cx+\sum_{k}\theta_k\quad\text{s.t. } Ax=b,\ x\ge0,\ D_lx\ge d_l,\ E_{l(k)}x+\theta_k\ge e_{l(k)},$$

ignoring $\theta_k$ when scenario $k$ has no cut. Step 2 tests feasibility of each scenario at the master solution $x^\nu$ and, at the first infeasible one, adds a feasibility cut $(\sigma T_k,\sigma h_k)$ from the simplex multiplier $\sigma$ of a phase-one LP. Step 3 solves each second-stage problem at $x^\nu$ with simplex multiplier $\pi_k$; for every $k$ with $\theta_k<p_k\pi_k(h_k-T_kx^\nu)$ (condition (14)) it adds the optimality cut $(p_k\pi_kT_k,\ p_k\pi_kh_k)$. If no $k$ satisfies (14) the algorithm stops.

The cut set $\mathcal C_k$ is the finite set of all optimality cuts that Step 3 can produce for scenario $k$: the cuts of simplex-optimal bases of the scenario-$k$ problem at points of $K_1$.

Formalization targets

Goal: the iteration bound (17)

The paper states (Theorem, p. 388):

Let b be the slope number of the second stage of (2). Then, the maximum number of iterations for the multicut algorithm is 1 + K(b^{m₂} − 1) (17) while the maximum number of iterations for the L-shaped algorithm is [1 + K(b − 1)]^{m₂} (18) where K is the number of the different realizations of ξ.

The goal is (17) with the number of facets replaced by the number of distinct cuts: if $|\mathcal C_k|\le M$ for every $k$ and $M\ge1$, then in every run of the algorithm, for every choice of optimal master solutions and optimal bases,

$$\#\{\text{returns to Step 1 from Step 3}\}\ \le\ 1+K(M-1).$$

Milestones

1. The feasibility cuts determine $K_2$ (a point lies in $K_2$ exactly when it satisfies every feasibility cut, §2, p. 385), and each optimality cut is an affine minorant of $p_kQ_k$ touching it where it was generated (the multicut algorithm outer-linearizes each $Q_k$, p. 387).
2. Aggregating one cut per scenario gives a valid L-shaped cut, and $z(\text{multi})\ge z(\text{L-shaped})$ (proof of the Proposition, p. 387).
3. When (14) holds for no $k$, $x^\nu$ is optimal for (2) (stopping rule, p. 387).
4. The first return from Step 3 records one cut for each scenario, and every return records at least one cut not recorded before (proof of the Theorem, p. 388).

Significance

The bound explains why the multicut method needs few major iterations: the information sent to the master grows additively over scenarios, while the facets of $\Omega$ are combinations of facets of the $Q_k$ and their number can grow multiplicatively. The paper itself notes the trade-off this creates against master size ($m_1+K$ rows instead of $m_1+1$), which is the basis of later work on partial aggregation of cuts.

The mission produces a formal model of the multicut algorithm as a transition system over all admissible choices, valid-cut lemmas for both cut types with dual feasibility made explicit, the correctness of the stopping rule, and the counting argument. These results are proved on paper but, to our knowledge, no machine-checked version of the multicut L-shaped algorithm or its iteration bound exists. The model is reusable for other results on Benders-type methods for stochastic programs.

Difficulty

The counting argument is short once the right invariants are in place; the difficulty is the invariants. A cut recorded earlier must still be satisfied by the current master solution, while the cut added for a scenario satisfying (14) is violated by it, so the new cut differs from every recorded one. This uses that every recorded cut comes from a basis whose multiplier is dual feasible: a basis that merely attains the optimal value under degeneracy can produce a cut that is not valid. The stopping rule needs strong duality at the final bases and weak duality at all earlier ones, together with extended-real bookkeeping of $Q_k$ on points where a scenario is infeasible.

Formalization scope

The model is the published StochasticProg_Recourse_Instance ($Q_k$ in EReal, $+\infty$ when infeasible) with simplex bases and multipliers from StochasticProg_LShaped_Bases. Vectors are Fin n → ℝ, scenarios Fin K. A simplex-optimal basis is defined locally: invertible basic submatrix, nonnegative basic solution, and dual-feasible multiplier ($\pi W\le q_k$; for the phase-one LP, $\sigma W\le 0$ and $|\sigma_i|\le 1$). The algorithm is an inductive step relation on states (feasibility cuts, per-scenario cut lists, return counter); a run is any finite sequence of steps from the empty state. Master optima are attained optimal solutions, not infima.

Pinned-down readings:

• The paper writes the bound with $b^{m_2}$, from its slope number $b$, and asserts without derivation that each $Q_k$ has at most $b^{m_2}$ facets. We state the bound for any $M$ bounding the number of distinct cuts of each scenario, which is what the paper's proof counts. The L-shaped bound (18) is not stated.
• "Iterations" are returns to Step 1 from Step 3. The final, stopping solve is not counted, consistent with Appendix A (four facets of $\Omega$, five L-shaped solves; two multicut returns), and Step-2 (feasibility) returns are not counted, as in the paper's bound.
• Positive probabilities $p_k>0$ are assumed where $K_2$ or optimality appears (the paper's realizations form the support of $\xi$).
• A scenario with no optimality cut has $\theta_k$ omitted from the objective and always satisfies (14).

The transition relation allows every choice the paper allows; a relation that fixed, say, a particular basis or a particular master solution would prove a bound for fewer runs, and one that required the cut set to be smaller than the paper's would make the bound easy. Neither is done here.

Contributions welcome: proofs of the milestones, a sorry-free proof of the goal from them, and a worked check that the definitions admit the run of Appendix A.

Selected references

• J. R. Birge and F. V. Louveaux, A multicut algorithm for two-stage stochastic linear programs, European Journal of Operational Research 34 (1988) 384–392. https://doi.org/10.1016/0377-2217(88)90159-2
• R. M. Van Slyke and R. J.-B. Wets, L-shaped linear programs with applications to optimal control and stochastic programming, SIAM Journal on Applied Mathematics 17 (1969) 638–663. https://doi.org/10.1137/0117061
• J. F. Benders, Partitioning procedures for solving mixed-variables programming problems, Numerische Mathematik 4 (1962) 238–252. https://doi.org/10.1007/BF01386316
• J. R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4