Operations Research

Motivation

Classical cooperative game theory assumes that any coalition of players can form and coordinate. In many settings cooperation is mediated by pairwise relationships: communication lines, contracts, alliances, or trade links. Roger Myerson's discussion paper Graphs and Cooperation in Games (Northwestern University, 1976; published in Mathematics of Operations Research 2(3), 1977, doi:10.1287/moor.2.3.225) models such a cooperation structure as a graph on the set of players and asks how the players should share the worth of the game when only linked players can coordinate directly.

The answer, now called the Myerson value, is the starting point of the literature on communication situations and network games. It underlies later work on network formation (Jackson and Wolinsky, A strategic model of social and economic networks, JET 1996) and on allocation rules for networks, and it is a standard textbook example of an axiomatic solution concept.

Timeline:

• 1953. Shapley defines the Shapley value $\varphi$ for transferable-utility games by efficiency, symmetry, a carrier axiom and additivity (Shapley 1953).
• 1976–1977. Myerson introduces cooperation graphs, the fairness (equal gains from each link) condition, proves existence and uniqueness of the fair allocation rule, identifies it as the Shapley value of the graph-restricted game, proves its total stability for superadditive games, and extends existence and uniqueness to games without transferable utility in graph function form.

Setting

Let $N$ be a nonempty finite set of players and $CL$ the set of nonempty coalitions $S\subseteq N$. A game in characteristic function form is a vector $v\in\mathbb R^{CL}$; $v_S$ is the transferable wealth coalition $S$ can divide.

A link $n{:}m$ is an unordered pair of distinct players and a graph $g$ is a set of links; $GR$ is the set of all graphs, $\bar g^N$ the complete graph, $g\setminus n{:}m$ the graph with one link removed, and $|g|$ the number of links. Players $a,b$ are connected in $S$ by $g$ if $a=b\in S$ or a path of links of $g$ joins them through players of $S$ only; the classes form the partition $S/g$ of $S$, and $N/g$ is the set of connected components of $g$. The graph-restricted game is

$$(v/g)_S=\sum_{T\in S/g}v_T .$$

An allocation rule is a function $Y:GR\to\mathbb R^N$, with $Y_n(g)$ the payoff of player $n$ under cooperation structure $g$. It is a fair allocation rule for $v$ if

1. (efficiency, (7)) $\sum_{n\in S}Y_n(g)=v_S$ for every $g$ and every component $S\in N/g$, and
2. (equity, (10)) $Y_n(g)-Y_n(g\setminus n{:}m)=Y_m(g)-Y_m(g\setminus n{:}m)$ for every $g$ and every link $n{:}m\in g$.

$Y$ is totally stable if $Y_n(g)\ge Y_n(g\setminus n{:}m)$ for every $g$ and every link $n{:}m\in g$, and $v$ is superadditive if $v_{S\cup T}\ge v_S+v_T$ for disjoint $S,T\in CL$.

A game in graph function form assigns to every pair $(S,g)$ with $S\in N/g$ a closed, comprehensive (closed under decreasing coordinates), proper ($\emptyset\ne W\ne\mathbb R^S$) set $w(S,g)\subseteq\mathbb R^S$ of feasible payoffs; its fair allocation rule replaces (7) by (14), $(Y_n(g))_{n\in S}\in\partial w(S,g)$.

Formalization targets

Goal: Theorem 3 (p. 8)

If $v$ is superadditive, then the fair allocation rule $Y$ for $v$ is totally stable:

$$Y_n(g)\ge Y_n(g\setminus n{:}m)\qquad\text{for all } g\in GR,\ n{:}m\in g .$$

Theorem 1 (p. 7) and Theorem 4 (p. 10)

Every $v\in\mathbb R^{CL}$ has a unique fair allocation rule; every game $w$ in graph function form has a unique $Y$ satisfying (14) and (10).

Theorem 2 (p. 8)

The fair allocation rule is

$$Y(g)=\varphi(v/g)\quad\text{for all }g\in GR,\qquad\text{in particular } Y(\bar g^N)=\varphi(v).$$

The milestones follow the paper's Section 7: the steps of the proof of Theorem 4 (displays (15)–(17)), Theorem 4, Theorem 1, the decomposition of $v/g$ and the efficiency and equity of $\varphi(v/g)$ (proof of Theorem 2), Theorem 2, and the monotonicity of $v/g$ and $\varphi(v/g)$ in a link (proof of Theorem 3). Theorem 3 is the goal because its proof uses the formula of Theorem 2, whose proof uses the uniqueness of Theorem 1, which is the transferable-utility case of Theorem 4: all four numbered results lie on one path.

Significance

The theorems give an axiomatic foundation for allocation in networks: two natural requirements, component-wise efficiency and equal gains from each link, single out one rule, and that rule is an explicit formula built from the Shapley value. At the complete graph it recovers the Shapley value itself, so the result is also a new characterization of the Shapley value. Total stability says that, for superadditive games, no player has an incentive to break a link, which connects the allocation rule to the question of which networks form.

The results are proved in the paper. A search of the platform found no formalization of cooperation graphs, the graph-restricted game, the Myerson value or total stability; the Shapley value is available as a platform definition and is reused. This mission produces machine-checked statements of all four theorems and of the intermediate steps of their proofs, together with a reusable definition layer for communication situations.

Difficulty

The equity condition (10) relates the payoff at a graph to the payoff at a graph with one fewer link, and it constrains only pairs of linked players; it is not evident that these conditions, together with efficiency on components, determine the rule at every graph, nor that they are consistent. Uniqueness and existence must hold simultaneously for all $2^{|\bar g^N|}$ graphs, and the constraints couple each graph to all of its subgraphs and each player to every other player of its component. In the graph function form, efficiency becomes a boundary condition on a closed comprehensive set, and the existence and uniqueness of the relevant extremal point depend on all three properties of $w(S,g)$.

Identifying the rule with $\varphi(v/g)$ requires the efficiency of the Shapley value on each component of $g$, which is not the efficiency of $\varphi$ on $N$, and equity requires tracking how the partitions $S/g$ change when a link is removed. Total stability is false for general games: without superadditivity a player can gain by cutting a link, so the hypothesis cannot be dropped.

Formalization scope

Players are Fin n, with $0<n$ in every theorem as the paper assumes $N$ nonempty; the paper's player $k$ is index $k-1$. The general game carrier has its own definition module, and the graph-specific definitions build on it. Graphs are SimpleGraph (Fin n): $\bar g^N$ is ⊤, the empty graph ⊥, $h\subseteq g$ is h ≤ g and $h\subset g$ is h < g. A game is a function Finset (Fin n) → ℝ; its value at $\emptyset$ is a junk coordinate that no definition reads, and no theorem assumes $v_\emptyset=0$. Superadditivity quantifies over nonempty coalitions only. The Shapley value is the platform definition Supermodularity.Cooperative.ShapleyValue, applied after resetting the value at $\emptyset$ to $0$. $\mathbb R^S$ is ↥S → ℝ with the product topology, and $\partial$ is the topological frontier.

Explicit readings of the typescript:

