The OR Formalization Drive

Motivation

Minimum makespan scheduling on unrelated parallel machines, written $R\,||\,C_{\max}$, is one of the basic models of scheduling theory: $n$ jobs must each be run on one of $m$ machines, and the time a job takes depends arbitrarily on the machine. Lenstra, Shmoys and Tardos (CWI Report OS-R8714, 1987; journal version Math. Programming 46, 1990) gave a polynomial 2-approximation algorithm for this problem and, in the same paper, a matching limit from below: no polynomial algorithm can guarantee a factor smaller than $3/2$ unless $P = NP$ (their Corollary 2).

The two bounds have stood for more than three decades. Closing the gap between $3/2$ and $2$ for $R\,||\,C_{\max}$ is listed among the central open problems of approximation algorithms (Williamson and Shmoys, The Design of Approximation Algorithms, 2011, open problem on unrelated machines; Schuurman and Woeginger, Polynomial time approximation algorithms for machine scheduling: ten open problems, J. Scheduling 1999). The lower bound of $3/2$ is the subject of this mission.

Timeline:

• 1979: Graham, Lawler, Lenstra and Rinnooy Kan introduce the classification $R\,||\,C_{\max}$.
• 1987/1990: Lenstra, Shmoys and Tardos prove NP-completeness of deciding makespan at most 3 (Theorem 4, giving the bound $4/3$) and at most 2 (Theorem 5, giving $3/2$), both by reduction from 3-dimensional matching.
• Since then: the $3/2$ hardness bound has not been improved for general $R\,||\,C_{\max}$; progress has concentrated on special cases such as the restricted-assignment problem.

Setting

3-dimensional matching. There are three disjoint sets $A = \{a_1,\dots,a_n\}$, $B = \{b_1,\dots,b_n\}$, $C = \{c_1,\dots,c_n\}$ and a family $F = \{T_1,\dots,T_m\}$ of triples, each with one element of $A$, one of $B$ and one of $C$. A matching is a subfamily $F'$ with $|F'| = n$ whose union is $A \cup B \cup C$. In Lean an instance is a map $T : \mathrm{Fin}\,m \to \mathrm{Fin}\,n \times \mathrm{Fin}\,n \times \mathrm{Fin}\,n$, and HasMatching T says that a matching exists.

The scheduling model. Machines are $\mathrm{Fin}\,m$, jobs are $\mathrm{Fin}\,N$, and $p_{ij}$ is the positive integer processing time of job $j$ on machine $i$. A schedule $\sigma$ assigns each job to one machine; the load of machine $i$ is $\sum_{j:\sigma(j)=i} p_{ij}$ and the makespan $C_{\max}(\sigma)$ is the largest load. These are the published definitions MatousekLP.Scheduling.load and makespan.

The instance of Theorem 5. The triples containing $a_j$ are the triples of type $j$; let $t_j$ be their number. From $T$ the paper builds a scheduling instance with $m$ machines, machine $i$ corresponding to $T_i$, and with

1. $2n$ element jobs, one for each $b_k$ and each $c_l$;
2. $t_j - 1$ dummy jobs of type $j$, for each $j$.

If $T_i = (a_j, b_k, c_l)$, machine $i$ processes the element jobs of $b_k$ and $c_l$ in time $1$, each dummy job of type $j$ in time $2$, and every other job in time $3$. In Lean the processing-time matrix is P T.

A $\rho$-approximate schedule of an instance is a schedule $\sigma$ with $C_{\max}(\sigma) \le \rho\, C_{\max}(\tau)$ for every schedule $\tau$ of the same instance.

Formalization targets

Goal: Corollary 2 (p. 8)

For every instance $T$, every $\rho < 3/2$, and every $\rho$-approximate schedule $\sigma$ of the instance of Theorem 5 built from $T$,

$$C_{\max}(\sigma) \le 2 \iff T \text{ has a matching}.$$

This is the mathematical content of "for every $\rho < 3/2$ there is no polynomial $\rho$-approximation algorithm unless $P = NP$": a $\rho$-approximate answer on the reduced instance decides 3-dimensional matching.

Theorem 5 (p. 7)

For every instance $T$,

$$\exists\,\sigma:\ C_{\max}(\sigma) \le 2 \iff T \text{ has a matching}.$$

Milestones from the proof of Theorem 5 (pp. 7–8)

1. If every $t_j \ge 1$, then $\sum_j (t_j - 1) + n = m$: there are $m - n$ dummy jobs.
2. A matching yields a schedule with makespan at most $2$.
3. A schedule with makespan at most $2$ yields a matching.

Significance

The result. Theorem 5 shows that $R\,||\,C_{\max}$ is NP-hard already when every processing time lies in $\{1,2,3\}$ and the target makespan is $2$. Corollary 2 turns this into the best known inapproximability bound for the problem, $3/2$, which sits opposite the paper's own factor-2 algorithm. The same reduction pattern (machines as triples, dummy jobs that pin machines down) is reused in many later hardness proofs for scheduling and assignment problems.

Formalizing it. The result is proved on paper; no machine-checked version is known to exist. A formal proof requires the full combinatorial argument behind the reduction, including the counting of machines per type and the case where some element of $A$ lies in no triple, which the paper does not discuss. Together with mission 1 of this series (the factor-2 algorithm), it fixes both ends of the $[3/2, 2]$ gap in one formal library.

Difficulty

