All missions

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

Formalization targets

Goal: THEOREM 4 (p. 462)

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

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

Motivation

A two-person zero-sum stochastic game (also called a Markov game) is a Markov decision problem with two decision makers who pull in opposite directions: at every time point both players choose an action simultaneously, one player pays the other, and the system moves to a random next state whose law depends on the current state and both actions. Stochastic games were introduced by Shapley (Shapley 1953) and are the standard model for adversarial sequential decisions in operations research, economics and computer science (pursuit–evasion, inspection, robust control against an adversarial environment).

Shapley proved that a discounted stochastic game has a value and that both players have stationary optimal policies. The value, however, is in general not computable by linear programming: it need not lie in the field generated by the data. Kallenberg's Example 6.2.1 (after Parthasarathy and Raghavan) has rational data and an irrational value in one state. When only one player controls the transition probabilities, the situation changes: the value and stationary optimal policies are the optimal solutions of one pair of dual linear programs (Parthasarathy & Raghavan, as cited in Kallenberg 1983, pp. 192 and 196; Kallenberg 1983, Chapter 6).

Timeline.

• 1953: Shapley proves existence of the value and of stationary optimal policies for the discounted game.
• 1977–1978: Parthasarathy and Raghavan study games in which one player controls the transitions and identify an order-field property for the value and optimal decision rules (cited in Kallenberg 1983, pp. 192, 196).
• 1983: Kallenberg presents the dual pair (6.2.1)/(6.2.2), with the controlling player's policy read off the dual and the opponent's from the primal, and a constructive existence proof (Remark 6.2.2).

Setting

The state space is $E = \{1,\dots,N\}$ with $N>0$. In state $i$ player I chooses an action $a$ from a finite nonempty set $A(i)$ and player II an action $b$ from a finite nonempty set $B(i)$. Player I then receives $r_{iab}$ from player II, and the next state is $j$ with probability $p_{iabj} \ge 0$, where $\sum_j p_{iabj} \le 1$.

A history at time $t$ is $(i_1,a_1,b_1,\dots,i_{t-1},a_{t-1},b_{t-1},i_t)$. A policy $R_1$ of player I chooses, at each time and history, a probability distribution on $A(i_t)$; policies $R_2$ of player II are defined likewise. A policy is stationary, written $\pi^\infty$ or $\rho^\infty$, if the distribution depends only on the current state. With $v_i^t(R_1,R_2)$ the expected reward in period $t$ from initial state $i$, the total reward is $v_i(R_1,R_2) = \sum_{t\ge1} v_i^t(R_1,R_2)$.

A pair $(R_1^*,R_2^*)$ is optimal if, componentwise,

$$v(R_1,R_2^*) \le v(R_1^*,R_2^*) \le v(R_1^*,R_2) \qquad\text{for all policies } R_1,R_2, \tag{6.1.1}$$

and then $\mathrm{val(TMG)} := v(R_1^*,R_2^*)$ is the value of the game.

Assumption 6.2.1 (contraction). There are $\mu \gg 0$ and $\alpha\in[0,1)$ with $\sum_j p_{iabj}\mu_j \le \alpha\mu_i$ for all $i$, $a\in A(i)$, $b\in B(i)$. The discounted game is the case $\mu = e$.

Assumption 6.2.2 (single controller). $p_{iabj}$ does not depend on $b$; it is written $p_{iaj}$.

For a stationary $\rho$ write $r_{ia}(\rho) = \sum_b r_{iab}\rho_{ib}$ and $p_{iaj}(\rho)=\sum_b p_{iabj}\rho_{ib}$. A vector $y$ is TMG-superharmonic if some stationary $\rho^\infty$ of player II satisfies $y_i \ge r_{ia}(\rho) + \sum_j p_{iaj}(\rho) y_j$ for all $a\in A(i)$, $i\in E$. For weights $\beta_j>0$ the two linear programs are

