The OR Formalization Drive

Why total tardiness on one machine

A shop that promises delivery dates is judged by how late its orders are, not by how early. For a single machine processing $n$ jobs that are all available at time $0$, the total tardiness of a processing order,

$$T=\sum_{i\in J}\max(0,\,C_i-d_i),$$

charges each job the amount by which its completion time $C_i$ exceeds its due date $d_i$, and nothing for finishing early. It is one of the basic criteria of deterministic scheduling (Conway, Maxwell and Miller, Theory of Scheduling, 1967), and the single-machine problem of minimizing it is the core subproblem of many dispatching and decomposition methods.

Two contrasting rules are classical. Sequencing in order of shortest processing time (SPT) minimizes total lateness $\sum_i (C_i-d_i)$ and total completion time (Smith, 1956), and it minimizes total tardiness when every job is tardy under it. Sequencing by earliest due date (EDD) minimizes total tardiness when at most one job is tardy under it. Between these extremes no simple rule is optimal, and before 1969 the proposed exact methods (Held and Karp, 1962; Lawler, 1964; Elmaghraby, 1968) searched subsets of schedules.

Timeline.

• 1956: Smith's ratio rule for weighted completion time; SPT for flow time and lateness.
• 1965: Root notes that SPT is optimal for total tardiness when all due dates are equal.
• 1969: Emmons (Operations Research 17(4)) proves dominance theorems that fix the relative order of pairs of jobs in some optimal schedule, and derives from them general sufficient conditions for SPT and EDD optimality.
• 1977: Lawler gives a pseudopolynomial algorithm, built on Emmons's dominance results (Annals of Discrete Mathematics 1).
• 1990: Du and Leung prove the problem NP-hard (Mathematics of Operations Research 15(3)), so sufficient conditions of Emmons's kind are the most one can expect from a simple rule.

This mission formalizes Emmons's SPT side: the pairwise dominance theorem for a shorter job before a longer one, and its corollary that the SPT schedule is optimal under a condition far weaker than "every job is tardy".

Setting

A finite set $J$ of jobs is processed on one machine. Job $i$ has a processing time $p_i\ge 0$ and a due date $d_i\in\mathbb R$. A schedule of $J$ is an ordering of the jobs of $J$; the machine starts at time $0$, never idles, and processes the jobs in that order, so a job's completion time $C_i$ is the sum of the processing times of the jobs up to and including it. Its tardiness is $T_i=\max(0, C_i-d_i)$, and the schedule's total tardiness is $T=\sum_{i\in J}T_i$. A schedule is optimal if no schedule of $J$ has smaller total tardiness.

Following Emmons, jobs are SPT-indexed: $J_1,\dots,J_n$ are numbered so that $j<k$ implies $p_j<p_k$, or $p_j=p_k$ and $d_j\le d_k$. The SPT schedule processes $J_1,J_2,\dots,J_n$ in this order.

Emmons's notation $j\leftarrow k$ ("$J_j$ precedes $J_k$ in an optimal schedule") means that there exists an optimal schedule having all properties already established and in which $J_j$ comes before $J_k$. The set $B_k$ collects the jobs already known to precede $J_k$.

Formalization targets

Goal: Corollary 1.4 (p. 705)

$$d_j+p_j\le\sum_{i=1}^{j+1}p_i\quad(j=1,\dots,n-1)\quad\Longrightarrow\quad\text{the SPT schedule minimizes } \sum_{i\in J}\max(0,C_i-d_i).$$

The condition can be read as $d_j\le C_j+(p_{j+1}-p_j)$ with $C_j$ the SPT completion time of $J_j$, so it allows jobs to be early. It is the paper's sufficient condition for SPT optimality, and the conclusion is optimality against every schedule of $J$.

Milestones

1. Interchange claim (proof of Theorem 1, p. 703): in a schedule where all of $B$ precede $J_k$ and $J_k$ precedes $J_j$, with $j<k$ and $d_j\le\max(\sum_{B}p_i+p_k,\,d_k)$, interchanging $J_j$ and $J_k$ does not increase total tardiness.
2. Theorem 1 (p. 703): if some optimal schedule has all of $B$ before $J_k$ and $d_j\le\max(\sum_{B}p_i+p_k,\,d_k)$, then some optimal schedule has all of $B$ before $J_k$ and also $J_j$ before $J_k$.
3. Corollary 1.1 (p. 704): if $d_1\le\max(p_i,d_i)$ for all $i>1$, then $J_1$ is first in an optimal schedule.
4. Time re-referencing (p. 705): processing $J_k$ first leaves the problem on $J\setminus\{J_k\}$ with due dates $d_i-p_k$.
5. First-job reduction (p. 705): $J_k$ followed by an optimal schedule of that reduced problem is optimal, whenever some optimal schedule starts with $J_k$.

Two further results are included as supporting statements: Corollary 1.2 (p. 705, $J_n$ last) and Corollary 2.3 (p. 707, the adjacent-pair rule $j\leftarrow k$ iff $d_j\le\max(W+p_k,d_k)$ after a waiting time $W$).

Significance

Corollary 1.4 turns an NP-hard problem into a closed-form answer on a recognizable class of instances: one pass over the SPT order checks the condition, and if it holds no search is needed. Theorem 1 is the more general tool. It orders pairs of jobs in an optimal schedule, and together with Emmons's companion theorems it underlies later exact methods for total tardiness, including Lawler's decomposition and the branch-and-bound algorithms that use Emmons's dominance rules for pruning.

The results are proved in the paper. What a formalization adds is a checked account of the step that the paper treats informally: dominance statements are existential ("some optimal schedule has $J_j$ before $J_k$"), and the paper argues on p. 702 that such statements can be accumulated. Each statement here makes explicit which previously established properties the new optimal schedule keeps. No machine-checked proof of these results was found on Prove2Me or in Mathlib at the time of drafting.

Difficulty

The obvious argument is a pairwise interchange, but the interchanged jobs are not adjacent. Moving $J_k$ from before $J_j$ to $J_j$'s position shifts every job in between, changes two tardiness terms in different directions, and the comparison depends on where the due dates fall relative to the start of $J_k$ and the end of $J_j$. The hypothesis involving $\sum_{B_k}p_i$ only controls the start time of $J_k$ through the information that $B_k$ precedes it, so the existence statement must carry that information along.

The goal is not a direct consequence of Theorem 1 applied pairwise: existential conclusions for different pairs need not hold in a common optimal schedule. Optimality of one fixed order requires all the pairwise decisions to be realized simultaneously, and the problem changes (due dates shift) once a job is fixed in place.

Formalization scope

Jobs are elements of a type $\iota$ with a linear order that plays the role of the paper's index, and the job set is a Finset ι; this lets the reduction remove a job and keep the remaining labels. Schedules and completion times are the published definitions MooreLateJobs.Shared.IsSchedule and MooreLateJobs.Shared.completionTime (duplicate-free lists containing exactly the jobs of $J$; prefix sums of processing times from time $0$). Tardiness, total tardiness, optimality (against every schedule of $J$), "precedes" (comparison of positions), the SPT indexing convention and the SPT schedule (the jobs sorted by index) are defined in EmmonsTardiness.SPT.Model. Processing times and due dates are real.

Conventions and deviations from the page:

• Added: processing times are nonnegative, $p_i\ge0$ for $i\in J$. They are durations; the proof of Theorem 1 uses that the start time of $J_k$ is at least $\sum_{B_k}p_i$, and Corollary 2.3's second direction is false without it.
• Not imposed: the reduction $d_i<\sum_J p_i$ of p. 703. It is a without-loss-of-generality preprocessing step that no statement needs, so dropping it makes the statements stronger.
• Kept: the SPT indexing convention of p. 703 is a hypothesis of every statement that refers to job indices.
• $j\leftarrow k$: the "properties already established" are the precedences named in hypothesis (1); the broader cumulative reading of p. 702 is not formalized.

A formalization of the goal as "some optimal schedule starts with $J_1$", or of Theorem 1 with an arbitrary set $B$ unrelated to optimal schedules, would be a different and weaker (or false) statement; the targets above state optimality of the SPT schedule itself and tie $B$ to an optimal schedule.