The construction is short, but the converse direction carries the weight: from an arbitrary schedule with makespan at most $2$ one must recover a matching, although nothing in the schedule singles out the triples that form it. The obvious first idea, to read the matching off the machines that receive unit-time jobs, fails as it stands: a machine may receive one unit-time job or none, and the argument must exclude this for every schedule, including the degenerate instances in which some $a_j$ lies in no triple or triples repeat. For Corollary 2, the passage from the real-valued approximation guarantee to the threshold $2$ depends on the strict inequality $\rho < 3/2$; at $\rho = 3/2$ the statement is no longer implied by Theorem 5.

Formalization scope

• Machines are Fin m; 3DM elements are Fin n; a 3DM instance is T : Fin m → Fin n × Fin n × Fin n, so a triple may repeat. A matching is a set of $n$ triple indices covering every $a_j$, $b_k$, $c_l$ (the covering form of the paper's definition, which forces disjointness).
• The jobs of the reduced instance are the sum type $\mathrm{Fin}\,n \oplus \mathrm{Fin}\,n \oplus \Sigma_j\,\mathrm{Fin}(t_j - 1)$. They are enumerated by a fixed bijection with $\mathrm{Fin}\,N$ so that the published MatousekLP.Scheduling.makespan applies. All statements quantify over every schedule, so the choice of bijection is irrelevant.
• $t_j - 1$ is natural-number subtraction. When some $t_j = 0$ (a case the paper leaves aside), type $j$ has no dummy job; the reduced instance then has neither a matching nor a schedule of makespan at most $2$, so Theorem 5 and Corollary 2 hold as stated, with no hypothesis $t_j \ge 1$. Only the dummy-count milestone assumes $t_j \ge 1$.
• Processing times are natural numbers cast to $\mathbb R$; makespans are real.
• Not formalized: "polynomial" (running time of an algorithm and of the reduction), membership in NP, "NP-complete" and "unless $P = NP$". Theorem 5 is stated as the reduction's equivalence; Corollary 2 is stated as the fact that any $\rho$-approximate schedule of the reduced instance, $\rho < 3/2$, decides 3-dimensional matching. The reduction is evidently polynomial, but this is not stated.
• The approximation hypothesis compares $\sigma$ with every schedule $\tau$ of the same reduced instance; a goal in which $\sigma$ is an arbitrary schedule, or is bounded against an unrelated quantity, would be a different statement. The strict inequality $\rho < 3/2$ is essential and kept.
• Contributions welcome: proofs of the three milestones, of Theorem 5 from them, and of Corollary 2; reusable lemmas about integer-valued makespans and about sum-type job sets.

Selected references

• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, CWI Report OS-R8714, Centre for Mathematics and Computer Science, Amsterdam, 1987 (FOCS 1987); the version cited for every theorem number in this mission.
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46 (1990) 259–271. https://doi.org/10.1007/BF01585745
• R. L. Graham, E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, 1979 (3-dimensional matching, problem [SP1]).
• P. Schuurman, G. J. Woeginger, Polynomial time approximation algorithms for machine scheduling: ten open problems, Journal of Scheduling 2 (1999) 203–213. https://doi.org/10.1002/(SICI)1099-1425(199909/10)2:5<203::AID-JOS26>3.0.CO;2-5
• D. P. Williamson, D. B. Shmoys, The Design of Approximation Algorithms, Cambridge University Press, 2011. https://doi.org/10.1017/CBO9780511921735

Motivation

Finite-horizon Markov decision processes ask which decisions minimize accumulated cost over a specified number of stages. In a stationary process, the same costs and transitions apply at every stage. This compact input can describe a horizon $T$ much larger than the state set, so a method that processes all $T$ stages one by one may take time exponential in the length of the written horizon. Papadimitriou and Tsitsiklis identified this issue while comparing sequential and parallel algorithms for decision processes. For the deterministic stationary case, their Theorem 5 states an NC classification, supported by a finite structural description of a cheapest long walk. Papadimitriou and Tsitsiklis (1987)

The structural description is the subject of this mission. It connects a policy optimization problem to bounded-length graph objects and an exact cost identity. This is useful independently of a particular model of parallel computation: it says which shorter walk and cycle costs determine the answer even when the horizon is very large. Papadimitriou and Tsitsiklis (1987), p. 447

Setting

Let $S$ be a finite nonempty set of states, with $n=|S|$, and fix an initial state $s_0$. At each state $s$, a finite nonempty set $D_s$ contains the available decisions. A decision $d\in D_s$ has a certain successor state $\operatorname{next}(s,d)$ and a real cost $c(s,d)$. The model is stationary: these data do not depend on time. The corresponding directed graph has one arc for each decision. It may have loops and parallel arcs, because distinct decisions can share endpoints. This is the deterministic graph translation made in §3 of the paper. Papadimitriou and Tsitsiklis (1987), pp. 444–445

A policy is a function $\delta(s,t)\in D_s$ of both state and time. Starting at $s_0$, it produces $s_{t+1}=\operatorname{next}(s_t,\delta(s_t,t))$. In the convention of the paragraph before Theorem 5, horizon $T$ means $T$ decisions and therefore a walk with $T$ arcs. Its cost is

$$J_T(s_0,\delta)=\sum_{t=0}^{T-1}c(s_t,\delta(s_t,t)),\qquad J_T^*(s_0)=\inf_\delta J_T(s_0,\delta).$$

A walk records the states and the decision arc used at each step; states may repeat. A simple path has no repeated state. A simple cycle has positive length, returns to its starting state, and has no other repeated state. A closed walk may repeat states internally and need not be a simple cycle. The distinction matters because the structural claim uses a simple cycle, whereas the computation in the target identity uses a cheapest closed walk of a chosen length.

Formalization targets

The first milestone identifies $J_T^*(s_0)$ with the minimum cost of a $T$-arc walk from $s_0$. The next milestones record a decomposition into a simple path and simple cycles, the restriction on cycles repeated more than $n$ times, and the existence of a cheapest walk with a short prefix and one repeated simple cycle. These are claims in the paragraph preceding Theorem 5, with corrections to the printed exchange and its connectivity justification documented in the formal statements. Papadimitriou and Tsitsiklis (1987), p. 447

For $l\le T$ and $u\in S$, let $w_{l,u}$ be the cheapest $l$-arc walk from $s_0$ that visits $u$. Let $r_{k,u}$ be the cheapest closed $k$-arc walk at $u$. Only choices for which these walks exist are included. The mission's goal is

$$J_T^*(s_0)=\min_{\substack{l\le T,\ l<n^3,\ u\in S,\\1\le k\le n,\ k\mid T-l}}\left(w_{l,u}+\frac{T-l}{k}\,r_{k,u}\right),\qquad T>n^2.$$

The $l<n^3$ bound is the paper's finite compression claim. The divisibility condition makes $(T-l)/k$ an integer number of cycle copies. The goal states an exact value, with the inner minima taken over genuine walks and the outer optimum still taken over all policies. Papadimitriou and Tsitsiklis (1987), p. 447

Significance

The identity replaces an optimization over arbitrarily many time-dependent policy decisions with costs of walks having fewer than $n^3$ arcs and closed walks of at most $n$ arcs. It gives the mathematical statement that must hold before the paper's proposed parallel calculation can be trusted. It also applies when several different decisions have the same endpoints, because each decision remains a separate weighted arc. Papadimitriou and Tsitsiklis (1987), pp. 445, 447

The paper proves the result informally and states the NC classification. The mission seeks machine-checked proofs of the graph and cost statements, including the printed argument's delicate boundary cases. The local proposal contains open Lean theorem statements, not proofs. Reusable outcomes include a decision-walk representation, a cycle decomposition that preserves the multiset of arcs, and finite-horizon policy-to-walk equivalence. A related published result, TropicalLA.exists_repeat, detects repetition for dense max-plus matrices; it does not state this weighted multigraph decomposition or the min-cost identity.

Difficulty

The obstacle is preserving both walk feasibility and the exact number of arcs when repeated cycles are rearranged. A cycle may be the only connection to other parts of a walk, so deleting its last copy can invalidate the remaining sequence. The printed exchange paragraph also reverses the cost-improving direction and appeals to a no-ties perturbation without carrying it through the bounded-prefix conclusion. Those issues affect the claimed $n^3$ bound; merely knowing that a long walk repeats a vertex does not establish the target identity. Papadimitriou and Tsitsiklis (1987), p. 447

Formalization scope

Lean represents $S$ and each $D_s$ as finite types and uses real costs. The decision sets are nonempty, making policies and arbitrarily long walks available. Policies depend on state and time, as in §2. A walk stores its decisions as well as its states, so loops and parallel arcs are represented. Cycle decompositions preserve endpoints, length, cost, and the multiset of decision arcs. A loop is a simple cycle of length one. Time starts at zero, and an $l$-arc walk has states at indices $0,\ldots,l$.

The paper's general finite-horizon definition sums costs from $0$ through $T$, while the Theorem 5 paragraph explicitly asks for a $T$-arc walk. This mission follows the latter convention: decisions occur at $0,\ldots,T-1$. The goal also imposes $l\le T$, which the printed loop leaves implicit, and uses a closed walk for $r_{k,u}$ because that is what the length-$k$ graph calculation computes. It does not assume distinct walk costs. The condition $T>n^2$ is retained from the paper even though related identities may hold in other ranges. Papadimitriou and Tsitsiklis (1987), pp. 444, 447

Theorem 5's NC membership, processor and parallel-time bounds, the membership-in-P discussion, log-space reductions, PSPACE membership, and Corollaries 1–2 are outside this mission. Mathlib does not supply the PRAM and complexity-class framework those claims require. The target is the exact cost identity behind the algorithm. Defining the optimum directly as the right-hand minimum, restricting policies to stationary policies, or allowing an empty policy class would trivialize or change it. Contributions proving the milestones, the goal, or reusable walk and cycle facts are welcome.

Selected references

• Christos H. Papadimitriou and John N. Tsitsiklis, The Complexity of Markov Decision Processes, Mathematics of Operations Research 12(3), 441–450, 1987. DOI: 10.1287/moor.12.3.441

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

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 describes repeated choices whose costs and subsequent states depend on the current state. Such models are used when a decision affects both today's expense and the options available tomorrow. Papadimitriou and Tsitsiklis studied how the computational difficulty of finding an optimal policy changes between stochastic and deterministic transitions. Their general finite-state problems are P-complete, while their deterministic cases admit highly parallel algorithms Papadimitriou and Tsitsiklis, 1987. The contrast makes the deterministic case a useful setting in which to isolate the precise graph problem hidden inside long-run optimization.

This mission concerns their infinite-horizon average-cost case. When transitions are certain, every decision is an arc in a directed graph. The long-run cost of a policy can be related to the mean cost of a cycle reachable from the initial state. That relation is the mathematical claim supporting the algorithm in the paper's Theorem 3, whose headline says that the deterministic average-cost problem is in NC Papadimitriou and Tsitsiklis, p. 446.

Setting

Let $S$ be a finite set of states and $s_0\in S$ the initial state. At each $s\in S$ there is a finite, nonempty decision set $D_s$. A decision $d\in D_s$ has a real cost $c(s,d)$ and moves the process with certainty to $\operatorname{next}(s,d)\in S$. All of these data are stationary: they do not change with time. A policy $\delta(s,t)$ chooses a decision for each state and each time $t=0,1,2,\ldots$. It generates a trajectory by $s_{t+1}=\operatorname{next}(s_t,\delta(s_t,t))$. The corresponding directed graph has a state for each node and a decision for each arc. It may contain loops and parallel arcs, since different decisions can lead to the same next state.

The paper prints the finite average with $T+1$ cost terms and denominator $T$:

$$a_T^\delta(s_0)=\frac{1}{T}\sum_{t=0}^{T}c(s_t,\delta(s_t,t)).$$

A time-dependent policy's averages may fail to converge. We use the upper limit $g^\delta(s_0)=\limsup_{T\to\infty}a_T^\delta(s_0)$ and optimize over all policies, $g^*(s_0)=\inf_\delta g^\delta(s_0)$. A state $u$ is reachable if some finite walk of decision arcs goes from $s_0$ to $u$. A simple cycle $C$ is a positive-length closed sequence of decision arcs with distinct states before it returns to its start; its mean cost is $\operatorname{mean}(C)=c(C)/|C|$. A loop is a one-arc simple cycle.

For states $u,v$, the min-plus adjacency entry $A_{uv}$ is the least cost of a decision arc from $u$ to $v$, or $+\infty$ when no such arc exists. A min-plus product uses addition in place of multiplication and minimum in place of addition. Thus $(A^k)_{uv}$ represents the least cost of a $k$-arc walk from $u$ to $v$, when such a walk exists Papadimitriou and Tsitsiklis, pp. 445–446.

Formalization targets

Reachable cycles

The first target identifies the value of the original policy optimization problem:

$$g^*(s_0)=\min_{\substack{C\text{ simple cycle}\\C\text{ reachable from }s_0}}\operatorname{mean}(C).$$

It also states that a policy attains this value with convergent finite averages. The milestone for following a reachable cycle gives the attainable direction; the milestone saying that no policy can improve the least mean gives the reverse direction. The latter is formulated with $\liminf$, so it applies even when a policy's averages oscillate.

Min-plus calculation

The second target identifies the finite graph calculation used in the paper:

$$g^*(s_0)=\min_{\substack{u\text{ reachable from }s_0\\1\leq k\leq |S|\\(A^k)_{uu}<+\infty}}\frac{(A^k)_{uu}}{k}.$$

The milestones establish what a min-plus power says about decision walks and why closed walks of lengths from $1$ through $|S|$ recover the least simple-cycle mean. The restriction to reachable $u$ is essential: a cheap cycle in a disconnected component cannot be used from $s_0$.

Significance

The result reduces optimization over infinitely many decision times and all state-and-time policies to finitely many closed-walk calculations. It also guarantees that an optimal long-run value is realized by a trajectory with a genuine limiting average, despite the nonconvergence possible for other policies. The finite formula lets one determine the value by comparing graph quantities indexed by states and lengths; it is the correctness statement beneath the paper's parallel algorithm Papadimitriou and Tsitsiklis, p. 446.

Formalizing the identity creates a reusable bridge between deterministic decision processes, weighted directed walks and min-plus powers. Related proved tropical-algebra results on maximum cycle means use dense matrices and a max-plus convention, rather than the reachable, possibly missing-arc, minimum-cost process here; for example, the platform's TropicalLA.tpow_isGreatest concerns greatest walk weights. The present mission keeps the policy optimum and reachability explicit. The paper proves the result mathematically; these Lean statements are open proof targets in the proposal.

Difficulty

An arbitrary policy can keep changing its choices at repeated visits to the same state. Its averages can oscillate, so one cannot simply assume that its infinite trajectory becomes periodic or that its printed limit exists. The lower-bound claim must apply to every such trajectory. There is a second distinction between a closed walk and a simple cycle: a diagonal min-plus entry allows repeated states, whereas the cycle characterization is stated using simple cycles. Finally, an unrestricted matrix calculation would include cycles unreachable from the chosen initial state.

Formalization scope

Lean represents the general finite stationary deterministic process in its own definition, then defines policies, finite walks, simple cycles, average costs and min-plus powers on top of it. Decisions are arcs, so parallel arcs remain distinguishable; $A_{uv}$ takes their least cost and uses WithTop ℝ for a missing arc. Decision sets are explicitly nonempty because a policy has to make a choice at every state. The finite state set is automatically nonempty once $s_0$ is supplied. Policy time starts at zero. The printed $T+1$ terms divided by $T$ are retained; Lean's $T=0$ quotient is zero and has no effect on the limit. The optimum is the infimum over all policies $\delta(s,t)$, not a quantity defined by cycles or by stationary policies. Finite states and finite decision sets bound the one-step costs and hence the averages; this gives real limsup and infimum their intended values.

The paper's Theorem 3 asserts membership in NC. This mission formalizes the exact optimization identity that makes that algorithm correct. Its processor count and parallel-time bound are outside the scope, as are membership in P, log-space computability of reductions, PSPACE membership and the paper's Corollaries 1–2. Contributions to the finite-walk and min-plus lemmas, the lower bound for arbitrary policy paths, and the cycle-attainment statement are all needed; the graph definitions can be reused in other deterministic control problems.

Selected references

• Christos H. Papadimitriou and John N. Tsitsiklis, The Complexity of Markov Decision Processes, Mathematics of Operations Research 12(3), 1987, pp. 441–450. DOI.

Motivation

A seller with one indivisible object must decide whether to keep it or transfer it to one of several bidders whose values she does not observe. The allocation and the payment rule affect what bidders choose to report. Myerson's 1981 paper identifies a revenue-maximizing rule when bidders' private value estimates are independent, their densities are positive, and their valuations may be revised after learning other bidders' information. It covers value distributions for which the usual virtual-value rule is not monotone, by replacing each bidder's virtual value with an ironed priority level.

The question matters to auction design because a pointwise revenue-maximizing assignment can reward a bidder for understating a value. The seller must maximize expected utility subject to both incentive compatibility and each bidder's ability to decline participation. The paper's main theorem gives a specific allocation and payment pair that meets those constraints and attains the maximum. The result is proved in the source; this mission asks for a machine-checked formalization of it.

Setting

There is a finite nonempty set $N$ of bidders and one seller. Bidder $i$ has a value estimate $t_i$ in a finite interval $[a_i,b_i]$, where $a_i<b_i$; endpoints may be negative and may differ between bidders. The continuous density $f_i$ is strictly positive on that interval and has total integral one. The bidders' estimates are independent, so a profile $t=(t_i)_{i\in N}$ has density $f(t)=\prod_i f_i(t_i)$ on $T=\prod_i[a_i,b_i]$. Write $F_i(s)=\int_{a_i}^{s}f_i(u)\,du$ for the distribution function. The seller's known value for keeping the object is $t_0$.

A revision effect $e_j(t_j)$ describes the change in everyone else's valuation after bidder $j$'s estimate becomes known. Bidder $i$'s revised value is $v_i(t)=t_i+\sum_{j\ne i}e_j(t_j)$, while the seller's is $v_0(t)=t_0+\sum_j e_j(t_j)$. A direct mechanism assigns each profile an allocation probability $p_i(t)$ and expected payment $x_i(t)$ for each bidder. Payments may be negative and need not vanish when a bidder loses. Its feasibility conditions say that allocation probabilities are nonnegative and sum to at most one, each bidder's interim expected utility is nonnegative at every possible value, and truthful reporting yields at least as much interim utility as any other report. The seller maximizes her expected utility over all feasible mechanisms.

The virtual value is $c_i(s)=s-e_i(s)-(1-F_i(s))/f_i(s)$. In the general case it need not increase with $s$. Myerson transforms $c_i$ through the quantile $q=F_i(s)$: $h_i(q)=c_i(F_i^{-1}(q))$, $H_i(q)=\int_0^q h_i(r)\,dr$, and $G_i$ is the convex envelope of $H_i$ on $[0,1]$. The slope $g_i$ of $G_i$, extended across kinks, gives the ironed priority $\bar c_i(s)=g_i(F_i(s))$. At profile $t$, the winning set $M(t)$ contains exactly those bidders whose priority is maximal and at least $t_0$.

Formalization targets

The goal is Myerson's §6 theorem. The proposed rule shares the object equally among bidders in $M(t)$, or keeps it when $M(t)$ is empty, and charges each bidder the envelope payment:

$$\bar p_i(t)=\begin{cases}|M(t)|^{-1},&i\in M(t),\\0,&i\notin M(t),\end{cases} \qquad \bar x_i(t)=\bar p_i(t)v_i(t)-\int_{a_i}^{t_i}\bar p_i(t_{-i},s)\,ds.$$

The target asserts that $(\bar p,\bar x)$ is feasible and that every feasible $(p,x)$ has seller utility no greater than that of $(\bar p,\bar x)$. The milestone list follows the paper's reduction: Lemma 2 characterizes feasible direct mechanisms by a monotone interim allocation rule and an envelope identity; equation (4.12) rewrites seller utility using virtual values; Lemma 3 turns maximization of virtual surplus into optimality. Equations (6.9)–(6.13) compare virtual and ironed priorities and establish the optimality and monotonicity of the proposed allocation.

Significance

The theorem specifies both who receives the object and how payments are computed, including irregular distributions and bidder-specific supports. The ironed priorities preserve incentives while retaining the seller's maximal expected utility. Equation (4.12) also gives the revenue-equivalence consequence: once the allocation rule and each lowest-type interim utility are fixed, expected seller utility is fixed.

A formal proof would connect several reusable results: product distributions with bidder-specific densities, interim incentive constraints, an envelope characterization, virtual-surplus accounting, and one-dimensional convex ironing. The source theorem and milestones are currently statements to be proved in this development, not existing machine-checked results. Related Börgers auction statements on Prove2Me use a common nonnegative support, at least two bidders, zero revision effects, and zero seller value; they do not provide this general theorem.

Difficulty

Maximizing virtual surplus at each profile is straightforward only if each bidder's virtual value rises with her report. When it falls, the resulting win probability can also fall, violating the incentive constraint. Replacing virtual values by slopes of a convex envelope restores monotonicity, but then the proof must account exactly for the difference between the original and ironed objectives, including flat portions of the envelope. Payments must satisfy the interim envelope identity for every type, while the seller's objective includes both transfers and her value for retaining the object.

Formalization scope

The Lean model uses a finite nonempty bidder type, real-valued reports and payments, one object, independent continuous positive densities normalized on each finite support, and continuous revision effects. The latter regularity is implicit in the paper's assertion that $c_i$ is continuous. No mean-zero condition on revision effects is imposed: the paper explicitly says its equation (2.9) is unnecessary. One bidder, negative support endpoints, unequal supports, and arbitrary seller value remain allowed.

The profile law is Lebesgue measure restricted to $T$ and weighted by the product density. Integrating a function after replacing coordinate $i$ represents the $T_{-i}$ integral, because bidder $i$'s marginal density has mass one. Mechanisms are total functions, but allocation and incentive conditions quantify over supported profiles and reports. Feasibility explicitly requires integrability of allocations, payments, and their report sections so no undefined Bochner expectation can acquire Lean's default value zero. The convex envelope is the two-point infimum of equation (6.3); its defining set is nonempty and bounded below on $[0,1]$. The slope uses the right derivative below quantile one and the left derivative at one. The theorem requires feasibility of the proposed pair as well as its utility bound, ruling out an empty or unconstrained maximization claim.

The Stieltjes expressions in (6.9), (6.12), and (6.13) are combined into equivalent ordinary-integral comparisons over the profile law. A complete proof needs the one-dimensional envelope theorem, product-measure integration and Fubini results, differentiation of the convex envelope, and a careful endpoint treatment. The definitions of interim utilities and ironing can be reused for related auction models; contributions that establish these analytic components or the listed source lemmas are in scope.

Selected references

• Roger B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1):58–73, 1981. DOI: 10.1287/moor.6.1.58.

