Linear Optimization

Motivation

The assignment problem asks how to assign $n$ men to $n$ jobs, one man per job, so that the total cost (or, equivalently, the total rating) is optimal. It is the simplest combinatorial optimization problem with a nontrivial polynomial-time algorithm, and it appears as a subroutine across operations research: in transportation and network-flow methods, in tracking and data association, in scheduling, and as the relaxation behind branch-and-bound methods for the travelling salesman problem.

The algorithm studied here is the one now usually called the Hungarian method or Kuhn–Munkres algorithm.

• 1931: Kőnig and Egerváry prove the theorem on lines and independent zeros of a matrix that the method rests on.
• 1955: H. W. Kuhn gives the Hungarian method, with finiteness argued for integer matrices through a decreasing integer sum (Kuhn 1955). M. Flood restates it as Steps A–D.
• 1957: J. Munkres gives a fully specified version, in which Step B of Flood's outline (find a minimal set of lines containing all zeros and a maximal set of independent zeros) is carried out by an explicit marking procedure with starred and primed zeros. He proves it correct, shows that the integrality assumption is unnecessary, and bounds the work by a polynomial in $n$ (Munkres 1957).

The mission formalizes Munkres' correctness proof for §1 of that paper.

Setting

Let $A=(x_{ij})$ be a real $n\times n$ matrix, $x_{ij}$ being the cost of assigning man $i$ (row $i$) to job $j$ (column $j$). A set of entries is independent if no two of them lie in the same line (row or column). An assignment is a permutation $\sigma$, with $\sigma(r)$ the man doing job $r$. Its cost is $\sum_r x_{\sigma(r)\,r}$, and $\sigma$ is an optimal assignment if this cost is at most that of every permutation $\tau$. Choosing $n$ independent entries of minimum sum is the same as choosing an optimal assignment.

The algorithm. A state of the algorithm holds the current matrix, a set of starred zeros $0^*$, a set of primed zeros $0'$, a set of covered rows and a set of covered columns. An entry is non-covered, once-covered or twice-covered according as it lies in zero, one or two covered lines.

• Preliminaries. Subtract from each row its smallest element, then from each column its smallest entry. Consider the zeros in turn and star each one that has no starred zero in its row or column. Cover the columns containing a $0^*$.
• Step 1. Prime a non-covered zero. If its row contains no $0^*$, go to Step 2. Otherwise cover its row and uncover the column of that $0^*$. When no non-covered zero remains, go to Step 3.
• Step 2. Build the alternating sequence $Z_0,Z_1,\dots,Z_{2k}$. It starts at the $0'$ just found. Each $Z_{2i+1}$ is the $0^*$ in the column of $Z_{2i}$, each $Z_{2i+2}$ is the $0'$ in the row of $Z_{2i+1}$, and the sequence stops at a $0'$ with no $0^*$ in its column. Unstar its starred zeros and star its primed zeros. Erase all primes, uncover all rows and cover the columns containing a $0^*$. Stop if all columns are covered; otherwise return to Step 1.
• Step 3. Let $h$ be the smallest non-covered element. Add $h$ to each covered row, subtract $h$ from each uncovered column, and return to Step 1 with all marks kept.

The quantity $n_k$, the maximal number of independent zeros of the matrix $A_k$, measures progress.

Formalization targets

Goal: correctness of the algorithm

For every real $n\times n$ matrix $A$:

$$\exists\,\text{start};\quad \text{every run is finite};\quad \text{no reachable non-final state is stuck};\quad \text{at a final state } \{0^*\}=\{(\sigma(r),r)\}\ \text{with}\ \sum_r x_{\sigma(r)r}=\min_\tau \sum_r x_{\tau(r)r}.$$

The four clauses are needed together: optimality at final states alone holds for an algorithm that never stops.

Milestones