Needed infrastructure: lemmas on prefix sums of lists, on the effect of a transposition on positions in a duplicate-free list, on removing the head of a schedule, and existence of an optimal schedule among the finitely many permutations of $J$. These list-scheduling lemmas are reusable for other single-machine results (Moore 1968, and the EDD mission of this series). Proofs of the milestones, alternative arguments, and general interchange lemmas are all welcome.

Selected references

• H. Emmons, One-Machine Sequencing to Minimize Certain Functions of Job Tardiness, Operations Research 17(4):701–715, 1969. https://doi.org/10.1287/opre.17.4.701
• R. W. Conway, W. L. Maxwell, L. W. Miller, Theory of Scheduling, Addison-Wesley, 1967.
• W. E. Smith, Various Optimizers for Single-Stage Production, Naval Research Logistics Quarterly 3:59–66, 1956. https://doi.org/10.1002/nav.3800030106
• J. G. Root, Scheduling with Deadlines and Loss Functions on k Parallel Machines, Management Science 11:460–475, 1965. https://doi.org/10.1287/mnsc.11.4.460
• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1):102–109, 1968. https://doi.org/10.1287/mnsc.15.1.102
• E. L. Lawler, A "Pseudopolynomial" Algorithm for Sequencing Jobs to Minimize Total Tardiness, Annals of Discrete Mathematics 1:331–342, 1977. https://doi.org/10.1016/S0167-5060(08)70742-8
• J. Du, J. Y.-T. Leung, Minimizing Total Tardiness on One Machine is NP-Hard, Mathematics of Operations Research 15(3):483–495, 1990. https://doi.org/10.1287/moor.15.3.483

Motivation

Semidefinite programs (SDPs) arise as convex relaxations of combinatorial problems such as maximum cut and the Lovász theta function, and in control and eigenvalue optimization. Interior-point methods solve them reliably but manipulate dense $n\times n$ matrices, which limits the size of the instances they can handle. Burer and Monteiro (Math. Program. 95 (2003)) proposed replacing the matrix variable $X\succeq 0$ by a factorization $X=RR^{T}$ with $R$ having only $r$ columns, and solving the resulting nonconvex program by a first-order augmented Lagrangian method. The approach rests on a theorem of Barvinok (1995) and Pataki (1998): an SDP with $m$ linear constraints has an optimal solution of rank $r$ with $r(r+1)/2\le m$, so a small number of columns suffices.

Because the factorized problem is nonconvex, a local minimum it returns is not automatically a solution of the SDP. Section 2 of the paper gives conditions under which it is. This mission formalizes those conditions, culminating in Proposition 2.5, which justifies the paper's strategy of increasing the rank one column at a time.

Setting

For real $p\times q$ matrices, the trace inner product is $A\bullet B=\operatorname{trace}(A^{T}B)$. The data are symmetric matrices $C, A_1,\dots,A_m\in\mathcal S^n$ and a vector $b\in\mathbb R^m$. The primal SDP and dual SDP are

$$\text{(1)}\quad \min\{C\bullet X : A_i\bullet X=b_i,\ i=1,\dots,m,\ X\succeq0\},\qquad \text{(3)}\quad \max\Big\{b^{T}y : S=C-\sum_{i=1}^m y_iA_i,\ S\succeq0\Big\}.$$

The standing assumptions of the paper are that $A_1,\dots,A_m$ are linearly independent and that there are feasible $X^*$ and $(S^*,y^*)$ with $C\bullet X^*=b^{T}y^*$.

For a positive integer $r\le n$, the low-rank program is

$$(N_r)\qquad \min\{C\bullet(RR^{T}) : A_i\bullet(RR^{T})=b_i,\ i=1,\dots,m,\ R\in\mathbb R^{n\times r}\}.$$

Its Lagrangian is $L(R,y)=C\bullet(RR^{T})-\sum_i y_i(A_i\bullet(RR^{T})-b_i)$, and $S(y)=C-\sum_i y_iA_i$. A feasible $R$ is a local minimum if it minimizes the objective among nearby feasible points; it is a regular point if $A_1R,\dots,A_mR$ are linearly independent; it is a stationary point with multiplier $y$ if $\nabla_RL(R,y)=0$. The injection of $R\in\mathbb R^{n\times r}$ is $\hat R=[\,R\ \ 0\,]\in\mathbb R^{n\times(r+1)}$, obtained by appending a zero column.

Formalization targets

Goal: Proposition 2.5

Let $r<n$ and let $R^*$ be a regular local minimum of $(N_r)$ with multiplier $y^*$, $S^*=S(y^*)$, $S^*R^*=0$. If $\hat R$ is a local minimum of $(N_{r+1})$, then

$$X^*=R^*(R^*)^{T}\ \text{solves (1)}\quad\text{and}\quad (S^*,y^*)\ \text{solves (3)}.$$

Milestones

1. The derivative formulas (9): $\nabla_R(A_i\bullet(RR^T)-b_i)=2A_iR$, $\nabla_RL(R,y)=2SR$, and $L''_{RR}(R,y)[D,D]=2S\bullet(DD^T)$.
2. Proposition 2.3: at a regular local minimum of $(N_r)$ there is a unique $y^*$ with $S^*R^*=0$, and $S^*\bullet(DD^T)\ge0$ for every $D$ with $A_iR^*\bullet D=0$ for all $i$.
3. Proposition 2.1: feasible $X$ and $(S,y)$ are simultaneously optimal if and only if $X\bullet S=0$.
4. Proposition 2.4: a stationary point of $(N_r)$ whose $S^*$ is positive semidefinite gives optimal $X^*=R^*R^{*T}$ and $(S^*,y^*)$.

Significance

Proposition 2.5 is a certificate of global optimality for a nonconvex problem obtained from local information alone. It is the basis of the rank-increase scheme described on p. 8 of the paper: compute a local minimum of $(N_r)$ for a small $r$; if the zero-column extension is still a local minimum of $(N_{r+1})$, the current point solves the SDP; otherwise a better point of $(N_{r+1})$ exists and $r$ is increased. Proposition 2.4 gives the companion test, valid for every $r$: positive semidefiniteness of the multiplier matrix at a stationary point. These statements underlie the later convergence analysis of the method (Burer & Monteiro 2005) and the literature on benign landscapes of low-rank SDP formulations (Boumal, Voroninski & Bandeira 2016).

The results are proved in the paper. What this mission adds is a machine-checked version of the full chain from the standard-form SDP to the rank-increase certificate, including the matrix calculus (9), the first- and second-order necessary conditions for an equality-constrained program over rectangular matrices, and SDP complementary slackness in standard form. No machine-checked proof of these results is recorded in Mathlib or on the platform.

Difficulty

The SDP side (Propositions 2.1 and 2.4) is linear algebra: weak duality and the fact that the trace inner product of two positive semidefinite matrices is nonnegative. The substance lies in Proposition 2.3. The feasible set of $(N_r)$ is a variety cut out by $m$ quadratic equations, and the multiplier rule and, especially, the second-order necessary condition require a constraint qualification and a curve in the feasible set realizing every tangent direction. Mathlib provides a first-order Lagrange multiplier rule, but not the second-order condition on the tangent space. A naive attempt to read Proposition 2.5 off Proposition 2.4 fails: local minimality of $R^*$ alone does not make $S^*$ positive semidefinite (when $r$ is below the minimal optimal rank, it is not); the hypothesis on $(N_{r+1})$ is indispensable.

Formalization scope

Matrices are Matrix (Fin n) (Fin r) ℝ with 0-based indices. The trace inner product is frob A B = trace(Aᵀ * B), defined for rectangular matrices. The data carry explicit symmetry hypotheses C.IsSymm and (A i).IsSymm; without them the formulas (9) are false. Primal feasibility uses Mathlib's PosSemidef, which over $\mathbb R$ includes symmetry. Optimality for (1) and (3) is defined relative to their entire feasible sets. The standing assumptions are a separate predicate carried as a hypothesis by Propositions 2.1, 2.3, 2.4 and 2.5, and every statement about $(N_r)$ carries $0<r$ and $r\le n$ (or $r<n$). Gradients are Fréchet derivatives under the Frobenius norm, identified with matrices through the trace inner product; local minima use IsLocalMinOn on the feasible set of $(N_r)$ together with feasibility. The injection appends the zero column as the last column.

