Optimization

Motivation

Many problems in mechanics and optimal control are posed as the minimization of a convex functional of the form $f(Av)-\langle b,v\rangle$, where $A$ is a differential operator and $f$ is non-smooth: an obstacle, a friction term, a plasticity threshold. Splitting the variable, $y=Av$, separates the linear operator from the non-smooth function, and a Lagrange multiplier for the constraint $Av-y=0$ turns the problem into a sequence of two simpler ones: a linear system in $v$ and a pointwise nonlinear problem in $y$. The scheme that alternates between the two and then updates the multiplier is now called the alternating direction method of multipliers (ADMM). It is one of the standard algorithms of large-scale convex optimization, statistics and imaging (Boyd, Parikh, Chu, Peleato and Eckstein, 2011).

Gabay and Mercier (IRIA report RR-126, 1975; Comput. Math. Appl., 1976) gave a convergence proof of this method in Hilbert space, for a stepsize $\rho$ anywhere in $(0,2r)$, where $r$ is the penalty parameter of the augmented Lagrangian.

Timeline.

• 1969: Hestenes and Powell introduce the augmented Lagrangian (method of multipliers).
• 1975: Glowinski and Marrocco propose the alternating scheme for nonlinear Dirichlet problems.
• 1975–76: Gabay and Mercier prove strong convergence of the primal iterates for $0<\rho<2r$ under strong monotonicity of $f_1'$ (this mission).
• 1983: Gabay identifies ADMM with Douglas–Rachford splitting applied to the dual.
• 1992: Eckstein and Bertsekas extend convergence to maximal monotone operators, without strong monotonicity, for $\rho=r$.

Setting

$V$ and $Y$ are real Hilbert spaces; $(\cdot,\cdot)$ and $|\cdot|$ are the inner product and norm of $Y$, $\|\cdot\|$ the norm of $V$. $A:V\to Y$ is a continuous linear operator and $b$ is a continuous linear functional on $V$, with value $\langle b,v\rangle$ at $v$. The dual of $Y$ is identified with $Y$. The function $f:Y\to(-\infty,+\infty]$ is a sum $f=f_1+f_2$ where

1. $f_1:Y\to\mathbb R$ is convex and continuously differentiable, and its gradient is strongly monotone: $(f_1'(y)-f_1'(z),y-z)\ge\gamma|y-z|^2$ for some $\gamma>0$ (2.3);
2. $f_2$ is proper (never $-\infty$, somewhere finite), convex and lower semicontinuous;
3. $|Av|^2\ge\alpha^2\|v\|^2$ for some $\alpha>0$ (2.5);
4. some $Av_0$ lies in the interior of $\operatorname{dom}f_2=\{y:f_2(y)<+\infty\}$ (qualification).

The problem is

$$(\mathcal P)\qquad \inf_{v\in V}\ f(Av)-\langle b,v\rangle ,$$

and a solution $v^*$ is a point where this value is finite and minimal. The Lagrangian and augmented Lagrangian are, for $\lambda\in Y$ and $r>0$,

$$\mathcal L(v,y;\lambda)=f(y)+(\lambda,Av-y)-\langle b,v\rangle,\qquad \mathcal L_r=\mathcal L+\frac r2|Av-y|^2 .$$

The modified dual algorithm (3.4) starts from any $(y^0,\lambda^0)\in Y\times Y$ and, for $n\ge0$,

1. finds $v^{n+1}$ with $r(Av^{n+1},Aw)=(ry^n-\lambda^n,Aw)+\langle b,w\rangle$ for all $w\in V$ (minimization of $\mathcal L_r$ in $v$);
2. finds $y^{n+1}$ with $\lambda^n+rAv^{n+1}-ry^{n+1}-f_1'(y^{n+1})\in\partial f_2(y^{n+1})$ (minimization of $\mathcal L_r$ in $y$);
3. sets $\lambda^{n+1}=\lambda^n+\rho(Av^{n+1}-y^{n+1})$.

$P$ denotes the orthogonal projection of $Y$ onto the range $R(A)$, which is closed by (2.5).

Formalization targets

Goal: Theorem 3.1

For $r>0$ and every stepsize with

$$0<\rho<2r,$$

every run of the algorithm satisfies

$$\|v^n-v^*\|\to0,\qquad |y^n-Av^*|\to0,\qquad \sup_n|\lambda^n|<\infty,$$

where $v^*$ is the unique solution of $(\mathcal P)$. The multipliers need not converge.

Milestones

1. Proposition 2.1: $(\mathcal P)$ has a unique solution.
2. Theorem 2.1: a saddle point $(v^*,y^*;\lambda^*)$ of $\mathcal L$ consists of the solution $v^*$, $y^*=Av^*$ and $\lambda^*\in\partial f(Av^*)$ with $A'\lambda^*=b$; and a saddle point exists.
3. Theorem 2.2: for $r>0$, $\mathcal L_r$ and $\mathcal L$ have the same saddle points.
4. (3.8)–(3.10): a saddle point is a fixed point of Steps 1–2.
5. (3.11)–(3.12): $A(v^{n+1}-v^*)=P(y^n-y^*)-\frac1rP(\lambda^n-\lambda^*)$.
6. (3.19)–(3.20): the energy estimate

$$\gamma|y^{n+1}-y^*|^2+\Bigl(r-\frac\rho2\Bigr)|(I-P)(y^{n+1}-y^*)|^2+\frac r2|P(y^{n+1}-y^*)|^2+\frac1{2\rho}|(I-P)(\lambda^{n+1}-\lambda^*)|^2\le\frac r2|P(y^n-y^*)|^2+\frac1{2\rho}|(I-P)(\lambda^n-\lambda^*)|^2$$

and its sum over $n=0,\dots,N$. 7. $y^n\to y^*$ for $0<\rho\le2r$. 8. (3.22)–(3.23): a contraction-plus-summable-forcing recursion for $|P(\lambda^n-\lambda^*)|^2$, and the scalar lemma that such recursions tend to $0$. 9. $P(\lambda^n-\lambda^*)\to0$ and $v^n\to v^*$ for $0<\rho<2r$.

Significance

The theorem says that ADMM converges without any step-size tuning beyond $\rho<2r$, and that the primal iterates converge in norm in infinite dimension, which is what makes the method usable for finite element discretizations of variational problems (the companion mission on internal approximations treats the discretization). It covers obstacle problems, Bingham fluids and elasto-plastic torsion, where $f_2$ is an indicator or a non-differentiable norm.

The result is proved in the 1975 report. To our knowledge it has no machine-checked proof. Formalizing it adds a library-level convergence theorem for ADMM in Hilbert space with $\mathrm{EReal}$-valued convex functions, a saddle-point existence theorem for linearly constrained convex problems, and the energy estimate (3.19) as a reusable lemma. The formalization also fixes two defects of the printed text (see Formalization scope): a sign in Step 1 and a qualification hypothesis that is too weak.

Difficulty

The energy estimate (3.19) only controls the multiplier through its component in $R(A)^\perp$, and only the $y$-error through $\gamma>0$. The natural first idea, a Lyapunov function in $|\lambda^n-\lambda^*|^2$ alone that decreases at each step, does not work for $\rho\ne r$: the component $P(\lambda^n-\lambda^*)$ obeys a separate recursion whose contraction factor $|1-\rho/r|$ is below one only for $0<\rho<2r$, and whose forcing term must be shown summable from the $y$-estimate. The existence of a multiplier, i.e. of a saddle point, is a separate difficulty: it needs the subdifferential chain rule $\partial(f\circ A)=A'\partial f(A\,\cdot)$ in infinite dimension, under a constraint qualification.

Formalization scope

Lean conventions:

• $V$, $Y$ are InnerProductSpace ℝ with CompleteSpace; multipliers are elements of $Y$; $b$ is a StrongDual ℝ V.
• $f_1:Y\to\mathbb R$ (a Gateaux-differentiable function is finite), with a gradient f₁' at every point (HasGradientAt) that is continuous; "weakly continuous on finite-dimensional subspaces" is then automatic.
• $f_2:Y\to$ EReal, with IsProperFn, IsConvexFn, IsSubgradient from the published InertialFB.IFB.ConvexAnalysis and Mathlib's LowerSemicontinuous. No subtraction in EReal occurs: the variational inequalities (3.6), (3.9) are stated as subgradient inclusions, and the Lagrangians as a real part plus $f_2(y)$.
• A solution of $(\mathcal P)$ has finite value. A run is any triple of sequences indexed by $\mathbb N$ satisfying Steps 1–3 for every $n$; the start is arbitrary, and the well-posedness of the steps is not assumed or used.
• $P$ is the orthogonal projection onto the closure of $R(A)$, equal to $R(A)$ under (2.5).
• Strong convergence is convergence in norm; "bounded" is Bornology.IsBounded (Set.range λ).

Corrections to the printed text, each explained in the item's statement:

• Step 1 (3.5) and (3.8) carry $+\langle b,v\rangle$. The paper prints $-\langle b,v\rangle$ there and in Remark 1 of p. 15, which is inconsistent with $\mathcal L$ and $(\mathcal P)$: with the printed sign the iteration solves the problem with $-b$.
• The qualification (2.4), "$\operatorname{int}\operatorname{dom}f_2\ne\emptyset$", is strengthened to $\operatorname{int}\operatorname{dom}f_2\cap R(A)\ne\emptyset$. With (2.4) alone, Theorem 2.1's saddle point need not exist and the multipliers of Theorem 3.1 need not be bounded: $V=\mathbb R$, $Y=\mathbb R^2$, $Av=(v,0)$, $f_1=|\cdot|^2/2$, $f_2$ the indicator of the disc of centre $(0,1)$ and radius $1$, $\langle b,v\rangle=v$.
• Proposition 2.1 assumes that $f_2\circ A$ is somewhere finite, which its proof requires.

Ruled out: the solution $v^*$ is a hypothesis of the goal, so the hypotheses must not be contradictory. They are met by $V=Y=\mathbb R$, $A=\mathrm{id}$, $f_1(y)=y^2/2$, $f_2=0$, $b=0$, and a proper $f_2$ excludes the degenerate reading in which every point "solves" $(\mathcal P)$ with value $+\infty$.

A complete development needs: existence of minimizers of coercive convex l.s.c. functions on a Hilbert space; the subdifferential sum and chain rules under a continuity qualification; orthogonal projections onto closed ranges; and elementary facts about summable sequences. The saddle-point theory (Theorems 2.1–2.2) and the scalar lemma (3.23) are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs of the goal by a different route.

Selected references

• D. Gabay and B. Mercier, A dual algorithm for the solution of non linear variational problems via finite element approximation, IRIA Rapport de Recherche 126, 1975. https://hal.science/hal-04716124v1 ; journal version: Computers & Mathematics with Applications 2 (1976) 17–40, https://doi.org/10.1016/0898-1221(76)90003-1
• R. Glowinski and A. Marrocco, Sur l'approximation, par éléments finis d'ordre un, et la résolution, par pénalisation-dualité, d'une classe de problèmes de Dirichlet non linéaires, RAIRO Analyse Numérique 9 (1975) 41–76. https://doi.org/10.1051/m2an/197509R200411
• M. R. Hestenes, Multiplier and gradient methods, J. Optim. Theory Appl. 4 (1969) 303–320. https://doi.org/10.1007/BF00927673
• I. Ekeland and R. Temam, Analyse convexe et problèmes variationnels, Dunod, 1974 (the paper's [E]).
• J. Eckstein and D. P. Bertsekas, On the Douglas–Rachford splitting method and the proximal point algorithm for maximal monotone operators, Math. Programming 55 (1992) 293–318. https://doi.org/10.1007/BF01581204
• S. Boyd, N. Parikh, E. Chu, B. Peleato and J. Eckstein, Distributed optimization and statistical learning via the alternating direction method of multipliers, Found. Trends Mach. Learn. 3 (2011) 1–122. https://doi.org/10.1561/2200000016

Motivation

An integer program is a linear program whose variables must take integer values. Its linear relaxation can be solved efficiently, while the integer program itself is NP-hard in general, so a recurring question in integer programming is how much the optimal solution of the relaxation says about the integer optimum. Simple rounding of the fractional optimum does not answer it: examples show that the integer optimum need not lie within distance one of the LP optimum, even when the right-hand side is large.

R. E. Gomory's 1965 note in the Proceedings of the National Academy of Sciences (doi:10.1073/pnas.53.2.260) showed that, for right-hand sides lying deep inside the cone of an optimal LP basis, the integer program is solved exactly by the LP solution plus a correction computed in a finite abelian group. The resulting group relaxation (the "corner polyhedron" of Gomory's later work, Gomory 1969) underlies a large body of work on cutting planes, the master group problem, Gomory–Johnson functions and asymptotic integer programming.

Timeline. Gomory's fractional cutting-plane algorithm (Gomory 1958) introduced the "fractional rows" of the simplex tableau; the 1965 note identifies the group they generate with $M(I)/M(B)$ and proves the asymptotic theorem formalized here. Gomory 1969 develops the corner polyhedron; Gomory and Johnson (1972) study the continuous valid functions of the corner polyhedron.

Setting

