Motivation

In the cutting stock problem, stock rolls of length $L$ are cut into pieces of lengths $l_1,\dots,l_m$ to fill orders. Part I of Gilmore and Gomory's work (Opns. Res. 9 (1961)) solved its linear programming relaxation by the simplex method with column generation: the columns (cutting patterns) are too many to list, so each simplex iteration finds an improving column by solving a knapsack problem. Part II (Opns. Res. 11 (1963)) extends the method in several directions. One of them, customer tolerances, lets the amount produced of each length lie in a range $[N_i',N_i'']$ instead of matching a fixed demand. Total roll usage then stops being a good measure of quality, because overproducing within the tolerance is free. The natural objective becomes the fraction of waste: total waste divided by total material cut. This objective is a ratio of two linear functions, not a linear one.

The paper's answer, on p. 882, is that the ordinary simplex method still works for such an objective. It moves from vertex to vertex, at each vertex asks whether some edge improves the objective, and stops when none does. Ratio objectives of this kind, called linear-fractional programs, were studied in the same years by Isbell and Marlow (1956), Martos (1960–61, in Hungarian; in English in 1964), Charnes and Cooper (1962) and Dinkelbach (1962; see also 1967). Gilmore and Gomory say that their method is closest to Martos's. They derive the edge test for the ratio and show that, for cutting stock, choosing the entering column is again a knapsack problem.

Setting

Let $A$ be a real $m\times n$ matrix, $b\in\mathbb R^m$ and $c,d\in\mathbb R^n$. The linear-fractional program is

$$\text{minimize}\quad \zeta(x)=\frac{z_1(x)}{z_2(x)}=\frac{\sum_i c_ix_i}{\sum_i d_ix_i}\qquad\text{subject to}\quad Ax=b,\ x\ge 0 .$$

In the cutting stock instance (p. 881), column $j$ is either a cutting pattern $a_j\in\mathbb Z^m_{\ge0}$ with $\sum_ia_{ij}l_i\le L$ or a slack column $-e_i$. The right-hand side is $b_i=N_i'$. The numerator coefficient of a pattern is its waste $w_j=L-\sum_ia_{ij}l_i$ (eq. (4)), and $d_j=1$ on patterns and $0$ on slacks, so $\zeta$ is waste per roll cut. The paper drops the upper bounds $s_i\le N_i''-N_i'$ on the slacks from the discussion (p. 882), and so does this mission.

A basis is a set $B$ of $m$ column indices whose columns of $A$ are linearly independent. A basic feasible solution $\bar x$ with basis $B$ is a feasible point with $\bar x_k=0$ for every $k\notin B$. For a nonbasic $j\notin B$, the edge direction of $x_j$ is the vector $v$ with $Av=0$, $v_j=1$ and $v_k=0$ for the other nonbasic $k$. This is "the edge that would be traced out if $x_j$ were increased, but all other nonbasic variables kept zero" (p. 883). The quantity the simplex test inspects is the rate of change along the edge,

$$\frac{d\zeta}{dx_j}=\frac{d}{d\tau}\,\zeta(\bar x+\tau v)\Big|_{\tau=0}.$$

Formalization targets

Goal: the edge criterion (p. 882)

Assume $\sum_id_ix_i>0$ for every feasible $x$. Let $\bar x$ be a basic feasible solution with basis $B$, and suppose $d\zeta/dx_j\ge0$ for every $j\notin B$ and every edge direction of $x_j$. Then

$$\zeta(\bar x)\le\zeta(x)\qquad\text{for every } x\ge0 \text{ with } Ax=b .$$

Milestones (p. 882–883)

1. Monotonicity along lines. On an interval where the denominator does not vanish, $\tau\mapsto\zeta(x+\tau v)$ is strictly increasing, strictly decreasing or constant. Moreover $f'(\tau)\,D(\tau)^2$ is constant, where $D$ is the denominator.
2. Equation (5), first line.

$$\frac{d\zeta}{dx_j}=\frac{z_2\,(dz_1/dx_j)-z_1\,(dz_2/dx_j)}{z_2^2}.$$

3. The edge test. If $d\zeta/dx_j<0$, increasing $x_j$ strictly decreases $\zeta$ along any segment where the denominator does not vanish. Otherwise $\zeta$ does not decrease anywhere on that segment.
4. Column choice is a knapsack problem. With $k=Lz_2-z_1$ and $\bar\Pi_i=-(z_1\Pi^2_i-z_2\Pi^1_i-z_2l_i)$, the numerator of $d\zeta/dx_j$ for pattern $a$ equals $k-\sum_i\bar\Pi_ia_i$. Hence, for $z_2\ne0$, the most negative $d\zeta/dx_j$ is attained exactly by the patterns maximizing $\sum_i\bar\Pi_ia_i$ subject to $\sum_ia_il_i\le L$.

Significance

The result. The edge criterion turns a nonconvex problem into one the simplex method solves. A ratio of linear functions is neither convex nor concave, so a point where no feasible direction improves the objective locally is not obviously a global minimum. The criterion says that, on a polyhedron where the denominator keeps its sign, this local test at a vertex certifies global optimality, exactly as for a linear objective. It underlies the convergence of Martos's method and of every simplex-type algorithm for linear-fractional programming. Together with milestone 4, it is what makes column generation with a knapsack pricing step applicable to the waste-fraction objective of cutting stock.

Formalizing it. The result is classical and proved; no machine-checked version is known to exist. The published platform items closest to it are Derman's Charnes–Cooper transformation of a linear-fractional program into a linear program and Matoušek's reduced-cost optimality criterion for a linear objective. Neither states an edge criterion for a ratio. A formal proof here also settles the paper's own imprecisions (see below), and yields reusable lemmas about ratios of affine functions along lines.

Difficulty

The obvious argument does not reach the goal. Along any single segment the objective is monotone (milestone 1), so a nonnegative derivative at $\bar x$ in the direction of the segment would settle it. But the test at $\bar x$ inspects only the $n-m$ edge directions, while a feasible point $x$ lies in the direction $x-\bar x$, which is in general not an edge. Monotonicity along each edge says nothing directly about other directions, and $\zeta$ is neither convex nor concave, so local optimality along a few lines does not by itself transfer to the whole polyhedron. The step that has to be supplied is the passage from the edges to all feasible directions at a basic solution. It fails without the basis: at a feasible point that is not basic, or with linearly dependent columns, the edge directions need not reach every feasible point. At a degenerate vertex some edge directions leave the feasible set at once, and a test restricted to the feasible edges does not certify optimality.

Formalization scope

The feasible set and the objective are the published definitions DermanSeqDecisions.LinProg.IsFeasible11 ($x\ge0$, $Ax=b$) and DermanSeqDecisions.LinProg.fracObj ($(\sum c_ix_i)/(\sum d_ix_i)$). The basis is the published MatousekLP.BFS.IsBasis. Indices are 0-based. A mission definition adds the basic feasible solution and the relational edge direction. The edge direction is given by its defining equations, not through a basis inverse, and is not required to be feasible.

Committed conventions and disclosed choices:

