The OR Formalization Drive

Motivation

Firms that sell new products (consoles, books, films) often take preorders before release. A preorder serves two purposes at once. It lets the firm charge early adopters a different price from later buyers, a form of price discrimination, and the number of preorders is advance demand information: an early signal of how large regular-season demand will be. Li and Zhang (MSOM 15(1), 2013) ask whether better advance information always helps a seller who runs a preorder, when consumers are strategic and anticipate the seller's stocking decision. Their answer is no. The second-period stocking decision improves, but the preorder price can fall. Whether the net effect is positive depends on the low-type margin and the size of the early-adopter segment.

This mission formalizes that answer, §4 of the paper: the preorder profit as a function of the demand correlation $\rho$.

Setting

A seller sells a perishable product over two periods. High-type consumers, with valuation $v_H$, arrive in the first period and may preorder at price $p_1$. Low-type consumers, with valuation $v_L < v_H$, arrive in the second period, when the price is $p_2$. A high type who waits values the product at $\delta v_H$, where $\delta \le 1$ and $\delta v_H > v_L$. The unit cost is $c$, with $0 < c < v_L$. Unsold units have no salvage value and unmet demand carries no penalty. Write $\Delta = \delta v_H - v_L$.

The demands are jointly normal with correlation $\rho \in [0,1)$. The high-type demand has mean $\mu_H$, and $X$ denotes its standardization, a standard normal variable. The low-type demand has mean $\mu_L$, standard deviation $\sigma_L$ and $\lambda_L = \mu_L/\sigma_L$. Given $X = x$, the updated low-type demand $\tilde X_L(x)$ is normal with mean $\tilde\mu_L(x) = \mu_L + \rho\sigma_L x$ and standard deviation $\tilde\sigma_L = \sigma_L\sqrt{1-\rho^2}$. $\Phi$ and $\phi$ are the standard normal distribution function and density, and $z_L$ solves $\Phi(z_L) = (v_L - c)/v_L$.

In the second period the seller charges $p_2 = v_L$ and solves a newsvendor problem. It orders

$$Q(x) = \tilde\mu_L(x) + z_L\tilde\sigma_L \qquad (1)$$

and earns $\Pi_L(x) = (v_L - c)(\mu_L + \rho\sigma_L x) - v_L\phi(z_L)\sigma_L\sqrt{1-\rho^2}$ (2). A waiting high type believes half of the remaining consumers will be served before her, so her belief of product availability is

$$\xi(\rho) = \mathbb E\Big[\Pr\Big(\tfrac{\tilde X_L(X)}{2} < Q(X)\Big)\Big]. \qquad (3)$$

In the rational-expectations equilibrium every high type preorders at $p_1 = v_H - \Delta\xi$. The preorder profit is

$$\Pi^p(\rho) = (v_H - \Delta\xi(\rho) - c)\mu_H + \Pi_L(0). \qquad (4)$$

The threshold is

$$\tilde\mu(\rho) = -\frac{v_L\phi(z_L)\sigma_L}{2\Delta z_L\,\phi\big(2z_L\sqrt{1-\rho^2} + \lambda_L\big)}. \qquad (6)$$

Formalization targets

Goal: PROPOSITION 2

$$\begin{aligned} &\text{(i) } c < v_L < 2c:\ \Pi^p \text{ strictly increases on every interval where } \mu_H < \tilde\mu(\rho),\\ &\qquad\text{and strictly decreases on every interval where } \mu_H \ge \tilde\mu(\rho);\\ &\text{(ii) } v_L \ge 2c:\ \Pi^p \text{ strictly increases on } [0,1). \end{aligned}$$

Milestones

1. (1)–(2): $Q(x)$ is the unique maximizer of $\mathbb E[v_L\min(Q,\tilde X_L(x)) - cQ]$, and its value is $\Pi_L(x)$.
2. (3): $\xi(\rho) = \mathbb E\big[\Phi\big((\lambda_L + \rho X)/\sqrt{1-\rho^2} + 2z_L\big)\big]$.
3. LEMMA 1(i): if $c < v_L < 2c$, then $z_L < 0$ and $\xi$ is strictly increasing in $\rho$.
4. LEMMA 1(ii): if $v_L \ge 2c$, then $z_L \ge 0$ and $\xi$ is non-increasing in $\rho$, strictly so when $v_L > 2c$.
5. After (5): $\dfrac{d}{d\rho}\Pi_L(0) = v_L\phi(z_L)\sigma_L\,\rho/\sqrt{1-\rho^2} > 0$ for $\rho \in (0,1)$.
6. PROPOSITION 2(i), pointwise: for $\rho \in (0,1)$, $d\Pi^p/d\rho > 0 \iff \mu_H < \tilde\mu(\rho)$ and $d\Pi^p/d\rho < 0 \iff \mu_H > \tilde\mu(\rho)$.
7. LEMMA 2(i): if $-\lambda_L/2 < z_L < 0$, then $\tilde\mu$ is strictly increasing in $\rho$.
8. LEMMA 2(ii): if $z_L \le -\lambda_L/2$, then $\tilde\mu$ is quasi-convex in $\rho$.

Significance

The proposition splits the value of advance demand information into two effects with opposite signs. Better information always raises the second-period profit (milestone 5). Its effect on the preorder price depends on the margin. When $v_L < 2c$, the seller stocks below the conditional mean. A more precise forecast then raises the stock and the availability $\xi$, and waiting becomes more attractive, which lowers the preorder price. The threshold $\tilde\mu(\rho)$ says which effect wins, and LEMMA 2 describes its shape. This is the basis for the paper's later comparisons of preorder, price-guarantee and no-preorder strategies.

The paper states these results and leaves the proofs to an online appendix. None of them has a machine-checked proof. A complete development would also give reusable facts about normal laws: the expectation $\mathbb E[\Phi(a + bX)]$ for standard normal $X$, the normal newsvendor solution with its closed-form optimal profit, and derivatives of Gaussian integrals with respect to a correlation parameter.

Difficulty

