Operations Research

Motivation

Demand for many products does not arrive at a constant rate. It moves with an underlying environment: the economy, the season, a product's life-cycle stage, the state of a customer's own operations. Song and Zipkin (Oper. Res. 41(2):351–370, 1993) modelled this environment as a continuous-time Markov chain, the world, whose current state sets the Poisson demand rate, and showed that a basestock policy whose level depends on the current world state is optimal under linear order costs. Missions I and II of this series formalize those optimality results.

A practitioner who uses such a policy wants to know how the levels depend on the world. If a higher world state means more demand now and more demand later, a higher level should be kept. That is what intuition says, but the optimal level depends on the whole future of the world chain, not only on the current demand rate. §4 of the paper answers it for a world with an arbitrary partial order, which covers several independent demand drivers at once.

Setting

The world $A$ is a continuous-time Markov chain on a countable set $\mathbf I$ with generator $Q = (q_{ij})$, $q_i = -q_{ii}$, and bounded rates $q^* = \sup_i q_i$, $\lambda^* = \sup_i \lambda_i$. While $A = i$, unit demands arrive at rate $\lambda_i$, all demand is backlogged, and orders arrive after a random lead time $L$ that is independent of the world and the demand. Costs are discounted at rate $\alpha > 0$. With the unit order cost $\bar c$, holding rate $h$ and penalty rate $p$, set $c = \bar c\,E[e^{-\alpha L}]$ and

$$\hat C(x) = \max\{-px,\ hx\}, \qquad C(i,y) = E\big[e^{-\alpha L}\hat C(y - D^i_L)\big],$$

where $D^i_L$ is the demand during a lead time when the world starts in $i$. Uniformizing at a rate $\mu \ge q^* + \lambda^*$ with $\beta = 1/(\mu+\alpha)$ and $\gamma = \beta\mu$, the myopic cost is $G^+(i,y) = (1-\gamma)cy + \beta C(i,y)$. The linear-cost model ($K = 0$) is solved by value iteration from $W_0 \equiv 0$:

$$G_n(i,y) = G^+(i,y) + \beta\lambda_i c + \beta\Big\{\lambda_i W_{n-1}(i,y-1) + \sum_{j\ne i} q_{ij}W_{n-1}(j,y) + (\mu-\lambda_i-q_i)W_{n-1}(i,y)\Big\},$$

$W_n(i,x) = \min_{y\ge x} G_n(i,y)$, with limits $G_\infty$ and $W_\infty$. The myopic level $y^+(i)$, the finite-horizon levels $y^*_n(i)$ and the optimal level $y^*(i)$ are the smallest minimizers of $G^+(i,\cdot)$, $G_n(i,\cdot)$ and $G_\infty(i,\cdot)$, and $y^*_\infty(i) = \lim_n y^*_n(i)$. Throughout, $\alpha\bar c < p$ (Assumption 1).

The world states carry a partial order $\preceq$. The chain is stochastically partial-monotone (display (14)) if for every $i \preceq j$ there is a probability space carrying copies of $A$ started at $i$ and at $j$ whose paths satisfy $A(t) \preceq A'(t)$ for all $t \ge 0$ almost surely. Condition 1 requires this together with $\lambda_i$ nondecreasing in $i$.

Formalization targets

Goal: Theorem 8

Under Condition 1, the three families of levels exist and are nondecreasing along $\preceq$:

$$i \preceq j \ \Longrightarrow\ y^+(i) \le y^+(j),\qquad y^*(i) \le y^*(j),\qquad y^*_\infty(i) \le y^*_\infty(j).$$

Milestones

• Lemma 8, with its fixed-lead-time form from the proof: $D(l)$ given $A(0)=i$ is stochastically smaller than given $A(0)=j$ for each $l \ge 0$, and $D^i_L \le_{st} D^j_L$.
• Lemma 9: $\Delta C(i,y) \ge \Delta C(j,y)$ for $i \preceq j$.
• Theorem 7: for all $n \ge 1$ and fixed $x$, $\Delta W_{n-1}(i,x)$ and $\Delta G_n(i,x)$ are nonincreasing in $i$, and $y^*_n(i)$ is nondecreasing in $i$.
• Theorem 9 (companion): if $q_{ij} \ne 0$ only for $j \succeq i$, then $y^*(i) = y^+(i)$, so the myopic policy is optimal.
• Theorem 10 (companion): with a fixed order cost $K > 0$, the bounds $S^+(i)$, $r^+(i)$, $r^-(i)$, $r^{--}(i)$ on the optimal $(r,S)$ parameters are nondecreasing in $i$.

Significance

Theorem 8 turns an optimal policy into a structured one. A world-dependent basestock policy has one level per world state; monotonicity says the levels follow the order of the states, which reduces search, makes the levels interpretable, and gives sanity checks for computed solutions. Theorem 9 identifies when nothing beyond the one-step cost needs to be computed at all. Theorem 10 is the paper's substitute for an open question: the authors could not show that the optimal $(r,S)$ parameters are monotone, and instead bound them between monotone functions.

All of these results are proved in the paper. None of them has been machine-checked. The formalization requires a value-iteration argument for a model with unbounded one-period costs, a coupling argument for Markov-modulated Poisson demand, and the passage to the limit in the levels. These are the ingredients of most monotone-policy results in inventory theory with Markov-modulated demand.

Difficulty

The obvious argument fails at the generator. For a single scalar world, stochastic monotonicity is equivalent to the expectation inequality (15) for nondecreasing functions, and the inductive step of Theorem 7 only needs that. For a partial order, the expectation inequality is strictly weaker than the coupling (14) (Massey 1987). The induction must also handle the cross term $\sum_j q_{ij}\Delta W_{n-1}(j,x)$, which requires an embedded discrete-time chain whose one-step kernel preserves the order. The paper's Lemma 7 asserts that the embedded chain $P = I + Q/\nu$ is monotone for every $\nu \ge q^*$. As printed, this is false at $\nu = q^*$: for two states with $q_{01} = q_{10} = 1$, $P$ swaps the states. A complete proof cannot rely on that lemma as printed.

A second difficulty is that the one-period cost is unbounded. The classical theorems that ordered differences survive value iteration (Denardo, Lovejoy) assume bounded costs, so the induction has to be carried out by hand, and the limits $G_\infty$, $y^*_\infty$ must be justified by Lemma 4's uniform bounds.

Formalization scope

The Lean development lives in the namespace SongZipkinFluct.Monotone. World states form a countable nonempty type with a PartialOrder instance; no linear order is assumed. Inventory positions are integers. The demand-count law $f_i(d\mid l)$ and the world transition function $P(t)$ are defined by uniformization at the model's rate $\mu$, the paper's own device. The lead-time law is a probability measure on $[0,\infty)$, and $C(i,y)$ is the series $\sum_d g_i(d\mid\alpha)\hat C(y-d)$ of display (16). $W_n$ uses an infimum over integers $y \ge x$, and $W_\infty$, $G_\infty$ are suprema over $n$, which equal the limits because the sequences are nondecreasing and bounded. Monotonicity in $i$ is Monotone/Antitone with respect to $\preceq$. Smallest minimizers, maxima and minima are IsLeast/IsGreatest characterizations, never sInf on $\mathbb Z$.

Condition 1(a) is encoded as the coupling (14) itself, with one probability space per pair $i \preceq j$ and copies identified by their finite-dimensional distributions. Replacing it by the expectation inequality (15), or the partial order by a total order, would change the theorem and is ruled out. Every goal statement asserts the existence of the levels it constrains before constraining them, so no conclusion holds vacuously. The standing hypotheses together with Condition 1 are satisfiable: a one-state instance is checked in Lean.