$$\min\Big\{\textstyle\sum_j\beta_jy_j \ \Big|\ \sum_j(\delta_{ij}-p_{iaj})y_j-\sum_b r_{iab}\rho_{ib}\ge0;\ \sum_b\rho_{ib}=1;\ \rho_{ib}\ge0\Big\} \tag{6.2.1}$$ $$\max\Big\{\textstyle\sum_iz_i \ \Big|\ \sum_i\sum_a(\delta_{ij}-p_{iaj})x_{ia}=\beta_j;\ -\sum_a r_{iab}x_{ia}+z_i\le0;\ x_{ia}\ge0\Big\} \tag{6.2.2}$$

Formalization targets

Goal: Theorem 6.2.3

Under Assumptions 6.2.1 and 6.2.2, let $(y^*,\rho^*)$ and $(x^*,z^*)$ be optimal solutions of (6.2.1) and (6.2.2), and $\pi^*_{ia} := x^*_{ia}/\sum_a x^*_{ia}$. Then

$$v(R_1,(\rho^*)^\infty) \le v((\pi^*)^\infty,(\rho^*)^\infty) = y^* \le v((\pi^*)^\infty,R_2)\qquad\text{for all policies } R_1,R_2 .$$

The goal fixes no constants; it states that the LP pair produces the value and optimal stationary policies.

Milestones

1. Theorem 6.2.1 (Shapley): under Assumption 6.2.1 both players have stationary optimal policies.
2. Theorem 6.2.2: under Assumption 6.2.1, $\mathrm{val(TMG)}$ is the smallest TMG-superharmonic vector.
3. Theorem 6.2.4 (i): for a stationary $\pi^\infty$ of player I, $x_{ia}(\pi) = [\beta^T(I-P(\pi))^{-1}]_i\pi_{ia}$ and $z_i(\pi) = \min_{b} r_{ib}(\pi)\sum_a x_{ia}(\pi)$ give a feasible point of (6.2.2) with $\sum_i z_i(\pi) = \min_\rho \sum_j\beta_j v_j(\pi^\infty,\rho^\infty)$.
4. Theorem 6.2.4 (ii): every feasible $(x,z)$ of (6.2.2) has $x = x(\pi)$ and $z\le z(\pi)$ for $\pi_{ia} = x_{ia}/\sum_a x_{ia}$.

Theorems 6.2.1 and 6.2.2 hold for the general contracting game. Assumption 6.2.2 enters only from (6.2.1) on.

Significance

The result. Theorem 6.2.3 turns a single-controller game into a finite computation, Algorithm XXVII: solve one LP pair and read off the value and optimal stationary policies of both players. A consequence (Remark 6.2.1) is that the value and the optimal decision rules lie in the field generated by the rewards and transition probabilities. Example 6.2.1 shows this fails without Assumption 6.2.2. Theorem 6.2.4 matches the feasible points of the dual program with the stationary policies of the controlling player. This is the game version of the correspondence between state-action frequencies and policies in Markov decision problems.

Formalizing it. All results are proved in the book, and Theorem 6.2.1 is classical. None of them is formalized: the platform has turn-based stochastic games with positional strategies (TBSGStrategyIteration), which do not cover simultaneous moves or history-dependent randomized policies. The mission adds a reusable model of simultaneous-move stochastic games with history-dependent policies, together with machine-checked optimality of the LP solution against every such policy.

Difficulty

There are two difficulties. First, optimality in (6.1.1) is against every history-dependent randomized policy of the opponent, while the LP produces only stationary policies. Fixing one player's stationary policy reduces the game to a Markov decision problem for the other player (Remark 6.1.1), and the facts needed from that problem (stationary policies suffice, and the value is the smallest superharmonic vector) are theorems about contracting MDPs, not consequences of the LP. Second, Theorem 6.2.2 rests on Shapley's existence theorem, which is not a linear-programming fact: its usual proof is a fixed-point argument for the Shapley operator built from one-stage matrix games. Remark 6.2.2 indicates a route that avoids it, through the bounded polytope of state-action frequencies of a contracting MDP. Either way, LP duality alone does not give optimality against non-stationary opponents.

Formalization scope