The model is explicit, so the difficulty is not in modelling. It is in turning the two expectations into closed forms and differentiating them. The availability $\xi$ is an integral over $X$ of a normal probability whose mean and variance both move with $\rho$. The expected newsvendor profit involves $\mathbb E[\min(Q, Y)]$ for a normal $Y$. Neither closed form is in Mathlib, and neither is a derivative in $\rho$ of a Gaussian integral. The obvious route, differentiating under the integral sign in (3), needs domination estimates that are uniform in $\rho$ near each point, and these degenerate as $\rho \to 1$.

Signs are the second difficulty. $z_L$ changes sign at $v_L = 2c$, $\tilde\mu$ carries a leading minus and divides by $z_L$, and the derivative of $\Pi^p$ vanishes at $\rho = 0$ and wherever $\tilde\mu(\rho) = \mu_H$. Strict monotonicity on an interval has to be recovered from a derivative that is positive except at finitely many points.

Formalization scope

Everything lives in the namespace PreorderADI.Correlation. A structure Params holds $v_H, v_L, c, \delta, \mu_H, \mu_L, \sigma_L, z_L$. The predicate Params.Standing records the model's assumptions: $v_H > v_L$, $c < v_L$, $\delta \le 1$ and $\delta v_H > v_L$, together with $\Phi(z_L) = (v_L-c)/v_L$. $\sigma_H$ is omitted because nothing in §4 uses it after standardization. $\Phi$ is ProbabilityTheory.cdf (gaussianReal 0 1) and $\phi$ is gaussianPDFReal 0 1. The normal law with mean $m$ and standard deviation $s$ is gaussianReal m (s^2).

The formalization commits to the following conventions and additions:

• Added hypotheses. Four hypotheses are added to the page's assumptions:
  • $c > 0$, so that $z_L$ exists;
  • $\sigma_L > 0$, so that the conditional law is a genuine normal law;
  • $\mu_L > 0$, so that $\lambda_L > 0$, as LEMMA 2 presupposes;
  • $\mu_H > 0$, which PROPOSITION 2(ii) needs.
• $z_L$. $z_L$ is a parameter pinned down by $\Phi(z_L) = (v_L-c)/v_L$, not an inverse function with junk values.
• Range of $\rho$. $\rho$ ranges over $[0,1)$, the paper's "we will focus on $\rho \ge 0$" together with $\rho < 1$. Derivative statements use $(0,1)$.
• $\xi$ and $\Pi^p$. $\xi$ is defined as the first expression of (3), the expected probability, so that no closed form is assumed. $\Pi^p$ is defined by (4). PROPOSITION 1, which derives (4) as the unique equilibrium profit, is not formalized: the paper defines the equilibrium only through conditions that already assume every high type preorders.
• Monotonicity. "Increases in $\rho$ when $\mu_H < \tilde\mu(\rho)$" is formalized as strict monotonicity on every order-connected $I \subseteq [0,1)$ on which the condition holds. "Decreasing" in LEMMA 1(ii) is non-strict, since $\xi$ is constant when $v_L = 2c$. Quasi-convexity is Mathlib's QuasiconvexOn.
• The ε_v sentence is omitted. PROPOSITION 2(i) also claims that some $\varepsilon_v > 0$ makes $\Pi^p$ always decrease when $v_L < c + \varepsilon_v$. That claim is false in the paper's own model. As $v_L \downarrow c$, $\tilde\mu(\rho) \to \infty$ for $\rho$ below roughly $\sqrt 3/2$, so $\Pi^p$ increases there for every fixed $\mu_H$. The paper's Figure 1 shows the same behaviour.
• Out of scope. §5 rests on an approximation that treats normal demands as nonnegative, so it is excluded. §§6–7 depend on models given only in the online appendix and are excluded too.

A statement about the closed form $\Phi(\lambda_L + 2z_L\sqrt{1-\rho^2})$ in place of $\xi$ would make LEMMA 1 a one-line monotonicity fact. So would a definition of $\Pi^p$ that bypasses (3). The definitions rule both out.

Welcome contributions include proofs of the milestones, general Mathlib-style lemmas on Gaussian expectations of $\Phi$ and of $\min(Q, Y)$, and a formalization of PROPOSITION 1 from conditions (i)–(v).

Selected references

• C. Li and F. Zhang, Advance Demand Information, Price Discrimination, and Preorder Strategies, Manufacturing & Service Operations Management 15(1):57–71, 2013. https://doi.org/10.1287/msom.1120.0398
• G. P. Cachon and R. Swinney, Purchasing, Pricing, and Quick Response in the Presence of Strategic Consumers, Management Science 55(3):497–511, 2009. https://doi.org/10.1287/mnsc.1080.0948
• X. Su and F. Zhang, On the Value of Commitment and Availability Guarantees When Selling to Strategic Consumers, Management Science 55(5):713–726, 2009. https://doi.org/10.1287/mnsc.1080.0967

Motivation

A monotone variational inequality asks for a point at which a monotone operator and a convex function are in equilibrium. It unifies convex minimization (where $F$ is a gradient), convex–concave saddle-point problems (where $F$ is the skew gradient of a Lagrangian), Nash equilibria of monotone games, and complementarity problems in economics and traffic assignment. In operations research, first-order methods for such problems are the workhorse behind large-scale saddle-point formulations of linear and conic programs, where only one operator evaluation and one projection or proximal step per iteration are affordable.

The classical method for Lipschitz monotone operators is Korpelevich's extragradient method (1976) and its proximal variant, Tseng's forward–backward–forward method (2000); both need two evaluations of $F$ per iteration. The reflected projected gradient method of Malitsky (SIAM J. Optim., 2015) uses one evaluation of $F$ but evaluates it at $2z^k-z^{k-1}$, a point that may lie outside the domain of $g$. Malitsky's Golden Ratio Algorithm (GRAAL), introduced in Golden Ratio Algorithms for Variational Inequalities (preprint 2018; published in Mathematical Programming, doi:10.1007/s10107-019-01416-w), uses one evaluation of $F$, always at a feasible point, and one proximal step per iteration. Its fixed-step version, Theorem 1 of that paper, is the subject of this mission; the explicit, adaptive-step version (Theorem 2) is a separate mission of this series.