Lemma 7 is not included because it is false as printed. A guarded version (for instance with $\nu \ge 2q^*$) would be a welcome contribution. Reusable parts include the uniformized Markov-modulated Poisson process, the coupling definition of stochastic monotonicity for a countable partially ordered state space, and the usual stochastic order on $\mathbb N$. Proofs of Lemma 9 and Theorem 7 that avoid Lemma 7 are particularly welcome.

Selected references

• J.-S. Song and P. Zipkin, Inventory Control in a Fluctuating Demand Environment, Operations Research 41(2):351–370, 1993. https://doi.org/10.1287/opre.41.2.351
• W. A. Massey, Stochastic orderings for Markov processes on partially ordered spaces, Mathematics of Operations Research 12(2):350–367, 1987. https://doi.org/10.1287/moor.12.2.350
• J. Keilson and A. Kester, Monotone matrices and monotone Markov processes, Stochastic Processes and their Applications 5(3):231–241, 1977. https://doi.org/10.1016/0304-4149(77)90033-3
• A. F. Veinott Jr., Optimal policy for a multi-product, dynamic, nonstationary inventory problem, Management Science 12(3):206–222, 1965. https://doi.org/10.1287/mnsc.12.3.206
• W. S. Lovejoy, Ordered solutions for dynamic programs, Mathematics of Operations Research 12(2):269–276, 1987. https://doi.org/10.1287/moor.12.2.269

Optional stopping and the size of a test

Section 4 of Herbert Robbins's 1952 address Some aspects of the sequential design of experiments (Bull. Amer. Math. Soc. 58, 527–535, doi:10.1090/S0002-9904-1952-09620-8) isolates a problem that every user of significance tests meets: if the sample size is not fixed in advance, an experimenter can keep sampling until the test rejects. Robbins shows that a fixed-sample test then loses all control of its error probability, and he proposes the compromise of allowing the sample size to range over a window $n_1\le n\le n_2$, with an explicit bound on the resulting error.

The question is still current. "Optional stopping" and "peeking" at accumulating data are a standard concern in clinical trials and online A/B testing, and the modern theory of always-valid inference and confidence sequences (for example Howard, Ramdas, McAuliffe and Sekhon, Time-uniform, nonparametric, nonasymptotic confidence sequences, Ann. Statist. 49 (2021), arXiv:1810.08240) answers exactly the question Robbins raises: how large is the probability that a running statistic crosses a boundary at some time in a range. The earlier treatment Robbins cites is Feller's 1940 discussion of the statistics of ESP experiments.

Setting

Let $x_1,x_2,\dots$ be independent real random variables on a probability space $(\Omega,\mathcal F,P)$, each normal with mean $0$ and variance $1$. This is the null hypothesis $H_0:\theta=0$ for observations that are normal with unknown mean $\theta$ and unit variance; the alternative is $H_1:\theta>0$. Write

$$S_n=x_1+\cdots+x_n,\qquad S_0=0 .$$

The fixed-sample test of size $n$ rejects $H_0$ if and only if

$$S_n>\alpha n^{1/2}\qquad(21)$$

for a real constant $\alpha$. (In this mission $\alpha$ always denotes this test constant; in Section 2 of the paper the same letter is the mean of a coin.) The standard normal distribution function is

$$\Phi(x)=\frac{1}{(2\pi)^{1/2}}\int_{-\infty}^{x}e^{-t^2/2}\,dt .\qquad(23)$$

For integers $n_1\le n_2$ the window probability is

$$g(n_1,n_2,\alpha)=P\bigl[S_n>\alpha n^{1/2}\ \text{for some}\ n_1\le n\le n_2\bigr],\qquad(24)$$

and $\lambda=n_2/n_1$. In Lean these are Phi, S X n ω = ∑ i ∈ Finset.range n, X i ω and g P X n₁ n₂ α, in the namespace RobbinsSeqDesign.OptionalStopping.

Formalization targets

Goal: the window bound (25)

For integers $1\le n_1<n_2$ and every real $\alpha$, with $\lambda=n_2/n_1$,

$$g(n_1,n_2,\alpha)<\frac{1-\Phi(\alpha)}{1-\Phi\!\Bigl(\alpha\cdot\dfrac{\lambda^{1/2}-1}{(\lambda-1)^{1/2}}\Bigr)} .$$

The inequality is strict, as printed, and holds for every real $\alpha$, not only the large values of practical interest.

Milestone: the fixed-sample error (22)

For every $n\ge1$ and real $\alpha$,

$$\varepsilon(\alpha)=P\bigl[S_n>\alpha n^{1/2}\bigr]=1-\Phi(\alpha).$$

Milestone: rejection infinitely often

For every real $\alpha$, with probability $1$ the inequality $S_n>\alpha n^{1/2}$ holds for infinitely many $n$.

Significance

The results. (22) says that the fixed-sample test has error probability $1-\Phi(\alpha)$ whatever $n$ is. The infinitely-often statement says that this guarantee is void under unrestricted optional stopping: sampling until (21) holds rejects a true $H_0$ with probability one, however large $\alpha$ is. The goal (25) quantifies the compromise: if the stopping time is confined to $[n_1,n_2]$, the error probability is at most the fixed-sample error divided by $1-\Phi(\alpha c_\lambda)$, where $c_\lambda=(\lambda^{1/2}-1)/(\lambda-1)^{1/2}<1$ depends only on the window's ratio. For large $\alpha$ and moderate $\lambda$ this keeps the error of the same order as the fixed-sample error; Robbins notes that it is useful when $\lambda$ is not too large and that sharper inequalities can be devised.

Formalizing it. The three statements are classical and their proofs are short on paper, but none is machine-checked for Gaussian partial sums. The goal needs stopping-time machinery for discrete-time Gaussian random walks; the infinitely-often statement is a consequence of the lower half of the law of the iterated logarithm, which Mathlib does not contain. On the platform, DurrettProbability.brownian_limsup_sqrt (proved) gives $\limsup_t B_t/\sqrt t=\infty$ for Brownian motion, a different process, and AzumaWeightedSums.IteratedLog.theorem2_limsup_le_one gives an upper iterated-logarithm bound for weighted sums, the opposite direction; neither states any of the targets here, but both are related infrastructure.

Difficulty

The goal is a maximal inequality over a window of times. The obvious argument, a union bound over $n_1\le n\le n_2$, gives $(n_2-n_1+1)(1-\Phi(\alpha))$, which grows with the window length instead of depending on $\lambda$ alone, and exceeds $1$ for long windows. The events $\{S_n>\alpha n^{1/2}\}$ for different $n$ are strongly dependent, and the boundary $\alpha n^{1/2}$ is curved, so the bound has to account for when, inside the window, the boundary is first crossed; this requires stopping-time arguments for a discrete-time walk that are not yet available for Gaussian random walks in Mathlib. The strictness of the inequality also has to be tracked through the argument. The infinitely-often statement cannot be obtained from the central limit theorem alone, which gives only $P(S_n>\alpha n^{1/2}\ \text{i.o.})\ge 1-\Phi(\alpha)>0$; upgrading this to probability one needs a zero–one law or the law of the iterated logarithm.

Formalization scope

The observations are X : ℕ → Ω → ℝ on a probability space (Ω, P) with [IsProbabilityMeasure P], iIndepFun X P and ∀ i, HasLaw (X i) (gaussianReal 0 1) P; the paper's $x_i$ is X (i - 1). The explicit readings committed to are:

• $\Phi$ is the integral printed in (23) (a local check shows it equals Mathlib's cdf (gaussianReal 0 1)).
• "The probability of rejecting $H_0$" is P.real of the event; (22) is stated for $n\ge1$.
• "With probability 1 … for infinitely many values of $n$" is ∀ᵐ ω ∂P, ∃ᶠ n in atTop, α * √n < S X n ω, for every real $\alpha$.
• The window of (24) is $n_1\le n\le n_2$ with both endpoints; the stray comma printed in "$n_1, \le n$" is a typesetting slip.
• In (25), $\lambda$ is the real quotient $n_2/n_1$, and the hypotheses $1\le n_1<n_2$ make $\lambda>1$ well defined; the inequality is strict and there is no sign restriction on $\alpha$.
• The numeric example "$\alpha=3.09$ then $\varepsilon(\alpha)\cong .001$" and the phrase "useful when $\lambda$ is not too large" are not formalized.

A trivializing formalization is ruled out: $g$ is the probability of the union over the whole window (not the event at $n=n_2$ alone), $\Phi$ is the fixed standard normal distribution function (not an arbitrary monotone function), and the parameter range excludes $\lambda=1$, where Lean's convention $x/0=0$ would replace the right side by $2(1-\Phi(\alpha))$.

A complete development needs the law of a sum of independent Gaussians, the strong Markov property of a Gaussian random walk at a stopping time (or an equivalent first-passage decomposition), and, for the infinitely-often milestone, either the lower law of the iterated logarithm for Gaussian walks or the Hewitt–Savage/Kolmogorov zero–one law combined with the central limit theorem. These pieces are reusable well beyond this mission; contributions of any of them, as separate lemmas, are welcome.

Selected references

• H. Robbins, Some aspects of the sequential design of experiments, Bull. Amer. Math. Soc. 58 (1952), 527–535. https://doi.org/10.1090/S0002-9904-1952-09620-8
• W. Feller, Statistical aspects of ESP, J. Parapsychology 4 (1940), 271–298 (reference [11] of the paper).
• S. R. Howard, A. Ramdas, J. McAuliffe, J. Sekhon, Time-uniform, nonparametric, nonasymptotic confidence sequences, Ann. Statist. 49 (2021), 1055–1080. https://arxiv.org/abs/1810.08240

Motivation

A linear program $\max c\cdot x$ subject to $Ax\le b$, $x\ge 0$ assumes that the constraint matrix $A$ is known exactly. In practice the columns of $A$ — the activity vectors, describing how much of each resource one unit of activity $j$ consumes — are estimates. A. L. Soyster's 1973 technical note in Operations Research (doi:10.1287/opre.21.5.1154) asked what a decision $x$ should satisfy if every activity vector is known only to lie in a given convex set, and the decision has to be feasible for every possible realisation. He called this inexact linear programming, a term he attributes to K. O. Kortanek.

The note is the earliest formulation of what is now called robust linear optimization. Its answer — replace each uncertain column by its coordinatewise worst case — is the "Soyster model" that later work on robust optimization takes as its point of departure: Ben-Tal and Nemirovski (Math. Oper. Res. 1998; Math. Program. 2000) and Bertsimas and Sim (Oper. Res. 2004) both introduce their less conservative uncertainty sets as alternatives to it.

Setting

Fix integers $m,n\ge0$. Vectors in $\mathbb R^m$ are compared componentwise. For a set $S\subseteq\mathbb R^m$ and a scalar $t$, $tS=\{ta: a\in S\}$, and the sum of sets is Minkowski addition, $S+T=\{s+t: s\in S,\ t\in T\}$.

Let $K_1,\dots,K_n\subseteq\mathbb R^m$ be nonempty convex activity sets and $K\subseteq\mathbb R^m$ a nonempty convex resource set. Problem (I) is

$$\sup\ c\cdot x\quad\text{subject to}\quad x_1K_1+x_2K_2+\cdots+x_nK_n\subseteq K,\quad x_j\ge0,$$

and $X\subseteq\mathbb R^n$ denotes its set of feasible $x$. Problem (Ib) is the special case $K=K(b)=\{y\in\mathbb R^m: y\le b\}$ for a right-hand side $b\in\mathbb R^m$.

The support functional of a set $S$ is $\delta^*(y\mid S)=\sup_{a\in S}y\cdot a$, a value in $[-\infty,+\infty]$. With $e_i$ the $i$-th unit vector, the auxiliary matrix $\bar A$ is the $m\times n$ matrix with entries

$$\bar a_{ij}=\delta^*(e_i\mid K_j)=\sup_{a_j\in K_j}a_{ij},$$

defined when all of these are finite, and LP$(\bar A)$ is the linear program $\max c\cdot x$ subject to $\bar Ax\le b$, $x\ge0$. Finally $M$ is the set of $m\times n$ matrices $(a_1,\dots,a_n)$ whose $j$-th column lies in $K_j$.

In the application, the activity sets are Euclidean balls $K_j=\{a\in\mathbb R^m:\|a-a_j\|_2\le\rho_j\}$ around nominal columns $a_j$ of a matrix $A_0$, with radii $\rho_j\ge0$.

Formalization targets

Goal: the THEOREM (p. 1156)

Assume every $K_j$ is nonempty and convex and $\delta^*(e_i\mid K_j)<\infty$ for all $i,j$. Then

$$\{x : x\ \text{feasible for (Ib)}\}=\{x : \bar Ax\le b,\ x\ge 0\},$$

and for every objective $c$, the optimal solutions of (Ib) and of LP$(\bar A)$ coincide.

Milestones

1. Feasibility for (I) is equivalent to $x\ge0$ and $\sum_j x_ja_j\in K$ for every choice $a_j\in K_j$ (p. 1154).
2. LEMMA (p. 1155): $X$ is convex.
3. If $\delta^*(e_i\mid K_j)=\infty$ for some $i$, every feasible $x$ of (Ib) has $x_j=0$ (p. 1155).
4. Compact activity sets have $\delta^*(e_i\mid K_j)<\infty$ (p. 1156).
5. $x$ is feasible for (Ib) iff $Ax\le b$ for every $A\in M$ and $x\ge0$ (p. 1156).
6. Every $A\in M$ satisfies $A\le\bar A$ entrywise (proof of THEOREM).
7. Feasible for LP$(\bar A)$ implies feasible for (Ib) (proof of THEOREM).
8. Feasible for (Ib) implies $\sum_j x_j\sup_{a_j\in K_j}a_{ij}\le b_i$ for every $i$, i.e. feasible for LP$(\bar A)$ (proof of THEOREM).
9. For Euclidean balls, $\delta^*(e_i\mid K_j)=a_{ij}+\rho_j$, so $\bar a_j=a_j+\rho_je$ with $e$ the all-ones vector (p. 1157).
10. Inexact LP over balls: (Ib) has the same feasible and optimal solutions as $\max c\cdot x$ subject to $\sum_j x_j(a_j+\rho_je)\le b$, $x\ge0$ (p. 1157).

Significance

The THEOREM turns a semi-infinite constraint — one linear inequality for every matrix in $M$, of which there are typically uncountably many — into a single linear program of the original size, whose data are the support functionals of the activity sets. Any LP solver then solves the uncertain problem. The hypersphere corollary shows the cost of this guarantee concretely: every entry of column $j$ is inflated by the full radius $\rho_j$, which is why the model is called conservative and why later robust-optimization work introduced ellipsoidal and budgeted uncertainty sets as less conservative alternatives. The LEMMA classifies (I) as a convex program in general, for resource sets that are not half-space intersections.

The results are proved in the paper and are standard. To our knowledge they have no machine-checked proof in Lean or Mathlib. The mission produces a formal statement of the set-inclusive constraint as an actual Minkowski-sum inclusion, the support-functional reduction with its finiteness hypotheses made explicit, and the Euclidean-ball computation — a base that robust-counterpart results for other uncertainty sets can be compared against.

Difficulty

The individual arguments are short; the work is in the bookkeeping that the paper leaves implicit. The step from "for every $A\in M$" to $\bar A$ uses that the supremum of a sum of independent terms is the sum of suprema, which needs every $K_j$ nonempty and the scalars $x_j$ nonnegative; with an empty activity set the Minkowski sum is empty and every $x\ge0$ becomes feasible. The support functional is valued in the extended reals, and its conversion to a real matrix entry is exact only under the finiteness assumption, which the paper secures by deleting columns. The ball computation needs the Euclidean norm and its dual characterisation of the maximum of a coordinate over a ball.

Formalization scope

• Vectors are Fin m → ℝ and Fin n → ℝ, with indices $0,\dots,m-1$ in place of $1,\dots,m$; the order on vectors is componentwise.
• Feasibility of (I) is the Minkowski-sum inclusion (∑ j, x j • K j) ⊆ R (pointwise set operations) together with $x\ge0$. It is not defined as "for every choice $a_j\in K_j$", which would make milestones 1 and 5 trivial, and $\bar A$ is constructed from the $K_j$, not an arbitrary matrix dominating $M$, which would make the goal trivial.
• $\delta^*$ is valued in EReal. The entries of $\bar A$ are its real conversions, so every statement mentioning $\bar A$ assumes $K_j\neq\emptyset$ and $\delta^*(e_i\mid K_j)<\infty$, the paper's standing assumptions (pp. 1154–1156). Convexity of the $K_j$ is also kept as a hypothesis wherever the paper has it, although only the LEMMA uses convexity (of $K$).
• An optimal solution is a feasible point attaining the maximum of $c\cdot x$; the paper writes $\sup$ and does not discuss attainment. Because the goal identifies the feasible sets, the two problems also have equal suprema.
• Hyperspheres use the Euclidean norm (EuclideanSpace ℝ (Fin m)), not the sup norm of Fin m → ℝ, with radii $\rho_j\ge0$.
• The support functional restates the published FenchelRobust.Counterpart.supportFun with the same body.
• Not formalized: Magnanti's extension to $\ge$ and $=$ rows (p. 1156), and the remarks on (GLP) and stochastic programming. Contributions of proofs of any milestone, and of an EReal statement equating the optimal values, are welcome.

Selected references

• A. L. Soyster, Convex Programming with Set-Inclusive Constraints and Applications to Inexact Linear Programming, Operations Research 21(5), 1154–1157, 1973. https://doi.org/10.1287/opre.21.5.1154
• G. B. Dantzig, Linear Programming and Extensions, Princeton University Press, 1963. https://doi.org/10.1515/9781400884179
• A. Ben-Tal and A. Nemirovski, Robust Convex Optimization, Mathematics of Operations Research 23(4), 769–805, 1998. https://doi.org/10.1287/moor.23.4.769
• A. Ben-Tal and A. Nemirovski, Robust solutions of Linear Programming problems contaminated with uncertain data, Mathematical Programming 88, 411–424, 2000. https://doi.org/10.1007/PL00011380
• D. Bertsimas and M. Sim, The Price of Robustness, Operations Research 52(1), 35–53, 2004. https://doi.org/10.1287/opre.1030.0065

Motivation

An inventory controller must decide how much to order while demand changes with an observed external condition. A single demand rate misses that dependence: the same inventory position can justify different orders when the condition changes. Song and Zipkin's 1993 study asks whether a simple policy remains optimal when the condition follows a continuous-time Markov chain and orders arrive after a random lead time. The answer for linear ordering costs is a world-dependent basestock policy: each world state has one target inventory position, and an order raises the current position to that target when it lies below it.

The policy claim concerns an infinite horizon. It is stronger than showing that a particular collection of target levels performs well or that such a policy minimizes a one-step cost. Theorem 2 of Song and Zipkin identifies the targets through a limiting value function and establishes optimality for the full discounted problem. This mission formalizes that theorem and the finite-stage results the authors use to state its limit precisely.

Setting

The world state $i$ belongs to a nonempty countable set $I$. The world evolves according to a conservative continuous-time Markov generator $Q=(q_{ij})$, with exit rate $q_i=-q_{ii}$. When the world is in state $i$, customers demand individual units at rate $\lambda_i\ge0$. The exit rates and demand rates are bounded above. Inventory is fully backlogged: a negative inventory level records unmet demand. The controller observes the world state and the inventory position $x\in\mathbb Z$, which includes outstanding orders, and chooses an order-up-to position $y\ge x$.

An order has actual unit cost $\bar c\ge0$ and may have fixed cost $\bar K\ge0$. This mission takes the linear-cost case, so the discounted fixed cost is $K=0$. The lead time $L$ is a finite nonnegative random time, independent of the world and demand process. Its Laplace transform discounts the ordering costs to $c=\bar c\,E[e^{-\alpha L}]$, where $\alpha>0$ is the discount rate. Holding one unit costs $h>0$ per unit time; backlogging one unit costs $p>0$.

Write $D_L^i$ for the number of demands during the lead time conditional on initial world state $i$. The cost rate of an inventory level $z$ is $\widehat C(z)=-pz$ for $z<0$ and $hz$ otherwise. The lead-time cost and myopic cost are

$$C(i,y)=E[e^{-\alpha L}\widehat C(y-D_L^i)],\qquad G^+(i,y)=(1-\gamma)cy+\beta C(i,y),$$

where $\mu>0$ is a uniformization rate at least $\sup_iq_i+\sup_i\lambda_i$, $\beta=(\mu+\alpha)^{-1}$, and $\gamma=\beta\mu$. The paper's Assumption 1, $\alpha\bar c<p$, applies to the later results. It ensures the myopic cost has finite nonnegative minimizers. The smallest such minimizer in world state $i$ is $y^+(i)$, and $y^+_{\min}=\min_i y^+(i)$.

With zero fixed cost and zero terminal cost, the $n$-stage transformed cost $W_n(i,x)$ minimizes the auxiliary cost $G_n(i,y)$ over $y\ge x$. Each $G_n$ combines the myopic cost with the expected discounted continuation after a demand, a world-state jump, or a self-loop. Let $W_\infty$ and $G_\infty$ denote their pointwise limits. A basestock policy $\pi(y)$ orders to $\max\{x,y(i)\}$ in state $(i,x)$; it never cancels an outstanding order.

Formalization targets

The main target is the finite, smallest global minimizer $y^*(i)$ of $G_\infty(i,\cdot)$ for each world state, with the inequalities of Theorem 2(c):

$$0\le y^+_{\min}\le y^*(i)\le y^*_\infty(i)\le y^+(i), \qquad G_\infty(i,y^*_\infty(i))=\min_{z\in\mathbb Z}G_\infty(i,z).$$

Here $y^*_\infty(i)$ is the limit of the smallest finite-stage minimizers $y^*_n(i)$. Theorem 2(e) then asserts that $\pi(y^*)$ has minimum infinite-horizon expected discounted cost from every state among all feasible policies. The milestone list states Lemmas 1, 2 and 4, Corollaries 1 and 2, all parts of Theorem 1 as identified by the paper's internal references, and the limit and optimality-equation clauses of Theorem 2. Together they fix the finite-stage and limiting objects used by the goal.

Significance

The theorem reduces a decision at every integer inventory position to one integer target for each observed world state. It gives an exact policy structure for a model with a changing demand rate and random lead time, rather than an approximation derived from a constant-demand model. The limiting inequalities also locate an optimal target relative to the myopic target and the finite-stage targets, giving a mathematically specified range for policy computation. These claims are the linear-cost part of Song and Zipkin's analysis; the paper proves the result but supplies no Lean proof.

Formalization will leave reusable definitions for countable-state uniformization with a demand counter, integer convexity of inventory cost functions, and discounted costs of history-dependent policies. The mission's theorem statements compile as open goals. The remaining work is to verify the analytic properties of the lead-time demand law, the finite-stage inequalities, convergence, and the infinite-horizon policy comparison. The fixed-order-cost and monotone-world-state results of the paper are separate missions.

Difficulty

The world can have countably many states, so a continuation value includes a series over possible world jumps. The stage cost grows with inventory position, so a bounded-cost finite-state dynamic-programming theorem does not directly cover the model. The minimization is over an unbounded set of integers, and the minimizers themselves change with the stage number. Convexity of a one-stage cost alone does not establish that the limiting policy beats policies that use the entire observation history. These are the specific gaps the paper's bound, ordered-difference, and limit results address.

Formalization scope

World states are a nonempty countable Lean type, inventory positions and order-up-to levels are integers, and costs are real until policy evaluation. The lead-time law is a probability measure on finite nonnegative real times, independent of world and demand. The demand-count law is defined by exact Poisson uniformization at rate $\mu$, with demand, world-jump, and self-loop branches. The infinite-horizon policy cost uses extended nonnegative reals and a supremum of finite-horizon costs, so it can express an infinite expected cost without a default real value. Policies may depend on all past observed states; the goal compares its basestock policy against every feasible deterministic policy in this class. Randomized policies are omitted because they cannot improve expected nonnegative costs on this countable state space.

Assumption 1 is attached only to the results that use it. The linear-cost recursion has $K=0$ and $W_0=0$. Integer convexity means nondecreasing forward differences. Smallest minimizers and the minimum across world states are asserted to exist; neither is encoded by an integer infimum that returns a default on an empty or unbounded set. The goal requires an actual optimal policy cost comparison from every state, so solving the limiting optimality equation only within basestock policies cannot close it. Contributions to the lead-time mixture, integer convexity, boundedness of the real series and infima, and unrestricted policy comparison all fit this scope.

Selected references

• Jing-Sheng Song and Paul Zipkin, Inventory Control in a Fluctuating Demand Environment, Operations Research 41(2):351–370, 1993. DOI 10.1287/opre.41.2.351.

Why a nonsmooth implicit-function theorem

The classical implicit-function theorem solves an equation $F(x, y) = 0$ for $x$ as a function of a parameter $y$ near a known solution $(x_0, y_0)$, provided $F$ is (strongly) Fréchet differentiable in $x$ with an invertible partial derivative. Much of optimization does not meet that hypothesis. Optimality conditions of constrained problems, complementarity problems and variational inequalities are routinely rewritten as equations involving the projection onto a convex set, the componentwise $\min$, or the normal map of a polyhedron. These maps are Lipschitzian and piecewise smooth, but not differentiable. Sensitivity analysis asks whether the solution of such a system moves Lipschitz-continuously with the problem data, and the classical theorem cannot answer it.

Stephen M. Robinson, An Implicit-Function Theorem for a Class of Nonsmooth Functions, Mathematics of Operations Research 16(2), 1991, pp. 292–309, gives a theorem with the same shape as the classical one, in which differentiability is replaced by strong approximation by a function whose inverse is Lipschitzian. The paper's §4 applies it to parametric variational inequalities over polyhedral sets through the normal map.

Timeline. Robinson's Strongly regular generalized equations (Math. Oper. Res. 5, 1980) proved an implicit-function theorem for generalized equations under a linearization hypothesis called strong regularity. The 1991 paper reformulates that idea for single-valued nonsmooth equations: the approximating function $f$ need not be linear. Lemma 3.1 extends the Banach perturbation lemma for linear operators (Kantorovich–Akilov, Functional Analysis, Th. 4(2.V)) to Lipschitzian functions; after acceptance, A. Ioffe pointed the author to closely related results of Dmitruk, Milyutin and Osmolovskii (Lyusternik's theorem and the theory of extrema, Russian Math. Surveys, 1980, Theorems 1.2, 1.3), credited in the paper's footnote.

