All missions

Motivation

A manufacturer of a perishable good (newspapers, magazines, bread, seasonal fashion, printed books) sells through a retailer who must commit to an order before demand is known. Unsold units lose most of their value; unmet demand costs goodwill. When the retailer alone bears the risk of leftovers, it orders less than an integrated firm would, and the channel as a whole earns less. This inefficiency is the double marginalization of the newsvendor problem, and return policies, under which the manufacturer buys back unsold units, are the instrument publishers and other suppliers of perishable goods actually use against it.

Barry Alan Pasternack's paper Optimal Pricing and Return Policies for Perishable Commodities (Marketing Science, 1985) was the first to show, in a single-period newsvendor model, which return policies restore the integrated firm's order quantity. It became the starting point of the literature on supply-chain contracts: buy-back contracts are now a textbook chapter (Cachon 2003; Snyder and Shen, Fundamentals of Supply Chain Theory), and the paper's result is the standard example of a contract that coordinates a channel while letting the two firms split the profit.

Setting

A manufacturer produces at unit cost $c$. A retailer sells at the fixed retail price $p$. Leftover units are salvaged at $c_3$ per unit. Each unit of unmet demand costs the retailer a goodwill penalty $g \ge 0$ and the manufacturer an additional penalty $g_1 \ge 0$; write $g_2 = g + g_1$. The data satisfy $c_3 < c < p$.

The manufacturer chooses a policy $(c_1, c_2, R)$: the retailer pays $c_1$ per unit ordered and may return up to the fraction $R \in [0,1]$ of its order $Q$ for a credit $c_2$ per unit. The paper assumes

$$c_3 < c < c_1 < p, \qquad c_3 < c_2 \le c_1 < p. \qquad (1),\ (2)$$

Demand $X \ge 0$ is random with distribution function $F$. Three expected profits are defined as functions of the order $Q$: $EP_T(Q)$, equation (3), the profit of a company store in which the manufacturer sells directly; $EP_R(Q)$, equation (6), the independent retailer's profit under the policy; and $EP_M(Q)$, equation (8), the manufacturer's profit when the retailer orders $Q$. An optimal order for a profit function is a $Q \ge 0$ maximizing it over $[0,\infty)$. The policy coordinates the channel when the retailer's optimal orders are exactly the company store's optimal orders: the decentralized channel then produces the integrated firm's quantity.

The Lean development uses the same letters: Costs carries $c, c_3, p, g, g_1$; Costs.Admissible K c1 c2 R is (1)–(2) with $0 \le R \le 1$; EPT, EPR, EPM are (3), (6), (8); IsOptimalOrder and Coordinates are the two notions just defined; $F$ is cdf D for a demand law D.

Formalization targets

Goal: Theorem 3

A policy which allows for unlimited returns at partial credit will be system optimal for appropriately chosen values of $c_1$ and $c_2$. Precisely, for every price $c_1$ with $c < c_1 < p$ there is a credit $c_2$ with

$$c_3 < c_2 < c_1, \qquad c_1 = (p+g) - \frac{(p+g_2-c)(p+g-c_2)}{p+g_2-c_3} \quad (11),$$

such that the policy $(c_1, c_2, R = 1)$ coordinates the channel for every continuous demand distribution on $[0,\infty)$ with finite mean. The credit is chosen before, and independently of, the demand law.

Milestones

1. (4)–(5): the company store has an optimal order, and $Q$ is optimal iff $F(Q) = (p+g_2-c)/(p+g_2-c_3)$.
2. (7): under an admissible policy, $Q$ is optimal for the retailer iff $0 = -c_1 + p + g - F(Q)[p+g-c_2] - F((1-R)Q)[(1-R)(c_2-c_3)]$.
3. (9)–(10): an admissible policy coordinates the channel iff (10) holds at every system-optimal order.
4. (11): with $R = 1$ and $c_2 < c_1$, coordination holds iff (11) holds, whatever the demand law.
5. Appendix, proof of Theorem 3: for $c < c_1 < p$, (11) has a solution $c_2$ with $c_3 < c_2 < c_1$.

Significance

The result. Theorem 3 says that a buy-back contract with full returns at a partial credit aligns the retailer's incentives with the channel's, and that the coordinating credit depends only on costs. The second point carries the paper's practical conclusion: a manufacturer selling one product to many retailers with different demand distributions can post one price and one return credit and still have every retailer order its system-optimal quantity. The one-parameter family of coordinating pairs $(c_1, c_2)$ then splits the channel profit between the firms. The companion mission (Optimal Pricing and Return Policies for Perishable Commodities II) formalizes the negative results, Theorems 1 and 2: neither full credit with unlimited returns nor a no-returns policy coordinates.

Formalizing it. The paper's proofs are first-order conditions and a short algebraic argument. A machine-checked version adds three things. It makes the analytic content explicit: existence of the system optimum, global optimality of the first-order conditions for an arbitrary atomless demand law, and the quantifier structure "one credit for all demand laws". It repairs a gap: the printed argument for $c_3 < c_2$ establishes only $c_2 > c_3 - g_1$, which suffices only when $g_1 = 0$, although the claim holds for all $g_1 \ge 0$. And it gives a reusable newsvendor layer with returns. Related results are proved on Prove2Me in a different model: Snyder–Shen's SupplyChainTheory.buyback_coordinates (Theorem 14.4) and SupplyChainTheory.buyback_profit_identities. They are not referenced here, because their contract data require a retailer cost $c_r > v \ge 0$, which excludes Pasternack's retailer (no own cost), and because they fix the buy-back price and derive the wholesale price, with no range claim.

Difficulty

