All missions

Motivation

In a supply chain with stock at two locations, a supplier holds inventory that replenishes a retailer, and the retailer serves customers. Each firm sets its own inventory level to minimize its own cost. The retailer bears only part of the cost of customer backorders, and the supplier bears none of the retailer's holding cost, so their incentives differ. The resulting equilibrium generally differs from the policy that minimizes total cost. Cachon and Zipkin (Management Science 45(7), 1999) studied this game and proposed linear transfer payments that align the firms' incentives. In the chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, vol. 11, 2003, doi:10.1016/S0927-0507(03)11006-7), Cachon re-derives that analysis, adds a parameter $\lambda$ that divides the retail-level costs between the firms, and answers two questions the original paper left open: whether the contracts allow an arbitrary division of cost, and whether the optimal policy is the unique equilibrium under the contracts. This mission formalizes the second answer, together with the analysis of the decentralized game and of the optimal policy that it rests on (§6.8 of the 2003 chapter, read in the author's January 2003 draft).

Setting

Two firms, a retailer $r$ and a supplier $s$, each use a base stock policy: firm $i$ keeps its inventory position equal to its base stock level $s_i \in \mathbb R$. A negative supplier base stock means planned backorders. Let $D_r$ and $D_s$ be the demands during the retailer's and the supplier's lead times. They are nonnegative with finite means $\mu_r$, $\mu_s$, and their distribution functions $F_r$, $F_s$ are continuous, zero at $0$, strictly increasing on $[0,\infty)$ and differentiable on $(0,\infty)$. Holding costs are $h_r$ and $h_s$, with $0 < h_s < h_r$. Each backorder at the retailer costs the retailer $\beta_r > 0$ and the supplier $\beta_s > 0$ per unit time. Write $\beta = \beta_r + \beta_s$.

At retailer inventory level $y$ the expected on-hand stock is $I_r(y) = E[(y-D_r)^+]$ and the expected backorders are $B_r(y) = E[(D_r-y)^+]$. The retail-level cost rates are $c_r(y) = h_rI_r(y) + \beta_rB_r(y)$, $c_s(y) = \beta_sB_r(y)$ and $c(y) = c_r(y) + c_s(y)$. Because the supplier may stock out, the retailer's actual inventory level is $s_r - (D_s - s_s)^+$, and every retail-level quantity is averaged accordingly:

$$g(s_r,s_s) = E\big[g(s_r - (D_s-s_s)^+)\big] = F_s(s_s)g(s_r) + \int_{s_s}^\infty g(s_r+s_s-x)f_s(x)\,dx .$$

With the supplier's inventory $I_s(y) = E[(y-D_s)^+]$ and backorders $B_s(y) = \mu_s - y + I_s(y)$, the firms' costs and the chain's cost are

$$\pi_r(s_r,s_s) = c_r(s_r,s_s), \qquad \pi_s(s_r,s_s) = h_sI_s(s_s) + c_s(s_r,s_s), \qquad \Pi = \pi_r + \pi_s .$$

A pair $\{s_r^o, s_s^o\}$ minimizing $\Pi$ is an optimal policy. A Nash equilibrium is a pair from which neither firm can lower its own cost by a unilateral change of its base stock.

Under a linear transfer the supplier pays the retailer $t_II_r(s_r,s_s) + t_B^rB_r(s_r,s_s) + t_B^sB_s(s_s)$ (a negative amount is a payment the other way). The Cachon–Zipkin contracts with parameter $\lambda \in (0,1]$ are

$$t_I = (1-\lambda)h_r, \qquad t_B^r = \beta_r - \lambda\beta, \qquad t_B^s = \lambda h_s\frac{F_s(s_s^o)}{1-F_s(s_s^o)} .$$

Formalization targets

Goal: the contracts coordinate, uniquely

If $\{s_r^o, s_s^o\}$ is optimal with $s_s^o > 0$ and $\lambda \in (0,1]$, then under the contracts

$$\pi_r = \lambda c(s_r,s_s) - t_B^sB_s(s_s), \qquad \pi_s = (h_s+t_B^s)I_s(s_s) + (1-\lambda)c(s_r,s_s) + t_B^s(\mu_s - s_s),$$

$\{s_r^o, s_s^o\}$ is a Nash equilibrium, and it is the only one. The goal contains no numerical constants. It holds for every demand distribution in the class and every $\lambda$ in the range.

Milestones

1. In the uncontracted game, every retailer best response exceeds $\hat s_r > 0$, where $F_r(\hat s_r) = \beta_r/(h_r+\beta_r)$, and every supplier best response is positive (pp. 79–80).
2. In the uncontracted game, for every $s_s$ the retailer's optimal base stock is below the chain's; consequently the competition penalty $(\Pi(s^*) - \Pi(s^o))/\Pi(s^o)$ is positive at every equilibrium $s^*$ (pp. 80–81).
3. The partial derivatives (35)–(36) of $\Pi$, and every optimum with $s_s > 0$ satisfies $c'(s_r) = h_s$, i.e. $F_r(s_r) = (h_s+\beta)/(h_r+\beta)$ (37) (p. 83).
4. Optima with $s_s \le 0$ have $s_r + s_s = \bar s$, where $\Pr(D_r + D_s \le \bar s) = \beta/(h_r+\beta)$ (38) (p. 83).
5. The cost identities (42)–(43) under the contracts (p. 84).
6. Under the contracts the retailer's best response decreases in $s_s$, and the supplier's marginal cost along it has the closed form printed on p. 84.

Significance

The goal says that a contract built from quantities both firms can measure, namely the retailer's inventory and backorders and the supplier's backorders, makes the system-optimal policy the only equilibrium. The firms therefore reach the optimum without coordinating on an equilibrium. The parameter $\lambda$ splits the retail-level costs between the firms in any proportion up to $\lambda = 1$. Milestone 2 shows the contract is needed: without transfers, decentralization is always strictly suboptimal when the supplier is charged for retail backorders. The transfers $t_I$ and $t_B^r$ are those of the single-location model (§6.7), even though the retailer's target fractile changes from $\beta/(\beta+h_r)$ to $(\beta+h_s)/(\beta+h_r)$.

The results are proved in the source and in Cachon and Zipkin (1999), with informal derivative arguments. No machine-checked version is known. Formalizing them requires differentiating expectations of piecewise-linear convex functions of a random lead-time shortfall. The page's argument also assumes densities, which the formal statements avoid, and contains several printing slips (see below). These would be settled by a complete development.

Difficulty

The firms' costs are compositions: a convex single-location cost evaluated at the random level $s_r - (D_s - s_s)^+$, which is concave in $s_s$. The supplier's cost is therefore not obviously convex in $s_s$; its convexity at $s_r = s_r^o$ depends on the value of $t_B^s$ and on $c'(s_r^o) = h_s$. Uniqueness is the hard part. Under the contracts the retailer's best response $s_r(s_s)$ decreases, but the supplier's marginal cost along that best response, $F_s(s_s)(h_s - (1-\lambda)c'(s_r(s_s)) + t_B^s) - t_B^s$, is not monotone in general when $\lambda$ is small, contrary to a literal reading of p. 84. A uniqueness argument has to show that it has at most one zero, not that it increases.