• Model. $E$ is Fin N with $N>0$. Actions live in finite types α, β, and $A(i)$, $B(i)$ are nonempty Finsets. Rows are substochastic.
• Policies. A history in $H_{n+1}$ is a record of $n+1$ states and $n$ actions of each player. A policy is a family of distributions indexed by time and history, supported on the current action set. Stationary policies are the image of state-dependent decision rules.
• Probabilities and reward. History probabilities are explicit finite products, with no measure theory. The total reward is the tsum of the period rewards, which converges absolutely under Assumption 6.2.1, and every theorem assumes it.
• Linear programs. Their variables are functions on all actions that vanish off $A(i)$ (resp. $B(i)$). Optimality means feasible and attaining the min/max over the feasible set. The common $p_{iaj}$ is $p_{iab_0j}$ for a fixed $b_0\in B(i)$, and Assumption 6.2.2 makes the choice irrelevant. $\beta_j>0$ is a hypothesis, as on p. 194.
• The minimum in Theorem 6.2.4 (i) is over stationary policies of player II and is stated with attainment.

Restricting either player's policy class to stationary policies would make the optimality claims of Theorems 6.2.1 and 6.2.3 a statement about a finite family and is ruled out: the comparison class is all history-dependent randomized policies.

Lemma 6.1.1 is Mathlib's isSaddlePointOn_value (Mathlib/Order/SaddlePoint.lean) and is not restated. The LP duality theorems of Chapter 1 are proved on the platform (LinearOptimization.lp_strong_duality, lp_complementary_slackness) and may be used. Useful contributions include: the reduction of Remark 6.1.1 (a fixed stationary opponent gives an MDP), the contracting-MDP facts it needs, and a proof of Theorem 6.2.1. The model definitions are reusable for any finite stochastic game.

Selected references

• L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983, Chapter 6. https://ir.cwi.nl/pub/13008
• L. S. Shapley, Stochastic games, Proceedings of the National Academy of Sciences 39 (1953) 1095–1100. https://doi.org/10.1073/pnas.39.10.1095
• T. Parthasarathy and T. E. S. Raghavan, Finite algorithms for stochastic games, International Conference on Dynamic Programming, Vancouver, 1977; cited in Kallenberg 1983, p. 232. https://ir.cwi.nl/pub/13008
• T. Parthasarathy and T. E. S. Raghavan, An order field property for stochastic games when one player controls the transition probabilities, Game Theory Conference, Cornell, 1978; cited in Kallenberg 1983, p. 233. https://ir.cwi.nl/pub/13008

Why optimize only transient policies?

A Markov decision model describes a system that repeatedly occupies a state, receives a reward when an action is chosen, and then moves according to action-dependent probabilities. Termination may occur after any action. In a model with signed rewards, a policy that continues indefinitely can have a different total-reward behavior from one that eventually leaves the active states. Section 3.3 of Kallenberg's 1983 monograph therefore asks for the best policy within the transient class. The restriction occurs naturally in stopping problems: a decision maker may continue for a while, but the expected number of visits to each active state must remain finite.

The chapter relates that policy problem to a finite linear program. The central question is stronger than finding a policy with a large average over initial states. It asks for one policy that is optimal from every initial state among all transient policies, including policies that randomize and use the entire observed history. Kallenberg's Theorem 3.3.5 says that an extreme optimal point of the program identifies such a policy, and that the policy can be pure and stationary. Theorem 3.3.5, p. 57.

The finite model and its policies

Let $E=\{1,\ldots,N\}$ be a nonempty finite state set. Each state $i$ has a finite nonempty set $A(i)$ of available actions. If action $a\in A(i)$ is selected, the system earns the real reward $r_{ia}$ and then moves to $j$ with probability $p_{iaj}\ge0$. The row sum $\sum_jp_{iaj}$ is at most one; any missing mass represents termination. Action sets can differ across states. These are the conventions of Section 2.2, pp. 19–20.

A policy $R$ selects an action distribution at each decision epoch. It may depend on the entire state-action history. A Markov policy depends only on time and the current state; a stationary policy uses the same state-dependent distribution at every time; a pure stationary policy selects one action $f(i)\in A(i)$ in each state. These four classes are denoted $C$, $C_M$, $C_S$, and $C_D$. The first decision occurs at time $t=1$ in the book.