The algebraic core, milestone 5, is short. The work sits in the analytic milestones. Differentiating under the integral sign in (3) and (6) needs the integrands' piecewise structure and the absence of atoms; the global-maximum claim needs concavity of the expected profits on $[0,\infty)$, including the boundary $Q = 0$. Coordination is a statement about sets of maximizers, not about one first-order condition: when $F$ is flat at the critical fractile, the optimal orders form an interval, and showing that the retailer's maximizers coincide with the system's requires the monotonicity of the retailer's marginal profit, strict where $F$ increases. The naive reading "both first-order conditions hold at $Q^*_T$" proves one inclusion only.

Formalization scope

Demand is a probability measure D on $\mathbb R$ with D (Iio 0) = 0 and finite mean (IsDemand), and $F$ is cdf D. The paper's density is the hypothesis NullSingletonClass D (no atoms), imposed on each theorem that uses it. The expected profits are Lean integrals of the paper's piecewise integrands, written with if. The goodwill costs satisfy $g, g_1 \ge 0$, implicit in the paper. $R$ is a fraction in $[0,1]$. Optimal orders are maximizers over $Q \ge 0$ that are themselves $\ge 0$. Coordination is equality of the retailer's and the company store's sets of optimal orders. The denominator $p + g_2 - c_3$ is positive under these assumptions, so no division is degenerate.

The goal is not the algebraic statement "there is $c_2 \in (c_3, c_1)$ solving (11)": that is milestone 5. A formalization of Theorem 3 must conclude Coordinates, a statement about the maximizers of the actual profit functions (3) and (6), and must place the quantifier over demand laws inside the existence of $c_2$.

A complete development needs: differentiation of parametric integrals with piecewise-linear integrands, concavity of the newsvendor profit, the intermediate value theorem for continuous distribution functions, and the critical-fractile characterization. The newsvendor layer (milestones 1 and 2) is reusable for any single-period contract model. Proofs of the milestones, alternative proofs (for example via the identity $EP_R = k \cdot EP_T + \text{const}$ under (11), which also removes the no-atoms hypothesis), and the profit formulas (12)–(14) at the coordinated optimum are all welcome.

Selected references

• B. A. Pasternack, Optimal Pricing and Return Policies for Perishable Commodities, Marketing Science 4(2):166–176, 1985. https://doi.org/10.1287/mksc.4.2.166
• G. P. Cachon, Supply Chain Coordination with Contracts, in Handbooks in Operations Research and Management Science 11, 2003, 227–339. https://doi.org/10.1016/S0927-0507(03)11006-7
• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019. https://doi.org/10.1002/9781119584445

Why add-with-carry generators

Simulation, Monte Carlo integration and randomized algorithms consume long streams of numbers that should behave like independent uniform draws. A deterministic generator with finite state is eventually periodic, so its period is the first figure of merit: a stream cannot be longer than its cycle. G. Marsaglia and A. Zaman, A new class of random number generators (Ann. Appl. Probab. 1 (1991)), introduced the add-with-carry and subtract-with-borrow generators. They keep $r$ machine words plus one carry bit, use only additions or subtractions of words, and still reach periods such as $2^{640}$ when the base $b$ is near $2^{32}$ (p. 465). The paper's mechanism for this is number-theoretic: the generated digits are the base-$b$ digits of a fraction $k/m$ written backwards, so the period of the generator is the period of a repeating base-$b$ expansion, i.e. the multiplicative order of $b$ modulo $m$.

Generators of this family were used widely in the following decades (Lüscher's RANLUX generator in lattice field theory is built on subtract-with-borrow), and later work showed that they are equivalent to linear congruential generators with modulus $m$ (Tezuka, L'Ecuyer and Couture 1993). This mission treats the add-with-carry generator. A companion mission treats subtract-with-borrow.

Setting

Fix a base $b \ge 2$ and two lags $r$ and $s$ with $0 < s < r$. A state (or seed vector) is

$$x = (x_1, x_2, \dots, x_r, c),$$

where each $x_i \in \{0, 1, \dots, b-1\}$ is a base-$b$ digit and $c \in \{0, 1\}$ is the carry bit. The digit $x_1$ is the oldest one. The add-with-carry map $f$ (p. 465) is

$$f(x_1, \dots, x_r, c) = \begin{cases} (x_2, \dots, x_r,\ x_{r+1-s} + x_1 + c,\ 0) & \text{if } x_{r+1-s} + x_1 + c < b,\\ (x_2, \dots, x_r,\ x_{r+1-s} + x_1 + c - b,\ 1) & \text{if } x_{r+1-s} + x_1 + c \ge b, \end{cases}$$

and the generated sequence of a seed $x$ is $x, f(x), f^2(x), \dots$. Reading off the last digit of each state gives a digit stream $x_1, \dots, x_r, x_{r+1}, x_{r+2}, \dots$ obeying $x_n = x_{n-r} + x_{n-s} + c \bmod b$, with the carry updated at each step. The two trivial seeds are $(0, \dots, 0, 0)$ and $(b-1, \dots, b-1, 1)$. The modulus of the generator is

$$m = b^r + b^s - 1 .$$

For $0 \le k < m$ and $j \ge 1$, the $j$-th base-$b$ digit of $k/m$ after the point is $d_j(k/m) = \lfloor b \cdot (b^{j-1} k \bmod m) / m \rfloor$. The order $\operatorname{ord}_m(b)$ is the least $p \ge 1$ with $b^p \equiv 1 \pmod m$, and $b$ is a primitive root of a prime $m$ when $\operatorname{ord}_m(b) = m - 1$.

Formalization targets

