Linear Optimization

Motivation

Sequential planning problems — inventory replenishment, hydro-thermal power scheduling, asset-liability management — routinely span more than two decision epochs, with information about the future revealed gradually as each period unfolds. A two-stage recourse model (decide now, observe once, recourse once) is too coarse for these: it either collapses the whole horizon into a single "wait and see" observation or forces an ad-hoc rolling-horizon heuristic with no optimality guarantee. The multistage stochastic program is the natural model that keeps the full sequence of decisions and observations, and Benders (L-shaped) decomposition is the workhorse algorithm the field has used to solve it since Van Slyke and Wets [1969] introduced it for the two-stage case. Ho and Manne [1974] and Glassey [1973] first proposed nested decomposition for deterministic multistage models; Louveaux [1980] extended it to multistage quadratic stochastic programs, and Birge [1985] gave the linear multistage generalization this mission formalizes, later implemented at scale by Pereira and Pinto [1985] and Gassmann [1990] and still the basis of production stochastic-programming solvers today.

Setting

A multistage stochastic linear program unfolds over $H$ stages $t = 1,\dots,H$. At each stage, uncertainty resolves into one of finitely many realizations, so the whole process of realizations forms a scenario tree: a single scenario at $t=1$ (the root), branching into finitely many scenarios at $t=2$, each of those again branching at $t=3$, and so on. Write $k$ for a scenario (a tree node) and $a(k)$ for its ancestor, the scenario at stage $t-1$ that $k$ descends from; $D^{t+1}(j)$ is the set of scenario $j$'s descendants at the next stage. Each scenario $k$ at stage $t$ carries its own decision vector $x^t_k \ge 0$, bounded above ($x^t_k \le u^t_k$, coordinatewise), subject to the linear constraint

$$W^t x^t_k = h^t_k - T^{t-1}_k x^{t-1}_{a(k)},$$

where the recourse matrix $W^t$ depends only on the stage (fixed recourse) while the transition matrix $T^{t-1}_k$ and right-hand side $h^t_k$ may vary scenario by scenario. Stacking every scenario's constraint over the whole tree gives the deterministic equivalent linear program, minimizing the probability-weighted total cost $\sum_k p_k (c^t_k)^\top x^t_k$ over this feasible region — problem (3.4.1) in the source.

The nested L-shaped method solves (3.4.1) by decomposition rather than forming this (typically enormous) single LP directly. Each scenario $k$ owns a small subproblem, $\mathrm{NLDS}(t,k)$, that looks exactly like a two-stage L-shaped subproblem: it has $k$'s own constraint and bound, plus a running set of feasibility cuts and optimality cuts accumulated so far, plus, if $k$ has descendants, an approximation variable $\theta^t_k$ standing in for the (unknown, convex, piecewise-linear) future cost $Q^{t+1}_k$ of everything downstream of $k$. Solving $\mathrm{NLDS}(t,k)$ either finds it infeasible — in which case a feasibility cut is derived from the infeasibility certificate and sent up to $k$'s parent — or finds an optimal dual solution, whose aggregate over all of $j$'s children (weighted by conditional probability) becomes a candidate optimality cut for $j = a(k)$. The method sweeps forward and backward across the tree, feasibility and optimality cuts accumulating at every internal node, until no node's subproblem produces a fresh cut.

Formalization targets

Goal (Chapter 6, Theorem 1)

$$\text{if every }\Xi_t\text{ is finite and every }x_t\text{ has a finite upper bound, then the nested L-shaped method}$$ $$\text{converges finitely to an optimal solution of the deterministic equivalent (3.4.1), or correctly certifies its infeasibility.}$$

This is the chapter's only numbered result and the weakest faithful statement of "the method works": it makes no claim about the number of iterations beyond finiteness, and none about which sequencing protocol (forward-forward-back, or any other) is used to choose which subproblem to solve next.

Significance

Finite convergence is what separates an algorithm from a heuristic: without it, nothing rules out an infinite sequence of ever-finer cuts that never certifies optimality or infeasibility. Birge's 1985 result is the reason nested Benders decomposition can be used as an exact method rather than an approximation, and every later refinement (bunching, sifting, multicuts, parallel implementations, all mentioned in the source text) modifies how cuts are generated or which subproblem is solved next without touching this finiteness guarantee — they are all still instances of the same cut-generation mechanism this mission formalizes. The two-stage case (Chapter 5, Theorem 2) is the $H=2$ special case of this theorem; the mission's tree-indexed state and transition relation are written to specialize to the two-stage development directly when the tree has one branching level, though the two developments are not connected by an import (see Formalization scope). No machine-checked proof of either the two-stage or multistage case appears to exist prior to this series; formalizing it here produces the first Lean statement of the mechanism nested Benders decomposition rests on.

Difficulty

The obvious first idea — prove finiteness by bounding the total number of cuts a node can ever receive, the way a flat scenario set bounds the two-stage method's cut count by its number of LP bases — fails because a node's own subproblem is not a fixed-size LP: every cut recorded at node $k$ becomes a new row of $k$'s own constraint set, so the "number of possible bases" at $k$ keeps changing as the algorithm runs, and the bound at $k$ depends recursively on how many cuts $k$'s own children could ever produce. The book's actual argument (p. 290) is a genuine induction on the stage index, from the last stage backward: assume the bound holds for every node at stage $t+1$, then combinatorially bound the finite number of extended bases at stage $t$ that this permits, then take the finite union over every possible extension size. This mission's Lean development commits to a scope that keeps a node's basis a fixed-size object (see below) rather than re-deriving that combinatorial bound.