• The printed definition of "connected in $S$ by $g$" (p. 3) asks $n^i\in S$ only for $i\ge1$; the formalization requires every vertex of the path, including the start, to lie in $S$, which makes $S/g$ the partition of $S$ the paper describes.
• Comprehensiveness (p. 10) prints "$\forall n\in N$" for coordinates of vectors in $\mathbb R^S$; read as $n\in S$.
• Display (17) writes $Y_n(h)$ under the index $m\in S$; read as $Y_m(h)$, as in (18b).
• The proof headed "PROOF OF THEOREM 4." on p. 13 is the proof of Theorem 3.
• "The unique fair allocation rule" in Theorems 2 and 3 is stated for every fair allocation rule; existence and uniqueness are Theorem 1.
• The paper's $N$ is nonempty; every theorem carries the corresponding hypothesis $0<n$.

The equity and stability conditions quantify over links of $g$ only. Quantifying over all pairs of players would make Theorem 1 false and the goal vacuous, so that reading is ruled out. Likewise (14) is boundary membership, not membership in $w(S,g)$.

Contributions welcome: general lemmas on the partitions $S/g$ (refinement under link deletion, restriction to components), Möbius inversion over the subgraph lattice of a finite simple graph, the carrier and null-player properties of the Shapley value, and the extremal-point lemma for closed comprehensive sets. These are reusable beyond this mission.

Selected references

• R. B. Myerson, Graphs and Cooperation in Games, Discussion Paper No. 246, CMS-EMS, Northwestern University, September 1976; published in Mathematics of Operations Research 2(3):225–229, 1977. https://doi.org/10.1287/moor.2.3.225
• L. S. Shapley, A Value for n-Person Games, in Contributions to the Theory of Games II, Annals of Mathematics Studies 28, Princeton University Press, 1953, pp. 307–317. https://doi.org/10.1515/9781400881970-018
• M. O. Jackson and A. Wolinsky, A Strategic Model of Social and Economic Networks, Journal of Economic Theory 71(1):44–74, 1996. https://doi.org/10.1006/jeth.1996.0108

Why a threshold rule matters

In a finite stopping problem, a decision maker observes rewards one at a time and must accept one without seeing the future. A fully informed observer takes the maximum. This comparison is often called a prophet inequality. The abstract bound that an optimal stopping rule can secure at least half the expected maximum does not say how to choose a simple rule. Samuel-Cahn showed that a threshold chosen from a median of the maximum already gives this guarantee, even when the rewards are independent but differently distributed. The rule requires one number fixed before observations begin. Samuel-Cahn, 1984

The paper builds on earlier comparisons between the maximum and the best stopping value, then narrows attention to rules that accept an observation when it crosses a fixed threshold. This mission isolates its first main result, Theorem 1, and the two cases that determine whether the crossing test is strict or weak. The paper's second main result, concerning the sharpness of the constant for identically distributed rewards, belongs to the next mission in this series. Samuel-Cahn, 1984, pp. 1213–1215

Observations and threshold rules

Let $n\ge1$, and let $X_1,\ldots,X_n$ be independent, nonnegative real random variables. Write $X_n^*=\max(X_1,\ldots,X_n)$. For a threshold $c\ge0$, the weak threshold rule $t(c)$ takes the first $X_i$ with $i<n$ and $X_i\ge c$; the strict threshold rule $s(c)$ uses $X_i>c$. If no earlier observation qualifies, either rule takes $X_n$, even when $X_n$ is below the threshold. Hence every rule returns exactly one observed reward.

The paper distinguishes the full stopped reward from its positive threshold reward. In its notation,

$$E^+X_{t(c)}=E[X_{t(c)}\mathbf1_{\{X_{t(c)}\ge c\}}], \qquad E^+X_{s(c)}=E[X_{s(c)}\mathbf1_{\{X_{s(c)}>c\}}].$$

The last forced observation may contribute to $E X_{t(c)}$ or $E X_{s(c)}$ while contributing zero to $E^+X_{t(c)}$ or $E^+X_{s(c)}$. This difference is essential to the theorem's middle bounds. A median $m$ of $X_n^*$ means both $P(X_n^*<m)\le\tfrac12$ and $P(X_n^*>m)\le\tfrac12$. Define the excess sum $\beta=\sum_{i=1}^n E(X_i-m)^+$, where $x^+=\max(x,0)$. The two median inequalities allow an atom at $m$, and the two threshold rules handle that boundary differently. Samuel-Cahn, 1984, pp. 1213–1214, (1.1)–(1.2)

Formalization targets

Theorem 1: a median threshold

For every median $m$, the goal retains both of the paper's conditional conclusions:

$$\begin{aligned} \beta\ge m&\Longrightarrow E X_n^*\le2E^+X_{s(m)}\le2E X_{s(m)},\\ \beta\le m&\Longrightarrow E X_n^*\le2E^+X_{t(m)}\le2E X_{t(m)}. \end{aligned}$$

At equality $\beta=m$, both conclusions apply. The attack path follows the expected maximum bound (1.3), the displayed identities and probability bound in (1.4), and the companion weak threshold display. Each milestone points to an actual line of the paper. The NOTE and ASSERTION give a further interval of working thresholds: if $a^*=E(X_n^*-a^*)^+$ and $b^*=\sum_iE(X_i-b^*)^+$, then every $a^*\le c\le b^*$ satisfies the same chain with $t(c)$. Remark 1 records the special case of observations taking values in one common two point set. Samuel-Cahn, 1984, pp. 1214–1215

What the result gives

Theorem 1 replaces the unspecified best stopping policy with a specific threshold chosen from the distribution of the maximum. It also shows that the thresholded part of the stopped reward alone meets the factor two bound. That stronger middle statement distinguishes the theorem from an outer comparison $E X_n^*\le2E X_\tau$. For a reward distribution with atoms, the theorem says exactly when to use $>$ and when to use $\ge$. Its companion ASSERTION shows that a median is not the only useful threshold choice. Samuel-Cahn, 1984, p. 1214

The result is proved in the paper; the work here is to express its assumptions, boundary behavior, and all displayed inequalities as Lean statements that solvers can prove. The milestones expose reusable facts about positive parts, forced stopping, and independence of a current observation from the event that the rule has survived earlier ones. No machine checked proof of these drafted statements is claimed. The second mission can use the completed theorem to formalize why the factor two cannot be improved uniformly over threshold rules, even for identically distributed observations.

Where the formal proof is delicate

The event that a rule reaches index $i$ depends on the observations before $i$. Establishing its independence from the excess of $X_i$ requires mutual independence of the whole family; pairwise independence does not express enough. A forced stop at $n$ also makes the positive threshold reward smaller than the full stopped reward whenever the last observation misses the threshold. Ignoring that last case would erase one of the theorem's conclusions. Finally, atoms at the median prevent the strict and weak crossing events from being interchanged. Samuel-Cahn, 1984, (1.1)–(1.4)

Formalization scope

Lean indexes the $n$ observations by Fin $n$ with $n>0$. Its index zero is the paper's index one, and the greatest index is the paper's mandatory final stop $n$. The rules are the least qualifying index or that final index. The paper's $s(m)>i-1$ and $t(m)>i-1$ therefore become $i\le s(m)$ and $i\le t(m)$. Observations are measurable, nonnegative almost surely, and mutually independent under a probability measure.

Expectations use the extended nonnegative integral of the positive part, taking values in $[0,\infty]$. This keeps infinite expected rewards visible without imposing an integrability assumption absent from Theorem 1. The median has both strict tail inequalities from (1.1). The identities for positive stopped rewards state $m\ge0$ directly; in the goal this follows from nonnegativity and the median condition. The balance thresholds $a^*$ and $b^*$ are parameters satisfying the paper's defining equations, with no extra uniqueness hypothesis in statements that do not use it.

