Optimization

Motivation

The vehicle routing problem with time windows (VRPTW) asks for minimum-cost routes from a central depot that serve every customer exactly once, respecting vehicle capacity and a time interval in which each customer's service must begin. It models school bus routing, parcel and retail distribution, and dial-a-ride services. Desrochers, Desrosiers and Solomon (Oper. Res. 40 (1992) 342–354) gave an optimization algorithm for the VRPTW that solved benchmark instances with up to 100 customers to optimality, a size far beyond earlier exact methods. Their method, which solves the linear relaxation of a set partitioning model by column generation with routes priced out by a resource-constrained shortest path dynamic program, is the template that later exact vehicle routing algorithms ("branch-and-price") follow.

The mathematical core of the method is a certificate: once the pricing subproblem reports that no route has negative marginal cost (reduced cost), the current linear programming solution is optimal over all routes the subproblem can generate, its value bounds every VRPTW solution from below, and an integral solution covering each customer exactly once is VRPTW-optimal. This mission formalizes that certificate and the lemmas of the paper it rests on.

Setting

The nodes are a depot $d$ and customers $N\setminus\{d\}$. An arc set $A$ carries, for each arc $(i,j)$, a cost $c_{ij}$ and a duration $t_{ij}$; each node has a demand $q_i$ and a time window $[a_i,b_i]$; vehicles have capacity $Q$.

A path $(d, i_1, \dots, i_K, d)$ uses arcs of $A$ and passes through the depot only at its ends. It is resource-feasible when there are service start times $T_0 = 0, T_1, \dots, T_{K+1}$ with $T_k + t_{i_k i_{k+1}} \le T_{k+1}$ (waiting is allowed) and $a_{i_k}\le T_k\le b_{i_k}$, and its load $\sum_{k=1}^{K} q_{i_k}$ is at most $Q$. Its cost is $c_r = \sum_{k=0}^{K} c_{i_k i_{k+1}}$, and $\gamma_{ir}$ is the number of visits of $r$ to customer $i$. The paper uses three solution spaces:

1. feasible routes $R$: resource-feasible paths visiting each customer at most once;
2. second-model paths: resource-feasible paths where customers may repeat (the state-space relaxation that tracks load and time but not the set of visited customers);
3. third-model paths: second-model paths with no 2-cycle $(i, j, i)$.

A VRPTW solution is a set of feasible routes covering each customer exactly once; its cost is the sum of the route costs.

The set covering type model (Sec. 4) over a column set $\mathcal R$ is

$$\min \sum_r c_r x_r \quad\text{s.t.}\quad \sum_r \gamma_{ir}x_r \ge 1\ (i \ne d),\quad \sum_r x_r - X_d = 0,\quad \sum_r c_r x_r - X_c = 0,$$

with $x_r\in\{0,1\}$ and $X_d, X_c\ge 0$ integer. Its LP relaxation replaces $x_r\in\{0,1\}$ by $x_r\ge 0$ and drops integrality. For dual values $\pi_i$, $\pi_d$, $\pi_c$ of the three rows, the marginal cost of a column and of an arc are

$$\bar c_r = c_r - \sum_{i\ne d}\pi_i\gamma_{ir} - \pi_d - \pi_c c_r,\qquad \bar c_{ij} = (1-\pi_c)c_{ij} - \pi_i\quad(\pi_i := \pi_d \text{ at } i = d).$$

Formalization targets

Goal: the column generation certificate

Let $R_0$ be a finite set of third-model paths, $\bar z = (\bar x, \bar X_d, \bar X_c)$ an optimal solution of the LP relaxation restricted to $R_0$, and $(\pi,\pi_d,\pi_c)$ an optimal solution of its dual. If every third-model path has nonnegative marginal cost, $\sum_{k=0}^{K}\bar c_{i_k i_{k+1}} \ge 0$, then

$$\bar z \text{ is optimal for the LP relaxation over all third-model paths},$$

and, when arc costs are nonnegative, $\sum_r c_r \bar x_r \le \text{cost}(S)$ for every VRPTW solution $S$; if moreover $\bar x$ is integral and covers each customer exactly once, its support is an optimal VRPTW solution.

Milestones

1. Feasible routes $\subseteq$ third-model paths $\subseteq$ second-model paths (Sec. 3, p. 346).
2. $\bar c_r = \sum_{k=0}^{K}\bar c_{i_k i_{k+1}}$ for every path (Sec. 4.1, p. 347).
3. Nonnegative column marginal costs over all third-model paths make the restricted optimum optimal (Sec. 4, p. 346).
4. Every VRPTW solution is a feasible LP point of equal cost (Sec. 2, p. 344).
5. An integral, exactly covering LP point is a VRPTW solution of equal cost (Sec. 5, p. 348).
6. Under the strict triangle inequality, LP optima over routes do not overcover (Sec. 5, p. 348).
7. The four time window reduction conditions preserve the set of paths (Sec. 6.1, p. 349).
8. The Figure 1 example has 11, 22 and 12 solutions in the three models (pp. 345–346).

Significance

The certificate is the correctness statement of column generation for vehicle routing: it says when the algorithm may stop, what the value it stops with means, and when the branch-and-bound tree can be skipped. The same argument, with a different subproblem, underlies branch-and-price for crew scheduling, cutting stock and many other set partitioning formulations. Milestone 2 is the observation that turns pricing into a shortest path problem on the original network, and milestone 7 is the preprocessing used before every dynamic program over time windows.

The paper's results are classical and their proofs are short in prose. None of them, nor any VRPTW column generation statement, has a machine-checked proof on the platform; the closest existing items concern split deliveries (Desaulniers 2010) or general finite LP duality. The mission produces a reusable formal model of resource-constrained paths, the set covering LP and its restricted dual, on which later branch-and-price papers can build.

Difficulty

The goal combines three ingredients that do not fit together automatically. First, LP duality for the restricted problem: the hypothesis gives an optimal dual, but optimality over all columns needs equality of the restricted primal and dual values, which is strong duality for a finite LP with equality rows and sign-constrained auxiliary variables. Second, the column set of the full LP is infinite in general: a nonelementary path can repeat customers, so the comparison must go through the finitely many columns a given feasible point uses. Third, the pricing hypothesis is about arc sums along node sequences while the LP is about column costs and visit counts; matching them needs the depot to appear exactly at the two ends of a path.

The tempting shortcut of quantifying the pricing hypothesis over the current columns only gives dual feasibility for the restricted LP, which says nothing about columns not yet generated. The lower bound also fails for arbitrary real costs, because row (4) with $X_c \ge 0$ excludes negative-cost solutions from the LP while the VRPTW still contains them.

Formalization scope

Nodes are Fin (n+1) with the depot 0. A path is the list of its customers; its node sequence is 0 :: p ++ [0], so a path visits at least one customer and meets the depot only at its ends. The arc set is an arbitrary relation; costs, durations, demands and windows are arbitrary reals, and every sign or triangle condition a statement needs appears in its own hypotheses. The committed readings:

• service times are indexed by position (a second-model path may visit a node twice), with $T_0 = 0$;
• the depot's window also applies at the return ($0 \le k \le K+1$, where the page prints $0\le k\le K$);
• the capacity constraint is load $\le Q$ (the page says "less than"; the recurrences and Figure 1 use $\le$);
• a 2-cycle is a pattern of the customer list, so $(d, i, d)$ is not one;
• the LP relaxation keeps $X_d, X_c \ge 0$, relaxes $x_r\in\{0,1\}$ to $x_r\ge 0$ with no upper bound, and is the root LP without branching rows; its dual is that of the restricted LP, with $\pi_i, \pi_d, \pi_c \ge 0$;
• LP points are finitely supported functions on lists (Finsupp); VRPTW solutions are Finsets of routes;
• clauses 2–3 of the goal and milestone 4 assume nonnegative arc costs (the paper's costs are distances);
• milestone 6 adds complete arcs, positive costs, a triangle inequality on durations and nonnegative demands; milestone 7 applies the conditions at customers only; milestone 8 lists $(d,2,1,2,1,d)$ where the page prints $(d,2,1,2,d)$ twice.

The goal is not to be trivialized: the pricing hypothesis ranges over all third-model paths, not the current columns; equality of primal and dual values is not assumed; the full column set is not $R_0$; and "covered exactly once" is not presupposed to mean elementary columns, which must be derived from integrality.

Contributions welcome: proofs of the milestones, a reusable finite LP strong duality interface for Finsupp-indexed columns, and lemmas about arc sums over node sequences.

Selected references

• M. Desrochers, J. Desrosiers, M. Solomon, A new optimization algorithm for the vehicle routing problem with time windows, Operations Research 40(2), 1992, 342–354. https://doi.org/10.1287/opre.40.2.342
• N. Christofides, A. Mingozzi, P. Toth, State-space relaxation procedures for the computation of bounds to routing problems, Networks 11(2), 1981, 145–164. https://doi.org/10.1002/net.3230110207
• D. J. Houck, J.-C. Picard, M. Queyranne, R. R. Vemuganti, The travelling salesman problem as a constrained shortest path problem: theory and computational experience, Opsearch 17, 1980, 93–109.
• G. Desaulniers, Branch-and-price-and-cut for the split-delivery vehicle routing problem with time windows, Operations Research 58(1), 2010, 179–192. https://doi.org/10.1287/opre.1090.0713

Motivation

Large scale unconstrained optimization often makes an exact Newton step expensive. At each iterate, Newton's method asks for a solution of a linear system involving the Hessian, and the cost of solving that system can dominate the cost of evaluating the objective. Dembo and Steihaug's 1983 truncated Newton method uses conjugate gradients to stop the linear solve early, either when the residual is small enough or when the current direction has insufficient positive curvature. The resulting direction is paired with a line search. The question for this mission is whether those early exits still give a globally reliable optimization method under the paper's assumptions. The answer, in Theorem 2.1, is that every resulting run has gradient norm tending to zero, and a positive definite Hessian at one limit point makes the whole sequence converge to that point.

Setting

The objective is a twice continuously differentiable function $f:\mathbb R^n\to\mathbb R$. Write $g(x)=\nabla f(x)$ for its gradient and $H(x)=Dg(x)$ for its Hessian. For every initial point $x_0$, the paper assumes that the sublevel set $L(x_0)=\{x:f(x)\le f(x_0)\}$ is bounded. The formalization uses the Euclidean norm and its inner product, so the operator norm of $H$ is also Euclidean.

At a major iterate $x_k$, the minor conjugate-gradient iteration starts at $p_0=0$ with residual and direction $r_0=d_0=-g(x_k)$. It maintains a scalar $\delta_i$, initialized to $\|r_0\|^2$, alongside the usual conjugate-gradient state. Before taking its next conjugate-gradient step, it checks whether $\langle d_i,H(x_k)d_i\rangle\le\varepsilon\delta_i$. If so, it returns $d_0=-g(x_k)$ when $i=0$ and the current approximation $p_i$ otherwise. If this first test fails, it takes a conjugate-gradient step and checks whether $\|r_{i+1}\|\le\eta_k\|g(x_k)\|$. If so, it returns $p_{i+1}$. A TNCG direction is the direction returned by the first exit that occurs. The forcing value $\eta_k$ sets the residual tolerance.

The major iteration chooses a positive step length $\lambda_k$. With $p_k$ the minor iteration's output and $0<\alpha<1/2$, $\alpha<\beta<1$, the line search requires both sufficient decrease and a curvature condition:

$$f(x_k+\lambda_k p_k)\le f(x_k)+\alpha\lambda_k\langle g(x_k),p_k\rangle, \qquad \langle g(x_k+\lambda_kp_k),p_k\rangle\ge\beta\langle g(x_k),p_k\rangle.$$

The update is $x_{k+1}=x_k+\lambda_kp_k$. A run is a sequence satisfying this rule from its specified starting point. The paper also states an alternative function-value curvature condition; this mission defines it because the local unit-step theorem discusses both choices, although the main run uses the displayed gradient condition.

Formalization targets

Global convergence

For every starting point there is a TNCG run, and every run satisfies

$$\|g(x_k)\|\longrightarrow0.$$

If $x^*$ is a limit point of that run and $H(x^*)$ is positive definite, then

$$x_k\longrightarrow x^*.$$

The existence clause is the formal meaning of the paper's assertion that the iterates are well defined. The six milestones follow the paper's appendix: the conjugate-gradient relations of Theorem A.1; the uniform descent and direction bounds of Lemma A.2; the line-search existence and directional-derivative limit used in the proof of Theorem A.3; Theorem A.3 itself; and eventual unit-step admissibility in Theorem A.4. The companion Theorem 2.2 addresses the eventual residual exit and unit-step behavior when a run converges to a point with positive definite Hessian. These results are all stated in the original paper.

Significance

The target shows that the computational shortcut in the inner linear solve preserves a global first-order guarantee: no TNCG run can maintain a gradient norm bounded away from zero. It also identifies when the sequence has one limit, rather than merely having stationary accumulation points. The local companion result describes the regime where the truncated method can take full steps and the residual stopping test governs the minor iteration.

The mathematical results are proved in the 1983 paper, while this mission's Lean statements are open proof targets. A complete formalization would connect the finite-dimensional conjugate-gradient recurrence, the line-search argument on bounded sublevel sets, and the convergence statement in one machine-checked development. The conjugate-gradient identities and line-search facts could be reused in other optimization algorithms; the exact first-exit model and the global conclusion are specific to this method.

Difficulty

The minor iteration is not an ordinary positive definite conjugate-gradient solve. The Hessian may be indefinite away from a solution, and the iteration must stop at insufficient curvature before using a later residual state. A convergence argument that assumes positive definiteness at every iterate would therefore miss the case the algorithm was designed to handle. The line search must work for the returned direction, including the first iteration's steepest-descent fallback. The limit-point conclusion adds a separate issue: a vanishing gradient norm alone does not force an entire sequence to converge to a chosen limit point.

Formalization scope

Lean represents $\mathbb R^n$ as EuclideanSpace ℝ (Fin n), uses its Euclidean norm and inner product, and defines $H(x)$ as the derivative of the gradient. The objective is $C^2$ and every sublevel set is bounded, as specified at the start of the paper. The TNCG recurrence is total, but an admissible direction must come from its first actual exit, with the curvature test preceding the residual test. At $i=0$, the curvature exit returns $-g$, not the zero initial approximation. This prevents a false stationary run. The residual test is written as a product inequality, equivalent to the paper's quotient when the residual test is reached.

Step lengths are positive. A run is extended through stationary points by zero directions, giving an infinite sequence on which a limit can be stated. Theorem 2.1 imposes no extra restriction on the forcing sequence and no upper bound on step lengths. Theorem A.1 corrects the printed Krylov-space index from $H^{k-1}g$ to $H^kg$. Theorem A.4 adds $g(x^*)=0$, needed for the conclusion and true in the paper's applications. Theorem 2.2 requires nonnegative forcing values and guards its residual-exit conclusion at stationary iterates. These corrections are recorded item by item in the moderation notes. Contributions to the conjugate-gradient identities, bounded-level-set line search, and isolated-limit-point argument are all within scope.

Selected references

• R. S. Dembo and T. Steihaug, Truncated-Newton algorithms for large-scale unconstrained optimization, Mathematical Programming 26 (1983), 190–212. DOI: 10.1007/BF02592055.

Motivation

Truncated-Newton methods minimize a smooth function $f:\mathbb{R}^n\to\mathbb{R}$ by taking, at each iterate $x_k$, a search direction obtained by solving the Newton equation $H(x_k)p=-g(x_k)$ only approximately, with the linear conjugate gradient (CG) method. Here $g$ is the gradient and $H$ the Hessian of $f$. The approach was analysed by Dembo and Steihaug (Math. Programming 26, 1983), building on the inexact Newton framework of Dembo, Eisenstat and Steihaug (SIAM J. Numer. Anal. 19, 1982), and Newton–CG with curvature tests remains a standard large-scale method (Nocedal and Wright, Numerical Optimization, Ch. 7).

Away from a minimizer the Hessian need not be positive definite, and CG on an indefinite system can produce directions along which $f$ curves downward. The Dembo–Steihaug method stops CG when it meets such a direction. A practical question follows: started at or near a stationary point that is not a local minimizer, will the method ever notice the nonpositive curvature? Theorem 2.4 of the paper answers it for exact CG: it does, except in a degenerate case described by the eigenspaces of $H$.

Setting

Fix a symmetric linear operator $H$ on $\mathbb{R}^n$, with the Euclidean inner product $u^{\mathsf T}v$ and norm $\|\cdot\|$, and a vector $g\in\mathbb{R}^n$. In the paper these are $H(x_k)$ and $g(x_k)$ at the current iterate.

The TNCG minor iteration (p. 194) runs CG on $Hp=-g$ from $p_0=0$. Its state at iteration $i$ is $(p_i,r_i,d_i,\delta_i)$:

$$p_0=0,\quad r_0=-g,\quad d_0=r_0,\quad \delta_0=r_0^{\mathsf T}r_0,$$

and, writing $q_i=Hd_i$,

$$\alpha_i=\frac{r_i^{\mathsf T}r_i}{d_i^{\mathsf T}q_i},\ \ p_{i+1}=p_i+\alpha_id_i,\ \ r_{i+1}=r_i-\alpha_iq_i,\ \ \beta_i=\frac{r_{i+1}^{\mathsf T}r_{i+1}}{r_i^{\mathsf T}r_i},\ \ d_{i+1}=r_{i+1}+\beta_id_i,\ \ \delta_{i+1}=r_{i+1}^{\mathsf T}r_{i+1}+\beta_i^2\delta_i .$$

At iteration $i$ the method first applies the curvature test (2.1), $d_i^{\mathsf T}Hd_i\le\varepsilon\,\delta_i$, and stops if it holds; otherwise it computes $r_{i+1}$ and applies the truncation test (2.2), $\|r_{i+1}\|/\|g\|\le\eta$, and stops if it holds. With $\varepsilon=\eta=0$, (2.1) reads $d_i^{\mathsf T}Hd_i\le0$ and (2.2) reads $r_{i+1}=0$. The method exits through (2.1) at $i$ when no test fired at any iteration $j<i$ and (2.1) holds at $i$.

For $\mu\in\mathbb{R}$ the eigenspace is $E(\mu,H)=\{v: Hv=\mu v\}$ (A.21). The span of vectors $v_1,\dots,v_m$ is written $[v_1,\dots,v_m]$; the Krylov space of $g$ is $[g,Hg,\dots,H^{m}g]$.

Formalization targets

Goal: Theorem 2.4 (p. 197)

Let $\eta_k=\varepsilon=0$. If $H$ is not positive definite, then either the minor iteration exits through (2.1) at some iteration $i$, so that

$$d_i^{\mathsf T}Hd_i\le 0 \quad\text{at an iteration } i \text{ the method reaches},$$

or

$$g^{\mathsf T}v=0\quad\text{for every } v \text{ with } Hv=\mu v,\ \mu\le0 .$$

Milestones

1. Theorem A.1, (A.2) and (A.5), at $\varepsilon=0$ (p. 206). If $d_i^{\mathsf T}Hd_i>0$ for $i=0,\dots,k$, then $d_i^{\mathsf T}Hd_j=0$ for $i\ne j\le k$, and $[d_0,\dots,d_k]=[g,Hg,\dots,H^kg]$.
2. Theorem A.5 (p. 210). If $g$ has a nonzero projection on each eigenspace of $H$, $k$ is the number of distinct eigenvalues, and vectors $d_0,\dots,d_{k-1}$ are $H$-conjugate with $(d_i,Hd_i)>0$ and span $[g,\dots,H^{k-1}g]$, then $H$ is positive definite.
3. The first sentence of the proof of Theorem 2.4 (p. 211). If $g$ is not orthogonal to any eigenspace of $H$, and exact CG passes the curvature test up to iteration $i$ and ends with $r_{i+1}=0$, then $H$ is positive definite.

Significance

The theorem is the theoretical justification, given in the paper on p. 197, for using the direction of negative curvature $d_i$ produced in case (ii) of the minor iteration: with exact arithmetic and no truncation, CG either produces a direction of nonpositive curvature or the gradient lies entirely in the span of eigenvectors with positive eigenvalues. The paper draws the consequence that if $x_k\to x^*$ and the method terminates through (2.2), then, outside this rare case, $x^*$ is a strong local minimizer. Theorem A.5 is a self-contained statement about conjugate families in Krylov spaces, usable in any analysis of CG on indefinite systems.

The result is proved in the paper (Appendix, pp. 206–211), with the CG relations of Theorem A.1 cited from Hestenes and Stiefel. No machine-checked proof of these statements is known to this mission. Formalizing them produces a Lean development of CG on a symmetric, possibly indefinite operator, with its conjugacy and Krylov-span relations, which classical treatments state only for positive definite systems.

Difficulty

The CG relations of Theorem A.1 are usually proved for positive definite $H$, where every denominator is positive. Here $H$ is indefinite, and the relations hold only as long as the curvature along the directions has stayed positive; the induction must carry that hypothesis and must also show the residuals do not vanish early. The passage from "CG ended with $r=0$" to a statement about all eigenspaces is the second obstacle: the CG run sees only the Krylov space of $g$, so one must relate that space to the eigenspaces that $g$ meets, using symmetry of $H$ and a count of distinct eigenvalues. A direct argument via "the directions span $\mathbb{R}^n$" fails, because when $g$ misses an eigenspace the Krylov space is a proper subspace.

Formalization scope

$\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n); $H$ is a continuous linear map that is self-adjoint (IsSelfAdjoint H), as the paper's $H$ is a Hessian. Positive definiteness is $v^{\mathsf T}Hv>0$ for all $v\ne0$. The CG recursion is total and carries no stopping test; division by zero returns $0$ in Lean, so states after a would-be stop are junk, and the statements read the iteration only through first-exit predicates. The test (2.2) is encoded in the product form $\|r_{i+1}\|\le\eta\|g\|$.