The statement admits several trivializing encodings, all excluded here: optimality defined relative to the factorized feasible set instead of the whole SDP, an empty or unconstrained $(N_r)$ (an unconstrained local minimum or a local minimum without feasibility), a stationarity notion that already includes $S\succeq0$, and an injection other than the zero-column extension.

A complete development needs the matrix calculus of $R\mapsto RR^{T}$, a second-order necessary optimality condition under linear independence of the constraint gradients, and standard-form SDP weak duality and complementary slackness; all of these are reusable well beyond this mission. Proofs of individual milestones, in particular the derivative formulas and Proposition 2.4, are welcome independently of the goal.

Selected references

• S. Burer and R. D. C. Monteiro, A nonlinear programming algorithm for solving semidefinite programs via low-rank factorization, Mathematical Programming 95 (2003), 329–357. https://doi.org/10.1007/s10107-002-0352-8 (statements cited from the authors' manuscript of March 9, 2001)
• A. Barvinok, Problems of distance geometry and convex properties of quadratic maps, Discrete & Computational Geometry 13 (1995), 189–202. https://doi.org/10.1007/BF02574037
• G. Pataki, On the rank of extreme matrices in semidefinite programs and the multiplicity of optimal eigenvalues, Mathematics of Operations Research 23 (1998), 339–358. https://doi.org/10.1287/moor.23.2.339
• R. D. C. Monteiro and M. Todd, Path-following methods for semidefinite programming, in Handbook of Semidefinite Programming, Kluwer, 2000 (source of Proposition 2.1).
• S. Burer and R. D. C. Monteiro, Local minima and convergence in low-rank semidefinite programming, Mathematical Programming 103 (2005), 427–444. https://doi.org/10.1007/s10107-004-0564-1
• N. Boumal, V. Voroninski and A. S. Bandeira, The non-convex Burer–Monteiro approach works on smooth semidefinite programs, NeurIPS 2016. https://arxiv.org/abs/1606.04970

Why posted prices

A seller who must decide whom to serve among several buyers with private values can, in principle, run Myerson's revenue-optimal mechanism: collect bids, compute virtual values, serve the feasible set of largest virtual surplus, and charge threshold payments (Myerson 1981). In practice sellers rarely do this. Retail, ticketing and online platforms mostly use posted prices: each buyer is offered a take-it-or-leave-it price and accepts if and only if the price does not exceed the buyer's value. Posted prices are simple to explain, are trivially truthful, and do not require buyers to reveal their values.

Chawla, Hartline, Malec and Sivan (arXiv:0907.2435, STOC 2010) asked how much revenue is lost by this simplification, and showed that for a wide range of feasibility constraints a sequential posted-price mechanism recovers a constant fraction of the optimal revenue. The matroid case, a factor of 2, is the first and most widely cited of their results. It is a revenue analogue of the prophet inequality and was one of the starting points of the literature on "simple versus optimal" mechanisms.

Setting

There are $n$ single-parameter agents, indexed by $[n]$, and one seller. Agent $i$ has a private value $v_i$ for being served, drawn independently from a distribution $F_i$ with density $f_i$. The virtual valuation of agent $i$ is

$$\phi_i(v_i) = v_i - \frac{1 - F_i(v_i)}{f_i(v_i)},$$

and $F_i$ is regular if $\phi_i$ is non-decreasing.

The seller faces a feasibility constraint: a downward-closed family $\mathcal J$ of subsets of $[n]$, the sets of agents that can be served together. The rank of a set $S$ is $\operatorname{rank}(S) = \max_{S' \subseteq S,\, S' \in \mathcal J} |S'|$. The constraint is a matroid if it satisfies the augmentation axiom: whenever $A, B \in \mathcal J$ and $|A| > |B|$, some $e \in A \setminus B$ has $B \cup \{e\} \in \mathcal J$. Examples are $k$ identical units ($k$-uniform matroids) and disjoint markets with separate capacities (partition matroids).

A mechanism $M$ maps reported values $\mathbf v$ to a feasible set $M(\mathbf v) \in \mathcal J$ of served agents and a payment $\pi_i(\mathbf v)$ for each agent. It is truthful if reporting the true value is a dominant strategy and no agent ends with negative utility. Its expected revenue is $\mathcal R^M = \mathbb E[\sum_i \pi_i(\mathbf v)]$, and $q^M_i = \Pr[i \in M(\mathbf v)]$ is the probability that it serves agent $i$.

A sequential posted-price mechanism (SPM) with ordering $\sigma$ and prices $\mathbf p$ approaches the agents in the order $\sigma$. When agent $i$'s turn comes, if adding $i$ to the set $A$ of agents served so far keeps $A$ feasible, $i$ is offered price $p_i$ and is served (and pays $p_i$) if $p_i \le v_i$; otherwise $i$ is blocked. Its expected revenue is $\mathcal R^\sigma_{\mathbf p}$.

The mechanism $\mathcal S$ of the paper sets $p_i = F_i^{-1}(1 - q^M_i)$, so that agent $i$ accepts an offer with probability exactly $q^M_i$, and approaches the agents in decreasing order of price.

Formalization targets

Goal: Theorem 5

For regular, independent values and a matroid constraint, for every truthful mechanism $M$ and the SPM $\mathcal S$ built from its service probabilities,

$$\mathcal R^M \le 2\, \mathcal R^\sigma_{\mathbf p}.$$

Taking $M$ to be Myerson's optimal mechanism gives the paper's statement that $\mathcal S$ 2-approximates the optimal revenue.

Milestones

1. Proposition 1 (p. 5): the expected revenue of a truthful mechanism equals its expected virtual surplus $\mathbb E[\sum_{i \in M(\mathbf v)} \phi_i(v_i)]$.
2. Lemma 2 (p. 5): $\mathcal R^M \le \sum_i p^M_i q^M_i$ with $p^M_i = F_i^{-1}(1 - q^M_i)$.
3. Revenue of an SPM (§2.2, p. 4): $\mathcal R^\sigma_{\mathbf p} = \sum_i c_i q_i p_i$, where $c_i$ is the probability that agent $i$ is offered service and $q_i = 1 - F_i(p_i)$.
4. Rank bound (§4, p. 6): $\sum_{i \in S} q^M_i \le \operatorname{rank}(S)$ for every set $S$.
5. Lost revenue (proof of Theorem 5, p. 7): in any run under a matroid, with prices in decreasing order and weights $q$ satisfying the rank bound, $\sum_{i \text{ blocked}} p_i q_i \le \sum_{i \text{ served}} p_i$.
6. Half of the benchmark (p. 7): under the same conditions, $\sum_i p_i q_i \le 2 \mathcal R^\sigma_{\mathbf p}$.

Significance

The theorem shows that under a matroid constraint the optimal mechanism's advantage over a single round of posted prices is at most a factor of 2, uniformly over all regular distributions. Prices, rather than an auction, then suffice up to a constant, which justifies posted pricing in settings where an auction is impractical. The same argument, with the matroid replaced by an intersection of $m$ matroids, gives the paper's Theorems 7 and 8, and the bound underlies the analysis of VCG with reserve prices (Theorem 32). Lemma 2's benchmark $\sum_i p^M_i q^M_i$ became a standard tool for "ex ante relaxation" arguments.