The goal cannot be satisfied by replacing $E^+X_\tau$ with $E X_\tau$, by permitting a rule to return no observation, or by making the median predicate empty. Useful contributions include the measurable threshold rule interface, the pathwise excess decomposition, the factorization under mutual independence, and the remaining extended nonnegative arithmetic. Those pieces can also support other finite prophet inequality developments.

Selected references

• E. Samuel-Cahn, Comparison of Threshold Stop Rules and Maximum for Independent Nonnegative Random Variables, The Annals of Probability 12(4), 1213–1216, 1984. DOI: 10.1214/aop/1176993150

Motivation

Primal–dual interior point methods follow a path of strictly feasible solutions to a linear program. Their worst case iteration bounds come from controlling a term that is quadratic in each search step. Mizuno, Todd, and Ye asked whether that term is typically much smaller than its worst case bound under a model in which a certain subspace is randomly oriented. Theorem 5 in their technical report gives a probability bound for the negative part of that term. It is a statement about one randomly oriented subspace and a fixed input vector, rather than a stochastic model for an entire algorithm run. The authors explicitly note that assigning the same random subspace model independently at successive iterations would be inconsistent with the algorithm's evolving state. Mizuno, Todd, and Ye, §6

Setting

Fix a dimension $n$, an integer $d$ with $0\le d\le n$, and a vector $r\in\mathbb R^n$. Draw a random $d$-dimensional subspace $U$ from the distribution invariant under orthogonal transformations. Let $p$ be the Euclidean orthogonal projection of $r$ onto $U$, and put $q=r-p$, its projection onto $U^\perp$. The matrix $P=\operatorname{diag}(p)$ turns the vector $q$ into the coordinatewise product $Pq=(p_jq_j)_{j=1}^n$.

For a coordinate vector $z$, let $z^-=(\min\{z_j,0\})_{j=1}^n$ and $\|z\|^-_\infty=\|z^-\|_\infty$. Thus $\|Pq\|^-_\infty$ records the magnitude of the largest negative coordinate of $Pq$. An unsubscripted vector norm is always the Euclidean $\ell_2$ norm. These definitions follow the report's notation on printed pages 2 and 4. Mizuno, Todd, and Ye, §§1–2

The formal model samples an $(n-d)\times n$ matrix $G$ with independent standard normal entries and sets $U=\ker G$. The report itself gives this construction as an example of the orthogonally invariant law. With probability one, this null space has dimension $d$. The construction covers the endpoint cases $d=0$ and $d=n$ as well: the projection product is then zero. This probabilistic model has no linear programming data in its statement. The optimization setting explains why the quantity matters, while the result depends only on Euclidean projection geometry. Mizuno, Todd, and Ye, §6

Formalization targets

Theorem 5

For arbitrary choices $r_n\in\mathbb R^n$ and $d_n\le n$ at each dimension, the central target is

$$\Pr\left\{\|P_nq_n\|^-_\infty\le \frac{\log n}{n}\|r_n\|_2^2\right\} \longrightarrow 1\qquad(n\longrightarrow\infty).$$

The logarithm is natural. The theorem asks for the exact coefficient shown in the report, rather than only an asymptotic order. The choice of $r_n$ and $d_n$ may change with $n$; the result does not require a common probability space for all dimensions. Mizuno, Todd, and Ye, Theorem 5, printed p. 13

Source milestones

The mission includes Lemma 6, which identifies a beta distributed radial coordinate and a uniform spherical direction for a projected vector; the componentwise identities and inequality (18)–(19); the Gaussian norm limit (20); the Gaussian coordinate maximum limit cited in the proof; and Lemma 7, which bounds the sup norm of a rotated uniform spherical direction by $\sqrt{3\log n/n}$ with probability tending to one. Their statements, constants, and order follow printed pages 14–15 of the report. Mizuno, Todd, and Ye, §6

Significance

The result gives a precise high probability bound for the negative coordinates of the projection product. In the report this product represents the second order term of a primal–dual search direction, and a smaller value permits a larger admissible step in the relevant neighborhood analysis. The theorem therefore supplies a mathematically definite part of the paper's discussion of anticipated improved behavior. It does not by itself prove a typical iteration count: the paper does not provide a consistent random model for the sequence of subspaces visited by the algorithm. Mizuno, Todd, and Ye, §§2, 6–7

The report proves Theorem 5 and the two numbered lemmas on paper. The formalization work is to provide machine checked proofs of the random subspace representation, the beta and spherical laws, the finite dimensional Gaussian limits, and their connection to the projection bound. These results are reusable in other questions about random projections and coordinatewise estimates. The statements in this mission are open formalization targets; compilation of a statement with a proof placeholder does not count as a machine checked proof.

Difficulty

A direct norm bound on $p$ and $q$ loses the coordinate information needed for the factor $\log n/n$. The difficult part is that the desired bound concerns the most negative coordinate of a product of two dependent projections, while the distribution is specified through a random subspace. The paper's deterministic identity (18)–(19) relates this product to an angular coordinate. The remaining probabilistic statements must control the largest coordinate of a uniformly distributed spherical vector, including the numerical constant in Lemma 7. The laws of the radial and angular coordinates also need a sound measurable construction; simply writing a mapped measure without checking the map would not establish the claimed distributions.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin n), so $\|r\|$ is the $\ell_2$ norm. Coordinate sup norms are separate definitions. A complete development needs finite dimensional inner product geometry, orthogonal projections, Gaussian product measures, beta measures, the uniform spherical law, and limits of real probabilities. The spherical law is encoded as the direction of a standard Gaussian vector. The Gaussian matrix construction fixes the invariant subspace distribution and must be connected to the stated $d$-dimensional law almost surely.

Lemma 6 concerns $d,m\ge1$ and $n\ge2$, where the beta parameters and the spherical direction are nondegenerate. Its angular direction is assigned zero at the zero coordinate, which has probability zero in this regime; the claimed decomposition and unit norm hold almost surely. Theorem 5 retains $d=0$, $d=n$, and $r=0$. Lemma 7 is stated only for frames in dimensions at least two; finitely many smaller dimensions are assigned probability one in its limit expression. Equation (20) keeps the report's condition $\varepsilon>0$. All limits are probabilities tending to one, never probability one at every finite $n$.

Contributions should preserve the source's constants and all three claims of Lemma 6. A proof of the beta law alone, or a bound for a single fixed direction, does not close the corresponding target. The invariant random subspace and projection model, the Gaussian and spherical distribution facts, and the coordinate estimates are each useful independently of this mission.

Selected references

• Shinji Mizuno, Michael J. Todd, and Yinyu Ye, On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming, Cornell ORIE Technical Report No. 944, 1990, revised 1991; published in Mathematics of Operations Research 18(4), 1993. DOI
• Sidney I. Resnick, Extreme Values, Regular Variation, and Point Processes, Springer, 1987, pp. 42 and 71, cited in the report for the Gaussian maximum estimate. DOI

Motivation

A single processor receives jobs over time, each with a known amount of work, and may interrupt a job at any moment to work on another. Which rule should decide what to process? For the number of jobs waiting or in service, the answer is the Shortest Remaining Processing Time (SRPT) rule: at every moment, work on the job in system that is closest to completion. Its optimality is pathwise. It holds for every sequence of arrival times and processing times, not on average under a probabilistic model, so it applies to any single-server queue whatever the distribution of interarrival and processing times. By Little's law it also minimizes mean response time, which is why SRPT and its approximations are the reference policy in the analysis of size-based scheduling for web servers and networks (Harchol-Balter et al., 2003).