Theorem 2.4 is stated for an arbitrary symmetric $H$ and vector $g$ rather than at an iterate of a run of the full algorithm. It uses nothing else about $f$ or the run, and every such pair occurs as the Hessian and gradient of an admissible objective. The paper's (A.5) prints $H^{k-1}g$ as the last Krylov vector; the correct $H^kg$ is used.

A trivializing formalization exists and is ruled out: the first alternative is not "$d_i^{\mathsf T}Hd_i\le0$ for some $i$" over the unstopped recursion, which holds automatically once a residual vanishes (the recursion then continues with $d=0$); it requires that iteration $i$ is reached with no earlier exit. The goal does not assume conjugacy, the Krylov span identity, or the hypotheses of Theorem A.5.

A complete development needs the spectral theorem for self-adjoint operators on finite-dimensional spaces (in Mathlib), finiteness of the set of eigenvalues, and the CG invariants. The CG lemmas are reusable for any Newton–CG or trust-region CG analysis. Proofs of the milestones, and of auxiliary CG invariants such as (A.3)–(A.4), are welcome.

Selected references

• R. S. Dembo and T. Steihaug, Truncated-Newton algorithms for large-scale unconstrained optimization, Mathematical Programming 26 (1983) 190–212. https://doi.org/10.1007/BF02592055
• R. S. Dembo, S. C. Eisenstat and T. Steihaug, Inexact Newton methods, SIAM Journal on Numerical Analysis 19 (1982) 400–408. https://doi.org/10.1137/0719025
• M. R. Hestenes and E. Stiefel, Methods of conjugate gradients for solving linear systems, Journal of Research of the National Bureau of Standards 49 (1952) 409–436. https://doi.org/10.6028/jres.049.044
• T. Steihaug, The conjugate gradient method and trust regions in large scale optimization, SIAM Journal on Numerical Analysis 20 (1983) 626–637. https://doi.org/10.1137/0720042
• J. Nocedal and S. J. Wright, Numerical Optimization, 2nd ed., Springer, 2006. https://doi.org/10.1007/978-0-387-40065-5

Motivation

