The OR Formalization Drive

Motivation

Every manufacturer who makes a part in batches faces the trade-off Ford W. Harris described in 1913: large lots spread the fixed set-up cost of an order over many pieces, but they also tie up money in stock that must be carried. Harris's article "How many parts to make at once" (Factory, The Magazine of Management 10(2), 1913, reprinted in Operations Research 38(6), 1990) resolved the trade-off with a closed formula, the square-root or economic order quantity (EOQ) formula. It is the starting point of deterministic inventory theory and is still taught as the first model of every operations-management course.

Timeline. Harris published the formula in 1913, without proof ("the solution of this problem involves higher mathematics"). The same formula was popularised by R. H. Wilson in 1934 and was for decades attributed to him. D. Erlenkotter traced it back to Harris (Operations Research 38(6), 1990, 937–946), and the article was reprinted in the same issue. Later work built stochastic (Q, r) models on top of it; Zheng (1992) compared the EOQ heuristic with the optimal (Q, r) policy.

Setting

A part is used at a regular rate of $M$ units per month (the movement). Each unit costs $C$ dollars (the unit cost), and each order costs $S$ dollars to set up. Parts are made in lots of $X$ units, the lot size. Under regular movement a lot of $X$ is delivered when the stock reaches nothing and is then used up at rate $M$, so the stock at time $t \ge 0$ (months, from a delivery) is the sawtooth

$$\operatorname{stock}(t) = X\bigl(1 - \{Mt/X\}\bigr),$$

with $\{u\}$ the fractional part. Interest and depreciation on stock are charged at ten per cent a year, a rate the paper fixes.

Harris prices a unit in three parts:

1. the interest charge per piece: the average stock is $X/2$, its value including set-up is $\tfrac12(CX+S)$, ten per cent of this is the annual charge, and dividing by the $12M$ units used a year gives $\frac{1}{240M}(CX+S)$;
2. the set-up cost per piece $S/X$;
3. the unit cost $C$.

The cost per unit is therefore

$$Y(X) = \frac{1}{240M}(CX + S) + \frac{S}{X} + C,$$

and the economic lot size is $X^* = \sqrt{240MS/C}$. In Lean these are stockLevel, interestPerPiece, costPerUnit and econLotSize in the namespace HarrisEOQ.Lot.

Formalization targets

Goal: the square-root formula

For $M, C, S > 0$,

$$X^* > 0, \qquad Y(X^*) \le Y(X) \text{ for all } X > 0, \qquad Y(X) = Y(X^*),\ X > 0 \implies X = X^* .$$

This is Harris's claim that the value of $X$ giving the minimum value to $Y$ "reduces to the square root of (240MS divided by C)": $X^*$ is admissible, attains the minimum, and is the only lot size that does.

Milestones: the derivation of $Y$

1. The long-run average of the sawtooth stock is $X/2$: $\lim_{T\to\infty}\frac1T\int_0^T \operatorname{stock}(t)\,dt = X/2$.
2. The interest charge per piece, built in the paper's steps, equals $\frac{1}{240M}(CX+S)$, and $Y$ is the sum of the three per-piece costs.

These justify the objective $Y$, not its minimization; the paper gives no argument for the minimization.

Companion statements