Write $\mathbb P_R(X_t=j,Y_t=a\mid X_1=i)$ for the chance of being in state $j$ and choosing action $a$ at time $t$, given initial state $i$. A policy is transient if the expected number of visits to each state is finite from every initial state:

$$\sum_{t=1}^{\infty}\mathbb P_R(X_t=j\mid X_1=i)<\infty\qquad(i,j\in E).$$

For such a policy, its expected total reward $v_i(R)$ is finite. Section 3.3 assumes that at least one transient policy exists. Its transient value is $w_i=\sup\{v_i(R):R\text{ transient}\}$, which can still be infinite as the policy varies. Section 2.2, pp. 21–23; §3.3, pp. 49–50.

Formalization targets

Fix positive weights $\beta_j>0$. The linear program (3.3.7) maximizes $\sum_{i,a}r_{ia}x_{ia}$ over nonnegative state-action arrays satisfying the flow equations

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

Its feasible set is $P$. A transient stationary rule $\pi$ has an occupation vector $x(\pi)$, where $x_{ia}$ is the $\beta$-weighted expected number of visits to state-action pair $(i,a)$. Theorem 3.3.3 identifies transient stationary rules bijectively with $P$ and identifies extreme points with pure rules. Theorem 3.3.4 compares the occupation sets of all four policy classes: $\overline{K(D)}\subset K(S)=K(M)=K=P$, where the bar means closed convex hull. Theorems 3.3.3–3.3.4, pp. 54–55.

The goal is Theorem 3.3.5, p. 57. If $x^*$ is an extreme optimal solution of that program and $f_*(i)$ is the action with $x^*_{i f_*(i)}>0$, then the pure stationary policy $f_*^\infty$ is transient and

$$v_i(R)\le v_i(f_*^\infty) \qquad\text{for every transient policy }R\text{ and every }i\in E.$$

A stronger companion statement is Theorem 3.3.6, p. 58: under the correspondence of Theorem 3.3.3, a stationary policy is optimal transient exactly when its occupation vector is optimal for (3.3.7), in the two directions printed on the page. The milestone list follows the chapter's numbered results on the finite-value Bellman equation, the smallest superharmonic vector, the stationary-policy/LP correspondence, the four occupation sets, and the preservation of optimality. The goal itself does not assume that $w$ is finite; the existence of an extreme LP optimum is its stated premise.

What the result gives

An LP optimum is a vector of occupation amounts, not an implementable policy by itself. Theorem 3.3.5 converts an extreme optimum into an action choice at each state. It also upgrades a scalar objective weighted by $\beta$ to simultaneous optimality of the resulting policy from every initial state. This is the bridge between the finite optimization problem and the original control problem. The scope is specifically transient optimality: Example 3.3.4, p. 58 gives a policy outside that comparison class with larger total reward.

The result is proved in the book. The work here is to give its model, occupation map, linear program, and numbered supporting statements precise Lean interfaces that can later receive machine-checked proofs. The reusable parts include finite substochastic MDP data, history-dependent policy semantics, transient visit sums, and state-action occupation vectors. The theorem proofs are open in this proposal.

Where the difficulty lies

Optimizing a weighted sum of rewards is not, by itself, the same as optimizing every state's reward. The linear program also describes flows of expected visits, while the theorem talks about actual policies and all initial states. A solver must account for both links without assuming that all policies are stationary. The geometry of an extreme feasible point matters because the theorem selects an action from each state using a positive coordinate. Existence of a transient policy does not by itself bound the supremum of transient rewards; Example 3.3.1, p. 50 makes that distinction explicit.

Formalization scope

Lean uses Fin N with $N>0$ for states and a finite action type with a state-dependent finite nonempty available-action set. Only available state-action pairs index occupation vectors and LP variables. Transition rows are substochastic, not necessarily stochastic. Rewards are real and may have either sign. A general policy is a normalized action kernel on full finite histories; its Markov, stationary, and pure stationary subclasses remain distinct. The history list is stored newest first, and Lean's time index zero corresponds to the book's time one. All state-action probabilities are finite sums over histories; transience is summability of state-visit probabilities, and occupation counts are infinite sums used under that condition.