1. Remark (2): subtracting row constants $u_i$ and column constants $v_j$ does not change the optimal assignments.
2. The zeros starred in the Preliminaries are independent.
3. At Step 2 the sequence $Z_0,\dots,Z_{2k}$ exists, is unique and has distinct elements.
4. Step 2 leaves an independent set of starred zeros, larger by one.
5. Lines containing all the zeros number at least the maximal number of independent zeros.
6. At Step 3 the starred zeros are a maximal independent set and the covered lines a minimal cover.
7. At Step 3, $h>0$; the transformation subtracts $h$ from non-covered entries, adds $h$ to twice-covered ones, keeps every $0^*$ and $0'$ a zero, and $n_{k+1}\ge n_k$.
8. If $n_{k+1}=n_k$, Step 2 does not occur before the next Step 3, which begins with more covered rows.
9. While $n_k$ is constant, Step 3 is applied at most $n$ times.
10. Every row and column of the matrix always contains a zero.
11. Step 3 decreases the sum of the entries by $n(n-n_k)h$.

Significance

Correctness of the Hungarian method is the basis of a standard algorithm for the assignment problem and, through it, of methods for transportation problems, minimum-cost bipartite matching and weighted bipartite matching. Its $O(n^3)$ refinements remain in practical use. The invariants of the proof are the primal–dual structure of the problem: the row and column constants subtracted along the way form a dual solution, and the starred zeros at the end are a primal solution satisfying complementary slackness.

The result has been proved since 1957 and is in every textbook on combinatorial optimization. A machine-checked version of Munkres' specific procedure, as a transition system with all its free choices, with finiteness for real (not only integer) matrices, is not available on this platform; Mathlib has no assignment algorithm. The mission produces a verified specification of the algorithm, reusable invariants about covers and independent zeros, and a termination argument that does not rely on integrality.

Difficulty

Optimality at termination is short once the invariants are known. The work lies in two places.

First, the invariants hold only along runs. "Each $0^*$ is covered by precisely one line", "no column contains more than one $0^*$" and "no row contains more than one $0'$" fail for arbitrary marked matrices, so they must be carried as an inductive invariant through every move, including the Step 3 transformation, which keeps the primes.

Second, termination. The obvious measure, the sum of the entries, decreases by $n(n-n_k)h$ at each Step 3, but for real entries $h$ can be arbitrarily small, so the decreasing sum gives no bound on the number of steps. The page replaces this argument by the stronger result of p. 35 (milestone 8), which holds for real entries. Turning it into a proof that every run of the nondeterministic move relation is finite, including the moves inside Step 1 and Step 2, is the core of the formalization.

Formalization scope

• Matrices and positions. Entries are arbitrary reals, as on p. 35. Positions are Fin n × Fin n (row, column).
• Output orientation. The output permutation follows the published definition HeldWolfeCrowder_Assignment_Setting: σ r is the row assigned to column r, the starred positions are $(\sigma(r),r)$, and optimality is IsOptimalAssignment A σ with respect to the original input matrix.
• Nondeterminism. The algorithm is an inductive move relation Step. The order in which the Preliminaries consider the zeros, and the non-covered zero primed in Step 1, are free choices. Every claim holds for every run.
• Relational steps. Step 2's sequence and Step 3's $h$ are described relationally. Their existence, and $h>0$, are theorems, not built into the moves.
• Reachable states. Invariants are stated for states reachable from a start state, never for arbitrary states.
• Finiteness. Finiteness of every run is accessibility (Acc) of each start state for the reversed move relation.
• Termination test after the Preliminaries. "If all columns are covered, stop" is also applied when leaving the Preliminaries. The page goes to Step 1 unconditionally there. If the Preliminaries already star $n$ zeros, Step 3 would then have no non-covered element.
• Independent zeros. The maximal number of independent zeros is a finite maximum of cardinalities, so it has no junk value.
• Edge case $n=0$. No positivity of $n$ is assumed. For $n=0$ the start state is final.
• Ruled out. A goal stating only optimality at final states, or invariants stated for arbitrary states, would be a trivializing formalization; the goal states termination of every run and absence of stuck states as well.

Not formalized: the operation count $(11n^3+12n^2+31n)/6$ of pp. 35–36, whose cost model is informal; the argument that returning to the standard input after Step 3 is unnecessary (pp. 34–35); König's theorem (Remark (1), cited); and §2 on the transportation problem, which is stated without proof.