Goal: the period is the order of $b$

Let $m = b^r + b^s - 1$ be prime, and let $x$ be any seed other than the two trivial seeds. Then $f^r(x)$ is a periodic point of $f$ and

$$\min\{p \ge 1 : f^{p}(f^{r}(x)) = f^{r}(x)\} = \operatorname{ord}_m(b).$$

This is the italic summary of p. 472 ("whatever the seed vector, except for the two trivial seeds, the add-with-carry and subtract-with-borrow sequences become periodic after a few iterations of the generating function, and the periods are the order of the base $b$ for the appropriate modulus"), with the claim of §4.2 (p. 467) and its proof (p. 468). The goal fixes no particular $b$, $r$, $s$ and does not assume that $b$ is a primitive root. When it is, the period is $b^r + b^s - 2$, the value announced in §2.

Milestones

1. §4.1 (p. 467): for $\gcd(k, m) = \gcd(b, m) = 1$, $p > 0$ is a period of the base-$b$ expansion of $k/m$ iff $\operatorname{ord}_m(b) \mid p$.
2. §4.1 (p. 467): if $b$ is a primitive root of the prime $m$, every proper fraction $k/m$ has least period $m - 1$.
3. p. 472: $f(x) = x$ iff $x$ is a trivial seed.
4. p. 472: $f^r(x)$ is periodic for every seed.
5. §4.2 (p. 468): for every seed other than $(b-1, \dots, b-1, 1)$ and every $C$, there is $0 \le k < m$, positive iff the seed is nonzero, with

$$x_n = d_{C+1-n}(k/m) \qquad (r + 1 \le n \le C).$$

6. p. 472, Method 3: $x$ is periodic iff $c = 0$ and $x_r \cdots x_{s+1} \ge x_{r-s} \cdots x_1$, or $c = 1$ and $x_r \cdots x_{s+1} \le x_{r-s} \cdots x_1$ (digit strings read as base-$b$ integers).
7. §2 (p. 465): the instance $b = 10$, $r = 2$, $s = 1$, period $108$.
8. §7 (p. 477): the instance $b = 6$, $r = 21$, $s = 2$, period $6^{21} + 6^2 - 2$.

Significance

The result. The goal reduces the period of the generator, a property of a dynamical system on $2b^r$ states, to the multiplicative order of one residue. That is the computation the paper performs in §6 to certify its recommended generators, and it is how one chooses $b, r, s$: search for primes $m = b^r + b^s - 1$ and check the order of $b$. Milestone 5 is stronger than the goal. It needs no primality and identifies the whole output stream, not only its period, with the expansion of a fraction. That identification is what later work used to relate carry generators to linear congruential generators with modulus $m$. Milestone 6 answers the paper's "periodic seed" puzzle: it says exactly which seeds lie on their own cycle.

Formalizing it. The results are proved in the paper, the general §4.1 facts are classical, and the method-specific rules of §4.5 (milestone 6) are stated there without proof. None of it is machine-checked on Prove2Me or, to our knowledge, in Mathlib, which has orderOf and ZMod but no theory of base-$b$ expansions of rationals. The mission produces a checked link from a concrete integer recurrence to modular arithmetic. That link can serve as a template for other carry-based and lagged generators.

Difficulty

The obvious argument says the digit recurrence is linear, so the period divides something like the order of a companion matrix. This fails because of the carry: $f$ is not linear over $\mathbb{Z}/b$, and the state $(x_1, \dots, x_r, c)$ does not live in a group in any evident way. The link to the order of $b$ modulo $m$ goes through an identity between a finite digit string and a fraction (milestone 5). Stating it with exact indices is itself delicate: the digits run in reverse order, the fraction depends on the string's length, and the trivial seed $(b-1, \dots, b-1, 1)$, whose digits are those of $m/m = 1$, has to be excluded.

A second difficulty is the preperiod. A seed need not lie on its own cycle (p. 472), so the period must be measured after the transient. Bounding that transient by $r$ (milestone 4) and characterising the periodic seeds (milestone 6) are separate combinatorial facts about the carry. The paper states the second without proof.

Formalization scope

• Representation. All declarations are in namespace CarryRNG.AWC. Lags are a structure Lags with fields r, s and proofs of $0 < s$ and $s < r$. A state is a structure with digits x : Fin r → Fin b and carry c : Fin 2, so $c \le 1$ holds by typing. Lean index $i$ is the paper's $x_{i+1}$: x 0 is $x_1$ (the digit the step drops), and the partner digit $x_{r+1-s}$ is index $r - s$. step is defined directly from the two-case formula of p. 465, not through $k/m$. The digit stream out is one-based: the seed digits for $n \le r$, then the last digit of $f^{\,n-r}(x)$. digit b m k j is the exact integer formula above, used for $j \ge 1$ only.
• Period. "The period" is Mathlib's Function.minimalPeriod. It is $0$ at non-periodic points, so the goal's equation with the positive $\operatorname{ord}_m(b)$ also asserts periodicity. A divisibility or inequality form would be vacuous and is not used. For digit sequences, "period $L$" is stated as "$p > 0$ is a period iff $L \mid p$".
• Quantifier readings. "With appropriately chosen base $b$, lags $r$ and $s$ and seed vector $x$" (p. 465) is read as: $m$ prime and $x$ not a trivial seed, following p. 468 ("Making $m$ a prime ensures this") and p. 472. "After a few iterations" is "after at most $r$", the paper's own bound (p. 472), so the goal is stated at $f^r(x)$. In milestone 5 the fraction $k$ depends on the length $C$ of the finite string, as in the paper's "arbitrarily long finite string". In milestone 8, "for any set of 21 seed digits" is stated at $f^{21}(x)$ for the same reason.
• Corrected misprints. p. 465 prints the second trivial seed as "(9, 9, 9)"; the last entry is the carry, so milestone 7 excludes $(9, 9, 1)$. p. 473, example (a), prints the Method 3 inequalities reversed; milestone 6 follows p. 472, which exhaustive checks on small parameters confirm. p. 478 repeats the die period with "− 1" for "− 2"; milestone 8 quotes p. 477.
• Ruled-out trivializations. The goal is not "some period divides $m - 1$" and not "every orbit is eventually periodic". Both hold for any self-map of a finite set or are vacuous. The trivial seeds are named states, not excluded by an assumption such as $f(x) \neq x$.
• Infrastructure and contributions. Needed: periods of base-$b$ expansions of rationals (milestones 1–2, reusable beyond this mission) and finite-dynamics facts about minimalPeriod along an orbit. Proofs of any milestone are welcome, as are primality and order certificates for milestone 8 as separate lemmas.