Timeline:

• 1966. Schrage and Miller analyse the M/G/1 queue under SRPT and state, without proof, that SRPT minimizes the number in system at every time for every arrival sequence (Schrage–Miller, 1966).
• 1968. Schrage publishes a letter giving a proof by an interchange argument (Schrage, 1968). This mission formalizes that letter.
• 1978. D. R. Smith gives a new proof of the same statement (Smith, 1978) by a different argument.

Setting

An arrival stream is a sequence of pairs $(A(n), P(n))$, $n = 0, 1, 2, \dots$, of real numbers: $A(n)$ is the arrival time and $P(n)$ the processing time of job $n$. A schedule is a family of measurable functions $\delta(n, \cdot) : \mathbb R \to \{0, 1\}$, with $\delta(n, t) = 1$ meaning that the processor works on job $n$ at time $t$. No job is processed before it arrives ($\delta(n, t) = 0$ for $t < A(n)$), and the processor works on at most one job at a time.

The remaining processing time of job $n$ at time $t$ is

$$S(n, t) = P(n) - \int_{A(n)}^{t} \delta(n, x)\,dx,$$

and its completion time is

$$C(n) = \min\Big\{x \ge A(n) : \int_{A(n)}^{x} \delta(n, t)\,dt \ge P(n)\Big\},$$

or $+\infty$ if the job never receives its processing time. The set of jobs in system at time $t$ is $\theta(t) = \{n : A(n) \le t,\ S(n, t) > 0\}$, and $N(t)$ is its cardinality.

A schedule follows SRPT if, at every time $t$ with $\theta(t) \ne \emptyset$, the processor works on a job $k \in \theta(t)$ with $S(k, t) \le S(j, t)$ for all $j \in \theta(t)$. Ties may be broken arbitrarily.

Formalization targets

Goal: SRPT minimizes the number in system at every time

For every locally finite arrival stream, every SRPT schedule $\delta_s$ and every schedule $\delta$ of the same stream,

$$N_s(t) \le N(t) \qquad \text{for all } t \in \mathbb R.$$

The goal has no constants and no distributional assumptions. It is the statement quoted on p. 687 and concluded at the end of the PROOF on p. 689.

Milestones: the steps of the letter's interchange argument

All five come from the PROOF on p. 689. They compare an original schedule $\delta_o$ with a revised schedule $\delta_r$.

1. Idle case (b1). If the processor is idle on $[t, t+v]$ while job $j$ waits, processing $j$ there gives $C_r(j) < C_o(j)$ and $C_r(i) = C_o(i)$ for $i \ne j$.
2. Max identity. Reassigning the capacity that two jobs $j, k$ share after time $t$, in any way, leaves $\max\{C(k), C(j)\}$ unchanged.
3. SRPT minimizes the minimum. Giving that capacity first to the job with the smaller remaining time minimizes $\min[C(k), C(j)]$.
4. Relation (2). If $k$ is served on $[t, t+v]$ while $j$ with $S_o(j,t) < S_o(k,t)$ waits, the SRPT reassignment gives $\min[C_r(k), C_r(j)] < \min[C_o(k), C_o(j)]$.
5. Counting. Relations (1)–(3) on completion times give $N_r(y) = N_o(y) - 1$ for $C_r(j) \le y < \min[C_o(k), C_o(j)]$, and $N_r(y) = N_o(y)$ otherwise.

Significance

The result. The goal is a sample-path dominance. Each consequence for averages follows by taking expectations or time averages: SRPT minimizes the mean number in system and, through Little's law (Little, 1961), the mean response time in every G/G/1 queue with known job sizes. It makes SRPT the benchmark against which other preemptive disciplines, size-based or size-oblivious, are measured.

Formalizing it. The statement has been proved on paper since 1968 and given a complete proof in 1978. No machine-checked proof of it is known to this mission. A formalization contributes three things: a precise continuous-time model of preemptive single-server schedules with measurable service indicators and possibly infinite completion times; checked proofs of the exchange steps of the 1968 letter, each of which needs a hypothesis the letter leaves implicit; and a checked proof of the pathwise optimality theorem itself.

Difficulty

The letter argues that a non-SRPT schedule contains an interval on which SRPT is violated, and that swapping service on that interval improves the schedule. The first step fails for measurable schedules. A schedule can violate SRPT on a set of positive measure that contains no interval (a fat Cantor set), or only on a null set. So the "interval of non-SRPT behaviour" need not exist, and a single interchange does not turn an arbitrary schedule into an SRPT one. Repeating interchanges also gives no obvious termination or limit argument, because the improvements can accumulate at a point. The goal therefore cannot be reached by formalizing the letter's induction literally. The milestones are the letter's local claims, which are true under the hypotheses stated with them. The goal needs an argument that compares an SRPT schedule with an arbitrary one at every time directly.

Formalization scope

All declarations live in the namespace SchrageSRPT.Opt. Jobs are indexed by ℕ from $0$, and times, arrival times and processing times are real. A schedule is δ : ℕ → ℝ → ℝ with values in $\{0,1\}$, each δ n measurable, $\delta(n,t) = 0$ before arrival, and at most one job served at a time. The letter's $\sum_n \delta(n,t) \le 1$ is stated as "two served jobs are equal", not as a series. Assumption (I) of the letter (the arrival stream does not depend on the discipline) is encoded by comparing schedules of one fixed stream. Assumption (II) (preemption wastes no work) is the formula for $S(n,t)$, which has no setup term. Completion times take values in WithTop ℝ, with $+\infty$ for a job that never completes. A job is in system on $[A(n), C(n))$. $N(t)$ is Set.ncard, and the goal assumes local finiteness ($\{n : A(n) \le t\}$ is finite for every $t$) so that it is a genuine count. SRPT is the verbal rule of p. 687, required at every $t$.

Two encodings would trivialize the goal, and both are ruled out. The displayed condition of p. 688 ("$S(k,t) > S(j,t)$ for $j \in \theta(t)$ implies $\delta(k,t)=0$") is satisfied by the schedule that never works, so it is not used as the definition of SRPT. The competitor class is every schedule of the stream: it is not restricted to work-conserving schedules, to finitely many jobs, or to schedules in which every job completes.

The milestones add disclosed hypotheses that the letter uses silently:

• finiteness of $C_o(j)$ in the idle case;
• no service on a job after it completes in the max identity;
• that one of the two jobs completes under $\delta_o$ in relation (2).

The counting milestone uses the half-open interval, since the letter's closed right endpoint is a slip.

A complete development needs:

• continuity and monotonicity of $x \mapsto \int_{A(n)}^x \delta(n,t)\,dt$;
• the characterization $n \in \theta(t) \iff A(n) \le t < C(n)$;
• interval integrals of schedules modified on sets.

All of this is reusable for other continuous-time preemptive scheduling results. Contributions are welcome in particular for this infrastructure, for proofs of the milestones, and for a complete proof of the goal.

Selected references