Welcome contributions: proofs of the milestones, a general library of lines and independent zeros in matrices (reusable for König–Egerváry), and an executable refinement of the move relation.

Selected references

• J. Munkres, Algorithms for the assignment and transportation problems, J. Soc. Indust. Appl. Math. 5 (1957), 32–38. https://doi.org/10.1137/0105003
• H. W. Kuhn, The Hungarian method for the assignment problem, Naval Research Logistics Quarterly 2 (1955), 83–97. https://doi.org/10.1002/nav.3800020109
• M. Held, P. Wolfe, H. P. Crowder, Validation of subgradient optimization, Mathematical Programming 6 (1974), 62–88. https://doi.org/10.1007/BF01580223 (source of the published assignment-cost definitions reused here)

Motivation

A finite Markov decision system asks how to choose actions while a changing state controls which actions are available. The choice can affect both the reward now and the distribution of future states. In a total-reward problem, the process can continue indefinitely; if transitions are substochastic, it can also terminate. Kallenberg's treatment of positive dynamic programming connects this control problem to a finite linear program and uses an optimal flow to identify a policy that is optimal from every initial state Kallenberg, Chapter 3.

The connection matters when an optimizer is easier to compute as state-action frequencies than as an infinite sequence of decisions. A policy may depend on the entire observed history and may randomize at every decision. The theorem under study says that, when the dual linear program has an extreme optimal solution, its positive coordinates identify a pure stationary policy as good as every such general policy. This assertion includes models in which the selected policy is not transient Kallenberg, Theorem 3.5.2 and Example 3.5.1.

Setting

Let $E=\{1,\ldots,N\}$ be a nonempty finite state space. At state $i$, one chooses an action from the nonempty finite set $A(i)$. Action $a\in A(i)$ earns a real reward $r_{ia}$ and moves to state $j$ with probability $p_{iaj}\ge0$. The sum $\sum_jp_{iaj}$ is at most one; any missing probability represents termination. Positive dynamic programming imposes $r_{ia}\ge0$ for every admissible state-action pair Kallenberg, Section 2.2 and Assumption 3.5.1.

A policy $R=(\pi^1,\pi^2,\ldots)$ assigns an action distribution after each finite history. The history records the initial state and all states and actions observed so far. Write $C$ for this full policy class. A pure stationary policy $f^\infty$ always chooses one fixed admissible action $f(i)$ whenever it visits $i$.

Starting from state $i$, let $v_i(R)$ be the expected total reward of $R$, and let $v_i=\sup_{R\in C}v_i(R)$. Because the rewards are nonnegative, the finite-horizon expected totals increase to $v_i(R)$; both policy and optimal values may be $+\infty$. A real vector $w=(w_i)$ is TMD superharmonic if $w_i\ge r_{ia}+\sum_jp_{iaj}w_j$ for each $i$ and $a\in A(i)$ Kallenberg, Definition 3.3.1.

For given weights $\beta_j>0$, equation (3.5.2) is a linear program over nonnegative state-action flows $x_{ia}$. It maximizes $\sum_{i,a}r_{ia}x_{ia}$ subject to

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

The set $E_x=\{i:\sum_{a\in A(i)}x_{ia}>0\}$ records the states with positive flow Kallenberg, Notation 3.1.1 and equation (3.5.2).

Formalization targets

Superharmonic value

Theorem 3.5.1 identifies $v$ as the smallest nonnegative TMD-superharmonic vector. The original superharmonic definition ranges over real vectors; the value must also be allowed to take $+\infty$. The formal statement gives both the extended superharmonic inequalities for $v$ and its componentwise bound by every nonnegative real superharmonic vector:

$$0\le v_i,\qquad v_i\ge r_{ia}+\sum_jp_{iaj}v_j,\qquad v_i\le w_i\quad\text{for every nonnegative real superharmonic }w.$$

This is the numbered milestone of the mission Kallenberg, Theorem 3.5.1.

Policy from an extreme optimal dual flow