The LP flow constraints are equalities and $\beta$ is strictly positive. The goal does not normalize $\beta$ to a probability distribution, matching (3.3.7); Theorem 3.3.4 uses the initial-distribution convention of p. 55 and hence normalizes it. Theorem 3.3.3 uses the matrix inverse $(I-P(\pi))^{-1}$ only for transient stationary rules. For Theorems 3.3.1–3.3.2, nonemptiness of the transient class and boundedness above of each transient reward set make the real supremum meaningful. Theorem 3.3.5 uses neither boundedness as an extra hypothesis nor a restriction of the comparison class to stationary policies. A formalization that compares $f_*^\infty$ only with stationary (or Markov) policies, or that identifies the classes $C$, $C_M$, $C_S$, $C_D$, would make Theorems 3.3.4 and 3.3.5 much weaker or trivial, and is ruled out: the comparison class is every history-dependent randomized transient policy. Mathlib's finite sums, matrices, summability, convex hull, and extreme-point definitions provide the general library interface. Contributions establishing the policy/occupation identities and the chapter's numbered milestones are within scope.

Selected references

• L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983, §§2.2 and 3.3, pp. 19–23 and 49–60. Publisher repository.

Motivation

Integer linear programming asks for the best point whose coordinates are integers, even though linear programming methods naturally search over real points. In his 1958 note, Gomory describes a systematic way to add a constraint that excludes a fractional simplex solution while retaining every nonnegative integer solution. This mission isolates that single cut and its effect on the objective value. The note announces an iterative finite algorithm, but explicitly defers a proof of finiteness to another treatment. The target here is the cut's correctness for one tableau.

The cut belongs to the history of cutting plane methods for integer programs. Related formalized objects include a Chvátal closure and intersection cuts based on lattice free sets, but their data and cut constructions differ from the row and fractional part formula in Gomory's note. The note itself contrasts its systematic row operation with earlier problem specific constraints used by Dantzig, Fulkerson, and Johnson and by Markowitz and Manne. Those comparisons explain why a reusable row formula is useful; they do not assert an identity between the different cuts.

Setting

A tableau is a finite array of real numbers $a'_{i,j}$. Row $0$ represents the objective variable $w$; rows $1,\ldots,m$ represent $x'_1,\ldots,x'_m$. Column $0$ holds constants; columns $1,\ldots,n$ multiply the negatives of the variables $t'_1,\ldots,t'_n$. A solution of (2) is a pair $(x',t')$ satisfying

$$x'_i=a'_{i,0}+\sum_{j=1}^{n}a'_{i,j}(-t'_j),\qquad 0\le i\le m.$$

The original integer program requires $w=x'_0$, every $x'_i$, and every $t'_j$ to be nonnegative integers. The simplex solution of this tableau has $t'=0$ and $x'_i=a'_{i,0}$. It is a real tableau solution, whether or not any of its coordinates are integers.

Choose a row $i_0$ whose constant $a'_{i_0,0}$ is not an integer. For each coefficient let $n'_{i_0,j}=\lfloor a'_{i_0,j}\rfloor$ be the greatest integer at most that coefficient, and let $f'_{i_0,j}=a'_{i_0,j}-n'_{i_0,j}$ be its fractional part. Equation (3) defines a new variable