Setting

Let $\mathcal E$ be a finite-dimensional real inner product space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\| = \sqrt{\langle\cdot,\cdot\rangle}$. Let $g:\mathcal E\to(-\infty,+\infty]$ and write $\operatorname{dom} g = \{x : g(x)<+\infty\}$. Let $F:\operatorname{dom} g\to\mathcal E$. The variational inequality is

$$\text{find } z^*\in\mathcal E \quad\text{such that}\quad \langle F(z^*), z-z^*\rangle + g(z)-g(z^*)\ \ge\ 0\qquad \forall z\in\mathcal E. \tag{1}$$

The standing assumptions are:

• (C1) the solution set $S$ of (1) is nonempty;
• (C2) $g$ is proper (never $-\infty$, finite somewhere), convex, and lower semicontinuous;
• (C3) $F$ is monotone: $\langle F(u)-F(v),u-v\rangle\ge0$ for all $u,v\in\operatorname{dom} g$.

The proximal operator of $g$ is $\operatorname{prox}_g(z) = \operatorname{argmin}_x\{g(x)+\tfrac12\|x-z\|^2\}$. Let $\varphi = \frac{\sqrt5+1}{2}$ be the golden ratio, so that $\varphi^2 = 1+\varphi$. For a step $\lambda>0$ and arbitrary starting points $z^1,\bar z^0\in\mathcal E$, the Golden Ratio Algorithm generates, for $k\ge1$,

$$\bar z^k = \frac{(\varphi-1)z^k + \bar z^{k-1}}{\varphi},\qquad z^{k+1} = \operatorname{prox}_{\lambda g}\big(\bar z^k - \lambda F(z^k)\big). \tag{6}$$

The first line is a convex combination of the newest iterate and the previous average; the second is a forward–backward step taken from the average rather than from $z^k$.

Formalization targets

Goal: Theorem 1

If $F$ is $L$-Lipschitz on $\operatorname{dom} g$ ($L>0$), (C1)–(C3) hold, and $\lambda\in\big(0,\frac{\varphi}{2L}\big]$, then there is $z^*\in S$ with

$$z^k\to z^*\qquad\text{and}\qquad \bar z^k\to z^*\qquad(k\to\infty).$$

Both sequences converge, to one and the same solution. The goal is stated with the paper's exact step range; no rate is claimed, as the paper claims none.

Milestones

1. Eq. (4), the prox-inequality: for proper convex lsc $g$,

$$\bar x = \operatorname{prox}_g z \iff \langle\bar x - z, x-\bar x\rangle\ge g(\bar x)-g(x)\quad\forall x\in\mathcal E.$$

2. Eq. (12), an identity using only the averaging step of (6): for every point $z^*$,

$$\|z^{k+1}-z^*\|^2 = (1+\varphi)\|\bar z^{k+1}-z^*\|^2-\varphi\|\bar z^k-z^*\|^2+\tfrac1\varphi\|z^{k+1}-\bar z^k\|^2 .$$

3. Eq. (14), the energy inequality: for $z^*\in S$ and $k\ge2$,

$$(1+\varphi)\|\bar z^{k+1}-z^*\|^2+\tfrac\varphi2\|z^{k+1}-z^k\|^2\le(1+\varphi)\|\bar z^k-z^*\|^2+\tfrac\varphi2\|z^k-z^{k-1}\|^2-\varphi\|z^k-\bar z^k\|^2 .$$

4. Lemma 1 (Bauschke–Combettes, Theorem 5.5): a sequence that is Fejér monotone with respect to a nonempty set $C$ and whose cluster points all lie in $C$ converges to a point of $C$.

Significance

The result. Theorem 1 shows that monotone variational inequalities with a Lipschitz operator can be solved with one operator evaluation and one proximal step per iteration, with $F$ evaluated only at points of $\operatorname{dom} g$, where it is defined. This matters when $F$ is expensive (a large matrix–vector product, a simulation) or undefined outside the feasible set (for instance an operator involving $\log x$ on the positive orthant). The analysis also explains the constant: the averaging weight $\varphi$ is the largest $c$ with $1/c\ge c-1$, and the step bound $\varphi/(2L)$ follows from it. The fixed-step analysis is the template for the explicit, adaptive-step EGRAAL of the same paper (Theorem 2), which needs only local Lipschitz continuity of $F$.

The formalization. The theorem has a published proof, and no machine-checked version of it or of GRAAL is known. Mathlib contains the golden ratio, Lipschitz conditions, lower semicontinuity and cluster points, but no proximal operator of an extended-valued function, no prox-inequality and no Fejér-monotonicity convergence lemma. This mission produces those pieces and a complete convergence proof for a first-order VI method, which are reusable for projected gradient, forward–backward, extragradient and reflected-gradient analyses.

Difficulty

The naive approach, to show that $\|z^k-z^*\|$ decreases, fails: GRAAL is not Fejér monotone in $z^k$, because the forward step is taken from the average $\bar z^k$ and uses $F(z^k)$ rather than $F$ at the new point. The quantity that decreases is an energy mixing $\|\bar z^k-z^*\|^2$ with the successive difference $\|z^k-z^{k-1}\|^2$, and both the averaging identity and the Lipschitz estimate must produce matching coefficients for the cross terms to cancel. The energy inequality alone gives only boundedness and vanishing successive differences; convergence of the whole sequence, and the fact that the limit solves (1) when $g$ is merely lower semicontinuous and extended-valued, is a separate step. On the formal side, $g$ takes the value $+\infty$, so the prox-inequality and the variational inequality must be handled in extended arithmetic without letting $\infty-\infty$ decide anything.

Formalization scope