• L. Schrage, A proof of the optimality of the shortest remaining processing time discipline, Operations Research 16(3):687–690, 1968. https://doi.org/10.1287/opre.16.3.687
• L. E. Schrage and L. W. Miller, The queue M/G/1 with the shortest remaining processing time discipline, Operations Research 14(4):670–684, 1966. https://doi.org/10.1287/opre.14.4.670
• D. R. Smith, A new proof of the optimality of the shortest remaining processing time discipline, Operations Research 26(1):197–199, 1978. https://doi.org/10.1287/opre.26.1.197
• J. D. C. Little, A proof for the queuing formula L = λW, Operations Research 9(3):383–387, 1961. https://doi.org/10.1287/opre.9.3.383
• M. Harchol-Balter, B. Schroeder, N. Bansal and M. Agrawal, Size-based scheduling to improve web performance, ACM Transactions on Computer Systems 21(2):207–233, 2003. https://doi.org/10.1145/762483.762486

Motivation

A production process deteriorates over time, and the state it is in cannot be observed directly. Each period the operator chooses among three actions: produce without looking, produce and inspect the item (which reveals the current state at a cost), or revise the process back to its good state. This is one of the earliest partially observed Markov decision problems with a costly observation action, and it is the prototype of the inspection and machine-replacement models that followed in operations research and maintenance theory. Ross (Management Science 17(9), 1971) set it up for a countable state space, reduced it to a fully observed problem on beliefs, and determined the structure of an optimal policy for two states.

Intuition suggests a three-region policy for two states: produce while the probability of the bad state is small, inspect at intermediate probabilities, revise when it is large. Ross showed that the true structure has up to four regions: produce, inspect, produce again, revise. This mission formalizes that structure theorem and the general results it rests on.

Setting

The underlying process has a countable set of states $0,1,2,\dots$, with transition probabilities $P_{ij}$ from state $i$ at the end of a period to state $j$ at the beginning of the next. In state $i$, producing without inspection costs $C_i$, producing with inspection costs $I_i$, and revising costs $R_i$; costs are bounded, and future costs are discounted by $\beta\in(0,1)$. A revision puts the process in state $0$.

The decision maker tracks a belief $P=(P_0,P_1,\dots)$, a probability vector on the states, ranging over

$$S=\Big\{P: P_i\ge0,\ \sum_iP_i=1\Big\}.$$

Producing without inspection moves the belief to $TP$, with $(TP)_i=\sum_jP_jP_{ji}$. Inspecting reveals the state; if it is $i$, the next belief is the row $e^i=(P_{i0},P_{i1},\dots)$. Revising leads to $e^0$.

The $\beta$-discounted optimal cost $V_\beta$ is the limit of value iteration: $V^0=0$ and

$$V^{n+1}(P)=\min\Big\{\sum_iP_iC_i+\beta V^n(TP);\ \sum_iP_iI_i+\beta\sum_iP_iV^n(e^i);\ \sum_iP_iR_i+\beta V^n(e^0)\Big\}.$$

The three terms with $V^n$ replaced by $V_\beta$ form the right side of the optimality equation (1). The $\beta$-optimal produce, inspect and revise regions are the sets of beliefs at which the corresponding term equals $V_\beta(P)$, and a stationary rule is $\beta$-optimal when it always selects an action attaining the minimum.

In the two-state process of §3, state $0$ is good and state $1$ is bad: $P_{00}=1-\pi$, $P_{11}=1$, $C_0=0$, $C_1=C$, $I_0=I_1=I$, $R_0=R_1=R$, with $C<I<R$. The belief is a number $P\in[0,1]$, the probability of the bad state, $TP=P+\pi-\pi P$, and the optimality equation becomes

$$V_\beta(P)=\min\{CP+\beta V_\beta(TP);\ I+\beta PV_\beta(1)+\beta(1-P)V_\beta(\pi);\ R+\beta V_\beta(\pi)\}.\tag{3}$$

Formalization targets

Goal: Theorem 3.3, the four-region structure

There are thresholds $\pi\le P_1\le P_2\le P_3$ with $P_2\le1$ such that the rule

$$\text{produce on }[0,P_1),\quad\text{inspect on }[P_1,P_2),\quad\text{produce on }[P_2,P_3),\quad\text{revise on }[P_3,1]$$

is $\beta$-optimal, and $P_3\le1$ whenever revising is $\beta$-optimal at some belief. Degenerate thresholds (empty intervals) are allowed, so the statement fixes only the order of the regions, not their number.

Milestones

1. (1): value iteration converges on $S$, $V_\beta$ is bounded, solves (1), and is its unique bounded solution.
2. Lemma 2.1: $V_\beta$ is concave on $S$.
3. Theorem 2.2: the $\beta$-optimal inspect and revise regions are convex.
4. (3): the two-state optimality equation, as an instance of (1).
5. Lemma 3.1: in the two-state model $V_\beta$ is nondecreasing on $[0,1]$.
6. Lemma 3.2: for $0\le P\le\pi$, producing is strictly better than inspecting and than revising.

Significance

Theorem 3.3 reduces the search for an optimal policy in the two-state problem to the choice of three numbers, and it fixes the order of the regions: there is never a revise region below an inspect region, and inspection never occurs below the deterioration probability $\pi$. Together with Theorems 3.4 and 3.7 of the same paper (separate missions in this series), it is the basis for computing optimal inspection policies by searching over thresholds. Theorem 2.2 holds for any countable state space and is the general form of the observation that, in partially observed problems with linear-in-belief action costs, the regions of the "information" and "reset" actions are convex while the region of the passive action need not be.

The results are proved in the paper. As far as a search of the Prove2Me library shows (October 2026), none of them is formalized. Related formal work treats other models: belief-state reductions of finite POMDPs, and abstract contraction models for discounted dynamic programming. The mission produces machine-checked versions of the general model's optimality equation, the concavity of its value function, the convexity of two of its regions, and the two-state structure theorem.

Difficulty

The paper's proofs are short and lean on facts quoted from the literature. Theorem 3.3's proof is two sentences long. Filling it in requires several facts that the paper leaves implicit. The revise region of the two-state model is a closed right-hand interval. The inspect region meets $[0,1]$ in an interval, through the affine embedding $P\mapsto(1-P,P)$ of $[0,1]$ into $S$. The half-open endpoints of the rule select optimal actions. That last point needs continuity of $V_\beta$ inside $(0,1)$, a consequence of concavity, and Lemma 3.2 at the left end. The naive reading of the printed theorem, with all three thresholds in $[0,1]$, is false in general (see below), so the threshold bookkeeping cannot be skipped.

On the general side, the optimality equation (1) is quoted from Blackwell. Here it must be proved for value iteration on the belief simplex of a countable state space, where the inspect term is an infinite series of values at the rows $e^i$. Its convergence and the contraction estimates use the boundedness of the costs.

Formalization scope

The general model is a structure over a type ι with [Countable ι], a distinguished state i₀, a transition matrix Pm, costs C I R : ι → ℝ and β. A separate predicate Model.Valid requires nonnegative entries, rows with HasSum (Pm i) 1, bounded costs and 0 < β < 1. The simplex uses HasSum P 1, never tsum, so it consists of genuine probability vectors. $V_\beta$ is defined as limUnder atTop of value iteration from $V^0=0$, which is the paper's own characterization in the proof of Lemma 2.1. It is not an arbitrary function assumed to satisfy (1). The paper's definition as an infimum over measurable policies is not formalized; the policy class would be a separate mission. Regions are subsets of $S$.