Let $A$ be an integer $m\times(m+n)$ matrix of the form $(A',I)$, let $b\in\mathbb Z^m$ and $c\in\mathbb R^{m+n}$. Problem P1 is

$$\max\ z_1=cx\quad\text{s.t.}\quad Ax=b,\ x\ge0,$$

and P2 is P1 with $x$ integer. A basis is a nonsingular $m\times m$ submatrix $B$ of $A$; after rearranging, $A=(B,N)$ with $B=(\alpha_1,\dots,\alpha_m)$ and $N=(\alpha_{m+1},\dots,\alpha_{m+n})$, and $c=(c_B,c_N)$. The relative cost of a nonbasic column is $c^*_i=c_i-c_BB^{-1}\alpha_i$, and $B$ is an optimal basis when all $c^*_i\le0$. The cone of the basis is $K^B=\{\beta\in\mathbb R^m: B^{-1}\beta\ge0\}$; removing from it all points within Euclidean distance $d$ of its boundary gives the reduced cone $K^B(d)$.

Let $M(I)=\mathbb Z^m$ and $M(B)=\mathfrak L_B$ the lattice of integer combinations of $\alpha_1,\dots,\alpha_m$. The factor module $M(I)/M(B)$ is a finite abelian group with $D=|\det B|$ elements; write $\bar\alpha_i$, $\bar b$ for the classes of $\alpha_i$, $b$. The group problem (4) is

$$\max\ \sum_{i=1}^n c^*_{i+m}y_i\quad\text{s.t.}\quad\sum_{i=1}^n\bar\alpha_{i+m}y_i=\bar b,\quad y_i\ge0\text{ integer},$$

with optimal value $\varphi^B(b)$. Finally $l=\max_{i>m}\|\alpha_i\|$.

Formalization targets

Goal: THEOREM 1 (p. 261)

If $b\in K^B(l(D-1))$, then P1, P2 and (4) attain their optima, the value $z_2(b)$ of P2 is

$$z_2(b)=z_1(b)+\varphi^B(b),$$

an optimal solution of P2 is

$$x(b)=\big(B^{-1}(b-Ny^B(b)),\ y^B(b)\big)$$

for an optimal solution $y^B(b)$ of (4) with $\sum_iy^B_i(b)\le D-1$, and $\varphi^B$, $y^B$ are $m$-periodic: $\varphi^B(b+\alpha_i)=\varphi^B(b)$.

Milestones

In the order of the paper's proof: $|M(I)/M(B)|=D$ (p. 262); periodicity of (4) (p. 263); the cost identity (5)–(6); "$c_BB^{-1}b$ is $z_1(b)$", the simplex optimality criterion (a published, proved theorem); the projection of a solution of P2 to a solution of (4); the bound (7), $z_2(b)\le z_1(b)+\varphi(b)$; the extension of a solution of (4) to an integer solution; the LEMMA (an optimal solution of (4) with $\sum y_i\le D-1$); and the bound $\|Ny\|\le(D-1)l$ that places $b-Ny$ in $K^B$.

Companions

THEOREM 2: the optimal $x(b)$ satisfies $\sum_{i>m}x_i=\sum_iy_i\le D-1$. THEOREM 4 (with the bound corrected, see below): if an optimal $y$ of (4) has $\prod_i(y_i+1)>D$, the optimum of (4) is not unique.

Significance

THEOREM 1 reduces integer programming, for right-hand sides far from the boundary of an optimal cone, to a shortest-path-type problem over a group of order $D$: the integer optimum is determined by the LP optimum and a periodic correction, and it can be computed in time polynomial in $n$ and $D$ (THEOREM 3, not formalized here). It explains why rounding fails while a structured correction succeeds, and it is the starting point of the corner-polyhedron and cutting-plane theory built on the group relaxation. THEOREM 2 bounds how far the integer optimum lies from a lattice point of $\mathfrak L_B$, an early proximity result.

The results are classical and proved in the paper; none of them has a machine-checked proof that this mission is aware of. The mission produces a Lean statement and proof of the asymptotic theorem, together with reusable statements about the group $\mathbb Z^m/B\mathbb Z^m$ and the zero-sum shortening argument of the LEMMA.

Difficulty

The decomposition $z_2\le z_1+\varphi$ is a direct computation. The difficulty is the converse: an optimal solution $y$ of the group problem extends to an integer point $x_B=B^{-1}(b-Ny)$, but nothing in (4) forces $x_B\ge0$. Optimality of $y$ alone does not bound $y$: an optimal solution may carry zero-cost cycles of arbitrary length, and then $b-Ny$ can leave the cone $K^B$. The theorem therefore depends on choosing the right optimal solution of (4), one whose total size is bounded by the group order, and on relating that combinatorial bound to the Euclidean geometry of the cone.

Formalization scope

• The basis is fixed: $B$ is an integer $m\times m$ matrix and $N$ an integer $m\times n$ matrix; column $j$ of $N$ ($0$-based) is the paper's $\alpha_{m+1+j}$. The costs $c_B$, $c_N$ are real.
• The standing assumptions of pp. 260–262 are hypotheses of the goal: $\det B\neq0$; every unit vector of $\mathbb Z^m$ is a column of $B$ or of $N$ (the paper's $A=(A',I)$, without which P2 can be infeasible); all relative costs $c^*_i\le0$ ($B$ is optimal, without which (4) is unbounded).
• P2's variables are natural numbers (integer and nonnegative). The group problem is written as "$b-Ny\in B\mathbb Z^m$", which is equivalent to $\sum\bar\alpha_{i+m}y_i=\bar b$.
• Optimal values are greatest elements of the sets of objective values, never suprema; the goal asserts that they are attained.
• The norm in $l$ and in $K^B(d)$ is Euclidean. $K^B(d)$ is the set of points whose closed ball of radius $d$ lies in $K^B$. $l=0$ when $n=0$.
• In part (3) of the goal, $y^B(b)$ ranges over optimal solutions of (4) with $\sum_iy_i\le D-1$, the solutions the paper's LEMMA and dynamic program produce.
• THEOREM 4 is stated with the hypothesis $\prod(y_i+1)>D$: the printed $>D-1$ is false ($m=n=1$, $B=(2)$, $N=(1)$, $c=(2,0)$, $b=1$ has the unique optimum $y=1$ with $\prod(y_i+1)=2$).
• A trivializing formalization is ruled out: the goal assumes none of the LEMMA, the inequality (7), integrality of $B^{-1}(b-Ny)$ or the norm bound, and it states the existence of the optima instead of assuming them.
• Not in scope: the operation counts of THEOREM 3 and the recursion (8), which need a machine model the paper does not define.

Needed infrastructure: the cardinality of $\mathbb Z^m/B\mathbb Z^m$ (available in Mathlib through determinants of basis changes), a zero-sum/pigeonhole argument in a finite abelian group, the simplex optimality criterion (published), and elementary Euclidean estimates. The group-theoretic lemmas are reusable for other group-relaxation and proximity missions. Proofs of the milestones, alternative arguments and the extension to the open-ball reading of $K^B(d)$ are welcome.

Selected references

• R. E. Gomory, On the relation between integer and noninteger solutions to linear programs, Proc. Natl. Acad. Sci. USA 53(2):260–265, 1965. https://doi.org/10.1073/pnas.53.2.260
• R. E. Gomory, Outline of an algorithm for integer solutions to linear programs, Bull. Amer. Math. Soc. 64:275–278, 1958. https://doi.org/10.1090/S0002-9904-1958-10224-4
• R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra Appl. 2:451–558, 1969. https://doi.org/10.1016/0024-3795(69)90017-2
• R. E. Gomory and E. L. Johnson, Some continuous functions related to corner polyhedra, Math. Programming 3:23–85, 1972.
• J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Springer, 2007 (simplex optimality criterion). https://doi.org/10.1007/978-3-540-30717-4

Motivation

Two parties who can cooperate for mutual benefit must still agree on how to share the benefit. In The Bargaining Problem (Econometrica, 1950) John Nash asked which agreement two rational bargainers of equal skill should reach. His answer is not a model of haggling: it is a list of conditions any reasonable rule should satisfy, together with a proof that exactly one point of the set of feasible agreements is compatible with them. That point maximizes the product of the two parties' utility gains. Known as the Nash bargaining solution, it is the reference point of cooperative bargaining theory. Economics, operations research and networking all use it: in supply contracts, in wage bargaining, and in fair bandwidth allocation, where maximizing a product of gains becomes maximizing a sum of logarithms (proportional fairness).

Timeline:

• 1944. von Neumann and Morgenstern axiomatize expected utility. A utility is determined up to a positive affine transformation $au+b$. Nash quotes this on p. 157.
• 1950. Nash introduces the two-person bargaining problem and the axioms of Pareto efficiency, independence of irrelevant alternatives and symmetry, the solution being invariant under the choice of utility scales. He proves that they force the maximizer of the product $u_1u_2$ (doi:10.2307/1907266).
• 1953. Nash's Two-Person Cooperative Games adds the threat game that fixes the disagreement point.
• 1975. Kalai and Smorodinsky replace independence of irrelevant alternatives by monotonicity and obtain a different solution.
• 1986. Binmore, Rubinstein and Wolinsky show that the Nash solution is the limit of equilibria of alternating-offers bargaining as the time between offers vanishes.

Setting

A bargaining problem is a pair $\langle S,d\rangle$. Here $S\subseteq\mathbb R^2$ is the set of utility pairs $u=(u_1,u_2)$ the two players can reach by agreement, including lotteries over agreements. $d\in S$ is the disagreement point, the utilities of no cooperation. As in the platform goal, $S$ is compact and convex, and some $s\in S$ has $s_1>d_1$ and $s_2>d_2$ (both individuals could gain). Write $\mathcal B$ for the set of such pairs.

A bargaining solution is a map $g$ from $\mathcal B$ to $\mathbb R^2$. Nash requires:

• Selection. $g(S,d)\in S$.
• PAR (Nash's assumption 6). If $s,t\in S$ and $t$ is strictly better than $s$ for both players, then $g(S,d)\neq s$.
• IIA (assumption 7). If $S\subseteq T$ and $g(T,d)\in S$, then $g(S,d)=g(T,d)$.
• SYM (assumption 8). If $d_1=d_2$ and $S$ is symmetric in the line $u_1=u_2$, then $g(S,d)$ lies on that line.
• INV. For $L(s)=(\alpha_1s_1+\beta_1,\ \alpha_2s_2+\beta_2)$ with $\alpha_1,\alpha_2>0$, $g(L(S),L(d))=L(g(S,d))$.

The paper has no separate INV axiom. It normalizes the disagreement utility to $0$ and notes that each utility is then determined only up to a positive multiple (p. 158), so the solution must not depend on that choice.

Formalization targets

Goal

The goal is the platform theorem NashBargaining.nash_bargaining_solution_unique, posed by Nickrobbins95 and currently Open. This mission references it and does not restate it. It asserts that there is a solution $f$ such that a solution $g$ satisfies selection, INV, SYM, IIA and PAR if and only if $g=f$, and that for every $\langle S,d\rangle\in\mathcal B$

$$f(S,d)\ge d,\qquad (s_1-d_1)(s_2-d_2)<(f_1-d_1)(f_2-d_2)\ \text{ for all } s\in S,\ s\ge d,\ s\neq f(S,d).$$

Nash's paper proves the necessity half: a solution satisfying the conditions must select the maximizer of the Nash product. The sufficiency half, that the maximizer map satisfies the five conditions, is not argued in the paper. It must be supplied by whoever closes the goal.

Milestones

1. On a compact convex $S\ni(0,0)$ that contains a point where both players gain, $u_1u_2$ has exactly one strict maximizer $p$ in the closed first quadrant, and $p_1,p_2>0$.
2. Multiplying the utilities by positive constants maps the maximizer to the maximizer, so $p$ may be moved to $(1,1)$.
3. If $S$ is convex and $(1,1)$ maximizes $u_1u_2$, then $u_1+u_2\le2$ on all of $S$.
4. A compact $S$ under that line lies in a square $Q_h=\{2-2h\le u_1+u_2\le2,\ |u_1-u_2|\le h\}$.
5. $(1,1)$ is the only point of $Q_h$ on the diagonal that no point of $Q_h$ strictly dominates.
6. Necessity. Under the five conditions, $g(S,d)$ is the strict maximizer of $(s_1-d_1)(s_2-d_2)$ over $S\cap\{s\ge d\}$.

Two further items formalize the paper's examples: the Bill–Jack barter, whose solution is the vertex $(12,5)$ reached by exactly one exchange, and trade with money, where the solution gives equal money profits.

Significance

The Nash product characterization is used, mostly without proof, wherever a "fair" split of a cooperative surplus is needed. Examples are generalized Nash bargaining in supply-chain contracting and labour economics, the proportional-fairness criterion in network rate control, and the Nash-in-Nash models of bilateral negotiations. Many papers that build on it apply it to a specific feasible set. They therefore rely on the necessity direction, which is the step that makes the maximizer the unique answer rather than one answer among several.

The result has been proved since 1950, while the referenced Prove2Me goal remains Open. This mission supplies the milestones of Nash's own argument in the encoding of that goal, so that the necessity direction can be assembled from them. Sufficiency remains as separate work. The two examples are small, concrete checks of the solution concept.

Difficulty

Each step is elementary. The difficulty is in keeping the bookkeeping honest across the normalizations. The axioms are stated on the class $\mathcal B$, and a solution is a function on a subtype. Every application of INV, SYM or IIA therefore needs a membership proof for a transformed set: the image of $S$ under an affine map, or the enclosing square. It also needs the disagreement point to be carried along. The tempting short cut is to argue "without loss of generality $d=0$ and $p=(1,1)$". That is exactly what INV licenses, but only after compactness, convexity, the point where both gain, and the location of $d$ inside the square have been re-established for each transformed problem. Uniqueness of the maximizer also needs care at the boundary of the quadrant, where the product vanishes.

Formalization scope

Utility pairs are ℝ × ℝ, with u.1 player 1's utility and u.2 player 2's. Milestones 1–5 work at $d=(0,0)$, the paper's normalization. Milestone 6 has a general $d$ and the goal's encoding. Milestones 1–5 make the following readings explicit:

• "First quadrant" is the closed quadrant $u_1\ge0,\ u_2\ge0$.
• "The point where $u_1u_2$ is maximized" is the strict maximizer over $S$ in that quadrant, in the goal's form. Milestone 1 also states $p_1,p_2>0$, which follows from the point where both gain (p. 158).
• Milestone 3's hypothesis is the weak maximum $s_1s_2\le1$. Its conclusion covers every point of $S$, not only first-quadrant points.
• The square is the explicit set $Q_h$. Its compactness, convexity and literal symmetry $(a,b)\in Q_h\iff(b,a)\in Q_h$ are part of milestone 4's conclusion.
• "Satisfying assumptions (6) and (8)" in the square means lying on $u_1=u_2$ and being strictly dominated by no point of the square.

Milestone 6's five hypotheses are copied verbatim from the goal, and its conclusion is the goal's last conjunct for the given $g$. It does not restate the goal: it has no existence claim and no "if and only if".

Trivializing formalizations are ruled out. The point where both gain is a hypothesis wherever uniqueness is claimed; without it a segment on an axis has many maximizers of $u_1u_2=0$. The square is a concrete set, not "some symmetric compact convex set", and the solution's properties are quantified over the goal's class $\mathcal B$, which is nonempty.

The examples need finite sums, convex hulls of finite sets, and extreme points, all in Mathlib. Contributions are welcome on each milestone and on the sufficiency half of the goal.

Related platform work treats other bargaining models. These are Rubinstein's alternating-offers game (RubinsteinBargaining.PEP) and the Chatterjee–Samuelson sealed-offer double auction (ChatterjeeSamuelson). Neither is used here. The von Neumann–Morgenstern utility theorem behind the normalization is formalized as TheoryOfGames.Utility.utility_existence_uniqueness.

Selected references

• J. F. Nash, Jr., The Bargaining Problem, Econometrica 18(2), 155–162, 1950. doi:10.2307/1907266
• J. von Neumann, O. Morgenstern, Theory of Games and Economic Behavior, Princeton University Press, 1944.
• J. F. Nash, Jr., Two-Person Cooperative Games, Econometrica 21(1), 128–140, 1953. doi:10.2307/1906951
• E. Kalai, M. Smorodinsky, Other Solutions to Nash's Bargaining Problem, Econometrica 43(3), 513–518, 1975. doi:10.2307/1914280
• K. Binmore, A. Rubinstein, A. Wolinsky, The Nash Bargaining Solution in Economic Modelling, RAND Journal of Economics 17(2), 176–188, 1986. doi:10.2307/2555382
• M. J. Osborne, A. Rubinstein, Bargaining and Markets, Academic Press, 1990, Theorem 2.3.

Motivation

A newsvendor retailer who may order twice faces a tradeoff. Ordering late lets the retailer use a better demand forecast. Ordering early lets the supplier produce more cheaply, with longer procurement lead times and no overtime labor. Fisher and Raman (1996) document such forecast improvements between ordering epochs in fashion apparel. A decentralized supply chain must balance cheap early production against well-informed late production, and it is not obvious that a simple contract can induce both firms to strike the balance an integrated firm would choose.

This mission formalizes §6.6 of G. P. Cachon's survey chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, Vol. 11, 2003), read in the author's January 2003 draft. The section builds on Donohue (2000), who studied the same two-mode production problem under forced compliance. The chapter's model lets the supplier operate under voluntary compliance: she may deliver less than the retailer orders, and she may produce more in period 1 than was ordered. The question is whether a buy back contract with one wholesale price per ordering epoch still coordinates the supply chain.

Setting

A demand signal $\xi \ge 0$ with density $g$ and distribution function $G$ is observed once before the selling season. Given $\xi$, demand $D$ has distribution function $F(\cdot\,|\,\xi)$, continuous and strictly increasing on $[0,\infty)$. Demand is stochastically increasing in the signal: $F(x\,|\,\xi_h) < F(x\,|\,\xi_l)$ for $\xi_h > \xi_l$. Expected sales are $S(q\,|\,\xi) = E[\min(q,D)\,|\,\xi]$. Period 1 is before the signal and period 2 is after it. The retailer's total order is $q_1$ after period 1 and $q_2 \ge q_1$ after period 2. The supplier's unit production cost is $c_i$ in period $i$, with $c_1 < c_2 < p$, where $p$ is the retail price. Salvage values and goodwill costs are zero.

The supply chain's period-2 objective is

$$\Omega_2(q_2\,|\,q_1,\xi) = pS(q_2\,|\,\xi) - c_2 q_2 + c_2 q_1 ,$$

and $q_2(q_1,\xi)$ maximizes it over $q_2 \ge q_1$. The supply chain's expected profit is $\Omega_1(q_1) = -c_1 q_1 + E[\Omega_2(q_2(q_1,\xi)\,|\,q_1,\xi)]$.

Under the buy back contract $\{w_1, w_2, b\}$ the retailer pays $w_i$ per unit ordered in period $i$, and the supplier refunds $b$ per unsold unit. The retailer's period-2 profit is $\pi_2(q_2\,|\,q_1,\xi) = (p-b)S(q_2\,|\,\xi) - (w_2-b)q_2 + w_2 q_1$, and his period-1 profit is $\pi_1(q_1) = -w_1 q_1 + E[\pi_2(q_2(q_1,\xi)\,|\,q_1,\xi)]$. The supplier's period-2 profit $\Pi_2$ and her period-1 profit $\Pi_1(x\,|\,q_1)$, as functions of the stock $x$ she holds, are given in the mission's Profits definition.

Formalization targets

Goal: the buy back contract coordinates

For $\lambda \in [0,1]$ with

$$p - b = \lambda p,\qquad w_2 - b = \lambda c_2,\qquad w_1 - w_2 + \lambda c_2 = \lambda c_1,$$

the identities

$$\pi_2(q_2\,|\,q_1,\xi) = \lambda\big(\Omega_2(q_2\,|\,q_1,\xi) - c_2 q_1\big) + w_2 q_1,\qquad \pi_1(q_1) = \lambda\,\Omega_1(q_1)$$

hold, so the supply chain's optima in both periods are the retailer's optima (with equivalence for $\lambda > 0$). In addition,

$$w_2 - c_2 = w_1 - \big(\lambda c_1 + (1-\lambda)c_2\big) < w_1 - c_1 \quad (\lambda < 1).$$

Milestones

1. The structure of the period-2 problem, Eqs. (25)–(26): $q_2(\xi)$ solves $F(q_2(\xi)\,|\,\xi) = (p-c_2)/p$ and increases in $\xi$, and the threshold $\xi(q_1)$ splits the signals into those that trigger a period-2 order and those that do not.
2. The retailer's period-2 identity (p. 65).
3. The supplier fills any period-2 order up to $q_2(q_1,\xi)$, and for $\lambda < 1$ she does not fill a larger one (p. 65).
4. The retailer's period-1 identity (p. 66).
5. The first-order condition (27) for $q_1^o$.
6. The supplier's period-2 profit increases in her stock below $q_1$, so she produces at least the period-1 order (p. 66).
7. The supplier produces exactly the period-1 order (p. 67).
8. The margin comparison (p. 67).

Significance

The result shows that the buy back contract, which coordinates the single-period newsvendor, extends to a setting with a forecast update and two production modes, even when the supplier is free to under-deliver or to stockpile. Profit can be divided arbitrarily through $\lambda$. Coordination also forces the supplier's margin on expensive late production below her margin on cheap early production, which contradicts the intuition that the better-informed late order should command a premium. Milestone 7 rules out stranded inventory: under the coordinating terms the supplier never stocks more than the retailer ordered in period 1.

These results are established on paper in Cachon's chapter. No machine-checked version is known. The identities are algebraic. The supplier's production result needs differentiation of an expectation over the signal across the moving threshold $\xi(x)$.

Difficulty

The retailer's identities reduce to algebra once the contract terms are substituted, and the margin comparison is one line. The substantive steps are the derivative formulas (27) and $\partial \Pi_1(x\,|\,q_1)/\partial x = -c_1 + c_2(1 - G(\xi(x)))$. The obvious move, differentiating inside the expectation term by term, fails because the period-2 optimum $\max(q_1, q_2(\xi))$ has a kink at $\xi = \xi(q_1)$. The integrand switches between two regimes, and the switch point moves with $q_1$. The supplier's period-1 profit is not differentiable at $x = q_1$; only its right derivative is negative at $q_1^o$. Turning the page's derivative statements into the global claim that $x = q_1^o$ is her unique optimum needs a monotonicity argument on both sides of $q_1^o$.

Formalization scope

The conditional law is a measurable family $\xi \mapsto D_\xi$ of probability measures on $\mathbb R$ supported on $[0,\infty)$, each with a finite mean, a continuous distribution function, and a distribution function strictly increasing on $[0,\infty)$. The signal has a measurable density $g \ge 0$ with $\int_0^\infty g = 1$, and demand has a finite unconditional mean. These standing assumptions follow the chapter's p. 7 newsvendor model, together with the measurability needed for expectations over the signal. $0 < c_2 < p$ makes the critical ratio lie in $(0,1)$. Expected sales reuse the platform definition SupplyChainTheory.expSales (from SupplyChainTheory_contracts).

The optimum $q_2(q_1,\xi)$ is a hypothesis-carried selection maximizing $\Omega_2$ over $q_2 \ge q_1$. It is never an arbitrary function: a formalization that let $q_2(q_1,\xi)$ be unconstrained would make $\pi_1 = \lambda\Omega_1$ a statement about meaningless orders. The thresholds $\xi(q_1)$ enter as solutions of (26) whose existence is assumed where the page assumes it. Optimal order quantities are taken over $q_1 \ge 0$ and $q_2 \ge q_1$. Derivatives are stated with HasDerivAt (or HasDerivWithinAt for the right derivative at a kink).

Three corrections of the print are disclosed in the item notes:

• the strict margin inequality fails at $\lambda = 1$;
• the p. 66 identity for $\Pi_2(x, q_1, q_2, \xi)$ is off by the constant $(1-\lambda)c_2q_1$;
• "retailer optimal equals chain optimal" needs $\lambda > 0$ in the converse direction.

Contributions are welcome on all milestones. A lemma that differentiates $q \mapsto E[\max_{q_2 \ge q} \Omega_2]$ with a density-driven threshold would be reusable beyond this mission.

Selected references

• G. P. Cachon, Supply Chain Coordination with Contracts, in S. Graves and T. de Kok (eds.), Handbooks in Operations Research and Management Science, Vol. 11: Supply Chain Management, North-Holland, 2003, Ch. 6. https://doi.org/10.1016/S0927-0507(03)11006-7
• K. L. Donohue, Efficient Supply Contracts for Fashion Goods with Forecast Updating and Two Production Modes, Management Science 46(11), 1397–1411, 2000. https://doi.org/10.1287/mnsc.46.11.1397.12088
• M. Fisher and A. Raman, Reducing the Cost of Demand Uncertainty Through Accurate Response to Early Sales, Operations Research 44(1), 87–99, 1996. https://doi.org/10.1287/opre.44.1.87

Motivation

A retailer can keep too little inventory even when its own stocking decision is optimal. In the single-location model of Cachon, Supply Chain Coordination with Contracts (2003), the supplier suffers a cost when the retailer has backorders, but the retailer does not bear that part of the cost. The supplier and retailer therefore prefer different base-stock levels. Section 6.7 asks whether payments tied to expected inventory and backorders can make the retailer choose the level that minimizes their combined cost. The result also describes how the contract divides that cost between the firms.

The model concerns a continuing operation with repeated replenishment opportunities and backordered demand. A base-stock policy keeps the retailer's inventory position at a chosen level by replacing units as demand occurs. Cachon reduces the cost calculation for such a policy to the distribution of demand over one replenishment lead time. That reduction allows the coordination question to be stated with one real stock-level decision rather than a full inventory trajectory. The chapter presents this model as a building block for its two-location system in §6.8 Cachon (2003).

Setting

Let $D_r$ denote lead-time demand, the amount demanded while the retailer waits for replenishment. It is nonnegative and has a finite mean $\mu_r=\mathbb E[D_r]$, distribution function $F_r$, and density $f_r$. At inventory level $s\in\mathbb R$, expected inventory is $I_r(s)=\mathbb E[(s-D_r)^+]$ and expected backorders are $B_r(s)=\mathbb E[(D_r-s)^+]$, where $x^+=\max(x,0)$. The section assumes $F_r(0)=0$ and a strictly increasing differentiable $F_r$ on nonnegative levels. These assumptions place the optimum above zero.

The retailer pays holding cost $h_r I_r(s)$ and its own backorder cost $\beta_r B_r(s)$. The supplier pays a further backorder cost $\beta_s B_r(s)$. All three cost rates are positive. Thus $c_r(s)=h_r I_r(s)+\beta_r B_r(s)$ and $c_s(s)=\beta_s B_r(s)$ are the firms' costs, while $c(s)=c_r(s)+c_s(s)$ is the channel cost. Write $\beta=\beta_r+\beta_s$. Because demand is backordered rather than lost, the section treats the sales rate as constant across the stock decisions and compares costs alone Cachon (2003), §6.7.1.

The proposed contract pays the retailer $t_I I_r(s)+t_B B_r(s)$ from the supplier, where $t_I$ and $t_B$ are transfer rates. A positive rate is a subsidy; a negative rate charges the retailer. For a parameter $\lambda\in(0,1]$, the contract sets $t_I=(1-\lambda)h_r$ and $t_B=\beta_r-\lambda\beta$. The retailer's contracted cost is its original cost minus this transfer; the supplier's contracted cost is its original cost plus it. The parameter $\lambda$ describes a family of printed contract rates and is not itself a payment term Cachon (2003), p. 74.

Formalization targets

The milestones establish the two expectation identities, the channel's cost formula and strict convexity, the channel's critical ratio, the retailer's lower uncontracted stock level, and the retailer's cost after the printed transfer. In the notation above, the channel optimum $s_r^\circ$ is unique and satisfies

$$F_r(s_r^\circ)=\frac{\beta}{h_r+\beta};$$

the uncontracted retailer has its own unique optimum $s_r^*$ with $s_r^*<s_r^\circ$. Three further statements of §6.7.1 complete the section: the signs of the transfer rates over the family ($t_I\ge0$, with $t_I>0$ exactly for $\lambda<1$, and $\{t_B:0<\lambda\le1\}=[-\beta_s,\beta_r)$); the decomposition

$$t_I I_r(y)+t_B B_r(y)=(t_I+t_B)I_r(y)+t_B(\mu_r-y);$$

and the equivalence with the newsvendor model: with lead-time demand as newsvendor demand, retail price $p=h_r+\beta_r$ and wholesale price $w=h_r$, the newsvendor retailer's profit $pS(q)-wq$, with expected sales $S(q)=\mathbb E[\min(q,D_r)]$, equals $-c_r(q)+\beta_r\mu_r$. The mission goal is the coordinating identity of Eq. (33), together with the unique optimality it implies:

$$c_r^\lambda(s)=\lambda c(s),\qquad c_s^\lambda(s)=(1-\lambda)c(s) \quad\text{for all }s\in\mathbb R\text{ and }0<\lambda\le1.$$

Consequently, the retailer's contracted cost has the same unique minimizer $s_r^\circ$ as the channel cost. At each stock level the retailer's contracted cost is strictly increasing in $\lambda$, which is the page's statement that the retailer's share of the cost increases with $\lambda$. The result does not prescribe one fixed allocation of cost: each $\lambda$ in the stated interval gives a contract with the same coordinated stock level and a different retailer share Cachon (2003), Eq. (33), p. 74.

Significance

The theorem identifies an explicit transfer that corrects an incentive gap created by the supplier's backorder cost. Without it, the retailer sets stock according to $\beta_r$, while the channel's stock decision uses $\beta_r+\beta_s$. Under the contract, the retailer bears the fraction $\lambda$ of total cost at every stock level, so its decision agrees with the integrated channel's decision. This conclusion connects a decentralized cost objective to the base-stock target used in the next section's two-location analysis Cachon (2003), §§6.7–6.8.

The chapter proves these claims informally; this mission asks for machine-checked Lean proofs of the expectation identities, convexity and optimality claims, and the contract identity. Its reusable output is the precise treatment of expected positive-part inventory and backorders under a demand law with finite mean. The local definitions may also support later formalizations of inventory contracts. Expected sales in the newsvendor comparison is the published SupplyChainTheory.expSales (definition SupplyChainTheory_contracts), referenced rather than redefined. The existing proved SupplyChainTheory.chain_optimal_fractile concerns a single-period newsvendor profit objective; its critical ratio is related mathematically but belongs to a different model and is not substituted for Eq. (31).

Difficulty

The algebra of the transfer rates is short, but the unique-optimum claim depends on more than algebra. It requires expected inventory and backorders to match the distribution formulas, the cost to have the required curvature at nonnegative levels, and the optimum to occur at a positive level. A formal statement that defines the retailer's contracted cost directly as $\lambda c$ would erase the coordinating claim. The negative-stock region also matters: since demand is nonnegative, expected inventory vanishes there and cost is affine rather than strictly convex. The formulation must keep strict convexity on the range where it holds while still identifying the unique optimum among all real stock levels.

Formalization scope

Lean represents $D_r$ by a probability measure on $\mathbb R$ supported on $[0,\infty)$, with an explicit integrable first moment. The density is a measurable nonnegative function whose induced measure is the demand law; the cdf is continuous, strictly increasing on $[0,\infty)$, equals zero at zero, and has that density as its derivative at positive levels. These are the section's distribution assumptions. The positive rates $h_r,\beta_r,\beta_s$ are fields of one model, and $I_r,B_r$ are defined by expectations. This rules out accidental zero values from nonintegrable real integrals. The cost functions are constructed from the expected inventory and backorders; the transfer is constructed from the two printed rates. The identities in Eqs. (28)–(33) are theorem targets, not definitions.

Stock levels are real, including negative levels, because the section does not explicitly restrict the decision set. The formal result states strict convexity on nonnegative levels and uniqueness of the cost minimizers over all real levels. The page's sentence that $t_I>0$ for all $\lambda\in(0,1]$ fails at $\lambda=1$, where $t_I=0$; the formal statement asserts $t_I\ge0$ with strict positivity exactly for $\lambda<1$. The contract range is exactly $0<\lambda\le1$; $\lambda=0$ would make every retailer stock level cost-equivalent. The transfer sign is positive from supplier to retailer, as on p. 73. Risk neutrality and full information are the chapter's standing conventions. The continuous-review state process, supplier capacity, and proof that a base-stock policy attains the displayed long-run average are not modeled; the mission formalizes the section's explicit lead-time-demand cost reduction. Contributions that establish integrability, distribution identities, strict convexity, and critical-ratio optimality are all needed for closure.

Selected references

• Gérard P. Cachon, Supply Chain Coordination with Contracts, in Handbooks in Operations Research and Management Science, vol. 11, North-Holland, 2003; source used here: author's third draft, January 2003, §6.7. DOI.

Motivation

A retailer who controls both inventory and price can respond to a supply contract in two ways. A contract that induces the right order quantity at a fixed price may change the retailer's incentive to raise or lower that price. For a one-season supply chain, Cachon's chapter compares familiar contracts under price-dependent demand and identifies a price-contingent buy-back, also called a price-discount contract, that aligns both decisions. The mission concerns §6.3 of the author's January 2003 third draft, on printed pages 33–38. Those page and equation numbers belong to the draft and may differ from the typeset chapter.

Setting

One risk-neutral supplier and one risk-neutral retailer have full information before a single selling season. The retailer chooses a nonnegative stocking quantity $q$ and a retail price $p$ from an admissible price set $P$; the price stays fixed during the season. Demand has a probability law $D_p$ that depends on $p$. Write $F(y\mid p)$ for its distribution function, $S(q,p)=\mathbb E_p[\min(q,D)]$ for expected sales, and $\mu(p)=\mathbb E_p[D]$ for mean demand. Demand is nonnegative, has a finite mean and, in the chapter's regular setting, its distribution function increases with demand level and has a positive price derivative at positive demand levels. Higher prices thus lower demand in the stochastic order used by the chapter. The price set is nonempty and open so an admissible price optimum has an interior first-order condition.

The supplier's unit cost is $c_s$, the retailer's unit procurement cost is $c_r$, and $c=c_s+c_r$ is total unit cost. Their goodwill penalties for unmet demand are $g_s$ and $g_r$, with $g=g_s+g_r$. An unsold unit has salvage value $v$ at the retailer. The integrated channel's expected profit is

$$\Pi(q,p)=(p-v+g)S(q,p)-(c-v)q-g\mu(p).$$

A buy-back contract charges a wholesale price $w_b$ for each ordered unit and pays the retailer $b$ for each unsold unit. A revenue-sharing contract charges a wholesale price $w_r$ and gives the retailer a fraction $\phi$ of sales and salvage revenue. In this section the supplier offers the terms and the retailer chooses $(q,p)$. The profit formulas use the chapter's convention that a positive transfer goes from retailer to supplier.

Formalization targets

The goal is the price-contingent buy-back on p. 35, with $\lambda\in[0,1]$:

$$b(p)=(1-\lambda)(p-v+g)-g_s,\qquad w_b(p)=\lambda c_s+(1-\lambda)(p+g-c_r)-g_s.$$

In the chapter's zero-goodwill case, $g_r=g_s=0$, every feasible $(q,p)$ then gives the retailer $\lambda\Pi(q,p)$ and the supplier $(1-\lambda)\Pi(q,p)$. The same retailer profit is obtained from revenue sharing with $\phi=\lambda$ and $w_r=\lambda(c-v)-c_r+\lambda v$. Thus every existing maximizer $(q^\circ,p^\circ)$ of the integrated profit maximizes each firm's profit under the contingent buy-back. At $\lambda=0$ the retailer is indifferent; at $\lambda=1$ the supplier is indifferent.

The milestones follow the chapter's printed claims in attack order:

1. the integrated price condition (14), p. 34;
2. the quantity-flexibility condition (15), p. 34: price coordination forces $w_q=v-c_r$ or $\delta=0$;
3. the fixed buy-back condition (16), p. 35: price coordination forces $b=-g_s$ and then $w_b=c_s-g_s$;
4. the linear price-contingent terms derived from (5)–(6), p. 35;
5. the p. 36 profit split $\pi_r=\lambda(\Pi+g\mu)-g_r\mu$, $\pi_s=(1-\lambda)\Pi-(\lambda g-g_r)\mu$, valid for all goodwill penalties as an identity;
6. the zero-goodwill revenue-sharing price claim following (17), p. 36 (the milestone quotes its restatement in §6.3.2, p. 38);
7. the price-contingent revenue-sharing parameters, p. 37;
8. the quantity discount $w_d(q)$, pp. 37–38: with $g_s=0$ it does not distort the price, and given $p^\circ$ it makes $q^\circ$ optimal for both firms.

Significance

The result identifies a contract schedule under which the same quantity-price pair is best for the integrated channel and for the two firms' reported profit functions. It also explains the relation between a buy-back whose terms vary with the chosen price and a revenue-sharing arrangement. In the zero-goodwill setting, both allocate every realized choice's expected channel profit in fixed shares. The general-goodwill identity shows the additional mean-demand terms that matter when the retailer controls price.

The source presents these results analytically; this mission asks for Lean proofs of the stated price and profit relationships. A published Prove2Me definition already supplies expected sales and mean demand for a single demand law, and the model here applies those functions to each price's law. The earlier open theorem RevShareCoord.Single.price_quantity_coordination (from Cachon and Lariviere's revenue-sharing paper) treats deterministic revenue and a simpler cost convention. It is an overlap in theme, but its statement does not include price-indexed demand, salvage value, retailer cost or the contingent buy-back terms, so it is not posed again here. The new model can support further price-dependent contract comparisons in the chapter.