Formalization scope

Every stage shares one decision dimension $n$ and one constraint dimension $m$ (Fin n, Fin m); the book allows these to vary by stage but nothing in Theorem 1's statement needs that generality. Scenario probabilities p are the unconditional probability of reaching a node, required strictly positive and summing to $1$ within each stage (Instance.hp_pos, Instance.hp_sum); the aggregation formulas use only the ratio $p_k/p_j$ for $k$ a child of $j$, which reads the same whether p is unconditional or conditional, so this is a normalization choice, not a substantive restriction. The upper bound ub is ℝ-valued rather than extended-real-valued, which is Theorem 1's own hypothesis ("finite upper bounds"), not an added convention.

The one deliberate scope-narrowing choice, flagged here and in MODERATION_NOTES.md, and strengthened in this revision after moderator review (2026-09-19, CHANGES_REQUESTED.md #2): a node $k$'s dual witness (Basis, FeasBasis) is read off $k$'s original constraint (1.2) alone — the fixed-size recourse matrix $W^{\mathrm{stage}(k)}$ — never off the extended constraint set (1.2)-(1.4). The gap this leaves is broader than "accumulated cuts are ignored": $k$'s own continuation variable $\theta_k$ — present in (1.1)'s objective, and fixed to $0$ from Step 0 onward, not merely absent until cuts accumulate — has no representation at all in Basis, multiplier, basisValue, or the optimality-cut coefficients optCutCoeffs computes for a parent $j$ of $k$. Consequently, whenever a child $k$ used in an optimality cut is itself an interior node ($k$ has children of its own, i.e. $\mathrm{stage}(k) < H-1$, which happens for every $H \geq 3$ tree), the mechanized cut coefficients are not the book's $(E^{t-1}_j, e^{t-1}_j)$ of Eq. (1.1) and are not the printed algorithm's mechanism at that node — they are the dual of $k$'s plain sub-LP alone, omitting $k$'s own contribution to the recourse value entirely, not only the portion contributed by $k$'s accumulated cuts. This gap is inert exactly when every child aggregated in a cut is a last-stage node ($H \le 2$, where the mechanism coincides with the already-published two-stage sibling 05-two-stage-methods) and active for every deeper cut, which is most of what a general Tree H actually exercises. Concretely: as mechanized, the optimality-cut half of Step (Bases.optCutCoeffs, Step.opt) is faithful to the printed nested L-shaped method's cut-generation step only when every child it aggregates over is a last-stage node; for an interior child it computes a value that omits that child's own $\theta$ term rather than the book's recursive one. The feasibility-cut half (Bases.feasCutCoeffs, Step.feas) has no such gap — feasibility does not involve $\theta$ at any stage — and the tree/instance layer (Tree, Instance) and the goal theorem's own outer shape are unaffected: thm1_finite_convergence's statement (existence of a finite, Step-reachable state that is infeasible-certified or globally optimal) is not weakened, but the reader should treat the mechanized Step relation itself, for H ≥ 3, as a documented variant of Steps 1-2 rather than a literal transcription of them at every node — see STATUS.md's Revision section for the moderator exchange this responds to. Reworking cut generation to consume each child's own current $(x_k, \theta_k)$ witness directly, so that an interior child's continuation value is no longer dropped, is left to a future revision; it is a materially larger change (the child's local optimum is then piecewise-linear rather than linear in its own parent's decision, so the duality argument needs a genuinely different — not merely extended — basis notion) than this session's time budget allows. This keeps every basis type a fixed-size Fin m → Fin n object, exactly as in the two-stage method, and keeps the algorithm's finite-step bound an explicit, provable cardinality (|Node × FeasBasis| + |Node → Basis|) rather than the book's own implicit, recursively-defined one. The trivializing formalization this scope choice must not fall into — declaring victory by proving the plain two-stage case is what convergence "reduces to" without ever quantifying over the tree — is avoided because every definition and the goal statement itself are stated for a general Tree H with unrestricted branching, not merely $H = 2$; what is disclosed above is a gap in how faithfully Step models the book's own cut-generation mechanism at depth, not a restriction of the statement to $H = 2$.

Reusable beyond this mission: Def_StochasticProg_Multistage_Tree (the finite scenario tree) is a natural building block for 07-integer-programs (an integer restriction of the same two-stage subproblem) and 10-multistage-approximations (multistage Jensen bounds, which need the same tree). Contributions welcome: a faithful account of the extended-basis induction sketched above, and a formalization of Chapter 6, Theorem 3 (finite termination of the quadratic nested decomposition of Section 6.2), which this mission omits for time (see STATUS.md).

Selected references

• J.R. Birge, "Decomposition and Partitioning Methods for Multistage Stochastic Linear Programs", Operations Research 33(5), 1985.
• R.M. Van Slyke, R. Wets, "L-Shaped Linear Programs with Applications to Optimal Control and Stochastic Programming", SIAM Journal on Applied Mathematics 17(4), 1969. https://doi.org/10.1137/0117061
• H.I. Gassmann, "MSLiP: A Computer Code for the Multistage Stochastic Linear Programming Problem", Mathematical Programming 47, 1990. https://doi.org/10.1007/BF01580858
• M.V.F. Pereira, L.M.V.G. Pinto, "Stochastic Optimization of a Multireservoir Hydroelectric System: A Decomposition Approach", Water Resources Research 21(6), 1985. https://doi.org/10.1029/WR021i006p00779
• J.R. Birge, F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer Series in Operations Research and Financial Engineering, 2011. https://doi.org/10.1007/978-1-4614-0237-4

Motivation

Interior point methods solve linear programs in a number of arithmetic operations polynomial in the bit length of the input (Karmarkar 1984). Whether linear programming admits a strongly polynomial algorithm, one whose number of arithmetic operations is bounded by a polynomial in the number of variables and constraints alone, is open; it is the ninth of Smale's problems for the next century (Smale 1998/2000, see the references). A natural question is whether some interior point method is strongly polynomial. Primal-dual path-following methods follow the central path of a log-barrier problem and are the methods used in practice.

Allamigeon, Benchimol, Gaubert and Joswig (arXiv:1708.01544, SIAM J. Appl. Algebra Geom. 2018) gave such a family. For linear programs $\mathbf{LW}_r(t)$ with $2r$ variables and $3r+1$ constraints, every path-following method that stays in the wide neighborhood of the central path needs at least $2^{r-1}$ iterations once $t$ is large enough. The same family disproves the "continuous Hirsch conjecture" of Deza, Terlaky and Zinchenko (DTZ09, see the references) on the total curvature of the central path. That curvature result is the subject of a separate mission. This mission formalizes the iteration bound.

Setting

For a real $m\times n$ matrix $A$, $b\in\mathbb R^m$, $c\in\mathbb R^n$ and $N:=n+m$, the paper considers the linear program in slack form and its dual,

$$\mathrm{LP}(A,b,c):\ \min\ \langle c,x\rangle\ \text{ s.t. }\ Ax+w=b,\ (x,w)\ge0,\qquad \mathrm{DualLP}(A,b,c):\ s-A^\top y=c,\ (s,y)\ge0 .$$

A primal-dual point is $z=(x,w,s,y)\in\mathbb R^{2N}$. The set $\mathcal F^\circ$ of strictly feasible points consists of the $z$ with all $2N$ coordinates positive that satisfy both equality systems. The duality measure is

$$\bar\mu(z)=\frac1N\big(\langle x,s\rangle+\langle w,y\rangle\big),$$

and for $0<\theta<1$ the wide neighborhood of the central path is

$$\mathcal N^{-\infty}_\theta=\Big\{z\in\mathcal F^\circ:\ x_js_j\ge(1-\theta)\bar\mu(z)\ \forall j,\ \ w_iy_i\ge(1-\theta)\bar\mu(z)\ \forall i\Big\}.$$

The central path itself is the set of points where all products $x_js_j$, $w_iy_i$ are equal. The neighborhood bounds the products only from below. It contains the $\ell_2$ and $\ell_\infty$ neighborhoods used by short-step, long-step and predictor-corrector methods.

The instance is $\mathbf{LW}_r(t)$, for $r\ge1$ and $t>0$:

$$\min\ x_1\ \text{ s.t. }\ x_1\le t^2,\ x_2\le t,\ x_{2j+1}\le t\,x_{2j-1},\ x_{2j+1}\le t\,x_{2j},\ x_{2j+2}\le t^{1-1/2^j}(x_{2j-1}+x_{2j})\ (1\le j<r),\ x_{2r-1},x_{2r}\ge0 .$$

With slacks $w_1,\dots,w_{3r-1}$ it becomes $\mathbf{LW}^=_r(t)=\mathrm{LP}(A,b,c)$ with $n=2r$, $m=3r-1$, $N=5r-1$. Its wide neighborhood is written $\mathcal N^{-\infty}_{\theta,t}$. A polygonal curve is a union $[z^0,z^1]\cup\dots\cup[z^{p-1},z^p]$ of $p$ segments, and it is contained in the neighborhood when every point of every segment is.

The milestones use the tropical semifield $\mathbb T=\mathbb R\cup\{-\infty\}$ with $a\oplus b=\max(a,b)$ and $a\odot b=a+b$. The tropical segment $\mathsf{tsegm}(u,v)$ is the set of points $\lambda\odot u\oplus\mu\odot v$ with $\lambda\oplus\mu=0$. The Funk metric is $\delta_F(x,y)=\max(0,\max_k(y_k-x_k))$, with $d_\infty(x,y)=\max(\delta_F(x,y),\delta_F(y,x))$ and the directed Hausdorff distance $d_\infty(X,Y)=\sup_{x\in X}\inf_{y\in Y}d_\infty(x,y)$. Finally, $\log_t$ is applied coordinatewise, with $\log_t0=-\infty$.

Formalization targets

Goal: Theorem 30 (p. 27)

Let $r\ge1$ and $0<\theta<1$, and suppose that

$$t>\Big(\max\Big((10r-2)!,\ \frac{((10r-1)!)^{24}}{(1-\theta)^3}\Big)\Big)^{2^{r-1}} .\tag{36}$$

If a polygonal curve $[z^0,z^1]\cup\dots\cup[z^{p-1},z^p]$ is contained in $\mathcal N^{-\infty}_{\theta,t}$ with $\bar\mu(z^0)\le1$ and $\bar\mu(z^p)\ge t^2$, then

$$p\ge2^{r-1}.$$

The threshold (36) is the paper's own explicit constant. Corollary 31 (Theorem B of the introduction) restates the result for algorithms. Any method whose iterates and the segments joining them stay in the wide neighborhood performs at least $2^{r-1}$ iterations to reduce the duality measure from $t^2$ to $1$.

Milestones

1. Proposition 1 (p. 5). On the primal-dual feasible set, $\bar\mu((1-\alpha)z+\alpha z')=(1-\alpha)\bar\mu(z)+\alpha\bar\mu(z')$ for all $\alpha\in\mathbb R$.
2. Lemma 5 (p. 10). For $u\le v$ in $\mathbb T^d$, $\mathsf{tsegm}(u,v)$ is a polygonal curve whose segments, oriented from $u$ to $v$, have directions $e^{K_1},\dots,e^{K_\ell}$ with $K_1\subsetneq\dots\subsetneq K_\ell$ and $\ell\le d$.
3. Lemma 8 (p. 11). For a segment $S=[u,v]$ in $\mathbb R^d_+$ and $t>1$,

$$d_\infty\big(\mathsf{tsegm}(\log_tu,\log_tv),\ \log_tS\big)\le\log_t2 .$$

4. Lemma 11 (p. 13). For a $d\times d$ matrix $\mathbf M$ with monomial entries $\pm t^{\alpha_{ij}}$ and $t>1$, $\log_t|\det\mathbf M(t)|$ and $\operatorname{val}(\det\mathbf M)$ differ by at most $\log_td!$; the lower bound holds once $t\ge(d!)^{1/\eta(\mathbf M)}$.
5. Proposition 20 (p. 19). The explicit recursion for $x^\lambda$ gives the greatest point of the tropical polyhedron $\{x\in\mathcal P':x_1\le\lambda\}$, where $\mathcal P'\subseteq\mathbb T^{2r}$ is cut out by the tropicalized constraints (26) of $\mathbf{LW}_r$.

Significance

The theorem shows that the iteration count of a large class of primal-dual log-barrier interior point methods cannot be bounded by any function of $r$ that grows more slowly than $2^{r-1}$, uniformly in the data. The class includes the methods of Kojima–Mizuno–Yoshise, Monteiro–Adler and Mizuno–Todd–Ye. No such method is strongly polynomial. The constraint matrix of $\mathbf{LW}_r(t)$ is fixed by $r$ and $t$ alone, so the bound concerns the combinatorial dimension, not the bit length. The only property of the method used is that its trajectory stays in $\mathcal N^{-\infty}_{\theta,t}$. The lower bound therefore applies to every method with that property, whatever rule chooses its steps.

The result is proved in the paper; no machine-checked proof of it or of its tropical ingredients is known. A formalization would check the explicit threshold (36), which the paper derives in a few lines from bounds on Puiseux polyhedra. It would also produce reusable statements about tropical segments, the Funk and Hilbert metrics on $\mathbb T^d$, and determinants of monomial matrices.

Difficulty

Following the central path is not hard in principle: the obvious argument tracks the duality measure, which decreases by a constant factor per iteration in a neighborhood of the path. That argument gives only upper bounds. The lower bound requires showing that the neighborhood itself, for large $t$, is too thin to be crossed in a few straight steps, uniformly over every possible trajectory. The paper does this by passing to the limit $t\to\infty$ on logarithmic scale. The image of $\mathcal N^{-\infty}_{\theta,t}$ under $\log_t$ collapses onto a piecewise-linear tropical central path, and a segment of $\mathbb R^{2N}$ becomes, up to $\log_t2$, a tropical segment. The tropical central path of $\mathbf{LW}_r$ then has to be shown to need $2^{r-1}$ tropical segments. The limit argument has to be made quantitative at a finite, explicit $t$. That is where the Puiseux-series machinery (Theorems 12, 15 and 19 of the paper) and the explicit constant enter.

Formalization scope

Everything is stated over $\mathbb R$ and $\mathbb T$; the goal typechecks without the field of Puiseux series. A primal-dual point is an element of $\mathbb R^n\times\mathbb R^m\times\mathbb R^n\times\mathbb R^m$. The dual equation is $s-A^\top y=c$ with Mathlib's transpose, $\bar\mu$ divides by $N=n+m$ (equal to $5r-1$ for $\mathbf{LW}^=_r$), and the wide neighborhood is one-sided. The instance matrix is generated from the paper's 1-based row and column numbers; Lean indices are 0-based. A polygonal curve is a map $z:\{0,\dots,p\}\to\mathbb R^{2N}$ with segment ℝ (z i) (z (i+1)) ⊆ N. The power $2^{r-1}$ in (36) is a natural-number power and the factorials are natural-number factorials. $\mathbb T$ is WithBot ℝ, and distances that can be infinite take values in EReal, with the convention $-\infty+(+\infty)=-\infty$ encoded explicitly.

Two statements are repaired or restated. Lemma 11 is printed for all $t>0$, but its first inequality fails for $0<t<1$ (for $\mathbf M=\begin{pmatrix}t&1\\1&1\end{pmatrix}$ at $t=1/2$), so it is stated for $t>1$. Lemma 8 makes explicit its implicit hypotheses $t>1$ and $u,v\ge0$. Proposition 20 is stated in the form its proof establishes, as the greatest point of a tropical polyhedron. Its identification with the valuation of the Puiseux central path is not part of the item. Monomial matrices are given by sign and exponent matrices, and the valuation of the determinant is computed from the permutation expansion.

A trivializing formalization is ruled out: $\mathcal N^{-\infty}_{\theta,t}$ is not empty, since the build includes a sorry-free proof that it contains an explicit point for $r=1$, $t=2$, $\theta=1/2$. A curve with $p=0$ cannot satisfy both duality-measure conditions, since $t^2>1$.

The paper's Puiseux-series results are not posed: Theorems 12, 15, 19 and 29, Propositions 14, 16, 21 and 28, Corollary 17, and the count $\gamma([0,2])\ge2^{r-1}$ of §6.2. They need a faithful model of the field of absolutely convergent generalized Puiseux series and of the tropical central path. Contributions of that infrastructure, and of these statements as further milestones, are welcome. So are proofs of the five milestones, which need no Puiseux series. Proposition 1, Lemma 5 and Proposition 20 are elementary, and Lemma 8 and Lemma 11 are estimates with explicit constants.

Selected references

• X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Log-barrier interior point methods are not strongly polynomial, SIAM J. Appl. Algebra Geom. 2(1), 2018; arXiv:1708.01544v2. https://arxiv.org/abs/1708.01544
• A. Deza, T. Terlaky, Y. Zinchenko, Central path curvature and iteration-complexity for redundant Klee–Minty cubes, in Advances in Applied Mathematics and Global Optimization, Adv. Mech. Math. 17, Springer, 2009, pp. 223–256. https://doi.org/10.1007/978-0-387-75714-8
• S. Smale, Mathematical problems for the next century, Math. Intelligencer 20(2), 1998, 7–15; reprinted in Mathematics: Frontiers and Perspectives, AMS, 2000. https://doi.org/10.1007/BF03025291
• M. Develin, B. Sturmfels, Tropical convexity, Doc. Math. 9, 2004. https://arxiv.org/abs/math/0308254
• S. J. Wright, Primal-Dual Interior-Point Methods, SIAM, 1997. https://doi.org/10.1137/1.9781611971453
• X. Allamigeon, S. Gaubert, M. Skomra, Tropical spectrahedra, Discrete Comput. Geom. 63, 2020; arXiv:1610.06746. https://arxiv.org/abs/1610.06746

Motivation

Two-stage adaptive optimization models decisions taken in two steps: a first-stage decision $x$ is fixed before an uncertain right-hand side $b$ is revealed, and a second-stage decision $y(b)$ is chosen afterwards, with the worst case over an uncertainty set $\mathcal U$ to be minimized. Problems of this form arise in capacity planning, network design and inventory control, where the first stage is an investment and the second stage a recourse. Computing the fully adaptable optimum is hard in general, so tractable restrictions are used in practice, most prominently affine policies $y(b)=Pb+q$ (Ben-Tal, Goryashko, Guslitzer, Nemirovski, Math. Program. 2004).

Bertsimas and Goyal (Math. Program. Ser. A, DOI 10.1007/s10107-011-0444-4) characterize how well affine policies perform. Their Section 5 shows a factor $O(\sqrt m)$ when the first-stage matrix satisfies $A\ge 0$. Section 6, the subject of this mission, drops the sign condition on $A$: it constructs, from $\mathcal U$, a polytope $\mathcal U^0$ with at most $m+1$ vertices that dominates $\mathcal U$, and shows that an optimal first stage for $\mathcal U^0$ is a $4\sqrt m$-approximate first stage for the original problem.

Timeline. Ben-Tal et al. (2004) introduced affinely adjustable robust counterparts. Bertsimas, Iancu and Parrilo (Math. Oper. Res. 2010) proved optimality of affine policies for one-dimensional multistage problems. Bertsimas and Goyal (Math. Oper. Res. 2010) analysed static robust solutions for two-stage problems. The present paper (received 2009, published 2011) gives the $\Theta(m^{1/2})$ picture for affine policies and the general-case first-stage approximation formalized here.

Setting

Fix matrices $A\in\mathbb R^{m\times n_1}$, $B\in\mathbb R^{m\times n_2}$ and cost vectors $c\in\mathbb R^{n_1}_+$, $d\in\mathbb R^{n_2}_+$. The uncertainty set $\mathcal U\subseteq\mathbb R^m_+$ is convex, compact and full-dimensional. A feasible solution of $\Pi_{Adapt}(\mathcal U)$ is a pair $(x,y)$ with $x\ge0$ and, for every $b\in\mathcal U$, $y(b)\ge0$ and $Ax+By(b)\ge b$, componentwise. Its worst-case cost is $\sup_{b\in\mathcal U}\, c^Tx+d^Ty(b)$, and the fully adaptable optimum is

$$z_{Adapt}(\mathcal U)=\inf_{(x,y)\ \text{feasible}}\ \sup_{b\in\mathcal U}\ c^Tx+d^Ty(b).$$

An optimal solution attains this value.

For $j=1,\dots,m$ let $\mu_j=\max\{b_j: b\in\mathcal U\}$ and let $\beta^j\in\mathcal U$ be a maximizer, $\beta^j_j=\mu_j$ (display (38)). Algorithm $\mathcal A$ (Fig. 1 of the paper) starts with the index set $J_1=\{1,\dots,m\}$; while some $b\in\mathcal U$ has $\sum_{j\in J_1}b_j/\mu_j>\sqrt m$, it picks a maximizer $u^k$ of that scaled sum over $\mathcal U$, adds $u^k$ to a running total on the coordinates of $J_1$, and removes from $J_1$ every coordinate whose total has reached $\mu_j$. It stops after $K$ iterations and returns $\beta=u^1+\dots+u^K$. The dominating set is

$$\mathcal U^0=\operatorname{conv}\{2\sqrt m\cdot\beta^1,\dots,2\sqrt m\cdot\beta^m,\ 2\beta\}.\tag{66}$$

Formalization targets

Goal: Theorem 6

For every run of Algorithm $\mathcal A$, every choice of the maximizers $\beta^j$, and every optimal solution $(\tilde x,\tilde y)$ of $\Pi_{Adapt}(\mathcal U^0)$,

$$\forall b\in\mathcal U\ \ \exists y\ge 0:\quad A\tilde x+By\ge b,\qquad c^T\tilde x+d^Ty\le 4\sqrt m\cdot z_{Adapt}(\mathcal U).$$

The page states the factor as $O(\sqrt m)$; $4\sqrt m$ is the constant its proof establishes.

Milestones

1. Lemma 12. $\mathcal U^0$ dominates $\mathcal U$: every $b\in\mathcal U$ has some $b'\in\mathcal U^0$ with $b\le b'$.
2. Lemma 13 (inequality). $\Pi_{Adapt}(\mathcal U^0)$ is feasible with finite worst-case cost, and

$$z_{Adapt}(\mathcal U^0)\le 4\sqrt m\cdot z_{Adapt}(\mathcal U).$$

3. The domination claim in the proof of Theorem 6. If $V$ dominates $W$ and $(\tilde x,\tilde y)$ is optimal for $\Pi_{Adapt}(V)$ with finite worst-case cost, then every $b\in W$ can be served from $\tilde x$ at cost at most $z_{Adapt}(V)$.

Significance

The result gives a first-stage decision with a guarantee of order $\sqrt m$ for two-stage problems with an arbitrary first-stage matrix, a setting where the affine-policy analysis of Section 5 does not apply. The decision is obtained from a problem whose uncertainty set has at most $m+1$ extreme points, so it reduces an adaptive problem over a general convex set to one over a polytope with few vertices. Together with the paper's lower bounds (Theorems 2 and 3, $\Omega(m^{1/2-\delta})$ for affine policies), it places the general-case approximability of the first stage at the same order as the affine-policy gap.

The result is proved in the paper. It has no machine-checked proof that we know of. The formalization produces, beyond the theorem itself, an encoding of model (1) with values that are honest infima, a relational encoding of Algorithm $\mathcal A$ usable for its termination and output properties, and a reusable domination lemma for two-stage problems. Mission IV of this series (the case $A\ge0$) formalizes Lemmas 9 and 10 on Algorithm $\mathcal A$, which the proofs here use.

Difficulty

The obvious argument replaces $\mathcal U$ by a simple set that contains or dominates it, such as the box $\prod_j[0,\mu_j]$, and solves over that set. This loses a factor $m$, not $\sqrt m$: for $\mathcal U=\operatorname{conv}\{0,e_1,\dots,e_m\}$ with $A=0$, $B=I$, $c=0$, $d=e$, the optimum over $\mathcal U$ is $1$ while the optimum over the box is $m$. A dominating set with few vertices whose cost is only $O(\sqrt m)$ times the original optimum has to be built from $\mathcal U$ itself, and controlling the cost of its vertex $2\beta$ depends on the number $K$ of iterations of Algorithm $\mathcal A$, which is bounded only through the potential argument of Lemma 10 in the paper.

A second difficulty is that $z_{Adapt}$ is an infimum, not an attained minimum, over second-stage rules that are arbitrary functions; the cost comparison must work from near-optimal solutions of $\Pi_{Adapt}(\mathcal U)$.

Formalization scope

Vectors are functions on Fin m, matrices are Matrix (Fin m) (Fin n) ℝ, and inequalities between vectors are componentwise. The paper's coordinate $j$ is Fin index $j-1$. $z_{Adapt}(\mathcal U)$ is the infimum of the set of bounds $t$ such that some feasible $(x,y)$ satisfies $c^Tx+d^Ty(b)\le t$ for all $b\in\mathcal U$; this avoids a real supremum of a possibly unbounded worst case. An optimal solution is a feasible one that achieves every achievable bound. $\mu$ and the maximizers $\beta^j$ enter the theorems as data with their defining properties. Algorithm $\mathcal A$ is a relation on a choice sequence $u^1,u^2,\dots$: the theorems hold for every run and every choice of maximizers, never for "some simplex dominating $\mathcal U$".

Standing assumptions of (1) carried by the goal and Lemma 13: $c\ge0$, $d\ge0$, $\mathcal U\subseteq\mathbb R^m_+$ convex, compact and with nonempty interior, and (1) feasible. There is no sign condition on $A$. Lemma 12 keeps only nonnegativity and full-dimensionality of $\mathcal U$; the domination claim is stated for arbitrary scenario sets $V$ and $W$ with $V$ dominating $W$ and assumes that the optimal solution over $V$ has a finite worst-case cost.

The printed Lemma 13 also asserts $z_{Aff}(\mathcal U^0)=z_{Adapt}(\mathcal U^0)$ on the grounds that $\mathcal U^0$ is a simplex. Its $m+1$ generators need not be affinely independent, so this equality is not part of the mission; Theorem 6 does not use it.

A bound on $z_{Adapt}(\mathcal U^0)$ alone is not the goal: the goal requires, for each scenario of the original set $\mathcal U$, a feasible second stage completing the fixed first stage $\tilde x$ at the stated cost. Lemma 13 also asserts feasibility over $\mathcal U^0$ with a finite bound, so its inequality cannot hold through the value of an infimum over an empty set.

A complete development needs elementary facts about convex hulls of finitely many points (representation by convex weights), the properties of Algorithm $\mathcal A$ (its output bound and termination, Lemmas 9 and 10 of the paper), and $\varepsilon$-approximation arguments for infima. The encoding of model (1) and of Algorithm $\mathcal A$ is shared with the other missions of this series. Contributions of these supporting lemmas are welcome.

Selected references

• D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Math. Program. Ser. A, 2011. https://doi.org/10.1007/s10107-011-0444-4
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Math. Program. 99, 2004. https://doi.org/10.1007/s10107-003-0454-y
• D. Bertsimas, D. A. Iancu, P. A. Parrilo, Optimality of affine policies in multistage robust optimization, Math. Oper. Res. 35, 2010. https://doi.org/10.1287/moor.1100.0444
• D. Bertsimas, V. Goyal, On the power of robust solutions in two-stage stochastic and adaptive optimization problems, Math. Oper. Res. 35, 2010. https://doi.org/10.1287/moor.1090.0440

Motivation

Two-stage adaptive optimization models decisions taken in two steps: a first-stage decision $x$ is fixed before an uncertain right-hand side $b$ is revealed, and a second-stage recourse $y(b)$ is chosen afterwards, with the worst case over an uncertainty set $\mathcal U$ to be minimized. The fully-adaptable problem, in which $y$ may be an arbitrary function of $b$, is intractable in general. The standard tractable restriction, introduced by Ben-Tal, Goryashko, Guslitzer and Nemirovski (2004), requires $y$ to be an affine policy $y(b)=Pb+q$; it turns the problem into a single convex program and is used throughout robust inventory, network design and energy planning.

How much is lost by this restriction? Bertsimas and Goyal (Math. Program. 2012) answer the question for problems with a nonnegative constraint matrix. On one side, affine policies are optimal when $\mathcal U$ is a simplex, and are within a factor $O(\sqrt m)$ of the optimum on every instance of the class, where $m$ is the number of constraints. On the other side, the bound is nearly tight: Section 4 of the paper constructs an instance on which the best affine policy costs $\Omega(m^{1/2-\delta})$ times the fully-adaptable optimum, for any $\delta>0$. This mission formalizes that lower bound.

Timeline: Ben-Tal et al. (2004) propose affinely adjustable robust counterparts; Bertsimas, Iancu and Parrilo (2010) prove optimality of affine policies for one-dimensional multistage problems; Bertsimas and Goyal (2012) give the $O(\sqrt m)$ upper bound and the matching lower-bound example formalized here.

Setting

The two-stage problem $\Pi_{\mathrm{Adapt}}(\mathcal U)$ has data $A\in\mathbb R^{m\times n_1}$, $B\in\mathbb R^{m\times n_2}$, $c\in\mathbb R^{n_1}_+$, $d\in\mathbb R^{n_2}_+$ and $\mathcal U\subseteq\mathbb R^m_+$:

$$z_{\mathrm{Adapt}}(\mathcal U)=\min_{x,\,y(\cdot)}\ c^\top x+\max_{b\in\mathcal U}d^\top y(b)\quad\text{s.t.}\quad Ax+By(b)\ge b,\ x\ge0,\ y(b)\ge0\ \ \forall b\in\mathcal U .$$

The value $z_{\mathrm{Aff}}(\mathcal U)$ is the same minimum over policies of the form $y(b)=Pb+q$; such a policy must be nonnegative on all of $\mathcal U$.

The large-gap instance $\mathcal I$ of display (19) has $n_1=n_2=m$, a parameter $\delta>0$ with $m^\delta>200$ (condition (18)), and

$$\theta_0=\frac{1}{m^{(1-\delta)/2}},\qquad r=\lceil m^{1-\delta}\rceil,$$ $$c=0,\quad d=e=(1,\dots,1)^\top,\quad A=0,\quad B_{ij}=\begin{cases}1,&i=j,\\ \theta_0,&i\ne j,\end{cases}$$ $$\mathcal U=\operatorname{conv}\Bigl(\{0,\ e_1,\dots,e_m,\ \tfrac{1}{\sqrt m}e\}\cup\{\theta_0\mathbf 1_S:\ |S|=r\}\Bigr),$$

where $e_j$ are the unit vectors and $\mathbf 1_S$ is the indicator vector of a set $S$ of coordinates. A permutation $\sigma$ of the coordinates acts on vectors by $b^\sigma=(b_{\sigma(1)},\dots,b_{\sigma(m)})$ and on matrices by $P^\sigma_{ij}=P_{\sigma(i),\sigma(j)}$.

Formalization targets

Goal: Theorem 3, explicit form

$$z_{\mathrm{Aff}}(\mathcal U)>\frac{m^{1/2-\delta}}{4}\cdot z_{\mathrm{Adapt}}(\mathcal U)\qquad\text{for all }\delta>0\text{ and }m\text{ with }m^\delta>200 .$$

The paper writes $z_{\mathrm{Aff}}(\mathcal U)=\Omega(m^{1/2-\delta})\cdot z_{\mathrm{Adapt}}(\mathcal U)$; the constant $1/4$ is the one the proof establishes, so the explicit statement is the stronger one.

Milestones

1. Lemma 4: $z_{\mathrm{Adapt}}(\mathcal U)\le1$, with a feasible solution attaining cost at most $1$.
2. Lemma 5: $\mathcal U$ is permutation-invariant under every $\sigma\in S^m$.
3. Lemma 6: the permuted instance $\mathcal I(\sigma)$ of (22) equals $\mathcal I$.
4. Lemma 7: if $y(b)=Pb+q$ is an optimal affine solution, so is $y^\sigma(b)=P^\sigma b+q^\sigma$.
5. Lemma 8: some optimal affine solution has $\hat P_{ij}=\mu$ ($i\ne j$), $\hat P_{jj}=\theta$, $\hat q_j=\lambda$.
6. The three Claims of the proof of Theorem 3: for a symmetric feasible affine policy with worst-case cost at most $m^{1/2-\delta}/4$, one has $0\le\lambda\le m^{-1/2-\delta}$, $\theta\ge1/3$, and $-m^{-1-\delta/2}\le\mu<0$.

Significance

The result shows that the $O(\sqrt m)$ approximation guarantee for affine policies on problems with $A\ge0$ (Theorem 4 of the same paper) cannot be improved beyond a factor $m^{\delta}$, so the uncertainty set that looks like a portion of the unit sphere in the nonnegative orthant is essentially the worst case for affine recourse. It also explains why later work moved to piecewise-affine and finitely adaptable policies to close the gap. The example satisfies $c,d\ge0$, $A,B\ge0$ and $\mathcal U\subseteq\mathbb R^m_+$, so the lower bound applies to every larger problem class.

The theorem is proved in the paper; to our knowledge no machine-checked version exists. A formalization adds checked statements of the symmetrization argument (an optimal affine policy may be taken invariant under the symmetry group of the instance), which applies to any symmetric robust linear program, and a checked derivation of the explicit constant.

Difficulty

The upper bound $z_{\mathrm{Adapt}}\le1$ is a direct construction. The difficulty lies in the lower bound on $z_{\mathrm{Aff}}$, which must hold for every affine policy, a family with $m^2+m$ free parameters. Bounding the cost of a policy at a few chosen points of $\mathcal U$ does not suffice without first reducing the parameters, and the reduction requires that an optimal affine solution exists (attainment of the minimum over an unbounded parameter set) and that averaging over the symmetric group preserves both feasibility and optimality. The remaining argument balances three different generators of $\mathcal U$ against each other, and the exponents of $m$ must be tracked exactly through ceilings and real powers.

Formalization scope

Vectors are Fin m → ℝ with the componentwise order and 0-based indices; matrices are Matrix (Fin m) (Fin m) ℝ. The values $z_{\mathrm{Adapt}}$ and $z_{\mathrm{Aff}}$ are infima of the sets of worst-case cost bounds achieved by feasible solutions (epigraph form), so they do not rely on a supremum of a possibly unbounded function. Affine policies must be nonnegative on $\mathcal U$. Optimal solutions are defined as feasible solutions whose worst-case cost is bounded by every achievable bound, so Lemma 8 asserts attainment. Powers $m^{a}$ are real powers; $\theta_0=1/m^{(1-\delta)/2}$ and $r=\lceil m^{1-\delta}\rceil$ exactly as on the page. $\mathcal U$ is the convex hull of its listed generators; the generator count $N$ printed in (19) plays no role.

The parameter $\delta$ is not restricted beyond $\delta>0$ and $m^\delta>200$, as in the paper. Lemma 4's proof on the page uses $\delta\le1$; the statement is kept for all $\delta>0$, where it remains true with a different witness. The Claims are stated for any symmetric feasible affine policy with cost at most $m^{1/2-\delta}/4$; their hypotheses are jointly unsatisfiable by Theorem 3, which is inherent in steps of a proof by contradiction.

A trivializing formalization is excluded: the goal mentions only the instance data and the two optimal values, not the symmetric parameters $\mu,\theta,\lambda$, and the nonemptiness of the feasible sets is established by Lemma 4 and by the existence of a feasible affine policy, so neither value is a junk infimum of an empty set.

A complete development needs: convex hulls of finite point sets in $\mathbb R^m$ and their extreme points; the action of $S^m$ by coordinate permutation; averaging over the finite group $S^m$; and existence of minimizers for linear programs over a polytope. The symmetrization lemmas (5–8) are reusable for other symmetric robust problems. Proofs of any milestone, including partial infrastructure for linear-programming attainment, are welcome.

Selected references

• D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Mathematical Programming Ser. A 134 (2012) 491–531. https://doi.org/10.1007/s10107-011-0444-4
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Mathematical Programming 99 (2004) 351–376. https://doi.org/10.1007/s10107-003-0454-y
• D. Bertsimas, D. A. Iancu, P. A. Parrilo, Optimality of affine policies in multistage robust optimization, Mathematics of Operations Research 35 (2010) 363–394. https://doi.org/10.1287/moor.1100.0444