Setting

Let $X$, $Y$, $Z$ be real normed linear spaces, with $X$ complete. Fix $x_0 \in X$, $y_0 \in Y$, a neighborhood $\Xi$ of $x_0$ and a neighborhood $H$ of $y_0$. Let $F$ map $\Xi \times H$ to $Z$, with $F(x_0, y_0) = 0$, and let $f$ map $\Xi$ to $Z$, with $f(x_0) = 0$. $B(x, \rho)$ denotes the closed ball of radius $\rho$ about $x$.

Expansion modulus. For a map $f$ between metric spaces and a set $S$,

$$\delta(f, S) = \inf\left\{ \frac{\|f(x_1) - f(x_2)\|}{\|x_1 - x_2\|} : x_1 \ne x_2,\ x_1, x_2 \in S \right\}.$$

If $\delta(f,S) > 0$, then $f$ is one-to-one on $S$ and its inverse is Lipschitzian with modulus $\delta(f,S)^{-1}$. In Lean the mission works with lower bounds: ExpansionAtLeast f S d says $d\,\|x_1 - x_2\| \le \|f(x_1) - f(x_2)\|$ on $S$, i.e. $d \le \delta(f,S)$.

Strong approximation (Definition 2.4). $f$ strongly approximates $F$ in $x$ at $(x_0, y_0)$, written $f \approx_x F$ (Lean: StronglyApproxInX f F x₀ y₀), if for each $\varepsilon > 0$ there are neighborhoods $U$ of $x_0$ and $V$ of $y_0$ with