• $\mathcal E$ is a type E with [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E].
• $g$ is E → EReal. (C2) is IsProperConvexLSC g: never $\bot$, somewhere finite, convex epigraph $\{(x,t)\in E\times\mathbb R: g(x)\le t\}$, and LowerSemicontinuous g on all of E. $\operatorname{dom} g$ is effDom g = {x | g x ≠ ⊤}.
• $F$ is a total function E → E; monotonicity and the Lipschitz bound $\|F(u)-F(v)\|\le L\|u-v\|$ are required on effDom g only. The step range is 0 < λ, λ ≤ φ / (2 * L) with 0 < L and φ = Real.goldenRatio.
• $S$ is solutionSet g F: points of effDom g satisfying (1) for every $z\in E$, evaluated in EReal.
• The proximal step is the argmin predicate IsProxPoint (fun x => λ * g x) w z⁺, not a choice function, so no junk value is involved. A run of (6) is IsGRAALRun g F λ z zbar on sequences ℕ → E indexed as in the paper: $z^1$ and $\bar z^0$ are free and the entry $z^0$ is unused.
• The conclusion is ∃ zs ∈ solutionSet g F, Tendsto z atTop (𝓝 zs) ∧ Tendsto zbar atTop (𝓝 zs).

The hypotheses of the goal are jointly satisfiable, so the theorem is not vacuous: for $g\equiv0$ and $F\equiv0$ every point is a solution and constant sequences form a run of (6); a formalization under which IsGRAALRun has no instances, or in which $S$ may be empty, is ruled out. Two hypotheses are added to printed statements and flagged in their notes: $C\neq\emptyset$ in Lemma 1, which is false without it, and $z^1\in\operatorname{dom} g$ in Eq. (14), needed at $k=2$ because the paper's $F$ is only defined on $\operatorname{dom} g$.

Welcome contributions: existence and uniqueness of the proximal point of a proper convex lsc function in finite dimensions; the prox-inequality; Fejér-monotonicity lemmas; the energy inequality; and the final convergence argument. The prox and Fejér infrastructure is independent of the golden ratio and is shared with the second mission of this series.

Selected references

• Y. Malitsky, Golden Ratio Algorithms for Variational Inequalities, preprint, Optimization Online 6598, 2018. https://optimization-online.org/wp-content/uploads/2018/05/6598.pdf ; published in Mathematical Programming. https://doi.org/10.1007/s10107-019-01416-w
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Springer, 2011 (2nd ed. 2017). https://doi.org/10.1007/978-3-319-48311-5
• G. M. Korpelevich, The extragradient method for finding saddle points and other problems, Ekonomika i Matematicheskie Metody 12 (1976) 747–756.
• P. Tseng, A modified forward–backward splitting method for maximal monotone mappings, SIAM J. Control Optim. 38 (2000) 431–446. https://doi.org/10.1137/S0363012998338806
• Y. Malitsky, Projected reflected gradient methods for monotone variational inequalities, SIAM J. Optim. 25 (2015) 502–520. https://doi.org/10.1137/14097238X

Why reduce scenarios

Multistage and two-stage stochastic programs are solved numerically on a discrete probability distribution: a finite set of scenarios $\omega_1,\dots,\omega_N$ with probabilities $p_1,\dots,p_N$. The size of the resulting optimization problem grows with $N$, and scenario sets produced by sampling or by historical data are often far too large to be solved directly. Scenario reduction replaces the original distribution by one supported on a small subset of the scenarios, chosen so that the optimal value and solutions of the stochastic program change as little as possible.

Stability theory for stochastic programs (Rachev and Römisch, 2002) shows that this change is controlled by a probability distance of Fortet–Mourier type, which for discrete measures is bounded by the value of a transportation problem. Dupačová, Gröwe-Kuska and Römisch (2003) turned this into a combinatorial problem and proposed greedy backward and forward heuristics. Heitsch and Römisch (2003) gave faster versions of both heuristics; the forward version, fast forward selection, is the subject of this mission. Implementations of these reduction heuristics are distributed with the GAMS modelling system (SCENRED) and are used in energy and finance applications of stochastic programming.

Setting

Let $E$ be a finite-dimensional real vector space with a norm $\|\cdot\|$, let $\omega_0\in E$, and let $h:[0,\infty)\to[0,\infty)$ be continuous and nondecreasing with $h(0)=0$. The cost between two points of $E$ is

$$c(\omega,\tilde\omega)=\max\bigl\{1,\,h(\|\omega-\omega_0\|),\,h(\|\tilde\omega-\omega_0\|)\bigr\}\,\|\omega-\tilde\omega\| .$$

It is nonnegative, symmetric, and zero on the diagonal.

The original distribution is $P=\sum_{i=1}^N p_i\delta_{\omega_i}$ with $p_i>0$ and $\sum_i p_i=1$. Deleting the scenarios in a set $J\subset\{1,\dots,N\}$ and assigning new weights $q_j\ge 0$, $\sum_{j\notin J}q_j=1$, to the kept ones gives $Q=\sum_{j\notin J}q_j\delta_{\omega_j}$. The distance $D(J;q)$ between $P$ and $Q$ is the optimal value of the transportation problem

$$D(J;q)=\min\Bigl\{\sum_{i=1}^N\sum_{j\notin J}c(\omega_i,\omega_j)\eta_{ij}:\ \eta_{ij}\ge 0,\ \sum_{i}\eta_{ij}=q_j,\ \sum_{j\notin J}\eta_{ij}=p_i\Bigr\}.$$

The reduction cost of deleting $J$ is

$$D_J=\sum_{i\in J}p_i\min_{j\notin J}c(\omega_i,\omega_j),$$

and the optimal reduction problem (8) minimizes $D_J$ over all $J$ with $\#J=N-n$, where $n$ is the number of scenarios to keep.

Forward selection builds the kept set greedily. With $J^{[0]}=\{1,\dots,N\}$ and $J^{[i]}=\{1,\dots,N\}\setminus\{u_1,\dots,u_i\}$, it chooses

$$u_i\in\arg\min_{u\in J^{[i-1]}}D_{J^{[i-1]}\setminus\{u\}},\qquad i=1,\dots,n. \tag{16}$$