Difficulty

The obstacle is that matching the retailer's quantity incentive at a fixed price can change the retailer's price incentive. The buy-back rate required by the fixed-price coordination equations depends on $p$; a fixed buy-back contract therefore does not generally align both choices. Revenue sharing with goodwill penalties has a similar price dependence. The integrated profit need not be concave or unimodal in $(q,p)$, so a price first-order condition by itself does not establish coordination. The chapter assumes a finite integrated optimum exists and treats the price condition as necessary, not sufficient.

Formalization scope

Lean represents price-dependent demand as a family of probability measures on $\mathbb R$, one for each price in $P$. Each admissible law is supported on nonnegative demand, has no atom at zero and has an integrable identity function, so $\mu(p)$ is a genuine finite expectation. Sales are defined by $\mathbb E_p[\min(q,D)]$, using the published SupplyChainTheory_contracts definition; they are not defined by the equivalent CDF integral. The admissible decisions are exactly $q\ge0$ and $p\in P$. Unit costs and goodwill penalties are nonnegative, each admissible price exceeds $c=c_s+c_r$, and $v<c$, as in the model of §6.2. The chapter's standing risk-neutrality and full-information conventions appear in the use of expected profit with the same demand laws available to both firms.

There is a material qualification. With price-dependent demand, $\mu(p)$ may change with $p$. The printed first-order condition (14) and the p. 36 inference from $\pi_r=\lambda(\Pi+g\mu)-g_r\mu$ to a joint optimum omit that effect when goodwill penalties are positive. Price first-order and optimality statements here therefore use $g_r=g_s=0$, a case explicitly discussed in the chapter; general-goodwill claims are limited to algebraic identities. The printed p. 36 equality of price derivatives under revenue sharing also misses its factor $\phi$, which the formal statement restores. The contingent buy-back terms are defined by the chapter's linear formulas, not by a property that hard-codes coordination. The algebraic statement permits parameter values that may violate economic buy-back bounds such as $0\le b\le w_b$; those bounds need separate checks when selecting a contract.