The results are proved in the paper; none of them has a machine-checked proof. Formalizing them requires Myerson's revenue characterization in a multi-agent, dominant-strategy setting with a general feasibility constraint, which Lean's libraries do not have, and a probabilistic analysis of a sequential process over a product measure. Related formalizations exist for narrower models: the single-unit, Bayesian incentive compatible revenue identity MechanismDesign.Auctions.revenue_eq_virtual_surplus (Börgers' textbook, common support) and the i.i.d. multi-unit RevenueManagement.revenue_equivalence. Neither covers per-agent supports, set-system constraints or dominant-strategy truthfulness.

Difficulty

The obvious argument compares the SPM with the hypothetical mechanism that ignores the feasibility constraint, whose revenue is exactly $\sum_i p_i q_i$. The SPM loses the revenue of agents who would have accepted but are blocked. The difficulty is that blocking is correlated with the values of earlier agents, and the lost revenue must be bounded by revenue actually collected. A naive per-agent charge fails in a general matroid, because one served agent can block many others; the bound has to use the matroid's rank structure together with the decreasing price order.

On the mechanism side, Lemma 2 needs the full Myerson theory: monotonicity of truthful allocations, the payment identity, and an optimization over interim allocation rules with a fixed service probability, where regularity is used.

Formalization scope

All objects live in the namespace CHMSPricing.SpmMatroid. Agents are Fin n. The following conventions are fixed.

• Distributions. Each $F_i$ is given by a measurable density, strictly positive on a bounded interval $[\underline v_i, \overline v_i]$ with $0 \le \underline v_i < \overline v_i$, integrating to $1$ there, with no mass outside. There are no point masses, so the randomized variant of $\mathcal S$ in §4 does not arise. The prior is the product measure.
• Regularity. Monotone non-decreasing virtual values on the support (Definition 2). All goals assume regular distributions, as the body's analyses do; the non-regular case (the second paragraph of Lemma 2, Appendix E) uses randomized prices and is out of scope.
• Truthfulness. Deterministic mechanisms, dominant-strategy incentive compatible with deviations within the support, ex-post individually rational, feasible on the type space, with measurable allocation events and measurable integrable payments. Payments of unserved agents are not forced to zero.
• Benchmark. The goal is stated for every truthful $M$, with $\mathcal S$ built from $M$'s own service probabilities; this is stronger than comparing with Myerson's mechanism alone and avoids constructing it.
• Prices. $p_i = F_i^{-1}(1 - q_i)$ is passed as an argument with the hypotheses $p_i \in [\underline v_i, \overline v_i]$ and $F_i(p_i) = 1 - q_i$, rather than through a generalized inverse.
• SPM. Positions are $0$-based; the price belongs to the agent; acceptance is $p_i \le v_i$; ties in the decreasing price order are arbitrary, and the goal holds for every such order.
• Proposition 1 additionally assumes the normalization that an agent with value $\underline v_i$ has zero utility, which is how the paper's payments are pinned down.

The goal cannot be trivialized by a free choice of prices: the prices are tied to the mechanism's service probabilities, and the SPM uses the same matroid as the mechanism. Individual rationality is essential, since without it a "truthful" mechanism can extract unbounded revenue.

A complete development needs Myerson's lemma for dominant-strategy single-parameter mechanisms, a quantile/revenue-curve argument under regularity, matroid span and rank facts for the paper's finite set systems, and independence arguments for a sequential process on a product measure. The rank bound and the deterministic lost-revenue inequality are independent of the probabilistic parts and are good first contributions; the Myerson-side lemmas are reusable for the other missions of this series.

Selected references

• S. Chawla, J. D. Hartline, D. Malec, B. Sivan, Multi-parameter Mechanism Design and Sequential Posted Pricing, arXiv:0907.2435v2, 2010; STOC 2010. https://arxiv.org/abs/0907.2435
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1):58–73, 1981. https://doi.org/10.1287/moor.6.1.58
• J. Bulow, J. Roberts, The Simple Economics of Optimal Auctions, Journal of Political Economy 97(5):1060–1090, 1989. https://doi.org/10.1086/261643
• R. Kleinberg, S. M. Weinberg, Matroid Prophet Inequalities, STOC 2012. https://arxiv.org/abs/1201.4764

Motivation

A seller who knows the distributions of buyers' values can maximise expected revenue with Myerson's optimal mechanism (Myerson 1981): collect bids, compute virtual values, serve a feasible set of maximum virtual surplus, and charge threshold payments. Real sellers seldom run such auctions. They post prices: a buyer is offered a take-it-or-leave-it price and either accepts or walks away. Posted prices need no bidding, involve no competition between buyers, and are trivially truthful. The question is how much revenue they give up.

Chawla, Hartline, Malec and Sivan (arXiv:0907.2435, STOC 2010) answer this for a range of feasibility constraints with a single construction, the sequential posted-price mechanism (SPM) $\mathcal S$. For general matroids it loses at most a factor $2$ (Theorem 5). For uniform and partition matroids, that is, multi-unit sales and unions of multi-unit sales, it loses at most a factor $e/(e-1)\approx1.58$ (Theorem 6), and the paper shows this factor is tight for its mechanism. This mission targets Theorem 6.

Timeline. Myerson (1981) characterised the optimal single-parameter mechanism. Blumrosen and Holenstein (2008) showed that the best single-unit SPM can be a factor $\sqrt{\pi/2}$ below Myerson's revenue even with i.i.d. buyers. Chawla, Hartline and Kleinberg (EC 2007) used posted prices to approximate multi-parameter unit-demand pricing. Chawla, Hartline, Malec and Sivan (2010) gave the matroid, partition-matroid and matroid-intersection bounds. Yan (SODA 2011) explained the $e/(e-1)$ factor through the correlation gap of submodular functions and sharpened it for $k$ units to $1-k^ke^{-k}/k!$.

Setting

There are $n$ agents. Agent $i$ has a private value $v_i$ for being served, drawn independently from a distribution $F_i$ with density $f_i$. The virtual value is $\varphi_i(v)=v-\frac{1-F_i(v)}{f_i(v)}$, and $F_i$ is regular if $\varphi_i$ is non-decreasing. The seller may serve any set in a downward-closed family $\mathcal J\subseteq2^{[n]}$.

A partition matroid assigns each agent $i$ to a part $\mathrm{part}(i)$ and each part $b$ a capacity $\mathrm{cap}(b)\in\mathbb N$. A set is feasible iff it contains at most $\mathrm{cap}(b)$ agents of every part $b$. With one part of capacity $k$ this is the $k$-uniform matroid: at most $k$ agents are served.

A truthful mechanism $M$ maps a value vector $\mathbf v$ to a feasible set $M(\mathbf v)$ and payments $\pi_i(\mathbf v)$. It is dominant-strategy incentive compatible and individually rational. Its expected revenue is $\mathcal R^M=\mathbb E[\sum_i\pi_i(\mathbf v)]$, and $q^M_i=\Pr[i\in M(\mathbf v)]$ is its service probability for agent $i$.

The sequential posted-price mechanism $\mathcal S$ built from $M$ sets the price $p_i=F_i^{-1}(1-q^M_i)$ for agent $i$, so that agent $i$ accepts with probability exactly $q^M_i$. It approaches the agents one at a time in decreasing order of price ($\sigma$ is the ordering). It offers agent $i$ the price $p_i$ if adding $i$ to the agents already served keeps the set feasible. The agent accepts iff $p_i\le v_i$. Its expected revenue is $\mathcal R^\sigma_{\mathbf p}$.

Formalization targets

Goal: Theorem 6, partition matroids

For every partition matroid, every truthful $M$, and $\mathcal S$ built from $M$ as above,

$$\mathcal R^M\le\frac{e}{e-1}\,\mathcal R^\sigma_{\mathbf p}.$$

Taking $M$ to be Myerson's mechanism gives the paper's statement.

Milestones

1. Lemma 2 (regular case): $\mathcal R^M\le\sum_ip^M_iq^M_i$ with $p^M_i=F_i^{-1}(1-q^M_i)$.
2. Rank bound (§4): $\sum_{i\in S}q^M_i\le\operatorname{rank}(S)$ for every set $S$; for a part $b$ this reads $\sum_{\mathrm{part}(i)=b}q^M_i\le\mathrm{cap}(b)$.
3. Single-unit revenue formula (App. C.2): $\mathcal R^{\mathcal S}=\sum_kc_kp_kq_k$ with $c_k=\prod_{j<k}(1-q_j)$, positions in offer order.
4. Lemma 20: with $p$ defined by $\sum_kp_kq_k=p\sum_kq_k$ (equation (2)) and prices decreasing, $p\sum_kc_kq_k\le\sum_kc_kp_kq_k$.
5. Display (3): if $\sum_kq_k=s\le1$, then $p\sum_kc_kq_k=p(1-\prod_k(1-q_k))\ge p(1-(1-s/n)^n)\ge(1-1/e)ps$.
6. Theorem 21: the goal for the $1$-uniform matroid.
7. Theorem 22: the goal for the $k$-uniform matroid, every $k$.

Significance

The theorem shows that a mechanism with no bidding loses at most about $37\%$ of the optimal revenue when the constraint is a union of multi-unit supplies. That covers selling several kinds of goods, each in limited stock, to single-minded buyers. The prices are computed once from the distributions. The order is fixed before any value is seen. No agent's payment depends on another agent's report. The factor is tight for this mechanism (App. C.2), and the same template (prices from service probabilities, decreasing order) gives factor $2$ for all matroids and $m+1$ for intersections of $m$ matroids.