• $X^* = K\sqrt M$ with $K = \sqrt{240S/C}$ (p. 948).
• The fourfold law: $X^*(M') = 2X^*(M) \iff M' = 4M$ (p. 950).
• A lot too small by $d$ costs more than one too large by $d$: $Y(X^*+d) < Y(X^*-d)$ for $0 < d < X^*$ (p. 949, general form of an observation made on an example).
• At the optimum, $S/X^* = CX^*/(240M)$ (p. 948).
• The paper's three worked lot sizes 2,190, 6,850 and 48.5, each to its last printed digit (pp. 948–949).

Significance

The result. The square-root formula gives the cost-minimising batch size in closed form from three observable numbers. Its consequences are the ones Harris draws: lot sizes grow only with the square root of demand (so consumption must quadruple to double a lot), the cost curve is flat near the optimum and asymmetric (erring small is worse than erring large), and at the optimum the set-up cost balances the variable carrying cost. Every later deterministic and stochastic lot-sizing model reduces to this one in its simplest case.

Formalizing it. The result is classical and proved in textbooks, but Harris's paper itself contains no proof. A formalization supplies the missing argument for the paper's exact objective, which differs from the textbook EOQ by charging interest on the set-up cost ($S/2$ in the stock value) and by the fixed ten per cent rate. It also makes the paper's modelling step precise: the claim that the average stock is $X/2$ becomes a statement about a time average of a sawtooth function. To our knowledge none of these statements has a machine-checked proof on the platform; the EOQ items of Zheng (1992) concern a different model, with backorders.

Difficulty

The minimization is elementary calculus; the substance of the mission is fidelity. The objective must be the display as printed, with $\frac{1}{240M}$ meaning $1/(240\cdot M)$, and the claim includes uniqueness, not only that $X^*$ is a minimizer. The average-stock milestone needs a genuine long-run average of a discontinuous periodic function over $[0, T]$ with $T$ not a whole number of cycles, which is where the integration and limit bookkeeping lies.

Formalization scope

All quantities are real numbers; lot sizes are not restricted to integers (the paper's own optimum is 48.5). The hypotheses $M, C, S > 0$ are not written on the page; they are implicit in the meaning of a usage rate, a price and a cost, and are added. Every quantifier over lot sizes is over $X > 0$. Time is measured in months, and the interest rate is fixed at ten per cent, so the constant $240 = 12 \cdot 2 \cdot 10$ appears as printed; the formula is not generalized to an arbitrary rate.

A trivializing formalization is ruled out: $Y$ is defined as the printed display, not rewritten around $X^*$; the average stock is an integral of the stock level, never defined as $X/2$; and the goal does not quantify over all real $X$, where Lean's convention $S/0 = 0$ would make $X = 0$ a spurious minimizer.

The manufacturing interval $T$ and the safe stock minimum play no role in the formula and are not modelled. The examples' cost figures (0.188 cents, $0.00028, and so on) are not formalized. The development needs only Mathlib's real numbers, square roots, fractional parts, interval integrals and limits; contributions of proofs of any item are welcome.

Selected references

• F. W. Harris, How many parts to make at once, Factory, The Magazine of Management 10(2):135–136, 152, 1913; reprinted in Operations Research 38(6):947–950, 1990. https://doi.org/10.1287/opre.38.6.947
• D. Erlenkotter, Ford Whitman Harris and the economic order quantity model, Operations Research 38(6):937–946, 1990. https://doi.org/10.1287/opre.38.6.937
• R. H. Wilson, A scientific routine for stock control, Harvard Business Review 13:116–128, 1934.
• Y.-S. Zheng, On properties of stochastic inventory systems, Management Science 38(1):87–103, 1992. https://doi.org/10.1287/mnsc.38.1.87

Motivation

The restricted shortest path problem asks for a shortest route between two points of a network subject to a budget on a second additive quantity, such as travel time, cost or risk. It appears as the pricing subproblem of column generation for crew scheduling and vehicle routing, in quality-of-service routing in communication networks, and in scheduling, where Hassin's own §7 uses it for a single-machine problem. The problem is NP-hard (Garey and Johnson, 1979), so exact polynomial algorithms are not expected, and the natural question is how well it can be approximated in polynomial time.

Timeline.

• 1966–1985. Practical exact methods and pseudopolynomial dynamic programs (Joksch 1966; Lawler 1976; Handler and Zang 1980; Aneja, Aggarwal and Nair 1983; Henig 1985).
• 1987. Warburton gives the first fully polynomial approximation scheme (FPAS) for this problem on acyclic graphs, based on rounding and scaling (Warburton, Oper. Res. 35, 1987).
• 1992. Hassin gives two faster FPASs: a rounding-and-scaling scheme driven by an approximate decision test (§3–§4), and a strongly polynomial scheme (§5–§6) (Hassin, Math. Oper. Res. 17, 1992).
• 2001. Lorenz and Raz give a simpler and faster scheme built on the same test-and-search pattern (Lorenz–Raz, Oper. Res. Lett. 28, 2001).

Hassin's combination of an approximate decision test with a geometric search on the bounds is the pattern later schemes for resource-constrained path problems refine, which is why his first scheme is the subject of this mission.

Setting

A directed graph has vertex set $\{1,\dots,n\}$, $n\ge 2$, and edge set $E$. Following the paper, the vertices are numbered so that every edge $(i,j)\in E$ has $i<j$; in particular the graph is acyclic. Each edge carries a positive integer length $c_{ij}$ and a positive integer transition time $t_{ij}$. A path $p=(v_0,\dots,v_m)$ has length $c(p)=\sum_r c_{v_{r-1}v_r}$ and transition time $t(p)=\sum_r t_{v_{r-1}v_r}$. For a nonnegative integer $T$, a $T$-path is a path from $1$ to $n$ with $t(p)\le T$, and $\mathrm{OPT}$ is the length of a shortest $T$-path.

Fix $0<\varepsilon<1$. For a real $V$, the rounded lengths are

$$\tilde c^V_{ij}=\Big\lfloor \frac{c_{ij}(n-1)}{V\varepsilon}\Big\rfloor .$$

Procedure TEST(V) deletes the edges with $c_{ij}>V$ and answers NO if, for some integer $c<(n-1)/\varepsilon$, some $1$–$n$ path in the remaining graph has transition time at most $T$ and rounded length at most $c$; otherwise it answers YES.

The Rounding Algorithm keeps bounds $(LB,UB)$ on OPT. Starting from initial bounds $(LB_0,UB_0)$, Step 1 repeats while $UB>2LB$: with $V=(LB\cdot UB)^{1/2}$ it sets $LB\leftarrow V$ if TEST(V) = YES and $UB\leftarrow V(1+\varepsilon)$ if TEST(V) = NO. Step 2 outputs a $T$-path that is shortest for the rounded lengths $\tilde c^{LB}_{ij}=\lfloor c_{ij}(n-1)/(\varepsilon LB)\rfloor$. The bounds after $k$ passes are written $(LB_k,UB_k)$.

Formalization targets

Goal: the approximation guarantee of the Rounding Algorithm

If $LB_0>0$ is a lower bound on the length of every $T$-path, $N$ is a stage at which $UB_N\le 2LB_N$, and $p$ is a Step 2 output at $LB_N$, then

$$c(p)\le (1+\varepsilon)\,c(q)\qquad\text{for every }T\text{-path }q,$$

that is, $c(p)\le(1+\varepsilon)\,\mathrm{OPT}$. The initial upper bound $UB_0$ is arbitrary.

Milestones (§3–§4)

1. Rounding error (§3, p. 38): with $\delta=V\varepsilon/(n-1)$, $0\le c_{ij}-\delta\tilde c^V_{ij}\le\delta$ for every edge, and $0\le c(p)-\delta\tilde c^V(p)\le V\varepsilon$ for every path.
2. TEST(V) = NO (§3, p. 38): some $T$-path has length $<V(1+\varepsilon)$, so $\mathrm{OPT}<V(1+\varepsilon)$.
3. TEST(V) = YES (§3, p. 38): every $T$-path has length $\ge V$, so $\mathrm{OPT}\ge V$.
4. Bound update (§4, p. 39): along the run, $LB_k>0$ and $LB_k$ is a lower bound on every $T$-path; if some $T$-path has length at most $UB_0$, some $T$-path has length at most $UB_k$.
5. Scaled-optimum error (§4, p. 39): a Step 2 output $p$ at any $LB>0$ satisfies $c(p)\le c(q)+\varepsilon LB$ for every $T$-path $q$.

Companion statements

• Termination when $(1+\varepsilon)^2<2$: some stage $N$ has $UB_N\le 2LB_N$; and an explicit instance with $\varepsilon=9/10$ on which Step 1 never stops.
• Initial bounds (Step 0, p. 39): every $1$–$n$ path has length between $1$ and the sum of the $n-1$ longest edge-lengths.
• Algorithms A and B (§2, pp. 37–38): their recursions compute $f_j(t)$ and $g_j(c)$, with $\mathrm{OPT}=f_n(T)=\min\{c\mid g_n(c)\le T\}$.

Significance

The guarantee makes the Rounding Algorithm a fully polynomial approximation scheme: combined with the paper's running-time analysis, a $(1+\varepsilon)$-approximate $T$-path is computed in time polynomial in the input size and $1/\varepsilon$. The two ingredients, an approximate decision test that answers "OPT $\ge V$" or "OPT $<V(1+\varepsilon)$", and a geometric search on the ratio $UB/LB$, are reused in later FPASs for constrained path, knapsack-type and scheduling problems; the milestones isolate them as separate statements.

The result has been proved since 1992 but, as far as a search of the platform and of Mathlib shows, none of it is machine-checked. This mission produces a checked version of the first scheme, stated for every stage at which the printed stopping test holds and every optimal Step 2 output. It also records, as a companion, that the printed Step 1 need not terminate when $\varepsilon>\sqrt2-1$, and proves termination under $(1+\varepsilon)^2<2$.

Difficulty

The arithmetic of each step is short; the difficulty is in the combinatorial facts the page uses without proof and in the bookkeeping of a run. The rounding error of a path is at most $V\varepsilon$ only because a $1$–$n$ path has at most $n-1$ edges, which follows from the numbering $i<j$ and must be derived for list-encoded paths. The YES case must cover $T$-paths through edges that TEST deleted, which the rounding argument does not see. The bound update needs both bounds to stay positive so that $(LB\cdot UB)^{1/2}$ is a meaningful test point, an invariant of the whole run rather than of one step. A tempting shortcut, assuming that LB is a lower bound on OPT at the stopping stage, would assume milestone 4; the goal assumes it only for $LB_0$.

Formalization scope

• Representation. Vertices are natural numbers; an instance is a structure with $n$, a finite edge set of pairs, and length and time functions, with a well-formedness predicate: $n\ge 2$, every edge $(i,j)$ has $1\le i<j\le n$, and lengths and times are positive. The requirement $n\ge2$ is not printed: a $1$–$n$ path and the divisions by $n-1$ presuppose it. Paths are nonempty vertex lists.
• Arithmetic. $n-1$ is taken in the reals; $\lfloor\cdot\rfloor$ is the natural-number floor of a nonnegative real; $(LB\cdot UB)^{1/2}$ is the real square root. Bounds and $\varepsilon$ are reals, $T$ is a natural number.
• OPT. OPT is never a number in the formal statements, because it is $\infty$ when no $T$-path exists. "OPT $\ge V$" is a bound on every $T$-path, "OPT $<V(1+\varepsilon)$" is the existence of a $T$-path, and the goal compares the output with every $T$-path. Algorithms A and B use values in $\mathbb N\cup\{\infty\}$.
• TEST(V) is defined by the answer the procedure reaches, not through Algorithm B's printed recursion, whose initial condition $g_j(0)=\infty$ is wrong for rounded lengths $0$; for $n\ge2$ and $\varepsilon<1$ the answers agree.
• The run is the iterate of one pass of Step 1; a stopped state is a fixed point. Step 2 outputs any $T$-path optimal for the rounded lengths, without pruning edges, as printed.
• Added hypothesis. The termination statement assumes $(1+\varepsilon)^2<2$, which the page does not state; without it the printed loop can run forever, and an explicit instance is included.
• Not a trivialization. The goal assumes nothing about TEST's correctness, the rounding error or the lower-bound invariant along the run, and the termination companion shows that its stopping hypothesis is reachable.
• Out of scope. The second, strongly polynomial scheme of §5–§6 is not included, because as printed its Partitioning Algorithm can report infeasibility on a feasible instance and formalizing it would require a corrected algorithm that is not the author's. All running-time claims, stated as $O(\cdot)$ bounds under an informal operation count, are also excluded, as are the $V'$ variant of the test points and the scheduling application of §7.
• Reusable parts. The list-based path layer with two additive weights, and the correctness of the pseudopolynomial recursions of Algorithms A and B, are independent of the approximation scheme. Contributions of proofs for any milestone or companion are welcome.

Selected references

• R. Hassin, Approximation schemes for the restricted shortest path problem, Mathematics of Operations Research 17(1):36–42, 1992. https://doi.org/10.1287/moor.17.1.36
• A. Warburton, Approximation of Pareto optima in multiple-objective, shortest-path problems, Operations Research 35(1):70–79, 1987. https://doi.org/10.1287/opre.35.1.70
• D. H. Lorenz and D. Raz, A simple efficient approximation scheme for the restricted shortest path problem, Operations Research Letters 28(5):213–219, 2001. https://doi.org/10.1016/S0167-6377(01)00069-4
• M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.

Motivation

Iterative methods for a system of linear inequalities $Ax\le b$ stop at a vector $\bar x$ that only almost satisfies the system: the violation $(A\bar x-b)^+$ is small but not zero. A user then needs to know that $\bar x$ is close to an actual solution. Hoffman's 1952 paper (J. Res. Nat. Bur. Standards 49) gives the first quantitative form of this fact: the distance from $\bar x$ to the solution set is at most a fixed multiple of the violation. The paper itself names one application: in Brown's method for solving games, the computed strategy vector approaches the set of optimal strategy vectors.

The result is now known as Hoffman's error bound and the constant as the Hoffman constant. It is a standard tool in convergence analysis, sensitivity analysis of linear programs, and the theory of error bounds.

Timeline.

• 1952: S. Agmon (The relaxation method for linear inequalities, NAML Report 52-27, NBS; later Canad. J. Math. 6, 1954, doi:10.4153/CJM-1954-037-2) proves the two geometric lemmas on which Hoffman's proof rests, and a bound in the Euclidean/max norm setting.
• 1952: A. J. Hoffman proves the bound for arbitrary positive homogeneous size functions $F_n$, $F_m$, and gives explicit constants in the max and sum norms by way of matrix games.
• Later work (Robinson 1973; Güler, Hoffman and Rothblum 1995; Peña, Vera and Zuluaga 2021) extends the bound to perturbed systems, characterises the sharp constant, and studies its computation.

Setting

Let $A=(a_{ij})$ be a real $m\times n$ matrix with rows $A_1,\dots,A_m$ and let $b\in\mathbb R^m$. The system (1) is $A_i\cdot x\le b_i$ for $i=1,\dots,m$, briefly $Ax\le b$; its solution set is $\Omega=\{x : Ax\le b\}$, and the system is consistent if $\Omega\ne\emptyset$. The $i$th half space is $\{x : A_i\cdot x\le b_i\}$.

For a real number $a$, $a^+=a$ if $a\ge0$ and $a^+=0$ otherwise; for a vector, $y^+$ is taken coordinatewise. So $(Ax-b)^+$ records by how much $x$ violates each inequality.

Hoffman measures sizes with a positive homogeneous function $F_k$ on $\mathbb R^k$: a continuous real function with (i) $F_k(x)\ge0$ and $F_k(x)=0$ only for $x=0$, and (ii) $F_k(\alpha x)=\alpha F_k(x)$ for $\alpha\ge0$. Norms are examples, but $F_k$ need not be symmetric, subadditive or convex.

For a set $S$ of rows, $M$ is the $m\times n$ matrix obtained from $A$ by replacing the rows outside $S$ by $0$, and $\bar y$ keeps the coordinates of $y\in\mathbb R^m$ in $S$ and zeroes the others. "Nearest" always refers to Euclidean distance. The set $E$ consists of the points $x$ outside the cone $\{z : Mz\le0\}$ whose nearest point in that cone is the origin; $K'$ is the cone spanned by the rows of $M$ with the origin removed.

Section 3 uses three norms: $|x|$ (largest absolute coordinate), $\|x\|$ (sum of absolute coordinates) and the Euclidean norm. With $g_{ij}=A_i\cdot A_j$, $a_S$ is the largest absolute coordinate of a row in $S$, and $v_S=\min_\lambda\max_{i\in S}\sum_{j\in S}g_{ij}\lambda_j$ over probability vectors $\lambda$ on $S$, the value of the matrix game $(g_{ij})_{i,j\in S}$.

Formalization targets

Goal: Hoffman's theorem (Section 2, p. 263)

If $Ax\le b$ is consistent and $F_n$, $F_m$ are positive homogeneous, there is $c>0$ such that for every $x$ some solution $x_0$ satisfies

$$F_n(x-x_0)\le c\,F_m\bigl((Ax-b)^+\bigr).$$

The constant is existential and fixed before $x$; no value is asserted. This is the weakest statement that carries the content and survives any later improvement of the constant.

Milestones: the proof's lemmas (pp. 263–264)

• Lemma 2: if $y$ is the point of $\Omega$ nearest to $x\notin\Omega$, then $x$ lies outside the intersection $\Omega_S$ of the half spaces active at $y$, and $y$ is also the point of $\Omega_S$ nearest to $x$.
• Lemma 3: for every set $S$ of rows there is $d_S>0$ with $F_m((Mx)^+)\ge d_S F_n(x)$ for all $x\in E$.
• Lemma 1: there is $e>0$ with $F_m(\bar y)\le e\,F_m(y)$ for all $y$ and all $S$.
• Lemma 4: $K'=E$.

Milestones: explicit constants (pp. 264–265)

$$\text{(9)}\quad |x-x_0|\le\frac{a}{v}\,|(Ax-b)^+|\quad\text{if all }A_i\cdot A_j>0,\ v=\min_{i,j}A_i\cdot A_j,\ a=\max_{i,j}|a_{ij}|;$$ $$\text{(10)}\quad |x-x_0|\le\frac{a}{w}\,\|(Ax-b)^+\|\quad\text{if } w=\min_i\Bigl(g_{ii}+\sum_{j:\,g_{ij}<0}g_{ij}\Bigr)>0;$$ $$\text{(8)}\quad |x-x_0|\le c\,|(Ax-b)^+|,\qquad c=\max_{v_S>0}\frac{a_S}{v_S}.$$

Each is stated as in the theorem: for every $x$ there is a solution $x_0$ with the bound.

Significance

The result. The theorem converts a residual estimate into a distance estimate. Any scheme that drives $(Ax-b)^+$ to zero brings its iterates to the solution set at a linear rate in the residual. Linear convergence proofs for projection and first-order methods on polyhedral problems and stability results for LP solution sets build on it. Formulas (8)–(10) show that in the max and sum norms the constant can be read off the rows of $A$ through a matrix game.

Formalizing it. The theorem has been proved since 1952, and later papers give several alternative proofs. The mission formalizes Hoffman's own proof route, Lemmas 1–4, in Lean and Mathlib, and the explicit constants (8)–(10). Mathlib has Farkas-type results and projections onto closed convex sets in inner product spaces, but no error bound for linear inequality systems, and the Prove2Me library has no statement of Hoffman's theorem.

Difficulty

For a single $x$, a bound is trivial: take $x_0$ the nearest solution and choose $c$ accordingly. The whole content is that one $c$ works for all $x$, including $x$ far from $\Omega$ and $x$ approaching $\Omega$ along every direction. A compactness argument on $\{x : F_n(x)=1\}$ alone fails, because the ratio $F_n(x-x_0)/F_m((Ax-b)^+)$ is not a continuous function of $x$ on a compact set: the nearest solution and the set of active constraints jump as $x$ moves. Lemma 3 needs a positive lower bound on a set $E$ that is not obviously closed away from the origin; its closedness comes from Lemma 4, i.e. from Farkas' lemma. Since $F_n$, $F_m$ are not norms, no argument using the triangle inequality or symmetry is available. For (8), a set $S$ can arise in Lemma 2 with $v_S=0$ (e.g. $x_1\le0$, $-x_1\le0$ in $\mathbb R^2$ with $x=(1,0)$), contrary to an unnumbered remark on p. 265; the bound (8) is still true, but that remark cannot be used.

Formalization scope

• Vectors are Fin k → ℝ, $A$ is Matrix (Fin m) (Fin n) ℝ, the system is A *ᵥ x ≤ b (componentwise), and $y^+$ is posPartVec y = fun i => max (y i) 0.
• $F_n$, $F_m$ are arbitrary functions satisfying IsPosHomogeneous (continuity, nonnegativity, vanishing exactly at $0$, positive homogeneity); they are never specialised to norms in the goal or Lemmas 1, 3.
• "Nearest" is Euclidean and written with the dot product: $y$ is nearest to $x$ in $\Omega$ if $(x-y)\cdot(x-y)\le(x-z)\cdot(x-z)$ for all $z\in\Omega$. (Mathlib's dist on Fin n → ℝ is the sup distance and is not used.) Lemmas 2 and 3 take "a nearest point" as hypothesis; since the Euclidean nearest point of a closed convex set is unique, this is the page's "the nearest point".
• A "subset $S$ of the half spaces" is a Finset (Fin m) of row indices; $M$ keeps all $m$ rows, with zero rows outside $S$.
• In (8)–(10), $|x|$ is ⨆ i, |x i| and $\|x\|$ is ∑ i, |x i|; minima and maxima over finite index sets are ⨅/⨆ in ℝ, equal to the attained min/max on nonempty sets. $v_S$ is defined directly by (7) as a min over the simplex of a max, for nonempty $S$, so no minimax theorem is needed. In (8), $c$ is the maximum over nonempty $S$ with $v_S>0$ and is $0$ when there is none (only when $A=0$). In $w$, the page's summation range "$j=1,\dots,n$" is read as ranging over the $m$ rows, since $g$ is indexed by rows.
• Consistency is a hypothesis of the goal and of (8)–(10).

The quantifier order $\exists c>0,\ \forall x,\ \exists x_0$ is part of the statement: a version with $c$ chosen after $x$ is trivially true and is not this theorem; likewise $e$ precedes $y$ and $S$ in Lemma 1 and $d_S$ precedes $x$ in Lemma 3.

Infrastructure a complete development needs: existence and the variational characterisation of the Euclidean projection onto a polyhedron in Fin n → ℝ; Farkas' lemma in cone form (published as LinearOptimization.farkas_cone_corollary); compactness of level sets of positive homogeneous functions. The projection and polyhedral-cone lemmas are reusable well beyond this mission. Proofs of any milestone, alternative proofs of the goal, and sharper or equivalent forms of the constants are welcome.

Selected references

• A. J. Hoffman, On Approximate Solutions of Systems of Linear Inequalities, J. Res. Nat. Bur. Standards 49(4) (1952), 263–265. https://doi.org/10.6028/jres.049.027
• S. Agmon, The Relaxation Method for Linear Inequalities, Canad. J. Math. 6 (1954), 382–392. https://doi.org/10.4153/CJM-1954-037-2
• S. M. Robinson, Bounds for error in the solution set of a perturbed linear program, Linear Algebra Appl. 6 (1973), 69–81. https://doi.org/10.1016/0024-3795(73)90007-4
• O. Güler, A. J. Hoffman, U. G. Rothblum, Approximations to solutions to systems of linear inequalities, SIAM J. Matrix Anal. Appl. 16(2) (1995), 688–696. https://doi.org/10.1137/S0895479892237744
• J. Peña, J. C. Vera, L. F. Zuluaga, New characterizations of Hoffman constants for systems of linear constraints, Math. Program. 187 (2021), 79–109. https://doi.org/10.1007/s10107-020-01473-6

Motivation

A Markov decision problem with the average reward criterion asks for a policy that maximises the long-run reward per period of a controlled finite Markov chain. It is the standard model for repeated operational decisions with no natural horizon: inventory replenishment, machine maintenance, queue admission and routing. For finitely many states and actions, Howard (1960) and Blackwell (1962) showed that a pure stationary average optimal policy exists, and policy iteration finds one.

Linear programming formulations are older for the discounted problem (d'Epenoux, 1960) and for chains with a single recurrent class (Manne, 1960). Without a structural assumption, a stationary policy can split the state space into several recurrent classes, the multichain case, and the gain becomes a vector rather than a number. Denardo and Fox (1968) gave a linear programming approach for this case. Hordijk and Kallenberg (1979) showed that a single pair of dual linear programs suffices: an optimal policy can be read off an extreme optimal solution of the dual program. Kallenberg's tract (1983, Chapter 4) is the systematic account of this theory, and this mission formalizes its §4.2–4.4.

Setting

Let $E$ be a finite set of states. Each state $i$ has a nonempty finite set $A(i)$ of actions, a reward $r_{ia}\in\mathbb R$ for each action, and transition probabilities $p_{iaj}\ge 0$ with $\sum_j p_{iaj}=1$. A policy $R$ chooses, at each epoch $t=1,2,\dots$, a probability distribution on $A(X_t)$ that may depend on the whole history. A stationary policy $\pi^\infty$ uses fixed weights $\pi_{ia}$ at every epoch. A pure stationary policy $f^\infty$ always plays $f(i)\in A(i)$. Write $P(\pi)_{ij}=\sum_a p_{iaj}\pi_{ia}$, $r(\pi)_i=\sum_a r_{ia}\pi_{ia}$, and $P(f)$, $r(f)$ in the pure case.

The average reward of $R$ from state $i$ is

$$\phi_i(R)=\liminf_{T\to\infty}\frac1T\sum_{t=1}^T\sum_j\sum_a\mathbb P_R(X_t=j,\ Y_t=a\mid X_1=i)\,r_{ja},$$

and $\hat\phi_i(R)$ is the same expression with $\limsup$. The AMD-value-vector is $\phi_i=\sup_R\phi_i(R)$, where $R$ ranges over all policies, and $R^*$ is average optimal if $\phi(R^*)=\phi$. A policy is Blackwell optimal if it maximises the discounted reward $v^\alpha(R)=\sum_{t\ge1}\alpha^{t-1}\mathbb E_R[r_{X_tY_t}]$ for all discount factors $\alpha$ in some interval $[\alpha_0,1)$.

For a stochastic matrix $P$, the stationary matrix $P^*$ is the Cesàro limit of $P^n$, and the deviation matrix is $D=(I-P+P^*)^{-1}-P^*$. For a pure policy, $\phi(f^\infty)=P^*(f)r(f)$ and $u(f^\infty)=D(f)r(f)$.

A vector $\tilde\phi$ is AMD-superharmonic if some $\tilde u$ satisfies $\tilde\phi_i\ge\sum_jp_{iaj}\tilde\phi_j$ and $\tilde\phi_i+\tilde u_i\ge r_{ia}+\sum_jp_{iaj}\tilde u_j$ for all $a\in A(i)$, $i\in E$. For weights $\beta_j>0$ with $\sum_j\beta_j=1$, the primal program (4.2.10) minimises $\sum_j\beta_j\tilde\phi_j$ over such pairs. Its dual is

$$\max\Big\{\sum_{i,a}r_{ia}x_{ia}\ \Big|\ \sum_{i,a}(\delta_{ij}-p_{iaj})x_{ia}=0,\ \ \sum_ax_{ja}+\sum_{i,a}(\delta_{ij}-p_{iaj})y_{ia}=\beta_j\ \ (j\in E),\ \ x,y\ge0\Big\}.\tag{4.2.11}$$

Write $E_x=\{i\mid\sum_ax_{ia}>0\}$.

Formalization targets

Goal: Theorem 4.2.4

If $(x^*,y^*)$ is an optimal solution of (4.2.11) and an extreme point of its feasible set, then a decision rule $f_*$ with

$$x^*_{if_*(i)}>0\ \ (i\in E_{x^*}),\qquad y^*_{if_*(i)}>0\ \ (i\in E\setminus E_{x^*})$$

exists, and every such $f_*^\infty$ is average optimal.

The goal is stated for every finite model, with no assumption on the chain structure, and for every rule-conforming $f_*$.

Milestones

1. Optimality equations (Theorem 4.2.1): a Blackwell optimal pure policy gives $(\phi^\circ,u^\circ)$ with $\phi^\circ_i=\max_{a\in A(i)}\sum_jp_{iaj}\phi^\circ_j$ and $\phi^\circ_i+u^\circ_i=\max_{a\in\bar A(i)}\{r_{ia}+\sum_jp_{iaj}u^\circ_j\}$.
2. Superharmonic characterisation (Theorem 4.2.2): $\phi$ is the smallest AMD-superharmonic vector.
3. Lim sup optimality (Theorem 4.2.3): a pure stationary average optimal $f^\infty$ satisfies $\hat\phi(f^\infty)\ge\hat\phi(R)$ for every $R$.
4. The three propositions inside the proof of Theorem 4.2.4: complementary slackness along $f_*$ (4.2.1), closedness of $E_{x^*}$ under $P(f_*)$ (4.2.2), and transience of $E\setminus E_{x^*}$ under $P(f_*)$ (4.2.3).
5. The policy–solution correspondence (§4.3): the representative $(x(\pi),y(\pi))$ is feasible (Theorem 4.3.1); the map is one-to-one with inverse (4.3.1) (Theorem 4.3.2); $E_x$ is closed under, and is exactly the recurrent set of, $P(\pi(x,y))$ (Propositions 4.3.2–4.3.3); the correspondence preserves optimality (Theorem 4.3.3); pure policies map to extreme points (Theorem 4.3.4).
6. Policy evaluation (Theorem 4.4.1): the system $(I-P(f))\tilde\phi=0$, $\tilde\phi+(I-P(f))\tilde u=r(f)$, $\tilde u+(I-P(f))\tilde z=0$ is solvable, and every solution has $\tilde\phi=\phi(f^\infty)$ and $\tilde u=u(f^\infty)$.

Significance

Theorem 4.2.4 reduces the multichain average reward problem to one linear program. Combined with Theorems 4.3.3 and 4.3.4, every pure stationary average optimal policy arises from some extreme optimal solution, so enumerating extreme optimal solutions enumerates all of them (Remark 4.2.5). The same program is the starting point for the constrained average reward problems of §4.7, where a policy must also satisfy linear constraints on its state–action frequencies. Theorem 4.4.1 is the evaluation step of multichain policy iteration.

The results are proved in the tract and, earlier, in Hordijk and Kallenberg (1979). None of them is formalized in a proof assistant. The platform has machine-checked average reward results only for unichain models, where the gain is a scalar. This mission adds the multichain theory, with general history-dependent randomized policies as competitors, and also yields reusable statements about stationary and deviation matrices of finite chains.

Difficulty

Under a unichain assumption, the dual variables $x$ form a stationary distribution and the $y$-variables are unnecessary, so the obvious argument reads a policy off $x$ alone. In the multichain case the $x$-part of an optimal solution can vanish on whole sets of states, and on those states the policy must be read off $y$. The argument then has to show that these states are transient under the selected policy, which is where extremality is essential. For a non-extreme optimal solution the book passes instead to the randomized policy (4.3.1), which needs the separate argument of Theorem 4.3.3. A second obstacle is that optimality is against all history-dependent randomized policies, so the comparison of $\phi(f_*^\infty)$ with $\phi$ must pass through the superharmonic characterisation (Theorem 4.2.2), whose proof uses the existence of a Blackwell optimal policy.

Formalization scope

The model is the published MarkovDecisionProcesses.StationaryMDP: finite state and action types, a nonempty Finset of admissible actions per state, and stochastic rows. General policies are the published AvgHRPolicy (decision rules depending on the epoch and the full history). The criteria are the published gainInf, gainSup and optGainInf; all values are real. Average optimality is the book's lim inf notion, $\phi_i(R^*)=\sup_R\phi_i(R)$ for every $i$. It is not Puterman's stronger IsAverageOptimal. The stationary and deviation matrices are the published Cesàro limitMatrix and deviationMatrix. Their existence and invertibility (Theorem 2.4.1) are never assumed as hypotheses. LP variables are indexed by admissible state–action pairs, so Set.extremePoints is the book's notion of extreme feasible solution. Recurrence is the classical finite-chain notion: every state accessible from $i$ leads back to $i$. The ergodic set of a recurrent state is the set of states accessible from it.

A formalization that assumes a unichain or ergodic model trivializes the mission (it reduces Theorem 4.2.4 to known unichain results). No statement here makes such an assumption, and the weights $\beta_j$ are strictly positive and sum to one, as in (4.2.10).

The proofs need finite Markov chain theory: the Cesàro limit, $P^*P=PP^*=P^*$, $P^*D=0$, transience versus $P^*_{\cdot j}=0$, and positivity of the stationary distribution on ergodic sets. They also need LP duality with complementary slackness and the existence of a Blackwell optimal pure policy. The last result is posed separately on the platform (Blackwell 1962, Theorem 5). LP duality is available as proved platform theorems (LinearOptimization.*), whose sign conventions must be matched. Contributions on the Markov chain layer are reusable across the whole series.

Selected references

• L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983. https://ir.cwi.nl/pub/13008
• A. Hordijk and L. C. M. Kallenberg, Linear programming and Markov decision chains, Management Science 25(4):352–362, 1979. https://doi.org/10.1287/mnsc.25.4.352
• D. Blackwell, Discrete dynamic programming, Annals of Mathematical Statistics 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
• E. V. Denardo and B. L. Fox, Multichain Markov renewal programs, SIAM Journal on Applied Mathematics 16(3):468–487, 1968.
• J. G. Kemeny and J. L. Snell, Finite Markov Chains, Van Nostrand, 1960.

Motivation

Finite Markov decision models describe repeated choices whose consequences depend on the present state. They are used when a planner needs one rule that works from every starting state, yet the rule may in principle respond to the entire observed history. Linear programming offers a different description: it records how often each state and action are used, without representing the order of decisions. Kallenberg's account connects these two descriptions for a contracting total-reward model, in which the system may terminate after a transition and all policies have finite expected occupation counts (Kallenberg 1983, §§2.2 and 3.4).

The question is whether the frequency vectors attainable by general randomized policies are already attainable through the simpler stationary classes. This matters for constrained planning: restrictions on expected total resource use are linear in frequencies, while a direct search over every history-dependent policy has no comparable finite parameterization. Kallenberg's Theorem 3.4.8 makes the exact comparison, including initial distributions that assign zero probability to some states (Kallenberg 1983, pp. 72–74).

Setting

Let $E$ be a nonempty finite set of states. Each $i\in E$ has a nonempty finite action set $A(i)$. Taking $a\in A(i)$ earns a real reward $r_{ia}$ and moves to $j$ with probability $p_{iaj}\ge 0$. A row may sum to less than one; the missing probability is termination. A policy $R$ specifies a probability distribution over $A(i)$ after every finite history ending in $i$. A Markov policy uses only time and current state, a stationary policy uses only current state, and a pure stationary policy chooses a single action $f(i)$ in each state. These are the classes $C$, $C_M$, $C_S$, and $C_D$ of §2.2 (Kallenberg 1983, pp. 19–21).

The standing contraction assumption supplies weights $\mu_i>0$ and $0\le\alpha<1$ with

$$\sum_{j\in E}p_{iaj}\mu_j\le\alpha\mu_i \qquad(i\in E,\ a\in A(i)).$$

It is weaker in form than fixing a common discount factor: the weights may differ across states. The assumption makes every policy transient, so expected total rewards and state-action frequencies are finite (Kallenberg 1983, Assumption 3.4.1 and Theorem 3.2.4).

For an initial probability distribution $\beta$, with $\beta_i\ge0$ and $\sum_i\beta_i=1$, write $x_{ja}(R)$ for the expected total number of visits to state $j$ at which action $a$ is chosen, averaged over the initial state. Let $K$, $K(M)$, $K(S)$, and $K(D)$ collect these frequency vectors for the four policy classes. The frequency polytope $P$ consists of nonnegative vectors $x$ satisfying conservation of expected flow at each state:

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

These equalities are those of the dual linear program (3.3.7), and the set names follow Notation 3.3.1 (Kallenberg 1983, pp. 53–55).

Formalization targets

The first milestones identify the total-reward value vector as the smallest TMD-superharmonic vector, establish a bijection between stationary policies and feasible frequencies when every $\beta_i>0$, and show that an optimal linear-programming solution yields a pure stationary policy optimal from every state (Kallenberg 1983, Theorems 3.4.1–3.4.3).

The mission goal allows zero entries in the initial distribution and compares all four policy classes:

$$\overline{K(D)}=K(S)=K(M)=K=P.$$

The overbar is Kallenberg's notation for the closed convex hull, rather than topological closure alone. Since there are finitely many pure stationary policies, $K(D)$ is finite and its convex hull is already closed (Kallenberg 1983, Definition 1.2.1(i) and Theorem 3.4.8).

Significance

The goal says that the finite LP flow constraints characterize exactly the frequencies of arbitrary history-dependent randomized policies. It also says that every such vector is a convex combination of frequencies from pure stationary policies. A resource-constrained objective that depends linearly on expected state-action use can therefore be expressed over $P$ without losing feasible frequency vectors. Kallenberg states this constrained consequence in Theorem 3.4.9; that theorem is beyond this mission's selected milestones (Kallenberg 1983, pp. 73–74).

The results are proved in the book. The remaining work here is a machine-checked development of their definitions and proofs, including the passage from arbitrary histories to finite flow equations. The history and frequency interfaces can also be reused for other finite, terminating control models. A proof of the goal would make explicit which uses of contraction and finite action sets justify the infinite sums and the closed convex hull.

Difficulty

For a stationary policy, the frequency equation can be written with a finite transition matrix. A general policy has a separate decision distribution after each possible history, so there is no single stationary transition matrix to substitute into that formula. A direct identification of $K$ with $P$ therefore skips the main issue. Moreover, the stationary-policy correspondence is one-to-one only when every initial weight is positive. When $\beta_j=0$, different rules at never-visited states may have identical frequencies; the set equality must survive this loss of injectivity (Kallenberg 1983, Theorem 3.4.2 and Remark 3.4.3).

Formalization scope

States and their action sets are finite and nonempty. Actions are indexed by their state, so an illegal state-action pair cannot occur. Transition rows are substochastic; rewards, values, and frequencies are real. Histories contain the past state-action pairs and current state, and time index $n=0$ represents the book's period $t=1$. The four frequency sets range over genuinely different policy classes. In particular, the general set permits every legal history-dependent randomized policy; defining it through stationary policies would erase the goal's content.

The initial distribution in the goal may have zero coordinates. The strictly positive weights in the bijection and LP-optimality milestones are the different convention of §3.3. Frequencies and rewards use infinite sums; contraction supplies their convergence. The value vector is a coordinatewise supremum over legal policies, bounded under contraction. The LP uses equalities, not relaxed inequalities, and the pure-policy set is convexified only in the goal's first equality. Needed infrastructure includes finite history probabilities, stationary transition matrices, inverse stationary flows, superharmonic vectors, and finite-dimensional convex geometry. Contributions that establish these interfaces and the three stated milestones are in scope.

Selected references

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

Motivation

Finite Markov decision models are often described by policies that choose an action from the current state. The admissible class in a total reward problem is wider: a randomized decision may use the complete history of observed states and chosen actions. For an undiscounted infinite horizon, the expected number of visits to a state may be infinite, and the total reward may be an extended real number. It matters whether a test carried out on finitely many pure stationary policies really controls this wider class. Kallenberg's Section 3.2 answers that question for finite models whose transition rows may lose probability mass when the process terminates.

The chapter is part of a 1983 account of linear programming methods for finite Markovian control. Its Theorem 3.2.4 collects earlier characterizations of transience and relates them to a finite linear program. The historical attribution in Kallenberg's Remark 3.2.2 is precise: Veinott (1969) established the equivalence of the first three conditions for nonrandomized policies, Hordijk (1976, course notes) extended the first four to general policies, and Denardo and Rothblum (1979) established the link between pure stationary transience and the LP condition. The mission targets Kallenberg's combined five-way statement, rather than treating those partial precedents as separate conclusions. Kallenberg, pp. 42–43.

Setting

Let $E$ be a finite nonempty state space of size $N$. For every state $i$, let $A(i)$ be a nonempty finite set of actions. Choosing $a\in A(i)$ gives the transition number $p_{iaj}\ge0$ to state $j$, with $\sum_jp_{iaj}\le1$. The missing mass is the probability that the system terminates before another decision epoch. This is a substochastic model; replacing the inequality by equality would change the question. Kallenberg, §2.2.

A policy $R$ specifies, at each epoch $t\ge1$, a probability distribution on $A(i_t)$ after the full history $(i_1,a_1,\ldots,a_{t-1},i_t)$. It may be randomized and may depend on all preceding states and actions. A memoryless policy depends only on the epoch and current state. A pure stationary policy $f^\infty$ chooses a single admissible action $f(i)$ in state $i$ at every epoch. Write $P_R(X_t=j\mid X_1=i)$ for the probability of state $j$ at epoch $t$ from initial state $i$. The policy is transient when $\sum_{t\ge1}P_R(X_t=j\mid X_1=i)<\infty$ for every pair $i,j$. Kallenberg, pp. 20–23.

The finite-horizon survival recursion starts from $y_i^0=1$ and sets $y_i^t=\max_{a\in A(i)}\sum_jp_{iaj}y_j^{t-1}$ for $t\ge1$. A model is contracting if there is a strictly positive vector $\mu$ and a scalar $0\le c<1$ for which $\sum_jp_{iaj}\mu_j\le c\mu_i$ for every admissible $(i,a)$. These objects are determined by the transition system; rewards do not enter the five-way characterization. Kallenberg, p. 23 and pp. 41–43.

Formalization targets

Five equivalent conditions

For any fixed $\beta_j>0$, Theorem 3.2.4 states the equivalence of: transience of every pure stationary policy; transience of every policy; $\max_i y_i^N<1$; contraction; and existence of a finite solution of

$$\max\left\{\sum_{i\in E}\sum_{a\in A(i)}x_{ia}:\ \sum_{i\in E}\sum_{a\in A(i)}(\delta_{ij}-p_{iaj})x_{ia}\le\beta_j\ (j\in E),\quad x_{ia}\ge0\right\}.$$

“Finite solution” means an attained finite optimum. The $\beta_j$ are arbitrary positive right-hand sides, not a choice that the theorem is allowed to make after seeing the model. The state count $N$ is the exponent in $y^N$, and the inequality is strict. Kallenberg, Theorem 3.2.4, pp. 42–43.

Supporting targets

The milestones follow the results the chapter uses on the way to Theorem 3.2.4, in attack order:

1. Theorem 2.5.1 (Derman–Strauch) and its Corollary 2.5.1: for a fixed initial distribution, a memoryless policy reproduces the state-action probabilities $P_R(X_t=j,Y_t=a\mid X_1=i)$ of any policy or of any countable mixture of policies.
2. Lemma 3.2.1: under Assumption 3.2.1, $\lim_{\alpha\uparrow1}v_i^\alpha(R)=v_i(R)$ in $[-\infty,+\infty]$.
3. Theorem 3.2.1: under Assumption 3.2.1 there is a pure stationary policy $f^\infty$ with $v(f^\infty)=v$, where $v_i=\sup_Rv_i(R)$.
4. Theorem 3.2.2: if $v$ is p-summable, then $v_i=\max_{a\in A(i)}\{r_{ia}+\sum_jp_{iaj}v_j\}$.
5. Theorem 3.2.3: if some policy is transient, some pure stationary policy is transient.
6. Lemma 3.2.2: $y_i^t=\sup_R\sum_jP_R(X_{t+1}=j\mid X_1=i)$, attained by the policy $(f_t,f_{t-1},\dots,f_1,f_1,\dots)$ built from maximizers of the recursion.

Assumption 3.2.1 says that every policy's expected total reward $v_i(R)=\lim_T\sum_{t\le T}v^t_i(R)$ exists in $[-\infty,+\infty]$; it is a hypothesis of items 2–4 only. Kallenberg, pp. 32–33, 37–42.

Significance

The theorem gives four finite or structured ways to recognize a property quantified over all policies. The survival condition uses only $N$ recursion steps, and the contraction condition supplies a weighted geometric bound on continuation. The LP links the same property to a finite-dimensional optimization problem. Each characterization can serve a different later argument without assuming the policy class has been reduced to stationary rules. Kallenberg, Theorem 3.2.4.

The five-way theorem and its supporting results are proved in the book; this mission asks for machine-checked proofs of their stated finite-model versions. The Derman–Strauch policy result is quoted by Kallenberg without proof, so its formal proof is a separate substantial contribution. None of these results has a machine-checked proof yet. The general history and occupancy definitions can be reused by later total-reward and constrained-control missions.

Difficulty

Checking only the finitely many pure stationary transition matrices does not directly bound the occupation counts of a history-dependent policy. Such a policy can change its action distribution after each observed path, and it need not be a mixture of stationary policies chosen once at the start. Likewise, $y_i^N<1$ is a finite-horizon bound, whereas transience is a statement about an infinite series of visit probabilities. The main difficulty is connecting these different quantifiers without changing the policy class. The LP condition adds a second boundary: its constraints use $\le\beta_j$, and finite value includes attainment. Kallenberg, pp. 41–45.

Formalization scope

States are Fin N with $N>0$, and actions form one finite ambient type with a nonempty admissible subset $A(i)$ at each state. Transitions are real nonnegative numbers with row sums at most one. Epoch $t=1$ is Lean index zero. A history records states and earlier actions; policy decision rules are normalized and supported on the current state's admissible actions. Occupancies are finite sums of transition products, so the definition of transience is summability of a nonnegative real sequence, not a bound on an individual term.

The reward layer is separate from the transition system. It uses extended real limits under Assumption 3.2.1, while the five-way goal needs no reward hypothesis. Sums $\sum_jp_{iaj}x_j$ of extended reals are only asserted for p-summable $x$, where no $+\infty$ and $-\infty$ meet with positive coefficients; the convention $0\cdot(\pm\infty)=0$ is the book's. The LP objective and constraints range only over admissible state-action pairs. Its finite-solution predicate includes a feasible optimizer. Contraction allows an arbitrary componentwise positive weight $\mu$ and requires $0\le c<1$; it does not normalize $\mu$ to the all-ones vector. The $N$-step test uses the cardinality of the original state space.

All-policy transience means every history-dependent randomized policy. Restricting that quantifier to Markov or stationary policies would remove the central content of the theorem. Useful contributions include finite-history probability identities, the Derman–Strauch occupancy theorem, the maximal-survival recursion, the stationary total-optimality result, and the finite LP characterization. The occupancy and policy definitions are reusable beyond this mission.

Selected references

• L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983. https://ir.cwi.nl/pub/13008
• C. Derman and R. E. Strauch, A note on memoryless rules for controlling sequential control processes, Annals of Mathematical Statistics 37 (1966), 276–278. https://doi.org/10.1214/aoms/1177699618
• A. F. Veinott Jr., Discrete dynamic programming with sensitive discount optimality criteria, Annals of Mathematical Statistics 40 (1969), 1635–1660. https://doi.org/10.1214/aoms/1177697379
• E. V. Denardo and U. G. Rothblum, Optimal stopping, exponential utility, and linear programming, Mathematical Programming 16 (1979), 228–244. https://doi.org/10.1007/BF01582110
• A. Hordijk and L. C. M. Kallenberg, Linear programming and Markov decision chains, Management Science 25 (1979), 352–362. https://doi.org/10.1287/mnsc.25.4.352

Motivation

A linear program often has two objectives that pull in different directions, for example cost and risk, or two policy goals whose relative weight is a matter of judgment. Gass and Saaty (NRLQ 1955) put the question in its simplest form: let every cost coefficient be an affine function $d_j + \lambda d'_j$ of one real parameter $\lambda$, and find, for every value of $\lambda$, an optimal solution. Their paper turned this into a procedure that runs the simplex method once and then walks along the $\lambda$-axis, changing one basis column at a time. This parametric objective function method became a standard chapter of linear programming texts and is the prototype of parametric and sensitivity analysis in optimization software.

Timeline.

• 1951: Dantzig publishes the simplex method (Cowles Commission Monograph No. 13, Ch. XXI; the paper's reference [1]), with the optimality test $z_j - c_j \le 0$ for a minimization problem.
• 1954: Gass and Saaty summarize the parametric procedure (J. Oper. Res. Soc. Amer. 2 (1954), 316–319).
• 1955: the present paper gives the procedure in detail, proves the THEOREM that makes it work, and reports computations on the National Bureau of Standards SEAC computer.

Setting

For each real $\lambda$ the problem is

$$\text{minimize } \sum_{j=1}^n (d_j + \lambda d'_j)\,x_j \quad\text{subject to}\quad x_j \ge 0\ (j = 1,\dots,n),\qquad \sum_{j=1}^n a_{ij}x_j = a_{i0}\ (i = 1,\dots,m).$$

Write $A = (a_{ij})$, an $m\times n$ real matrix with columns $A_1,\dots,A_n$, and $b = (a_{i0})$. A basis is a list of $m$ linearly independent columns $A_{B(1)},\dots,A_{B(m)}$; its basic solution $x$ has $x_j = 0$ off the basis and $Ax = b$, and it is a basic feasible solution when also $x \ge 0$. Every column has coordinates $y_{ij}$ in the basis, $A_j = \sum_i y_{ij}A_{B(i)}$. For a cost vector $c$ the simplex method uses $z_j = \sum_i y_{ij}c_{B(i)}$; for the cost $c = d + \lambda d'$ the number $z_j - c_j$ is affine in $\lambda$:

$$z_j - c_j = \alpha_j + \lambda\beta_j .$$

The basis is optimal at $\lambda$ when $\alpha_j + \lambda\beta_j \le 0$ for all $j$ (inequalities (3)). The critical values of the basis are

$$\underline\lambda = \max_{\beta_j<0}\Big(-\frac{\alpha_j}{\beta_j}\Big)\ (-\infty \text{ if all }\beta_j\ge 0),\qquad \bar\lambda = \min_{\beta_j>0}\Big(-\frac{\alpha_j}{\beta_j}\Big)\ (+\infty \text{ if all }\beta_j\le 0).$$

The paper assumes throughout that the problem is nondegenerate: no basic feasible solution has more than $n - m$ zero components.

Case A is the situation where the current basis is optimal for some $\lambda$, so that (3) is consistent. If $\bar\lambda$ is finite, attained at an index $s$ with $\beta_s > 0$, and some $y_{is} > 0$, the method brings $A_s$ into the basis and removes the column $A_r$, $r = B(\ell)$, chosen by the simplex ratio test; $y_{rs} > 0$. Call the new basis $B'$ and its basic feasible solution $x'$.

Formalization targets

Goal: the THEOREM (p. 41)

$$\bar\lambda = \min\big\{\lambda\in\mathbb R : x' \text{ minimizes } (d+\lambda d')^{\top}x \text{ over } Ax = b,\ x \ge 0\big\}.$$

This contains both sentences of the paper's THEOREM: the new basis yields a minimum for at least one $\lambda$ (namely $\bar\lambda$), and the left end $\underline\lambda'$ of its interval of optimality equals $\bar\lambda$. The statement uses "least element" and so does not presuppose that the set is an interval.

Milestones

1. (3): under nondegeneracy, a basic feasible solution is a minimum at $\lambda$ if and only if $\alpha_j + \lambda\beta_j \le 0$ for all $j$.
2. (4)–(5): if (3) is consistent, it holds exactly for $\underline\lambda \le \lambda \le \bar\lambda$.
3. The reduced-cost optimality criterion and its nondegenerate converse, and feasibility of the basis after a simplex pivot (both already proved on the platform).
4. [1]: $\bar\lambda$ satisfies the inequalities (3') $\alpha'_j + \lambda\beta'_j \le 0$ of the new basis.
5. (7): $\alpha'_r = -\alpha_s/y_{rs}$ and $\beta'_r = -\beta_s/y_{rs}$.
6. (7)–(8): no $\lambda < \bar\lambda$ satisfies (3').
7. Case A stop: in the nondegenerate Case A setup, if every $y_{is} \le 0$, there is no minimum for any $\lambda > \bar\lambda$.
8. Summary (4): under the section's standing assumptions, the set of $\lambda$ for which a minimum exists is closed and connected.

Significance

The THEOREM is what makes the parametric procedure correct. The optimality intervals of successive bases meet end to end: the basis entered at $\bar\lambda$ takes over exactly where the old one stops, with no gap and no overlap. Together with the stopping rule this gives the paper's summary: starting from one optimal basis, the procedure produces a finite list of bases and characteristic values covering every $\lambda$ for which the problem has a minimum, and that set is a closed interval. The same structure underlies the piecewise linear, concave optimal value as a function of $\lambda$, the parametric right-hand-side method by duality, and the shadow-vertex simplex method.

The result is classical and its proof is short, but as printed it contains a sign slip: display (8) on p. 41 states the inequality in the wrong direction, so the contradiction the authors claim does not follow from what they wrote. The formal development states the corrected argument. To our knowledge none of these parametric statements has a machine-checked proof; the fixed-cost facts they rest on (the reduced-cost optimality criterion, Bertsimas–Tsitsiklis Theorem 3.1, and the feasibility of the pivoted basis, Theorem 3.2) are already proved on the platform in Shuze Chen's LinearOptimization library and are reused here as reference items.

Difficulty

The natural first idea is to observe that $\bar\lambda$ satisfies (3') and conclude. This proves only that the new basis is optimal at $\bar\lambda$. The statement that nothing below $\bar\lambda$ works is a statement about optimality, not about the inequalities (3'): one must know that failure of (3') at $\lambda$ means that $x'$ is not optimal at $\lambda$. That converse of the optimality test is false for a degenerate basic solution, which can be optimal while some $z_j - c_j$ is positive. The nondegeneracy assumption is therefore essential, and it must be transported to the new basic solution. The other ingredient is the pivot update of $z_j - c_j$ when one column leaves and another enters, which the paper uses through (7) without writing it down.

Formalization scope

The problem data are A : Matrix (Fin m) (Fin n) ℝ, b : Fin m → ℝ and cost vectors d d' : Fin n → ℝ; the parameter $\lambda$ is the Lean variable t (λ is a Lean keyword). Indices are 0-based. Feasible set, optimality, bases, reduced costs, basic directions, the coordinates $y_{ij}$ (pivotColumn) and basic feasible solutions (IsSimplexState) are the published LinearOptimization definitions. The commitments and readings of the paper's phrases are:

• Sign. The platform's reduced cost is $\bar c_j = c_j - c_B'B^{-1}A_j = -(z_j - c_j)$; $\alpha_j$ and $\beta_j$ are defined as the negatives of the reduced costs for $d$ and $d'$, and (3), (3'), (5), (7) are stated in the paper's sign.
• "Yields a minimum" means that the point is feasible and its cost is at most that of every feasible point (IsLpOptimal), never a comparison of values.
• $\bar\lambda$ is finite in the THEOREM; it is the real number $-\alpha_s/\beta_s$ for an index $s$ with $\beta_s > 0$ attaining the minimum. As a function, (5) is valued in WithTop ℝ and WithBot ℝ; no real infimum of a possibly empty set is used.
• Nondegeneracy is stated for every basic feasible solution, including in the Case A stopping rule and Summary (4). The stopping rule also carries Case A consistency, and Summary (4) carries the section's available basic feasible solution. Linear independence of the rows of $A$ is assumed where the platform's criteria need it; it follows from the existence of a basis.
• "By the simplex method" is the reduced-cost optimality criterion; "the simplex prescription" is the ratio test; "no minimum" in the stopping rule is the unbounded outcome, optimal value $-\infty$, with the absence of a minimizer stated explicitly.
• The paper's interval $\delta \le \lambda \le \phi$ of interest plays no role in the THEOREM and is dropped.

The goal is not satisfied by a degenerate reading: its set is defined by optimality, not by the inequalities (3'), and its hypotheses hold on an explicit instance, so the statement is neither the definition of the critical value restated nor vacuous.

Not formalized: Case B (the search for a first $\lambda$ with a minimum), Summary (1)–(2) on the whole procedure, the no-repetition remark, the computing experience (§3) and the worked example (§4). Contributions welcome include the pivot-update formula for reduced costs, which is reusable for any simplex-based argument, and the closedness of the set of cost vectors with a finite optimum.

Selected references

• S. Gass and T. Saaty, The computational algorithm for the parametric objective function, Naval Research Logistics Quarterly 2 (1955), 39–45. https://doi.org/10.1002/nav.3800020106
• T. Saaty and S. Gass, The parametric objective function, Journal of the Operations Research Society of America 2 (1954), 316–319. https://doi.org/10.1287/opre.2.3.316
• G. B. Dantzig, Maximization of a linear function of variables subject to linear inequalities, in T. C. Koopmans (ed.), Activity Analysis of Production and Allocation, Wiley, 1951, Ch. XXI (Cowles Commission Monograph No. 13).
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, §3.1–3.2 and §5.2.