Formalization scope

Demand laws are probability measures on $\mathbb R$ with no mass below $0$, finite means, and continuous distribution functions, zero at $0$, strictly increasing on $[0,\infty)$ and differentiable on $(0,\infty)$. These are the section's standing assumptions, together with $0 < h_s < h_r$ and $\beta_r, \beta_s > 0$ (footnote 34 excludes the zero cases). Expectations are Lebesgue integrals: $I_r$, $B_r$, $I_s$ and the two-location averages are defined by expectation, and the page's integral forms are consequences. Integrals against $f_s(x)\,dx$ are written against the law of $D_s$, so no density hypothesis is made. Base stocks range over all of $\mathbb R$, and "optimal" means minimizing $\Pi$ over $\mathbb R^2$; the existence of an optimum is a hypothesis, as on p. 77. Derivatives are stated with HasDerivAt. Independence of $D_r$ and $D_s$, implicit on the page, enters only through the convolution of their laws in (38).

The contracted costs are defined from the firms' original costs and the transfer payment. Defining them by the closed forms (42)–(43) would make the identities trivial and is ruled out.

Corrected slips: (42) is stated with $\lambda c(s_r,s_s)$ where the page prints $\lambda\Pi(s_r,s_s)$ (the difference $\lambda h_sI_s(s_s)$ does not depend on $s_r$). The retailer's single-location fractile on p. 79 is stated as $\beta_r/(h_r+\beta_r)$, not the printed $\beta/(h_r+\beta)$. The garbled display after (43) and the $f_s$/$F_s$ slip in the best-response derivative are not reproduced. Not included: the contraction condition (34), the case split for the optimal policy (p. 84), the case $s_s^o \le 0$, and the alternative schemes of §6.8.5 (Lee–Whang, Chen). Contributions of those, or of a reusable library for derivatives of $E[g(s - (D-t)^+)]$, are welcome. The platform's Clark–Scarf items (InventoryControl_clarkScarf, ClarkScarf.Serial.*) concern periodic-review echelon policies and are not reused.

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, North-Holland, 2003, §6.8. https://doi.org/10.1016/S0927-0507(03)11006-7
• G. P. Cachon and P. H. Zipkin, Competitive and cooperative inventory policies in a two-stage supply chain, Management Science 45(7), 936–953, 1999. https://doi.org/10.1287/mnsc.45.7.936
• F. Chen and Y.-S. Zheng, Lower bounds for multi-echelon stochastic inventory systems, Management Science 40(11), 1426–1443, 1994. https://doi.org/10.1287/mnsc.40.11.1426
• A. Federgruen and P. Zipkin, Computational issues in an infinite-horizon, multiechelon inventory model, Operations Research 32(4), 818–836, 1984. https://doi.org/10.1287/opre.32.4.818

Motivation

In 1983 H. W. Lenstra, Jr. proved that integer linear programming with a fixed number of variables is solvable in polynomial time (Lenstra 1983). The algorithm became one of the founding results of algorithmic geometry of numbers: it introduced the strategy of making a convex body "round" by a linear change of coordinates, and then either finding a lattice point in it or showing that the body is covered by few parallel lattice hyperplanes, which reduces the dimension by one.

The algorithm rests on two geometric facts, each with its own proof. The first (§1 of the paper, the companion mission Integer Programming with a Fixed Number of Variables 1) says that a round body that misses the lattice meets few lattice hyperplanes. This mission is the second (§2): an explicit construction of the rounding transformation. Starting from a simplex inside the polytope, the algorithm repeatedly swaps a vertex for a point of the polytope as long as this increases the simplex's volume by more than a factor $3/2$. When no such swap exists, a linear map that makes the simplex regular also makes the polytope round, with an explicit roundness ratio $2n^{3/2}$.

Short timeline. Khachiyan's ellipsoid method (1979) made linear programming polynomial and supplied the subroutine that Lenstra uses to maximize linear functions on $K$. Lenstra's algorithm (preprint 1981, published 1983) combined it with the lattice basis reduction of Lenstra, Lenstra and Lovász (1982). Remark (c) of the paper notes that rounding with a maximal-volume inscribed ellipsoid achieves the better ratio $n$, but not by a polynomial algorithm for varying $n$; later work (Kannan 1987, Grötschel–Lovász–Schrijver 1988) refined the rounding step with ellipsoid methods.

Setting

Work in $\mathbb R^n$ with the Euclidean length $|\cdot|$, and write $B(p, \rho) = \{x \in \mathbb R^n : |x - p| \le \rho\}$ for the closed ball. For points $w_0, \dots, w_n \in \mathbb R^n$, the simplex volume is

$$\mathrm{vol}(w_0, \dots, w_n) = \frac{|\det M|}{n!},$$

where $M$ has column vectors $w_1 - w_0, \dots, w_n - w_0$.

Let $K \subseteq \mathbb R^n$ be convex, and let $v_0, \dots, v_n \in K$ with $v_1 - v_0, \dots, v_n - v_0$ linearly independent. Choose linear functions $g_0, \dots, g_n : \mathbb R^n \to \mathbb R$ with

$$g_i \text{ constant on } \{v_j : j \ne i\}, \qquad g_i(v_i) \ne g_i(v_j) \ (j \ne i). \tag{15}$$

Thus $g_i$ measures the height above the facet opposite $v_i$. The stopping condition of the second stage is

$$|g_i(x - v_j)| \le \tfrac32\, |g_i(v_i - v_j)| \quad \text{for all } x \in K \text{ and all } i \ne j. \tag{16}$$

The ratio $|g_i(x - v_j)|/|g_i(v_i - v_j)|$ is the factor by which the volume changes when $v_i$ is replaced by $x$, so (16) says that no such swap enlarges the simplex by more than $3/2$.

Let $\tau$ be a nonsingular linear map of $\mathbb R^n$ such that $z_j = \tau(v_j)$ span a regular simplex, meaning that all distances $|z_i - z_j|$, $i \ne j$, are equal. Let $p = (n+1)^{-1}\sum_j z_j$ be its centroid and $S$ its convex hull. For $c \ge 1$, the paper defines

$$T_c = \{x \in \mathbb R^n : \mathrm{vol}(z_0, \dots, z_{i-1}, x, z_{i+1}, \dots, z_n) \le c\cdot \mathrm{vol}(z_0, \dots, z_n) \text{ for all } i\}.$$

The proof of the LEMMA works in model coordinates. There $\mathbb R^n$ is the hyperplane $\sum_{j=0}^n r_j = 1$ of $\mathbb R^{n+1}$, the $z_j$ are the standard basis vectors, $p = (\tfrac1{n+1}, \dots, \tfrac1{n+1})$, and $T_c = \{r : |r_j| \le c \text{ for all } j,\ \sum_j r_j = 1\}$.