On the formal side, the paper's results are proved but none is machine-checked as far as we know. The platform has Myerson-type results for a single unit with Bayesian incentive compatibility and a common support (Börgers), and for i.i.d. buyers with a fixed number of units (Talluri and van Ryzin). Neither covers independent, non-identical buyers under a set-system constraint with dominant-strategy truthfulness. A complete development would include the ex-ante revenue bound of Lemma 2 for regular distributions, which is reusable for any posted-price or prophet-inequality argument, and the $1-1/e$ correlation-gap inequality.

Difficulty

The obvious argument compares $\mathcal S$ with Myerson's mechanism one agent at a time. That fails, because $\mathcal S$ may stop offering to an agent once the units of its part are gone, and the agents blocked this way can be the ones Myerson's mechanism serves. The loss has to be bounded in aggregate, using only the ex-ante constraint $\sum_{\mathrm{part}(i)=b}q_i\le\mathrm{cap}(b)$. The single-unit case reduces to an inequality about products $\prod(1-q_j)$. For $k$ units, the printed proof (pp. 15–16) is an induction that compares the run with a hypothetical single-unit instance with probabilities $q_i/k$. Its second case is informal, so a formal proof needs its own argument for the $k$-unit bound. Passing from uniform to partition matroids needs the observation that with a global order the run inside each part depends only on that part's agents. Lemma 2 needs the revenue-curve concavity that regularity gives, stated through densities rather than derivatives.

Formalization scope

• Values. Each $F_i$ has a density that is measurable and strictly positive on a bounded interval $[\underline v_i,\bar v_i]$ with $0\le\underline v_i$, integrates to $1$ there, and has no mass outside. The paper says only "with density $f_i$". This pin rules out point masses, so the randomised-price variant of $\mathcal S$ never arises. The prior is the product of these laws.
• Regularity is $\varphi_i$ non-decreasing on the support, assumed for every agent in the goal, as in the paper's §4 analyses. The non-regular extension (second paragraph of Lemma 2, Appendix E) is out of scope.
• Truthful means deterministic, dominant-strategy incentive compatible over the support, ex-post individually rational, feasible, with measurable allocations and integrable payments.
• Prices are arguments tied to $M$ by $p_i\in[\underline v_i,\bar v_i]$ and $F_i(p_i)=1-q^M_i$. No inverse distribution function is defined.
• Order. The order $\sigma$ is a permutation with $\sigma(0)$ first, decreasing in price, and ties are arbitrary. It is global across parts. Parts of capacity $0$ are allowed.
• Constant. The constant is exactly $e/(e-1)$.
• No free prices. The theorem is not stated with free or existentially chosen prices. Prices are pinned to $M$'s service probabilities, and $\mathcal S$ uses the same constraint as $M$. A statement in which the prices could be chosen after the fact, or in which $M$ were not required to be individually rational, would be a different or false theorem.
• Every truthful $M$. The comparison is with every truthful $M$, not with a constructed Myerson mechanism. This form is at least as strong as the paper's, and it is what the paper's proof shows.

Welcome contributions: proofs of the algebraic milestones (Lemma 20, display (3)), the revenue formula, Lemma 2 (reusable payment-identity infrastructure for dominant-strategy mechanisms), and a correlation-gap argument for $k$ units.

Selected references

• S. Chawla, J. D. Hartline, D. L. Malec, B. Sivan, Multi-parameter Mechanism Design and Sequential Posted Pricing, STOC 2010; arXiv:0907.2435v2, 2010. https://arxiv.org/abs/0907.2435
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
• L. Blumrosen, T. Holenstein, Posted Prices vs. Negotiations: An Asymptotic Analysis, ACM EC 2008.
• Q. Yan, Mechanism Design via Correlation Gap, ACM-SIAM SODA 2011.

Motivation

Myerson's optimal auction (Myerson 1981) maximizes a seller's expected revenue when buyers have independent private values, but it is a sealed-bid mechanism: every buyer reports a value, and the allocation and payments are computed from all reports at once. Real sellers more often post prices: buyers arrive, each sees a take-it-or-leave-it price, and buys or leaves. Chawla, Hartline, Malec and Sivan (arXiv:0907.2435) ask how much revenue such simple mechanisms lose. Their strongest notion is the order-oblivious posted-price mechanism (OPM): the prices are fixed in advance, and the guarantee must hold whatever order the buyers arrive in, even an adversarial one.

The tool behind the guarantee for sellers of $k$ identical units is a prophet inequality. In the single-choice version, a gambler inspects independent random rewards one at a time and must accept or reject each on the spot; Krengel and Sucheston, and Samuel-Cahn (Ann. Probab. 1984), showed that a single fixed threshold earns at least half of what a prophet who sees all rewards earns. The paper extends Samuel-Cahn's threshold rule to $k$ choices (Appendix D.2) and turns it into a revenue guarantee (Theorem 10).

Setting

There are $n$ agents $[n]$. Agent $i$'s value $v_i$ for being served is drawn independently from a distribution $F_i$ with density $f_i$; the virtual valuation is $\phi_i(v) = v - (1 - F_i(v))/f_i(v)$ (Definition 1), and $F_i$ is regular if $\phi_i$ is non-decreasing (Definition 2). The seller may serve any set of agents in a downward-closed set system $\mathcal J$; this mission uses the $k$-uniform matroid, where a set is feasible exactly when it has at most $k$ members.

A mechanism $M$ maps reported values $\mathbf v$ to an allocation $M(\mathbf v) \in \mathcal J$ and payments $\pi_i(\mathbf v)$. It is truthful if reporting the true value is a dominant strategy and no agent ever gets negative utility. Its expected revenue is $\mathcal R^M = \mathbb E_{\mathbf v}[\sum_i \pi_i(\mathbf v)]$, and $\mathcal R^{\mathcal M}$ denotes the revenue of Myerson's mechanism, the largest over truthful mechanisms (Theorem 19).

Given prices $\mathbf p$ and values $\mathbf v$, agent $i$ desires service if $v_i \ge p_i$. Let $\mathcal S_{\mathbf v}$ be the class of maximal feasible sets of desiring agents. When agents arrive in an arbitrary order and each buys if it desires service and can still be feasibly served, the set of buyers lies in $\mathcal S_{\mathbf v}$. The paper's pessimistic revenue estimate is

$$\mathcal R^{\mathrm{obl}}_{\mathbf p} = \mathbb E_{\mathbf v \sim \mathbf F}\ \min_{S \in \mathcal S_{\mathbf v}} \sum_{i \in S} p_i .$$

For the prophet inequality, $X_1, \dots, X_n$ are independent nonnegative random variables with order statistics $X_{(1)} \ge \dots \ge X_{(n)}$, and $(x)^+ = \max(0, x)$. The threshold rule with threshold $c$ picks indices $t_1(c), \dots, t_k(c)$, where $t_i(c)$ is the lesser of $n-k+i$ and the $i$-th smallest index $j$ with $X_j \ge c$ (or $n - k + i$ if there is none). The numbers $a^*$ and $b^*$ are the unique solutions of

$$a = \sum_{i=1}^k \mathbb E\big(X_{(i)} - a/k\big)^+, \qquad b = \sum_{i=1}^n \mathbb E\big(X_i - b/k\big)^+ .$$

Formalization targets

Goal: Theorem 10 (p. 9)

$$\exists\, \mathbf p\ \ \forall M \text{ truthful}:\qquad \mathcal R^M \le 2\, \mathcal R^{\mathrm{obl}}_{\mathbf p}$$

for every instance with regular distributions and a $k$-uniform matroid constraint. The prices are chosen once, before the mechanism it is compared with; this is the paper's "$\mathcal R^{\mathrm{obl}}_{\mathbf p}$ 2-approximates $\mathcal R^{\mathcal M}$".

Milestones

1. Proposition 1 (p. 5): under regularity, the expected revenue of a truthful mechanism equals its expected virtual surplus $\mathbb E[\sum_{i \in M(\mathbf v)} \phi_i(v_i)]$ (with the lowest type receiving zero utility).
2. $a^*$ and $b^*$ exist and are unique (App. D.2, p. 18).
3. The claim $a^* \le b^*$ (App. D.2, p. 18).
4. Theorem 24 (p. 18), the $k$-choice prophet inequality: for $a^* \le k c \le b^*$,