$$\big\|[F(x, y) - f(x)] - [F(x', y) - f(x')]\big\| \le \varepsilon \|x - x'\| \qquad (x, x' \in U,\ y \in V).$$

When $f$ is the partial derivative map $x \mapsto F_x(x_0,y_0)(x - x_0)$ this is strong partial Fréchet differentiability; in general $f$ may be piecewise linear or any map with a Lipschitzian inverse.

Formalization targets

Goal: Theorem 3.2 (p. 299)

Assume (a) $f \approx_x F$ at $(x_0, y_0)$; (b) for each $x \in \Xi$, $F(x, \cdot)$ is Lipschitzian on $H$ with modulus $\varphi$; (c) $f(\Xi)$ is a neighborhood of $0$ in $Z$; (d) $\delta(f, \Xi) =: d_0 > 0$. Then for each $\lambda > d_0^{-1}\varphi$ there are neighborhoods $U \subseteq \Xi$ of $x_0$, $V \subseteq H$ of $y_0$ and a function $x : V \to U$ with

$$x(y_0) = x_0, \qquad \|x(y_1) - x(y_2)\| \le \lambda \|y_1 - y_2\| \ (y_1, y_2 \in V), \qquad \{\xi \in U : F(\xi, y) = 0\} = \{x(y)\} \ (y \in V).$$

Every $\lambda$ strictly above $\varphi/d_0$ is claimed; $\lambda = \varphi/d_0$ is not.

Milestones

1. Lemma 3.1 (p. 298), the Lipschitz perturbation lemma: if $f$ maps $\Omega$ onto a ball $B(y_0, \alpha)$, $h$ is Lipschitzian with modulus $\eta < \delta := \delta(f, \Omega)$, $\Omega \supseteq B(x_0, \delta^{-1}\alpha)$ and $\theta := (1 - \eta\delta^{-1})\alpha - \|h(x_0)\| \ge 0$, then

$$(f + h)\big(B(x_0, \delta^{-1}\alpha)\big) \supseteq B(y_0, \theta), \qquad \delta(f + h, \Omega) \ge \delta - \eta > 0.$$

2. (3.1)–(3.2) in the proof of Theorem 3.2 (p. 300): for every $\varepsilon \in (0, d_0)$ there are $\alpha, \kappa > 0$ and a neighborhood $V \subseteq H$ of $y_0$ with $\Omega = B(x_0, d_0^{-1}\alpha) \subseteq \Xi$ such that for each $y \in V$

