Operations Research

Motivation

Traffic information systems (TIS) such as navigation apps send drivers private, noisy signals about the state of the road network: incidents, weather, closures. When several such systems coexist, their subscribers act on different information, and the congestion each population experiences depends on how all of them route. A question then arises for transport planners and for the information providers themselves: if travelers are free to choose which system to subscribe to, which market shares of the competing systems are stable?

Wu, Amin and Ozdaglar (Operations Research 69(1):148–163, 2021; preprint arXiv:1808.10590) model this situation as a Bayesian routing game with heterogeneous information and answer the question exactly: the equilibrium adoption rates are the minimizers of a convex function of the population sizes, the equilibrium value of a weighted potential. This mission formalizes that characterization (Theorem 4 of the paper) together with the results its proof rests on. A companion mission (Value of Information in Bayesian Routing Games I) formalizes the paper's other main result, the sign and monotonicity of the relative value of information between two populations.

Setting

A Bayesian routing game $\Gamma(\lambda)$ has a single origin–destination pair, a finite set of edges $\mathcal E$ and a finite nonempty set of routes $\mathcal R$ (each route a set of edges), and a finite set of network states $\mathcal S$. Travelers of total demand $D>0$ are split into populations $i\in\mathcal I$, one per TIS; population $i$ has size $\lambda^iD$, where the size vector $\lambda$ lies in the simplex $\Delta=\{\lambda:\lambda^i\ge0,\ \sum_i\lambda^i=1\}$. Each population receives a signal (its type) $t^i$ from a finite set $\mathcal T^i$; states and type profiles $t=(t^i)_i$ are drawn from a common prior $\pi\in\Delta(\mathcal S\times\mathcal T)$. Edge $e$ in state $s$ has cost $c^s_e(w)$ at load $w$, positive, strictly increasing and differentiable.

A strategy profile $q$ assigns to each population and type a split $q^i_r(t^i)\ge0$ of its demand over routes, with $\sum_rq^i_r(t^i)=\lambda^iD$; these form the polytope $\mathcal Q(\lambda)$. It induces route flows $f_r(t)=\sum_iq^i_r(t^i)$ and edge loads $w_e(t)=\sum_{r\ni e}f_r(t)$. A traveler of population $i$ with signal $t^i$ forms the belief $\beta^i(s,t^{-i}\mid t^i)=\pi(s,t^i,t^{-i})/\Pr(t^i)$ and evaluates the expected route cost $\mathbb E[c_r(q)\mid t^i]=\sum_{s,t^{-i}}\sum_{e\in r}\beta^i(s,t^{-i}\mid t^i)\,c^s_e(w_e(t))$. A Bayesian Wardrop equilibrium (BWE) is a $q\in\mathcal Q(\lambda)$ in which every type uses only routes of minimal expected cost. The equilibrium population cost is

$$C^{i*}(\lambda)=\sum_{t^i\in\mathcal T^i}\Pr(t^i)\min_{r\in\mathcal R}\mathbb E[c_r(q^*)\mid t^i].$$

The weighted potential is $\Phi(q)=\sum_{s,e,t}\pi(s,t)\int_0^{w_e(t)}c^s_e(z)\,dz$, and $\Psi(\lambda)=\min_{q\in\mathcal Q(\lambda)}\Phi(q)$ is its equilibrium value. In route-flow form, $\widehat\Phi(f)$ is the same expression in terms of $f$; route flows satisfy linear constraints (14a)–(14c) (a separability condition across populations, total demand $D$, nonnegativity) and one information impact constraint per population, $\widehat J^i(f)\le\lambda^iD$, where $\widehat J^i(f)=D-\sum_r\min_{t^i}f_r(t^i,\widehat t^{-i})$ measures how much of the demand reacts to population $i$'s signal. Let $\mathcal F^\dagger$ be the set of minimizers of $\widehat\Phi$ subject to (14a)–(14c) only, and

$$\Lambda^\dagger=\{\lambda\in\Delta:\ \exists f^\dagger\in\mathcal F^\dagger,\ \widehat J^i(f^\dagger)\le\lambda^iD\ \ \forall i\}.$$

In the two-stage game, travelers first choose a TIS, inducing $\lambda$, and then play $\Gamma(\lambda)$. A size vector is a vector of equilibrium adoption rates if no traveler gains by switching TIS:

$$\lambda^i>0\ \Longrightarrow\ C^{i*}(\lambda)=\min_{j\in\mathcal I}C^{j*}(\lambda)\qquad\forall i\in\mathcal I.\tag{31}$$

Formalization targets

Goal: Theorem 4

For every $\lambda\in\Delta$ and every BWE of $\Gamma(\lambda)$,

$$(31)\ \text{holds}\iff\lambda\in\Lambda^\dagger .$$

With the existence of a BWE for every $\lambda\in\Delta$, this is the paper's statement that the set of equilibrium adoption rates is $\Lambda^\dagger$.

Milestones

1. Theorem 1. $q$ is a BWE of $\Gamma(\lambda)$ iff $q$ minimizes $\Phi$ over $\mathcal Q(\lambda)$; the equilibrium edge load $w^*(\lambda)$ is unique.
2. Proposition 2. A route flow in the flow polytope $\mathcal F(\lambda)$ ((14a)–(14c) plus all information impact constraints) is an equilibrium flow iff it minimizes $\widehat\Phi$ over $\mathcal F(\lambda)$.
3. Lemma 5. $\Psi$ is convex on $\Delta$, and with $z^{ij}=e_i-e_j$ and $V^{ij*}=C^{j*}-C^{i*}$,

$$\lim_{\epsilon\to0^+}\frac{\Psi(\lambda+\epsilon z^{ij})-\Psi(\lambda)}{\epsilon}=-D\,V^{ij*}(\lambda).$$

4. Proposition 5. $\Lambda^\dagger$ is convex, $\Lambda^\dagger=\operatorname{argmin}_{\lambda\in\Delta}\Psi(\lambda)$, and the equilibrium edge load equals the size-independent load $w^\dagger$ of $\mathcal F^\dagger$ iff $\lambda\in\Lambda^\dagger$.

A separate item states the existence of a BWE for every $\lambda\in\Delta$.

Significance

The result. Theorem 4 reduces a question about a two-stage game with a continuum of travelers and private signals to the minimization of one convex function over a simplex. It shows that the stable market shares form a convex set, generally not a single point, so each system's equilibrium adoption rate ranges over an interval; and that this set is determined by the joint information environment of all systems, not by each system's signal alone. On $\Lambda^\dagger$ the equilibrium edge load does not depend on the shares at all, which identifies when changes in market shares leave congestion unchanged.

Formalizing it. The proofs of Theorem 1, Proposition 2 and Proposition 5 are in the paper's online e-companion, and Lemma 5 relies on sensitivity results for parametric convex programs cited from the literature. No part of this development has, to our knowledge, been machine-checked. A complete formalization would produce a verified potential-game characterization of Bayesian Wardrop equilibria with heterogeneous information and a verified directional-derivative formula for the optimal value of a parametric convex program; nothing comparable is currently on the platform (the existing Wardrop development covers complete information only).

Difficulty

The direction "$\lambda\in\Lambda^\dagger$ implies (31)" is not a pointwise statement about costs: it follows from $\Lambda^\dagger$ being the argmin of $\Psi$ together with the formula linking directional derivatives of $\Psi$ to cost differences. Both are hard. The derivative formula (26) is a statement about the optimal value of a convex program whose feasible set moves with $\lambda$; its standard proofs pass through uniqueness of Lagrange multipliers, which fails exactly at the degenerate size vectors ($\lambda^i=0$) that Theorem 4 must cover, since an unused TIS is a legitimate outcome. The identity $\Lambda^\dagger=\operatorname{argmin}\Psi$ needs the route-flow reformulation (Proposition 2), in which the size vector enters only through the information impact constraints, and the uniqueness of the minimizing edge load. The natural first idea, comparing population costs directly at a given equilibrium, gives no handle on which size vectors make them equal.