$$s_1=-f'_{i_0,0}-\sum_{j=1}^{n}f'_{i_0,j}(-t'_j).$$

The augmented system (2)* adds this equation to the tableau. Feasibility now also requires $s_1\ge0$; an integer solution additionally requires $s_1\in\mathbb Z$. For example, the one row relation $x'=\tfrac12-\tfrac12t'$ admits the integer solution $(x',t')=(0,1)$, and its cut value is $s_1=0$. At the simplex point $t'=0$, the same cut value is $-\tfrac12$.

Formalization targets

Fractional cut and integer optimum

The main target combines exclusion of the simplex solution, exact correspondence of nonnegative integer solutions, and equality of their attained objective values. Writing $\mathcal I_2$ and $\mathcal I_{2^*}$ for the two sets of nonnegative integer solutions, the correspondence is

$$(x',t')\in\mathcal I_2\quad\Longleftrightarrow\quad (x',t',s_1(x',t'))\in\mathcal I_{2^*}.$$

Every member of $\mathcal I_{2^*}$ has the displayed cut value for $s_1$, and the projection that drops $s_1$ leaves $w$ unchanged. Consequently a real $W$ is the greatest attained $w$ value for (2) exactly when it is the greatest attained value for (2*). The statement does not assume either set has a maximum.

Supporting claims

The milestones follow the paragraphs on page 277: projection of feasible solutions, the impossibility of integer solutions when the selected row has a fractional constant but only integral other coefficients, exclusion of the simplex point, the identity proving $s_1$ integral, and its nonnegativity on integer solutions. These are the claims the note uses to pass from the cut formula to the correspondence and the objective statement.

Significance

The result certifies that equation (3) removes the current fractional simplex point while retaining every integer candidate and its objective value. It is the local correctness condition needed before one can safely reoptimize an integer program after adding this constraint. The note's argument is a mathematical result about one tableau, independent of whether the subsequent sequence of pivots terminates.

This mission supplies a machine checkable interface for the tableau, the fractional cut, and the projection between their integer feasible sets. The theorem statements are drafted and compile with open proofs; this mission does not claim that the paper's result already has a machine checked proof here. A completed proof would make the one cut result available for later developments about iterations, optimization, or stronger cut families.

Difficulty

The cut value is visibly at least $-f'_{i_0,0}$ when the nonbasic variables are nonnegative, but that inequality alone does not give $s_1\ge0$: the right side is negative for the chosen row. The key additional statement is that the real expression for $s_1$ is an integer on an integer tableau solution. Formalization must preserve both facts while using the same sign convention for the tableau and the cut. Merely defining the augmented solution as a pair together with its computed cut value would make the correspondence automatic and would omit the new variable's integrality and nonnegativity requirements.

Formalization scope

Lean uses real valued tableau coefficients and real valued variables with a separate predicate for being an integer. This lets the fractional simplex point and integer feasible points inhabit the same space. The row and column sets are finite, including the cases $m=0$ and $n=0$; row $0$ is $w$, column $0$ is the constant column, and Lean's Fin n index $j$ denotes the paper's $t'_{j+1}$. The selected row can be row $0$ in Lean. Gomory chooses a constraint row, but the local cut argument needs only the selected row's variable to be integral, and $w$ is integral in the stated problem. Every variable, including $w$ and the added $s_1$, is required to be nonnegative and integral in an integer solution.

The fractional part uses the greatest integer at most a real number, including negative coefficients. The objective comparison uses greatest elements of the sets of attained $w$ values, so empty and unbounded sets receive no artificial supremum. Nonnegative constants and objective row coefficients are features of the simplex setting, but the five local claims and goal remain valid without those extra hypotheses. The paper's loose phrases “cuts off,” “one-one correspondence,” and “can be replaced” are represented by infeasibility of the augmented simplex point, a unique extension and projection preserving $w$, and equivalence of greatest attained $w$ values, respectively.

The mission does not formalize the derivation of (2) from (1) by simplex pivots, dual simplex reoptimization, finiteness of repeated cutting, the $m+n+2$ equation bound and deletion of re-entering $s$ variables, the suggested choice of largest fractional part, or the reported E101 runs. These concern an iterative process the note does not define fully, or empirical observations. Reusable contributions include a verified fractional part identity, the integer extension theorem, and solution set correspondence for a real tableau.

Selected references

• Ralph E. Gomory, Outline of an Algorithm for Integer Solutions to Linear Programs, Bulletin of the American Mathematical Society 64(5), 1958, 275–278. DOI: 10.1090/S0002-9904-1958-10224-4.
• George B. Dantzig, R. Fulkerson, and S. Johnson, Solution of a Large-Scale Traveling-Salesman Problem, Operations Research 2(4), 1954, 393–410. DOI: 10.1287/opre.2.4.393.

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

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

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

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.