Operations Research

Motivation

Shop scheduling asks how to process a set of jobs, each a sequence of tasks on prescribed machines, so that all work is completed as early as possible. The flow shop, in which every job visits the machines in the same order, is the most studied of these models in operations research. For two machines, Johnson's rule (1954) computes a schedule of minimum finish time in $O(n\log n)$ time, and for two machines allowing interruptions (preemption) does not help. Garey, Johnson and Sethi (Math. Oper. Res. 1976) and Brucker, Lenstra and Rinnooy Kan (Mathematisch Centrum report BW 43/75, 1975; Ann. Discrete Math. 1977) showed that the non-preemptive problem becomes NP-complete with three machines.

Gonzalez and Sahni (Operations Research, 1978) extended this picture to preemptive schedules. Their Theorem 1 shows that minimizing the finish time of a three-machine flow shop is NP-complete with or without preemption, even when every job has at most two tasks of nonzero length. When every job has only one task the problem is trivial, so this is the simplest NP-complete case of the flow-shop finish-time problem. The result explains why no exact polynomial algorithm is expected and motivates the approximation results in the second half of the same paper.

Timeline:

• 1954: Johnson, two-machine flow shop, optimal non-preemptive rule.
• 1975: Brucker, Lenstra, Rinnooy Kan: non-preemptive three-machine flow shop NP-complete, including the case of two nonzero tasks per job (the paper's Corollary 1, which it says "is also obtained in [1]").
• 1976: Garey, Johnson, Sethi: non-preemptive three-machine flow shop NP-complete even when the problem size is the sum of the task lengths.
• 1978: Gonzalez, Sahni: the preemptive three-machine flow shop is NP-complete, by a reduction from PARTITION that also covers the non-preemptive case with two nonzero tasks per job.

Setting

A flow shop has $m\ge1$ processors $P_1,\dots,P_m$ and a finite set of jobs. Task $j$ of job $i$ must be processed on $P_j$ for $t_{j,i}\ge 0$ time units, and it can start only after task $j-1$ of the same job is completed. Task times may be zero. The schedule starts at time $0$.

A preemptive schedule gives every task a finite set of pieces $(s,f)$ with $0\le s<f$: the task is processed on its processor during $[s,f)$. Pieces on the same processor do not overlap, the pieces of a task have total length $t_{j,i}$, and every piece of a task starts after every piece of the earlier tasks of the same job has ended. A non-preemptive schedule processes every task in at most one piece. For a schedule $S$, $f_i(S)$ is the time at which job $i$ is completed and the finish time is $\mathrm{FT}(S)=\max_i f_i(S)$.

PARTITION. A multiset $S=\{a_1,\dots,a_n\}$ of nonnegative integers has a partition if some set $u$ of indices satisfies $\sum_{i\in u}a_i=\tfrac12\sum_{i=1}^n a_i$.

The instance FS. With $T=\sum_i a_i$, the flow shop $\mathrm{FS}$ has $m=3$ processors and $n+2$ jobs:

$$t_{\cdot,i}=(a_i,0,a_i)\ (1\le i\le n),\qquad t_{\cdot,n+1}=(T/2,\,T,\,0),\qquad t_{\cdot,n+2}=(0,\,T,\,T/2),$$

and the threshold is $\tau=2T$. Every job has at most two nonzero tasks.

Formalization targets

Goal: Theorem 1 (p. 38)

For every $n$ and every $a_1,\dots,a_n\in\mathbb N$:

$$\mathrm{FS}\ \text{has at most two nonzero tasks per job},$$ $$\big(\exists\,S'\ \text{preemptive},\ \mathrm{FT}(S')\le 2T\big)\iff S\ \text{has a partition},$$ $$\big(\exists\,S'\ \text{non-preemptive},\ \mathrm{FT}(S')\le 2T\big)\iff S\ \text{has a partition}.$$

Milestones

• Lemma 1(a) (p. 39): a partition of $S$ yields a non-preemptive schedule of FS with $\mathrm{FT}=2T$ (Figure 1).
• Observations (i)–(ii) (p. 39): in any preemptive schedule with $\mathrm{FT}\le 2T$, task $t_{1,n+1}$ ends by $T$ and task $t_{3,n+2}$ starts no earlier than $T$.
• Lemma 1(b) (p. 39): if $S$ has no partition, every preemptive schedule of FS has $\mathrm{FT}>2T$.
• Lemma 1 (p. 38): the preemptive equivalence.
• Corollary 1 (p. 39): the non-preemptive equivalence.

Significance