$$\sum_{i=1}^k \mathbb E\big[X_{(i)}\big] \le 2 \sum_{i=1}^k \mathbb E\big[X_{t_i(c)}\big].$$

Significance

The theorem says that a seller of $k$ identical units can fix one price per buyer, ignore the arrival order entirely, and still collect half of the optimal revenue. The factor 2 is tight: Appendix D.2 gives a single-item example with two buyers where no order-oblivious pricing does better. Corollary 11 extends the result to partition matroids, and Theorem 24 is reused for the graphical-matroid result (Theorem 12, App. D.3). Theorem 24 is a statement in optimal stopping independent of mechanism design, and $k$-choice prophet inequalities are now a standard tool for online allocation.

The results are proved in the paper (preprint arXiv:0907.2435v2; a conference version appeared at STOC 2010). To our knowledge none of them, nor any prophet inequality, has a machine-checked proof; Mathlib has independence of random variables but no order statistics, stopping-rule prophet inequalities, or Myerson's revenue characterization in this multi-agent dominant-strategy form. A related single-unit, Bayesian-incentive-compatible form of Proposition 1 exists on the platform (MechanismDesign.Auctions.revenue_eq_virtual_surplus), in a different model.

Difficulty

The threshold rule picks the first values above $c$, not the largest, and its picks are dependent random indices; the expectation $\mathbb E[X_{t_i(c)}]$ does not factor. The obvious comparison of the gambler with the prophet term by term fails, because the gambler can exhaust its $k$ picks on early, small values. The bound has to balance two events: either at least $k$ values reach $c$, or a value is picked whenever it exceeds $c$; independence enters exactly in the second. The rule also has forced picks at the end of the sequence, which must be handled as stated.

On the mechanism side, $\mathcal R^{\mathrm{obl}}_{\mathbf p}$ is a minimum over an adversarially chosen family, not the revenue of one run, so it cannot be read off from a single sequential mechanism. Proposition 1 needs the full revenue-equivalence argument: monotone allocations, the payment identity, and an integration by parts against the density.

Formalization scope

• Distributions: each $F_i$ has a bounded support $[\underline v_i, \overline v_i]$ with $0 \le \underline v_i$, and a measurable density positive on it (a pinned convention; the paper says only "with density $f_i$"). Regularity is required on the support. The prior is the product of the marginals.
• Mechanisms: deterministic, dominant-strategy incentive compatible and ex-post individually rational on the type space, with measurable allocation events and measurable, integrable payments. Payments of unserved agents are not forced to be zero.
• $\mathcal R^{\mathcal M}$ is not constructed. The goal is stated against every truthful mechanism, which by Theorem 19 is equivalent. Quantifier order matters: "for every mechanism there are prices" is a weaker statement and is not the goal.
• Proposition 1 carries the normalization that an agent of the lowest type gets zero utility, which the paper presupposes on p. 12.
• $\mathcal R^{\mathrm{obl}}_{\mathbf p}$ is a genuine minimum over the finite, nonempty family $\mathcal S_{\mathbf v}$; maximality is essential, since without it the empty set makes the estimate $0$ and the goal false. Prices are arbitrary reals.
• $a^*$ and $b^*$ are characterised by their equations as hypotheses, not defined by an infimum. Order statistics count multiplicity. Lean indices are 0-based. The threshold rule includes the page's forced picks $t_i(c) = n - k + i$; it is not replaced by a pure threshold rule. Theorem 24 and the claims about $a^*, b^*$ assume $1 \le k \le n$; the goal assumes nothing about $k$.
• Out of scope: non-regular distributions (ironing), Corollary 11, and the p. 19 identity rewriting $\mathcal R^{\mathrm{obl}}_{\mathbf p}$ as a sum of virtual values (a proof step, not a milestone).

Useful reusable infrastructure: order statistics and their measurability, Samuel-Cahn-type threshold rules, and Myerson's payment identity for dominant-strategy mechanisms. Proofs of any milestone, and supporting lemmas on these objects, are welcome.

Selected references

• S. Chawla, J. D. Hartline, D. Malec, B. Sivan, Multi-parameter Mechanism Design and Sequential Posted Pricing, arXiv:0907.2435v2, 2010 (STOC 2010). https://arxiv.org/abs/0907.2435
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
• E. Samuel-Cahn, Comparison of Threshold Stop Rules and Maximum for Independent Nonnegative Random Variables, Annals of Probability 12(4), 1984. https://doi.org/10.1214/aop/1176993150

Motivation

(r, Q) policies are the standard replenishment rule for a single item under continuous review: whenever the inventory position (stock on hand plus on order minus backorders) drops to the reorder point $r$, an order of size $Q$ is placed. They are known to be optimal in the classical models with Poisson or compound renewal demand, constant or exogenous lead times and full backlogging, and they are used widely in practice and in multi-item and multi-echelon systems where they are applied item by item.

For decades, computing an optimal pair $(r, Q)$ exactly was not routine. The textbook treatment of Hadley and Whitin (1963) gives approximations; as Browne and Zipkin (1991) put it, "until recently, there was no reliable, straightforward method for computing an optimal (r, Q) policy, even in the simple case of Poisson demand processes." Many heuristics were proposed (surveyed by Lee and Nahmias, 1989); the only exact procedure in circulation was in Zipkin's classnotes, based on a result of Sahin (1982).

Federgruen and Zheng (1992) give a short exact algorithm, Algorithm OPT, whose work is linear in the optimal order quantity $Q^*$. It rests only on the form of the cost, not on a particular demand model.

Setting

Inventory positions are integers (demand arrives unit by unit). A fixed cost $\kappa>0$ is charged per order, and $G:\mathbb Z\to\mathbb R$ is the expected holding and backlogging cost rate as a function of the inventory position $y$. In all the models of the paper the long-run average cost of the $(r,Q)$ policy, for an integer $r$ and an integer $Q\ge1$, has the form

$$C(r,Q)=\Big[\kappa+\sum_{y=r+1}^{r+Q}G(y)\Big]\Big/Q. \tag{1}$$

The paper's standing assumptions on $G$ are:

1. $-G$ is unimodal: there is an integer $m$ with $G$ nonincreasing on $\{y\le m\}$ and nondecreasing on $\{y\ge m\}$ (flat stretches allowed);
2. $\lim_{|y|\to\infty}G(y)=\infty$.

The sequence $y_Q$. Let $y_1$ be an integer minimizing $G$. Given $y_1,\dots,y_Q$, let $L(Q)=\min\{y_1,\dots,y_Q\}$ and $R(Q)=\max\{y_1,\dots,y_Q\}$, and set

$$y_{Q+1}=\begin{cases}L(Q)-1 & \text{if } G(L(Q)-1)\le G(R(Q)+1),\\ R(Q)+1 & \text{otherwise.}\end{cases}$$

So the window $[L(Q),R(Q)]$ grows by one point at a time towards the smaller neighbouring value, ties going left. Write $r^*(Q)$ for an optimal reorder point for a given $Q$, and

$$C^*(Q)=\Big[\kappa+\sum_{i=1}^{Q}G(y_i)\Big]\Big/Q .$$

Algorithm OPT, Step 1. Variables $S,Q,C^*,r,R$ start at $S=\kappa+G(y_1)$, $Q=1$, $C^*=S$, $r=y_1-1$, $R=y_1+1$. Each pass compares $G(r)$ and $G(R)$; on the smaller side (left on ties) it stops if $C^*$ is at most that value, and otherwise adds the value to $S$ and moves $r$ one step left or $R$ one step right; then $Q:=Q+1$ and $C^*:=S/Q$. The output is the final $(r,Q)$.

Formalization targets

Goal: Theorem 1

Under the standing assumptions, Step 1 of Algorithm OPT, started from any global minimizer $y_1$ of $G$, stops after finitely many passes, and its output $(r,Q)$ satisfies $Q\ge1$ and

$$C(r,Q)\le C(r',Q')\qquad\text{for all integers } r' \text{ and all integers } Q'\ge 1 .$$

The goal fixes no constants and no demand model: it is a statement about every $G$ satisfying the standing assumptions.

Milestones, in proof order