Two first-order statements, (15) and (16), compare price derivatives; they take the derivative of expected sales in price as a hypothesis, and (15) also takes differentiation under the integral sign of $\int_{(1-\delta)q}^{q}F(y\mid p)\,dy$ as a disclosed regularity hypothesis. For the quantity discount, the statement claims what the page shows, undistorted prices for each $q$ and optimality of $q^\circ$ given $p^\circ$, not joint optimality of $(q^\circ,p^\circ)$ for the retailer. The page's claim that revenue sharing with goodwill coordinates only with $\phi=g_r/g$ is not stated, for the mean-demand reason above.

A trivializing formalization is ruled out: no contract term is defined by the profit identity it should satisfy, the demand family cannot be replaced by a single law, and the optimal pair is a hypothesis about the integrated profit, not a chosen witness.

Reusable contributions include the price-indexed demand family, the expected-profit model with five contract types, and the price-maximizer statements. Proofs of the first-order milestones need Fermat's interior-extremum theorem on the open price set and, for (15), positivity of an interval integral; the identities need the expectation algebra of $S$ and $\mu$, including $S(0,p)=0$.

Selected references

• Gérard P. Cachon, “Supply Chain Coordination with Contracts,” in Handbooks in Operations Research and Management Science, vol. 11, Supply Chain Management, North-Holland, 2003. DOI 10.1016/S0927-0507(03)11006-7. Formalization source: author's third draft, January 2003, §6.3, pp. 33–38.
• Fernando Bernstein and Awi Federgruen, “Decentralized supply chains with competing retailers under demand uncertainty,” Management Science 51(1), 2005 (the price-discount sharing contract; cited in the draft as a 2000 working paper). DOI 10.1287/mnsc.1040.0230
• Nicholas C. Petruzzi and Maqbool Dada, “Pricing and the newsvendor problem: a review with extensions,” Operations Research 47(2), 1999, 183–194. DOI 10.1287/opre.47.2.183