The result. The equivalence shows that a polynomial-time algorithm deciding whether a three-machine flow shop (with two nonzero tasks per job) has a schedule of finish time at most $\tau$, preemptive or not, would decide PARTITION in polynomial time. With membership in NP (the paper's Lemma 2) it gives NP-completeness of both versions. It also marks the boundary with the polynomial cases: $m=2$ (Johnson's rule), and jobs with a single task.

Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge no machine-checked proof of this reduction exists, and the platform has no formal model of preemptive shop schedules. The mission produces one: a piece-based preemptive schedule with zero task times, which subsumes the non-preemptive case, together with the first formal NP-hardness reduction for preemptive flow shops on the platform.

Difficulty

Direction (a) asks for one explicit schedule. Direction (b) must rule out every preemptive schedule of FS, and preemption is exactly what makes this delicate: a task may be split into any finite number of pieces placed anywhere on its processor, so the naive intuition that a failed partition leaves "unusable gaps" is no longer evident, since pieces of different jobs can be interleaved to fill gaps. A correct argument must therefore be an accounting of processor time over the pieces, valid for any number and position of pieces, and it must treat zero-length tasks, which occupy no processor time but still delay the next task of their job. Finally, the non-preemptive equivalence is not a formal consequence of the preemptive one alone: it uses that (a) produces a non-preemptive schedule and that (b) holds for all preemptive schedules, which include the non-preemptive ones.

Formalization scope

• Processors are Fin 3 ($P_1,P_2,P_3$ = 0, 1, 2), jobs of FS are Fin n ⊕ Fin 2 (Sum.inr 0 is job $n+1$, Sum.inr 1 is job $n+2$). Task times are real numbers; the PARTITION data are a : Fin n → ℕ, and "has a partition" is $2\sum_{i\in u}a_i=\sum_i a_i$ in $\mathbb N$.
• A schedule is a Finset of pieces $(s,f)$ per task with the four conditions of the Setting. Non-preemptive means at most one piece per task. Zero tasks have no pieces and occupy no processor time. $f_i(S)$ and $\mathrm{FT}(S)$ are maxima with baseline $0$.
• Explicit constants: $T=\sum_i a_i$, the times $T/2$ and $T$ of jobs $n+1,n+2$, and the threshold $\tau=2T$, as on p. 39. Lemma 1(a) states finish time exactly $2T$, as the paper does.
• Not formalized: "NP-complete", the reducibility relation "$\alpha$", membership in NP (Lemma 2, p. 40) and the polynomial computability of FS from $S$. The paper states Theorem 1, Lemma 1 and Corollary 1 as complexity claims. Their proofs establish the equivalences above for the constructed instance, and those equivalences are what is formalized.
• No trivializing reading is admitted: the statements concern the specific instance FS built from $a$, not an arbitrary flow shop, and the schedule model rules out overlapping pieces and out-of-order tasks while still allowing zero tasks. A sorry-free check confirms that Figure 1 is a valid non-preemptive schedule of FS for $S=\{1,1\}$.
• Reusable beyond this mission: the flow-shop model with preemptive pieces, and PARTITION. Proofs of the milestones and a proof of the goal from them are welcome.

Selected references

• T. Gonzalez, S. Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1), 36–52, 1978. https://doi.org/10.1287/opre.26.1.36
• M. R. Garey, D. S. Johnson, R. Sethi, The Complexity of Flowshop and Jobshop Scheduling, Mathematics of Operations Research 1(2), 117–129, 1976. https://doi.org/10.1287/moor.1.2.117
• S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1), 61–68, 1954. https://doi.org/10.1002/nav.3800010110
• P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum report BW 43/75, 1975; Annals of Discrete Mathematics 1, 343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
• R. M. Karp, Reducibility among Combinatorial Problems, in Complexity of Computer Computations, Plenum, 85–103, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9

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

Every pure integer program, once its linear programming relaxation has been solved, can be relaxed further to a problem over a finite Abelian group: the nonbasic variables must satisfy a single congruence in the group of the optimal basis. R. E. Gomory introduced this relaxation in 1965 and studied the convex hull of its solutions in Some polyhedra related to combinatorial problems (Linear Algebra Appl. 2 (1969), 451–558, doi:10.1016/0024-3795(69)90017-2). The facets of these group polyhedra are valid inequalities for every integer program whose basis produces the same group, and they became the source of cutting planes for integer programming: Gomory's mixed-integer cut and the later theory of corner polyhedra and subadditive valid inequalities descend from them.

The number of facets grows fast with the order of the group, so a list of facets for each group is not a usable description. Section 3D of the paper, "Lifting up Faces", gives a structural tool instead: facets of the polyhedron of a small group produce facets of the polyhedron of every larger group that maps onto it. This mission formalizes that construction (THEOREM 19) and its converse (THEOREM 20).

Setting