• §2, p. 811: $\{y_1,\dots,y_Q\}$ is the contiguous block $[L(Q),R(Q)]$ of $Q$ integers and carries the $Q$ smallest values of $G$.
• Figure 1 (p. 809): $y_{Q+1}$ has the least $G$-value outside the window; in particular $G(y_1)\le G(y_2)\le\cdots$.
• Lemma 1: $L(Q)-1$ is an optimal reorder point for $Q$.
• Corollary 1: $r^*(Q)-1\le r^*(Q+1)\le r^*(Q)$.
• Display before (6): $\min_r C(r,Q)=C^*(Q)$.
• (6): $C^*(Q+1)=[QC^*(Q)+G(y_{Q+1})]/(Q+1)$, and $C^*(Q+1)<C^*(Q)$ iff $G(y_{Q+1})<C^*(Q)$.
• Lemma 2: the smallest $q$ with $C^*(q)\le G(y_{q+1})$ exists and is an optimal order size.
• Step 1 tracks the sequence: from the state $(\kappa+\sum_{i\le Q}G(y_i),\,Q,\,C^*(Q),\,L(Q)-1,\,R(Q)+1)$ one pass stops with $(L(Q)-1,Q)$ exactly when $C^*(Q)\le G(y_{Q+1})$ and otherwise moves to the same state for $Q+1$.

Significance

The result turns the joint minimization of (1) over $(r,Q)\in\mathbb Z\times\mathbb Z_{\ge1}$, an unbounded two-dimensional integer problem, into a single scan whose length is $Q^*$ plus the distance to the minimizer of $G$. Because it uses only the form (1) and the unimodality of $-G$, it applies at once to Poisson and compound Poisson demand, to stochastic lead times with an equilibrium lead-time demand, and to cost structures with stockout penalties; the paper also notes extensions to $(r,nQ)$ policies. Lemma 1 and Corollary 1 additionally give the structure of the optimal reorder point as a function of $Q$.

The result has been proved on paper since 1992. What this mission adds is a machine-checked proof of the algorithm's correctness for general $G$ under exactly the paper's hypotheses. The platform already has the linear-cost special case of the underlying lemmas for one discrete demand model (InventoryControl.rq_discrete_recursion, rq_discrete_joint_optimal), but with $C(Q)$ and $Q^*$ given as hypotheses and no algorithm; nothing on the platform states the algorithm or treats general unimodal $-G$.

Difficulty

The obvious argument says: for fixed $Q$ the sum in (1) should cover the $Q$ smallest values of $G$, and the greedy window collects exactly those. Both halves need care on the integers with flat stretches of $G$: "the $Q$ smallest values" is ambiguous under ties, and the claim that a greedy window holds them relies on $y_1$ being a global minimizer together with the unimodality of $-G$, not on convexity.

The stopping rule is the second point. Lemma 2 looks like a first-order condition, but $C^*(\cdot)$ need not be convex; optimality of the first stopping $q$ for all larger $Q$ uses that the values $G(y_i)$ are nondecreasing along the sequence, which the paper uses without stating. Termination of the algorithm is not discussed on the page; it needs $G\to\infty$, and fails for constant $G$.

Finally, the goal is about an imperative loop. Connecting its five variables to $y_Q$, $C^*(Q)$ and $L(Q)$ is an invariant argument that has to match the tie-breaking and the non-strict stopping tests exactly.

Formalization scope

• Types. $G:\mathbb Z\to\mathbb R$, $\kappa\in\mathbb R$ with $\kappa>0$, reorder points in $\mathbb Z$, order quantities in $\mathbb N$ with $Q\ge1$ required wherever a cost appears. Lean's $x/0=0$ makes $C(r,0)=0$, so optimality is always quantified over $Q'\ge1$ and the goal asserts that the returned $Q$ is $\ge1$.
• Assumptions. "$-G$ unimodal" is NegUnimodal G: $\exists m$, $G$ antitone on $(-\infty,m]$ and monotone on $[m,\infty)$. "$\lim_{|y|\to\infty}G=\infty$" is Coercive G: $G\to+\infty$ along atBot and atTop. Mathlib's QuasiconvexOn ℤ is not used: over $\mathbb Z$-weights it holds for every function.
• The sequence. $L(Q),R(Q)$ are defined by recursion on the window, and $y$ is 1-based with an unused value at index 0; that $L,R$ are the minimum and maximum of $\{y_1,\dots,y_Q\}$, as the paper defines them, is the first milestone.
• The algorithm. Step 1 is transcribed literally, including $G(r)\le G(R)$ → left and the non-strict tests $C^*\le G(r)$, $C^*\le G(R)$; $G$ is evaluated directly instead of through the $\Delta G$ bookkeeping. The loop runs with a pass budget and returns nothing when the budget runs out; the goal states that for every large enough budget it returns an optimal pair.
• Step 0 is not formalized. It scans $L=0,1,\dots$ for the first $L$ with $\Delta G(L)\ge0$, under the paper's simplification $y_1>0$; under unimodality alone it can stop on a plateau before the minimum. The goal starts Step 1 from a given global minimizer $y_1$, which is the paper's own §2 setup and matches its p. 812 remark that Step 0 may be replaced by a bisection search.
• Not formalized: Theorem 1's second sentence (the operation count), the derivations of (1) for specific demand models, and (5).
• Corrected slips. The printed proof of Lemma 2 writes $C(Q)-C(Q^*)$ with $C^*(Q)$ inside the bracket; the correct identity has $C^*(Q)-C^*(Q^*)$ and $C^*(Q^*)$. Lemma 2's "$Q^*$" is formalized as existence of the smallest $q$ with the property plus its optimality, since minimizers need not be unique; likewise "$r^*(Q)=L(Q)-1$" means $L(Q)-1$ is an optimal reorder point.
• Ruled out. Defining the algorithm's output as an argmin of $C$, or by searching for Lemma 2's $q$, would make the goal trivial; the algorithm is defined by its steps. A statement of the form "if the run returns a pair, it is optimal" would be vacuous for a loop that never stops; termination is part of the goal.

Proofs of any milestone are welcome, as are general lemmas on windows of unimodal integer sequences, which are reusable beyond this mission.

Selected references

• A. Federgruen and Y.-S. Zheng, An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4):808–813, 1992. https://doi.org/10.1287/opre.40.4.808
• G. Hadley and T. M. Whitin, Analysis of Inventory Systems, Prentice-Hall, 1963.
• S. Browne and P. Zipkin, Inventory Models with Continuous, Stochastic Demands, Annals of Applied Probability 1(3):419–435, 1991. https://doi.org/10.1214/aoap/1177005875
• H. L. Lee and S. Nahmias, Single-Product, Single-Location Models, in Handbooks in OR & MS vol. 4, 1993 (cited by the paper as a 1989 working paper).
• I. Sahin, On the Objective Function Behavior in (s, S) Inventory Models, Operations Research 30(4):709–724, 1982. https://doi.org/10.1287/opre.30.4.709

Motivation

The dynamic lot size model asks when, and how much, to order of a single item over a planning horizon of $n$ periods with known, time-varying demands, setup costs, unit order costs and holding costs. It is the textbook model of production planning and the building block of material requirements planning, multi-item scheduling and many decomposition schemes for larger supply-chain problems.

Wagner and Whitin (1958) showed that some optimal policy orders only when inventory is zero, which turns the problem into a shortest-path recursion with $O(n^2)$ running time. For more than thirty years this was the standard algorithm. In 1991 three groups independently reduced the complexity: Federgruen and Tzur (Management Science 37(8), 1991), Wagelmans, van Hoesel and Kolen (Operations Research 40, 1992) and Aggarwal and Park (Operations Research 41, 1993). Each obtained $O(n \log n)$ in general and $O(n)$ under special cost structures. The Federgruen–Tzur algorithm is a forward algorithm: at iteration $j$ it keeps a short list of periods that could still be the best last setup period for some future horizon, and updates it by local tests on neighbouring entries. This mission formalizes the theorem that justifies those tests.

Setting

For periods $i = 1, 2, \dots$ let $d_i$ be the demand, $K_i$ the setup cost, $c_i$ the variable per unit order cost and $h_i$ the cost of carrying a unit of inventory at the end of period $i$. Write $D(i) = \sum_{k=1}^{i} d_k$ and $H(i) = \sum_{k=1}^{i} h_k$, so $D(0) = H(0) = 0$. For $i < j$ let $c_{ij} = c_i + h_i + \dots + h_{j-1}$, let $\tilde C(i) = c_i - H(i-1)$, and let