Formalization targets

Goal (§2, p. 543)

Under (15) and (16), with $\tau$ making the simplex regular and $p$ its centroid, there are positive reals $r, R$ with

$$B(p, r) \subseteq \tau K \subseteq B(p, R), \qquad \frac{R}{r} \le 2n^{3/2}.$$

These are conditions (3)–(4) of §1 with $c_1 = 2n^{3/2}$.

Milestones, in the order the proof uses them

1. (16) is a statement about $T_{3/2}$ (p. 543). Condition (16), for all $x \in K$ and $i \ne j$, holds exactly when $\tau K \subseteq T_{3/2}$.
2. Vertices of $T_c$ (pp. 543–544). In the model, $T_c$ is the convex hull of the coordinate permutations of $e_0 - c\sum_{j=1}^m e_j + c\sum_{j=m+1}^n e_j$ ($n = 2m$), or of $(1-c)e_0 - c\sum_{j=1}^m e_j + c\sum_{j=m+1}^n e_j$ ($n = 2m+1$).
3. Outer radius (p. 544). $T_c \subseteq B(p, R)$ with $R^2 = nc^2 + \tfrac{n}{n+1}$ ($n$ even) or $(n+1)c^2 - 2c + \tfrac{n}{n+1}$ ($n$ odd).
4. Inner radius (p. 544). $B(p, r) \subseteq S$ inside the hyperplane, with $r^2 = \tfrac{1}{n(n+1)}$.
5. LEMMA (p. 543). For $c \ge 1$ and any regular simplex, $B(p, r) \subseteq S \subseteq T_c \subseteq B(p, R)$ for positive $r, R$ with

$$\Big(\frac Rr\Big)^2 = \begin{cases} c^2n^3 + (c^2+1)n^2 & n \text{ even},\\ c^2n^3 + (2c^2 - 2c + 1)n^2 + (c^2 - 2c)n & n \text{ odd}.\end{cases}$$

The paper's own proof derives the goal from milestone 1 and the LEMMA at $c = 3/2$. At $n = 1$ the constant $2n^{3/2}$ cannot be improved by this argument.

Significance

The result. The theorem is the only place in the paper where the roundness constant $c_1$ is computed, and $c_1$ enters the bound $1 + c_1c_2\sqrt n$ on the number of lattice hyperplanes that the algorithm branches over. Remark (c) of the paper uses the exact LEMMA for other values of $c$ to obtain $c_1 = ((1+\epsilon)(n^3 + 2n^2))^{1/2}$ ($n$ even) and $((1+\epsilon)(n^3+n^2-n))^{1/2}$ ($n$ odd). The LEMMA itself is a self-contained fact about the regular simplex. In Euclidean geometry it says how far the "volume-$c$ neighbourhood" $T_c$ of a regular simplex extends.

The formalization. The result is classical and proved in the paper. Nothing in it has been machine-checked: there is no regular simplex in Mathlib, and no formal result relates simplex volumes to barycentric coordinates in this form. The platform has the related ellipsoid rounding ConvexOptimization.lowner_john_polytope_rounding (the John-ellipsoid version with factor $n$, by Shuze Chen) and its definition ConvexOptimization_IsLownerJohn. That is the alternative construction of Remark (c). It has a different constant and is not used here. This mission and its companion together give a formal account of the geometry behind Lenstra's algorithm. The algorithm itself is not formalized: its running time needs a machine model and an encoding that the paper does not fix.

Difficulty

There are two separate difficulties. The first is the translation in milestone 1. It needs the volume of a simplex with one vertex replaced to be identified with a barycentric coordinate, through a determinant identity, and it needs this identification to survive the linear map $\tau$. The second is the transfer to the model. The paper's "similarity transformation" identifies $\mathbb R^n$ with a hyperplane of $\mathbb R^{n+1}$ and sends the regular simplex to the standard one. In Lean the vertex description (milestone 2), the radii (milestones 3–4) and $T_c$ must all be carried across this isometry up to scaling. The LEMMA is stated in $\mathbb R^n$, not in the model. The "straightforward analysis" behind milestone 2 is a vertex enumeration of a cube cut by a hyperplane, and its parity split is where sign errors appear.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) and the model $\mathbb R^{n+1}$ is EuclideanSpace ℝ (Fin (n+1)). Distances are Euclidean, never the sup norm. Vertices are indexed by Fin (n+1), matching $0, \dots, n$.
• The volume keeps the paper's normalisation $|\det M|/n!$. $T_c$ is defined from volumes exactly as on p. 543, not from barycentric coordinates.
• Readings of loose phrases. "Nonsingular endomorphism" is a linear equivalence. "Span a regular $n$-simplex" means all pairwise distances are equal and positive. "Certain/two positive real numbers $r, R$" is an existential with $0 < r$ and $0 < R$ in the conclusion; without them, $R/r$ with $r = 0$ would be $0$ in Lean. The LEMMA keeps the printed equality for $(R/r)^2$. (15) is two hypotheses on $g$, and (16) is quantified over all $x \in K$ and all pairs $i \ne j$.
• Generalizations, all harmless. The paper's $K$ is a bounded polyhedron and the $v_j$ are vertices; the claim is stated for any convex $K$ and any points $v_j \in K$, and boundedness of $K$ follows from (16). Milestone 1 holds for any set $K$. The LEMMA is stated for any regular simplex, since $\tau$ plays no role in it.
• $n \ge 1$ throughout. In the model, the ball of milestone 4 is intersected with the hyperplane $\sum_j x_j = 1$, the paper's $\mathbb R^n$. The full ball of $\mathbb R^{n+1}$ is not inside $S$.
• No trivializing formalization is possible: the hypotheses are satisfiable (checked at $n = 1$, $K = [0,1]$), the radii are positive, and the sets are computed from the data rather than assumed.
• Useful infrastructure, reusable beyond this mission: the volume of a simplex with one vertex replaced, as a multiple of a barycentric coordinate; existence and properties of regular simplices in $\mathbb R^n$; the isometric embedding of a regular simplex onto the standard simplex. Contributions of any of these as separate lemmas are welcome.

Selected references

• H. W. Lenstra, Jr., Integer programming with a fixed number of variables, Mathematics of Operations Research 8(4) (1983) 538–548. https://doi.org/10.1287/moor.8.4.538
• A. K. Lenstra, H. W. Lenstra, Jr., L. Lovász, Factoring polynomials with rational coefficients, Mathematische Annalen 261 (1982) 515–534. https://doi.org/10.1007/BF01457454
• L. G. Khachiyan, A polynomial algorithm in linear programming, Soviet Math. Doklady 20 (1979) 191–194.
• R. Kannan, Minkowski's convex body theorem and integer programming, Mathematics of Operations Research 12(3) (1987) 415–440. https://doi.org/10.1287/moor.12.3.415
• M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4