The main goal is Theorem 3.5.2. Suppose $x^*$ is an extreme point of the feasible region of (3.5.2) and has objective at least as large as every feasible flow. Then every pure stationary rule $f$ choosing $x^*_{i,f(i)}>0$ on $E_{x^*}$, with arbitrary admissible actions outside $E_{x^*}$, is total optimal:

$$v_i(f^\infty)=v_i=\sup_{R\in C}v_i(R)\qquad(i\in E).$$

The goal records the finite-optimum case by requiring an actual optimal solution $x^*$; it makes no extra assumption that every policy is transient Kallenberg, Theorem 3.5.2.

Significance

The theorem converts an extreme optimal state-action flow into one decision rule that is optimal simultaneously for all starting states. Since $C$ includes policies that change with time, use full histories or randomize, it establishes that those freedoms cannot improve the total-reward value when the stated dual optimizer exists. The positive model also reveals when extended values matter: outside the finite-optimum case, the dual objective may be unbounded and an optimal total reward may be infinite Kallenberg, pp. 78–83.

A formal development of this result must keep the policy class and the linear program in the same model. It provides reusable definitions of a finite substochastic control system, finite-history probabilities, extended total rewards, state-action flows and superharmonic vectors. The result is proved in the book; the mission asks for a machine-checked proof of its statement, not for a new optimization theorem. The draft statements are open goals until such proofs are supplied.

Difficulty

A finite linear program has finitely many variables, while the value compares a flow-derived rule with every infinite, history dependent policy. A comparison restricted to stationary or transient policies would miss the main assertion. The proof also has to treat zero-flow states: the dual solution does not prescribe an action there, yet the theorem permits every admissible choice. Finally, the superharmonic milestone permits an infinite value, while the linear program itself uses real coordinates. A development must connect those representations without turning an infinite reward into an arbitrary default real value.

Formalization scope

Lean represents states as Fin N with $N>0$, and each $A(i)$ as a nonempty finite subset of a finite action type. The transition rows sum to at most one. Histories carry past states and actions, and the first action has internal index zero, corresponding to the book's time one. Policy probabilities are nonnegative, vanish outside $A(i)$ and sum to one. The expected reward of a finite horizon is a finite sum over histories; nonnegative total reward is its supremum in EReal. The value takes the supremum over the full policy type, not over a restricted policy subclass.

Dual flow coordinates exist only for admissible state-action pairs. Extreme points are taken in the feasible set of (3.5.2) in those coordinates, and its balance constraints retain the source's $\le\beta_j$ direction. The goal quantifies over every admissible pure rule satisfying the positive-flow condition. These choices exclude the vacuous shortcut of defining the value using only pure stationary policies or assuming optimality as a hypothesis.

The mathematical infrastructure includes finite policy histories, state-action occupancy probabilities, extended nonnegative reward limits, the real flow polyhedron and its extreme points. The history and flow definitions can support later work on other finite decision models. Contributions to those foundational results and to the full comparison with history dependent policies are within the mission's scope. The negative-reward regime of Section 3.6, whose claims involve average optimality and recurrent classes in an extended stochastic model, requires its own representation and is outside this positive-reward target.

Selected references

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

Motivation

Finite group equations arise when an integer program is expressed relative to an integer basis: the residue of a candidate solution in a finite Abelian group records whether it satisfies the original integrality requirement. Gomory's group polyhedron collects the nonnegative integer solutions with one prescribed residue. Its faces give valid linear inequalities for the group relaxation, so a description of those faces is useful to anyone studying integer programming cuts or the geometry of integer hulls. Gomory's 1969 paper develops the group equation and its polyhedra in this setting and then gives a finite system for the faces of the largest, or master, polyhedron. Gomory 1969, pp. 457–458, 474, 480–483.

The main question is how to recognize a facet inequality without ranging over every nonnegative integer solution of the group equation. The paper's Theorem 7 characterizes facets through a system with one row for each integer solution, an infinite collection in general. Theorem 18 replaces that family by rows determined by pairs of group elements and a rank condition at the candidate coefficient vector. Gomory 1969, pp. 469–470, 481–483.

Setting