Let $\mathcal G$ be a finite Abelian group, written additively, with zero $\bar 0$ and order $D=|\mathcal G|$, and let $\mathcal G^+=\mathcal G-\{\bar 0\}$. For a right-hand side $g_0\in\mathcal G$, the group equation asks for nonnegative integers $t(g)$, $g\in\mathcal G^+$, with

$$\sum_{g\in\mathcal G^+}t(g)\cdot g=g_0 .$$

Its solution set is $T(\mathcal G,g_0)$; when $g_0=\bar 0$, the zero solution is excluded, as stipulated on p. 474. Each solution is a point of $\mathbb R^{\mathcal G^+}$, a space of dimension $n'=D-1$, and the master polyhedron $P(\mathcal G,g_0)$ is the convex hull of $T(\mathcal G,g_0)$. Gomory reads a solution $t$ as a path from $\bar 0$ to $g_0$ that uses the element $g$ exactly $t(g)$ times; with arc lengths $\pi(g)$ its length is $\pi\cdot t=\sum_g\pi(g)t(g)$.

An inequality $\pi\cdot t\ge\pi_0$, written $(\pi,\pi_0)$, is a face of $P(\mathcal G,g_0)$ when $\pi\ne0$, every $t\in T(\mathcal G,g_0)$ satisfies it, and the solutions on the hyperplane $\pi\cdot t=\pi_0$ generate that hyperplane: every point of it is a weighted sum, with total weight 1, of such solutions. A face is therefore a facet; Gomory says "face" throughout, and so does this mission. The solutions with $\pi\cdot t=\pi_0$ are the minimal paths.

Let $\psi$ be a homomorphism of $\mathcal G$ onto a second finite Abelian group $\mathcal H$, with kernel $\mathcal K=\psi^{-1}(\bar 0)$. A coefficient vector $\pi'$ on $\mathcal H^+$ is lifted to $\mathcal G^+$ by

$$\pi(g)=\pi'(\psi g),\qquad \pi'(\bar 0)=0,$$

so that every element of the kernel gets coefficient $0$.

Formalization targets

Goal: THEOREM 19 (p. 486)