Formalization scope

The Lean development lives in the namespace BayesRouting.Adoption. Populations, types, states, edges and routes are finite types; type spaces and the route set are nonempty; routes are edge sets. The game is a structure whose fields include the paper's standing assumptions: the prior is a probability distribution, $D>0$, and each cost is positive on nonnegative loads, strictly increasing and differentiable (on all of $\mathbb R$, which loses no generality). One assumption is added: every type profile has positive probability. Without it the equilibrium edge load need not be unique and the beliefs can be undefined; it excludes the paper's Example 2(i) (perfectly correlated signals).

Conventions: size vectors range over the probability simplex; $\Psi$ is the infimum of $\Phi$ over $\mathcal Q(\lambda)$ and is only compared at points of the simplex (outside it the feasible set can be empty and the value is a default); $C^{i*}$ is the last form of the paper's (7), well defined when $\lambda^i=0$; $\widehat J^i$ is the maximum over reference profiles, which equals the paper's value on flows satisfying (14a); equilibrium statements are made for every BWE rather than for "the" equilibrium; $\mathcal F^\dagger$ and similar sets are argmin sets. Lemma 5 is stated for the directions $z^{ij}$ with $\lambda^j>0$ (otherwise $\lambda+\epsilon z^{ij}$ leaves the simplex); $\lambda^i=0$ is allowed.

A trivializing formalization is ruled out: the existence of a BWE is its own item, so "for every BWE" is not vacuous, and $\Lambda^\dagger$ is defined by (30) from the flow problem (28), not as the argmin of $\Psi$, so the goal is not a restatement of Proposition 5.

Infrastructure a complete development needs: KKT conditions for convex programs with linear constraints, convexity of integrals of increasing functions, compactness arguments for existence of minimizers, and one-sided directional derivatives of optimal-value functions. The last two are reusable well beyond this mission. Proofs of any item, and of auxiliary lemmas such as Proposition 1 of the paper (feasible route flows form the polytope $\mathcal F(\lambda)$), are welcome.

Selected references

• M. Wu, S. Amin, A. E. Ozdaglar, Value of Information in Bayesian Routing Games, Operations Research 69(1):148–163, 2021. https://doi.org/10.1287/opre.2020.1999 (preprint: https://arxiv.org/abs/1808.10590)
• W. H. Sandholm, Potential games with continuous player sets, Journal of Economic Theory 97(1):81–108, 2001. https://doi.org/10.1006/jeth.2000.2696
• A. V. Fiacco, J. Kyparisis, Convexity and concavity properties of the optimal value function in parametric nonlinear programming, Journal of Optimization Theory and Applications 48(1):95–126, 1986. https://doi.org/10.1007/BF00938592

Motivation

The periodic-review inventory model with a fixed ordering cost is one of the basic models of operations research. When every order incurs a set-up cost $K$ in addition to holding and shortage costs, the optimal replenishment rule over an infinite horizon is, under standard convexity assumptions, a stationary $(s, S)$ policy: whenever the stock falls below the reorder point $s$, order up to the level $S$. Existence of such an optimal policy goes back to Scarf (1960) and Iglehart (1963). Knowing that an optimal $(s, S)$ policy exists does not say how to find one, and the average cost of an $(s, S)$ policy is neither convex nor unimodal in $(s, S)$.

Veinott and Wagner (Management Science 11 (1965) 525–552) gave an exact algorithm. It proceeds in three steps: (i) compute integers $\underline{s} \le \bar{s} \le \underline{S} \le \bar{S}$ bounding an optimal policy; (ii) find the set $\mathcal S$ of all policies within those bounds that minimize the cost for starting stocks below $\underline{s}$; (iii) choose from $\mathcal S$ a policy that is optimal for every starting stock. This mission formalizes the theory behind Step iii. It is the third mission of a series on the paper: mission I treats the renewal closed form of the discounted cost, mission II the bounds of Step i.

Setting

Demands $\xi_1, \xi_2, \dots$ are independent non-negative integer random variables with common distribution $\varphi$ and finite mean. Following the paper's Eq. (2), the unit purchase cost and the holding and penalty costs are combined into a single function $G_\alpha : \mathbb Z \to \mathbb R$, assumed convex with $G_\alpha(y) \to \infty$ as $|y| \to \infty$; the set-up cost is $K \ge 0$ and $\alpha$ is the discount factor.

A stationary $(s, S)$ policy, with integers $s \le S$, sets the stock after ordering to

$$Y_t = S \text{ if } X_t < s, \qquad Y_t = X_t \text{ if } X_t \ge s,$$

and the stock evolves as $X_{t+1} = Y_t - \xi_t$ from $X_1 = x$. Its discounted cost is

$$f(x \mid s, S) = \sum_{t \ge 1} \alpha^{t-1} E\bigl[K\delta(Y_t - X_t) + G_\alpha(Y_t)\bigr],$$

where $\delta(z) = 1$ for $z > 0$ and $\delta(0) = 0$, and its equivalent average cost is $a_\alpha(x \mid s, S) = (1-\alpha) f(x \mid s, S)$.

A policy $(s', S')$ is optimal for a set $\mathfrak X$ of integers if, for each $x \in \mathfrak X$, it minimizes $a_\alpha(x \mid s, S)$ over all $(s, S)$ policies; it is optimal if it is optimal for every integer $x$. Under a fixed policy, $x'$ is accessible from $X_1 = x$ if $\Pr(X_t = x' \mid X_1 = x) > 0$ for some $t > 1$.

Below the reorder point the cost does not depend on the starting stock; its value is written $\mathcal L_\alpha(S, D)$ with $D = S - s$. The bounds are: $\underline{S}$ the smallest minimizer of $G_\alpha$; $\bar{S}$ the smallest integer $\ge \underline{S}$ with $G_\alpha(\bar{S}+1) \ge G_\alpha(\underline{S}) + \alpha K$ (21); $\underline{s}$ the smallest integer with $G_\alpha(\underline{s}) \le G_\alpha(\underline{S}) + K$ (22); $\bar{s}$ the smallest integer with $G_\alpha(\bar{s}) \le G_\alpha(\underline{S}) + (1-\alpha)K$ (23). The candidate set $\mathcal S$ consists of the policies with $\underline{s} \le s \le \bar{s}$, $\underline{S} \le S \le \bar{S}$ that minimize $\mathcal L_\alpha(S, S-s)$ among such policies.

Formalization targets

Goal: Theorem 2 (p. 543)

For $0 < \alpha < 1$ and $(s^i, S^i), (s^j, S^j) \in \mathcal S$: if $(s^i, S^i)$ is optimal and every $x'$ with

$$\min(s^i, s^j) \le x' < \max(s^i, s^j)$$

is accessible from $S^j$ under $(s^j, S^j)$, then $(s^j, S^j)$ is optimal.

Milestones

1. §3, p. 533. For $x < s$, $f(x \mid s, S) = K + f(S \mid s, S)$.
2. Theorem 1, p. 542. For $0 \le \alpha < 1$ and $s \le s'$: if $a_\alpha(x \mid s, S) = a_\alpha(x \mid s', S')$ for all $x < s'$, then equality holds for all $x$.
3. Lemma 1, p. 543. For $0 < \alpha < 1$: if $(s, S)$ is optimal for $X_1 = x$, it is optimal for every $x'$ accessible from $x$.