Minimizing a smooth function subject to simple bounds on the variables, $l\le x\le u$, is one of the most common problems in nonlinear optimization: it arises on its own (nonnegativity constraints, box-constrained least squares, parameter estimation with physical ranges) and as the subproblem of augmented Lagrangian and penalty methods. The classical approaches are active-set methods, which follow the boundary of the box and must guess which bounds are tight, and projected-gradient methods, which project trial points onto the box.

Coleman and Li proposed an alternative that never touches the boundary: an interior-reflective Newton method. Every iterate is strictly feasible; a new affine scaling $D(x)$ measures how far each variable is from the bound its gradient points toward; and the line search follows a reflective path, which bounces off the faces of the box instead of stopping at them or being projected back. The method is the basis of the trust-region-reflective algorithm in MATLAB's Optimization Toolbox (fmincon, lsqnonlin), so its convergence theory underlies a widely used solver.

Timeline:

• 1992–1994: Coleman and Li introduce the interior-reflective approach and analyse its convergence (Math. Programming 67, 1994), proving first-order global convergence (Theorem 8) and local quadratic convergence (Theorem 13).
• 1996: Coleman and Li extend the approach to trust-region subproblems (SIAM J. Optim. 6, 1996), the version implemented in MATLAB.

This mission is the first of two drawn from the 1994 paper; the second treats the local quadratic rate.

Setting

The problem (1.1) is

$$\min_{x\in\mathbb R^n} f(x)\quad\text{subject to}\quad l\le x\le u,$$

with $l\in(\mathbb R\cup\{-\infty\})^n$, $u\in(\mathbb R\cup\{+\infty\})^n$, $l\le u$. The feasible box is $\mathcal F=\{x:l\le x\le u\}$ and its strict interior is $\operatorname{int}(\mathcal F)=\{x:l<x<u\}$. Write $g(x)=\nabla f(x)$ and $H(x)=\nabla^2 f(x)$, and $g_k=g(x_k)$, $H_k=H(x_k)$ along a sequence.

The standing assumption (p. 191): for the starting point $x_1$, the level set $\mathcal L=\{x\in\mathcal F: f(x)\le f(x_1)\}$ is compact, and $f$ is twice continuously differentiable on an open set $D\supseteq\mathcal F$.

The scaling vector $v(x)$ (Definition 2) has components $v_i=x_i-u_i$ if $g_i<0$ and $u_i<\infty$; $v_i=x_i-l_i$ if $g_i\ge0$ and $l_i>-\infty$; $v_i=-1$ if $g_i<0$ and $u_i=\infty$; $v_i=1$ if $g_i\ge0$ and $l_i=-\infty$. The scaling matrix is $D(x)=\operatorname{diag}(|v(x)|^{1/2})$, and $D_k=D(x_k)$. The system $D(x)^2g(x)=0$ is equivalent to the first-order optimality conditions of (1.1).

The reflective transformation $R$ (Fig. 6) folds $\mathbb R^n$ onto $\mathcal F$ coordinate by coordinate: a coordinate with one finite bound is reflected about it, and a coordinate with two finite bounds is folded periodically (a triangle wave between $l_i$ and $u_i$). The reflective path from $x$ in the direction $s$ is $p(\alpha)=R(x+\alpha s)-x$: it moves along $s$ and reverses the corresponding component of the direction whenever it meets a face. A breakpoint is a stepsize at which the path lies on the boundary.

The interior-reflective algorithm (Fig. 9), with $0<\sigma_l<\sigma_u<1$ and $\rho>0$, starts at $x_1\in\operatorname{int}(\mathcal F)$; at each step it chooses a descent direction $s_k$ and a stepsize $\alpha_k>0$ that is not a breakpoint and satisfies

$$f(x_{k+1})<f(x_k)+\sigma_l\big(\alpha_kg_k^{T}s_k+\tfrac12\alpha_k^2\min(s_k^{T}H_ks_k,0)\big)\qquad(3.4)$$

and either

$$f(x_{k+1})>f(x_k)+\sigma_u\big(\alpha_kg_k^{T}s_k+\tfrac12\alpha_k^2\min(s_k^{T}H_ks_k,0)\big)\qquad(3.5)$$

or $\alpha_k>\rho$; then $x_{k+1}=x_k+p_k(\alpha_k)$.

The directions $\{s_k\}$ are constraint-compatible (Definition 3) if $\{D_k^{-2}s_k\}$ is bounded, and consistent (Definition 4) if $s_k^{T}g_k\to0$ implies $D_kg_k\to0$.

Formalization targets

Goal: Theorem 8

If $\{x_k\}$ is generated by the algorithm of Fig. 9 and $\{s_k\}$ is both consistent and constraint-compatible, then

$$D_k^2g_k\to0\qquad\text{and}\qquad\alpha_k^2\min(s_k^{T}H_ks_k,0)\to0 .$$

No constants are involved; the statement is the paper's.

Milestones

1. The iterates stay in $\mathcal L$ and $f(x_k)$ strictly decreases (proof of Theorem 8, p. 207).
2. Theorem 3: constraint compatibility bounds the breakpoints $BR_k(j)=|v_{kj}|/|s_{kj}|$ away from zero.
3. Lemma 7, in its one-sided form: if $\alpha_k\to0$, then $f(x_{k+1})-f(x_k)\le\alpha_kg_k^{T}s_k+C\alpha_k^2$ eventually.
4. $\alpha_kg_k^{T}s_k\to0$ and $\alpha_k^2\min(s_k^{T}H_ks_k,0)\to0$ (proof of Theorem 8, p. 208).
5. $g_k^{T}s_k\to0$ for constraint-compatible directions (proof of Theorem 8, p. 208).

Companion results: Theorem 2 (the acceptable stepsize interval exists, so the algorithm is well defined), and Theorems 5 (1)–(2) and 6 (1)–(2) (the scaled steepest-descent directions $-D_k^2g_k$ and $-D_k^2\operatorname{sgn}(g_k)$ are constraint-compatible and consistent).

Significance

Theorem 8 is the global first-order convergence theorem of the interior-reflective approach. With Theorems 5 and 6 it shows that the simplest instance, scaled steepest descent along the reflective path, reaches first-order points from any strictly feasible start; the paper's later second-order and quadratic results for the trust-region variant are built on it. Constraint compatibility and consistency isolate exactly what a search direction must satisfy, so the theorem applies to any direction rule that can be checked against these two conditions.

The result has been proved since 1994 but, to our knowledge, not machine-checked. A formalization requires a precise model of the reflective path, which the paper describes by an algorithm (Fig. 4) and a coordinate formula (Fig. 6), and a careful treatment of points where the scaling degenerates. The formal statements also make explicit a point the printed text leaves loose: Lemma 7 is printed as an equality but only an inequality holds, and only the inequality is used.

Difficulty

The argument has the shape of a standard sufficient-decrease proof, but the step that is routine for straight-line searches fails here. The path is not a line: as $\alpha$ grows, components of the direction are reversed at breakpoints, so $f(x_k+p_k(\alpha))-f(x_k)$ is not $\alpha g_k^{T}s_k+O(\alpha^2)$ in general, since a reflected component changes the linear term by an amount of order $\alpha$. Lemma 7 must show that, for constraint-compatible directions, only components whose reflection decreases the linear term can be reflected at small steps, and the Taylor remainders must be controlled uniformly over a run, on a neighbourhood of the compact level set inside the open set where $f$ is $C^2$. The scaling also degenerates at the boundary, where $v$ vanishes; the iterates must be kept strictly interior for $D_k^{-2}$ to be meaningful.

Formalization scope

Points are EuclideanSpace ℝ (Fin n); the bounds are EReal vectors with $l_i\neq+\infty$, $u_i\neq-\infty$ and $l\le u$. The box and the level set are the published LewisTorczon.BoundPS.box and levelSet. The gradient is Mathlib's gradient, and $s^{T}H(x)s$ is the inner product of the derivative of the gradient map applied to $s$ with $s$. $D(x)$ is never formed as a matrix: $D^2g$, $Dg$, $D^{-2}s$ and $D^2\operatorname{sgn}(g)$ are written componentwise. The reflective path is $R(x+\alpha s)-x$ with $R$ the transformation of Fig. 6, which the paper describes as the same method as Fig. 4 in another notation (p. 199); "not a breakpoint" is the requirement that the new iterate be interior. Descent direction is footnote 3's: strict decrease along the path for all small $\alpha>0$. Sequences start at index 0, which is the paper's $x_1$. The standing compactness and smoothness assumption is carried as explicit hypotheses.