If $\psi g_0\ne\bar 0$ and $(\pi',\pi_0)$ is a face of $P(\mathcal H,\psi g_0)$ with $\pi_0>0$, then

$$\Big(\pi,\pi_0\Big),\quad \pi(g)=\pi'(\psi g),\quad\text{is a face of } P(\mathcal G,g_0).$$

For instance, the face $t_1\ge1$ of $P(\mathcal G_2,(1))$ lifts through reduction mod 2 to the face $t_1+0t_2+t_3+0t_4+t_5\ge1$ of $P(\mathcal G_6,(5))$ (p. 488).

Milestones

1. Face criterion (p. 469, proof of THEOREM 7). For $\pi_0>0$, $(\pi,\pi_0)$ is a face iff it is valid on $T$ and $n'$ linearly independent solutions satisfy $\pi\cdot t=\pi_0$.
2. Pushing paths forward (p. 486). A solution $t$ for $\mathcal G$ maps to the solution $\tau(h)=\sum_{g\in\psi^{-1}h}t(g)$ for $\mathcal H$ of the same length; hence the lifted inequality is valid.
3. Lifted minimal paths (p. 487). From a minimal path $\tau$ for $\mathcal H$ and a kernel element $k$, the path $T_k(\tau)$ is a minimal path for $\mathcal G$.
4. Rank $D-1$ (pp. 487–488). The lifted inequality has $D-1$ linearly independent minimal paths.

Further result: THEOREM 20 (p. 489)

Conversely, a face $(\pi,\pi_0)$ of $P(\mathcal G,g_0)$ with $\pi_0>0$ and $\pi(g)=0$ for some $g\ne\bar0$ is the lift of a face of $P(\mathcal H,\psi g_0)$ for some $\psi$ of $\mathcal G$ onto a group $\mathcal H$ with $\psi g=\bar 0$.

Significance

THEOREMS 19 and 20 together say that the faces of $P(\mathcal G,g_0)$ with $\pi_0>0$ and a zero coefficient are exactly the faces lifted from proper quotients of $\mathcal G$. A catalogue of these positive-right-hand-side faces therefore only needs the faces with all coefficients positive; the rest come from smaller groups. Gomory uses this to explain the tables of Appendix 5: for $\mathcal G_{2,2}$ and $\mathcal G_{2,2,2}$ every such face is a lift of the single nontrivial face of $P(\mathcal G_2,(1))$, and for a direct sum $\mathcal G=\mathcal K_1\oplus\mathcal K_2$ every face of the polyhedron of a summand not containing $g_0$ extends to a face for $\mathcal G$ (p. 489). The same idea, sending facets of one group problem to facets of another by a homomorphism, recurs in the later theory of group relaxations and infinite group problems.

Both theorems are proved in the paper. To the knowledge of this mission, neither the group polyhedra, their faces nor the lifting theorem has a machine-checked formalization; the platform's other "lifting" results (lifted cover facets of the knapsack polytope, cone lifts of convex sets) are different notions. The mission produces a reusable definition layer for master group polyhedra and their faces, stated once for an arbitrary finite Abelian group, and a formal version of the passage between faces of a group and of its quotients.

Difficulty

Validity of the lifted inequality is a one-line computation (milestone 2). The content is that the lift is a facet: one must exhibit $D-1$ affinely independent solutions on the hyperplane, while the quotient face only supplies $|\mathcal H|-1$ of them. A solution of the quotient problem does not determine a solution for $\mathcal G$; coset representatives must be chosen and the path closed by a kernel element, and the kernel coordinates, which all have coefficient zero, must still be filled to full rank.

The obvious reduction, "a facet pulls back to a facet under a surjective map", fails here because the map from $\mathcal G$-paths to $\mathcal H$-paths is a linear projection from dimension $D-1$ to $|\mathcal H|-1$ and does not lift independence by itself. It also fails at $\pi_0=0$: with $\mathcal G=\mathbb Z_6$, $\mathcal H=\mathbb Z_3$, $g_0=1$, the face $t(1)\ge0$ of $P(\mathbb Z_3,(1))$ lifts to $t(1)+t(4)\ge0$, which is valid but not a face of $P(\mathbb Z_6,(1))$.

Formalization scope

The formalization uses one definition file for an arbitrary finite Abelian group ([AddCommGroup G] [Fintype G] [DecidableEq G]), instantiated at both $\mathcal G$ and $\mathcal H$. It commits to the following readings:

• Vectors are indexed by the subtype $\{g\mid g\ne\bar0\}$, so $\bar0$ has no coordinate and the dimension of T-space is $|\mathcal G|-1$ for each group separately; solutions are $\mathbb N$-valued, nonzero, and cast to $\mathbb R$. When $g_0\ne\bar0$, the group equation already excludes the zero vector.
• "Generated by the points on the hyperplane" means that the affine span of the tight solutions equals the hyperplane $\{x:\pi\cdot x=\pi_0\}$; $\pi\ne0$ is part of the definition and $\pi_0\ge0$ is not (THEOREM 6 proves it).
• Paths are vectors and "minimal path" means a solution with $\pi\cdot t=\pi_0$.
• $\pi'(\bar0)=0$ is built into the lift; "onto" is Function.Surjective ψ, and $g_0\notin\mathcal K$ is $\psi g_0\ne\bar0$.
• Added hypothesis $\pi_0>0$ in THEOREM 19 and the rank milestone: the page omits it, and the $\mathbb Z_6\to\mathbb Z_3$ example above shows the statement is false without it.
• The face criterion is THEOREM 7's "basic feasible solution" unfolded into $n'$ linearly independent tight solutions, stated for the master polyhedron only and for nontrivial groups, where $n'>0$.
• Pushing a path forward uses $\psi g_0\ne\bar0$, the standing hypothesis of THEOREM 19, so the pushed path cannot become the excluded zero solution.
• The lifted path $T_k(\tau)$ puts its closing $1$ on the kernel element $g_0-\sum_{g\notin\mathcal K}t_k(g)\cdot g$ itself, and adds nothing when that element is $\bar0$.
• In THEOREM 20, "nontrivial" is $\pi_0>0$, the printed $(\pi_1,\pi_0)$ is read as $(\pi,\pi_0)$, and the conclusion requires $\psi g=\bar0$ for the given zero coefficient: without it the identity map would satisfy the statement.

A formalization that proves only validity of the lift, or that defines faces without the generation condition (so that every valid inequality is a "face"), would be trivial and is ruled out by the definition of IsFace.

The development needs finite sums over fibres of $\psi$, a choice of coset representatives, and a rank argument for a block matrix with full-rank diagonal blocks. The definitions of $T$, $P(\mathcal G,g_0)$ and face are reusable for any further result on master group polyhedra. Proofs of the milestones in any order, alternative proofs of the face criterion, and a proof of THEOREM 20 are welcome.

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
• R. E. Gomory, On the relation between integer and noninteger solutions to linear programs, Proceedings of the National Academy of Sciences 53 (1965), 260–265. doi:10.1073/pnas.53.2.260
• R. E. Gomory and E. L. Johnson, Some continuous functions related to corner polyhedra, Mathematical Programming 3 (1972), 23–85. doi:10.1007/BF01584976

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.