$$\delta(F(\cdot, y), \Omega) \ge d_0 - \varepsilon, \qquad F(\cdot, y)(\Omega) \supseteq B(0, \theta(y)) \supseteq B(0, \kappa),$$

where $\theta(y) = (1 - \varepsilon d_0^{-1})\alpha - \|F(x_0, y)\|$.

Significance

The result. Theorem 3.2 yields existence, local uniqueness and Lipschitz dependence of solutions of parametrized nonsmooth equations, with an explicit Lipschitz modulus arbitrarily close to $\varphi/d_0$. In the paper it underlies Theorem 3.3 and Corollary 3.4 (approximation and B-differentiation of the implicit function) and the sensitivity results of §4 for parametric variational inequalities over polyhedral convex sets. The same template, an equation approximated by a map with Lipschitzian inverse, is the basis of later strong-regularity and semismooth-Newton analyses in nonlinear programming and complementarity.

Formalizing it. The theorem is proved in the paper; it has not been machine-checked. The platform has the smooth implicit-function theorem (FamousTheorems.implicit_function_theorem, Rudin.ch09_implicit_function) and Mathlib has the contraction mapping principle, but there is no Lipschitz-inverse perturbation result and no notion of strong approximation. The mission produces both, together with the formal Theorem 3.2 that a follow-on mission (Theorem 3.3, Corollary 3.4, §4) would reference.

Difficulty

The obvious approach, differentiate and invert, is unavailable: $f$ need not have a derivative anywhere near $x_0$, so neither Mathlib's implicit-function theorem nor its inverse-function theorem applies. The difficulty is to obtain surjectivity of $F(\cdot, y)$ onto a ball uniformly in $y$ from information about $f$ alone. Injectivity transfers directly from $f$ through the small Lipschitz modulus of $F(\cdot, y) - f$; surjectivity does not, because $f$ carries no information about $F(\cdot, y)$ beyond the small Lipschitz modulus of the difference, and the domain ball, the image ball and the parameter neighborhood must be chosen once for all $y$. Completeness of $X$ is essential (the paper stresses this on p. 306) and is not available for $Y$ and $Z$.

Formalization scope

All statements live in namespace RobinsonNSIFT.Implicit. Committed conventions:

• Scalars are real; $X$ is a complete normed space ([CompleteSpace X]); $Y$, $Z$ are normed spaces without completeness. Lemma 3.1's domain is a complete metric space, not a normed one.
• $\delta(f, S)$ via lower bounds. Every statement takes a real $d$ with ExpansionAtLeast f S d in place of "$d = \delta(f,S)$", universally quantified. This is equivalent to the paper's statements and avoids a real infimum that would be $0$ on sets with fewer than two points.
• Total functions. $F$ is a curried total function F : X → Y → Z and $f : X \to Z$; hypotheses constrain them on $\Xi \times H$ only, and the conclusions keep the implicit function inside the domain: $U \subseteq \Xi$, $V \subseteq H$, $x(V) \subseteq U$. This makes explicit what the paper leaves implicit (its $F$ is only defined on $\Xi \times H$). Likewise $\Omega \subseteq \Xi$, used implicitly in the paper's proof, is a conclusion of milestone 2.
• Closed balls (Metric.closedBall), radii $\delta^{-1}\alpha$ written α / δ; neighborhoods are filter members ∈ 𝓝 _, not necessarily open; Lipschitz moduli are ℝ≥0 and Lipschitz conditions are LipschitzOnWith on the stated set.
• Lemma 3.1 keeps the paper's hypothesis that $\Omega$ is open, although Theorem 3.2's proof applies it to a closed ball.
• Milestone 2 states as an existence claim, for every $\varepsilon \in (0, d_0)$, the choices the paper makes at the start of its proof.

A formalization in which hypothesis (a) is the weak approximation of Definition 2.1 (only at $y = y_0$), in which $V$ may shrink to $\{y_0\}$, $\lambda$ is existential, or uniqueness is asserted outside $\Xi$, would be a different and trivial or false statement; the statements here rule these out.