Motivation

A supplier that sells through many competing retailers usually worries that competition among them pushes orders too high, because each retailer ignores the demand it takes from the others. Deneckere, Marvel and Peck (1997) identified the opposite failure. When the retail price is set by the market after demand is realized, retailers who hold too much stock in a weak market bid the price down, and anticipating this, perfectly competitive retailers order too little. The supplier then needs a contract that raises orders, and the classical justification for resale price maintenance (a price floor imposed on retailers) comes out of this model. G. P. Cachon's survey chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, Vol. 11, 2003) presents the model in §6.5.2 as a closed-form example. In it the supplier's best wholesale price contract is computed explicitly and compared with two contracts that recover the monopoly profit: resale price maintenance and a full-refund buy-back.

This mission is volume V of a series that formalizes the section capstones of that chapter, read in the author's 3rd draft (January 2003), pp. 53–58.

Setting

Fix $\theta>1$. Industry demand is low or high, each with probability $1/2$. If the retailers hold a total stock $q$, the market clearing price is

$$p_l(q)=(1-q)^+\ \text{(low state)},\qquad p_h(q)=\Big(1-\frac q\theta\Big)^+\ \text{(high state)}.$$

Leftover inventory has no salvage value, and the supplier's production cost is zero.

• Monopolist benchmark. A single firm orders a stock $Q$, observes the state, and sells $x_l\le Q$ (low) or $x_h\le Q$ (high) at the market clearing price. Its expected profit is $\tfrac12p_l(x_l)x_l+\tfrac12p_h(x_h)x_h$, and $\Pi^o$ is the maximum of this.
• Wholesale price contract. The supplier charges $w$ per unit. A continuum of retailers orders before demand is known and sells everything at the market clearing price. Their aggregate expected profit is

$$\pi(q)=\tfrac12p_l(q)q+\tfrac12p_h(q)q-wq .$$

Perfect competition means the retailers keep ordering until expected profit is zero. The competitive order is the $q>0$ with $\pi(q)=0$ and $\pi>0$ on $(0,q)$. The supplier earns $wq$.

• Resale price maintenance $(\bar p,w)$: retailers may not sell below $\bar p$. When the clearing price would fall below $\bar p$, only the demand at $\bar p$ is sold, allocated in proportion to stock.
• Buy-back $(w,b)$: the supplier pays $b$ per unsold unit. The market price then cannot fall below $b$, and retailers sell at most $1-b$ units (low) and $\theta(1-b)$ units (high).

The page's notation $q_1(w)=\frac{2\theta}{1+\theta}(1-w)$, $q_2(w)=\theta(1-2w)$, $\pi_s(w)$ and $w^*(\theta)$ is kept in Lean under the names q1, q2, supplierProfit, wStar.

Formalization targets

Goal (pp. 55, 57)

With

$$\pi_s^*=\begin{cases}\dfrac{\theta}{2(1+\theta)}&\theta\le3,\\[4pt]\dfrac\theta8&\theta>3,\end{cases}$$

the goal states four things:

1. $\pi_s^*$ is the greatest supplier profit $wq$ over all wholesale prices and their competitive orders.
2. $w^*(\theta)$ attains it.
3. The monopolist's maximum is $\Pi^o=(1+\theta)/8$, and $\pi_s^*<\Pi^o$.
4. Under the buy-back $b=w=1/2$ the competitive order is $\theta/2$ and the supplier earns exactly $\Pi^o$.

Milestones

1. $\Pi^o=(1+\theta)/8$ (p. 54).
2. The competitive order is $q_1(w)$ if $w\ge\tfrac12-\tfrac1{2\theta}$ and $q_2(w)$ otherwise, for $0\le w<1$ (p. 55).
3. $w^*(\theta)$ maximizes $\pi_s$ on $[0,1)$, with the value $\pi_s^*$ (p. 55).
4. The orders and market clearing prices at $w^*(\theta)$ (p. 55).
5. Under resale price maintenance with $\bar p=1/2$ and total stock $\theta/2$, $\pi_r(t)=q(t)\big(\frac{1+\theta}{4\theta}-w\big)$ (p. 56).
6. Under $(\bar p,\bar w)$ the competitive order is $\theta/2$ and the supplier earns $\Pi^o$ (p. 57).
7. Under the buy-back $b=1/2$ the retailers' profit is $q\big(\frac34-w-\frac q{2\theta}\big)$ for $1/2<q<\theta/2$ (p. 57).
8. $1/2>(1+\theta)/(4\theta)$ (p. 57).

Significance

The goal shows that in this model a wholesale price contract always falls short of the integrated profit, whatever $\theta$. It also shows where the shortfall comes from: at the optimal wholesale price the low-state market price falls below the monopoly price $1/2$ (milestone 4). Restoring the monopoly profit therefore requires a mechanism that holds the low-state price at $1/2$. Resale price maintenance and a full-refund buy-back both do this, so the section gives a closed-form efficiency argument for vertical restraints that are often treated as anticompetitive. The section also contrasts the buy-back with revenue sharing, which coordinates the single newsvendor (§6.2) but not this model.

The results are proved on the printed pages by elementary algebra. None of them has a machine-checked proof, and nothing on Prove2Me covers this model. The mission produces checked versions of the case analysis, including the $\theta=3$ tie and the two regimes of the competitive order. It also adds a reusable encoding of "perfect competition" as the first zero of aggregate expected profit.

Difficulty

Every statement reduces to one-variable inequalities, but the case structure is easy to get wrong.

• The retailers' profit is piecewise (prices hit zero at $q=1$ in the low state and at $q=\theta$ in the high state). The competitive order lies on either side of $q=1$ depending on $w$.
• The supplier's profit $\pi_s$ is piecewise in $w$, and its second branch peaks at $w=1/4$ only when $\theta>2$.
• The global optimum switches at $\theta=3$, where both prices are optimal.
• A statement "the competitive order is $q_1(w)$" needs the order to exist, to be unique, and to have positive profit everywhere below it. Exhibiting a root is not enough.
• The buy-back profit is identically zero for $q\ge\theta/2$ when $b=w=1/2$. Only the "first zero" reading of perfect competition pins the order at $\theta/2$.

Formalization scope

All quantities are real numbers and $\theta>1$ throughout. The continuum of retailers enters only through the total order. No measure space of retailers is formalized, and footnote 26's multiplicity of individual equilibria is not stated. The sales rules under resale price maintenance (proportional allocation) and under the buy-back (price floor $b$) are written into the contract definitions, as the page describes them in words. The theorems use only $\bar p=b=1/2$.