Selected references

• G. Marsaglia and A. Zaman, A new class of random number generators, Ann. Appl. Probab. 1(3) (1991), 462–480. https://doi.org/10.1214/aoap/1177005878
• S. Tezuka, P. L'Ecuyer and R. Couture, On the lattice structure of the add-with-carry and subtract-with-borrow random number generators, ACM Trans. Model. Comput. Simul. 3(4) (1993), 315–331. https://doi.org/10.1145/159737.159749
• R. Couture and P. L'Ecuyer, Distribution properties of multiply-with-carry random number generators, Math. Comp. 66 (1997), 591–607. https://doi.org/10.1090/S0025-5718-97-00827-2
• M. Lüscher, A portable high-quality random number generator for lattice field theory simulations, Comput. Phys. Commun. 79 (1994), 100–110. https://doi.org/10.1016/0010-4655(94)90232-1

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

Weighted voting bodies often combine a few large blocs with a mass of small, unorganized voters: shareholders' meetings with a handful of large holders and a dispersed float, legislatures with party blocs and independents. The Shapley value measures each participant's voting power as the probability of being pivotal — the one whose arrival first turns a losing coalition into a winning one — when participants arrive in a uniformly random order. For many small voters this computation becomes a combinatorial problem whose size grows with the number of voters.

Milnor and Shapley (RAND RM-2649, 1961; revised as Mathematics of Operations Research 3(4), 1978) replaced the small voters by a continuum, the ocean, and obtained explicit formulas for the power of the large voters. The memorandum is the second of a RAND series on values of large games; the first (L. S. Shapley and N. Z. Shapiro, Values of Large Games, I: A Limit Theorem, RM-2648, 1960) proves the limit theorem for finite games with many small players on which the oceanic model rests. This mission formalizes the part of the memorandum that leads to explicit closed forms for the values of interior oceanic games (§2, §4, §5).

Setting

There are $m$ major players $M = \{1, \dots, m\}$ with weights $w_1, \dots, w_m \ge 0$, and $w(S) = \sum_{j \in S} w_j$. The ocean is the interval $I = [0,1]$ with Lebesgue measure, carrying total weight $\alpha > 0$. In the oceanic game $[c; w_1, \dots, w_m; \alpha]$ with quota $c$, a coalition wins when the weight of its major players plus $\alpha$ times its share of the ocean is at least $c$.

The random order is modelled by a uniform random point $x = (x_1, \dots, x_m)$ of the cube $I^m$: major player $j$ is inserted into the ocean at position $x_j$, and $P(t) = \{ j : x_j < t \}$ is the set of major players placed before position $t$. Player $i$ is pivotal when

$$w(P(x_i)) + \alpha x_i \le c \le w(P(x_i)) + w_i + \alpha x_i, \qquad (2.4)$$

and the value $\varphi_i$ of player $i$ is the probability of (2.4), i.e. the volume of the set $A_i \subseteq I^m$ where it holds. The combined value of the ocean is $\Phi = 1 - \sum_{i} \varphi_i$ (2.5).

With the quota $y$ as a variable, $\Gamma(y) = [y; w_1, \dots, w_m; \alpha]$ has values $\varphi_i(y)$, $\Phi(y)$, and the pivot location $F(y) = \inf\{t \ge 0 : w(P(t)) + \alpha t \ge y\}$ is a random, nondecreasing, piecewise linear function of $y$ with expectation $E\{F(y)\}$. Adding a major player $m+1$ of weight $w_{m+1}$ gives the game $\Gamma^+$.

The game is interior when

$$w(M) \le c \le \alpha,$$

that is, the ocean alone wins and the major players together lose. With $\bar w_j = \alpha - w_j$, define $\pi(S) = \prod_{j \in S} \tfrac{w_j}{\alpha} \prod_{j \in M - S} \tfrac{\bar w_j}{\alpha}$ for $S \subseteq M$, the analogous product $\pi_i(S)$ over $M - \{i\}$ for $S \subseteq M - \{i\}$, and the integers $a_0 = 1$, $a_n = 1 - n a_{n-1}$, i.e. $1, 0, 1, -2, 9, -44, \dots$

Formalization targets

Goal: Theorem 6 (p. 20)

In an interior game, with $s = |S|$,

$$\varphi_i = \frac{w_i}{\alpha} \sum_{S \subseteq M - \{i\}} a_s \, \pi_i(S), \qquad \Phi = \sum_{S \subseteq M} a_s \, \pi(S).$$

Both identities are part of the goal. The values do not depend on $c$ within the interior range.

Milestones