Needed infrastructure: the contraction mapping principle on a closed subset of a complete space (Mathlib's ContractingWith), Lipschitz estimates on sets, and the two definitions of this mission. Lemma 3.1 is reusable for any Lipschitz-perturbation argument. Proofs of either milestone, or a direct proof of the goal, are welcome.

Selected references

• S. M. Robinson, An Implicit-Function Theorem for a Class of Nonsmooth Functions, Mathematics of Operations Research 16(2), 1991, 292–309. https://doi.org/10.1287/moor.16.2.292
• S. M. Robinson, Strongly Regular Generalized Equations, Mathematics of Operations Research 5(1), 1980, 43–62. https://doi.org/10.1287/moor.5.1.43
• A. V. Dmitruk, A. A. Milyutin, N. P. Osmolovskii, Lyusternik's theorem and the theory of extrema, Russian Mathematical Surveys 1980, No. 6, 11–51 (as cited in Robinson 1991, p. 298).
• L. V. Kantorovich, G. P. Akilov, Functional Analysis, cited in Robinson 1991 as [17].

Why edge-disjoint spanning trees

A connected network survives the failure of any single link exactly when it has no bridge, but a stronger and more useful property is to carry several edge-disjoint spanning trees: each tree can broadcast to every node on its own, so $k$ such trees give $k$ independent routing or broadcast structures, and the network stays connected after any $k-1$ link failures. The question of when a graph contains $k$ edge-disjoint spanning trees was answered in 1961, simultaneously and independently, by W. T. Tutte (On the problem of decomposing a graph into n connected factors) and C. St.J. A. Nash-Williams (Edge-disjoint spanning trees of finite graphs). The answer is a min-max condition over vertex partitions, now called the Tutte–Nash-Williams tree-packing theorem. It is a standard result in combinatorial optimization and the graphic case of Edmonds's matroid base-packing theorem (1965).

Timeline:

• 1961. Tutte proves the theorem in an equivalent form; Nash-Williams, unaware of Tutte's work, gives a different proof a few months later, the one formalized here.
• 1964. Nash-Williams proves the companion covering theorem: the edges can be covered by $k$ forests iff every vertex set $U$ spans at most $k(|U|-1)$ edges.
• 1965. Edmonds derives both results from matroid partition (Minimum partition of a matroid into independent subsets).

Setting

A graph $G$ here is a finite unoriented multigraph in which every edge joins two distinct vertices; two vertices may be joined by several edges. Write $V$ for its vertex set and $E$ for its edge set. A tree on a non-empty vertex set $W$ is an edge set $T$, all of whose edges have both ends in $W$, containing no cycle (two parallel edges count as a cycle), such that any two vertices of $W$ are joined by a path of $T$-edges. A spanning tree of $G$ is a tree on all of $V$ using edges of $G$. Spanning trees are edge-disjoint if no two share an edge.

A partition $P$ of $V$ is a set of non-empty, pairwise disjoint subsets of $V$ whose union is $V$; $|P|$ is the number of its members. The crossing edges $E_P(G)$ are the edges whose two ends lie in different members of $P$, counted with multiplicity. Throughout, $k$ is a fixed positive integer. For $X \subseteq V$, $E_X$ is the set of edges with both ends in $X$, $e_X = |E_X|$, and

$$\Delta_G(X) = k(|X|-1) - e_X .$$

Formalization targets

Goal: Theorem 1

$$G \text{ has } k \text{ edge-disjoint spanning trees} \iff |E_P(G)| \ge k(|P|-1) \text{ for every partition } P \text{ of } V. \tag{1}$$

Milestones, in the order of the proof

1. Lemma 1: a tree on $W$ has $|W|-1$ edges. Lemma 2: every connected graph has a spanning tree.
2. Necessity: $k$ edge-disjoint spanning trees imply (1) for every $P$.
3. (*) On couples $[G,g]$ ($g \ge 0$ on vertices, $\Delta_G \ge 0$ on non-empty sets): critical sets ($\Delta_G = 0$) whose intersection is non-empty are closed under $\cap$ and $\cup$. The same holds for crucial sets ($\Gamma = 0$, where $\Gamma(X) = \Delta_G(X) - s + g\,.\,\bar X$) when the couple is $s$-good.
4. Lemma 3: for $s \ge 1$, an $s$-good couple has an $(s-1)$-good supercouple with one added edge. Corollary 3A: an $s$-good couple has an $s$-supercouple, obtained by adding $s$ edges.
5. (†) and Lemma 4: a spanning tree of a graph produced by fusions at $\xi$ (replacing edges $\xi\eta$, $\xi\zeta$ by a new edge $\eta\zeta$) pulls back to a spanning tree of the original graph.
6. Lemma 5: a graph with $|E| = k(|V|-1)$ satisfies (1) iff $\Delta_G(X) \ge 0$ for every non-empty $X$.
7. Lemma 6: under the inductive hypothesis of the proof, a critical partition other than $\{V\}$ and the partition into singletons yields $k$ edge-disjoint spanning trees.

Significance

The theorem gives an exact, checkable certificate in both directions: a family of $k$ trees certifies the packing, and a single partition violating (1) certifies that no packing exists. Corollaries include that every $2k$-edge-connected graph has $k$ edge-disjoint spanning trees, and that the maximum number of edge-disjoint spanning trees (the strength-type parameter used in network reliability and in Nagamochi–Ibaraki style connectivity algorithms) is the minimum of $\lfloor |E_P(G)|/(|P|-1) \rfloor$ over partitions with $|P| \ge 2$. The partition condition is also the prototype of the rank condition in matroid base packing.

The result itself is classical and fully proved. What this mission adds is a machine-checked version in a multigraph setting. Mathlib has trees and spanning trees for simple graphs (SimpleGraph.IsTree, SimpleGraph.Connected.exists_isTree_le), but not edge-disjoint tree packing, and its simple graphs cannot express the parallel edges that the theorem and its proof need. Related items on the platform include the multigraph layer NagamochiIbaraki.EdgeConn.Multigraph (reused here), the Keller–Trotter spanning-forest count for simple graphs, and Edmonds's matroid partition theorem with Nash-Williams's covering corollary. Covering and packing are different statements, so none of these yields Theorem 1 directly. Formalizing Tutte's alternative proof, or deriving Theorem 1 from a formalized matroid union theorem, would also be welcome.

Difficulty

Necessity is a counting argument. The difficulty lies in sufficiency. The obvious induction deletes an edge or contracts a set of vertices, but deleting an edge can destroy (1), and contracting changes the vertex set, so neither reduction preserves the hypothesis on its own. The hardest case is a graph in which only the partition into singletons is critical. There a vertex of degree less than $2k$ has to be removed while (1) is preserved on the remaining graph, and the trees found there have to be converted back into trees of the original graph. Both steps need careful bookkeeping of edges incident with that vertex. A simple-graph development cannot carry the argument, because the edges that the reduction adds among the neighbours of the removed vertex may be parallel to existing ones.

Formalization scope

• Graphs. A vertex type V, an edge type E (both finite, in Type), and ends : E → Sym2 V, the published encoding of NagamochiIbaraki.EdgeConn. Loops are excluded by the hypothesis ∀ e, ¬ (ends e).IsDiag. Parallel edges are allowed, and simplicity is never assumed. A subgraph is a pair (W : Finset V, F : Finset E).
• Trees. "Tree" means non-empty vertex set, edges inside it, no cycle (IsForest: every edge is a bridge) and connected. $|T| = |W|-1$ is Lemma 1, not part of the definition. "$k$ edge-disjoint spanning trees" is a family Fin k → Finset E of pairwise disjoint spanning trees.
• Partitions are Mathlib Finpartition (Finset.univ : Finset V). (1) is required for every partition, including the one-part partition and the singletons. All counts involving subtraction ($\Delta_G$, (1), criticality, $\Gamma$) are in $\mathbb Z$.
• Explicit readings. $V$ is non-empty in Theorem 1, since the paper's graphs have a vertex and on $V = \emptyset$ condition (1) holds while no tree exists. $k \ge 1$ in every statement. The paper's "$X \subset V(G)$" includes $X = V(G)$ and is read as $\subseteq$. "Exactly $g(\xi)-h(\xi)$ new edges" is written $\deg_{\text{new}}(\xi) + h(\xi) = g(\xi)$, without natural-number subtraction. A supergraph with $s$ added edges has edge type E ⊕ Fin s, so the added edges always exist; none of them may be a loop. A fusion uses a given fresh edge ρ : E in an ambient edge type, and a sequence of fusions is a list, each valid on the graph produced by the later ones ($L = \Phi_1\cdots\Phi_n G$ applies $\Phi_n$ first). In (†) and Lemma 4, "is a tree" means "is a spanning tree of $G$", since the vertex set is all of $V$. Lemma 6 carries the paper's inductive hypothesis as an explicit hypothesis: Theorem 1 (admissible implies $k$ trees) for all loopless multigraphs with smaller $|V|+|E|$.
• Ruled out. Defining a spanning tree by an edge count alone, or by acyclicity alone, would make Lemma 1 or the goal trivial; the definitions require both acyclicity and connectivity on the stated vertex set. Taking added edges from a fixed ambient type would make Lemma 3 false. Dropping or globalizing Lemma 6's inductive hypothesis would turn it into the goal or a tautology.
• Infrastructure. Multigraph trees, the tree edge count and spanning-tree existence, contraction $G_P$ of a partition, and splitting-off at a vertex. All of these are reusable beyond this mission. Contributions of general multigraph lemmas are welcome.

Selected references

• C. St.J. A. Nash-Williams, Edge-disjoint spanning trees of finite graphs, J. London Math. Soc. 36 (1961), 445–450. https://doi.org/10.1112/jlms/s1-36.1.445
• W. T. Tutte, On the problem of decomposing a graph into n connected factors, J. London Math. Soc. 36 (1961), 221–230. https://doi.org/10.1112/jlms/s1-36.1.221
• C. St.J. A. Nash-Williams, Decomposition of finite graphs into forests, J. London Math. Soc. 39 (1964), 12. https://doi.org/10.1112/jlms/s1-39.1.12
• J. Edmonds, Minimum partition of a matroid into independent subsets, J. Res. Nat. Bur. Standards 69B (1965), 67–72. https://doi.org/10.6028/jres.069B.004
• C. Berge, Théorie des graphes et ses applications, Dunod, Paris, 1958.

Why private information changes bargaining

An arbitrator choosing an outcome for several people can ask them about their preferences, but the answer to that question may affect the outcome. A person who expects to gain from a false report may give one. Roger Myerson's 1979 paper puts this incentive problem inside a bargaining model: the arbitrator may randomize over collective choices, and an allocation is considered feasible only if some mechanism makes truthful reporting an equilibrium. The paper then applies a weighted Nash bargaining criterion to the resulting set of feasible interim payoffs. The mission formalizes the existence and uniqueness result for that criterion, along with the finite Bayesian model on which it depends.

The issue matters whenever an agreement is selected using information known privately to its participants. If the arbitrator evaluates a payoff vector that can arise only when somebody has a reason to lie, that vector cannot serve as a credible bargaining alternative under the model's own behavior assumption. Myerson's feasible set keeps the behavioral constraint visible when the group compares agreements. This mission addresses the paper's Theorems 1 and 3 and the claims between them that establish the relevant sets and their reference point.

The finite Bayesian choice problem

Let $I$ be a nonempty finite set of players. Player $i$ has a nonempty finite type set $A_i$, and the group has a nonempty finite set $C$ of possible choices. A type profile is $\alpha\in\prod_{i\in I}A_i$. The utility $U_i(c,\alpha)\in\mathbb R$ is player $i$'s payoff when choice $c$ occurs and $\alpha$ is the true profile. A nonnegative function $P$ on type profiles, summing to one, is the common prior. Write $R_i(a_i)$ for the probability that player $i$ has type $a_i$, and $P_i(\alpha\mid a_i)$ for the posterior probability of $\alpha$ conditional on that type. Every $R_i(a_i)$ is positive, so the conditional probabilities are defined.

A choice mechanism $\pi$ asks each player for a response and assigns a probability $\pi(c\mid s)$ to each choice $c$ at each response profile $s$. For the direct mechanisms used here, the response set of player $i$ is $A_i$: a response is a claimed type. The probabilities are nonnegative and sum to one for each response profile. If a player whose true type is $a_i$ instead reports $b_i$, while the others report truthfully, the player's conditional expected utility is $Z_i(\pi,b_i\mid a_i)$. The posterior $P_i(\alpha\mid a_i)$ weights true profiles; the mechanism sees the profile with only coordinate $i$ replaced by $b_i$; and utility is evaluated at the true profile $\alpha$.

The mechanism is Bayesian incentive-compatible when $Z_i(\pi,a_i\mid a_i)\ge Z_i(\pi,b_i\mid a_i)$ for every player and pair of types. Its interim payoff vector $V(\pi)$ has one coordinate $V_{i,a_i}(\pi)=Z_i(\pi,a_i\mid a_i)$ for every player-type pair. The set $F$ contains the vectors attained by all direct choice mechanisms; $F^*$ contains those attained by Bayesian incentive-compatible direct choice mechanisms. Theorem 1 says $F^*$ is nonempty, convex, compact, and contained in $F$. The nonemptiness claim includes the mechanism that selects each choice with probability $1/|C|$, independent of all reports.

Formalization targets

Fix a conflict outcome $c^*\in C$: the choice that occurs if bargaining fails. Its conflict payoff vector $t$ gives each player type the conditional expected utility from that fixed choice. A constant mechanism selects $c^*$ regardless of reports. It is incentive-compatible and generates $t$, so $t\in F^*$. The individually rational incentive-feasible set is

$$F^*_+=\{x\in F^*: x_{i,a_i}\ge t_{i,a_i}\text{ for all }i,a_i\}.$$

For $x\in F^*_+$, the generalized Nash product of equation (18) is

$$N(x)=\prod_{i\in I}\prod_{a_i\in A_i} (x_{i,a_i}-t_{i,a_i})^{R_i(a_i)}.$$

A bargaining solution is a vector in $F^*_+$ that maximizes $N$ over that set. Myerson's Theorem 3, the goal of this mission, says that if the constant conflict mechanism is not incentive-efficient—that is, an incentive-compatible mechanism strictly improves every player-type payoff over it—then exactly one such vector exists:

$$\neg\operatorname{Efficient}(\pi_{c^*}) \quad\Longrightarrow\quad \exists!x\in F^*_+\;\forall y\in F^*_+,\;N(y)\le N(x).$$

The milestones follow the paper's claims: the uniform mechanism is incentive-compatible; $F^*$ has the four properties in Theorem 1; the conflict vector belongs to $F^*$; every Nash-product maximizer strictly improves each conflict payoff when such improvement is feasible; and every implementing mechanism is incentive-efficient. The final claim concerns a mechanism that realizes the maximizing vector. It does not assert uniqueness of that mechanism.

What the result provides

Theorem 1 supplies a feasible set that respects truthful reporting. Theorem 3 selects a unique interim payoff vector from that set after a conflict outcome is specified. It thereby gives a well-defined allocation criterion for the paper's finite Bayesian collective choice problems. Myerson also observes that several mechanisms may implement the same solution. The allocation, rather than a unique mechanism, is the object selected by the theorem.

The result was proved in the 1979 paper. The work here is a machine-checked statement and, for solvers, a proof of that known result and its supporting claims in Lean. The mission's statements are open proof targets; the source paper's proof is not claimed to have been formalized already. A related platform item on Nash's two-player axiomatic characterization concerns a solution function on compact convex subsets of $\mathbb R^2$. It is a distinct result and supplies neither this paper's Bayesian model nor Theorem 3.

The mathematical obstacle

The set of all real-valued functions on choices and reports is much larger than the set of mechanisms: probabilities must be nonnegative and sum to one at every report profile. Bayesian incentive compatibility adds inequalities involving the true and reported type in different positions. Theorem 1 requires these constraints to give the compact, convex set of attainable interim payoffs, rather than merely a formal collection of payoff functions.

The Nash product also has a boundary: an individually rational vector may match the conflict payoff in one coordinate, making its product zero. Theorem 3's hypothesis has to rule out a zero maximum before uniqueness of an interior maximum can be concluded. The weights $R_i(a_i)$ matter in that uniqueness statement, and the result ranges over all player-type coordinates, not only one aggregate payoff per player. Restricting the maximization to an arbitrary small subset, fixing two players, or assuming a positive maximum would change the theorem.

Formalization scope

Lean represents players, each type set, and choices as finite nonempty types. Type profiles are dependent functions $\prod_i A_i$; interim vectors are real functions on the disjoint union $\sum_i A_i$, with the product topology. A mechanism is a real function $\pi:C\to(\prod_i A_i)\to\mathbb R$ subject to explicit nonnegativity and sum-to-one constraints. Both $F$ and $F^*$ quantify only over functions satisfying those constraints. Conditional beliefs use the common prior in equations (3)–(4), and positive marginal probabilities make every denominator meaningful without requiring positive probability for each full profile. The positivity of every $R_i(a_i)$ is an assumption the paper makes implicitly by dividing by it in (3); it is a field of the problem structure, not a hypothesis of the theorems. The subjective reading of $P_i$ and $R_i$ that the paper permits on p. 63, the response-plan equilibria of Section 3, and the numerical example of Section 6 are outside this mission.

Strict dominance means a strict gain for every player type. The constant mechanism, conflict vector, and individually rational set are defined from the problem data. The conflict vector is defined by equation (16), while its equality with the constant mechanism's payoff is a theorem item. The product uses real powers with the paper's marginal weights and is compared only on $F^*_+$, where each base is nonnegative. A solution is a maximizer property; it is not chosen in advance or supplied as a theorem hypothesis. These choices exclude vacuous encodings of incentive efficiency, unrestricted mechanisms, and a maximization domain that already contains only a nominated winner.

A complete proof development needs finite sums and products, continuous and convex maps on finite-dimensional real spaces, compactness of the constrained mechanism set, and facts about positive weighted real powers or logarithms on the strictly positive region. The model definitions can be reused for the paper's separate revelation-principle mission; this mission also welcomes proofs of the explicit claims about the uniform mechanism, the conflict mechanism, and product maximizers.

Selected references

• Roger B. Myerson, Incentive Compatibility and the Bargaining Problem, Econometrica 47(1), 61–73, 1979. DOI: 10.2307/1912346.
• John F. Nash, The Bargaining Problem, Econometrica 18(2), 155–162, 1950. DOI: 10.2307/1907266.
• John C. Harsanyi and Reinhard Selten, A Generalized Nash Solution for Two-Person Bargaining Games with Incomplete Information, Management Science 18(5), P80–P106, 1972. DOI: 10.1287/mnsc.18.5.80.