The two-state model is the instance ι = Fin 2 with $P_{00}=1-\pi$, $P_{01}=\pi$, $P_{10}=0$, $P_{11}=1$, and its value at the scalar belief $P$ is the general $V_\beta$ at $(1-P,P)$. The general Lemma 2.1 and Theorem 2.2 therefore apply to it without restatement. Standing hypotheses of §3 are $0<\beta<1$, $0\le\pi\le1$ and $0<C<I<R$. $0<C$ is implicit in the paper, where the good state costs $0$ and the bad state $C$. "$\beta$-optimal rule" means a rule selecting a minimizer of the right side of (3) at every $P\in[0,1]$, the criterion the paper quotes on p. 588. "Every $\beta$-optimal policy produces" (Lemma 3.2) means that producing is the unique minimizer.

Threshold repair. The paper prints $\pi\le P_1\le P_2\le P_3\le1$. This is false when revising is never optimal, for instance when $R>C/(1-\beta(1-\pi))$: then always producing is optimal and revising at $P=1$ is strictly worse, so no rule revising on a nonempty $[P_3,1]$ is optimal. The goal keeps $P_3\le1$ exactly when the $\beta$-optimal revise region is nonempty and otherwise allows $P_3>1$; the rest of the printed chain, $\pi\le P_1\le P_2\le1$, is kept. Adding the hypothesis $R<C/(1-\beta(1-\pi))$ instead would drop a case the paper covers.

The statement admits no trivializing reading. The thresholds are quantified existentially, but the rule must be optimal at every belief in $[0,1]$, $V_\beta$ is pinned down by its definition, and the paper's numbers ($C=4$, $\pi=0.1$, $I=6$, $R=10$, $\beta=0.9$) satisfy all hypotheses.

Infrastructure needed: tsum manipulations on the belief simplex (linearity of $T$, summability of $\sum_iP_iV(e^i)$ for bounded $V$), a sup-norm contraction argument for value iteration, and closure of concavity under minima and pointwise limits. The value-iteration and contraction lemmas are reusable for any discounted model with bounded costs. Contributions of intermediate lemmas, such as continuity of the two-state $V_\beta$ on $(0,1]$ or the bridge identities $T(1-P,P)=(1-TP,TP)$, are welcome.

Selected references

• S. M. Ross, Quality Control under Markovian Deterioration, Management Science 17(9):587–596, 1971. https://doi.org/10.1287/mnsc.17.9.587
• D. Blackwell, Discounted Dynamic Programming, Annals of Mathematical Statistics 36(1):226–235, 1965. https://doi.org/10.1214/aoms/1177700285
• K. J. Åström, Optimal Control of Markov Processes with Incomplete State Information, Journal of Mathematical Analysis and Applications 10(1):174–205, 1965. https://doi.org/10.1016/0022-247X(65)90154-X

Motivation

A prophet inequality compares two observers of a sequence of nonnegative random variables $X_1, \dots, X_n$. The prophet knows all values in advance and collects $X_n^* = \max(X_1, \dots, X_n)$. The gambler sees the values one at a time and must decide, irrevocably, when to stop and collect the current value. For independent variables the gambler's optimal value is at least half of $EX_n^*$, and the factor $2$ is sharp. Prophet inequalities are a basic tool in the analysis of online mechanisms, posted-price auctions and online selection problems, where the gambler's rule is a pricing policy and the prophet is the offline optimum.

Optimal stopping rules are often difficult to compute and to implement. A threshold rule, which stops at the first value at least $c$, is a posted price, and is the form used in applications. Samuel-Cahn (Ann. Probab. 12 (1984) 1213–1216) proved that a threshold rule alone attains the factor $2$: with $m$ a median of $X_n^*$, Theorem 1 of the paper gives $EX_n^* \le 2E^+X_{s(m)}$ or $EX_n^* \le 2E^+X_{t(m)}$. Mission I of this series formalizes that theorem.

Timeline (as recounted on p. 1213 of the paper).

• 1978: Krengel and Sucheston show $EX_n^* \le 2V_n(\underline X)$, where $V_n$ is the optimal stopping value, for independent $X_i \ge 0$; the constant $2$ cannot be improved for any $n \ge 2$.
• 1981: Hill and Kertz show that strict inequality holds in all but trivial cases.
• 1982: Hill and Kertz show that for i.i.d. $X_i$ the best constant $\alpha_n$ for optimal rules depends on $n$ and is bounded by $1.6$.
• 1983: Kertz (unpublished at the time) proves $\lim \alpha_n = 1 + a^* = 1.341\ldots$ for a constant $a^*$ given by an integral equation.
• 1984: Samuel-Cahn shows that a median threshold rule achieves the factor $2$ (Theorem 1), and that for threshold rules the factor $2$ cannot be lowered even for i.i.d. variables (Theorem 2). This mission is Theorem 2.

Setting

Fix $n \ge 1$ and a probability law $\mu$ on $[0, \infty)$. Let $X_1, \dots, X_n$ be independent with common law $\mu$, and $X_n^* = \max(X_1, \dots, X_n)$. For a constant $c \ge 0$ the threshold rules are

• $t(c)$: the smallest $i < n$ with $X_i \ge c$, and $t(c) = n$ otherwise;
• $s(c)$: the smallest $i < n$ with $X_i > c$, and $s(c) = n$ otherwise.

The stopped value is $X_{t(c)}$ or $X_{s(c)}$. The truncated expectations are $E^+X_{t(c)} = E[X_{t(c)} I(X_{t(c)} \ge c)]$ and $E^+X_{s(c)} = E[X_{s(c)} I(X_{s(c)} > c)]$: they discard the forced stop at time $n$ below the threshold. The class $T_n^*$ is the set of all $t(c)$ and $s(c)$ with $c \ge 0$.

The lower half of the theorem uses an explicit family. For $0 < a < 1$, $b > 0$, $c > 0$ and $n > b + c$, the variables $X_i^{(n)}$ take the values $0$, $a$, $1$ with probabilities $1 - (b+c)/n$, $c/n$, $b/n$. Two constants enter:

$$a^* = \frac{c(1 - e^{-b}) - b e^{-b}(1 - e^{-c})}{c(1 - e^{-b-c})}, \qquad Q(b, c) = 1 + \frac{e^{-b} - e^{-b-c}}{1 - e^{-b-c}} - \frac{b(e^{-b} - e^{-b-c})^2}{c(1 - e^{-b-c})(1 - e^{-b})}.$$

This $a^*$ is unrelated to the $a^*$ of the NOTE in §1 of the paper.

In Lean (SamuelCahnProphet.IID), a sample is x : Fin n → ℝ under iidLaw μ n, the product measure; tIdx x c and sIdx x c are $t(c)$ and $s(c)$; Emax, EstopT, EstopS, EplusT, EplusS are $EX_n^*$, $EX_{t(c)}$, $EX_{s(c)}$ and the $E^+$ terms; supE and supEplus are the two suprema over $T_n^*$; threePoint n a b c is the law of $X_i^{(n)}$; aStarIID and Q are the constants above.

Formalization targets

Goal: Theorem 2 (p. 1215)

$$\sup_n \sup_{\underline X} \left[\frac{EX_n^*}{\sup_{t \in T_n^*} E^+X_t}\right] = \sup_n \sup_{\underline X} \left[\frac{EX_n^*}{\sup_{t \in T_n^*} EX_t}\right] = 2,$$

over i.i.d. nonnegative $\underline X$. It is stated as three facts: $EX_n^* \le 2 \sup_{T_n^*} E^+X_t$ for every $n$ and law; $\sup_{T_n^*} E^+X_t \le \sup_{T_n^*} EX_t$; and for every $\varepsilon > 0$ some $n$ and law with $(2 - \varepsilon)\sup_{T_n^*} EX_t < EX_n^*$.