1. §2, p. 5: the pivot sets $A_1, \dots, A_m$ overlap only in measure zero.
2. (4.3): $\varphi_i(y) = \operatorname{Prob}\{F(y) = x_i\}$ for $0 \le y \le w(M) + \alpha$.
3. (4.4)–(4.5): for $0 < y < w(M) + \alpha$, $F$ is differentiable at $y$ almost surely, $\sum_i \varphi_i(y) = \operatorname{Prob}\{F'(y) = 0\}$ and $\Phi(y) = \operatorname{Prob}\{F'(y) = 1/\alpha\}$.
4. Theorem 2, (4.7): $\Phi(y) = \alpha \, \frac{d}{dy} E\{F(y)\}$.
5. Lemma, (4.12)–(4.13): $\varphi^+_{m+1}(z) = \frac{1}{\alpha} \int_{t_1}^{t_2} \Phi(y)\, dy$ with $t_1 = \max(z - w_{m+1}, 0)$, $t_2 = \min(z, w(M) + \alpha)$.
6. Theorem 5, (5.4): if $[c; w_1, \dots, w_m; \alpha]$ and $[d; w_1, \dots, w_{m+1}; \alpha]$ are both interior, $\varphi^+_{m+1} = \frac{1}{\alpha} \Phi w_{m+1}$.
7. Proof of Theorem 6, p. 21: the right-hand sides above add up to 1, an identity valid for all real $w_j$ and $\alpha \ne 0$.