Fast forward selection (Algorithm 2.4) computes the same choices through an updated cost matrix: $c^{[1]}_{ku}=c(\omega_k,\omega_u)$, $c^{[i]}_{ku}=\min\{c^{[i-1]}_{ku},c^{[i-1]}_{ku_{i-1}}\}$, $z^{[i]}_u=\sum_{k\in J^{[i-1]}\setminus\{u\}}p_kc^{[i]}_{ku}$, and $u_i\in\arg\min_{u\in J^{[i-1]}}z^{[i]}_u$.

Formalization targets

Goal: Theorem 2.5

For $1\le n\le N$ and every run $u_1,\dots,u_n$ of Algorithm 2.4, with any tie-breaking in the arg min,

$$u_i\ \text{satisfies (16)}\quad\text{and}\quad z^{[i]}_{u_i}=D_{J^{[i]}}\qquad(i=1,\dots,n).$$

Milestones

1. Theorem 2.1 (redistribution). For $J$ with at least one kept scenario, $D_J=\min_q D(J;q)$, and the minimum is attained at $\bar q_j=p_j+\sum_{i\in J,\,j(i)=j}p_i$ for every choice of nearest kept scenarios $j(i)$.
2. Eq. (10). $D_{\{1,\dots,N\}\setminus\{u\}}=\sum_{i=1}^Np_ic(\omega_i,\omega_u)$, so (8) with $\#J=N-1$ is problem (10).
3. Eq. (12). The sum $lb$ of the $N-n$ smallest single-deletion costs $p_l\min_{j\neq l}c(\omega_l,\omega_j)$, taken in the greedy order (11), is at most $D_J$ for every $J$ with $\#J=N-n$.
4. Optimality condition (p. 191). If each $l_i$ has a nearest other scenario outside $\{l_1,\dots,l_{N-n}\}\setminus\{l_i\}$, then $\{l_1,\dots,l_{N-n}\}$ solves (8).
5. Eq. (17), unrolled recursion. For any index sequence, $c^{[i]}_{ku}=\min_{j\notin J^{[i-1]}\setminus\{u\}}c(\omega_k,\omega_j)$ for $u\in J^{[i-1]}$.
6. Eq. (17), conclusion. For any index sequence, $z^{[i]}_u=D_{J^{[i-1]}\setminus\{u\}}$ for $u\in J^{[i-1]}$.

Significance

Theorem 2.5 certifies that the cheap update of Algorithm 2.4 (one pairwise minimum per matrix entry and step) produces exactly the greedy forward selection defined through the reduction costs, and that the running objective $z^{[i]}_{u_i}$ is the reduction cost of the scenarios deleted so far. Combined with Theorem 2.1, $z^{[i]}_{u_i}$ is the optimal transportation distance between $P$ and the best measure on the kept scenarios, which is the quantity practitioners monitor to decide how many scenarios to keep. The lower bound (12) and the optimality condition give a posteriori quality certificates for any reduced set.

All results of this mission are proved in the paper or in the works it cites (Dupačová et al., 2003); none is open. To the best of a platform search, none has been machine-checked. The mission provides a verified specification of a widely deployed algorithm, a formal link between a combinatorial set-covering objective and a finite transportation problem, and definitions (reduction cost, transportation plans with a partially free target marginal, greedy runs with arbitrary tie-breaking) reusable by the regular-tree missions of this series and by later scenario-tree construction papers.

Difficulty

The mathematics is elementary; the difficulty is bookkeeping. The recursion for $c^{[i]}$ refers to the previous step's column $u_{i-1}$, which itself was updated, so unrolling it to a minimum over $\{u,u_1,\dots,u_{i-1}\}$ is an induction on $i$ in which the index sets $J^{[i]}$, the 1-based step counter and the complement structure all move together. The natural first attempt, identifying $c^{[i]}_{ku}$ with the minimum over the complement of $J^{[i]}$, is off by one step: the correct set is the complement of $J^{[i-1]}\setminus\{u\}$, which contains $u$ itself. For Theorem 2.1 the lower bound requires using that $c(\omega_i,\omega_i)=0$ for kept scenarios and that every plan ships all of $p_i$ somewhere outside $J$; the attainment part requires constructing the plan explicitly from the choice $j(\cdot)$, including scenarios for which several kept scenarios are equally near.

Formalization scope

• Scenarios are ω : Fin N → E with E a finite-dimensional real normed space; the paper's closed set $\Omega\subset\mathbb R^s$ plays no role beyond containing the scenarios and is omitted. Scenarios need not be distinct.
• $h$ is a function ℝ → ℝ with the paper's assumptions imposed on $[0,\infty)$ (IsGrowthFunction); every theorem carries them, together with $p_i>0$ and $\sum_ip_i=1$.
• The functions $f_0$, $g$ and the stochastic program (1)–(2) that motivate $c$ appear in no statement.
• $D(J;q)$ is the paper's finite transportation problem (p. 188), not the Kantorovich functional on measures. Weights $q$ and plans $\eta$ are indexed by all of $\{1,\dots,N\}$ with entries at deleted indices fixed to $0$.
• $D_J$ requires a proof that the complement of $J$ is nonempty; minima are Finset.inf', never a real infimum with a default value.
• Algorithm 2.4 is a relation on sequences u : ℕ → Fin N with 1-based steps. $c^{[i]}$ is the printed recursion, extended to all indices; runs are any sequences satisfying the arg-min conditions, so every tie-breaking rule is covered.
• The paper's standing restriction $n<N$ is relaxed to $n\le N$ in Theorem 2.5; the statement remains true at $n=N$.
• A trivializing formalization is ruled out: defining $c^{[i]}$ or $z^{[i]}$ directly as the minimum over the selected set or as $D_{J^{[i-1]}\setminus\{u\}}$ would make Theorem 2.5 hold by definition, and proving it for one fixed tie-breaking rule would prove less than the paper; neither is done.
• Proofs of the milestones, alternative proofs of Theorem 2.1 via LP duality, and a verified executable implementation of Algorithm 2.4 are all welcome.

Selected references