Motivation

A Markov decision process is the standard model of sequential decision making under uncertainty: a controller observes the state of a finite system, chooses a decision, pays a cost, and the system moves to a random next state. In many applications (maintenance, inventory with unreliable records, robotics, medical treatment) the controller does not see the state itself, only partial information about it. This is the partially observed problem, and the usual way to solve it is to replace the state by the conditional distribution of the state given the observations (Åström 1965; Bertsekas). That reformulation has an infinite state space, and Smallwood and Sondik (1973) showed that the finite-horizon cost-to-go is nevertheless piecewise linear, but with a number of pieces that may grow exponentially with the horizon.

Papadimitriou and Tsitsiklis (Math. Oper. Res. 12(3), 1987) asked whether this blow-up is an artefact of the reformulation or intrinsic to the problem. Their Theorem 6 answers it: deciding whether a partially observed process can achieve a given expected cost is PSPACE-hard, already for stationary processes and horizons shorter than the number of states. This mission formalizes the reduction behind that theorem.

Setting

A partially observed stationary Markov decision process has a finite state set $S$, a partition $\Pi$ of $S$, and an initial state $s_0$. For a state $s$ write $z(s) \in \Pi$ for the set containing it. Each set $z$ carries a nonempty finite set $D_z$ of decisions; decision $i \in D_z$ costs $c(z, i)$ and moves a current state $s \in z$ to the next state $s'$ with probability $p(s, s', i)$. The controller sees only the sequence of sets visited, so a policy $\pi$ maps each observation sequence $z_0, \dots, z_t$ to a decision in $D_{z_t}$. For a horizon $T$, the expected cost of $\pi$ is