Further items, not milestones: the Corollary (5.5), Theorem 3 (averaged over all quotas, each value equals the player's share of the total weight), Theorem 4 (small players behave like ocean), and (5.8) with its footnote ($|a_n|$ is the nearest integer to $n!/e$ and counts derangements).

Significance

Theorem 6 turns the voting power of the large blocs, a priori a probability over a continuum of orderings, into a finite multilinear polynomial in the ratios $w_j/\alpha$. Table 1 of the memorandum lists the cases $m \le 3$, and the theorem gives every $m$. Its coefficients are signed derangement numbers. The Corollary (5.5) states that a major player's value per vote equals the ocean's value per vote in the game without that player.

The memorandum's arguments are short and partly heuristic: "E commutes with the derivative", the disjointness of the pivot sets is "obvious", and the induction for Theorem 6 relies on the symmetry of the value in the major players, which is never stated. A formalization makes each of these steps precise, including the measure-zero exceptions and the quota ranges. To our knowledge none of these results has a machine-checked proof; Mathlib has the Lebesgue measure on cubes, interval integrals and derangement numbers, but no game-theoretic value with a continuum of players.

Difficulty

The values are volumes of regions of $I^m$ cut out by inequalities whose shape depends on the order of the coordinates, so a direct computation splits into $m!$ order cells, with the quota $c$ entering each. The paper's route avoids this by passing through the random function $F$, Theorem 2 and the Lemma; that route needs differentiation under the integral sign for a function that is only piecewise linear in $y$, with kinks at random locations, and an exact bookkeeping of the interval of integration when the quota approaches the ends of $[0, w(M) + \alpha]$. Theorem 6 is then an induction on $m$ that uses Theorem 5 for every player in turn, so it also needs the invariance of $\varphi_i$ under a relabelling of the major players.

Formalization scope

• Major players are Fin m ($m = 0$ is allowed; then $\Phi = 1$). The probability of an event is the Lebesgue volume of its intersection with $[0,1]^m$; no probability space is built.
• $P(t)$ uses the strict inequality $x_j < t$, as printed.
• $\varphi_i$ is defined as the volume of the pivot set (2.4), for every real quota. $\Phi$ is defined by (2.5), as the paper allows ("We might equally well take (2.5) as the definition of $\Phi$"). Neither is defined through the formulas of Theorem 6 or through $F$; defining them that way would make the goal an unfolding, and is ruled out.
• The paper writes (4.2) as a minimum $F(y) = \min\{x \mid w(P(x)) + \alpha x \ge y\}$, which need not be attained; $F$ is the infimum over $t \ge 0$, the value shown in its Fig. 3.
• The standing assumptions $w_j \ge 0$ and $\alpha > 0$ (§2) are explicit hypotheses. The p. 5 footnote's $0 \le c \le w(M)+\alpha$ applies to the pivot-set milestone. Other quota ranges are explicit: $0 \le y \le w(M) + \alpha$ for (4.3) and Theorem 2 (one-sided derivatives at the ends), the open interval for (4.4)–(4.5) (two-sided derivatives, stated with HasDerivAt), and $0 \le z \le w(M) + w_{m+1} + \alpha$ for the Lemma, as on p. 14.
• The added player is appended with Fin.snoc as index Fin.last m.
• Corollary (5.5) assumes $w_i > 0$, since it divides by $w_i$. Theorem 4, stated in the paper "in the general oceanic game", is false at quota $0$ and when the limit game has no winning coalition; it is stated for $0 < c \le w(M - \{i\}) + \alpha$.
• The identity of milestone 7 is pure algebra and is stated for all real weights and $\alpha \ne 0$.

A complete development needs: measurability of the pivot sets and of $F$ in $x$, the structure of $F$ as a piecewise linear function of $y$, differentiation of $E\{F\}$, and invariance of the values under permutations of the major players. The pivot-set and $F$ infrastructure is reusable for the companion mission on limits of finite weighted majority games. Contributions of any of the milestones, of the symmetry lemma, and of the non-milestone items are welcome.

Selected references

• J. W. Milnor and L. S. Shapley, Values of Large Games, II: Oceanic Games, The RAND Corporation, Research Memorandum RM-2649, February 1961. https://www.rand.org/pubs/research_memoranda/RM2649.html
• J. W. Milnor and L. S. Shapley, Values of Large Games II: Oceanic Games, Mathematics of Operations Research 3(4):290–307, 1978. https://doi.org/10.1287/moor.3.4.290
• 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, 307–317. https://doi.org/10.1515/9781400881970-018
• L. S. Shapley and N. Z. Shapiro, Values of Large Games, I: A Limit Theorem, The RAND Corporation, Research Memorandum RM-2648, November 1960.
• R. J. Aumann and L. S. Shapley, Values of Non-Atomic Games, Princeton University Press, 1974. https://doi.org/10.1515/9781400867080

Motivation

An isometric model of a graph assigns vectors to vertices so that vector distances reproduce shortest-path distances exactly. The choice of norm matters: a graph that needs many Euclidean coordinates may admit a smaller realization under a different norm. Linial, London, and Rabinovich used this freedom to study the dimension of graph metrics and related geometric questions in their 1995 paper on graph embeddings (Linial–London–Rabinovich, 1995). The complete graph is the first calibration point for the invariant. Every two distinct vertices are equally far apart, so the question becomes how many pairwise equidistant points an arbitrary real normed space of dimension $d$ can contain.

The answer is a sharp base-two logarithm. It separates the role of dimension from the particular shape of a norm's unit ball. In particular, a cube equipped with the supremum norm supplies many equidistant vertices, while no norm in the same dimension can accommodate more. Establishing both directions gives a reference case for more complicated graph metrics in the paper's Section 5.

Setting

A finite pseudometric space has a finite point set $X$ and a distance $\delta(x,y)\ge0$ that is symmetric, vanishes on the diagonal, and satisfies the triangle inequality. Distinct points may have distance zero, as the paper explicitly allows. A norm $N$ on $\mathbb R^d$ is nonnegative, vanishes only at the zero vector, is absolutely homogeneous, and satisfies the triangle inequality. It induces the distance $N(u-v)$ between vectors.

An isometric embedding of $(X,\delta)$ into a $d$-dimensional normed space is a map $\varphi:X\to\mathbb R^d$ with $N(\varphi(x)-\varphi(y))=\delta(x,y)$ for every pair. The isometric dimension $\dim(X,\delta)$ is the least $d$ for which such a norm and map exist. The norm may depend on $X$ and $d$; it is part of the realization rather than a fixed background choice. Lemma 5.1 of the paper states that every $m$-point metric space has an isometric realization in $\ell_\infty^m$, so this least dimension is taken over a nonempty set (Linial–London–Rabinovich, p. 229).

The complete graph $K_n$ has an edge between every pair of distinct vertices. Its shortest-path distance is zero from a vertex to itself and one between distinct vertices. An isometric realization of $K_n$ is therefore a collection of $n$ points whose pairwise distances are exactly one. The paper's Section 5 treats connected graphs, so this mission takes $n\ge1$. Its convention is that every logarithm has base two.

Formalization targets

Finite metric spaces have a realization

The foundational target is the paper's finite embedding statement:

$$|X|=m\quad\Longrightarrow\quad (X,\delta)\hookrightarrow\ell_\infty^m.$$

It establishes the domain on which the least-dimension definition has its intended meaning. The remaining milestones isolate the geometric assertions used for complete graphs: a difference-body inclusion, separation of the interiors of certain convex-hull translates, and a cardinality bound $n\le2^d$ for equilateral points in $\mathbb R^d$.

Complete graph dimension

The goal is Proposition 5.4 (Linial–London–Rabinovich, p. 231):

$$\dim(K_n)=\lceil\log_2 n\rceil\qquad(n\ge1).$$

The lower bound applies to every real norm on $\mathbb R^d$. The upper bound has the more specific target $K_n\hookrightarrow\ell_\infty^{\lceil\log_2 n\rceil}$. Both inequalities, including $n=1$ and dimension zero, are part of the mission.

Significance

The equation determines the optimal dimension for an equilateral finite metric space when the norm is unrestricted. It also bounds the size of an equilateral set in every $d$-dimensional real normed space by $2^d$, with equality attainable by vertices of a binary cube under the supremum norm. For graph metrics, it gives a precise baseline against which dimension bounds for trees, cubes, and other connected graphs can be compared. The surrounding section of the paper uses the same geometric vocabulary for those other families (Linial–London–Rabinovich, Section 5).

The mathematical result is proved in the 1995 paper. This mission asks for machine-checked Lean proofs of the specified statements. The local declarations presently encode open proof obligations; compilation checks their types and imports, but does not establish the theorems. A completed development would provide a reusable interface for finite isometric dimension and for equilateral configurations under arbitrary finite-dimensional norms.

Difficulty

The easy direction uses points of a binary cube. The difficult direction must hold uniformly over every possible norm, whose unit ball need not be round or smooth. A direct coordinate count cannot assume that vectors have bounded entries in a prescribed basis. The paper formulates its argument through the convex hull of an equilateral configuration and a comparison of translated sets (Linial–London–Rabinovich, p. 231). Its printed volume line also leaves a degenerate case: if that convex hull has zero volume in the ambient space, cancellation of $\operatorname{vol}(D)$ gives no numerical bound. A complete formal proof must account for such configurations without weakening the theorem to full-dimensional sets.

Formalization scope

The Lean representation of $\mathbb R^d$ is the function space Fin d → ℝ. A norm is an explicit function with all norm axioms, including definiteness and absolute homogeneity. Isometric dimension takes the infimum over dimensions admitting such a norm and an exact distance-preserving map. The complete graph is Mathlib's ⊤ : SimpleGraph (Fin n); its graph distance is converted to a real number. This distance is the discrete zero-or-one metric. The lower bound quantifies over every explicit norm. The cube milestone uses the supremum norm on finite real coordinate vectors. Convex hulls and interiors use the standard topology of this finite-dimensional vector space, which every norm induces.

The formal goal assumes $n\ge1$, matching the paper's connected-graph convention; $n=1$ remains included, with dimension zero. The logarithmic expression is Nat.clog 2 n, the ceiling of the base-two logarithm, rather than a floor or a real logarithm. The source uses no unspecified asymptotic constant in Proposition 5.4 or its listed milestones. The empty point space is allowed in the general finite embedding lemma; its pairwise claim is vacuous, while the nonempty cases carry the intended content. The dimension definition is only used for realizable finite distances, so a totalized infimum's value on an unrealizable function has no role in the target.

The exact norm axioms and exact distance equality prevent shortcuts through seminorms, truncated distances, or a weaker distortion bound. The cardinality theorem retains lower-dimensional affine configurations; assuming positive ambient volume would discard part of the result. A complete development needs finite pseudometric geometry, the supremum norm, convex hulls and interiors, and a dimension-sensitive measure argument. Those components are useful beyond this graph. The paper's independent results on degrees, trees, cubes, and other graph families, as well as algorithmic running-time claims elsewhere in the article, are outside this mission.

Selected references

• N. Linial, E. London, and Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2), 215–245 (1995). DOI: 10.1007/BF01200757.