Why minimum-cost circulation needs a real-cost iteration bound

A minimum-cost circulation is a way to send flow around a directed network while respecting capacities and paying a cost per unit on each arc. It is a basic form of network optimization: a minimum-cost flow with prescribed supplies and demands can be reduced to a circulation problem, and the circulation formulation exposes the residual arcs on which a flow can be improved. Goldberg and Tarjan's successive-approximation method relaxes exact optimality by an error parameter and repeatedly reduces that error. Its ordinary stopping rule for integer costs depends on the largest cost. For arbitrary real costs, including irrational costs, a decreasing positive error need never cross a fixed numerical cutoff. The strongly polynomial loop in their 1987 technical report, later published in Mathematics of Operations Research instead tests the smallest error parameter appropriate to the current circulation and stops when it is zero.

This mission formalizes the number of refinement calls made by that loop. It builds on the related Goldberg–Tarjan 1988 max-flow and 1989 minimum-mean cycle-canceling series: those develop different algorithms for network flow, while the published 1989 circulation and approximate-optimality definitions provide this mission's common network model. The result here concerns successive approximation and its fixed-arc progress measure.

Network and approximate optimality

The vertex set $V$ is finite, with $n=|V|$, and $E$ is a symmetric set of directed arcs, with $m=|E|$. Symmetry means that $(v,w)\in E$ brings $(w,v)\in E$ too. Each arc has a real capacity $u(v,w)$ and a real cost $c(v,w)$; costs obey $c(v,w)=-c(w,v)$. A circulation $f$ obeys $f(v,w)\le u(v,w)$, $f(v,w)=-f(w,v)$, and conservation of flow at every vertex. Its total cost is half the sum of $c(v,w)f(v,w)$ over directed arcs, since each unordered edge appears twice. A minimum-cost circulation costs no more than any other circulation of the network.