$$J_\pi(T) = \mathbb{E}_\pi\Bigl[\sum_{t=0}^{T} c\bigl(z(s_t), \pi(z(s_0), \dots, z(s_t))\bigr)\Bigr],$$

and the optimal cost is $\inf_\pi J_\pi(T)$.

A quantified Boolean formula is $Q_1 x_1 \cdots Q_n x_n\, F(x_1, \dots, x_n)$ with each $Q_j \in \{\exists, \forall\}$ and $F$ a conjunction of $m$ clauses $C_1, \dots, C_m$, each a set of literals $x_j$ or $\neg x_j$. It is true if there is a value of $x_1$ such that for all values of $x_2$, and so on, $F$ comes out true. Deciding truth (QSAT) is PSPACE-complete (Stockmeyer and Meyer 1973).

From a formula with $m \ge 1$ clauses the paper builds a process $M_\varphi$: an initial state, six states $A_{ij}, A'_{ij}, T_{ij}, T'_{ij}, F_{ij}, F'_{ij}$ per clause $i$ and variable $j$, end states $A_{i,n+1}, A'_{i,n+1}$, and one absorbing state, so $|S| = 6mn + 2m + 2$. The first transition chooses a clause uniformly; primed states record that the chosen clause is not yet satisfied; existential variables are set by decisions and universal ones by fair coins; the only nonzero cost, $1$, is paid at $A'_{i,n+1}$. The horizon is $T = 2n + 2$.