Motivation

Discounted Markov decision problems are solved in practice by two classical schemes. Value iteration (successive approximations) is cheap per step but contracts the error only by the discount factor $\lambda$ per step, which is slow when $\lambda$ is close to $1$. Policy iteration (Howard, 1960) converges in few steps, but each step solves a linear system for the value of the current policy. Puterman and Brumelle (Mathematics of Operations Research, 1979) showed that policy iteration is Newton's method applied to the optimality equation.

Puterman and Shin (Management Science 24, 1978) interpolated between the two schemes: replace the exact policy evaluation by $k+1$ steps of successive approximation. This is modified policy iteration of order $k$. For $k=0$ it is value iteration; as $k\to\infty$ it approaches policy iteration. The paper proves that every order converges and bounds its rate. The scheme remains a standard algorithm in dynamic programming (Puterman, Markov Decision Processes, Wiley 1994, §6.5), and it appears in reinforcement learning as "optimistic" or "generalized" policy iteration.

Timeline. Howard (1960): policy iteration for finite problems. Puterman–Brumelle (1979, circulated earlier): policy iteration as Newton–Kantorovich iteration, and the support inequality for the optimality operator. van Nunen (1976) and van Nunen–Wessels: convergence of related value-oriented methods in a different framework. Puterman–Shin (1978): convergence of modified policy iteration of every order from a starting point with $Bv_0\ge 0$, and the rate bound formalized here.

Setting

$S$ is a set of states with a $\sigma$-algebra. A family $\mathcal P$ of policies is given. Each $P\in\mathcal P$ is a transition operator: a Markov kernel assigning to each state $s$ a probability distribution $P(s,\cdot)$ on $S$. Each policy also has a one-period reward $c_P:S\to\mathbb R$, and the rewards are uniformly bounded: $\sup_P\sup_s|c_P(s)|\le M<\infty$. The discount rate satisfies $0\le\lambda<1$.

$V$ is the Banach space of bounded measurable functions $v:S\to\mathbb R$ with $\|v\|=\sup_s|v(s)|$. A kernel acts on $V$ by $(Pv)(s)=\int v(t)\,P(s,dt)$. For linear $A$ on $V$, $\|A\|=\sup_{\|x\|\le 1}\|Ax\|$.

The optimality equation is

$$Bv\equiv\max_{P\in\mathcal P}\{c_P+(\lambda P-I)v\}=0. \tag{1}$$

The paper assumes throughout that the maximum in (1) is attained for every $v\in V$, by a single policy $P_v$ at every state.

For $k\ge 0$, the truncated Neumann series is $A^k_P=\sum_{i=0}^k(\lambda P)^i$. Modified policy iteration of order $k$ runs the recursion

$$v_{n+1}=v_n+A^k_{P_n}Bv_n, \tag{4}$$

where $P_n$ attains the maximum in (1) at $v_n$. A solution $v^*\in V$ of $Bv^*=0$ exists and is unique. $P^*=P_{v^*}$ denotes a policy attaining the maximum at $v^*$. The proofs also use the operators $U^kv=\max_P\{\sum_{i=0}^k(\lambda P)^ic_P+(\lambda P)^{k+1}v\}$ and the set $V_B=\{v\in V:Bv\ge 0\}$.

Formalization targets

Goal: Theorem 2, bound (8)

If $v_0\in V$ and $Bv_0\ge 0$, then for every $n$

$$\|v^*-v_{n+1}\|\ \le\ \min\Big\{\lambda,\ \frac{\lambda[1-\lambda^k]}{1-\lambda}\,\|P_n-P^*\|+\lambda^{k+1}\Big\}\,\|v_n-v^*\|. \tag{8}$$

Milestones