The formulas $q_1$, $q_2$, $\pi_s$ and $w^*$ are definitions transcribed from the page. That they are the competitive order and the optimum is the content of the theorems. Defining $\Pi^o$ or the competitive order by its closed form would trivialize the mission, so the competitive order is defined only by the zero-profit property and $\Pi^o$ as a greatest element of the monopolist's feasible profits. The goal is stated over all real wholesale prices, so it also rules out profitable prices outside $[0,1)$. Uniqueness of $w^*(\theta)$ is not asserted at $\theta=3$.

The chapter's standing assumptions used here are risk neutrality and full information, together with the model paragraph of pp. 53–54 (two equally likely states, zero salvage value, zero production cost). No platform definition is referenced: no published item formalizes this model.

Selected references

• G. P. Cachon, Supply Chain Coordination with Contracts, in S. Graves, T. de Kok (eds.), Handbooks in Operations Research and Management Science, Vol. 11: Supply Chain Management, North-Holland, 2003, §6.5.2 (3rd draft, January 2003, pp. 53–58). https://doi.org/10.1016/S0927-0507(03)11006-7
• R. Deneckere, H. P. Marvel, J. Peck, Demand Uncertainty and Price Maintenance: Markdowns as Destructive Competition, American Economic Review 87(4), 619–641, 1997. https://www.jstor.org/stable/2951366
• R. Deneckere, H. P. Marvel, J. Peck, Demand Uncertainty, Inventories, and Resale Price Maintenance, Quarterly Journal of Economics 111(3), 885–913, 1996. https://doi.org/10.2307/2946675

Why effort breaks the standard coordinating contracts

A supplier selling through a retailer earns more when the retailer works harder at selling. Examples are a better shelf position, more knowledgeable sales staff, local advertising and keeping the display in order. These activities cost the retailer, raise demand, and usually cannot be observed or verified by the supplier, so no contract can be written on them directly. Chapter 6 of the Handbook of Operations Research and Management Science, Vol. 11: Supply Chain Management (G. P. Cachon, Supply Chain Coordination with Contracts, 2003) surveys contracts that align a retailer's decisions with the interest of the whole supply chain. Its §6.4 asks which of these contracts survive when the retailer also chooses such an unverifiable effort level.

The question goes back to the marketing literature on retail effort (Chu and Desai 1995, Desai and Srinivasan 1995, Desiraju and Moorthy 1997, Lal 1990, Lariviere and Padmanabhan 1997). It was taken up for newsvendor contracts by Taylor (2000), who showed that a sales rebate combined with a buy back restores coordination, and by Krishnan, Kapuscinski and Butz (2001), who let effort be chosen after demand is observed. This mission is the third in a series that formalizes the chapter's section capstones. It covers §6.4.1.

The newsvendor with effort-dependent demand

One supplier sells to one retailer for a single selling season. Before the season the retailer chooses an order quantity $q \ge 0$ and an effort level $e \ge 0$. Effort costs him $g(e)$, where $g(0) = 0$, $g' > 0$ and $g'' > 0$. Demand $D$ given effort $e$ has distribution function $F(\cdot \mid e)$ on $[0, \infty)$, with $F(0 \mid e) = 0$ and $F(\cdot \mid e)$ strictly increasing. Demand is stochastically increasing in effort: $\partial F(y \mid e)/\partial e < 0$ for $y > 0$. Units sell at the retail price $p$ and cost $c < p$ to produce. Goodwill costs, the salvage value and the retailer's own unit cost are zero. Expected sales and the integrated channel's profit are

$$S(q, e) = \mathbb E[\min(q, D)] = q - \int_0^q F(y \mid e)\,dy, \qquad \Pi(q, e) = pS(q, e) - cq - g(e).$$

Let $(q^o, e^o)$ maximize $\Pi$. A contract fixes the transfer the retailer pays the supplier, as a function of what the supplier can verify: the order and, for some contracts, sales or leftover units, but never effort. The contracts compared are the buy back $\{w_b, b\}$, quantity flexibility $\{w_q, \delta\}$, revenue sharing $\{w_r, \phi\}$, the sales rebate $\{w_s, r, t\}$ and the quantity discount $w_d(q)$. Under each, the retailer's profit $\pi_r(q, e)$ is his revenue $pS(q, e)$ less the transfer and $g(e)$.

Formalization targets

Goal

The goal combines the section's negative and positive results.

1. Buy backs distort effort (Eq. (19)). For every $b > 0$, $q > 0$ and $e > 0$,

$$\frac{\partial \pi_r(q, e, w_b, b)}{\partial e} < \frac{\partial \Pi(q, e)}{\partial e}.$$

2. The quantity discount aligns effort and splits profit. With

$$w_d(q) = (1 - \lambda)p\,\frac{S(q, e^o)}{q} + \lambda c - (1 - \lambda)\frac{g(e^o)}{q}, \qquad \lambda \in [0, 1],$$

the following hold for every $q > 0$. The retailer earns $\pi_r(q, e^o) = \lambda\Pi(q, e^o)$ and the supplier earns $(1 - \lambda)\Pi(q, e^o)$. The retailer's marginal profit of effort equals the channel's. His optimal efforts are the channel's. 3. The optimal order. If $(q^o, e^o)$ maximizes $\Pi$, both firms' profits at effort $e^o$ are maximized by $q^o$.

Milestones

The milestones follow the section's own claims: the integral form of $S$ (p. 41); the first-order condition (18) for the chain-optimal effort; (19); the analogous strict inequalities for quantity flexibility ($\delta > 0$) and revenue sharing ($\phi < 1$), and the reverse inequality for the sales rebate ($r > 0$, $q > t$); the two displays of $\pi_r$ under the quantity discount; and the fact that $S(q, e)/q$ decreases in $q$.

Significance

The result separates two jobs a contract does. To coordinate the order quantity, buy backs, quantity flexibility and revenue sharing all shield the retailer from part of the demand risk or take part of his revenue. The same shield dulls his incentive to raise demand, so each one leads him to under-invest in effort. The sales rebate pushes the other way, toward too much effort. The quantity discount works because the retailer keeps every unit of realized revenue and bears all of his own effort cost. The schedule then prices the order against expected revenue at the optimal effort, so the order is coordinated without touching the effort incentive. Because $\pi_r(q, e^o) = \lambda\Pi(q, e^o)$ with $\lambda$ free in $[0, 1]$, any split of the channel's optimal profit is attainable. The chapter extends this observation to retailers that also set price (p. 43).

The section's claims are proved on the page only in outline; several are introduced with "it can be shown". To our knowledge none has a machine-checked proof. Formalizing them requires differentiating expected sales in a parameter of the demand law. That step recurs throughout stochastic inventory and pricing models.

Difficulty

Most of the algebra is short. The substance is in the derivatives. $\partial S(q, e)/\partial e = -\int_0^q \partial F(y \mid e)/\partial e\,dy$ is a differentiation under the integral sign. The strict inequalities need this integral to be strictly negative. That in turn needs $\partial F/\partial e$ to be integrable and negative on a set of positive length, which is why $q > 0$ (and $q > t \ge 0$ for the sales rebate) matters.