Formalization targets

Goal: the reduction is correct

For every formula $\varphi$ in the paper's QSAT class (an alternating prefix beginning with $\exists x_1$ and ending with $\forall x_n$, and three literals per clause), with $m \ge 1$ clauses and $T = 2n+2$,

$$T < |S|, \qquad \bigl(\exists \pi:\ J_\pi(T) = 0\bigr) \iff \varphi \text{ is true}, \qquad \inf_\pi J_\pi(T) \le 0 \iff \varphi \text{ is true}.$$

The goal states all three claims the paper makes: the horizon bound (p. 448), the existence of a zero-cost policy (p. 449), and the bound on the optimum (p. 448).

Milestones

1. The cost splits over the clause chosen at time 1: each clause is chosen with probability $1/m$, and a policy has zero expected cost iff it has zero cost for every choice of clause.
2. If a trajectory of positive probability ends in $A'_{i,n+1}$, the expected cost is at least $2^{-n}/m$.
3. A zero-cost policy makes the formula true.
4. A true formula yields a zero-cost policy.

Significance

Theorem 6 locates the partially observed finite-horizon problem in the complexity landscape: unless P = PSPACE there is no polynomial-time algorithm for it, even for stationary processes with short horizons. The paper's Corollary 1 strengthens this into evidence that no polynomial-size precomputed controller exists either. Together these results explain why exact algorithms for partially observed processes are exponential and motivated the later work on approximation and on restricted policy classes.