Let $\mathcal G$ be a finite Abelian group with zero $0$, and let $\mathcal G^+=\mathcal G\setminus\{0\}$. For a subset $\mathcal N\subseteq\mathcal G^+$ and a right-hand side $g_0\in\mathcal G$, a group-equation solution is a nonnegative integer vector $t\in\mathbb N^{\mathcal N}$ satisfying

$$\sum_{g\in\mathcal N}t(g)g=g_0.$$

The set of solutions is $T(\mathcal G,\mathcal N,g_0)$, and the group polyhedron $P(\mathcal G,\mathcal N,g_0)$ is their convex hull in the real coordinate space $\mathbb R^{\mathcal N}$. The master polyhedron $P(\mathcal G,g_0)$ uses $\mathcal N=\mathcal G^+$. This mission concerns $g_0\ne0$; Gomory specifies a separate convention at $g_0=0$, excluding the zero solution from that master polyhedron. Gomory 1969, pp. 457–458, 474–475.

Gomory calls $\pi\cdot x\ge\pi_0$ a face when $\pi\ne0$, all points of $P$ satisfy the inequality, and its tight points generate the entire hyperplane $\pi\cdot x=\pi_0$ by affine combinations. Thus "face" means a facet of full hyperplane dimension here. The equivalent integer-point criterion uses the tight members of $T$, which is the representation adopted in Lean. A basic feasible solution of a linear system satisfies every equation and inequality and has tight rows whose coefficient vectors span the full variable space. Gomory 1969, pp. 468–469.

Formalization targets

The path to the goal starts with the sign of the face coefficients, the infinite-system characterization, and the shortest-path interpretation. An integer vector $t$ represents a path whose total group displacement is $\sum_g t(g)g$ and whose length is $\pi\cdot t$. The shortest-path statements lead to subadditivity and complementary equalities for face coefficients. For $P(\mathcal G,g_0)$, Theorem 17 collects the row conditions needed for the final system. Gomory 1969, pp. 469–473, 480–481.

The target is Theorem 18. Fix $g_0\ne0$ and $\pi_0>0$. With $\pi(0)=0$, system (13) is

$$\begin{aligned} \pi(g_0)&=\pi_0,\\ \pi(g)+\pi(g_0-g)&=\pi_0 &&(g\in\mathcal G^+,\ g\ne g_0),\\ \pi(g)+\pi(h)&\ge\pi(g+h) &&(g,h\in\mathcal G^+),\\ \pi(g)&\ge0 &&(g\in\mathcal G^+). \end{aligned}$$

The goal asserts the full equivalence

$$\pi\cdot x\ge\pi_0\text{ is a face of }P(\mathcal G,g_0) \quad\Longleftrightarrow\quad \pi\text{ is a basic feasible solution of (13).}$$

The equation rows, ordered pair rows, and nonnegativity rows all count toward basicness; $\pi_0$ is held fixed. Gomory 1969, pp. 481–483, Theorem 18.

Significance

Theorem 18 turns a geometric property defined against infinitely many integer vectors into a finite test in $|\mathcal G|-1$ coefficient variables. A solver can check its displayed equations and inequalities and then check whether the tight row vectors have full rank. That gives a concrete route to enumerating the facet coefficient vectors of $P(\mathcal G,g_0)$ for a fixed finite group, the use Gomory reports immediately after the proof. Gomory 1969, p. 483.

The result was proved in the paper; the work here is to formalize that known theorem and the numbered results it uses. The group-solution model, the integer-point facet criterion, and the generic tight-row definition of basic feasibility can also support other group-polyhedron arguments. The local prior-art search found related formalizations of facets and polyhedra, but none with the same integer-point-generated hyperplane and finite-group conventions, so these definitions are stated for this paper's objects.

Difficulty

Validity of the rows of (13) for a face does not by itself establish Theorem 18. Basicness requires the tight rows to span all $|\mathcal G|-1$ coefficient directions, and the converse must turn that rank information into enough tight integer solutions to generate a hyperplane. A supporting inequality that is tight at only a smaller face would pass a mere feasibility check while failing Gomory's face definition. The shortest-path results connect the group equations to the coefficient restrictions, but do not erase the rank requirement. Gomory 1969, pp. 468–470, 472–473, 481–483.