The residual capacity is $u_f(v,w)=u(v,w)-f(v,w)$. For a price function $p:V\to\mathbb R$, the report writes the reduced cost as $c_p(v,w)=c(v,w)-p(v)+p(w)$. A circulation is $\varepsilon$-optimal with respect to $p$ when every residual arc has reduced cost at least $-\varepsilon$. It is $\varepsilon$-optimal if some price function works, where $\varepsilon\ge0$. The tight error $\varepsilon(f)$ is the least such error. A circulation is $\varepsilon$-tight when it is $\varepsilon$-optimal but fails to be $\varepsilon'$-optimal at every $\varepsilon'<\varepsilon$. This includes attainment at $\varepsilon$.

An arc is $\varepsilon$-fixed if all $\varepsilon$-optimal circulations carry the same flow through it. Write $F_\varepsilon$ for the set of these arcs. Theorem 4.2 supplies an arc-fixing criterion from a large absolute reduced cost. Lemma 4.4 says that when a positive tight error falls by a factor of $2n$, $F_\varepsilon$ becomes strictly larger. Both are numbered results on printed pages 16–17 of the source report's journal counterpart.

Formalization targets

The goal is the circulation-level form of Theorem 4.5. Begin with a circulation $f_0$ and a sequence $f_0,f_1,\ldots$ whose positive-error steps satisfy the contract of Figure 3: if $\varepsilon(f_k)>0$, the next circulation is $\varepsilon(f_k)/2$-optimal. With the report's standing $n\ge2$ and $m\ge n-1$, the target is

$$\exists k\le m\left\lceil\log_2(2n)\right\rceil:\quad \varepsilon(f_k)=0\quad\text{and}\quad f_k\text{ is minimum-cost}.$$

The milestone list contains the already proved complementary-slackness characterization of minimum cost (Theorem 2.2), the cross-parameter arc-fixing result (Theorem 4.2), and strict growth of fixed arcs (Lemma 4.4). The report states Theorem 4.5 as $O(m\log n)$ iterations when each refinement decreases error by a constant factor. The target makes explicit the factor two used by the paper's refinements and the resulting finite count.

What the result establishes

The theorem gives a bound on the number of refinement calls that depends on the number of vertices and arcs, not on the magnitude, precision, or integrality of the costs. It gives an exact minimum-cost circulation rather than an arbitrary small-error approximation. This distinguishes the real-cost loop from an integer-cost stopping rule based on $1/n$. The bound counts refinement calls only; the report analyzes the work within particular implementations separately.

The published 1989 definitions and the complementary-slackness theorem already have machine-checked status on the platform. Theorem 4.2, Lemma 4.4, and this iteration theorem are the open formalization targets. A complete development will connect the tight error to residual-cycle structure, establish that its infimum is attained for circulations, and prove that zero tight error implies minimum cost. The mission thereby makes the fixed-arc argument reusable for other circulation algorithms that lower an approximate-optimality parameter.

Why the bound needs more than repeated halving

Repeatedly dividing a positive real error by two gives errors approaching zero, but it does not by itself produce a finite step with zero error. The missing finite progress is structural: an arc must become fixed after enough reductions, and only finitely many arcs exist. Proving that fixedness is strict is delicate because it compares all circulations at two different error levels, not just two consecutive flows. Theorem 4.2 is the quantitative bridge between a price certificate for one flow and agreement of an arc across every sufficiently accurate flow. At the boundary $\varepsilon=0$, the printed wording of Lemma 4.4 would require $F_0$ to be a proper subset of itself, so its positive-error regime must be made explicit.

Formalization scope

The Lean network uses CycleCanceling.MinMean.CircNetwork with a finite vertex type, a finite symmetric arc set, and real-valued capacities, costs, and flows. Off-arc values of these functions are irrelevant. The report assumes $m\ge n-1\ge1$ on printed page 5; the theorem binders express it as $n\ge2$ and $m\ge n-1$. The arc count is for ordered arcs, exactly as the report defines $m$. No integrality, rounding, or bounded-cost hypothesis is imposed. A feasible initial circulation is required because Figure 3 starts from one; infeasibility detection is outside this target.

The reused 1989 definitions write reduced cost as $c(v,w)+p(v)-p(w)$. Substituting $-p$ for $p$ gives the report's $c(v,w)-p(v)+p(w)$, so existential price certificates, $\varepsilon$-optimality, and absolute reduced-cost conditions agree. The tight error is represented by a real infimum; proving that it is attained is part of the work. The set $F_\varepsilon$ is filtered from $E$ and includes only arcs whose flow is shared by all $\varepsilon$-optimal circulations. The halving run computes its error from the current circulation; it does not take an unrelated error sequence. Once that error is zero, the loop has returned and later sequence entries are unconstrained. These choices exclude a vacuous or artificially fixed error parameter and a preselected optimal flow.

The explicit reading of the report's asymptotic count is $t=\lceil\log_2(2n)\rceil$ halvings per factor-$2n$ reduction and at most $m$ such blocks, giving $m t$ refinements. This is a statement about refinement count, not a RAM-operation bound. Contributions on Theorem 4.2, the residual-cycle characterization of positive tight error, the fixed-arc strictness lemma, and the final finite counting argument all support the goal. The circulation, price, and fixed-arc infrastructure can be reused beyond this particular implementation.

Selected references

• A. V. Goldberg and R. E. Tarjan, Finding Minimum-Cost Circulations by Successive Approximation, MIT/LCS/TM-333, July 1987; journal version in Mathematics of Operations Research 15(3), 1990, pp. 430–466. DOI: 10.1287/moor.15.3.430. The mission's page and theorem indices refer to the 1987 report.