The formalization adds a machine-checked proof of the correctness of the reduction, the step on which the hardness claim rests, together with a reusable definition of a finite partially observed process with observation-history policies and of quantified Boolean formulas. The paper's argument is a short paragraph; a formal proof has to make precise how a policy that only sees observation sequences determines a strategy for the existential player. As far as we know, no machine-checked proof of this reduction exists.

Difficulty

The "if" direction is a direct translation of a winning strategy into a policy. The "only if" direction is where the work is. A zero-cost policy acts on observation sequences, and the paper argues that it never learns which clause was chosen. Under the paper's own partition this is not literally true: the sets $T_j$ and $T'_j$ differ, so the observations reveal whether the chosen clause was already satisfied. The existential strategy must therefore be extracted from the policy's behaviour on the observation histories in which the clause is still unsatisfied, and one must check that it is a single strategy, independent of the clause, that satisfies every clause against every choice of the universal variables. The bound of milestone 2 also requires tracking the probability of a single trajectory through the coin flips.

Formalization scope

The process is a Lean structure POMDP S Z with an observation map obs : S → Z encoding the partition, nonempty finite decision types D z, real costs c z i, and next-state laws given as Mathlib PMFs, so every transition row is a probability vector. A policy is a function List Z → (z : Z) → D z of the earlier observations and the current one. The expected cost is a finite sum over trajectories $x_0, \dots, x_T$ of their probability times $\sum_{t=0}^{T} c$, and the optimum is the infimum over all policies. Paper clause $C_i$ and variable $x_j$ are Lean indices $i - 1$ and $j - 1$.