• H. Heitsch, W. Römisch, Scenario Reduction Algorithms in Stochastic Programming, Computational Optimization and Applications 24 (2003), 187–206. https://doi.org/10.1023/A:1021805924152
• J. Dupačová, N. Gröwe-Kuska, W. Römisch, Scenario reduction in stochastic programming: an approach using probability metrics, Mathematical Programming 95 (2003), 493–511. https://doi.org/10.1007/s10107-002-0331-0
• S. T. Rachev, W. Römisch, Quantitative stability in stochastic programming: the method of probability metrics, Mathematics of Operations Research 27 (2002), 792–818. https://doi.org/10.1287/moor.27.4.792.304

Motivation

A processor, a machine shop or a single server must work through a set of jobs one at a time, and each job is costly when it is late. Deciding the order is the single-machine sequencing problem, the simplest and most studied model of scheduling theory. Robert McNaughton's 1959 article Scheduling with Deadlines and Loss Functions (Management Science 6(1):1–12) treats it for a computer that must run several tasks, each with a deadline and a loss that grows linearly with the lateness. Its §2 gives the first sufficient condition under which a simple ratio rule is optimal in the presence of deadlines, and shows that interrupting and resuming tasks ("splitting", now called preemption) never helps on one processor.

Timeline.

• 1956: W. E. Smith, Various optimizers for single-stage production (Naval Research Logistics Quarterly 3), proves that sequencing jobs by non-increasing weight-to-processing-time ratio minimizes the total weighted completion time over non-preemptive sequences.
• 1959: McNaughton, §2 of the present paper, proves independently that the same ratio order is optimal against all schedules, split or not and with idle time (Theorem 2.3), and extends it to deadlines when no task finishes early in that order (Theorem 2.4). §3 of the same paper gives the "wrap-around" rule for preemptive makespan on identical processors, and §4 the non-preemptive optimality for weighted completion time on several processors.
• 1977: J. K. Lenstra, A. H. G. Rinnooy Kan and P. Brucker show that minimizing total weighted tardiness on one machine, the general problem of §2, is strongly NP-hard (Annals of Discrete Mathematics 1); this is why §2 gives a sufficient condition and not an algorithm.

Setting

There are $m$ tasks $(1),\dots,(m)$ for a single processor, and the present is time $0$. Task $(i)$ takes $a_i > 0$ units of processing time, has a deadline $d_i$ and a penalty rate $p_i \ge 0$. If $(i)$ is finished at time $C_i \le d_i$ there is no loss; otherwise the loss on $(i)$ is $p_i x$, where $x = C_i - d_i$ is the time from the deadline to the completion. Thus the loss on a task completed at time $t$ is

$$\ell_i(t) = p_i \max(0,\ t - d_i).$$

The ratio of task $(i)$ is $r_i = p_i / a_i$.

A task may be split: part of it may run between times 4 and 6 and the remainder between times 8 and 11, and similarly in any finite number of parts. A schedule $S$ is therefore a finite list of pieces, each a task together with a start and a stop time. It is feasible when every piece lies in $[0,\infty)$ with start $\le$ stop, no two pieces overlap in time, and the pieces of each task $(i)$ have total length exactly $a_i$. The completion time $C_i(S)$ is the latest stop time of a piece of $(i)$, and the total loss is

$$c(S) = \sum_{i=1}^{m} \ell_i\bigl(C_i(S)\bigr).$$

For an order $\sigma$ of the tasks ($\sigma(k)$ in position $k$), the sequenced schedule $S_\sigma$ runs the tasks without splits and without unused time: $\sigma(k)$ occupies $\bigl[\sum_{l<k} a_{\sigma(l)},\ \sum_{l\le k} a_{\sigma(l)}\bigr]$. The order is in decreasing $r_i$ when $k \le l$ implies $r_{\sigma(l)} \le r_{\sigma(k)}$. Finally $c^*(S)$ denotes the total loss of $S$ computed as if $d_1 = \dots = d_m = 0$.

Formalization targets

Goal: Theorem 2.4 (p. 5)

If $\sigma$ is in decreasing $r_i$ and no task finishes before its deadline in $S_\sigma$, i.e. $d_i \le C_i(S_\sigma)$ for every $i$, then $S_\sigma$ is feasible and

$$c(S_\sigma) \le c(S') \qquad \text{for every feasible schedule } S'.$$

The competitors $S'$ may split tasks and leave the processor idle. The condition is sufficient but not necessary.

Milestones, in attack order

1. Theorem 2.1 (p. 4): if both $(i)$ and $(j)$ run in the $a_i + a_j$ consecutive units of time after a time $t$ past both deadlines and $r_i > r_j$, their joint loss is strictly smaller when $(i)$ goes first:

$$\ell_i(t+a_i) + \ell_j(t+a_i+a_j) < \ell_j(t+a_j) + \ell_i(t+a_j+a_i).$$

2. The reduction in the proof of Theorem 2.2 (pp. 4–5): a feasible schedule with more than $m$ pieces can be replaced by a feasible one with fewer pieces and no greater loss.
3. Theorem 2.2 (p. 4): some optimal schedule, optimal among all feasible schedules, splits no task.
4. Theorem 2.3 (p. 5): if $d_1 = \dots = d_m = 0$, the sequenced schedule in decreasing $r_i$ minimizes the total loss over all feasible schedules.
5. The display of the proof of Theorem 2.4 (p. 6): if no task finishes early in $S = S_\sigma$, then for every feasible $S'$,

$$c(S') - c(S) \ge c^*(S') - c^*(S).$$

Significance

The result. Theorem 2.3 is the ratio rule for total weighted completion time, in its strongest single-machine form: it holds against preemptive schedules and schedules with idle time, not only against permutations. Theorem 2.4 carries the rule over to deadlines and linear tardiness penalties under a checkable condition on one schedule. Since weighted tardiness is strongly NP-hard in general, a condition of this kind is what one can hope for, and the paper's two-step heuristic for general deadlines (p. 6) is built on it. Theorem 2.2, as the paper remarks (p. 6), "does not depend on the linear loss function": it makes non-preemptive scheduling without loss of generality for single-machine objectives of this kind.

Formalizing it. All results of §2 are proved in the paper and are textbook material; none has a machine-checked proof on the platform. The platform's Scheduling Algorithms V mission formalizes the multi-processor results of §§3–4 (via Brucker's textbook), and nothing there states a single-processor ratio rule with deadlines. This mission supplies a single-processor schedule model with splitting, the interchange lemma, the non-preemption theorem and the ratio rule, each over all feasible schedules.