The goal does not assume $g_k^{T}s_k\to0$, $\alpha_k\to0$, or anything about breakpoints; a version of Theorem 8 that did, or one whose algorithm projected onto the box instead of reflecting, or whose run predicate no sequence can satisfy, would not be the paper's theorem. Lemma 7 keeps the paper's assumption $\alpha_k\to0$ and records the one-sided upper bound established by its proof. Theorem 3 uses the breakpoint distance in the direction of motion and applies its bound when that distance equals $|v_{kj}|/|s_{kj}|$.

A complete development needs Taylor's theorem with uniform remainder along piecewise linear paths in a box, and basic facts about the reflection $R$ (it maps into $\mathcal F$, is the identity on $\mathcal F$, and is continuous). These are reusable for any reflective or projected line search. Proofs of the milestones in any order are welcome, as are independent proofs of the companion results.

Selected references

• T. F. Coleman and Y. Li, On the convergence of interior-reflective Newton methods for nonlinear minimization subject to bounds, Mathematical Programming 67 (1994), 189–224. https://doi.org/10.1007/BF01582221
• T. F. Coleman and Y. Li, An interior trust region approach for nonlinear minimization subject to bounds, SIAM Journal on Optimization 6 (1996), 418–445. https://doi.org/10.1137/0806023
• R. M. Lewis and V. Torczon, Pattern search algorithms for bound constrained minimization, SIAM Journal on Optimization 9 (1999), 1082–1099 (source of the published box and level-set definitions reused here). https://doi.org/10.1137/S1052623496300507

Motivation

A seller with one indivisible object must decide whether to keep it or transfer it to one of several bidders whose values she does not observe. The allocation and the payment rule affect what bidders choose to report. Myerson's 1981 paper identifies a revenue-maximizing rule when bidders' private value estimates are independent, their densities are positive, and their valuations may be revised after learning other bidders' information. It covers value distributions for which the usual virtual-value rule is not monotone, by replacing each bidder's virtual value with an ironed priority level.

The question matters to auction design because a pointwise revenue-maximizing assignment can reward a bidder for understating a value. The seller must maximize expected utility subject to both incentive compatibility and each bidder's ability to decline participation. The paper's main theorem gives a specific allocation and payment pair that meets those constraints and attains the maximum. The result is proved in the source; this mission asks for a machine-checked formalization of it.

Setting

There is a finite nonempty set $N$ of bidders and one seller. Bidder $i$ has a value estimate $t_i$ in a finite interval $[a_i,b_i]$, where $a_i<b_i$; endpoints may be negative and may differ between bidders. The continuous density $f_i$ is strictly positive on that interval and has total integral one. The bidders' estimates are independent, so a profile $t=(t_i)_{i\in N}$ has density $f(t)=\prod_i f_i(t_i)$ on $T=\prod_i[a_i,b_i]$. Write $F_i(s)=\int_{a_i}^{s}f_i(u)\,du$ for the distribution function. The seller's known value for keeping the object is $t_0$.

A revision effect $e_j(t_j)$ describes the change in everyone else's valuation after bidder $j$'s estimate becomes known. Bidder $i$'s revised value is $v_i(t)=t_i+\sum_{j\ne i}e_j(t_j)$, while the seller's is $v_0(t)=t_0+\sum_j e_j(t_j)$. A direct mechanism assigns each profile an allocation probability $p_i(t)$ and expected payment $x_i(t)$ for each bidder. Payments may be negative and need not vanish when a bidder loses. Its feasibility conditions say that allocation probabilities are nonnegative and sum to at most one, each bidder's interim expected utility is nonnegative at every possible value, and truthful reporting yields at least as much interim utility as any other report. The seller maximizes her expected utility over all feasible mechanisms.

The virtual value is $c_i(s)=s-e_i(s)-(1-F_i(s))/f_i(s)$. In the general case it need not increase with $s$. Myerson transforms $c_i$ through the quantile $q=F_i(s)$: $h_i(q)=c_i(F_i^{-1}(q))$, $H_i(q)=\int_0^q h_i(r)\,dr$, and $G_i$ is the convex envelope of $H_i$ on $[0,1]$. The slope $g_i$ of $G_i$, extended across kinks, gives the ironed priority $\bar c_i(s)=g_i(F_i(s))$. At profile $t$, the winning set $M(t)$ contains exactly those bidders whose priority is maximal and at least $t_0$.

Formalization targets

The goal is Myerson's §6 theorem. The proposed rule shares the object equally among bidders in $M(t)$, or keeps it when $M(t)$ is empty, and charges each bidder the envelope payment:

$$\bar p_i(t)=\begin{cases}|M(t)|^{-1},&i\in M(t),\\0,&i\notin M(t),\end{cases} \qquad \bar x_i(t)=\bar p_i(t)v_i(t)-\int_{a_i}^{t_i}\bar p_i(t_{-i},s)\,ds.$$

The target asserts that $(\bar p,\bar x)$ is feasible and that every feasible $(p,x)$ has seller utility no greater than that of $(\bar p,\bar x)$. The milestone list follows the paper's reduction: Lemma 2 characterizes feasible direct mechanisms by a monotone interim allocation rule and an envelope identity; equation (4.12) rewrites seller utility using virtual values; Lemma 3 turns maximization of virtual surplus into optimality. Equations (6.9)–(6.13) compare virtual and ironed priorities and establish the optimality and monotonicity of the proposed allocation.

Significance

The theorem specifies both who receives the object and how payments are computed, including irregular distributions and bidder-specific supports. The ironed priorities preserve incentives while retaining the seller's maximal expected utility. Equation (4.12) also gives the revenue-equivalence consequence: once the allocation rule and each lowest-type interim utility are fixed, expected seller utility is fixed.

A formal proof would connect several reusable results: product distributions with bidder-specific densities, interim incentive constraints, an envelope characterization, virtual-surplus accounting, and one-dimensional convex ironing. The source theorem and milestones are currently statements to be proved in this development, not existing machine-checked results. Related Börgers auction statements on Prove2Me use a common nonnegative support, at least two bidders, zero revision effects, and zero seller value; they do not provide this general theorem.

Difficulty

Maximizing virtual surplus at each profile is straightforward only if each bidder's virtual value rises with her report. When it falls, the resulting win probability can also fall, violating the incentive constraint. Replacing virtual values by slopes of a convex envelope restores monotonicity, but then the proof must account exactly for the difference between the original and ironed objectives, including flat portions of the envelope. Payments must satisfy the interim envelope identity for every type, while the seller's objective includes both transfers and her value for retaining the object.

Formalization scope

The Lean model uses a finite nonempty bidder type, real-valued reports and payments, one object, independent continuous positive densities normalized on each finite support, and continuous revision effects. The latter regularity is implicit in the paper's assertion that $c_i$ is continuous. No mean-zero condition on revision effects is imposed: the paper explicitly says its equation (2.9) is unnecessary. One bidder, negative support endpoints, unequal supports, and arbitrary seller value remain allowed.

The profile law is Lebesgue measure restricted to $T$ and weighted by the product density. Integrating a function after replacing coordinate $i$ represents the $T_{-i}$ integral, because bidder $i$'s marginal density has mass one. Mechanisms are total functions, but allocation and incentive conditions quantify over supported profiles and reports. Feasibility explicitly requires integrability of allocations, payments, and their report sections so no undefined Bochner expectation can acquire Lean's default value zero. The convex envelope is the two-point infimum of equation (6.3); its defining set is nonempty and bounded below on $[0,1]$. The slope uses the right derivative below quantile one and the left derivative at one. The theorem requires feasibility of the proposed pair as well as its utility bound, ruling out an empty or unconstrained maximization claim.