Choices made explicit:

• Horizon. The paper prints $T = 2m + 2$ but says it is "just enough time for the process to reach one of $A_{i,n+1}$ or $A'_{i,n+1}$", which happens at time $2n+1$. With the printed value and $m < n$ the cost is never paid and every formula would map to a zero-cost process. We use $T = 2n+2$.
• The set $A_j$. The partition sentence puts all $A_{ij}$ and $A'_{ij}$ in one set $A_j$; the decision sentence mentions "the set $A'_j$". We follow the partition sentence.
• The new state reached from $A_{i,n+1}$ and $A'_{i,n+1}$ is unspecified; it gets its own set, one zero-cost decision and a self-loop.
• Formulas. The general QBF definition allows any quantifier prefix and clause width. Every theorem assumes IsPaperQSAT, which requires the paper's alternating prefix $\exists x_1 \forall x_2 \cdots \forall x_n$ with $n>0$ even and three literals per clause. Clauses are sets of literals; three witnesses allow repetitions. $m \ge 1$ is also a hypothesis.
• Decisions are nonempty; rows are probability vectors.

Policies see only observation sequences. A formalization in which the policy reads the state would make the "only if" direction false and the reduction meaningless; one in which it sees only the current observation would make the "if" direction false. Neither is admissible.

Not formalized: PSPACE-hardness itself (Mathlib has no PSPACE or polynomial-time reductions), the polynomial-time computability of the construction, the membership of the problem in PSPACE (sketched on p. 449), Corollary 1 (a $\Sigma_2^p$ collapse) and Corollary 2 (NP-completeness of the unobserved case, stated without proof).

The definitions of partially observed processes and quantified Boolean formulas are reusable. Contributions of lemmas on trajectory sums (marginalising later coordinates, the probability of a fixed prefix) are welcome; they also serve the other missions of this series.

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
• L. J. Stockmeyer and A. R. Meyer, Word problems requiring exponential time, Proc. 5th ACM STOC, 1973, 1–9. https://doi.org/10.1145/800125.804029
• R. D. Smallwood and E. J. Sondik, The optimal control of partially observable Markov processes over a finite horizon, Operations Research 21(5), 1973, 1071–1088. https://doi.org/10.1287/opre.21.5.1071
• K. J. Åström, Optimal control of Markov processes with incomplete state information, Journal of Mathematical Analysis and Applications 10, 1965, 174–205. https://doi.org/10.1016/0022-247X(65)90154-X
• D. P. Bertsekas, Dynamic Programming: Deterministic and Stochastic Models, Prentice-Hall, 1987.

Motivation

Sampling uniformly from a bounded region can be difficult when direct transformation of a familiar random variable is unavailable and rejection sampling spends most of its trials outside the region. Robert L. Smith studied procedures that move within the region: from the current point, choose a direction, form the line set through that point inside the region, and choose the next point uniformly on that line set. The resulting sequence is a homogeneous Markov chain. The Random Directions Algorithm, later commonly called hit-and-run, is a central instance of this construction. Smith's 1984 paper establishes conditions under which the chain approaches the uniform distribution even when its initial point is fixed rather than sampled uniformly (Smith 1984, pp. 1298–1301).