1. The support inequality (7): $Bw\ge Bv+(\lambda P_v-I)(w-v)$ for all $v,w\in V$.
2. Lemma 1: $U^k$ is a contraction with constant $\lambda^{k+1}$.
3. Lemma 2: $U^k$-iteration converges geometrically to the unique fixed point of $U^k$, and this fixed point solves $Bu=0$.
4. Lemma 3: $U^ku\ge(I+A^kB)v$ for $u\ge v$, and $(I+A^kB)u\ge U^0v$ if in addition $Bu\ge 0$.
5. Lemma 4: $V_B$ is invariant under $I+A^kB$.
6. Theorem 1: from $Bv_0\ge 0$, $\{v_n\}$ converges monotonically and in norm to $v^*$.
7. Corollary 1: $(U^0)^nv_0\le v_n\le (U^k)^nv_0$.
8. The two halves of (8): inequality (9), $\|v^*-v_{n+1}\|\le(\tfrac{\lambda[1-\lambda^k]}{1-\lambda}\|P_n-P^*\|+\lambda^{k+1})\|v^*-v_n\|$, and $\|v^*-v_{n+1}\|\le\lambda\|v^*-v_n\|$.

The mission also contains four further theorems that are not milestones: Corollary 2 (asymptotic rate at most $\lambda^{k+1}$ when $\|P_n-P^*\|\to 0$), Proposition 2 (monotonicity in the order $k$), the representation (6) $v_{n+1}=T_n^{k+1}v_n$, and Proposition 1 (policy iteration as Newton's method).

Significance

The result. Bound (8) gives two guarantees. Every order of modified policy iteration converges at least as fast as value iteration, with factor $\lambda$ per step. Once the improving policies stabilize near an optimal one, the factor approaches $\lambda^{k+1}$, the factor of $k+1$ value-iteration steps. This justifies spending $k$ cheap evaluation sweeps per policy improvement instead of solving a linear system. It also underlies the analysis of the many later variants: action elimination, asynchronous and approximate versions, and optimistic policy iteration in reinforcement learning.

Formalizing it. The theorems are proved on paper. As far as the platform's library shows, none of them is machine-checked: existing items cover value iteration and exact policy iteration for finite state spaces. This mission formalizes the whole chain on general measurable state spaces with Markov kernels, including the support inequality and the comparison operators $U^k$. Corollary 2 is stated as an upper bound only, because the equality printed on the page fails in degenerate runs (see the item's note).

Difficulty

The obvious route to a rate is the contraction argument for value iteration: $U^0$ is monotone and a $\lambda$-contraction, so its iterates converge geometrically. For $k\ge1$ that argument does not transfer to the map $v_n\mapsto v_n+A^k_{P_n}Bv_n$. The truncated series is taken for the policy chosen at the current point, so the map changes with $v_n$, and it is not monotone in general. The van der Wal–van Nunen example on p. 1133 of the paper shows that iterates of a higher order need not dominate those of a lower order from the same start. Moreover, without the condition $Bv_0\ge0$ the iterates need not even increase. A rate for (4) is therefore not a corollary of a fixed-point theorem for a single operator.

Formally, a second layer of difficulty is the setting itself. Everything happens in the space of bounded measurable functions on a general measurable space. So every operator applied to an iterate must be shown to preserve boundedness and measurability, and the maxima over policies are suprema over an arbitrary index set.

Formalization scope

The Lean development (namespace ModPolicyIter.Conv) represents:

• the policies as an index type $\iota$, policy $i$ being a Markov kernel P i : Kernel S S with a measurable reward c i, $|c_i|\le M$;
• $V$ by the predicate IsBM (measurable and bounded), with supNorm v = ⨆ s, |v s|;
• $P_iv$ as the Bochner integral against $P_i(s,\cdot)$;
• $B$ and $U^k$ as pointwise real suprema over $\iota$;
• $\|P_i-P_j\|$ as the supremum of $\|(P_i-P_j)x\|$ over the unit ball of $V$.

The standing assumptions of §2 are carried by the model fields; items using a maximizer assume either global attainment (MaxAttained) or an explicit maximizing policy. A run of (4) is a sequence of functions paired with a sequence of policies, each policy a maximizer at the current iterate. Only $v_0\in V$ is assumed; that later iterates lie in $V$ is part of the proofs.

Deviations from the page, all disclosed in the items:

1. Theorem 2 and its companions assume $Bv_0\ge0$, the hypothesis of Theorem 1, which the proof of Theorem 2 invokes.
2. Lemmas 1–2 and Corollary 1 assume that $U^k$ maps $V$ into $V$. This is implicit on the page, and for $k=0$ it follows from attainment. Lemma 1 states this mapping property alongside the contraction inequality.
3. The paper's $\mathcal P=\prod_s\mathcal P_s$ is generalized to an arbitrary index set.
4. Corollary 2 is stated as an upper bound.

The goal must not be trivialized by assuming $v_n\le v^*$, the support inequality, the sandwich of Corollary 1, or anything about $U^k$. These are milestones to be proved, and none of them is a hypothesis of the goal.

Reusable infrastructure includes Markov kernels as operators on bounded measurable functions (positivity, $\|P\|\le1$, measurability of $Pv$), completeness of $V$, and the Banach fixed point theorem on $V$. The first of these serves any discounted dynamic-programming mission on general state spaces. Contributions of any milestone, or of helper lemmas about these operators, are welcome.

Selected references

• M. L. Puterman and M. C. Shin, Modified policy iteration algorithms for discounted Markov decision problems, Management Science 24(11):1127–1137, 1978. https://doi.org/10.1287/mnsc.24.11.1127
• M. L. Puterman and S. L. Brumelle, On the convergence of policy iteration in stationary dynamic programming, Mathematics of Operations Research 4(1):60–69, 1979. https://doi.org/10.1287/moor.4.1.60
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• J. A. E. E. van Nunen, A set of successive approximation methods for discounted Markovian decision problems, Zeitschrift für Operations Research 20:203–208, 1976.
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887