The Stieltjes expressions in (6.9), (6.12), and (6.13) are combined into equivalent ordinary-integral comparisons over the profile law. A complete proof needs the one-dimensional envelope theorem, product-measure integration and Fubini results, differentiation of the convex envelope, and a careful endpoint treatment. The definitions of interim utilities and ironing can be reused for related auction models; contributions that establish these analytic components or the listed source lemmas are in scope.

Selected references

• Roger B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1):58–73, 1981. DOI: 10.1287/moor.6.1.58.

Motivation

A Markov decision process describes repeated choices whose costs and subsequent states depend on the current state. Such models are used when a decision affects both today's expense and the options available tomorrow. Papadimitriou and Tsitsiklis studied how the computational difficulty of finding an optimal policy changes between stochastic and deterministic transitions. Their general finite-state problems are P-complete, while their deterministic cases admit highly parallel algorithms Papadimitriou and Tsitsiklis, 1987. The contrast makes the deterministic case a useful setting in which to isolate the precise graph problem hidden inside long-run optimization.

This mission concerns their infinite-horizon average-cost case. When transitions are certain, every decision is an arc in a directed graph. The long-run cost of a policy can be related to the mean cost of a cycle reachable from the initial state. That relation is the mathematical claim supporting the algorithm in the paper's Theorem 3, whose headline says that the deterministic average-cost problem is in NC Papadimitriou and Tsitsiklis, p. 446.

Setting

Let $S$ be a finite set of states and $s_0\in S$ the initial state. At each $s\in S$ there is a finite, nonempty decision set $D_s$. A decision $d\in D_s$ has a real cost $c(s,d)$ and moves the process with certainty to $\operatorname{next}(s,d)\in S$. All of these data are stationary: they do not change with time. A policy $\delta(s,t)$ chooses a decision for each state and each time $t=0,1,2,\ldots$. It generates a trajectory by $s_{t+1}=\operatorname{next}(s_t,\delta(s_t,t))$. The corresponding directed graph has a state for each node and a decision for each arc. It may contain loops and parallel arcs, since different decisions can lead to the same next state.

The paper prints the finite average with $T+1$ cost terms and denominator $T$:

$$a_T^\delta(s_0)=\frac{1}{T}\sum_{t=0}^{T}c(s_t,\delta(s_t,t)).$$

A time-dependent policy's averages may fail to converge. We use the upper limit $g^\delta(s_0)=\limsup_{T\to\infty}a_T^\delta(s_0)$ and optimize over all policies, $g^*(s_0)=\inf_\delta g^\delta(s_0)$. A state $u$ is reachable if some finite walk of decision arcs goes from $s_0$ to $u$. A simple cycle $C$ is a positive-length closed sequence of decision arcs with distinct states before it returns to its start; its mean cost is $\operatorname{mean}(C)=c(C)/|C|$. A loop is a one-arc simple cycle.

For states $u,v$, the min-plus adjacency entry $A_{uv}$ is the least cost of a decision arc from $u$ to $v$, or $+\infty$ when no such arc exists. A min-plus product uses addition in place of multiplication and minimum in place of addition. Thus $(A^k)_{uv}$ represents the least cost of a $k$-arc walk from $u$ to $v$, when such a walk exists Papadimitriou and Tsitsiklis, pp. 445–446.

Formalization targets

Reachable cycles

The first target identifies the value of the original policy optimization problem:

$$g^*(s_0)=\min_{\substack{C\text{ simple cycle}\\C\text{ reachable from }s_0}}\operatorname{mean}(C).$$

It also states that a policy attains this value with convergent finite averages. The milestone for following a reachable cycle gives the attainable direction; the milestone saying that no policy can improve the least mean gives the reverse direction. The latter is formulated with $\liminf$, so it applies even when a policy's averages oscillate.

Min-plus calculation

The second target identifies the finite graph calculation used in the paper:

$$g^*(s_0)=\min_{\substack{u\text{ reachable from }s_0\\1\leq k\leq |S|\\(A^k)_{uu}<+\infty}}\frac{(A^k)_{uu}}{k}.$$

The milestones establish what a min-plus power says about decision walks and why closed walks of lengths from $1$ through $|S|$ recover the least simple-cycle mean. The restriction to reachable $u$ is essential: a cheap cycle in a disconnected component cannot be used from $s_0$.

Significance

The result reduces optimization over infinitely many decision times and all state-and-time policies to finitely many closed-walk calculations. It also guarantees that an optimal long-run value is realized by a trajectory with a genuine limiting average, despite the nonconvergence possible for other policies. The finite formula lets one determine the value by comparing graph quantities indexed by states and lengths; it is the correctness statement beneath the paper's parallel algorithm Papadimitriou and Tsitsiklis, p. 446.

Formalizing the identity creates a reusable bridge between deterministic decision processes, weighted directed walks and min-plus powers. Related proved tropical-algebra results on maximum cycle means use dense matrices and a max-plus convention, rather than the reachable, possibly missing-arc, minimum-cost process here; for example, the platform's TropicalLA.tpow_isGreatest concerns greatest walk weights. The present mission keeps the policy optimum and reachability explicit. The paper proves the result mathematically; these Lean statements are open proof targets in the proposal.

Difficulty

An arbitrary policy can keep changing its choices at repeated visits to the same state. Its averages can oscillate, so one cannot simply assume that its infinite trajectory becomes periodic or that its printed limit exists. The lower-bound claim must apply to every such trajectory. There is a second distinction between a closed walk and a simple cycle: a diagonal min-plus entry allows repeated states, whereas the cycle characterization is stated using simple cycles. Finally, an unrestricted matrix calculation would include cycles unreachable from the chosen initial state.

Formalization scope

Lean represents the general finite stationary deterministic process in its own definition, then defines policies, finite walks, simple cycles, average costs and min-plus powers on top of it. Decisions are arcs, so parallel arcs remain distinguishable; $A_{uv}$ takes their least cost and uses WithTop ℝ for a missing arc. Decision sets are explicitly nonempty because a policy has to make a choice at every state. The finite state set is automatically nonempty once $s_0$ is supplied. Policy time starts at zero. The printed $T+1$ terms divided by $T$ are retained; Lean's $T=0$ quotient is zero and has no effect on the limit. The optimum is the infimum over all policies $\delta(s,t)$, not a quantity defined by cycles or by stationary policies. Finite states and finite decision sets bound the one-step costs and hence the averages; this gives real limsup and infimum their intended values.

The paper's Theorem 3 asserts membership in NC. This mission formalizes the exact optimization identity that makes that algorithm correct. Its processor count and parallel-time bound are outside the scope, as are membership in P, log-space computability of reductions, PSPACE membership and the paper's Corollaries 1–2. Contributions to the finite-walk and min-plus lemmas, the lower bound for arbitrary policy paths, and the cycle-attainment statement are all needed; the graph definitions can be reused in other deterministic control problems.

Selected references

• Christos H. Papadimitriou and John N. Tsitsiklis, The Complexity of Markov Decision Processes, Mathematics of Operations Research 12(3), 1987, pp. 441–450. DOI.

Motivation

Markov decision processes are the standard model of sequential decision making under uncertainty in operations research, control and artificial intelligence. Their finite-horizon, discounted and average-cost versions are all solvable in polynomial time, by dynamic programming or linear programming. Papadimitriou and Tsitsiklis (The Complexity of Markov Decision Processes, Math. Oper. Res. 12(3), 1987) asked the next question: can these problems be solved fast in parallel, in polylogarithmic time on polynomially many processors (the class NC)? Their Theorem 1 answers no, unless every polynomial-time problem parallelizes: all three versions are P-complete. The proof is a short reduction from the circuit value problem (CVP), the canonical P-complete problem (Ladner, 1975). This mission formalizes the mathematical heart of that reduction: the constructed process has optimal expected cost zero exactly when the circuit evaluates to true.

The result is the first of a series of five missions on the same paper; the others treat the deterministic special cases (which are in NC) and the partially observed case (which is PSPACE-hard).

Setting

A circuit is a finite sequence of triples $C=((a_i,b_i,c_i),\ i=1,\dots,k)$ with $k\ge1$. Each $a_i$ is one of the operations false, true, and, or. A triple with $a_i\in\{\text{false},\text{true}\}$ is an input; a triple with $a_i\in\{\text{and},\text{or}\}$ is a gate, and a gate reads two earlier triples, $1\le b_i,c_i<i$. The value of an input is its constant; the value of a gate is the Boolean operation $a_i$ applied to the values of triples $b_i$ and $c_i$. The value of $C$ is the value of triple $k$.