For simulation, the initial point is usually chosen because it is known to be feasible. The question is therefore whether the distribution after many moves forgets that particular choice. A stationary distribution alone does not answer this: stationarity describes what happens if the chain already starts with that distribution. Smith's Theorem 2 gives the stronger, pointwise starting-state statement for the class of symmetric mixing algorithms satisfying his two regularity assumptions (Smith 1984, p. 1301).

Setting

Let $S$ be the state region and $V$ its finite, nonzero content measure. In Smith's geometric setting, $S$ is a bounded $k$-dimensional measurable region in $\mathbb R^n$, and $V$ is $k$-dimensional content; at $k=0$, content is counting measure. A Markov transition kernel $P$ assigns to every current point $x\in S$ a probability $P(x,A)$ of entering a measurable set $A\subseteq S$ on the next move. For the associated chain $(X_0,X_1,\ldots)$, the $m$-step transition probability is $P^m(x,A)=\mathbb P(X_m\in A\mid X_0=x)$.

The uniform law is $\lambda(A)=V(A)/V(S)$. Smith's Assumption (a) gives a measurable transition density $f(y\mid x)$ relative to $V$:

$$P(x,A)=\int_A f(y\mid x)\,V(dy).$$

For a symmetric mixing algorithm, the paper states that this density satisfies $f(y\mid x)=f(x\mid y)$ for all $x,y\in S$. Assumption (b) says $f(y\mid x)>0$ for all such pairs. These are pointwise conditions, including states of zero $V$-measure. A nonempty measurable set $A$ is closed if $P(x,A)=1$ for every $x\in A$. The chain is indecomposable in the paper's sense when it has no two disjoint closed sets (Smith 1984, pp. 1299–1300).

Formalization targets

Stationarity and indecomposability

Lemma 1 asserts that $\lambda$ is stationary: $\lambda(A)=\int_S P(x,A)\,\lambda(dx)$ for every measurable $A$. Lemma 2 excludes two disjoint closed sets. Both are direct prerequisites of the goal. Smith's Theorem 1 also establishes uniqueness of the stationary distribution and almost-sure convergence of empirical visit frequencies under a stationary start; it is described in the source, but its trajectory-level formalization is outside this proposal (Smith 1984, p. 1300).

Convergence from every starting point

The mission goal is Smith's Theorem 2. For every $x\in S$ and every measurable $A\subseteq S$,

$$\lim_{m\to\infty}P^m(x,A)=\lambda(A).$$

This is the paper's explicit meaning of strongly mixing. The milestone list also records the proof's stated nonperiodicity condition: for every $n\ge2$, the $n$-step transition law has no two disjoint closed sets. It is a target in its own right because it concerns all higher-step kernels, not only the one-step chain (Smith 1984, p. 1301).

Significance

Theorem 2 makes the uniform law the limiting distribution of the sample at time $m$, for any fixed feasible initial point. The paper's Theorem 1 supplies a different guarantee about long-run empirical frequencies under a stationary start, although it is not a target of this proposal. Smith later specializes the framework to the Random Directions Algorithm and gives a quantitative rate under additional geometric conditions; that rate is the subject of the companion mission (Smith 1984, pp. 1303–1304).

These results are proved in the paper but the declarations in this proposal are theorem statements with sorry, not machine-checked proofs. A completed formalization would turn the paper's measure-theoretic claims into reusable statements about general measurable state spaces and kernels. The normalized content law, the density interface, and closed-set predicate can be reused when studying other Monte Carlo kernels with the same hypotheses.

Difficulty

The main obstacle is the jump from stationary behavior to convergence from every starting point. Symmetry identifies the candidate stationary law, and strict positivity limits how the chain can split into closed parts, but neither sentence by itself establishes the claimed limit of $P^m(x,A)$. The distinction matters especially at starting points in $V$-null sets: an almost-everywhere starting-state result would leave out precisely the universal claim in Theorem 2. The paper appeals to a general-state Markov-chain convergence result for this step (Smith 1984, p. 1301).

Formalization scope

Lean uses a measurable type $\alpha$ as the whole region $S$, a finite measure $V$ with $V(S)\ne0$, a Markov kernel $P$, and an extended-nonnegative density $f:\alpha\to\alpha\to\mathbb R_{\ge0}^{\infty}$. The density is jointly measurable and is linked to $P$ by the integral identity above; symmetry is pointwise, and positivity is added only for Lemma 2 and Theorems 1–2. This abstract representation retains the hypotheses those results use without fixing a particular Euclidean dimension. It covers the counting-content case as well as continuous content, although it does not construct the geometric direction-and-chord algorithm. The Random Directions kernel belongs to the companion mission.

The uniform law is normalized by $V(S)$. Finiteness and nonzero total content prevent a meaningless inverse or an empty probability space. The $m$-step law is the published MarkovChainCLT.iterKernel. Theorem 2 quantifies over every $x$, rather than $\lambda$-almost every $x$, and uses setwise convergence on each measurable $A$. No invariance, uniqueness, minorization, or convergence premise is added to the goal. Detaching $f$ from $P$ would empty out the substantive assertion. Formal contributions can target the density-to-invariance argument, the closed-set conditions, and the general-state convergence theorem needed for the goal. The paper's separate pathwise Theorem 1 remains an appropriate later extension.

Selected references

• Robert L. Smith, Efficient Monte Carlo Procedures for Generating Points Uniformly Distributed over Bounded Regions, Operations Research 32(6), 1296–1308, 1984. DOI: 10.1287/opre.32.6.1296.