Significance

Theorem 2 turns the final selection step of the algorithm into a reachability check on the demand distribution: a policy of $\mathcal S$ is certified optimal without comparing average costs at every starting stock. Its corollaries give checkable sufficient conditions; for example (Corollary 2.2) if $\varphi(k) > 0$ for $k = 1, \dots, s^n - s^1$, the policy of $\mathcal S$ with the largest reorder point is optimal, which covers Poisson and negative binomial demand. Theorem 1 separately reduces the comparison of two policies to finitely many starting stocks.

The results are proved in the paper (Section 4 and Appendix §3). No machine-checked version is known: the platform has no discrete $(s, S)$ inventory chain, no discounted cost of a stationary policy on $\mathbb Z$, and no accessibility notion for such a chain. The mission produces these objects together with the paper's selection theory on top of them.

Difficulty

Theorem 1 needs a renewal decomposition at the first passage of the stock below $s'$, carried out for expectations over an unbounded integer state space with a discounted infinite sum. Lemma 1 is the delicate step. The paper's argument compares the $(s, S)$ policy with a hybrid policy that follows $(s, S)$ until the stock first reaches $x'$ and then switches to an optimal policy; the inequality "the hybrid cannot be better than the optimal policy" requires that some stationary $(s, S)$ policy is optimal among all ordering policies, including non-stationary ones. That existence result is cited by the paper (Section 2), not proved there. A proof of Lemma 1 within the class of $(s, S)$ policies alone does not go through, because the hybrid policy is not an $(s, S)$ policy.

Formalization scope

All objects live in the namespace VeinottWagnerSS.Selection. The model is the structure Model: the demand distribution φ : PMF ℕ with finite mean, K ≥ 0, and G : ℤ → ℝ convex (non-decreasing forward differences) and tending to $+\infty$ at both ends. The unit cost $c$, the function $L$ and the lead time $\lambda$ do not appear (the paper's own reduction, Eq. (2), p. 529). Stock levels are integers. stateLaw is the law of $X_{t+1}$, obtained by iterated PMF.bind; fCost is the expected discounted cost of that chain as a real series, which converges absolutely for $0 \le \alpha < 1$ because every $Y_t$ lies in $[s, \max(x, S)]$. aCost is $(1-\alpha)$ times fCost. Accessible uses the law of $X_t$ with $t > 1$ strictly. Optimality is among $(s, S)$ policies (p. 536); the class of general ordering policies is not formalized.

The bounds $\underline{s}, \bar{s}, \underline{S}, \bar{S}$ are infima of sets of integers; under the standing assumptions and $\alpha < 1$ these sets are nonempty and bounded below, so each bound is the least integer the paper describes. $\mathcal L_\alpha(S, D)$ is defined as $a_\alpha(S - D - 1 \mid S - D, S)$, the cost at the starting stock just below $s$; that this is the common value for every $x < s$ is milestone 1.

The standing assumptions are kept in every statement, including Theorem 1 and milestone 1, which do not need them; Lemma 1 and Theorem 2 are true only because of them. No printed slip was found in the three results.

Trivializing formalizations are excluded: $f$ is the expected cost of the stock process, not a closed formula or a fixed point of a recursion, so milestone 1 is not definitional; the bounds are the least integers of (21)–(23), not arbitrary integers, so $\mathcal S$ is determined by the data; the goal does not assume that $(s^j, S^j)$ is optimal below $\max(s^i, s^j)$, and Lemma 1 assumes optimality only at the single starting stock $x$.

Useful contributions beyond the milestones: summability lemmas for fCost, the Markov (one-step) equation for fCost, the first-passage decomposition, and, for Lemma 1, a formalization of general ordering policies with the existence of an optimal stationary $(s, S)$ policy. The chain and cost definitions are reusable for other $(s, S)$ results of the paper (Theorem 3, Corollaries 2.1 and 2.2).

Selected references

• A. F. Veinott, Jr. and H. M. Wagner, Computing Optimal (s, S) Inventory Policies, Management Science 11(5), 525–552, 1965. https://doi.org/10.1287/mnsc.11.5.525
• H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
• D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2), 259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259

Motivation

One-dimensional bin packing asks for the fewest unit-capacity bins that hold a given list of items with sizes in $(0,1)$. It is the model behind cutting stock (cutting rolls of paper or steel to ordered widths), memory and file allocation, and batch scheduling on identical machines, and it is NP-hard. Its algorithmic study is therefore about approximation: how close to the optimum a polynomial-time algorithm can guarantee to come.

• 1961–1963: Gilmore and Gomory introduce the configuration linear program for cutting stock and solve it by column generation (Gilmore–Gomory 1961).
• 1974: Johnson, Demers, Ullman, Garey and Graham analyse First Fit and related heuristics, with asymptotic ratio $17/10$ and $11/9$ (Johnson et al. 1974).
• 1981: Fernandez de la Vega and Lueker give the first asymptotic approximation scheme, packing within $(1+\varepsilon)\,OPT(I) + 1$ bins in time linear in $n$ for fixed $\varepsilon$, using elimination of small pieces and linear grouping (Fernandez de la Vega–Lueker 1981).
• 1982: Karmarkar and Karp replace the enumeration of configurations by an approximate solution of the configuration LP and a rounding step, obtaining an additive term polynomial in $1/\varepsilon$ (this mission), and, with geometric grouping, $OPT(I) + O(\log^2 OPT(I))$ (Karmarkar–Karp 1982).
• 2013–2017: Rothvoß and then Hoberg–Rothvoß improve the additive term to $O(\log OPT \cdot \log\log OPT)$ and $O(\log OPT)$ (Hoberg–Rothvoß 2017).

Setting

An instance $I$ is a finite multiset of piece sizes, each in the open interval $(0,1)$. Write $n(I)$ for the number of pieces, $m(I)$ for the number of distinct sizes, and $SIZE(I)$ for the sum of all sizes. A packing of $I$ is a finite multiset of bins, each a multiset of sizes, whose union is exactly $I$ and in which every bin has total size at most $1$. Its cost is the number of bins, and $OPT(I)$ is the minimum cost.

A configuration of $I$ is a nonempty multiset of sizes occurring in $I$ with total at most $1$. With $b_t$ the number of pieces of size $t$ and $a_{tc}$ the number of occurrences of $t$ in configuration $c$, the fractional bin-packing problem is the linear program

$$\min\ \mathbf 1\cdot x\quad\text{s.t.}\quad x\ge 0,\qquad \sum_c a_{tc}x_c \ge b_t\ \ \text{for every size } t,$$

whose optimal value is $LIN(I)$. A basic feasible solution is an extreme point of its feasible region.

For instances $I,J$, write $I\le J$ if there is a one-to-one map $f$ from the pieces of $I$ into the pieces of $J$ with $x\le f(x)$. Linear grouping with parameter $k$ sorts $I$ non-increasingly, cuts it into groups $G_1,\dots,G_q$ of $k$ consecutive pieces (the last possibly shorter), rounds every piece of $G_i$ up to the largest size of $G_i$ to get $G_i'$, and outputs $J = \bigcup_{i\ge 2} G_i'$ and $J' = G_1$.