• The goal is stated for minimization, the paper's problem; the paper's sentence says "maximize", which is the same statement for $-c$.
• "In a domain where the denominator does not vanish" is the hypothesis $\sum_id_ix_i>0$ for every feasible $x$ (the paper's footnote: $\sum_jx_j>0$). It is not required on all of $\mathbb R^n$, where it would be unsatisfiable for the cutting stock $d$.
• The derivative in the test is Mathlib's deriv of $\tau\mapsto\zeta(\bar x+\tau v)$ at $0$: the actual rate of change, not a formula assumed to equal it.
• The page says that along a line the derivative "will have the same value". This is false when the denominator varies along the line. Milestone 1 states the correct version: the derivative times the squared denominator is constant, so the sign is constant.
• In the formula after substituting (4), the page prints the coefficient $-l_i$ where $-z_2l_i$ is meant. Milestone 4 uses the corrected coefficient.
• The slack upper bounds are dropped, as on p. 882.

The following would trivialize the goal and are excluded: an edge hypothesis over all directions $v$ instead of the edge directions, which turns the goal into quasi-convexity along segments; an edge hypothesis stated as the global inequality; a positivity hypothesis on the denominator over all of $\mathbb R^n$; and dropping the basis, under which the goal is false.

The development needs elementary real calculus (derivatives of quotients, monotonicity from the sign of the derivative) and the linear algebra of a basis (existence, uniqueness and spanning of the edge directions). The lemmas about ratios of affine functions along lines and about edge directions of a basis are reusable for any simplex-type method. Contributions of proofs of the milestones, and of auxiliary lemmas on edge directions, are welcome.

Selected references

• P. C. Gilmore and R. E. Gomory, A linear programming approach to the cutting stock problem—Part II, Operations Research 11(6), 863–888, 1963. https://doi.org/10.1287/opre.11.6.863
• P. C. Gilmore and R. E. Gomory, A linear programming approach to the cutting stock problem, Operations Research 9(6), 849–859, 1961. https://doi.org/10.1287/opre.9.6.849
• B. Martos, Hyperbolic programming, Naval Research Logistics Quarterly 11(2), 135–155, 1964. https://doi.org/10.1002/nav.3800110204
• A. Charnes and W. W. Cooper, Programming with linear fractional functionals, Naval Research Logistics Quarterly 9(3–4), 181–186, 1962. https://doi.org/10.1002/nav.3800090303
• W. Dinkelbach, Die Maximierung eines Quotienten zweier linearer Funktionen unter linearen Nebenbedingungen, Zeitschrift für Wahrscheinlichkeitstheorie 1, 141–145, 1962 (cited by the paper as [11]).
• W. Dinkelbach, On nonlinear fractional programming, Management Science 13(7), 492–498, 1967. https://doi.org/10.1287/mnsc.13.7.492
• J. R. Isbell and W. H. Marlow, Attrition games, Naval Research Logistics Quarterly 3, 71–94, 1956 (cited by the paper as [9]).

Motivation

Chordal graphs (graphs in which every long cycle has a shortcut edge) appear wherever a sparse symmetric structure has to be eliminated without creating new interactions: Gaussian elimination on sparse symmetric matrices (Rose 1970), acyclic database schemes, junction trees for probabilistic graphical models, and phylogenetic and scheduling problems. In all of these applications the useful object is not the graph itself but a tree representation of it: a tree on which every vertex of the graph is a connected piece, and adjacency is overlap.

The theorem of this mission says that such tree representations exist exactly for chordal graphs. It extends the theory of interval graphs (intersection graphs of intervals on a line, i.e. of subpaths of a path), whose characterization was asked by Hajós (1957) and given by Lekkerkerker–Boland (1962), Gilmore–Hoffman (1964) and Fulkerson–Gross (1965), from paths to arbitrary trees.

Timeline. Dirac (1961) proved that every chordal graph has a simplicial vertex, a vertex whose neighbourhood is a complete subgraph. Rose (1970) used this to recognize chordal graphs efficiently, and Gavril (1972) showed that a chordal graph has at most as many maximal cliques as vertices. Renz (1970) studied intersection graphs of arcs in trees. Gavril (1974), together with Buneman (1974) and Walter (1972/1978) independently, proved that the intersection graphs of subtrees of trees are exactly the chordal graphs, and gave an algorithm that builds such a representation.

Setting

All graphs are finite and simple: a graph $G$ has a finite vertex set $V$ and a symmetric irreflexive adjacency relation. A completely connected set is a set of pairwise adjacent vertices, and a clique is a maximal completely connected set. The set of cliques of $G$ is $\mu(G)$, and $\mu_v(G) \subseteq \mu(G)$ is the set of cliques containing the vertex $v$. For a vertex $v$, $\Gamma v$ is the set of its neighbours; $v$ is simplicial if $\Gamma v$ is completely connected.

$G$ is chordal if every simple circuit $v_1, \dots, v_k, v_1$ with $k > 3$ vertices has a chord: an edge of $G$ joining two vertices of the circuit that are not consecutive on it.

A tree $T$ is a connected graph without simple circuits. A subtree of $T$ is a nonempty set of tree vertices that induces a connected subgraph of $T$. A family $(\bar v)_{v \in V}$ of subtrees of $T$ represents $G$ if, for all distinct $u, v \in V$,

$$u \sim_G v \iff \bar u \cap \bar v \neq \varnothing.$$

$G$ is a subtree graph if it has such a representation on some tree, and a proper subtree graph if it has one in which no subtree is contained in another.

Formalization targets

Goal: Theorem 3 (p. 51)

$$G \text{ is a subtree graph} \iff G \text{ is chordal}$$

for every finite simple graph $G$. The paper calls this "the main theorem of this paper".

Milestones

1. The three-point remark (p. 50): subtrees of a tree that each contain two of three given points have a common point.
2. Lemma 1 (p. 50): for every completely connected set $A$ of a subtree graph, $\bigcap_{v \in A} \bar v \neq \varnothing$.
3. For two different cliques $A_1 \neq A_2$, $\big(\bigcap_{v\in A_1}\bar v\big) \cap \big(\bigcap_{v \in A_2} \bar v\big) = \varnothing$ (p. 50).
4. Theorem 2 (p. 51): $G$ is a subtree graph if and only if there is a tree $T$ with vertex set $\mu(G)$ such that $T(\mu_v(G))$ is connected for every $v \in V$ (a clique tree).
5. Subtree graphs are chordal (proof of Theorem 3, p. 51).
6. Dirac–Rose (cited, p. 48): every nonempty finite chordal graph has a simplicial vertex.
7. For a simplicial vertex $v$, $\{v\} \cup \Gamma v$ is a clique (p. 52).
8. Induced subgraphs of chordal graphs are chordal (p. 52).
9. Every finite chordal graph has a clique tree (pp. 51–52).

Companion statements (§3 and §1)

$$G \text{ subtree graph} \implies G \text{ proper subtree graph}, \qquad \text{subtree} \iff \text{proper subtree} \iff \text{chordal},$$

and, cited on p. 49, $|\mu(G)| \le |V|$ for a nonempty finite chordal graph.

Significance

The result. The theorem turns a forbidden-structure condition (no chordless cycle of length at least four) into a constructive geometric one (a tree model), and Theorem 2 makes the tree canonical: its vertices are the maximal cliques. Clique trees are the data structure behind junction-tree inference, multifrontal sparse Cholesky factorization, and dynamic programming over tree decompositions; the treewidth of a graph is defined through chordal supergraphs and their clique trees. The proper-subtree result of §3 shows a contrast with interval graphs, where proper interval graphs form a strictly smaller class.

Formalizing it. The theorem is classical and fully proved in the literature, but Mathlib has no notion of chordal graph, no Helly property for subtrees, no clique trees and no simplicial-vertex theorem. This mission produces those definitions together with the characterization, the Helly property for finite families of subtrees, the Dirac–Rose theorem under the cycle–chord definition, and closure of chordality under induced subgraphs. As far as is known, none of these results has a machine-checked proof in Lean under the cycle–chord definition.

Difficulty

The "only if" direction is short on paper but rests on tree facts that are not packaged in Mathlib: a connected vertex set of a tree contains the unique path between any two of its vertices, and three pairwise paths of a tree meet. The "if" direction must produce a tree on the set $\mu(G)$ of maximal cliques, and the maximal cliques of a graph are not stable under passing to induced subgraphs: a clique of a subgraph need not be a clique of $G$, and two cliques of $G$ may restrict to the same set. Relating $\mu(G)$ to $\mu(G_1)$ for a smaller graph $G_1$ is the step where informal arguments are routinely loose, and it is where a formal proof spends most of its effort. The Dirac–Rose theorem is cited rather than proved in the paper and needs a separate development.

A tempting shortcut is to define chordality as the existence of a perfect elimination ordering. This builds the Dirac–Rose theorem into the definition and changes the theorem being proved; it is excluded here.

Formalization scope

• Graphs are G : SimpleGraph V with [Fintype V] in the goal, Theorem 2, the clique-tree claim, Dirac–Rose and the clique count. Milestones whose claims hold for infinite graphs (Lemma 1 for finite $A$, the three-point remark, the clique-disjointness claim, subtree ⇒ chordal, induced chordality, the simplicial clique, subtree ⇒ proper subtree) are stated without finiteness, which makes them stronger. $V$ may be empty in the goal and in Theorem 2; Dirac–Rose and the clique count assume $V$ nonempty, which they need.
• Chordality is the cycle–chord definition: for every cycle walk c of length at least 4 there are vertices x, y on c with G.Adj x y and s(x, y) not an edge of c.
• The paper's trees are topological and its subtrees connected closed portions that may end inside an edge. Here a tree is a combinatorial tree T : SimpleGraph β with T.IsTree (not necessarily finite), and a subtree is a vertex set s with (T.induce s).Connected; subdividing the topological tree at all end-points shows the class of subtree graphs is the same. The tree type lives in the same universe as V.
• The representing family is indexed by V; adjacency is compared only for distinct vertices. A clique is Maximal G.IsClique s; $\mu(G)$ is the subtype of such sets.
• Two trivializing formalizations are ruled out: chordality as a perfect elimination ordering, and representations by sets that need not be connected (with arbitrary sets every graph is an intersection graph, and the "only if" half would be false).
• Needed infrastructure: paths and connected sets in trees, Helly's property for subtrees, maximal cliques and their behaviour under induced subgraphs, and simplicial vertices. The tree lemmas and the Dirac–Rose theorem are reusable well beyond this mission. Proofs of any milestone, alternative routes (for example via perfect elimination orderings proved equivalent to the cycle–chord definition), and the clique-count bound are all welcome.

Selected references

• F. Gavril, Algorithms for minimum coloring, maximum clique, minimum covering by cliques, and maximum independent set of a chordal graph, SIAM J. Comput. 1 (1972) 180–187. https://doi.org/10.1137/0201013
• F. Gavril, The intersection graphs of subtrees in trees are exactly the chordal graphs, J. Combin. Theory Ser. B 16 (1974) 47–56. https://doi.org/10.1016/0095-8956(74)90094-X
• G. A. Dirac, On rigid circuit graphs, Abh. Math. Sem. Univ. Hamburg 25 (1961) 71–76. https://doi.org/10.1007/BF02992776
• D. J. Rose, Triangulated graphs and the elimination process, J. Math. Anal. Appl. 32 (1970) 597–609. https://doi.org/10.1016/0022-247X(70)90282-9
• P. Buneman, A characterisation of rigid circuit graphs, Discrete Math. 9 (1974) 205–212. https://doi.org/10.1016/0012-365X(74)90002-8
• J. R. Walter, Representations of chordal graphs as subtrees of a tree, J. Graph Theory 2 (1978) 265–267. https://doi.org/10.1002/jgt.3190020311
• D. R. Fulkerson and O. A. Gross, Incidence matrices and interval graphs, Pacific J. Math. 15 (1965) 835–855. https://doi.org/10.2140/pjm.1965.15.835

Motivation

Commuters choose not only a route but also a departure time, trading travel delay against the penalty of arriving early or late. Static traffic assignment, in the tradition of Wardrop's user-equilibrium principle, ignores the time dimension; dynamic traffic assignment adds it, and its central modelling question is what "equilibrium" means when flows, delays and costs all vary over a time horizon. Friesz, Bernstein, Smith, Tobin and Wie (Oper. Res. 41(1), 1993) proposed the simultaneous route-departure (SRD) equilibrium of a path-based dynamic model and showed that it is equivalent to an infinite-dimensional variational inequality. That equivalence is the starting point of a large literature on dynamic user equilibrium: existence theory, solution algorithms and differential-variational formulations all take the variational inequality as their definition of the problem.

Timeline, as far as this mission is concerned:

• 1952: Wardrop states the static user-equilibrium criterion (equal and minimal travel times on used routes).
• 1979–1980: Smith and Dafermos formulate static user equilibrium as a finite-dimensional variational inequality.
• 1989: Friesz, Luque, Tobin and Wie treat dynamic route choice with a fixed departure schedule as an optimal-control problem.
• 1993: Friesz et al. (this paper) formulate simultaneous route and departure-time equilibrium and prove its equivalence with a variational inequality on $(L^2[0,T])^{|P|}$ (Theorem 2, p. 187).

Setting

A traffic network has a finite set $P$ of paths. Each path $p$ connects exactly one origin–destination (OD) pair $kl$; $P_{kl}$ denotes the paths of pair $kl$. Travellers depart during the horizon $[0,T]$, $T>0$, which carries Lebesgue measure $\nu$; "$\forall_\nu(t)$" means "for $\nu$-almost every $t\in[0,T]$".

A vector of departure-time densities $h=(h_p)_{p\in P}$ assigns to each path a square-integrable, almost everywhere nonnegative function $h_p$ on $[0,T]$: $h_p(t)$ is the rate at which travellers depart at time $t$ on path $p$. The set of such vectors is $H_+$. Each OD pair has a fixed travel demand $Q_{kl}$, and the feasible set is

$$\Lambda=\Big\{h\in H_+ : \sum_{p\in P_{kl}}\int_0^T h_p(t)\,d\nu(t)=Q_{kl}\ \text{for every OD pair } kl\Big\}.\qquad(38)$$

A cost operator gives the effective delay $C_p(t,h)\ge 0$ of departing at time $t$ on path $p$ when the densities are $h$: travel time plus a penalty for early or late arrival (13). Because densities are defined only up to null sets, the relevant lowest achievable cost on a path is an essential infimum,

$$\mu_p(h)=\operatorname{ess\,inf}\{C_p(t,h):t\in[0,T]\}=\sup\{x\in\mathbb R:\ \nu\{t: C_p(t,h)<x\}=0\},$$

and the lowest achievable cost for pair $kl$ is $\mu_{kl}(h)=\min_{p\in P_{kl}}\mu_p(h)$.

Definition 3. For $h\in\Lambda$ and a nonnegative vector $\mu=(\mu_{kl})$, the pair $(h,\mu)$ is an SRD equilibrium if for every OD pair $kl$ and every $p\in P_{kl}$:

$$h_p(t)>0\ \Rightarrow\ C_p(t,h)=\mu_{kl}\quad\forall_\nu(t),\qquad C_p(t,h)\ge\mu_{kl}\quad\forall_\nu(t).$$

No positive-measure set of travellers can lower its cost by switching route or departure time.

Formalization targets

Goal: Theorem 2 (PIE VIP)

For $h^*$ with nonnegative, square-integrable costs $C_p(\cdot,h^*)$:

$$\big(\exists\,\mu^*:\ (h^*,\mu^*)\ \text{SRD equilibrium}\big)\ \Longrightarrow\ h^*\in\Lambda\ \text{and}\ \sum_{p\in P}\int_0^T C_p(t,h^*)\,[h_p(t)-h^*_p(t)]\,d\nu(t)\ge 0\ \ \forall h\in\Lambda,\qquad(39)$$

and conversely, if $h^*\in\Lambda$ solves (39), then $(h^*,\mu(h^*))$ with $\mu^*_{kl}=\mu_{kl}(h^*)$ is an SRD equilibrium. The formal goal states the two directions as two conjuncts; the second names the equilibrium cost vector explicitly, which is stronger than an equivalence with an existential $\mu^*$.

Milestones

1. Lemma 2: a measurable function positive on a set of positive measure exceeds some $\varepsilon_0>0$ on a set of positive measure.
2. The pointwise inequality (42) at an equilibrium, and the necessity half of Theorem 2.
3. Condition (17) holds by construction for $\mu^*=\mu(h^*)$.
4. The positive-measure sets (44)–(46) and (47) produced by a failure of (16).
5. Feasibility (50) of the mass-shifted vector (48)–(49), the value bound (54), and the sufficiency half of Theorem 2.

Significance

The result. Theorem 2 converts an equilibrium defined by almost-everywhere complementarity conditions into a single variational inequality over a convex subset of a Hilbert space. This is what makes dynamic user equilibrium accessible to the general theory of variational inequalities: existence via monotonicity or compactness arguments, and projection-type algorithms in function space or after time discretization. The sufficiency half also identifies the equilibrium cost levels: they are the essential infima $\mu_{kl}(h^*)$, so the multiplier $\mu^*$ need not be found separately.

Formalizing it. The theorem is proved in the paper; no machine-checked version is known. A formal proof requires essential infima, the shifting of mass between paths on sets of prescribed measure (the paper cites Halmos, Proposition 41.2, for the nonatomicity of Lebesgue measure), and careful integrability bookkeeping. The development is a self-contained template for "complementarity conditions a.e. ⇔ variational inequality in $L^2$" arguments, which recur in continuous-time equilibrium models.

Difficulty

Necessity is routine once integrability is in place, though the paper's text asserts the per-path identity $\int_0^T[h_p-h^*_p]\,d\nu=0$, which is false; only the sum over $P_{kl}$ vanishes, and that suffices. Sufficiency is the substantive half. The obvious approach, testing (39) against a perturbation that moves flow from an expensive to a cheap route, has to be carried out with sets rather than points: the costs are only defined almost everywhere, the minimal cost is an essential infimum that need not be attained at any time, and the perturbation must keep the demand constraints exact. This forces the choice of sets of exactly equal positive measure inside the positive-measure sets $S_p(\varepsilon,\delta)$ and $T_q(\varepsilon)$, a nonatomicity argument that a pointwise proof would miss.

Formalization scope

Densities are plain functions $\mathbb R\to\mathbb R$ with a square-integrability condition with respect to $\nu=$ Lebesgue measure restricted to $[0,T]$, not $L^2$ equivalence classes; every pointwise condition is $\nu$-almost everywhere, and values outside $[0,T]$ are unconstrained. Paths and OD pairs are finite types, with a map sending each path to its OD pair. The essential infimum is the literal formula (12), a real supremum; it is not the pointwise infimum, which changes when $C$ is altered on a null set and makes sufficiency false. $\mu_{kl}$ is a real infimum over $P_{kl}$; for a pair with no paths it is an unused default value.

The cost operator C is abstract, with the paper's measurability assumption strengthened to square-integrability so that every integral in (39) is a genuine Lebesgue integral. The network dynamics (3)–(11) that produce C in the paper are not formalized. Nonnegativity (the codomain $\mathbb R_+$ of (13)) and square-integrability are assumed only at $h^*$, which makes the formal statements stronger than the paper's. Without integrability, Lean's integral of a non-integrable function is $0$, so (39) could hold vacuously; the added hypothesis excludes that trivialization. The goal quantifies over every cost operator satisfying these hypotheses and never fixes one. In the milestones, the reduction from $p=q$ to $p\ne q$ (p. 188) is taken as the hypothesis $p\ne q$.

A complete development needs: properties of the real essential infimum (12) on a finite measure space; Lemma 2 (continuity of measure from below); the existence of measurable subsets of prescribed measure in Lebesgue measure (nonatomicity, available in Mathlib in some form); and integral bookkeeping for products of $L^2$ functions on a finite measure. The essential-infimum and mass-shift lemmas are reusable for other continuous-time equilibrium models. Proofs of any milestone, and cleaner restatements of the essential-infimum API, are welcome.

Selected references

• T. L. Friesz, D. Bernstein, T. E. Smith, R. L. Tobin and B. W. Wie, A variational inequality formulation of the dynamic network user equilibrium problem, Operations Research 41(1):179–191, 1993. https://doi.org/10.1287/opre.41.1.179
• J. G. Wardrop, Some theoretical aspects of road traffic research, Proceedings of the Institution of Civil Engineers 1(3):325–362, 1952. https://doi.org/10.1680/ipeds.1952.11259
• M. J. Smith, The existence, uniqueness and stability of traffic equilibria, Transportation Research B 13(4):295–304, 1979. https://doi.org/10.1016/0191-2615(79)90022-5
• S. Dafermos, Traffic equilibrium and variational inequalities, Transportation Science 14(1):42–54, 1980. https://doi.org/10.1287/trsc.14.1.42
• T. L. Friesz, J. Luque, R. L. Tobin and B. W. Wie, Dynamic network traffic assignment considered as a continuous time optimal control problem, Operations Research 37(6):893–901, 1989. https://doi.org/10.1287/opre.37.6.893
• P. R. Halmos, Measure Theory, Van Nostrand, 1950 (Proposition 41.2, nonatomicity of Lebesgue measure).

Motivation

The Chinese postman problem, posed by Meigu Guan (Kwan Mei-Ko) in 1962, asks for a shortest closed walk in a graph that traverses every edge at least once: the route of a postman who must cover every street and return to the post office. It is the basic model of arc routing (street sweeping, snow ploughing, meter reading, inspection of networks), and it is one of the first combinatorial optimization problems shown to be solvable in polynomial time by matching methods.

Edmonds and Johnson, Matching, Euler tours and the Chinese postman (Mathematical Programming 5, 1973), reduce the postman problem to a parity problem: choose nonnegative integers $x_e$, the number of extra traversals of each edge, so that every node becomes even, at minimum total length. Their §3 gives a complete linear description of this parity problem. The description is the first instance of what is now called the $T$-join polyhedron (with $T$ the set of odd-degree nodes), a standard object of polyhedral combinatorics and a frequent example of total dual integrality.

Timeline:

• 1962: Guan states the postman problem and an optimality criterion for it.
• 1965: Edmonds proves the matching polyhedron theorem and gives the blossom algorithm for weighted matching (Edmonds 1965).
• 1973: Edmonds and Johnson specialise both to the postman problem, giving the polyhedron in the edge variables alone (this mission) and a blossom algorithm that solves it (Edmonds–Johnson 1973).

Setting

A graph $G$ has a finite set $N$ of nodes and a finite set $E$ of edges; each edge meets two different nodes, and several edges may meet the same pair of nodes. The degree of a node $n$ is the number of edges meeting it, $\sum_{e\in E} a_{ne}$, where $a_{ne}=1$ if $e$ meets $n$ and $0$ otherwise. Set $b_n=1$ when the degree of $n$ is odd (an odd node) and $b_n=0$ otherwise.

An edge $e$ meets a set $S\subseteq N$ when exactly one of its two ends lies in $S$. A set $S\subseteq N$ is an odd set when it contains an odd number of odd nodes, and any number of even nodes.

The parity points $X\subseteq\mathbb R^E$ are the vectors with

$$x_e\in\mathbb Z,\quad x_e\ge 0\quad(e\in E),\qquad \sum_{e\in E}a_{ne}x_e\equiv b_n \pmod 2\quad(n\in N),$$

the conditions (3.1), (3.2), (3.6) of the paper. Adding $x_e$ copies of each edge $e$ to $G$ makes every degree even, and an Euler tour of the enlarged graph is a postman tour of $G$. The postman polyhedron is

$$P=\Big\{x\in\mathbb R^E:\ x_e\ge 0\ (e\in E),\ \ \sum\{x_e : e\text{ meets }S\}\ge 1\ \text{for every odd set } S\Big\},$$

the conditions (3.2) and (3.5). For lengths $c\in\mathbb R^E$ the objective is $z=\sum_e c_e x_e$. The dual linear program has a variable $y_S$ for each odd set, constraints $y_S\ge 0$ and $\sum\{y_S: e\text{ meets }S\}\le c_e$, and objective $v=\sum_S y_S$.

Formalization targets

Goal: the polyhedron theorem (p. 93)

$$\operatorname{conv} X = P .$$

Both inclusions are claimed. The equality is between subsets of $\mathbb R^E$, so it also asserts that the convex hull of $X$ is closed.

Milestones

In the paper's order of argument:

1. (3.13), p. 95: an integer solution of (3.6) has $\sum\{x_e : e\text{ meets }S\}\equiv 1 \pmod 2$ for every odd set $S$.
2. p. 95: $\operatorname{conv}X\subseteq P$.
3. (3.10), p. 94: weak duality, $v\le z$ for $x\in P$ and $y$ dual feasible.
4. (3.11)–(3.12), p. 95: complementary slackness makes $x$ and $y$ optimal.
5. p. 95: for $c\ge 0$ there is an integral parity point $x$ and a dual feasible $y$ satisfying (3.11) and (3.12). The paper proves this with the algorithm of §4.
6. p. 96: if some $c_e<0$, $z$ is unbounded below on $P$ and on $X$.
7. (3.19), p. 96: for $c\ge 0$, the minimum of $z$ over $P$ is attained at a parity point.

There are two companion statements. The first (pp. 93–94) says that in $\sum_e a_{ne}x_e-2w_n=b_n$ with $x\ge 0$, integrality of $w_n$ already forces $w_n\ge 0$. The second (p. 91) is the polyhedron theorem in the variables $(x,w)$: the convex hull of the integer solutions of (3.1)–(3.3) is the set of solutions of (3.2), (3.2′), (3.3), (3.5).

Significance

The theorem turns the parity problem, an integer program, into a linear program over an explicitly described polyhedron. Optimal postman tours therefore come with dual certificates: a packing of odd cuts whose total value matches the tour's extra length. The same description underlies the theory of $T$-joins and $T$-cuts (Schrijver 2003, Chapter 29).

No machine-checked proof of the $T$-join polyhedron theorem exists, on Prove2Me or, to our knowledge, in Mathlib. This mission states it in the multigraph setting of the paper. Milestones 1–4 and 6 are elementary and can serve as warm-ups. Milestone 5, total dual integrality of the odd-cut system, is the substantive step. The paper obtains it from a blossom algorithm; the milestone is stated as an existence result, so any proof of it closes it.

Difficulty

The inclusion $\operatorname{conv}X\subseteq P$ is a parity count. The reverse inclusion is the theorem. Two first ideas fail. Total unimodularity does not apply, because the odd-cut constraint matrix is not totally unimodular and $P$ has many constraints whose tightness interacts. Reading the result off the matching polyhedron theorem needs the auxiliary loops $w_n$ and an elimination step, and the 1965 matching polyhedron describes perfect matchings of a simple graph, not this parity system on a multigraph. Some argument for integrality of the minimum for every $c\ge 0$ is needed, and the paper's is an algorithm with a dual certificate. A further point is that $P$ and $X$ are unbounded: equality of hulls is not just agreement of minima over bounded objectives, and the case of objectives with a negative coefficient has to be handled separately (milestone 6).

Formalization scope

A graph is the local ChinesePostman.Polyhedron.Graph V E: a map ends : E → Sym2 V with a proof that no edge is a loop, over finite types V and E. Mathlib's SimpleGraph is not used, because the paper allows parallel edges. Degrees, odd nodes and $b_n$ are computed from the graph; the set of odd nodes is never a free parameter. "$e$ meets $S$" means exactly one end in $S$. Odd sets range over all subsets $S\subseteq N$ with an odd number of odd nodes, with no nonemptiness or properness condition. Parity points are real images of integer vectors E → ℤ, so integrality is part of $X$. Dual variables are functions Finset V → ℝ whose values matter only on odd sets: the sign condition and every sum are restricted to the odd sets. Lengths $c$ are arbitrary reals except where the page assumes $c_e\ge 0$ (milestones 5 and 7).

Trivializing readings are ruled out: (3.5) taken over nonempty proper sets only, "meets" read as "has at least one end in", the odd nodes taken as an arbitrary set $T$, or $X$ allowed to contain non-integral points would each give a different, and in some cases false or trivial, statement.

Every definition the statements need is in one file, ChinesePostman.Polyhedron.Setting. A complete development needs finite-dimensional convexity (Mathlib's convexHull) and linear programming duality or an integrality argument. A Lean proof of total dual integrality for odd-cut systems would be reusable for matching and $T$-join problems beyond this paper. Proofs of any milestone, and alternative proofs of milestone 5, are welcome.

Selected references

• J. Edmonds and E. L. Johnson, Matching, Euler tours and the Chinese postman, Mathematical Programming 5 (1973) 88–124. https://doi.org/10.1007/BF01580113
• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, Journal of Research of the National Bureau of Standards 69B (1965) 125–130. https://doi.org/10.6028/jres.069B.013
• M. Guan (Kwan Mei-Ko), Graphic programming using odd or even points, Chinese Mathematics 1 (1962) 273–277.
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003, Chapter 29 (T-joins and T-cuts). https://doi.org/10.1007/978-3-540-44389-6

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

Formalization targets

Goal: the column generation certificate

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

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

Selected references

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

Motivation

Fitting a probability distribution to prescribed margins or moments is a basic task in statistics and information theory. Starting from a reference distribution, one can enforce one constraint at a time by choosing the closest distribution in I-divergence, then cycle through the constraints. In a contingency table this procedure is iterative proportional fitting. A single projection onto the intersection is the desired answer, but each step of the iteration sees only one constraint set. Csiszár's 1975 paper proves that cyclic I-projections converge to the joint I-projection when the underlying set is finite and the constraint sets are linear. This mission formalizes that result together with the geometric statements needed to identify its limit.

Setting

Let $(X,\mathcal X)$ be a measurable space. A probability distribution (PD) is a probability measure on it. For PDs $P$ and $Q$, the I-divergence $I(P\|Q)$ is the Kullback–Leibler divergence: integrate the logarithm of the density of $P$ relative to $Q$ against $P$, with value $+\infty$ when $P$ is not absolutely continuous with respect to $Q$ or the integral diverges. It takes values in $[0,+\infty]$ and vanishes exactly when $P=Q$. The logarithmic conventions are $\log0=-\infty$ and $0\cdot(\pm\infty)=0$ (Csiszár 1975, (1.1)–(1.3)).

Given a PD $R$ and a set $\mathcal E$ of PDs that contains at least one $P$ with finite $I(P\|R)$, an I-projection $Q$ of $R$ onto $\mathcal E$ minimizes $I(P\|R)$ over $P\in\mathcal E$ and itself has finite divergence. The variation distance is the $L^1$ distance between the densities of two PDs relative to a common dominating measure. A set of PDs is linear here when every real affine combination of two members that is still a PD also belongs to the set. This includes distributions satisfying fixed linear moment constraints (Csiszár 1975, pp. 147 and 150–151).

For the goal, $X$ is finite. Choose $k\ge1$ linear sets $\mathcal E_1,\ldots,\mathcal E_k$, and write $\mathcal E=\bigcap_{i=1}^k\mathcal E_i$. Beginning with $Q_0=R$, let $Q_n$ be the I-projection of $Q_{n-1}$ onto $\mathcal E_i$ when $n=mk+i$ and $1\le i\le k$. The common feasible set is assumed nonempty and contains a PD absolutely continuous with respect to $R$. These assumptions ensure that the intended finite-divergence projection problem is present (Csiszár 1975, Theorem 3.2).

Formalization targets

The goal is the convergence statement of Theorem 3.2:

$$\forall x\in X,\qquad Q_n(\{x\})\longrightarrow Q(\{x\}), \quad Q=\operatorname{proj}^{I}_{\mathcal E}(R).$$

The goal also asserts existence of the cyclic sequence. On finite $X$, convergence of every point mass is equivalent to convergence in variation distance. The target fixes no rate. Its milestones include existence on variation-closed convex sets (Theorem 2.1), the identity (2.6) and the tangent-hyperplane Lemma 2.1, the Pythagorean characterization and transitivity of I-projections (Theorems 2.2–2.3), the density form under general linear constraints (Theorem 3.1) and the finite-moment exponential-density characterization (Corollary 3.1(A)), and the finite-space identity used in Theorem 3.2's proof. The two displayed identities in that proof are also targets:

$$I(Q\|R)=I(Q\|Q_n)+\sum_{i=1}^{n}I(Q_i\|Q_{i-1}),\qquad I(P\|Q_n)=I(P\|Q)+I(Q\|Q_n)\quad(P\in\mathcal E).$$

They specify the divergence relationships that the eventual convergence theorem must preserve (Csiszár 1975, (3.14)–(3.15)).

Significance

The theorem justifies enforcing finitely many linear distribution constraints one at a time while still obtaining the same I-projection as a simultaneous minimization. It gives a precise limit for the iterative proportional fitting procedure discussed by Csiszár, including cases in which the initial distribution has zero probabilities; strict positivity of $R$ is not required (Csiszár 1975, p. 155). The accompanying identities make the relation between a partial iterate and the final solution explicit. The result was proved in 1975. The work here is to provide machine-checked proofs of that known result and its supporting geometry, while keeping the source's extended-value and boundary conventions visible.

Difficulty

Successive projections minimize divergence over different sets. Minimization for one set by itself does not identify the minimizer over their intersection, and ordinary metric projection facts do not directly apply because I-divergence is asymmetric and can be infinite. The paper's statements need to handle zero densities and feasible distributions at infinite divergence without turning extended-real expressions into default values. On the finite space, convergence of a subsequence is available, but the formal claim must still identify every possible limit as the joint I-projection. These are the mathematical and representation difficulties faced by a complete proof (Csiszár 1975, §§2–3).

Formalization scope

Lean uses Measure X and Mathlib's InformationTheory.klDiv : ℝ≥0∞ for $I(P\|Q)$. A projection is a finite-divergence minimizer over the stated feasible set; no real-valued infimum or implicit arbitrary witness replaces it. Variation distance uses the densities relative to $P+Q$, which dominates both PDs and gives the value of (1.6). Variation closure is expressed by sequential convergence in this distance. The integral $\int\log q_R\,dP$ is represented in extended reals using positive and negative logarithmic parts and ENNReal.log; the theorem hypotheses keep the indeterminate $+\infty-(+\infty)$ case out. Density equations are $R$-almost everywhere, and a claim that $Q$ has an $R$-density explicitly includes $Q\ll R$.

For moment constraints, every integral is accompanied by integrability. Real affine combinations are tested through their values on measurable sets; the candidate combination must be a PD. The goal assumes a finite carrier with measurable singleton sets and $k\ge1$. Lean indexes the sets by Fin k from zero, so Qs (n+1) is projected onto the set at n % k; this is the paper's rule (3.13) shifted by one. The goal asserts existence of a recursive sequence before speaking about every such sequence, and the required feasible witness has $P\ll R$. These choices rule out an empty cyclic schedule, junk integrals, and a vacuous convergence assertion. Reusable contributions include the variation-distance and I-projection interfaces, their Pythagorean geometry, and the finite-moment density characterization; the mission's main closure remains Theorem 3.2.

Selected references

• I. Csiszár, I-Divergence Geometry of Probability Distributions and Minimization Problems, The Annals of Probability 3(1), 146–158 (1975). DOI: 10.1214/aop/1176996454.

Motivation

Delivering goods from one depot to many customers with a fleet of trucks is the vehicle routing problem. Dantzig and Ramser formulated it in 1959 as the "truck dispatching problem" (Management Sci. 6 (1959), doi:10.1287/mnsc.6.1.80). Five years later Clarke and Wright proposed the savings procedure (Oper. Res. 12 (1964), 568–581, doi:10.1287/opre.12.4.568): start with one truck per customer and repeatedly join two routes where joining saves the most distance, as long as the trucks can still carry the loads. On the twelve-customer example of Dantzig and Ramser it reached 290 units against their 294.

The savings procedure became the standard construction heuristic for vehicle routing. It appears in every textbook treatment of the problem, is the initial solution of many metaheuristics, and is the benchmark against which later construction methods are compared. The paper states the procedure and its bookkeeping (the half matrix, the vector $Q$, Table II) but proves nothing about it. That every run of the procedure ends, and ends in a feasible allocation, is left to the reader.

Setting

A depot $P_0$ serves customers $P_1,\dots,P_M$. The distance $d_{y,z}$ between every two points is given, and customer $P_j$ requires a load $q_j$. Trucks come in $n$ capacity classes: $x_i$ trucks of capacity $C_i$ are available, with $C_1<\dots<C_n$, and the trucks of the smallest capacity are unlimited, $x_1=\infty$ (p. 569).

A run is the ordered list of customers $P_{a_1},\dots,P_{a_k}$ served by one truck, which drives $P_0P_{a_1}\cdots P_{a_k}P_0$. Its load is $\sum_i q_{a_i}$. A state of the procedure is a list of runs; its mileage is the total length of its runs. A list of runs is an allocation if every customer lies on exactly one run, and it is feasible if each run can be given a truck of capacity at least its load without using more trucks of any class than are available.

The saving of the cell $(y:z)$ is $d_{0,y}+d_{0,z}-d_{y,z}$. The half matrix records $t_{y,z}=1$ if $P_y$ and $P_z$ are adjacent on a run, and $t_{y,0}\in\{0,1,2\}$ counts how many ends of runs lie at $P_y$. Table II counts, for each capacity level $C_i$, the runs with load above $C_i$ and the trucks with capacity above $C_i$.

The procedure starts with the runs $[P_1],\dots,[P_M]$, so $t_{y,0}=2$ for every customer. A cell $(y:z)$ is admissible if (I) $t_{y,0}>0$ and $t_{z,0}>0$; (II) $P_y$ and $P_z$ are on different runs; (III) after replacing those two runs by one run of load $Q_y+Q_z$, no column of Table II has more runs than trucks. A step links an admissible cell of maximum saving, ties broken arbitrarily, by joining the two runs end to end at $P_y$ and $P_z$. The procedure stops when no cell is admissible.

Formalization targets

Goal: correctness of the procedure

Assume symmetric distances, $C_1<\dots<C_n$, $x_1=\infty$, and that the initial one-truck-per-customer allocation passes the Table II test. Then every run of the procedure is finite whatever the tie-breaks; at every reachable state from which a link is possible a step exists; and every final state $S$ is a feasible allocation satisfying relation (A), $\sum_{z\ne y}t_{y,z}=2$ for every customer, with

$$\text{mileage}(S)=2\sum_{j=1}^M d_{0,j}-\sum_{\substack{1\le y<z\le M\\ t_{y,z}=1}}\bigl(d_{0,y}+d_{0,z}-d_{y,z}\bigr).$$

Milestones

$$\text{mileage}(\text{link}(S,y,z))=\text{mileage}(S)-(d_{0,y}+d_{0,z}-d_{y,z})\quad\text{for admissible }(y:z),$$

relation (A) at every reachable state, the permanence of links between customers, and

$$\#\{\text{runs with load}>C_i\}\le\sum_{k>i}x_k\ \ (i=1,\dots,n)\iff\text{the runs can be allocated to trucks},$$

which together give feasibility of every reachable state. Two further milestones: when $C_n\ge\sum_j q_j$ and the distances are a metric, the optimum equals the traveling salesman optimum (p. 569); and on the data of Table I every run of the procedure ends with total distance 290.

Significance

The goal is the specification the paper's procedure meets: it always terminates, never gets stuck, and outputs routes the fleet can actually drive, with the mileage the half-matrix bookkeeping predicts. The equivalence of the Table II test with truck feasibility is the reason the procedure can check capacities by counting columns instead of solving an assignment problem; it is a nested-class instance of Hall's marriage condition and is reusable for any routing or bin-assignment problem with ordered vehicle classes.

None of these statements is formalized anywhere, and the paper does not prove them. The paper makes no claim of optimality ("near-optimal", p. 568, is not quantified), and the mission does not either. A formal model of the procedure as a nondeterministic transition system is a base on which later results about savings heuristics (worst-case ratios, parallel and sequential variants) can be stated.

Difficulty

The obvious argument for termination, "each link removes a run", needs the invariant that every reachable state is a partition of the customers into runs; the procedure manipulates ordered lists and reverses runs, so the invariant must be carried through every step. Feasibility is not preserved by an arbitrary link but only by one that passes condition (III), and turning the column test into an actual assignment of runs to trucks is a matching argument that fails without both $x_1=\infty$ and the ordering of the capacities. Because ties are broken arbitrarily, every statement must hold for all runs of a nondeterministic procedure, not for one canonical execution. The worked example requires following every tie-break.

Formalization scope

Points are Fin (M+1) with depot 0, and a run's length is SupplyChainTheory.routeCost from the referenced module SupplyChainTheory_vrp. Capacity class i : Fin (n+1) is the paper's $C_{i+1}$; availabilities are in ℕ∞; loads and capacities are real. A state is a list of runs, each an ordered list of customers; the matrix $t$ and the vector $Q$ are computed from the state. The procedure is a step relation, and every invariant is stated for reachable states. Termination is Acc of the step relation at the initial state.

Choices committed to:

• distances are arbitrary real, symmetric numbers (the half matrix, p. 573); no nonnegativity or triangle inequality is assumed in the goal, and savings may be negative;
• every run: ties are free, as the paper suggests choosing randomly;
• reachable states: invariants are not claimed for arbitrary lists of runs;
• Table II is read cumulatively: column "Over $C_i$" compares runs with load $>C_i$ against all trucks of capacity $>C_i$, as the printed Tables II, IV and VI show;
• $x_1=\infty$ and $C_1<\dots<C_n$ are hypotheses; $q_j\le C_n$ is not separately assumed, since it follows from the initial Table II test;
• the initial one-truck-per-customer allocation is assumed feasible (p. 572);
• the metric hypotheses enter only the traveling-salesman milestone.

A correctness claim only about final states, without termination and progress, would hold for a procedure with no moves; a step relation with a fixed tie-break would prove less than the paper; invariants for arbitrary states are false; and a mileage identity for an arbitrary partition says nothing about the procedure's output. None of these is the target.

Not formalized: the informal $C_1\ll\sum q_j$, the shadow-cost reading of p. 571, the decomposition savings (2)–(5) of the general scheme, the load-splitting reduction of pp. 572–573, the Dantzig–Ramser methods, and the empirical comparisons and appendices.

Contributions welcome: proofs of the milestones, in particular the Table II equivalence, which needs a Hall-type argument for nested classes, and a decision procedure for the worked example.

Selected references

• G. Clarke and J. W. Wright, Scheduling of vehicles from a central depot to a number of delivery points, Operations Research 12(4) (1964), 568–581. https://doi.org/10.1287/opre.12.4.568
• G. B. Dantzig and J. H. Ramser, The truck dispatching problem, Management Science 6(1) (1959), 80–91. https://doi.org/10.1287/mnsc.6.1.80
• P. Hall, On representatives of subsets, Journal of the London Mathematical Society 10 (1935), 26–30. https://doi.org/10.1112/jlms/s1-10.37.26

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: correctness of the reduction

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

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

Milestones

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

Further statement

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

Significance

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

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

Difficulty

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

Formalization scope

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

Conventions committed to:

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

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

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

Selected references

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

Motivation

A Markov decision process with finitely many states and decisions, a discount factor $\beta\in(0,1)$ and the objective of minimizing expected discounted cost is the basic model of sequential decision making in operations research and reinforcement learning. It is solvable in polynomial time by linear programming. Papadimitriou and Tsitsiklis (Math. Oper. Res. 12(3), 1987) asked the finer question of whether it can be solved fast in parallel, and showed a sharp split: the general (stochastic) problem is P-complete (their Theorem 1), so it is unlikely to admit a polylogarithmic parallel algorithm, while the deterministic special case, where every transition probability is 0 or 1, is in NC (their Theorem 4).

The deterministic case is a shortest-path problem with a twist. Every policy traces a walk in a graph, and the cost of the walk counts its $t$-th arc with weight $\beta^t$. The paper's argument identifies the optimal discounted cost with the cost of a finite combinatorial object, a sigma, and computes it from discounted min-plus matrix products. This mission formalizes that identity.

Setting

A deterministic stationary Markov decision process consists of a finite set $S$ of $n$ states, an initial state $s_0\in S$, and for each state $s$ a finite nonempty set $D_s$ of decisions. Decision $i\in D_s$ costs $c(s,i)\in\mathbb R$ and leads with certainty to the state $\mathrm{next}(s,i)$. Equivalently, it is a directed graph on $S$ with an arc $s\to\mathrm{next}(s,i)$ of weight $c(s,i)$ for each decision; parallel arcs and loops are allowed.

A policy $\delta$ chooses a decision $\delta(s,t)\in D_s$ for every state $s$ and time $t=0,1,2,\dots$; it is stationary if $\delta(s,t)$ does not depend on $t$. From $s_0$ it produces the states $s_{t+1}=\mathrm{next}(s_t,\delta(s_t,t))$ and the discounted cost

$$J_\beta(\delta)=\sum_{t=0}^{\infty}\beta^t c\bigl(s_t,\delta(s_t,t)\bigr).$$

The optimal discounted cost is $J^*_\beta(s_0)=\inf_\delta J_\beta(\delta)$, the infimum over all policies $\delta(s,t)$.

A sigma is a walk $w_0=s_0,w_1,\dots,w_N$ along decisions $e_t\in D_{w_t}$ whose nodes $w_0,\dots,w_{N-1}$ are distinct and whose last node repeats an earlier one, $w_N=w_j$ with $j<N$: the walk from $s_0$ up to the first repetition of a node. It is a prefix of $j$ arcs followed by a cycle of $l=N-j\ge1$ arcs. Its discounted cost $c_\beta(P)$ is the discounted cost of the infinite walk that follows it and repeats its cycle forever.

In the min-plus semiring (addition is $\min$, multiplication is $+$, zero is $+\infty$), let $A_{uv}$ be the least cost of a decision from $u$ to $v$ ($+\infty$ if none), let $rA$ multiply every finite entry by $r$, and let

$$B_0=I,\qquad B_k=A\otimes\beta A\otimes\cdots\otimes\beta^{k-1}A ,$$

with $I$ the min-plus identity. The entry $(B_k)_{uv}$ is the least discounted cost $\sum_{t<k}\beta^t c_t$ of a $k$-arc walk from $u$ to $v$.

Formalization targets

Goal

For $0<\beta<1$,

$$J^*_\beta(s_0)=\min_{P\text{ sigma}}c_\beta(P)=\min\Bigl\{(B_k)_{s_0u}+\frac{\beta^{k}(B_l)_{uu}}{1-\beta^{l}}\;:\;u\in S,\ 0\le k\le n,\ 1\le l\le n,\ \text{both entries finite}\Bigr\},$$

with both minima attained. This is the claim on pp. 446–447 on which Theorem 4 rests. The algebraic expression is the corrected form of the paper's (see Formalization scope).

Milestones

1. The closed form of the cost of a sigma (p. 446): $c_\beta(P)=\sum_{t<j}\beta^tc_t+\frac{\beta^j}{1-\beta^l}\sum_{t<l}\beta^tc_{j+t}$.
2. A stationary optimal policy exists (§2, p. 444; cited on p. 446). The general finite stochastic statement is on the platform as BertsekasDP.discounted_main_theorem (Proved), and the deterministic case is stated in this mission's model.
3. The path of a stationary policy, cut at its first repeated node, is a sigma with the same discounted cost, and every sigma arises this way (p. 446).
4. The products $B_j$ are the cheapest discounted $j$-arc walks (p. 447).

Significance

The identity reduces an optimization over infinite objects, the time-dependent policies, to a minimum over finitely many closed-form expressions in matrix entries. Each $B_k$ is a product of $k$ min-plus matrices, and matrix products parallelize well; that is the source of the NC algorithm. The same reduction, with the discounting removed, underlies the minimum-mean-cycle characterization of the average-cost problem (mission II of this series), and the sigma structure reappears in the stationary finite-horizon analysis (mission IV).

On the formalization side, the result has been proved in the paper only as a short paragraph, which cites the existence of stationary optimal policies and leaves the algebra to the reader. Its printed formulas contain index slips (below). A machine-checked version fixes the exact constants. To our knowledge none of these statements has a formal proof. The existence of stationary optimal policies for finite discounted problems is formalized on the platform in Bertsekas's general stochastic setting.

Difficulty

The obvious argument says: an optimal policy may be taken stationary, a stationary deterministic policy produces an eventually periodic path, and an eventually periodic path is a sigma. The first step is the substantial one: the optimum is an infimum over all time-dependent policies $\delta(s,t)$, and a non-stationary policy can follow any walk at all, so this step is a statement about the whole dynamic program, not a combinatorial fact about a single walk. The second part of the goal adds a matching argument in the other direction: the expression ranges over arbitrary $k$-arc walks and closed $l$-walks, which need not be simple, so one must check that none of them beats the best sigma, and that the best sigma has $k\le n$ and $l\le n$. Finally, the discount factors must be tracked exactly; the printed formulas are off by one power of $\beta$ in two places.

Formalization scope

The Lean development lives in the namespace MDPComplexity.Discounted, with one definition file and five theorems. Conventions committed to:

• The model is stationary and deterministic. A DetMDP S has a finite state type, a nonempty finite decision type at each state (the paper says "a finite set $D_s$"; nonemptiness is implicit since a policy must choose a decision), a successor map and real costs.
• Policies are maps $\delta(s,t)$, time is $\mathbb N$ from $0$, and the optimum optDisc is the infimum over all such policies. Defining it over stationary policies or over sigmas would make the goal true by definition. That shortcut is ruled out, and the stationarity step is part of the content.
• Costs are tsums, which are junk ($0$) for non-summable series; every statement that sums costs assumes $0<\beta<1$, under which the series converge absolutely.
• A sigma is encoded as a lasso, $w_N=w_j$ with $j<N$. This includes $j=0$, a sigma whose cycle passes through $s_0$, which the printed form $(u_0,\dots,u_k,v_1,\dots,v_l,v_1)$ omits but the definition "a path from $u_0$ until the first repetition of a node" includes. The paper's $k$ is $j-1$.
• Corrected slips: (i) in the sigma display the cycle sum carries $\beta^{j-1}$, not $\beta^j$, for its $j$-th arc, and the indices are made consistent; (ii) the algorithm's expression is $\lambda+\beta^k\mu/(1-\beta^l)$ with $l\ge1$, not $\lambda+\beta^{k+1}\mu/(1+\beta^l)$ (one state with a loop of cost $1$ has optimum $1/(1-\beta)$, which the printed form misses); (iii) $B_0$, used but not defined, is the min-plus identity.
• Matrix entries are in Tropical (WithTop ℝ), so $+\infty$ is ⊤ and the product is Mathlib's matrix product over the tropical semiring.

Not formalized: membership in NC, the processor count $n^4$, the $\log^2 n+3\log n$ parallel time, and the P-completeness of the general problem. Mathlib has no parallel complexity classes. Only the identity that makes the algorithm correct is a target.

Contributions welcome: proofs of any milestone. A bridge from DetMDP to BertsekasSSPModel (taking decisions as controls and 0/1 transition rows) would let milestone 2 be derived from the platform's proved Proposition 7.3.1. A direct proof of the deterministic case is also welcome. The lasso and walk lemmas are reusable for the other missions of the series.

Selected references

• C. H. Papadimitriou and J. N. Tsitsiklis, The Complexity of Markov Decision Processes, Mathematics of Operations Research 12(3), 441–450, 1987. https://doi.org/10.1287/moor.12.3.441
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, §7.3 (discounted problems, Proposition 7.3.1).
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994, Ch. 6 (existence of stationary optimal policies for discounted models). https://doi.org/10.1002/9780470316887