A finite Markov decision process has a finite state set $S$, an initial state $s_0$, and at each state $s$ a nonempty finite set $D_s$ of decisions. Taking decision $i$ at state $s$ at time $t$ costs $c(s,i,t)$ and moves to $s'$ with probability $p(s,s',i,t)$. A policy $\delta$ chooses a decision $\delta(s,t)\in D_s$ for every state and time. For a horizon $T$ the expected cost of $\delta$ is

$$J_T(\delta)=\mathbb E_\delta\Bigl[\sum_{t=0}^{T}c\bigl(s_t,\delta(s_t,t),t\bigr)\Bigr],$$

and the optimal expected cost is $J_T^\ast=\inf_\delta J_T(\delta)$ over all policies.

From a circuit $C$ the proof of Theorem 1 builds a stationary process $M_C$: one state per triple plus an absorbing state $q$. An input state has one decision, moving to $q$, at cost $1$ if the input is false and $0$ if it is true. An or gate has two free decisions, $0$ moving to $b_i$ and $1$ moving to $c_i$. An and gate has one decision, moving to $b_i$ or $c_i$ with probability $1/2$ each. All other costs are zero. The initial state is triple $k$ and the horizon is $T=k$.

In the Lean development these are MDPComplexity.CircuitValue.MDP (with Policy, trajProb, expCost, optCost), Circuit (with val, value, lastIdx) and Circuit.toMDP.

Formalization targets

Goal: correctness of the reduction

$$J_k^\ast(M_C)\le 0\quad\Longleftrightarrow\quad \text{the value of } C \text{ is true},$$

for every circuit $C$ with $k\ge1$ triples (theorem1_reduction). This is the claim "the optimum expected cost is 0 or less iff the value of $C$ was true" on p. 445.

Milestones

1. Every policy has $J_k(\delta)\ge0$ ("it cannot be less").
2. For any finite process with nonnegative costs, $J_T(\delta)=0$ iff no positive cost is incurred on any trajectory of positive probability ("the states with positive costs are impossible to reach").
3. If some policy has $J_k(\delta)=0$, then $C$ is true.
4. If $C$ is true, some policy has $J_k(\delta)=0$.

Further statement

The discounted analogue, which the paper asserts in one sentence: for $\beta\in(0,1)$, the optimal expected discounted cost $\inf_\delta\sum_{t\ge0}\beta^t\,\mathbb E_\delta[c(s_t,\delta(s_t,t))]$ of $M_C$ is at most $0$ iff $C$ is true (discounted_reduction).

Significance

Combined with the log-space computability of $M_C$ from $C$, the goal shows that the finite-horizon Markov decision problem is P-hard, hence not in NC unless P = NC. This is the reason dynamic programming for general Markov decision processes is believed to be inherently sequential, and it frames the contrast drawn in the rest of the paper: deterministic processes are in NC, and partially observed ones are PSPACE-hard. The construction is also stationary, so it shows that even the stationary finite-horizon problem is P-hard, as the paper remarks.

The theorem is proved in the paper, in one paragraph; it is not open. To our knowledge no machine-checked proof of it exists. Formalizing it produces a precise statement of what the reduction proves, a reusable finite-trajectory model of finite-horizon Markov decision processes with time-dependent policies, and a reusable encoding of Boolean circuits and their value.

Difficulty

The informal argument is short, but two points need care. First, the optimum ranges over all time-dependent policies, which form an infinite type; the infimum is attained only because the expected cost depends on finitely many decisions, and this must be established rather than assumed. Second, the passage from "the expected cost is zero" to "the circuit is true" turns a statement about trajectory probabilities into a statement about the recursive value of the circuit, and the and gates (where both successors are reached with positive probability) behave differently from the or gates (where only the chosen successor is reached). Reasoning only along a single path, as for a deterministic process, does not suffice at and gates.

Formalization scope

Theorem 1 is a complexity statement: "The Markov Decision Process problem is P-complete in all three cases." Membership in P, the log-space computability of the construction, the notion of P-completeness, and the average-cost case are not part of this mission; Mathlib has no log-space reductions or class P. The mission states the correctness of the reduction, for the exact process of the proof.

Conventions committed to:

• Triples are indexed by Fin k (paper index $i$ is Lean index $i-1$); $k\ge1$ via [NeZero k]. The fields $b_i,c_i$ of an input are unused (the paper sets them to $0$, not a triple index). Triple $k$ need not be a gate.
• States of $M_C$ are Option (Fin k), with none the state $q$; decisions are Fin 2 at or gates and Fin 1 elsewhere.
• The and-gate row is $\tfrac12\mathbf 1[s'=b_i]+\tfrac12\mathbf 1[s'=c_i]$, so that $b_i=c_i$ (allowed by the paper) gives a probability vector.
• Rows of the transition kernel are probability vectors and every $D_s$ is nonempty (implicit in the paper, explicit here).
• The expected cost is a finite sum over trajectories, with the §2 horizon convention $\sum_{t=0}^{T}$ and $T=k$. The optimum is a real infimum over all policies $\delta(s,t)$, not over stationary ones.
• The discounted cost is $\sum_t\beta^t$ times the expected time-$t$ cost, which equals the expectation of the discounted series for bounded nonnegative costs.

A formalization that defines the optimal cost directly as "the cost of the best choice at the or gates", or optimizes only over stationary policies, would make the goal a restatement of the circuit's value; the mission's optimum is over all time-dependent policies of the general model.

Contributions welcome: proofs of the milestones and the goal; lemmas on the trajectory model (marginalization of trajProb, attainment of the infimum for policies that matter only up to time $T$) that are reusable for any finite-horizon process.

Selected references

• C. H. Papadimitriou and J. N. Tsitsiklis, The Complexity of Markov Decision Processes, Mathematics of Operations Research 12(3) (1987) 441–450. https://doi.org/10.1287/moor.12.3.441
• R. E. Ladner, The Circuit Value Problem is Log Space Complete for P, SIGACT News 7(1) (1975) 18–20. https://doi.org/10.1145/990518.990519
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

Assortment optimization asks which products a retailer should offer when customers choose among the offered products according to a probabilistic choice model, so as to maximize expected revenue. Under the nested logit model the products are grouped into nests: a customer first picks a nest, then a product inside it. The model is the standard relaxation of the independence of irrelevant alternatives property of the multinomial logit, and it is used throughout revenue management and transportation demand modelling.

Davis, Gallego and Topaloglu (Oper. Res. 62(2), 2014) classify the complexity of the assortment problem under four variants of the nested logit model, according to whether the dissimilarity parameters are at most one and whether a customer who picks a nest always buys there. The problem is NP-hard as soon as some dissimilarity parameter exceeds one (their Theorem 5), and also when the nests have positive no-purchase weights (Theorem 8), so for the general variant approximation is the realistic aim. §6.2 of the paper gives an approximation scheme for the most general variant: for any $\delta > 1$ it restricts each nest to a short list of candidate assortments indexed by the powers of $\delta$, solves a small linear program, and loses at most a factor $\delta^{2\bar\gamma+1}$ of the optimal revenue. This mission formalizes the guarantee behind that scheme, Theorem 12.

Setting

There are nests $M$ and products $N = \{1, \dots, n\}$ in each nest. Product $j$ of nest $i$ has revenue $r_{ij} \ge 0$ and preference weight $v_{ij} > 0$; the products are ordered so that $r_{i1} \ge \dots \ge r_{in}$. Nest $i$ has a no-purchase weight $v_{i0} \ge 0$ and a dissimilarity parameter $\gamma_i > 0$, and $v_0 \ge 0$ is the weight of leaving without choosing a nest. Offering $S_i \subseteq N$ in nest $i$ gives