Difficulty

The interchange argument of Theorem 2.1 compares only two schedules that differ in the order of two adjacent tasks. Turning it into optimality against every feasible schedule requires two further steps, and each fails if done naively. First, a competitor may split tasks and leave gaps; the interchange argument does not apply to such schedules, so a separate argument must remove splits without raising any completion time. Second, with deadlines the loss $\max(0, t - d_i)$ is not linear in the completion time, so the ratio order is in general not optimal; the obvious attempt to repeat the interchange argument fails as soon as a task can finish before its deadline, since moving such a task later costs nothing. This is why Theorem 2.4 needs its hypothesis that no task finishes early, and why the paper leaves the general case to a heuristic.

Formalization scope

Tasks and positions are the zero-based indices of Fin m; times, lengths, deadlines and penalties are real numbers. A schedule is a List of pieces (task, start, stop), mirroring the public definition SchedulingAlgorithms_ParallelMachines with one processor. Feasibility requires $0 \le$ start $\le$ stop, pairwise disjoint pieces, and exact total length $a_i$ per task; zero-length pieces and unsorted lists are allowed. The completion time is the maximum stop time of the task's pieces ($0$ for a task with no pieces, which feasibility excludes). "No split" means exactly one piece per task, so two abutting pieces count as a split. "Decreasing $r_i$" is non-increasing, with ties in any order. "Minimal" and "optimal" are stated as $\le$ against every feasible schedule, never as an infimum.

Standing assumptions, stated in every item: $a_i > 0$ (tasks take time, and $r_i = p_i/a_i$ needs $a_i \ne 0$), and $p_i \ge 0$ for Theorems 2.2–2.4 and the proof steps (penalties are non-negative; with a negative penalty and idle time allowed the loss is unbounded below). Theorem 2.1 carries no sign condition. No condition is placed on the deadlines.

A formalization that restricts the competitors of Theorems 2.2–2.4 to unsplit schedules, or to sequenced schedules of other orders, states a weaker theorem and is ruled out: every statement quantifies over all feasible schedules.

A complete development needs: sums over sublists of pieces, rearrangements of pieces of a schedule and their effect on completion times, and optimality over permutations of a finite set of tasks. The schedule model and the non-preemption argument are reusable for any single-machine regular objective. Contributions of intermediate lemmas on these points are welcome.

Selected references

• R. McNaughton, Scheduling with Deadlines and Loss Functions, Management Science 6(1):1–12, 1959. https://doi.org/10.1287/mnsc.6.1.1
• W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3(1–2):59–66, 1956. https://doi.org/10.1002/nav.3800030106
• J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Complexity of machine scheduling problems, Annals of Discrete Mathematics 1:343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
• P. Brucker, Scheduling Algorithms, 5th ed., Springer, 2007. https://doi.org/10.1007/978-3-540-69516-5

Why exact reduction distances matter

Multistage stochastic programs are solved on a finite scenario tree, a discrete probability measure whose atoms are paths of a stochastic process. The size of the deterministic equivalent grows with the number of scenarios, so practitioners replace the original measure $P=\sum_{i=1}^N p_i\delta_{\omega_i}$ by a measure supported on $n<N$ of its scenarios. Stability theory for stochastic programs (Dupačová, Gröwe-Kuska and Römisch, Math. Program. 95 (2003), doi:10.1007/s10107-002-0331-0) bounds the change of the optimal value by a probability metric between the two measures, which leads to the optimal scenario reduction problem: choose which $N-n$ scenarios to delete so that this distance is smallest.

That problem is a set-covering problem and is NP-hard, and the algorithms that Heitsch and Römisch study in the same paper (backward reduction, fast forward selection) are heuristics without error guarantees. To test them one needs original measures whose optimal reduction distance is known exactly. Section 3 of Heitsch and Römisch, Scenario Reduction Algorithms in Stochastic Programming, Comput. Optim. Appl. 24 (2003) (doi:10.1023/A:1021805924152) supplies such instances: regular binary and ternary scenario trees, for which the minimal distance to any reduced tree with at least a fixed fraction of the scenarios is an explicit formula. This mission formalizes the binary case, Proposition 3.1.

Setting

Fix a horizon $K\in\mathbb N$ and level parameters $\delta^1,\dots,\delta^K\ge0$, with $\delta^0=0$. A regular binary scenario tree has $N=2^K$ scenarios. A scenario is determined by a branch $i_k\in\{1,2\}$ at every level $k=1,\dots,K$, and is the vector $\omega_i=(\omega_i^0,\dots,\omega_i^K)\in\mathbb R^{K+1}$ with

$$\omega_i^k=\sum_{j=0}^k\delta^j_{i_j},\qquad \delta^j_{i_j}=(2i_j-3)\,\delta^j\in\{-\delta^j,+\delta^j\}.\tag{19}$$

All scenarios start at the root $\omega_i^0=0$ and carry probability $p_i=1/N$. Scenarios are compared in the maximum norm $\|\omega-\tilde\omega\|_\infty=\max_{k=0,\dots,K}|\omega^k-\tilde\omega^k|$.

Deleting the scenarios with indices in $J\subset\{1,\dots,N\}$ and moving each deleted scenario's probability to a nearest kept scenario costs the reduction cost

$$D_J=\sum_{i\in J}p_i\min_{j\notin J}\|\omega_i-\omega_j\|_\infty,\tag{8}$$