Formalization scope

Lean uses a finite Abelian group and a Finset $\mathcal N$ of nonzero elements. Its real vectors have coordinates indexed by $\mathcal N$ itself, with no unconstrained zero coordinate. The group equation is a finite sum of natural-number multiples in $\mathcal G$; $P$ is the real convex hull of the cast integer solutions. A face requires a nonzero normal, validity on every integer solution, and equality between the affine span of tight integer points and the entire hyperplane. This excludes the trivial reading that merely asks for one tight point. It also makes an empty solution set incapable of supplying a face. Theorem 7 assumes $\mathcal N$ nonempty ($n'\ge1$), as the paper does implicitly: with no coordinates every vector would be trivially basic.

Paths are represented by their nonnegative integer arc-multiplicity vectors. The same vector can describe several arc orders, but the length and group displacement used here depend only on multiplicity. Shortestness is stated by comparison with every competing vector of the same displacement; no infimum with an empty-set default is used. The complement and subadditivity rows of (13) use $\pi(0)=0$, and the subadditivity rows include ordered pairs with equal entries. Basic feasible solutions use the span of tight coefficient rows, including equation rows, in the full real space of $|\mathcal G|-1$ variables.

The mission includes the paper's Theorems 6, 7, 10, 17, Lemmas 1–2, and both numbered corollaries on p. 473 as milestones. Contributions that establish the affine-span and rank equivalences, or reusable finite-group shortest-path and polyhedral lemmas, directly advance the target. Theorems for $g_0=0$ and for other sections of the paper are outside this mission's stated domain.

Selected references

• R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra and Its Applications 2 (1969), 451–558. DOI: 10.1016/0024-3795(69)90017-2.

Why semi-Markov control matters

A decision maker may choose an action whenever a system changes state, even though the time until the next change is random. Maintenance and replacement decisions are examples: a repair choice changes both the next operating state and the length of time before another choice is available. A discrete-time Markov decision model gives every decision epoch the same duration. A semi-Markov decision process allows the holding time to depend on the current state, action, and next state. Kallenberg's Chapter 7 develops discounted and average-reward versions of this finite-state model, including a characterization of optimal discounted value through inequalities and a linear program (Kallenberg 1983, Chapter 7).

The mission focuses on the discounted part of that chapter. The result is known: Kallenberg proves it as Theorem 7.2.1. The formalization task is to state and eventually prove the result for the same policy class and the same general holding-time distributions. Those details matter because a stationary-policy-only version would omit the comparison that the theorem makes with all admissible policies.

Model and notation

Let $E$ be a nonempty finite state set. Each $i\in E$ has a finite nonempty set $A(i)$ of available actions. If action $a\in A(i)$ is chosen, the next state is $j$ with probability $p_{iaj}\geq0$, with $\sum_jp_{iaj}=1$. Conditional on $j$, the nonnegative time until that transition has distribution $F_{iaj}$. The action earns a lump reward $r_{ia}$ immediately and a reward rate $s_{ia}$ during the ensuing sojourn. Neither the holding-time laws nor the reward rates are required to be identical across transitions (Kallenberg 1983, pp. 210–212).

Fix a positive continuous discount rate $\lambda$. The factor applied after elapsed time $t$ is $e^{-\lambda t}$. Assumption 7.2.1 requires the Laplace–Stieltjes transform of each conditional holding-time law to satisfy

$$L_{iaj}(\lambda):=\int_0^\infty e^{-\lambda t}\,dF_{iaj}(t)<1 \qquad(i,j\in E,\ a\in A(i)).$$

The assumption is strict for every triple; it does not require a particular parametric family. Define the one-epoch expected discounted reward and discounted transition entry by

$$r^*_{ia}=\sum_jp_{iaj}\int_0^\infty \left(r_{ia}+s_{ia}\int_0^t e^{-\lambda u}\,du\right)dF_{iaj}(t), \qquad p^*_{iaj}=p_{iaj}L_{iaj}(\lambda).$$

A policy $R$ is a sequence of randomized decisions. At each epoch its choice may depend on every previously observed state and chosen action and the current state. It does not observe previous sojourn times when choosing. Let $v_i^\lambda(R)$ be the expected sum of discounted lump and rate rewards from initial state $i$, as in equation (7.2.1). The DRD value vector is $v_i^\lambda=\sup_R v_i^\lambda(R)$, with the supremum over this full policy class. A real vector $w$ is DRD-superharmonic when

$$w_i\geq r^*_{ia}+\sum_jp^*_{iaj}w_j \qquad(i\in E,\ a\in A(i)).$$

These are Kallenberg's Definitions 7.2.1 and 7.2.2 (p. 214).

Formalization targets

Goal: the smallest superharmonic vector

Theorem 7.2.1 states that the value vector itself satisfies the superharmonic inequalities and lies below every other vector satisfying them:

$$v^\lambda\text{ is DRD-superharmonic},\qquad w\text{ is DRD-superharmonic}\Longrightarrow v_i^\lambda\leq w_i\quad(i\in E).$$

This is the mission goal. Its content includes both clauses: merely showing that every superharmonic vector bounds policy rewards would leave out the assertion that the value is superharmonic.

Supporting results

Lemma 7.2.1 expresses $v_i^\lambda(R)$ as a sum of expected discounted state-action occupancies. Theorem 7.2.2 says that a feasible action choice attaining equality in the value equation at every state yields an optimal pure stationary policy. Theorem 7.2.3 says that positive support in an optimal solution of the dual linear program (7.2.11) yields such a policy. Their statements and exact conditions are the mission's milestones (Kallenberg 1983, pp. 212, 216–217).

What the results provide

The goal turns a supremum over possibly history-dependent randomized policies into a finite system of inequalities indexed by available state-action pairs. The next two results explain how equality in those inequalities and an optimal linear-programming solution identify a pure stationary policy with the same value. Thus the finite programs are statements about the original semi-Markov process rather than a separate discounted matrix model (Kallenberg 1983, pp. 214–217).

Kallenberg supplies paper proofs. This mission supplies Lean statements and a shared model interface; the proposed theorem items still require machine-checked proofs. The model's arbitrary conditional holding-time measures, its distinction between the current reward and future discounted value, and its history-dependent policy class are reusable for other finite semi-Markov arguments. The average-reward section of Chapter 7 is outside this mission.

Main difficulty

The straightforward finite-state discounted equation concerns expected one-step rewards. The source value, however, is defined from rewards earned at random physical times, and a policy can react to its entire discrete history. Identifying these two descriptions requires accounting for the joint state, action, and elapsed-time law without giving the policy access to past holding times. Holding times may equal zero with positive probability; the strict transform assumption excludes a degenerate law concentrated entirely at zero, but it does not make each holding time strictly positive. A second issue is real-valuedness: all-policy suprema and integrals must represent the finite quantities in the source rather than Lean's default values on ill-posed inputs.

Formalization scope

Lean uses finite types for states and actions, with a nonempty available-action finset for each state. Conditional sojourn laws are probability measures on $\mathbb R$ with no mass on negative times. This includes arbitrary distributions on $[0,\infty)$ and permits an atom at zero. The model stores stochastic transition rows, lump rewards, and rate rewards. The discounted layer stores $\lambda>0$ and the source's strict per-triple transform inequality. The expected one-epoch reward uses a Lebesgue integral against each sojourn law.

Policy decision rules read a list of past state-action pairs and the current state. Finite-horizon value recursively integrates the original epoch reward and its holding-time discount; policy value is its limit. The coordinatewise supremum ranges over all such policies. The occupation sum of Lemma 7.2.1 is a separate theorem, not the definition of policy value. A proof must establish convergence and boundedness from Assumption 7.2.1 so that Lean's total limit, integral, and real-supremum operations have their intended meanings.

The dual program sums only over actions available in each state and uses strictly positive weights $\beta_j$, equality flow constraints, and nonnegative variables as printed. Its pure stationary selector must choose an available action with positive dual mass in every state. Contributions establishing the occupation identity, value bounds, Bellman inequalities, or dual decoding all fit the mission.

Selected references

• L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983, Chapter 7, pp. 210–227. Publisher repository.

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