$$V_i(S_i) = v_{i0} + \sum_{j \in S_i} v_{ij}, \qquad R_i(S_i) = \frac{\sum_{j \in S_i} r_{ij} v_{ij}}{V_i(S_i)}, \qquad \Pi(S_1, \dots, S_m) = \frac{\sum_i V_i(S_i)^{\gamma_i} R_i(S_i)}{v_0 + \sum_i V_i(S_i)^{\gamma_i}}.$$

The optimal expected revenue $Z^* = \max \Pi$ is the optimal value of the linear program (3): minimize $x$ subject to $v_0 x \ge \sum_i y_i$ and $y_i \ge V_i(S_i)^{\gamma_i}(R_i(S_i) - x)$ for every nest $i$ and every $S_i \subseteq N$. Problem (4) keeps the second family of constraints only for a candidate collection of assortments in each nest.

Let $\bar\gamma = \max_i \gamma_i$, assumed $> 1$ throughout §6, and fix $\delta > 1$. Put $v^L_i = v_{i0} + \min_j v_{ij}$, $v^U_i = v_{i0} + \sum_j v_{ij}$, and let $l^L_i$, $l^U_i$ be the least integers with $\delta^{l} \ge v^L_i$, $\delta^l \ge v^U_i$. For each level $l = l^L_i, \dots, l^U_i$, problem (15) maximizes $\sum_{j \in S} r_{ij} v_{ij}$ over the assortments with $\delta^{l-1} \le V_i(S) \le \delta^l$; its value is $\hat G_{il}$. An assortment $\hat S_{il}$ is feasible for (15) and satisfies $\delta \sum_{j \in \hat S_{il}} r_{ij} v_{ij} \ge \hat G_{il}$. The candidate collection of nest $i$ is $\{\hat S_{il} : l = l^L_i, \dots, l^U_i\} \cup \{\emptyset\}$.

Formalization targets

Goal: Theorem 12 (p. 28)

If $(\hat x, \hat y)$ is an optimal solution of problem (4) over the candidate collections $\{\hat S_{il}\} \cup \{\emptyset\}$, then

$$\big(\delta^{2\bar\gamma+1}\hat x,\ \delta^{\bar\gamma+1}\hat y\big) \text{ is feasible for problem (3).}$$

Milestones (Appendix A.6, pp. 53–54)

1. $\hat x \ge 0$.
2. Every nonempty assortment of nest $i$ lies in some level $l^L_i \le l \le l^U_i$.
3. If $\delta^{l-1} \le a \le \delta^l$, then $a^{\gamma-1} \ge (\delta^l)^{\gamma-1}\delta^{-[\gamma-1]^+}$.
4. Under the same hypothesis, $(\delta^l)^{\gamma-1} \ge \delta^{-[1-\gamma]^+} a^{\gamma-1}$.
5. $\delta^{\bar\gamma}\delta^{-[\gamma_i-1]^+}\delta^{-[1-\gamma_i]^+} \ge 1$ and $\delta^{\bar\gamma+\gamma_i+1} \le \delta^{2\bar\gamma+1}$.
6. The scaled pair satisfies $\delta^{\bar\gamma+1}\hat y_i \ge V_i(S_i)^{\gamma_i}(R_i(S_i) - \delta^{2\bar\gamma+1}\hat x)$ for every nonempty $S_i$.
7. The same inequality for $S_i = \emptyset$.

Companions

• The guarantee stated after Theorem 12: with $v_0 > 0$, the assortment assembled from the candidates solving problem (5) earns at least $Z^*/\delta^{2\bar\gamma+1}$.
• Proposition 15 (p. 51): when (15) is feasible, one of the explicit assortments $\hat S(J_L, J_S)$, built from at most $q = \lceil \delta/(\delta-1)\rceil$ large and at most $q$ small products by a greedy continuous knapsack, is feasible for (15) and within a factor $\delta$ of $\hat G_{il}$.
• The count $l^U_i - l^L_i \le 1 + \log_\delta(v^U_i/v^L_i)$ (p. 28).

Significance

Theorem 12 is the analytical half of the approximation scheme. Together with the paper's Theorem 1 it shows that a linear program with $1 + m$ variables and at most $1 + m(2 + \log_\delta(v^U_i/v^L_i))$ constraints yields an assortment within a factor $\delta^{2\bar\gamma+1}$ of the optimum, for the most general variant, which is NP-hard, and Proposition 15 makes the candidate assortments computable. Letting $\delta \downarrow 1$ trades accuracy for running time, so the result is the paper's answer to how well the general problem can be approximated by this LP approach.

The result is proved in the paper; the work here is to formalize the known proof. To the best of a search of the Prove2Me library (local index and platform mirror, October 2026), no nested logit approximation result, and no knapsack lemma matching Proposition 15, has a machine-checked statement or proof. The definitions of the shared model (the instance, $V_i$, $R_i$, $\Pi$, the linear programs (3) and (4)) are common to the six missions of this series.

Difficulty

The obvious argument compares an arbitrary assortment $S_i$ with the candidate of its level and uses the candidate's constraint in (4). This fails as a direct comparison because the nest weight $V_i(\cdot)^{\gamma_i}$ enters twice with different exponents, $\gamma_i - 1$ in front of the revenue and $\gamma_i$ in front of $\hat x$, and within one level $V_i$ may vary by a factor $\delta$. When $\gamma_i > 1$ and when $\gamma_i \le 1$ the monotonicity of $t \mapsto t^{\gamma_i - 1}$ goes in opposite directions, so the losses must be tracked separately by $[\gamma_i - 1]^+$ and $[1 - \gamma_i]^+$, and they are absorbed by the common factor $\delta^{\bar\gamma}$ only because $\bar\gamma > 1$. The other half, Proposition 15, concerns a knapsack with both a lower and an upper bound on the total weight, where a feasible solution must be produced as well as a good objective value.

Formalization scope

Products are Fin n ($0, \dots, n-1$ for $1, \dots, n$), nests a finite type, powers $V^{\gamma}$ real powers, and $x/0 = 0$, which gives $R_i(\emptyset) = 0$. The shared model carries the standing assumptions of §1 with the disclosed pins $v_{ij} > 0$, $r_{ij} \ge 0$ and $\gamma_i > 0$ (the page allows $\gamma_i = 0$ and zero-weight padding products, under which its convention $0^{\gamma_i} = 0$ and its proofs fail). Every statement of the mission also assumes $n \ge 1$ (for $v^L_i$), $\bar\gamma$ is the greatest of the $\gamma_i$ (so at least one nest exists) with $\bar\gamma > 1$, and $\delta > 1$. Integer powers $\delta^l$ are zpow, and $l^L_i$, $l^U_i$ are written $\lceil \log_\delta v^L_i\rceil$, $\lceil \log_\delta v^U_i\rceil$, which equal the minima of the paper. An optimal solution of (4) is a feasible pair whose $x$ is minimal among feasible pairs. The companion guarantee adds $v_0 > 0$, the pin of Theorem 1. In Proposition 15 the capacity row of (33) includes $v_0$, correcting a printed slip, and the running-time claim is not stated.

The assortments $\hat S_{il}$ enter Theorem 12 as an arbitrary family with the two properties of p. 28; the theorem is stated for every such family. A level at which (15) has no feasible assortment imposes nothing on $\hat S_{il}$, as on the page. Requiring $\hat S_{il}$ to lie in its level unconditionally would make the hypothesis unsatisfiable for most instances and the goal vacuous; that encoding, and any goal that assumes displays (34)–(36) or the exponent bounds, is ruled out.

Contributions welcome: proofs of the real-power milestones (3)–(5), which are self-contained, of the two cases (6)–(7), and of Proposition 15, whose fractional knapsack lemma (the greedy solution of a continuous knapsack sorted by ratio is optimal) is reusable beyond this mission.

Selected references

• J. M. Davis, G. Gallego, H. Topaloglu, Assortment optimization under variants of the nested logit model, Operations Research 62(2), 2014; cited from the revised manuscript of June 18, 2013. https://doi.org/10.1287/opre.2014.1256
• A. M. Frieze, M. R. B. Clarke, Approximation algorithms for the m-dimensional 0–1 knapsack problem: worst-case and probabilistic analyses, European Journal of Operational Research 15(1), 1984. (cited on p. 50 of the paper for the continuous knapsack (33); link not verified here)
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.