ALGORITHM 1 takes $I$ and $\varepsilon>0$: (1) discard the pieces of size $\le \max(1/n(I), \varepsilon/2)$, leaving $J$; (2) apply linear grouping to $J$ with $k = \lceil n(J)\varepsilon^2\rceil$, giving $K$ and $K'$; (3) put each piece of $K'$ in its own bin; (4) obtain from a Fractional Bin-Packing subroutine a basic feasible solution $x$ of the LP of $K$ with $\mathbf 1\cdot x\le LIN(K)+1$; (5) round $x$ to a packing of $K$ with at most $\mathbf 1\cdot x + (m(K)+1)/2$ bins; (6) shrink the pieces back to obtain a packing of $J$; (7) insert the discarded pieces, opening a new bin only when a piece fits nowhere. $A(I)$ is the cost of the resulting packing.

Formalization targets

Goal: Theorem 3, as its proof establishes it

$$A(I) \le (1+2\varepsilon)\,OPT(I) + \frac{1}{2\varepsilon^2} + 3 \qquad\text{for every } \varepsilon>0,\ \text{every instance } I,\ \text{every run of ALGORITHM 1.}$$

The additive term depends on $\varepsilon$ only, so ALGORITHM 1 is an asymptotic approximation scheme. The paper prints the factor $1+\varepsilon$, which fails for ALGORITHM 1 as printed (see Formalization scope); running the algorithm with $\varepsilon/2$ gives the paper's main result (4), $A(I)\le(1+\varepsilon)OPT(I)+O(\varepsilon^{-2})$, stated as a separate corollary with the explicit term $2/\varepsilon^2+3$.

Milestones

1. Lemma 1: $OPT(I)\le 2\,SIZE(I)+1$.
2. Lemma 2: $SIZE(I)\le LIN(I)\le OPT(I)\le LIN(I)+\frac{m(I)+1}{2}$.
3. Corollary 1: every basic feasible solution $x$ can be rounded to a packing of cost $\le \mathbf 1\cdot x + \frac{m(I)+1}{2}$.
4. Lemma 3: inserting pieces of size $\le g/2$ last, with new bins only when necessary, costs at most $\max(A, (1+g)\,OPT(I)+1)$.
5. Monotonicity: $I\le J$ implies $OPT$, $LIN$ and $SIZE$ do not decrease.
6. Lemma 4: linear grouping loses at most $k$ in $OPT$, $LIN$ and $SIZE$.
7. Proof steps (ii)–(iii) (corrected): $k\le 2\varepsilon\,OPT(I)+1$.
8. Proof step (iv): $m(K)\le 1/\varepsilon^2$.
9. Proof step (vii): $\mathbf 1\cdot x\le OPT(I)+1$.
10. Proof step (viii) (corrected): the packing of Step 6 has at most $(1+2\varepsilon)OPT(I)+\frac{1}{2\varepsilon^2}+\frac52$ bins.

Significance

The result showed that the configuration LP, of exponential size in general, can be used for a guaranteed approximation: its value is within $(m+1)/2$ of the integer optimum, and grouping reduces $m$ at small cost. The same template (eliminate small items, group, solve the configuration LP, round a basic solution, reinsert) underlies later schemes for bin packing, cutting stock, bin packing with cardinality constraints and scheduling, and the LP-based analysis is the starting point of the Rothvoß and Hoberg–Rothvoß improvements.

The theorems are proved in the literature; none of them has a machine-checked proof on the platform or, to our knowledge, in Mathlib. This mission produces a checked analysis of the algorithm, including a correction: the printed approximation factor is not valid for the algorithm as printed, and the checked statement records the factor its proof yields. The definitions (instances, packings, the configuration LP, basic solutions, the order $I\le J$, any-fit insertion) are reusable for the second mission of the series and for other bin-packing results.

Difficulty

The Lean statements are short, but several proofs need linear-programming structure that is not in Mathlib in this form. Lemma 2 and Corollary 1 use that an extreme point of $\{x\ge0,\ Ax\ge b\}$ has at most as many nonzero coordinates as there are rows of $A$; the configuration LP is indexed by a finite but implicitly described set of multisets. Monotonicity of $LIN$ under $I\le J$ ("clearly" in the paper) requires transporting a fractional solution across a piece-to-piece matching whose images are types, not pieces. The existence of a run requires an optimal basic feasible solution of the configuration LP. Lemma 3 concerns an insertion process with unrestricted order and bin choice, so its bound has to hold for every execution, not for one greedy rule.

Formalization scope

• Sizes are real numbers in the open interval $(0,1)$; the paper says "a rational number between 0 and 1". Real sizes generalize rational ones; the open interval is what the paper's arguments use.
• Instances are Multiset ℝ; packings are Multiset (Multiset ℝ) with join equal to the instance, bin loads at most $1$, empty bins allowed and counted. $OPT$ is a natural-number infimum over a set that is always nonempty.
• LP solutions are Multiset ℝ →₀ ℝ supported on configurations. $LIN$ is a real infimum over a set that is nonempty (singleton configurations) and bounded below by $0$. "Basic" is the extreme-point property; the bound on the number of nonzero coordinates is a consequence, not the definition.
• The Fractional Bin-Packing subroutine is modelled by its contract only (§5, p. 315): any basic feasible solution of cost at most $LIN(K)+1$. The ellipsoid method of §6 is not modelled.
• ALGORITHM 1 is a relation Alg1Run ε I P: $P$ is a possible output. Every open choice is quantified: the subroutine's output, the packing of Step 5 (any packing within the stated bound), the size reduction of Step 6 (bin by bin), and the insertion of Step 7 (any order, any fitting bin). The goal holds for every run, and a separate item states that a run exists, so the goal is not vacuous.
• The paper's $O(\cdot)$ in result (4) is replaced by the explicit $2/\varepsilon^2+3$.
• Corrected statements. The printed Theorem 3 bound $(1+\varepsilon)OPT(I)+\frac{1}{2\varepsilon^2}+3$ fails: for $\varepsilon=1/10$ and $19\,000$ pieces of size $0.051$, some run uses $1180$ bins while the bound is $1153$. The failing step is (ii), $SIZE(J)\ge\varepsilon\,n(J)$, since Step 1 discards only pieces $\le\varepsilon/2$. Steps (ii)–(iii) and (viii) are stated with $2\varepsilon$; step (iv) is stated as $m(K)\le 1/\varepsilon^2$ because its first link $m(K)\le n(K)/k$ fails when the last group is short.
• Running time (Theorem 3's first half, Corollary 1's time bound, the function $T$) is out of scope.
• Trivializations are ruled out: "some packing has at most the bound" is not the goal; the goal constrains every output of the algorithm, and the packing property of that output is part of its conclusion.

Proofs of any item are welcome; Lemma 2, Corollary 1 and the monotonicity display are the most reusable.

Selected references

• N. Karmarkar, R. M. Karp, An Efficient Approximation Scheme for the One-Dimensional Bin-Packing Problem, Proc. 23rd FOCS (SFCS 1982), IEEE, pp. 312–320. https://doi.org/10.1109/sfcs.1982.61
• W. Fernandez de la Vega, G. S. Lueker, Bin packing can be solved within 1+ε in linear time, Combinatorica 1 (1981) 349–355. https://doi.org/10.1007/BF02579456
• P. C. Gilmore, R. E. Gomory, A Linear Programming Approach to the Cutting-Stock Problem, Operations Research 9 (1961) 849–859. https://doi.org/10.1287/opre.9.6.849
• D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms, SIAM J. Comput. 3 (1974) 299–325. https://doi.org/10.1137/0203025
• R. Hoberg, T. Rothvoß, A Logarithmic Additive Integrality Gap for Bin Packing, Proc. SODA 2017, 2616–2625. https://doi.org/10.1137/1.9781611974782.172

Motivation