The natural reading "the quantity discount makes $(q^o, e^o)$ the retailer's joint optimum" is not what the page shows, and it fails in general. The page gives two partial statements: for each fixed $q$ the retailer's effort incentive is the chain's, and at $e = e^o$ his best order is $q^o$. Since $\pi_r(q, e) = \Pi(q, e) - (1 - \lambda)\Pi(q, e^o)$, the retailer can gain by moving $q$ and $e$ together when $\lambda$ is small. The goal states exactly the two partial claims.

Formalization scope

The Lean namespace is CachonCoord.EffortNewsvendor. A structure Model collects the data: $p$ and $c$ with $0 \le c < p$; a family of demand laws indexed by effort (probability measures on $[0, \infty)$ with finite mean, no atom at $0$, strictly increasing distribution function); the effort derivative $\partial F(y \mid e)/\partial e$, negative for $y > 0$, $e > 0$; and $g$ with $g(0) = 0$ and positive first and second derivatives for $e > 0$. $S$ is defined as an expectation, and its integral form is a milestone. Derivative claims are HasDerivAt statements at interior efforts $e > 0$. The inequalities assert that both derivatives exist.

The following hypotheses are standing assumptions or disclosed additions:

• the chapter's model paragraph (p. 7) and the zeros $g_r = g_s = v = c_r = 0$ of p. 41;
• as regularity, differentiation of $e \mapsto \int_a^b F(y \mid e)\,dy$ under the integral sign, with interval-integrable $\partial F/\partial e$;
• $0 \le c$ (a production cost);
• $w_q > 0$ and $\delta \le 1$ for quantity flexibility (the contract's range, p. 24);
• $t \ge 0$ for the sales rebate threshold;
• $q > 0$ wherever $w_d$, which divides by $q$, is used.

Revenue sharing and the sales rebate use §6.2's profit functions (pp. 21, 27) with this section's zeros, less $g(e)$.

The page prints the last term of $w_d$ as $+(1 - \lambda)g(e^o)/q$. With that sign the page's own displays $\pi_r(q, e^o) = \lambda\Pi(q, e^o)$ and $\pi_r(q, e)$ fail by $2(1 - \lambda)g(e^o)$. The formalization uses $-(1 - \lambda)g(e^o)/q$, under which both hold. $w_d$ is the explicit printed schedule with this correction. It is not defined as "a schedule with $\pi_r = \lambda\Pi$", which would make the goal empty.

Not covered: the price-and-effort schedule at the bottom of p. 43, for which the page gives no argument. The cachon-2005 revenue-sharing effort results (RevShareCoord.Effort.*, deterministic revenue $R(q, e)$) are a different model and are not referenced. Proofs of any milestone, and a reusable library for differentiating newsvendor expectations in a parameter, are welcome.

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 (read in the author's 3rd draft, January 2003).
• T. A. Taylor, Supply Chain Coordination under Channel Rebates with Sales Effort Effects, Management Science 48(8), 2002, 992–1007. https://doi.org/10.1287/mnsc.48.8.992.168
• H. Krishnan, R. Kapuscinski, D. A. Butz, Coordinating Contracts for Decentralized Supply Chains with Retailer Promotional Effort, Management Science 50(1), 2004, 48–63. https://doi.org/10.1287/mnsc.1030.0154
• G. P. Cachon, M. A. Lariviere, Supply Chain Coordination with Revenue-Sharing Contracts: Strengths and Limitations, Management Science 51(1), 2005, 30–44. https://doi.org/10.1287/mnsc.1040.0215

Motivation

Strictly convex quadratic programs — minimize a positive definite quadratic subject to linear inequalities — are the subproblems solved at every iteration of successive quadratic programming (SQP) methods for nonlinear optimization, and they arise directly in least-squares estimation with constraints, portfolio selection and model predictive control. In SQP the unconstrained minimizer of the quadratic model is available at no cost, while a feasible point is not.

D. Goldfarb and A. Idnani (Math. Programming 27 (1983) 1–33) proposed a dual active-set method that exploits this asymmetry. It starts at the unconstrained minimizer, which is optimal for the problem with all constraints removed, and adds violated constraints one at a time while keeping the current point optimal for the subproblem defined by the current active set. No phase 1 is needed. The method, usually called the Goldfarb–Idnani algorithm, is the basis of widely used solvers (for example the quadprog package in R and QuadProg++), and the paper proves that it terminates finitely with a correct answer.

Earlier dual methods for quadratic programming include the modified-simplex methods of Lemke (Management Science 8 (1962) 442–453) and of Van de Panne and Whinston (1964), which the paper compares with its own in Section 7.

Setting

Fix $n, m \in \mathbb N$, a vector $a \in \mathbb R^n$, a symmetric positive definite $n\times n$ matrix $G$, an $n\times m$ matrix $C$ with columns $n_1,\dots,n_m$, and $b \in \mathbb R^m$. The quadratic program (1.1) is

$$\min_x\ f(x) = a^{\mathsf T}x + \tfrac12 x^{\mathsf T}Gx \quad\text{subject to}\quad s_i(x) = n_i^{\mathsf T}x - b_i \ge 0,\quad i \in K = \{1,\dots,m\}.$$

The gradient is $g(x) = Gx + a$. For $J \subseteq K$, the subproblem $P(J)$ keeps only the constraints indexed by $J$; $P(\emptyset)$ is solved by $x^0 = -G^{-1}a$. A set $A \subseteq K$ is linearly independent if the normals $n_i$, $i\in A$, are.

For an independent $A$, let $N$ be the matrix with columns $n_i$, $i\in A$, and define

$$N^* = (N^{\mathsf T}G^{-1}N)^{-1}N^{\mathsf T}G^{-1},\qquad H = G^{-1} - G^{-1}N(N^{\mathsf T}G^{-1}N)^{-1}N^{\mathsf T}G^{-1}.$$

The multipliers are $u(x) = N^*g(x)$; for a constraint $p \notin A$ with normal $n^+ = n_p$ the infeasibility multipliers are $r = N^*n^+$; a superscript $+$ denotes the same objects for $A^+ = A\cup\{p\}$.

An S-pair $(x, A)$ is an independent active set $A$ with $s_i(x) = 0$ for $i\in A$ and $x$ optimal for $P(A)$. A V-triple $(x, A, p)$ has $p\notin A$, $A^+$ independent, $s_p(x) < 0$, $s_i(x) = 0$ for $i \in A$, $H^+g(x) = 0$ and $u^+(x) = (N^+)^*g(x) \ge 0$.

The dual algorithm starts from $(x^0, \emptyset)$. In Step 1 it stops if $x$ is feasible; otherwise it picks any violated constraint $p$. In Step 2 it moves along the primal direction $z = Hn^+$ and the dual direction $(-r; 1)$ with step $t = \min\{t_1, t_2\}$, where $t_1$ is the largest step that keeps the multipliers nonnegative and $t_2 = -s_p(x)/z^{\mathsf T}n^+$ makes constraint $p$ active. If both are infinite it reports infeasibility. A full step ($t = t_2$) adds $p$ and returns to Step 1. A partial step ($t = t_1 < t_2$), or a dual step ($z = 0$), drops a constraint $k$ attaining $t_1$ and repeats Step 2.

Formalization targets

Goal: Theorem 3 (p. 11)

For every choice of the violated constraint $p$ and of the dropped constraint $k$:

$$\text{no run from } (x^0,\emptyset) \text{ is infinite, and every run that cannot continue ends in } \begin{cases}\text{STOP at an optimal } x \text{ of (1.1)}, \text{ or}\\ \text{STOP with } \{x : C^{\mathsf T}x \ge b\} = \emptyset.\end{cases}$$

Milestones, in attack order

1. Properties (2.6)–(2.9) (p. 5): $Hw = 0 \iff w \in \operatorname{range} N$; $H \succeq 0$; $HGH = H$; $N^*GH = 0$.
2. Optimality conditions (2.3)–(2.4) (p. 5): on the manifold of $A$, $x$ solves $P(A)$ iff $N^*g(x) \ge 0$ and $Hg(x) = 0$.
3. Lemma 1 (p. 8): along $\bar x = x + tHn^+$ from a V-triple, $H^+g(\bar x) = 0$, the constraints of $A$ stay active, $u^+(\bar x) = u^+(x) + t(-r;1)$ and $s_p(\bar x) = s_p(x) + t\,z^{\mathsf T}n^+$.
4. Theorem 1 (pp. 8–9): the step $t = \min\{t_1,t_2\}$ increases $s_p$ and $f$; a partial step yields a V-triple, a full step an S-pair.
5. Theorem 2 (p. 10): if $n_p = Nr$ and $s_p(x) < 0$ at an S-pair, then $r \le 0$ means $P(A\cup\{p\})$ is infeasible; otherwise dropping a minimizing $k$ gives a V-triple.
6. One round of Step 2 (p. 11): from an S-pair and a violated $p$, at most $|A|$ partial or dual steps and one final step end either in infeasibility of (1.1) or in a new S-pair $(\bar x, \bar A \cup\{p\})$ with $\bar A\subseteq A$ and $f(\bar x) > f(x)$.

Significance

Theorem 3 is the correctness certificate of the Goldfarb–Idnani method: whatever rule an implementation uses to choose the entering and leaving constraints, it cannot cycle and its answer is right. In particular the infeasibility verdict is a proof that (1.1) has no feasible point, which matters in SQP where infeasible subproblems trigger a different branch of the outer method. The intermediate results (the operator identities, Lemma 1, Theorems 1–2) are the standard analysis of dual active-set methods for quadratic programming.

The result is proved in the paper; to our knowledge it has not been machine-checked. A formal development produces verified projector identities for $N^*$ and $H$, a verified KKT characterization for equality-active subproblems, and a verified finite-termination proof for a nondeterministic algorithm with an explicit step relation. The platform already has a proved KKT sufficiency theorem for general convex programs (ConvexOptimization.kkt_sufficient_for_convex), stated over EuclideanSpace with general convex functions and gradient fields; it can serve as background for the sufficiency half of milestone 2, but it is not stated in this mission's matrix objects.

Difficulty

The obvious termination argument is that $f$ increases strictly at every iteration and there are finitely many active sets. It fails as stated: partial steps may leave $x$ unchanged (the dual steps of Step 2(c)(ii)), so $f$ is only nondecreasing between consecutive states. A termination proof therefore needs a measure that also decreases along steps that do not move $x$. Any such argument relies on invariants (independence of $A^+$, nonnegativity of the multipliers, $s_p < 0$ along partial steps) that hold only on reachable states, and the operators $N^*$ and $H$ are meaningful only while those invariants hold. Correctness of the infeasibility verdict requires the dependent case (Theorem 2), not only Theorem 1.

Formalization scope

Vectors are Fin n → ℝ, $G$ is Matrix (Fin n) (Fin n) ℝ with G.PosDef, $C$ is Matrix (Fin n) (Fin m) ℝ, and active sets are Finset (Fin m). Multiplier vectors are indexed by constraint index (Fin m → ℝ, zero off the active set), not by position in $A$. Lean's matrix inverse returns $0$ for singular matrices, so every statement about $N^*$ and $H$ assumes $G \succ 0$ and an independent active set (directly, or through an S-pair or V-triple).

The algorithm is the inductive relation Step on states step1 x A u, step2 x A p u⁺, stopOptimal x, stopInfeasible, with one transition per admissible choice of $p$ and $k$. Infinite step lengths are separate transitions; a tie $t_1 = t_2$ takes the full step, as the paper tests $t = t_2$ first. The running value of $f$ and the factorizations of Section 4 are not part of the state.

Explicit readings of the paper's words:

• "solves the QPP or indicates infeasibility in a finite number of steps" is: no infinite sequence of Step transitions from the Step-0 state, and every reachable state without a successor is a STOP whose verdict is correct (optimal for (1.1), or (1.1) infeasible);
• "S-pair" is: $A$ independent and active at $x$, with $x$ optimal for $P(A)$ (the reading every use in the paper needs);
• in Theorem 1 the partial-step clause carries $t < t_2$ (as in its proof), and the multiplier printed $u^+_{j+1}$ in (3.16) is $u^+_{q+1}$, the entry belonging to $p$;
• "an S-pair can never reoccur" is expressed as the strict increase $f(\bar x) > f(x)$ in milestone 6.

Property (2.10), printed $HH^+ = H^+$, is false unless $G = I$ and is not formalized. Equality constraints (1.2), Section 4 (numerically stable implementation), Sections 5–6 (computations), Section 7 (comparisons) and the Appendix example are out of scope.

A trivializing formalization is ruled out: the goal quantifies over every run of the relation (not one selection rule, not "some run terminates"), the infeasibility verdict is about (1.1) itself, and the algorithm is a relation that always has a successor until a STOP, so correctness cannot hold because a run gets stuck.

Needed infrastructure: Schur-complement and projector identities for $N^*$ and $H$; first-order optimality for convex quadratics on affine subspaces with inequality multipliers; well-foundedness arguments for a nondeterministic relation. The operator identities and the KKT characterization are reusable for other active-set and SQP analyses. Contributions of proofs of any milestone, and of reusable lemmas about $N^*$ and $H$, are welcome.

Selected references

• D. Goldfarb and A. Idnani, A numerically stable dual method for solving strictly convex quadratic programs, Mathematical Programming 27 (1983) 1–33. https://doi.org/10.1007/BF02591962
• C. E. Lemke, A method of solution for quadratic programs, Management Science 8 (1962) 442–453. https://doi.org/10.1287/mnsc.8.4.442
• J. Nocedal and S. J. Wright, Numerical Optimization, 2nd ed., Springer, 2006, Chapter 16. https://doi.org/10.1007/978-0-387-40065-5

Motivation

Minimum-cost circulation asks how to route flow around a directed network without accumulating flow at any vertex, while minimizing the total cost of the routed units. It is a basic network optimization problem: lower-bound and demand constraints in many flow models can be converted into circulation form. Goldberg and Tarjan's 1987 technical report develops a successive-approximation approach in which a local repair subroutine, refine, improves an approximately optimal circulation. The report was followed by a 1990 journal article; all theorem numbers and page citations in this mission refer to the 1987 report.

The mission isolates the generic form of refine, where an implementation may choose any applicable update at each step. Its question is whether every such choice sequence finishes after a controlled number of operations and returns a circulation with a stronger optimality certificate. The related Goldberg–Tarjan maximum-flow algorithm uses push and relabel operations with distance labels; here the labels are real-valued prices tied to arc costs. The authors' cycle-canceling work uses the same circulation network model and supplies published definitions reused in this development.

Setting

A circulation network has a finite vertex set $V$ and a symmetric set $E$ of directed arcs: whenever $(v,w)$ is an arc, so is $(w,v)$. Let $n=|V|$ and $m=|E|$, counting both orientations. Each arc has a real capacity $u(v,w)$ and cost $c(v,w)$, with $c(v,w)=-c(w,v)$. A pseudoflow $f$ respects capacities and the paired-arc relation $f(v,w)=-f(w,v)$. Its excess $e_f(v)$ is the sum of flow entering $v$. A circulation is a pseudoflow with zero excess everywhere. The already published CycleCanceling.MinMean.Network supplies this network, its circulation predicate, and residual capacity $u_f(v,w)=u(v,w)-f(v,w)$. An arc is residual when this capacity is positive.

A price function $p:V\to\mathbb R$ changes an arc's reduced cost to $c_p(v,w)=c(v,w)-p(v)+p(w)$. A pseudoflow is $\varepsilon$-optimal with respect to $p$ when every residual arc has reduced cost at least $-\varepsilon$. A vertex is active when its excess is positive. An admissible arc is a residual arc of negative reduced cost. Refine takes an input circulation that is $2\varepsilon$-optimal, saturates every arc whose reduced cost is negative, and then repeatedly applies an available update. A push sends flow from an active vertex along an admissible arc. A relabel raises the price of an active vertex with no outgoing admissible arc to the largest value permitted by $\varepsilon$-optimality. These rules are Figures 4 and 5, printed pages 18–19.

Formalization targets

The supporting targets are the paper's progress and correctness results, its price bound, and the three operation counts. For any generic refine run from a $2\varepsilon$-optimal circulation, Lemma 5.8 bounds each vertex's price increase by $3n\varepsilon$. Lemmas 5.9–5.11 bound the numbers $R,S,T$ of relabelings, saturating pushes, and nonsaturating pushes:

$$R\leq 3n(n-1),\qquad S\leq 3nm,\qquad T\leq 3n^2(m+n).$$

The goal combines the resulting bound on the number $K$ of updates with progress and correctness:

$$K\leq 3n(n-1)+3nm+3n^2(m+n).$$

If the final state has an active vertex, another update exists. If no update applies, the final pseudoflow is a circulation and is $\varepsilon$-optimal with respect to its final prices. This is the explicit operation-count content behind the generic subroutine's analysis in Section 5. It does not claim a bound for a particular data structure or a complete minimum-cost algorithm.

Significance

The theorem gives an order-independent finite bound: the choice of which applicable push or relabel to perform cannot cause generic refine to run forever or stop with an active vertex. Its output is a circulation whose approximate-optimality tolerance has been halved. That output can serve as the next input in the successive-approximation framework. For integral costs, the report's Theorem 2.3 later turns a sufficiently small tolerance into exact minimum cost; that outer-loop result is outside this mission.

This mission specifies the generic cost-scaling state machine in Lean and poses its quantitative analysis as open formalization targets. The shared network and circulation definitions from the published Goldberg–Tarjan 1989 series are available, and a related generic maximum-flow theorem in the 1988 series has a machine-checked proof. Those results do not prove refine's price-based bounds. Contributions that establish the paper's progress, price, or counting statements for this state machine, and reusable facts about finite residual networks, advance the open goal.

Difficulty

A push respects a capacity, but it can create activity at another vertex; a relabel changes which arcs are admissible. Thus checking a single update does not bound an arbitrary sequence. The price bound also depends on the circulation and prices supplied at entry, not merely on the current pseudoflow being $\varepsilon$-optimal. Finally, a vertex with no admissible outgoing arc may appear to be stuck when the relabel minimum is over an empty set. Feasibility of the original circulation network is needed to establish that an active vertex still has a genuine next update. The operation bound requires accounting for the three update types across every possible choice sequence.

Formalization scope

Vertices form a finite type, and capacities, costs, flows, and prices are real-valued functions. The network has symmetric ordered arcs and antisymmetric costs. There is no separate nonnegativity assumption on capacities; feasibility is supplied by the input circulation. The new $\varepsilon$ is positive, so the entry circulation is $2\varepsilon$-optimal before Figure 4 halves the error parameter. The run starts from the resulting saturated pseudoflow and records one applicable push or relabel per index $k<K$. Counts classify those actual steps by the selected arc's residual capacity after a push. Termination is the negation of the paper's loop guard, not a definition that assumes zero excess.

The reduced-cost sign is $c-p(v)+p(w)$, and relabel raises $p(v)$. This differs from the published 1989 epsilon-optimality definition, so only its network model is imported. The relabel relation requires an attained minimum over a nonempty set of outgoing residual arcs; it assigns no default value to an empty minimum. Loops may occur in the reused network model, but cost antisymmetry makes their reduced cost zero, so they cannot be push arcs. The explicit constants are the report's $3n\varepsilon$, $3n(n-1)$, $3nm$, and $3n^2(m+n)$; the goal sums the last three. The report's RAM-model $O(\cdot)$ running times are outside the formal statements. A definition that makes termination equivalent to conservation or assigns an arbitrary relabel price at an empty set would miss the target.

Selected references

• Andrew V. Goldberg and Robert E. Tarjan, Finding Minimum-Cost Circulations by Successive Approximation, MIT/LCS/TM-333, July 1987. Technical report.
• Andrew V. Goldberg and Robert E. Tarjan, Finding Minimum-Cost Circulations by Successive Approximation, Mathematics of Operations Research 15(3), 1990, pp. 430–466. DOI. The report above supplies this mission's numbering.
• Andrew V. Goldberg and Robert E. Tarjan, A New Approach to the Maximum-Flow Problem, Journal of the ACM 35(4), 1988. DOI.
• Andrew V. Goldberg and Robert E. Tarjan, Finding Minimum-Cost Circulations by Canceling Negative Cycles, Journal of the ACM 36(4), 1989. DOI.