which by Theorem 2.1 of the paper is the minimal Kantorovich-type distance between $P$ and a measure supported on the kept scenarios. The minimal reduction distance for $n$ kept scenarios is $D^{min}_n=\min\{D_J:\#J=N-n\}$.

In the Lean development, scenarios are indexed by σ : Fin K → Fin 2 (Fin-index $r$ is tree level $r+1$, value $0$ is the branch $-\delta$, value $1$ is $+\delta$), lev σ k is the branch at level $k$, scenario δ σ : Fin (K+1) → ℝ is $\omega_\sigma$, and redCost δ J hJ is $D_J$.

Formalization targets

Goal: Proposition 3.1 (3/4-solution)

Let $K\ge3$, $k_0\in\arg\min_{1\le k\le K}\delta^k$, $k_0\le K-2$ and $\max\{\delta^{k_0+1},\delta^{k_0+2}\}\le2\delta^{k_0}$. Then any two distinct scenarios are at distance at least $2\delta^{k_0}$; there is a set $J_*$ of $\frac34N$ scenarios each of which has a partner outside $J_*$ at distance exactly $2\delta^{k_0}$; and for every $n\in\mathbb N$ with $\frac N4\le n<N$

$$D^{min}_n=\min\{D_J:\#J=N-n\}=\frac{N-n}{N}\,2\delta^{k_0}.\tag{20}$$

Milestones

1. Two scenarios that first differ at level $l$ are at distance $\ge2\delta^l\ge2\delta^{k_0}$.
2. $D_J\ge\frac{N-n}{N}2\delta^{k_0}$ for every $J$ with $\#J=N-n$.
3. The index set $I_*$ (branch at $k_0$ opposite to the common branch at $k_0+1,k_0+2$) has $\#I_*=N/4$, so $\#J_*=\frac34N$.
4. Every $j\in J_*$ has a partner $i\in I_*$ with $\|\omega_i-\omega_j\|_\infty=2\delta^{k_0}$.
5. Example 4.1: for $K=10$ and the paper's parameters, Proposition 3.1 applies with $k_0=1$ and $D^{min}_n=\frac{N-n}{N}$ for $256\le n<1024$.

Significance

The result. Proposition 3.1 gives the exact optimum of an NP-hard combinatorial problem on an explicit, parametrized family of instances of every size $N=2^K$. Section 4 of the paper uses it (Example 4.1, $N=1024$) as ground truth for the relative accuracy of backward reduction and fast forward selection. Without it, the quality of a heuristic reduction on a large tree could only be compared with other heuristics or with lower bounds.

The formalization. The proposition is proved in the paper; to our knowledge no machine-checked version exists. A formal proof certifies the benchmark values, and the statement also corrects the printed text in two places. First, "there are $\frac34N$ distinct pairs … at distance exactly $2\delta^{k_0}$" is false as an exact count (for $K=3$, $\delta=(1,1,1)$ there are twenty such pairs, not six), so the goal states "at least", in the form the proof exhibits. Second, the paper's sign-based definition of $I_*$ degenerates when some $\delta^k=0$, although the proposition still holds; the mission defines $I_*$ by branch indices.

Difficulty

The lower bound is a direct computation. The content is the matching upper bound: a set $J$ of the prescribed size for which every deleted scenario has a kept scenario at the minimal possible distance. A natural first attempt pairs scenarios that differ only at level $k_0$. That handles only half of the scenarios with a single partner each, and it cannot reach $\frac34N$ deleted scenarios. Once scenarios differ at more than one level, their maximum-norm distance is a maximum of several partial sums, and keeping all of them at most $2\delta^{k_0}$ is exactly where the hypothesis $\max\{\delta^{k_0+1},\delta^{k_0+2}\}\le2\delta^{k_0}$ enters. Without it, eq. (20) fails: for $K=3$, $\delta=(1,3,3)$ and $n=2$ the true minimum is $\frac52$, not $\frac32$. The passage from $n=N/4$ to general $n\ge N/4$ also needs care: the deleted set must shrink while each remaining deleted scenario keeps its partner among the kept ones.

Formalization scope

• The index type is Fin K → Fin 2, which has exactly $2^K$ elements. The paper's $(K+1)$-tuple has a level-0 entry with no choice, so it is dropped, and the vector $\omega$ keeps its $K+1$ coordinates with $\omega^0=0$.
• The parameters are δ : ℕ → ℝ, with $\delta^k\ge0$ and the arg min stated for $k=1,\dots,K$ only. $\delta^k>0$ is not assumed, because the paper allows $\delta^k\in\mathbb R_+$ and the proposition holds with zeros.
• The cost is Mathlib's norm on Fin (K+1) → ℝ, which is the maximum norm, and $p_i=1/2^K$ is written out.
• $D_J$ requires a nonempty set of kept scenarios, and its inner minimum is a finite Finset.inf'.
• $D^{min}_n$ is stated with IsLeast over the set of attained values $D_J$, $\#J=N-n$, so both the lower bound and attainment are part of the goal. A proof of $D_{J}\le\frac{N-n}{N}2\delta^{k_0}$ for a single exhibited $J$, or a real infimum without attainment, does not prove the goal.
• "$\frac N4\le n$" is written $2^K\le4n$, and $\frac34N$ is $3\cdot2^{K-2}$.
• The pairs claim is "at least $\frac34N$ pairs", expressed as a set $J_*$ of that size with a partner outside $J_*$ for every member.
• All hypotheses on $k_0$ appear in the goal; dropping any of them makes (20) false.

Useful infrastructure: sup-norm lemmas for Fin n → ℝ (pi_norm_le_iff_of_nonneg, norm_le_pi_norm), Finset.inf' lemmas, and counting functions Fin K → Fin 2 with prescribed values (Fintype.card_fun, Fintype.card_pi). The tree and reduction-cost definitions are shared in spirit with the ternary-tree mission of this series (Proposition 3.2), and a proof whose structure transfers to $d=3$ is welcome. Contributions of proofs of the milestones individually, in any order, are welcome.

Selected references

• H. Heitsch, W. Römisch, Scenario Reduction Algorithms in Stochastic Programming, Computational Optimization and Applications 24 (2003), 187–206. doi:10.1023/A:1021805924152
• J. Dupačová, N. Gröwe-Kuska, W. Römisch, Scenario reduction in stochastic programming: An approach using probability metrics, Mathematical Programming 95 (2003), 493–511. doi:10.1007/s10107-002-0331-0