The Russian option of Shepp and Shiryaev pays its holder, at an exercise time of their choosing, the running maximum of the stock price, discounted, with no fixed maturity. It is the standard example of a perpetual lookback option, and its value is a model problem of optimal stopping for a two-dimensional Markov process (the price and its running maximum). Perpetual contracts are simple to analyse but economically unrealistic: every real contract ends. Canadization (Carr, Randomization and the American put, Rev. Financial Stud. 11, 1998, https://doi.org/10.1093/rfs/11.3.597) replaces a fixed maturity by an independent exponential time $\eta(\lambda)$. The holder must exercise before $\eta(\lambda)$; if they have not, they are paid the claim evaluated at $\eta(\lambda)$. Because the exponential law is memoryless, the problem stays time-homogeneous and its value can be computed in closed form, while it approximates a contract of finite expected life $1/\lambda$.

Avram, Kyprianou and Pistorius (AKP04) solved both the perpetual and the Canadized Russian problem when the log-price is a spectrally negative Lévy process: a process with stationary independent increments whose only jumps are downward. This covers Brownian motion with drift, the Black–Scholes model, and jump-diffusions with downward jumps (crashes). Their answer is written with the scale functions $W^{(q)}$, $Z^{(q)}$ of the process. This mission is the third of three drawn from that paper, and formalizes the Canadized problem (§7, Theorem 3).

Timeline. Shepp and Shiryaev (1993) solved the Russian option for geometric Brownian motion. Carr (1998) introduced Canadization for the American put. Kyprianou and Pistorius (Ann. Appl. Probab. 13, 2003) studied perpetual options through fluctuation theory; §7 of [AKP04] builds on their calculations. Avram, Kyprianou and Pistorius (2004) solved the perpetual and Canadized problems for general spectrally negative Lévy processes.

Setting

Let $(\Omega,\mathcal F,\mathbf F=\{\mathcal F_t\}_{t\ge0},\mathbb P)$ be a filtered probability space with $\mathbf F$ right-continuous, and let $X=\{X_t\}_{t\ge0}$ be a spectrally negative Lévy process adapted to $\mathbf F$: $X_0=0$, paths càdlàg with no upward jumps and not monotone, increments $X_{s+t}-X_s$ stationary and independent of $\mathcal F_s$. The standing assumption is that $X$ has unbounded variation, or bounded variation and a Lévy measure $\Lambda(dx)\ll dx$.

The Laplace exponent is $\psi(\theta)=\log\mathbb E[e^{\theta X_1}]$. Fix $r\ge0$ with $\psi(1)=r$, and let $\mathbb P^1$ be the Esscher measure, $d\mathbb P^1/d\mathbb P|_{\mathcal F_t}=e^{X_t-rt}$.

For $q\ge0$ the $q$-scale function $W^{(q)}:\mathbb R\to[0,\infty)$ vanishes on $(-\infty,0]$, is continuous on $(0,\infty)$, and satisfies $\int_0^\infty e^{-\theta x}W^{(q)}(x)\,dx=(\psi(\theta)-q)^{-1}$ for $\theta>\Phi(q)$, where $\Phi(q)$ is the largest root of $\psi(\theta)=q$. Further, $Z^{(q)}(x)=1+q\int_{-\infty}^xW^{(q)}(y)\,dy$. All scale functions in this mission are those of $(X,\mathbb P)$.

Starting from $Y_0=z\ge0$ (the paper's $\mathbb P^1_{-z}$), the reflected process is $Y_t=\overline X_t-X_t$, where $\overline X_t=\max\{0,\sup_{u\le t}(-z+X_u)\}$ and the position is $-z+X_t$. Its passage time above $k$ is $\tau_k=\inf\{t\ge0:Y_t\notin[0,k)\}$.

Let $\alpha>0$, and let $\eta(\lambda)$ be an exponential random variable of rate $\lambda>0$ which under $\mathbb P^1$ is independent of $\mathcal F_\infty$. The Canadized Russian problem (32) is

$$w^{CR}(z)=\sup_\tau\ \mathbb E^1_{-z}\Big[e^{-\alpha(\tau\wedge\eta(\lambda))+Y_{\tau\wedge\eta(\lambda)}}\Big],$$

over all $\mathbb P^1$-a.s. finite $\mathbf F$-stopping times $\tau$. Write $p=\alpha+\lambda+r$.

Formalization targets

Goal: Theorem 3

With

$$\kappa_*=\inf\{x\ge0:\ Z^{(p)}(x)-pW^{(p)}(x)\le-\lambda/(p-\lambda)\},\qquad h(z)=\frac{(p-\lambda)e^zZ^{(p)}(\kappa_*-z)}{p}+\frac{\lambda e^z}{p},$$

for every $z\ge0$:

$$w^{CR}(z)=h(z),$$

and $\tau_{\kappa_*}$ is a $\mathbb P^1$-a.s. finite $\mathbf F$-stopping time attaining the supremum. The statement covers every variation regime at once.

Milestones

In attack order:

1. Lemma 2 (i), which gives the monotonicity behind $\kappa_*$.
2. Corollary 1 (29), the value of stopping at $\tau_k$ at discount rate $\alpha+\lambda$.
3. The elimination of $\eta(\lambda)$ (display after (32)):

$$\mathbb E^1_{-z}\big[e^{-\alpha(\tau\wedge\eta)+Y_{\tau\wedge\eta}}\big]=\mathbb E^1_{-z}\Big[e^{-(\alpha+\lambda)\tau+Y_\tau}+\lambda\int_0^\tau e^{-(\alpha+\lambda)t+Y_t}dt\Big].$$

4. The Itô identity (34).
5. The expected $d\overline X$-integral up to $\tau_k$.
6. Lemma 3 (33), the value of $\tau_k\wedge\eta(\lambda)$.
7. Lemma 4, with two misprints corrected.
8. The supermartingale property of $U_t=e^{-(\alpha+\lambda)t}h(Y_t)+\lambda\int_0^te^{-(\alpha+\lambda)u+Y_u}du$.
9. The identity $h(z)=e^z+(p-\lambda)e^z\int_0^{\kappa_*-z}W^{(p)}\ge e^z$.

Significance

The result. Theorem 3 gives the price and the optimal exercise rule of a Russian option with random (exponential) maturity, for every spectrally negative Lévy model at once. It makes three things explicit. The optimal rule is a threshold rule for the reflected process $Y$. The threshold $\kappa_*$ is the crossing point of one explicit function of the scale functions. Whenever $W^{(p)}(0+)\ge(p-\lambda)^{-1}$ (possible only with bounded variation), immediate exercise is optimal. Because scale functions are known in closed form for many models, including Brownian motion with drift and hyper-exponential jump-diffusions (§8 of the paper), the theorem produces explicit prices.

Formalizing it. The result is proved on paper. It is not formalized in any proof assistant, and none of its infrastructure is available in Lean. This mission produces:

• a path-level definition of spectrally negative Lévy processes;
• scale functions defined as definite descriptions;
• the reflected process and its passage times;
• the Esscher change of measure as data;
• a continuous-time optimal stopping problem with an independent random horizon, valued in $[0,\infty]$.

A machine-checked proof would also check the verification argument, which the paper states in detail only for the unbounded-variation case.

Difficulty

The obvious route is to compute the value of every threshold rule (Lemma 3) and optimize over $k$. That identifies the right candidate, but it does not show that no other stopping time does better. The verification step needs two things for all regimes of $W^{(p)}(0+)$: that $U$ is a supermartingale, and that $U$ stopped at $\tau_{\kappa_*}$ is a martingale. For processes of bounded variation, $h$ is only continuous, not $C^1$, at $\kappa_*$, so a smooth Itô formula does not apply directly. Computing the expected $d\overline X$-integral up to $\tau_k$ uses excursion theory of $Y$ away from $0$, which Mathlib does not have. Eliminating $\eta(\lambda)$ is easy only if $\eta$ is independent of the whole filtration. If it is independent of $X$ alone, a stopping time could depend on $\eta$.

Formalization scope

• Conventions. Time is $[0,\infty)$ (ℝ≥0) and values are real. Random times take values in WithTop ℝ≥0, and the payoff is $0$ on $\{\tau=\infty\}$. Expectations of nonnegative payoffs are lower Lebesgue integrals in $[0,\infty]$, and $w^{CR}$ is an extended-real supremum, so no expectation defaults to $0$. Equalities with a real right-hand side also assert finiteness.
• Readings of informal words.
  • "The usual conditions" means right-continuity of $\mathbf F$, without completeness. Completing $\mathcal F_0$ with $\mathbb P$-null sets would contradict the Esscher relation, since $\mathbb P^1$ and $\mathbb P$ are typically singular on $\mathcal F_\infty$.
  • "Unbounded variation" means "not almost surely of bounded variation on compacts". (AC) is stated through jumps.
  • "ψ(v) < ∞" means integrability of $e^{vX_1}$.
  • "Decreases monotonically" means strictly decreasing, and "the unique root" means unique on $[0,\infty)$.
  • $W^{(p)}(0+)$ is the right limit.
  • "Almost surely finite" and the law and independence of $\eta(\lambda)$ are all under $\mathbb P^1$, where independence is from $\mathcal F_\infty$. "Parameter $\lambda$" is the rate.
  • $\mathbb P^1_{s,x}$ is encoded pathwise through the reflected process with $Y_0=s-x$.
  • The elimination of $\eta$ is stated τ by τ, which implies the page's equality of suprema.
  • The supermartingale claim, derived on the page in the unbounded-variation case, is stated for all cases.
  • Corollary 1's discount rate is renamed $a$.
  • (34) is stated as $pA+B=e^{s-x}+C$ with $A$, $B$, $C$ finite.
• Definition choices. Scale functions are defined by choice from their defining property, never as hypotheses on an arbitrary function. $W^{(q)}$ for $q<0$ is the series (5), not the tilting formula of Remark 4. $\mathbb P^1$ is a measure given with the Esscher relation. $d\overline X_t$ is the Lebesgue–Stieltjes measure of the running-maximum path.
• Corrected misprints. Lemma 4 is printed with $p^{-1}$ and $-\lambda/p$. The definition of $\kappa_*$ (p. 233) and the proof of Theorem 3 (p. 235) require $(p-\lambda)^{-1}$ and $-\lambda/(p-\lambda)$, and the printed version is false when $p^{-1}\le W^{(p)}(0+)<(p-\lambda)^{-1}$. The corrected statement is formalized.
• Ruled out. A supremum over stopping times of a filtration containing $\sigma(\eta)$, or a real-valued supremum or Bochner expectation that could be $0$ by default, would trivialize the goal or change it. The admissible class is every $\mathbb P^1$-a.s. finite stopping time of the given filtration, of which $\eta$ is independent. Replacing the goal by the $\eta$-free rewriting would state milestone 3 as if it were Theorem 3.
• Needed and reusable. A complete development needs Lévy process theory, scale functions, fluctuation identities for the reflected process, optional stopping in continuous time, and Itô or change-of-variable formulas for semimartingales with jumps. The Lévy-process, scale-function and reflected-process definitions are shared with the other two missions of the series and are reusable in ruin theory and queueing. Proofs of any milestone, and sorry-free facts about the definitions, are welcome.

Selected references

• F. Avram, A. E. Kyprianou, M. R. Pistorius, Exit problems for spectrally negative Lévy processes and applications to (Canadized) Russian options, Ann. Appl. Probab. 14(1), 215–238, 2004. https://doi.org/10.1214/aoap/1075828052
• P. Carr, Randomization and the American put, Rev. Financial Stud. 11(3), 597–626, 1998. https://doi.org/10.1093/rfs/11.3.597
• L. A. Shepp, A. N. Shiryaev, The Russian option: reduced regret, Ann. Appl. Probab. 3, 603–631, 1993. https://doi.org/10.1214/aoap/1177005715
• A. E. Kyprianou, M. R. Pistorius, Perpetual options through fluctuation theory, Ann. Appl. Probab. 13, 1077–1098, 2003. https://doi.org/10.1214/aoap/1060202835
• J. Bertoin, Lévy Processes, Cambridge University Press, 1996.

Motivation

Two strategic levers shape the balance of power between a manufacturer and the retailer that resells its product. The first is strategic inventory: a buyer that orders more than it sells today, and carries the surplus into the next period, weakens the supplier's leverage over tomorrow's wholesale price. Anand, Anupindi and Bassok (Management Science 2008) showed that in a two-period channel the buyer withholds inventory exactly when its unit holding cost is below $\alpha/4$. The second is supplier encroachment: a supplier that can sell directly to consumers competes with its own buyer. Arya, Mittendorf and Sappington (Marketing Science 2007) showed that the threat of encroachment can lower wholesale prices and benefit both parties.

Guan, Gurnani, Geng and Luo, Strategic Inventory and Supplier Encroachment (MSOM 2019), combine the two levers in one game. Their headline qualitative finding is Proposition 4.2. When the supplier's direct channel is costly, but not quite too costly to use, the buyer keeps withholding inventory at every finite holding cost. This contrasts with the $\alpha/4$ cutoff of Anand et al. This mission formalizes that proposition, together with the equilibrium characterizations of Appendix A on which it rests.

Setting

There is one supplier and one buyer, two periods, deterministic demand and complete information. In each period the market price is $p = \alpha - q$, where $q$ is the total quantity sold in that period and $\alpha > 0$ is the demand intercept. The buyer pays a per-unit holding cost $h \ge 0$ on inventory carried into period 2. The supplier pays a per-unit direct selling cost $s \ge 0$. All other costs and the salvage value are zero. The moves are:

1. The supplier quotes a wholesale price $w_1 \ge 0$.
2. The buyer orders $Q_1$ and sells $q_1$, with $0 \le q_1 \le Q_1$. It carries the inventory $I = Q_1 - q_1$ into period 2.
3. The supplier quotes $w_2 \ge 0$.
4. The buyer orders $Q_2 \ge 0$ and sells $q_2$, with $0 \le q_2 \le I + Q_2$.
5. Having observed everything, the supplier sells $q_s \ge 0$ directly. The period-2 price is $\alpha - q_2 - q_s$.

The total profits are

$$\Pi_b = (\alpha - q_1)q_1 - w_1 Q_1 - hI + (\alpha - q_2 - q_s)q_2 - w_2 Q_2, \qquad \Pi_s = w_1 Q_1 + w_2 Q_2 + (\alpha - q_2 - q_s - s)q_s .$$

A strategy profile assigns an action to every history at which a player moves. It is a subgame perfect equilibrium (SPE) if, at every feasible history, the mover's prescribed action is feasible and no feasible alternative, followed by the profile afterwards, raises the mover's total profit. The equilibrium path is the outcome the profile generates; the equilibrium inventory is $I$ on that path. Following the paper (§4), the goal theorem sets $\alpha = 1$.

Formalization targets

Goal: Proposition 4.2

With $\alpha = 1$,

$$\forall h > 0\ \ \exists \epsilon > 0\ \ \forall s \in \big(\tfrac56 - \epsilon, \tfrac56\big):\quad \text{an SPE exists, and every SPE has } I > 0 \text{ and } hI < \tfrac{11}{72}.$$

Here $\epsilon$ may depend on $h$, and the bound $11/72$ applies at the same $(h, s)$.

Milestones, in attack order

1. Stage-3 best response (§3.1.1): in every SPE, the supplier sells $q_s = (\alpha - q_2 - s)^+/2$ at every history.
2. Eq. (1) (§3.1.1): with no inventory, the buyer's period-2 quantity is the four-branch function $q_b(w)$ of the period-2 wholesale price $w$.
3. Proposition 4.1, existence half: an SPE exists for every $h \ge 0$ and $s \ge 0$.
4. Region 8 (Tables A.1 and A.4): for $h < h_{11}$ with $s_3 \le s < 5\alpha/6$, or for $h < \alpha/4$ with $5\alpha/6 \le s < \alpha$, every SPE has $I = 5(\alpha - 4h)/34$ and the path of Table A.4.
5. Region 7, second part (Tables A.1 and A.3): for $h_{11} < h < h_{10}$ and $s_3 \le s < 5\alpha/6$, every SPE has $I = I^* = (2\alpha - 3s + x)/2$ and the path of Table A.3.
6. Region 10, second part (Tables A.1 and A.4): for $h > h_7$ and $2\alpha/3 < s < 5\alpha/6$, every SPE has $I = 0$.

The thresholds $x$, $s_3$, $h_7$, $h_{10}$, $h_{11}$ are explicit algebraic functions of $s$, given in Appendix A.

Significance

Proposition 4.2 separates the combined model from the two models it merges. Without a direct channel, inventory disappears once $h \ge \alpha/4$. With a direct channel, a threat of encroachment that is only barely credible keeps inventory alive at every holding cost. The total holding cost nevertheless stays below a constant, because the inventory shrinks as $h$ grows. Milestone 6 shows the flip side: for a fixed $s < 5\alpha/6$, a large enough $h$ removes the inventory. This is why the window $\epsilon$ must depend on $h$.

The paper's proofs are in an online appendix that is not reproduced in the article. The article itself gives the equilibrium only as tables. A formal development would supply a checked backward-induction proof of those tables in the regions near $s = 5\alpha/6$. It would also give a machine-checked SPE framework for multi-stage pricing-and-quantity games in supply chains, which none of the following exists for: Stackelberg pricing, sequential quantity competition, or dual-channel encroachment. No part of this paper has been formalized before.

Difficulty

The equilibrium is found by backward induction through five stages. Each stage's value function is only piecewise smooth, because the supplier's direct-channel response $(\cdot)^+$ switches on and off. As a result the buyer's period-2 profit has kinks, the supplier's period-2 profit as a function of $I$ has several local maxima, and the period-1 problems must compare branches whose boundaries are the irrational thresholds of Appendix A. The obvious approach, solving the first-order conditions stage by stage, fails at the kinks. At some region boundaries it also misses that the supplier is indifferent between two first-period prices, which makes the equilibrium path change discontinuously. Proposition 4.2 then needs uniform control of $h_7$, $h_{10}$ and $h_{11}$ as $s \uparrow 5/6$, where the denominator $3s - 2 - x$ of $h_7$ tends to $0$.

Formalization scope

• Representation. Strategies are functions of the full history, not Markov rules in $I$. IsSPE imposes optimality at every feasible history, including off-path ones. All actions are real numbers; wholesale prices and quantities are nonnegative, with $q_1 \le Q_1$ and $q_2 \le I + Q_2$.
• Normalization. The goal instantiates $\alpha = 1$ as the paper does from §4 on. The milestones keep a general $\alpha > 0$.
• Uniqueness is not stated. Proposition 4.1's uniqueness claim is false for strategy profiles: after the off-path price $w_2 = 0$, every order $Q_2 \ge q_2 - I$ is optimal. The goal and the region milestones therefore quantify over every SPE and carry existence as a separate conjunct.
• Corrected hypotheses.
  • The printed $s_3 = (\sqrt{(37 - 3\sqrt{65})/34} + 4/6)\alpha \approx 1.28\alpha$ is replaced by $(\sqrt{37 - 3\sqrt{65}}/34 + 4/6)\alpha \approx 0.772\alpha$, which matches the paper's "≈0.77".
  • Eq. (1) excludes the corner $w = 0$, $s < \alpha/3$, where its second branch is wrong.
  • Region 8 drops its boundary $h = h_{11}$ and Region 7 drops $h = h_{10}$, because the equilibrium path switches there and need not be unique.
• Ruled-out trivialization. The inventory in the goal is the inventory on the path of an SPE of the game above. It is not the closed form $5(1 - 4h)/34$ or $I^*$ from the tables, and the regional characterization is not a hypothesis. Otherwise the goal would reduce to algebra about the thresholds.
• Infrastructure and contributions. The definitions Game, IsSPE and Thresholds are shared by every statement. Welcome contributions include:
  • lemmas on maximizing concave piecewise-quadratic functions on half-lines;
  • a reusable backward-induction lemma for finite-stage games with real action sets;
  • interval-arithmetic facts about $x$, $h_7$, $h_{10}$ and $h_{11}$ near $s = 5/6$;
  • proofs of the paper's other regions.

Selected references

• T. Guan, H. Gurnani, X. Geng, Y. Luo, Strategic Inventory and Supplier Encroachment, Manufacturing & Service Operations Management 21(3):536–555, 2019. https://doi.org/10.1287/msom.2018.0705
• K. Anand, R. Anupindi, Y. Bassok, Strategic Inventories in Vertical Contracts, Management Science 54(10):1792–1804, 2008. https://doi.org/10.1287/mnsc.1080.0894
• A. Arya, B. Mittendorf, D. Sappington, The Bright Side of Supplier Encroachment, Marketing Science 26(5):651–659, 2007. https://doi.org/10.1287/mksc.1070.0280

Motivation

A competitive equilibrium is a list of production plans, consumption plans and prices at which every firm maximizes profit, every consumer maximizes utility within the budget, and no market has excess demand. Whether such prices exist at all is the consistency question behind general equilibrium theory, the welfare theorems, and applied equilibrium models used in policy analysis. Arrow and Debreu gave the first proof of existence for a model with production, private ownership and general convex preferences (Econometrica 22, 1954), using Debreu's existence theorem for abstract economies (PNAS 38, 1952).

Their Theorem I assumes that every consumer initially holds a positive amount of every commodity (Assumption IV.a). The authors call this "clearly unrealistic" (p. 280): a household does not hold every good, and most households own little beyond their labor. Theorem II, the subject of this mission, removes that assumption. It only asks that every consumer be able to supply some type of labor that is always productive of a commodity everyone desires. This is the version of the existence theorem that allows a wage-earner economy.

Timeline. Wald (1935–36) proved existence for special production models. Nash (1950) proved existence of equilibrium points for finite games, and Debreu (1952) extended it to abstract economies, in which each player's feasible set depends on the others' choices. Arrow and Debreu (1954) proved Theorems I and II. McKenzie's independent existence proof was published the same year (Econometrica 22, 1954).

Setting

There are $l$ commodities, $n$ producers and $m$ consumers; vectors live in $\mathbb R^l$ and $x\leqq y$ is componentwise. Producer $j$ has a production set $Y_j$. Consumer $i$ has a consumption set $X_i$, a utility $u_i$ on $X_i$, an endowment $\zeta_i$ and profit shares $\alpha_{ij}$. Write $Y=\sum_jY_j$, $X=\sum_iX_i$, $\zeta=\sum_i\zeta_i$, and let $P=\{p\geqq0,\ \sum_hp_h=1\}$ be the price simplex. A competitive equilibrium $(x_1^*,\dots,x_m^*,y_1^*,\dots,y_n^*,p^*)$ satisfies four conditions. Each $y_j^*$ maximizes $p^*\cdot y_j$ on $Y_j$. Each $x_i^*$ maximizes $u_i$ on $\{x_i\in X_i: p^*\cdot x_i\le p^*\cdot\zeta_i+\sum_j\alpha_{ij}p^*\cdot y_j^*\}$. The price vector satisfies $p^*\in P$. Finally $z^*=\sum x_i^*-\sum y_j^*-\zeta\leqq0$ and $p^*\cdot z^*=0$.

The assumptions of Theorem II are as follows. I: production sets are closed, convex and contain $0$; $Y\cap\Omega=\{0\}$ (no output without input); $Y\cap(-Y)=\{0\}$ (no reversible production). II: each $X_i$ is closed, convex and bounded below. III: $u_i$ is continuous, has no satiation point, and satisfies $u_i(tx+(1-t)x')>u_i(x')$ whenever $u_i(x)>u_i(x')$ and $0<t<1$. IV.b: shares are nonnegative and sum to one for each firm. Two sets of commodities are defined from the data. The set $\mathcal D$ contains the commodities always desired by every consumer: from any $x_i\in X_i$, adding some positive amount of the commodity stays in $X_i$ and raises $u_i$. The set $\mathcal P$ contains the types of productive labor: for every $y\in Y$, (a) $y_h\le0$, and (b) some $y'\in Y$ satisfies $y'_{h'}\ge y_{h'}$ for all $h'\ne h$ and $y'_{h''}>y_{h''}$ for some $h''\in\mathcal D$. The remaining assumptions are:

• IV′.a: each consumer has some $x_i\in X_i$ with $x_i\leqq\zeta_i$ and $x_{hi}<\zeta_{hi}$ for some $h\in\mathcal P$;
• V: some $x\in X$ and $y\in Y$ satisfy $x_h<y_h+\zeta_h$ for every $h$;
• VI: $\mathcal D\ne\emptyset$;
• VII: $\mathcal P\ne\emptyset$.

Formalization targets

Goal: Theorem II (§4.5, p. 281)

$$\text{Assumptions I–III, IV}',\ \text{V–VII}\ \Longrightarrow\ \exists\,(x^*,y^*,p^*)\ \text{satisfying Conditions 1–4.}$$

Milestones (§5, pp. 282–287)

They follow the paper's proof. Let $\pi=|\mathcal P|$ and $P^\varepsilon=\{p\in P: p_h\ge\varepsilon\ \forall h\in\mathcal P\}$ for $0<\varepsilon\le1/(2\pi)$. Let $E^\varepsilon$ be the abstract economy in which consumers maximize utility under budget constraints, producers maximize profit, and a market participant chooses $p\in P^\varepsilon$ to maximize $p\cdot z$. The milestones are:

1. §5.0 (1). On $P^\varepsilon$ every consumer can spend strictly less than $p\cdot\zeta_i$.
2. §5.1.1 (5). Equilibrium points of $E^\varepsilon$ satisfy $x^*-y^*\leqq\zeta'$ for a vector $\zeta'$ independent of $\varepsilon$.
3. §5.2.0. The attainable sets relative to $\zeta'$ are bounded.
4. §5.2.1. The truncated economy $\tilde E^\varepsilon$ has an equilibrium point.
5. §5.2.2 (3)–(5). An equilibrium point of $\tilde E^\varepsilon$ is one of $E^\varepsilon$.
6. §5.3.0 (2). If $p^*_h>\varepsilon$ for all $h\in\mathcal P$, the point is a competitive equilibrium.
7. §5.3.2 (1). Limits of equilibrium points as $\varepsilon\to0$ are quasi-equilibria for consumers.
8. §5.3.4 (3). If the floors bind, some desired commodity has limit price $0$.
9. §5.3.4 (6). If the floors bind, limit consumption minimizes expenditure over $X_i$.
10. §5.3.5. For some $\varepsilon$ the floor does not bind.

Significance

Theorem II is the existence theorem for a competitive economy in which consumers may own nothing but their labor. It shows that the survival assumption IV.a can be traded for conditions on labor, desirability and the possibility of an overall excess supply. Section 5.3.3 of the paper also isolates the quasi-equilibrium, in which utility maximization under the budget is replaced by cost minimization at a given utility level. That notion is used in later existence and welfare arguments.

The theorem has been proved since 1954; this mission does not reopen it. The work here is the machine-checked proof. The companion mission on Theorem I formalizes the shared model and Debreu's lemma. As of September 2026 neither theorem has a Lean formalization on the platform, and Mathlib contains no general equilibrium theory.

Difficulty

The obvious approach reuses the proof of Theorem I: build the abstract economy of consumers, producers and a price-choosing participant, and apply Debreu's lemma. That fails at the boundary of the price simplex. Without IV.a, a consumer's cheapest point in $X_i$ can cost as much as the endowment at some prices, so the budget correspondence is not continuous there and the lemma does not apply. The paper therefore keeps prices of productive labor at least $\varepsilon$ and must then show that the floor does not bind for some $\varepsilon$. That is a limit argument as $\varepsilon\to0$ which uses Assumptions V, VI and VII together, and each of the milestones 7–9 is a step of it. Debreu's lemma itself needs a Kakutani-type fixed point theorem for correspondences, which Mathlib does not provide.

Formalization scope

Commodity vectors are Fin l → ℝ. Consumers are indexed by Fin m and producers by Fin n. The inner product is ⬝ᵥ. The paper's $x<y$ is strict in every component and is written componentwise, never as Lean's < on functions. $\mathcal D$ and $\mathcal P$ are computed from the economy, not supplied as parameters. Utilities are total functions, but every assumption on $u_i$ quantifies over $X_i$ only. "Maximizes" is membership plus an inequality against every feasible alternative; no supremum is used. $E$, $E^\varepsilon$ and $\tilde E^\varepsilon$ are built by one constructor over the players Fin m ⊕ Fin n ⊕ Unit. The vector $\zeta'$ takes the lower bounds $\xi_i$ of Assumption II as an explicit argument. The milestones of §5.3 are stated for the limit of a sequence of equilibrium points, which is how the paper constructs them. Assumption V is dropped from every milestone except §5.3.5 and the goal. With V, the case assumption of §5.3.1 is contradictory and those milestones would hold vacuously.

A trivializing formalization is ruled out as follows. The assumptions are satisfiable with IV.a failing: a sorry-free check covers two goods, one consumer who owns nothing and can only supply labor, and one firm turning labor into the desired good. The goal therefore does not hold vacuously.

Needed infrastructure includes a Kakutani fixed point theorem or Debreu's lemma, compactness of truncated action sets, and sequential compactness arguments in $\mathbb R^l$. AGT.brouwer_fixed_point is on the platform and can serve as a starting point. The lemma is reusable well beyond this mission. Contributions to any milestone, to the lemma, or to the boundedness results shared with Theorem I are welcome.

Selected references

• K. J. Arrow and G. Debreu, Existence of an Equilibrium for a Competitive Economy, Econometrica 22(3), 265–290, 1954. https://doi.org/10.2307/1907353
• G. Debreu, A Social Equilibrium Existence Theorem, Proceedings of the National Academy of Sciences 38(10), 886–893, 1952. https://doi.org/10.1073/pnas.38.10.886
• L. W. McKenzie, On Equilibrium in Graham's Model of World Trade and Other Competitive Systems, Econometrica 22(2), 147–161, 1954. https://doi.org/10.2307/1907352
• J. F. Nash, Equilibrium Points in n-Person Games, Proceedings of the National Academy of Sciences 36(1), 48–49, 1950. https://doi.org/10.1073/pnas.36.1.48