$$S(i, j) = \sum_{r=i}^{j-1} h_r\,\bigl(D(j) - D(r)\bigr)$$

be the carrying cost of an order placed in period $i$ that covers the demands of periods $i, \dots, j$.

The costs are given by the zero-inventory recursion (2): $F(0) = 0$ and, for $1 \le l \le t$,

$$F(l, t) = F(l-1) + K_l + S(l, t) + c_l\,[D(t) - D(l-1)], \qquad F(t) = \min_{1 \le l \le t} F(l, t).$$

$F(l, t)$ is the cost of the first $t$ periods when the last setup is in period $l$.

For two periods $k < l$ the difference $\Delta_{k,l}(t) = F(k,t) - F(l,t)$ is affine in $D(t)$, with intercept $A(k,l)$ given by (4) and slope $c_{k,l} - c_l = \tilde C(k) - \tilde C(l)$. Its root $G(k,l)$ is defined by (5): $A(k,l)/(\tilde C(l) - \tilde C(k))$ when the slopes differ, and $+\infty$ or $-\infty$ according to the sign of $A(k,l)$ when they agree. It is extended symmetrically, $G(l,k) = G(k,l)$.

At iteration $j$ the future demands are unknown, so a future horizon has a potential cumulative demand $x \ge D(j)$. The $j$th Minimal Optimal Predecessors list $\Omega(j)$ is the set of periods $l \le j$ that are the lowest-index optimal last setup period, among $\{1, \dots, j\}$, for every potential cumulative demand in some open interval above $D(j)$.

Formalization targets

Goal: Theorem 1(a)

Let $j \ge 1$ and let $S = \{i_1, \dots, i_r\}$ with $\Omega(j) \subseteq S \subseteq \{1, \dots, j\}$, ranked so that $\tilde C(i_1) \ge \dots \ge \tilde C(i_r)$, with equal $\tilde C$-values in ascending order of index. Put $g(1) = D(j)$ and $g(l) = G(i_l, i_{l-1})$ for $l = 2, \dots, r$. Then

$$S = \Omega(j) \iff g(1) < g(2) < \dots < g(r) < \infty. \tag{6}$$

Milestones

In attack order:

• identity (1a) for the carrying costs;
• Lemma 2(a)–(d), the linearity of $\Delta_{k,l}$ and the sign test against its root $G(k,l)$;
• the claim that $\Omega(j)$ contains an optimal last setup period for the horizon $j$;
• the strict chains (7)–(8) of the Appendix;
• Theorem 1(b), that under (6) the first entry $i_1$ is an optimal last setup period $l(j)$;
• Theorem 1(c)(i)–(iii), the three elimination rules: $g(2) \le D(j)$ removes $i_1$, $g(k+1) \le g(k)$ removes $i_k$, and $g(r) = \infty$ removes $i_r$.

A supporting item potCost_spec certifies that the potential costs used to define $\Omega(j)$ agree with the paper's $F(l,t)$, up to a term that does not depend on $l$.

Significance

Theorem 1 is what makes the forward algorithm correct. Part (a) reduces the minimality of a candidate list to a condition on consecutive pairs of a sorted list. Part (c) says which entry to delete when the condition fails. Part (b) says where to read off the optimal last setup period. With these, $\Omega(j)$ is maintained by deletions at the ends and in the interior of a list ordered by $\tilde C$, and each period is inserted and deleted at most once; the $O(n \log n)$ bound, and the $O(n)$ bound under the paper's special cost structures, follow from this bookkeeping. The same lower-envelope reasoning appears in the other 1991–1993 algorithms and in later extensions to backlogging and capacitated variants.

The result has a complete published proof. To our knowledge there is no machine-checked development of the Wagner–Whitin recursion or of any of the fast lot-sizing algorithms. This mission produces the model, the breakpoints and the Minimal Optimal Predecessors lists as reusable definitions, and a checked proof of the characterization. It also records two small corrections that a formal reading forces on the printed text (see Formalization scope).

Difficulty

Each piece in isolation is elementary algebra on affine functions. The difficulty is in the combinatorics of the lower envelope with ties. The natural argument "consecutive breakpoints increase, so each line owns an interval" must handle three things:

• equal slopes, where $G = \pm\infty$;
• several lines meeting at one point;
• the lowest-index tie-breaking that makes $\Omega(j)$ minimal.

The "only if" direction needs every failure of (6) to be traced to an element that is never the unique lowest-index optimum on an interval. Ties are exactly where the printed definition of $\Omega(j)$, read literally at a single demand value, breaks the theorem. A proof that ignores ties proves a statement that is false.

Formalization scope

• Data and costs. The data are four functions $\mathbb N \to \mathbb R$ bundled in a structure; values at index $0$ are unused, and no sign conditions are imposed. $F$ is defined by the recursion (2) with $F(0) = 0$. Its identification with the minimum cost over all feasible policies is the paper's Lemma 1 (Wagner–Whitin), which is not part of this mission. The horizon $n$ is not a parameter.
• Breakpoints. $G$ and the critical values $g(\cdot)$ take values in EReal, so $\pm\infty$ are kept distinct from every real number. The final "$< \infty$" of (6) is part of the condition.
• Ranked lists. A ranked set is a duplicate-free List ℕ. Lean lists are 0-based, so the paper's $i_{m+1}$ and $g(m+1)$ are entry $m$ and gval j L m.
• Disclosed change 1, $\Omega(j)$. The page asks for a single potential cumulative demand $D \ge D(j)$ at which $l$ is the lowest-index optimum. With that reading, Theorem 1(a) "only if" and Theorem 1(c) fail when two lines tie exactly at a breakpoint (an explicit five-period instance is in the definition's note). The formalization requires $l$ to be the lowest-index optimum on a nondegenerate open interval of potential demands above $D(j)$. This is the paper's own description of the list on p. 915: "the unique optimal last setup period for any horizon … with potential cumulative demand $g(k) < D < g(k+1)$".
• Disclosed change 2, Lemma 2(d). The printed hypothesis "$c_{k,l} < c_l$" duplicates part (c) and is read as "$c_{k,l} = c_l$". The equivalence "$\Delta_{k,l} \ge 0$ iff $D(t) \ge G(k,l)$" is stated under $A(k,l) \ne 0$, since $A(k,l) = 0$ gives $G = +\infty$ by (5).
• Ruling out trivial formalizations. The hypotheses of the goal are satisfiable for every $j \ge 1$: rank $\{1, \dots, j\}$ itself. $\Omega(j)$ is nonempty (a milestone). $F(t)$ for $t \ge 1$ is a minimum over the nonempty set $\{1, \dots, t\}$, never a default value. $G$ is never replaced by a real-valued junk value at equal slopes.
• Out of scope. Lemma 1, Lemma 3, Corollaries 1–5, Theorem 2, the Algorithm's pseudo-code and its complexity analysis, and the submodularity discussion of §5.
• Reusable infrastructure. The model, the recursion (2), $A$, $G$ and $\Omega(j)$ can be reused for the paper's algorithmic results and for related lot-sizing papers. Proofs of the milestones, in any order, are welcome.

Selected references

• A. Federgruen and M. Tzur, A Simple Forward Algorithm to Solve General Dynamic Lot Sizing Models with n Periods in O(n log n) or O(n) Time, Management Science 37(8):909–925, 1991. https://doi.org/10.1287/mnsc.37.8.909
• H. M. Wagner and T. M. Whitin, Dynamic Version of the Economic Lot Size Model, Management Science 5(1):89–96, 1958. https://doi.org/10.1287/mnsc.5.1.89
• A. Wagelmans, S. van Hoesel and A. Kolen, Economic Lot-Sizing: An O(n log n) Algorithm That Runs in Linear Time in the Wagner-Whitin Case, Operations Research 40(1-supplement-1):S145–S156, 1992. https://doi.org/10.1287/opre.40.1.S145
• A. Aggarwal and J. K. Park, Improved Algorithms for Economic Lot Size Problems, Operations Research 41(3):549–571, 1993. https://doi.org/10.1287/opre.41.3.549