Milestones (proof of Theorem 2, p. 1215)

1. The upper bound $EX_n^* \le 2\sup_{T_n^*} E^+X_t$, attributed to Theorem 1.
2. $\lim_n EX_n^{(n)*} = 1 - e^{-b} + a\{e^{-b} - e^{-b-c}\}$.
3. For the three-point law, $\sup_{T_n^*} EX_t = \max\{EX_{t(a)}, EX_{t(1)}\}$.
4. $W(a) = \lim_n EX^{(n)}_{t(a)} = (1 - e^{-b-c})(b + ac)/(b + c)$.
5. $W(1) = \lim_n EX^{(n)}_{t(1)} = 1 - e^{-b}$.
6. $W(a^*) = W(1)$ and $0 < a^* < 1$.
7. With $a = a^*$, $\lim_n EX_n^{(n)*}/\sup_{T_n^*} EX_t^{(n)} = Q(b, c)$.
8. $Q(b, c) \to 2$ as $b \to 0^+$ and $c \to \infty$.

Significance

Theorem 1 says a posted price recovers half of the prophet's value. Theorem 2 says this guarantee is tight within the class of threshold rules even under the most favourable independence structure, identical distributions. This matters because for optimal rules the i.i.d. constant is at most $1.6$ (Hill and Kertz 1982); the theorem separates threshold rules from optimal rules in the i.i.d. case and sets the benchmark that later single-threshold and order-selection analyses compare against.

The result is proved in the paper; to our knowledge no machine-checked proof exists. This mission produces one: a formal model of threshold rules on an i.i.d. sample, exact asymptotics of the expected maximum and of two stopped values for a triangular array of three-point laws, the reduction of the class $T_n^*$ to two rules, and the two-parameter limit. The upper bound (milestone 1) is the i.i.d. case of mission I's goal, and may later be closed by reference to it.

Difficulty

The limits are "easily seen" on the page, but each requires controlling $(1 - x/n)^{n-1}$ uniformly with the exact law of a stopped index on a product space, including the forced stop at $n$ whose contribution vanishes only in the limit. Milestone 3 is a finite claim over an uncountable family of rules: every $t(c)$ and $s(c)$ with $c \ge 0$ must be shown to coincide almost surely with one of $t(0)$, $t(a)$, $t(1)$ or stopping at $n$, and the first and last must be shown dominated by $t(a)$ for every finite $n > b + c$, not only asymptotically. The final step is a joint limit in $(b, c)$, in which $b/(1 - e^{-b}) \to 1$ while the correction term vanishes like $1/c$; an iterated limit is not the statement.

Formalization scope

The i.i.d. variables are the coordinates of $\mathbb R^n$ under the product measure $\mu^{\otimes n}$; all quantities depend only on the joint law, so the supremum over $\underline X$ is a supremum over laws $\mu$ with $\mu((-\infty, 0)) = 0$. Indices are 0-based in Fin n with [NeZero n], the paper's index $n$ being ⊤. Expectations are lintegrals of ENNReal.ofReal in $[0, \infty]$: no integrability is assumed and $EX_n^* = \infty$ is allowed. The sup over $T_n^*$ ranges over $c \ge 0$ and over both families $t(c)$ and $s(c)$. Limits along the triangular array are indexed by $n = k + 1$ and taken in $\mathbb R$ after toReal; the early terms with $n \le b + c$, where the clipped weights of threePoint do not form a probability measure, do not affect any limit.

The page's ratios are not written literally: in $[0, \infty]$ the quotients $0/0$ and $\infty/\infty$ take junk values, so a literal supremum of ratios would be decided by degenerate laws. The goal's third fact uses a strict inequality and requires an explicit probability law on $[0, \infty)$, which rules out the Dirac mass at $0$ and sub-probability witnesses.

A complete development needs: the law of the first index of a product sample entering a set, expectations of finite-valued functions under Measure.pi, the limit $(1 - x/n)^n \to e^{-x}$ along a triangular array, and elementary bounds on the exponential. The first two are reusable for any threshold or secretary-type stopping problem on i.i.d. samples. Proofs of the milestones in any order are welcome, as is a proof of the upper bound that does not route through the median.

Selected references

• E. Samuel-Cahn, Comparison of threshold stop rules and maximum for independent nonnegative random variables, Ann. Probab. 12(4) (1984) 1213–1216. https://doi.org/10.1214/aop/1176993150
• U. Krengel and L. Sucheston, On semiamarts, amarts, and processes with finite value, in Probability on Banach Spaces, Adv. Probab. Related Topics 4, Dekker, New York (1978) 197–266.
• T. P. Hill and R. P. Kertz, Ratio comparisons of supremum and stop rule expectations, Z. Wahrsch. verw. Gebiete 56 (1981) 283–285. https://doi.org/10.1007/BF00536175
• T. P. Hill and R. P. Kertz, Comparisons of stop rule and supremum expectations of i.i.d. random variables, Ann. Probab. 10(2) (1982) 336–345. https://doi.org/10.1214/aop/1176993861

Why this formulation matters

The traveling salesman problem asks for a shortest closed route through a set of cities. Writing it as an integer program requires linear constraints whose integer solutions are exactly the routes. The assignment constraints (each city entered once and left once) are not enough: their integer solutions include collections of disjoint cycles, called subtours, that never pass through the starting city. Some extra family of constraints must rule these out.

In 1960 C. E. Miller, A. W. Tucker and R. A. Zemlin gave such a family using one auxiliary real variable per city (J. ACM 7(4), 326–329). Their MTZ constraints have polynomially many rows, $n^2-n$ for $n$ cities, whereas the subtour elimination constraints of Dantzig, Fulkerson and Johnson (1954) (Oper. Res. 2(4)) have one row per subset of cities. They also handle a generalization: a salesman who returns to base several times, visiting at most $p$ cities per trip. This is the basic form of a capacitated vehicle routing problem. MTZ-type constraints remain standard in vehicle routing models and in textbook formulations of the TSP. Their linear relaxations are known to be weaker than those of the subtour elimination formulation (Padberg and Sung, 1991).

The paper attributes the model to Tucker and reports five machine experiments with Gomory's all-integer algorithm. The computational part is outside this mission.

Setting

There are $n$ cities $1,\dots,n$ and a base city $0$. A tour is a succession of visits to cities without stopping at city $0$. In problem (1) the salesman leaves $0$, visits each of the $n$ cities exactly once and returns to $0$, possibly several times, with at most $p$ cities per tour. Formally, an itinerary is a list $I=(T_1,\dots,T_t)$ of tours. Each tour is a nonempty list of cities other than $0$ of length at most $p$, and each city $1,\dots,n$ occurs exactly once in the concatenation of the tours. The number $t$ of tours is the number of returns to $0$. Tour $(c_1,\dots,c_k)$ travels the arcs $(0,c_1),(c_1,c_2),\dots,(c_k,0)$. $a_{ij}(I)$ denotes the number of times $I$ travels the arc $(i,j)$. For real distances $d_{ij}$, the length of $I$ is the sum of $d_{ij}$ over the arcs it travels.

Problem (2) has non-negative integer variables $x_{ij}$ ($0\le i\ne j\le n$) and real variables $u_1,\dots,u_n$:

$$\min \sum\sum_{0\le i\ne j\le n} d_{ij}x_{ij}\quad\text{s.t.}\quad \sum_{\substack{i=0\\ i\ne j}}^{n} x_{ij}=1\ (j\ge1),\quad \sum_{\substack{j=0\\ j\ne i}}^{n} x_{ij}=1\ (i\ge1),\quad u_i-u_j+p\,x_{ij}\le p-1\ (1\le i\ne j\le n).$$

When the number of tours $t$ is fixed, the relation $\sum_{i=1}^n x_{i0}=t$ is added. With $t=1$ and $p\ge n$, (1) is the standard traveling salesman problem.

Formalization targets

Goal: the equivalence of (1) and (2)

For every $n\ge0$ and every $p\ge1$:

$$\{\,x : \exists u,\ (x,u)\ \text{feasible for (2)}\,\} \;=\; \{\,a(I) : I \text{ a legitimate itinerary of (1)}\,\},$$

with $\sum_{i=1}^n x_{i0}$ equal to the number of tours $t(I)$, and with the $u_i$ in the converse taken to be non-negative integers. In addition, $\sum\sum_{i\ne j} d_{ij}\,a_{ij}(I)$ equals the length of $I$ for all real $d$. The paper says that (2) "will be shown to be equivalent to (1)". Its "burden of proof" is that the two feasible sets correspond and the two objectives agree, and the goal states exactly that.

Milestones, in the order of the paper's proof

1. The constraints of (2) force $x_{ij}\in\{0,1\}$ (p. 327).
2. Along a path $r_0,\dots,r_m$ of non-base cities with all $x_{r_kr_{k+1}}=1$, $u_{r_0}-u_{r_m}\le-m$ (p. 328).
3. A feasible $x$ has no cycle that avoids city $0$, so all tours include city 0 (pp. 327–328).
4. For $p\ge1$, no tour of a feasible $x$ visits more than $p$ cities (p. 328).
5. The converse: $u_i=$ the position of city $i$ in its tour makes $(a(I),u)$ feasible, with $1\le u_i\le p$ (p. 328).
6. Under $x=a(I)$ the objective of (2) is the distance travelled in (1) (p. 327).
7. An itinerary with $t$ tours of at most $p$ cities requires $tp\ge n$ (p. 326).

Significance

The result. The theorem justifies using (2) in place of (1). Because the feasible sets match and the objectives agree, an optimal solution of (2) is an optimal itinerary of (1), and the same holds with the number of tours fixed. It also shows that a compact, polynomial-size family of linear inequalities in auxiliary potentials excludes every subtour. The same idea, with the $u_i$ read as loads or arrival times, underlies the standard capacity and time-window constraints of vehicle routing.

Formalizing it. The result is classical and its proof is short, but the paper argues informally. It follows successor chains, treats "a tour" without defining an itinerary, and leaves several steps implicit, including the hypothesis $p\ge1$ and the distinctness of $r_{p+1}$ and $r_1$. No machine-checked statement of the MTZ equivalence is recorded on the platform. The remaining work is the whole formal proof: the combinatorics that turns a 0/1 matrix with unit row and column sums and no subtours into a list of tours, the converse labelling, and the bookkeeping identity between the two objectives.

Difficulty

The inequalities themselves are elementary. Each milestone about (2) is a short computation with the potentials $u_i$. The work is in the passage from a feasible matrix $x$ to an itinerary. The successor walk from city $0$ must be shown to terminate at $0$ and to cover every arc of $x$. The resulting tours must be listed so that their arc counts reproduce $x$ exactly, including the number of arcs leaving $0$. That number is not constrained directly in (2). It equals $\sum_{i}x_{i0}$ only through a counting argument on the row and column sums. A proof that only shows some itinerary exists does not establish the correspondence the paper claims.

Formalization scope

Cities are Fin (n + 1) with 0 the base city, which is the paper's indexing. The commitments, each also stated in the items' Formalization Notes, are:

• An itinerary is a List of tours, each tour a List of cities. The paper's "legitimate itinerary" is read as: every tour nonempty, free of 0, of length at most $p$; the concatenation duplicate-free; every city $1,\dots,n$ present.
• "A feasible solution to (2) has $x_{ij}$ which do define a legitimate itinerary" is read as $x=a(I)$, the arc counts of $I$, together with $\sum_{i=1}^n x_{i0}=t(I)$ ("The number of returns to city 0 is given by $\sum x_{i0}$"). Arc counts are counts, so $x_{ij}\in\{0,1\}$ is a theorem, not an encoding choice.
• "Together with appropriate $u_i$" is made explicit as the existence of natural-number $u_i$, following the paper's remark that the $u_i$ may be taken non-negative integers. The labelling $u_i=j$ is a definition.
• Problem (2) has no variables $x_{ii}$. The matrix $x$ is indexed by all pairs and the clause $x_{ii}=0$ encodes their absence. $u_0$ exists in the encoding but appears in no constraint.
• $x_{ij}\in\mathbb N$ ("non-negative integers"), $u_i\in\mathbb R$ ("arbitrary real numbers"), and $p-1$ and $p\,x_{ij}$ are computed in $\mathbb R$.
• Added hypothesis $p\ge1$ in the goal and in milestone 4. The paper does not state it, and the claim is false without it: for $n=1$, $p=0$, $x_{01}=x_{10}=1$ is feasible for (2) but no itinerary exists.
• The distances $d_{ij}$ are arbitrary reals, with no sign, symmetry or triangle condition, as on the page.
• Milestone 2 states the exact summed bound $-m$. The page prints the weaker $j+1-k$.
• Milestone 3 excludes every cycle of $x$ avoiding $0$. The page argues for the cycle met while following successors from $0$, by an argument that applies to any such cycle.

Not formalized: the constraint and variable counts and the elimination of $x_{i0},x_{0j}$ "to produce an equivalent problem with $n^2+n$ inequalities and $n^2$ variables" (p. 328), which the paper does not make precise, and the machine experiments (pp. 328–329).

Trivializing readings are ruled out. The goal identifies $x$ with the arc counts of an itinerary, not merely the existence of some itinerary. The hypotheses are satisfiable: for $n=3$, $p=2$, the itinerary $[[1,2],[3]]$ with $u=(1,2,1)$ is feasible for (2), while the subtour $x_{01}=x_{10}=x_{23}=x_{32}=1$ is not, for any $u$. Contributions welcome: proofs of the milestones, a reusable library of "functional digraph with unit in- and out-degree" decompositions, and the optimization corollary (equal optimal values of (1) and (2)).

Selected references

• C. E. Miller, A. W. Tucker, R. A. Zemlin, Integer Programming Formulation of Traveling Salesman Problems, Journal of the ACM 7(4), 326–329, 1960. https://doi.org/10.1145/321043.321046
• G. Dantzig, R. Fulkerson, S. Johnson, Solution of a Large-Scale Traveling-Salesman Problem, Operations Research 2(4), 393–410, 1954. https://doi.org/10.1287/opre.2.4.393
• M. Padberg, T.-Y. Sung, An analytical comparison of different formulations of the travelling salesman problem, Mathematical Programming 52, 315–357, 1991. https://doi.org/10.1007/BF01582894
• R. E. Gomory, Outline of an algorithm for integer solutions to linear programs, Bulletin of the AMS 64(5), 275–278, 1958. https://doi.org/10.1090/S0002-9904-1958-10224-4