Operations Research

Motivation

The periodic-review inventory problem with a fixed ordering cost is one of the basic models of operations research. A firm reviews its stock once per period, may order at a cost $K$ per order plus a unit cost, and then faces a random demand; unmet demand is backlogged. Scarf (1960) and Iglehart (1963) showed that for this model an $(s, S)$ policy is optimal: order up to $S$ whenever the stock falls below $s$, and otherwise do nothing. That result tells a manager what shape a good policy has, but not which pair $(s, S)$ to use.

Veinott and Wagner, Computing Optimal (s, S) Inventory Policies (Management Science 11 (1965) 525–552), gave the first practical algorithm for computing an optimal pair when demand is discrete. The algorithm rests on a closed form, their Eq. (11), for the discounted cost of an arbitrary stationary $(s, S)$ policy, obtained by a renewal argument in their Section 3. The same closed form, in the undiscounted limit, is the classical expression of the long-run average cost of an $(s, S)$ policy used throughout inventory theory textbooks.

Timeline:

• 1958: Arrow, Karlin and Scarf collect the early dynamic inventory models.
• 1960: Scarf proves optimality of $(s, S)$ policies in the finite-horizon model via $K$-convexity.
• 1963: Iglehart extends optimality to the infinite-horizon model.
• 1965: Veinott and Wagner derive the renewal closed form (10)–(11) and the bounds and search procedure built on it.

Setting

Demands $\xi_1, \xi_2, \dots$ are independent random variables on $\{0, 1, 2, \dots\}$ with common distribution $\varphi$, $\varphi(k) = \Pr(\xi_t = k)$. Write $\varphi^i$ for the $i$-fold convolution of $\varphi$ ($\varphi^0$ is the point mass at $0$) and $\Phi^i(k) = \sum_{t=0}^{k}\varphi^i(t)$ for its distribution function, so $\Phi^0 \equiv 1$.

In period $t$ the stock before ordering is $X_t \in \mathbb Z$ and the stock after ordering is $Y_t \ge X_t$; then $X_{t+1} = Y_t - \xi_t$. With the unit purchase cost eliminated as in the paper's Eq. (2), the cost of period $t$ is $K\delta(Y_t - X_t) + G_\alpha(Y_t)$, where $K \ge 0$ is the set-up cost, $\delta(0) = 0$, $\delta(z) = 1$ for $z > 0$, and $G_\alpha : \mathbb Z \to \mathbb R$ is the one-period cost. Period $t$ is discounted by $\alpha^{t-1}$ with $0 \le \alpha < 1$.

A stationary $(s, S)$ policy, for integers $s \le S$, sets $Y_t = S$ if $X_t < s$ and $Y_t = X_t$ otherwise. Its total expected discounted cost from $X_1 = x$ is

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

and its equivalent cost per period is $a_\alpha(x \mid s, S) = (1 - \alpha) f(x \mid s, S)$.

The renewal quantities are

$$m_\alpha(k) = \sum_{i=1}^{\infty}\alpha^i\varphi^i(k), \qquad M_\alpha(k) = \sum_{i=1}^{\infty}\alpha^i\Phi^i(k),$$

the latter being the discount renewal function,

$$L_\alpha(x, d) = G_\alpha(x) + \sum_{i=1}^{\infty}\sum_{k=0}^{d}\alpha^i G_\alpha(x - k)\varphi^i(k), \qquad r_\alpha(d) = \sum_{i=1}^{\infty}\alpha^i\bigl[\Phi^{i-1}(d) - \Phi^i(d)\bigr].$$

If $T(d)$ is the first period in which cumulative demand exceeds $d$, then $L_\alpha(x, d)$ is the expected discounted one-period cost over periods $1, \dots, T(d)$ from stock $x$ without ordering, and $r_\alpha(d) = E[\alpha^{T(d)}]$.

Formalization targets

Goal: Eq. (11)

With $D = S - s$,

$$a_\alpha(x \mid s, S) = \begin{cases} \dfrac{L_\alpha(S, D) + K}{1 + M_\alpha(D)} & x < s, \\[2ex] (1 - \alpha)L_\alpha(x, x - s) + \dfrac{L_\alpha(S, D) + K}{1 + M_\alpha(D)}\, r_\alpha(x - s) & x \ge s. \end{cases}$$

Milestones

1. Appendix §1: $M_\alpha(k) < \infty$ for $0 \le \alpha \le 1$ with $\alpha\varphi(0) < 1$.
2. Eq. (8): $L_\alpha(x, d) = G_\alpha(x) + \sum_{j=0}^{d} G_\alpha(x - j)m_\alpha(j)$.
3. Eq. (9): $r_\alpha(d) = \alpha - (1 - \alpha)M_\alpha(d)$.
4. The renewal equation $f(S) = L_\alpha(S, D) + Kr_\alpha(D) + f(S)r_\alpha(D)$.
5. $f(x) = K + f(S)$ for $x < s$.
6. $f(x) = L_\alpha(x, x - s) + Kr_\alpha(x - s) + f(S)r_\alpha(x - s)$ for $x \ge s$.
7. Eq. (10): the closed form of $f$ with denominator $1 - r_\alpha(D)$.

Significance

Eq. (11) turns the cost of an $(s, S)$ policy, an infinite series over the trajectories of a controlled Markov chain, into a finite expression in $G_\alpha$, $K$ and the renewal sequence $m_\alpha$, which the paper computes by a one-line recursion. Everything in the paper's Section 4 builds on it: the search for an optimal pair minimizes $a_\alpha(\cdot \mid s, S)$ over a finite box, and the undiscounted limit $\alpha \to 1$ gives the long-run average cost $(L_1(S, D) + K)/(1 + M_1(D))$.

The result is classical and proved in the paper. What this mission adds is a machine-checked derivation from the definition of the policy's expected cost, including the renewal step, which the paper states in one sentence ("a renewal of the process takes place"). It also produces a reusable Lean layer: discrete convolution powers, the discount renewal function, and the law of an $(s, S)$-controlled inventory chain. To the best of our knowledge none of these is formalized in Mathlib or on the platform.

Difficulty

The paper's argument conditions on the random time $T(D)$ at which the process renews and uses the strong Markov property at that time. In the formalization, $f$ is defined as a sum over periods of expectations under the law of $X_t$. Relating that sum to one that splits at the random time $T(D)$ requires either a stopping-time decomposition of the chain or an explicit accounting of the law of $X_t$ before and after the first order. Neither is a direct computation. A second difficulty is the interchange of the infinite sum over periods with the sum over states $y \in \mathbb Z$, which has infinitely many states reachable (demand is unbounded below). The renewal equation (milestone 4) alone does not determine $f(S)$ without the fact that $r_\alpha(D) < 1$ for $\alpha < 1$, which comes from (9).

Formalization scope

• Namespace VeinottWagnerSS.RenewalCost. Stock levels are integers, demands natural numbers; $x - s$ and $D = S - s$ enter $L_\alpha$, $M_\alpha$, $r_\alpha$ through Int.toNat, which is exact because the statements assume $s \le x$ or $s \le S$.
• Reduced model. The primitives are $G_\alpha$, $K$, $\alpha$ and $\varphi$, as in the paper's Eq. (2): the unit purchase cost is set to $0$ and the holding–penalty cost is replaced by $G_\alpha$.
• Demand is a real function $\varphi : \mathbb N \to \mathbb R$, non-negative and summing to $1$.
• The cost $f$ is the expected discounted cost of the controlled chain: the law of $X_t$ is built recursively from $X_1 = x$ and the transition $\Pr(X_{t+1} = z \mid X_t = y) = \varphi(Y(y) - z)$. It is not defined by (10) or by the renewal equations, and not as the solution of a fixed-point equation. A formalization in which any of milestones 4–7 or the goal holds by definition is ruled out.
• Series are real tsums. $L_\alpha$ is defined by the series (7) and $r_\alpha$ by the first line of (9), i.e. through the law $\Pr[T(d) = i] = \Phi^{i-1}(d) - \Phi^i(d)$; the paper's derivations of these series from $T(d)$ are not formalized. For $\alpha < 1$ all series converge for every $G_\alpha$, because after period $1$ the stock after ordering lies in the finite set $\{S\} \cup [s, \max(x, S)]$.
• Hypotheses. Milestones 1–3 assume $0 \le \alpha \le 1$ and $\alpha\varphi(0) < 1$, the paper's standing assumption on p. 533. Milestones 4–7 and the goal assume $0 \le \alpha < 1$, $K \ge 0$ and $s \le S$. The paper's standing assumptions that $G_\alpha$ is convex and tends to $+\infty$ as $|y| \to \infty$ are not imposed: the statements hold for every $G_\alpha$ when $\alpha < 1$, and the paper's derivation does not use them. This is a disclosed generalization.
• Printed slips. None found in the formalized statements.
• Not formalized: the recursion (A1) for $m_\alpha$, the limit (12) as $\alpha \to 1$, and the stationary analysis (13)–(20).

Contributions welcome: proofs of the milestones, general lemmas on discrete renewal sequences and convolution powers, and a first-passage decomposition for integer-valued Markov chains, which is reusable beyond this mission.

Selected references

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

Motivation

A variational inequality asks for a point of a convex set at which a vector field points "inward" against every feasible direction. The format covers the first-order optimality conditions of constrained optimization, nonlinear complementarity problems, traffic and economic equilibria (Wardrop, Walrasian, Nash–Cournot), and systems of nonlinear equations; see Harker and Pang's survey (Math. Programming 48, 1990) and Facchinei and Pang's monograph (Springer, 2003).

When the map has no special structure (not strongly monotone, not Lipschitz with known constant, not affine) and the feasible set is a general closed convex set, the practical algorithms are projection methods. The oldest is Korpelevich's extragradient method (1976). Without a known Lipschitz constant, extragradient-type methods need a linesearch in which every trial point costs one projection onto the feasible set, and projection onto a general convex set is itself an optimization problem.

Solodov and Svaiter (SIAM J. Control Optim. 37 (1999) 765–776) proposed a method that spends exactly two projections per iteration, whatever the linesearch does, and proved global convergence under only continuity of the map and a generalized monotonicity condition weaker than pseudomonotonicity. The method, often called the hyperplane projection method, is a standard reference point for later projection and extragradient-type algorithms.

Timeline:

• 1976: Korpelevich, extragradient method, Lipschitz monotone maps.
• 1987–1994: Khobotov (1987), Iusem (1994) and others: extragradient variants with Armijo-type stepsize rules, which need one projection per trial step.
• 1997: Iusem and Svaiter, a separating-hyperplane variant of extragradient for monotone maps (reference [9] of the paper).
• 1999: Solodov and Svaiter, Algorithm 2.1: two projections per iteration, convergence under condition (1.2) below.

Setting

Work in $\mathbb{R}^n$ with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. Let $C \subseteq \mathbb{R}^n$ be closed and convex and $F : \mathbb{R}^n \to \mathbb{R}^n$ continuous. The problem $\mathrm{VI}(F, C)$ is to find $x^*$ with

$$x^* \in C, \qquad \langle F(x^*), x - x^*\rangle \ge 0 \quad \text{for all } x \in C. \tag{1.1}$$

Its solution set is $S$. The projection onto a nonempty closed convex set $K$ is $P_K[x] := \arg\min_{y \in K}\|y - x\|$. The projected residual is $r(x) := x - P_C[x - F(x)]$; its zeros are exactly the points of $S$.

Condition (1.2) requires, for every $x^* \in S$,

$$\langle F(x), x - x^*\rangle \ge 0 \qquad \text{for all } x \in C. \tag{1.2}$$

It holds when $F$ is monotone or pseudomonotone, and in cases where $F$ is neither.

Algorithm 2.1. Fix $\gamma, \sigma \in (0,1)$ and $x^0 \in C$. Given $x^i$: if $r(x^i) = 0$, stop. Otherwise let $k_i$ be the smallest nonnegative integer $k$ with

$$\langle F(x^i - \gamma^k r(x^i)), r(x^i)\rangle \ge \sigma\|r(x^i)\|^2, \tag{2.1}$$

set $\eta_i = \gamma^{k_i}$, $z^i = x^i - \eta_i r(x^i)$, $H_i = \{x \mid \langle F(z^i), x - z^i\rangle \le 0\}$, and

$$x^{i+1} = P_{C \cap H_i}[x^i].$$

The hyperplane $\partial H_i$ separates $x^i$ from $S$.

Formalization targets

Goal: Theorem 2.1

If $C$ is closed and convex, $F$ is continuous, $S \ne \emptyset$ and (1.2) holds, then every sequence generated by Algorithm 2.1 converges to a single point of $S$:

$$\exists\, \hat x \in S:\quad x^i \to \hat x \quad (i \to \infty).$$

The theorem fixes no rate and no constant; it asserts convergence of the whole sequence, not only of a subsequence.

Milestones (in attack order)

• Lemma 2.1 (p. 768): for nonempty closed convex $B$, $\langle x - P_B[x], z - P_B[x]\rangle \le 0$ for $z \in B$, and $\|P_B[x]-P_B[y]\|^2 \le \|x-y\|^2 - \|P_B[x]-x+y-P_B[y]\|^2$.
• Residual characterization (p. 767): $x \in S \iff r(x) = 0$.
• (2.5) (p. 769): $\langle F(x), r(x)\rangle \ge \|r(x)\|^2$ for $x \in C$.
• Linesearch well-definedness (p. 769): for $x \in C$ with $r(x) \ne 0$, some $k$ satisfies (2.1).
• Lemma 2.2 (p. 768): $x^{i+1} = P_{C\cap H_i}[\bar x^i]$ with $\bar x^i = P_{H_i}[x^i]$.
• (2.6) (pp. 769–770): $\|x^{i+1}-x^*\|^2 \le \|x^i-x^*\|^2 - \|x^{i+1}-\bar x^i\|^2 - \big(\eta_i\sigma/\|F(z^i)\|\big)^2\|r(x^i)\|^4$ for every $x^* \in S$.
• (2.8) (p. 770): $\eta_i\|r(x^i)\| \to 0$.

Significance

Theorem 2.1 gives global convergence of a projection method for variational inequalities with no Lipschitz constant, no monotonicity and no knowledge of the problem beyond continuity and (1.2), at a fixed cost of two projections per iteration. Condition (1.2) covers pseudomonotone maps, which arise as gradients of pseudoconvex functions and in equilibrium models where monotonicity fails. The separating-hyperplane-and-project template of the proof is reused throughout the later literature on projection, proximal and hybrid methods for monotone inclusions.

The result has been proved since 1999. To the best of available knowledge no machine-checked proof of it, or of any convergence theorem for a projection method for variational inequalities, exists in Lean or Mathlib. This mission produces the statement and the supporting layer: a Euclidean projection onto closed convex sets with its standard inequalities, variational inequality solution sets, the projected residual, and a formal model of an Armijo-type linesearch algorithm with termination.

Difficulty

The Fejér-type inequality (2.6) quickly gives bounded iterates and $\eta_i\|r(x^i)\| \to 0$. The obvious next step, concluding $r(x^i) \to 0$, fails: nothing prevents the stepsizes $\eta_i$ from tending to zero, and in that regime the product going to zero says nothing about the residual. This regime is where the minimality of $k_i$ and the continuity of $F$ enter, and it is the step a naive formalization (for instance one that drops minimality, or fixes the stepsize) cannot reach. A second subtlety is that (1.2) is needed at an accumulation point that is only known to lie in $S$ at the end of the argument, which is why the condition must hold for every $x^* \in S$. Finally, subsequential convergence must be upgraded to convergence of the whole sequence to one solution; convergence of a subsequence, or of the distance to $S$, is strictly weaker.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) (not Fin n → ℝ, whose norm is the sup norm). The accumulation-point step needs finite dimension; no Hilbert-space generalization is intended.
• Projection encoding. projOnto K x is a nearest point of $K$ to $x$ when one exists, chosen by Classical.choose, and the junk value $x$ otherwise. On nonempty closed convex sets it is exactly $P_K[x]$; the paper only projects onto such sets ($C$, $H_i$, $C \cap H_i$), so the junk value is never reached under the hypotheses.
• Stopping-rule encoding. A run is a sequence x : ℕ → ℝⁿ with Armijo indices k : ℕ → ℕ (predicate IsAlg21Run). If $r(x^i) = 0$ the method has stopped and the run stalls, $x^{i+1} = x^i$; otherwise $k_i$ is the least index satisfying (2.1) and $x^{i+1} = P_{C \cap H_i}[x^i]$. A stalled point is a solution, so finitely terminating runs are included in the goal.
• Parameters $\gamma, \sigma$ are real with $0 < \gamma < 1$, $0 < \sigma < 1$, universally quantified; $n$, $C$, $F$ and $x^0 \in C$ are arbitrary.
• (2.6) is stated for one generic step ($x \in C$, $r(x)\ne 0$, $k$ satisfying (2.1)) rather than along a run; it is the same inequality with $x^i, k_i$ abstracted.
• Trivializing formalizations are ruled out: condition (1.2) is quantified over every solution and every $x \in C$ (not replaced by monotonicity or an existential), $k_i$ is the least index satisfying (2.1), the update projects $x^i$ onto $C \cap H_i$ (not onto $C$ alone), the stopped case is pinned down by the stall encoding, and the conclusion is convergence of the whole sequence to one solution, not $r(x^i) \to 0$ or $\operatorname{dist}(x^i, S) \to 0$.
• Needed infrastructure: existence, uniqueness and variational characterization of the projection (Mathlib has exists_norm_eq_iInf_of_complete_convex and norm_eq_iInf_iff_real_inner_le_zero), firm nonexpansiveness, the explicit projection onto a halfspace, and a bounded-sequence subsequence argument in $\mathbb{R}^n$. The projection lemmas are reusable for any projection-type method; contributions proving them as standalone lemmas are welcome.

Selected references

• M. V. Solodov and B. F. Svaiter, A New Projection Method for Variational Inequality Problems, SIAM J. Control Optim. 37(3), 765–776, 1999. https://doi.org/10.1137/S0363012997317475
• G. M. Korpelevich, The extragradient method for finding saddle points and other problems, Matecon 12, 747–756, 1976.
• A. N. Iusem and B. F. Svaiter, A variant of Korpelevich's method for variational inequalities with a new search strategy, Optimization 42, 309–321, 1997. https://doi.org/10.1080/02331939708844365
• P. T. Harker and J.-S. Pang, Finite-dimensional variational inequality and nonlinear complementarity problems: a survey of theory, algorithms and applications, Math. Programming 48, 161–220, 1990. https://doi.org/10.1007/BF01582255
• F. Facchinei and J.-S. Pang, Finite-Dimensional Variational Inequalities and Complementarity Problems, Springer, 2003. https://doi.org/10.1007/b97543

Motivation

Conjugate gradient methods minimize a smooth function $f:\mathbb R^n\to\mathbb R$ using only gradients and a handful of stored vectors. This makes them the standard choice when $n$ is too large for Newton or quasi-Newton methods, which store an $n\times n$ matrix. On a strictly convex quadratic with exact line searches the classical method of Hestenes and Stiefel terminates in at most $n$ steps. On general functions, and with the inexact line searches used in practice, its behaviour is much less clear.

D. F. Shanno's 1978 paper in Mathematics of Operations Research (doi:10.1287/moor.3.3.244) links conjugate gradient methods to quasi-Newton methods. It writes the search direction as $-\hat H g$, where $\hat H$ is a positive definite approximation of the inverse Hessian that is never stored. The resulting "memoryless" BFGS directions give descent without exact line searches. The paper's new algorithm uses two BFGS updates: one from the last restart and one from the current step. Its first update is scaled by the Oren–Spedicato factor $\gamma_t$. Shanno and Phua's CONMIN code implements the algorithm, and the memoryless BFGS direction is the one-pair case of the later limited-memory BFGS methods.

• 1952: Hestenes and Stiefel, linear conjugate gradients.
• 1964: Fletcher and Reeves, nonlinear conjugate gradients.
• 1969: Polak and Ribière, a second nonlinear variant.
• 1972: Beale, a restart procedure that keeps the computed direction $d_t$.
• 1977: Powell's restart criterion (Powell 1977).
• 1978: Shanno's reformulation as memoryless and two-update quasi-Newton methods (this paper).

Setting

Vectors are columns in $\mathbb R^n$. A prime denotes transpose: $u'v$ is the inner product and $uv'$ the outer product. An iterative method produces points $x_k$, steps $p_k = x_{k+1}-x_k = \alpha_k d_k$ along search directions $d_k$, gradients $g_k = \nabla f(x_k)$, and gradient changes $y_k = g_{k+1}-g_k$. A line search is exact when $p_k'g_{k+1} = 0$.

The BFGS update of a matrix $H$ with the pair $(p,y)$ is

$$H^+ = H - \frac{p\,y'H + H y\,p'}{p'y} + \left(1+\frac{y'Hy}{p'y}\right)\frac{pp'}{p'y}.$$

A restart cycle begins at iteration $t$. At a later iteration $k>t$, Shanno's self-scaled restart matrix is

$$\hat H_k = \gamma_t\left(I - \frac{p_ty_t'+y_tp_t'}{p_t'y_t} + \frac{y_t'y_t}{p_t'y_t}\frac{p_tp_t'}{p_t'y_t}\right) + \frac{p_tp_t'}{p_t'y_t}, \qquad \gamma_t = \frac{p_t'y_t}{y_t'y_t}.$$

The matrix $\hat H_{k+1}$ is its BFGS update with $(p_k,y_k)$, and the self-scaled two-update direction is $d_{k+1} = -\hat H_{k+1}g_{k+1}$. The unscaled variant uses the BFGS update of $I$ in place of the first matrix.

Beale's direction is

$$d_{k+1} = -g_{k+1} + \frac{y_k'g_{k+1}}{d_k'y_k}d_k + \frac{y_t'g_{k+1}}{d_t'y_t}d_t.$$

The quadratic case has gradient $g(x) = Ax + c$ with $A$ symmetric positive definite.

Formalization targets

Goal: reduction of the self-scaled method to Beale's method

Let $A$ be symmetric positive definite, $g_i = Ax_i + c$ and $t<k$. Assume that for $t\le i\le k$ we have $x_{i+1} = x_i + p_i$, $p_i = \alpha_i d_i$ and $p_i'g_{i+1}=0$, that $p_t'Ap_i = 0$ for $t<i\le k$, and that $p_t, p_k \ne 0$. Then

$$-\hat H_{k+1}g_{k+1} = \gamma_t\left(-g_{k+1} + \frac{y_k'g_{k+1}}{d_k'y_k}d_k + \frac{y_t'g_{k+1}}{d_t'y_t}d_t\right).$$

This is the paper's claim that "for $f(x)$ quadratic with exact searches each of the above methods reduces exactly to Beale's method defined by (28)", with the conclusion (44). The scale is exactly $\gamma_t$.

Companion statements

• The unscaled two-update direction equals Beale's direction exactly.
• Both two-update directions are descent directions, $g_{k+1}'d_{k+1} < 0$, whenever $p_t'y_t > 0$ and $p_k'y_k > 0$. No exact search is needed.

Milestones on the path

• (34): the expansion of $-\hat H_{k+1}g_{k+1}$.
• (40): its form under an exact search.
• (41): gradients along a run on a quadratic.
• $p_t'g_{k+1} = 0$.
• (38), corrected by a factor 2: the action of the self-scaled restart matrix.
• (42): its form when $p_t'g_{k+1} = 0$.
• (43): the direction after substitution.

Significance

The result. The reduction says that the new algorithm reproduces Beale's restarted conjugate gradient directions on a quadratic with exact line searches. So it keeps the finite-termination and rate-of-convergence properties behind Beale's restart. Away from that setting it behaves as a quasi-Newton method, whose directions are descent directions under any line search with $p'y>0$. The two regimes are what justify relaxing the line search, which the paper's computations exploit. The scale $\gamma_t$ changes only the length of the step, not its direction.

Formalizing it. The claim is proved in the paper by a short computation, and no machine-checked version is known. This mission produces:

• a checked statement of the claim with every hypothesis explicit, including the conjugacy the proof takes as known;
• a corrected version of display (38), which is misprinted;
• reusable definitions of the additive BFGS update and of Beale's direction.

Difficulty

The obvious attempt is to expand both BFGS updates symbolically and compare with Beale's formula. This fails without two facts that are not algebraic identities. The first is that the restart step stays orthogonal to every later gradient, $p_t'g_{k+1}=0$. It needs the affine gradient of a quadratic, the exact search at the restart step, and conjugacy of $p_t$ with all later steps. The second is $y_k'p_t = 0$, which again comes from conjugacy. Beale's formula also has to be matched in its $d$-form: the coefficient $\frac{y'g}{d'y}d$ equals $\frac{y'g}{p'y}p$ only when the step length is nonzero. The descent statements need a different argument: the BFGS update of a positive definite matrix with $p'y>0$ must be shown to remain positive definite, and this has to be done twice.

Formalization scope

Vectors are Fin n → ℝ and matrices Matrix (Fin n) (Fin n) ℝ. The inner product $u'v$ is u ⬝ᵥ v, the outer product $uv'$ is vecMulVec u v, and $Hv$ is H *ᵥ v. The quadratic enters only through its gradient A *ᵥ x + c with A.PosDef. The paper's (4) is the case $c = -A\hat x$. Iterates, steps, directions and gradients are sequences indexed by ℕ. Division is Lean's total division. Every statement that divides therefore carries hypotheses making its denominators nonzero: $p_t \ne 0$ and $p_k\ne0$ in the quadratic statements, and $p_t'y_t\ne 0$ or $p'y>0$ in the generic ones.

The conjugacy $p_t'Ap_i=0$ for $t<i\le k$ is a hypothesis, exactly as the paper's proof uses it. It is not derived from a full run of Beale's algorithm. The range $k\le t+n-1$ of Beale's formula is not assumed.

Several formalizations would make the claim easier than the paper's, and none of them is used:

• defining the direction by the expanded formula (34), or the restart matrix by (38);
• adding orthogonality or conjugacy hypotheses beyond those listed;
• concluding only that the two directions are parallel;
• dropping the restart term of Beale's direction;
• allowing a zero denominator.

The generic milestones — (34), (40), (38), (42), (43) and the descent statements — are statements about arbitrary vectors and matrices and are reusable for any BFGS-based method. Proofs of any milestone, and alternative derivations of the goal, are welcome.

Selected references

• D. F. Shanno, Conjugate Gradient Methods with Inexact Searches, Mathematics of Operations Research 3(3) (1978) 244–256. https://doi.org/10.1287/moor.3.3.244
• E. M. L. Beale, A derivation of conjugate gradients, in F. A. Lootsma (ed.), Numerical Methods for Nonlinear Optimization, Academic Press, 1972, 39–43.
• M. J. D. Powell, Restart procedures for the conjugate gradient method, Mathematical Programming 12 (1977) 241–254. https://doi.org/10.1007/BF01593790
• M. R. Hestenes and E. Stiefel, Methods of conjugate gradients for solving linear systems, J. Res. Nat. Bur. Standards 49 (1952) 409–436. https://doi.org/10.6028/jres.049.044
• S. S. Oren and E. Spedicato, Optimal conditioning of self-scaling variable metric algorithms, Mathematical Programming 10 (1976) 70–90. https://doi.org/10.1007/BF01580654

Motivation

Retailers hold point-of-sale data that their suppliers cannot observe, and large retailers sell access to it through data-sharing programs (Costco's CRX, Walmart's Retail Link and similar programs). When one retailer carries the substitutable products of two competing manufacturers, sharing its demand information is a strategic decision: a manufacturer who knows the demand signal sets his wholesale price in response to it, which changes the retailer's margin and the rival manufacturer's order uncertainty. Whether the retailer should sell the information, to how many manufacturers, and by which protocol, is the question of Shang, Ha and Tong (Management Science 62(1):245–263, 2016).

The paper belongs to the information-sharing literature of Li (2002), Li and Zhang (2008) and Ha, Tong and Zhang (2011), which studies competing supply chains or a single chain. The common-retailer structure differs: the retailer can price-discriminate between the manufacturers through the order in which she offers the information.

Setting

Two manufacturers $i \in \{1, 2\}$ sell substitutable products through one retailer. The demand for product $i$ is

$$q_i = a + \theta - (1+\phi)p_i + \phi p_j,$$

where $p_i$ is the retail price, $\phi > 0$ measures competition, and $\theta$ is a random shock with mean $0$ and variance $\sigma^2 > 0$. The retailer observes a demand signal $Y$ that is unbiased, $E[Y \mid \theta] = \theta$, and has linear expectation: $E[\theta \mid Y] = \beta Y$ for a weight $\beta$ (in the paper $\beta = t\sigma^2/(1+t\sigma^2)$, with $t$ the signal accuracy). The retailing cost is zero, and manufacturer $i$ produces $q$ units at cost $bq + c_d q^2$ with $b, c_d > 0$: a production diseconomy.

The game has four stages.

1. The retailer and the manufacturers contract on information sharing, which fixes each manufacturer's status $X_i \in \{I, U\}$ (informed or uninformed).
2. The retailer observes $Y$ and discloses it truthfully to the informed manufacturers.
3. The manufacturers set wholesale prices $w_i$ simultaneously, an informed one as a function of $Y$. The retailer then sets retail prices.
4. Demand realizes and payoffs are received.

The pricing stage is a Bayesian game. Its equilibrium ex ante profits are $\pi_M(n)$, $\pi_M^I(1)$, $\pi_M^U(1)$ for the manufacturers and $\pi_R(n)$ for the retailer, where $n$ is the number of informed manufacturers. They define a payoff table for the contracting stage.

Two contracting protocols are compared.

• Concurrent contracting: the retailer offers both manufacturers the same payment $T$, and they accept or reject simultaneously; a Pareto-optimal pure equilibrium is the outcome, and the retailer chooses $T$.
• Sequential contracting: the retailer offers one manufacturer $T_f$, he accepts or rejects, then the retailer offers the other $T_s$, and he decides having observed the first decision. The retailer cannot commit to $T_s = T_f$, and the solution is subgame perfect equilibrium.

Formalization targets

Goal: Proposition 4(d)

For every $\phi > 0$, $c_d > 0$ and every signal model, the pricing stage has an equilibrium; for every pricing equilibrium, both contracting games have equilibria; and for every concurrent outcome and every sequential subgame-perfect equilibrium (either first mover),

$$\Pi_R^{C} \le \Pi_R^{S}, \qquad \Pi_M^{S} \le \Pi_M^{C},$$

with both inequalities strict when $c_d > (\sqrt2 - 1)/(1+\phi)$. Here $\Pi_R$ is the retailer's profit after side payments and $\Pi_M$ the manufacturers' total profit net of them. The paper's word "higher" is read as $\ge$ because for small $c_d$ neither protocol sells information and all profits coincide.

Milestones

1. §4.1, Eq. (1): the retailer's best response $\hat p_i = \frac12(a + \beta Y + w_i)$ and the resulting demand.
2. Lemma 1: the pricing equilibrium exists, is unique, and is linear in $Y$.
3. §4.2: the closed forms of the seven ex ante profits.
4. Lemma 3: $\pi_M(2) > \pi_M^I(1) > \pi_M(0) > \pi_M^U(1)$, $\pi_R(0) > \pi_R(1) > \pi_R(2)$, $\pi_R(1) - \pi_R(2) > \pi_R(0) - \pi_R(1)$.
5. Proposition 1(b): without contracting, no information is shared.
6. Propositions 2 and 3: thresholds $c_d^C$ and $c_d^{S1}, c_d^{S2}$, depending only on $\phi$, at which the number of informed manufacturers changes under each protocol.
7. Proposition 4(a): $c_d^{S1} < c_d^C < c_d^{S2}$.

Significance

The result. Proposition 4(d) says that the order of the offers transfers surplus: selling information one manufacturer at a time lets the retailer exploit the manufacturers' fear of being the only uninformed firm, which raises her profit and lowers theirs. Propositions 2 and 3 show that concurrent contracting shares with both manufacturers or with neither, while sequential contracting can end with only one informed manufacturer. Together they give a complete map of the equilibrium sharing decisions in $(c_d, \phi)$ (Figure 1 of the paper).

Formalizing it. The results are proved in the paper, partly by "it can be shown" and "straightforward" steps: Lemma 3's proof is omitted, and so is the convexity of the function whose root is $c_d^{S2}$. No part of the paper has a machine-checked proof. A complete formalization would check every such step and make the equilibrium notions precise, in particular the Pareto selection and the tie-breaking at the thresholds, where the retailer is exactly indifferent.

Difficulty

Most of the work is in the contracting stage, not the algebra. The pricing stage must be solved over all square-integrable strategies measurable in the signal. Uniqueness is then almost sure and rests on the linear-expectation identities $E[\theta Y] = \sigma^2$ and $E[Y^2] = \sigma^2/\beta$. The concurrent game has multiple equilibria for intermediate payments, and the retailer's optimum lies at a payment where two equilibria coexist. The sequential game is a three-stage game with a continuum of offers: at each threshold the retailer is indifferent, and an SPE exists only if acceptance at indifference is chosen correctly. The threshold $c_d^{S2}$ has no closed form; it is the root of a convex rational function of $c_d$.

Formalization scope

The Lean development lives in the namespace InfoSharing.Diseconomy. Conventions:

• The probability space carries $\theta$ and $Y$ in $L^2$, with the two conditional-expectation identities holding almost everywhere. $\beta$ is a parameter fixed by $E[\theta \mid Y] = \beta Y$; Ericson's formula for $\beta$ is not formalized.
• Wholesale strategies are measurable, square-integrable functions of the signal value, and constants for an uninformed manufacturer. A pricing equilibrium is ex ante optimality over such strategies, which is equivalent to the paper's conditional optimization. The retailer's rule must be a best response at every wholesale-price pair.
• The payoff table is produced by an arbitrary pricing-equilibrium family, not by the §4.2 closed forms. A formalization that takes the closed forms as the definition of the profits would reduce the goal to algebra and a $2 \times 2$ game, and is ruled out.
• Payments are nonnegative, only pure strategies are used in the contracting games, and the concurrent outcome selects, among Pareto-optimal equilibria, the one best for the retailer.
• Threshold statements use two clauses: the printed value is attained on the closed region, and it is the only value on the region's interior. The thresholds depend only on $\phi$.
• Demands may be negative (θ is unbounded), as in the paper's formulas.

A complete development needs:

• the conditional-expectation algebra behind Lemma 1 and §4.2;
• rational-function inequalities for Lemma 3;
• a case analysis of the two contracting games.

The model layer is shared with the companion mission on production economy.

Selected references

• G. Shang, A. Y. Ha, S. Tong, Information Sharing in a Supply Chain with a Common Retailer, Management Science 62(1):245–263, 2016. https://doi.org/10.1287/mnsc.2014.2127
• W. A. Ericson, A note on the posterior mean of a population mean, Journal of the Royal Statistical Society B 31(2):332–334, 1969.
• L. Li, Information sharing in a supply chain with horizontal competition, Management Science 48(9):1196–1212, 2002. https://doi.org/10.1287/mnsc.48.9.1196.177
• L. Li, H. Zhang, Confidentiality and information sharing in supply chain coordination, Management Science 54(8):1467–1481, 2008. https://doi.org/10.1287/mnsc.1070.0851
• A. Y. Ha, S. Tong, H. Zhang, Sharing imperfect demand information in competing supply chains with production diseconomies, Management Science 57(3):566–581, 2011. https://doi.org/10.1287/mnsc.1100.1295
• X. Vives, Oligopoly Pricing: Old Ideas and New Tools, MIT Press, 1999.

Motivation

A b-matching with upper bounds in a graph $G=(V,E)$ assigns a nonnegative integer $x_e\le d_e$ to every edge so that the edges at each node $i$ carry at most $b_i$ in total. Maximizing a linear objective over such assignments is an integer program that contains ordinary matching ($b\equiv 1$, $d\equiv 1$) and appears in assignment, transportation and scheduling models with capacities on both nodes and arcs. Edmonds and Johnson showed that the integer hull of this system is described by adding the blossom (matching) inequalities to the linear relaxation (Edmonds–Johnson 1970; cited in the paper as [8], [13]). There are exponentially many blossom inequalities, so a cutting-plane method needs a separation procedure: given a fractional point $\bar x$, find a violated blossom inequality or certify that none exists.

M. W. Padberg and M. R. Rao, Odd Minimum Cut-Sets and b-Matchings, Mathematics of Operations Research 7 (1982), gave this procedure. Section 1 of the paper computes a minimum-capacity cut with an odd number of odd-labelled nodes in polynomial time; Sections 2 and 3 reduce blossom separation to that computation. This mission formalizes Section 3, the case with upper bounds $d$. The companion mission Odd Minimum Cut-Sets and b-Matchings 1 formalizes Section 1.

Timeline: Edmonds (1965) describes the perfect matching polytope; Edmonds and Johnson (1970) extend the description to capacitated $b$-matching; Gomory and Hu (1961) give the cut-tree that Section 1 of Padberg–Rao relies on; Padberg and Rao (1982) reduce separation to odd minimum cuts. Later work (Letchford, Reinelt and Theis, 2008) shortened the resulting algorithms; the reduction itself is the one stated here.

Setting

Let $G=(V,E)$ be a finite simple undirected graph, $b\in\mathbb Z_{>0}^V$ and $d\in\mathbb Z_{>0}^E$. The system is

$$Ax\le b,\qquad x\le d,\qquad x\ge 0, \tag{3.1}$$

with $A$ the node–edge incidence matrix. For $W\subseteq V$ write $E(W)$ for the edges with both ends in $W$ and $(W:V-W)$ for the cut-set of $W$, the edges with exactly one end in $W$. For $T\subseteq (W:V-W)$ with $b(W)+d(T)=\sum_{i\in W}b_i+\sum_{e\in T}d_e$ odd, the blossom inequality is

$$x(W)+x(T)=\sum_{e\in E(W)}x_e+\sum_{e\in T}x_e\le \tfrac12\bigl(b(W)+d(T)-1\bigr). \tag{3.3}$$

Let $\bar x$ be a real point feasible for (3.1) and $\bar s=b-A\bar x$ its node slacks. Let $E(\bar x)$ be the edges with $\bar x_e>0$. The labelled weighted graph $G(\bar x,d)$ has nodes $V$, a special node $S$, and one new node $i_e$ for each $e\in E(\bar x)$. For each such edge $e=[i,j]$, where $i$ is the end the construction scans first, it has an edge $[i,i_e]$ of weight $d_e-\bar x_e$ and an edge $[i_e,j]$ of weight $\bar x_e$. Each $i\in V$ is joined to $S$ with weight $\bar s_i$. There are no other edges. A node $i_e$ is odd iff $d_e$ is odd; $S$ is odd iff $b(V)$ is odd; a node $i\in V$ is odd iff $b_i$ plus the $d_e$ of the subdivided edges scanned from $i$ is odd. A node set $U$ is odd when it contains an odd number of odd nodes, and $\bar y(U:\tilde V-U)$ denotes the total weight of the edges leaving $U$ (its cut capacity).

Formalization targets

Goal: Theorem 3.1

For every feasible $\bar x$ and every scan order,

$$\exists\,W\subseteq V,\ T\subseteq (W:V-W):\ b(W)+d(T)\text{ odd},\ \bar x(W)+\bar x(T)>\tfrac12\bigl(b(W)+d(T)-1\bigr)$$ $$\Longleftrightarrow\quad \exists\,U\subseteq \tilde V \text{ odd}:\ \bar y(U:\tilde V-U)<1 .$$

The paper's closing sentence, that $W$ and $T$ can be obtained constructively from the proof of Lemma 3.2, describes the proof and is not part of the formal statement.

Milestones

1. Eq. (3.6): $2x(W)+x(W:V-W)+x(T)+s(W)+t(T)=b(W)+d(T)$ for $T\subseteq(W:V-W)$, with $t=d-x$.
2. Eq. (3.7): $\bar x$ violates (3.3) for $(W,T)$ iff $\bar x(W:V-W)+d(T)-2\bar x(T)+\bar s(W)<1$.
3. Lemma 3.1: if $T\subseteq (W:V-W)\cap E(\bar x)$ and $b(W)+d(T)$ is odd, some odd $U$ with $S\notin U$ has $\bar y(U:\tilde V-U)$ equal to the left side of (3.7) (Eq. (3.8)).
4. Lemma 3.2: every odd $U$ with $S\notin U$ and capacity $<1$ arises this way from some $(W,T)$ with $b(W)+d(T)$ odd.

Significance

Theorem 3.1 is what makes the blossom inequalities of capacitated $b$-matching usable in a linear-programming based cutting-plane method: combined with the odd minimum cut algorithm of Section 1, it separates them in polynomial time. By the equivalence of separation and optimization, it also yields a polynomial-time algorithm for capacitated $b$-matching through the ellipsoid method. The paper notes the further consequence that every odd cut-set of capacity less than one, not only a minimum one, gives a violated inequality.

The results are proved in the 1982 paper; none of them has a machine-checked proof that this mission is aware of. What the mission adds is a formal statement of the graph $G(\bar x,d)$ and of the reduction, and a checked proof of it. The definitions of the capacitated $b$-matching system, its blossom inequalities and the subdivided graph are reusable for later work on matching polytopes and on the uncapacitated case of Section 2.

Difficulty

The identities (3.6) and (3.7) are bookkeeping over incidences. The substance is the correspondence between node sets $W$ with complemented edge sets $T$ and odd node sets $U$ of $G(\bar x,d)$. In one direction the right $U$ must pick, for every cut edge, the side of $i_e$ that makes the edge contribute $\bar x_e$ or $d_e-\bar x_e$ as (3.7) requires, and its parity must be computed through the orientation-dependent labels. In the other direction an arbitrary odd cut of capacity below one must be shown to have this shape; this uses $d_e\ge 1$ to exclude every other position of a new node $i_e$, and it uses the evenness of the total label to pass from an odd set containing $S$ to its complement. A point $\bar x$ whose blossom violation uses an edge $e\in T$ with $\bar x_e=0$ has no new node for $e$. Such a $T$ has to be ruled out, and the argument uses the capacity bound. It is not an assumption of the theorem.

Formalization scope

The graph is a Mathlib SimpleGraph V on a finite type with decidable adjacency; edges are elements of G.edgeFinset : Finset (Sym2 V). The data are b : V → ℕ and d : Sym2 V → ℕ, positive on nodes and on edges, and a real point x : Sym2 V → ℝ. Feasibility means the linear relaxation of (3.1); integrality of $\bar x$ is not assumed. All halves and differences are computed in ℝ. When $W=V$ the cut-set is empty, so the paper's convention "$T$ is empty" holds automatically.

$G(\bar x,d)$ is fixed by definitions from $(G,b,d,\bar x)$ and an orientation tail choosing the end of each edge scanned first; every theorem quantifies over the orientation. The node type is Option V ⊕ {e // e ∈ E(x̄)}, with none the special node $S$. Weights are a symmetric function on nodes with $0$ meaning "no edge". The labels are given in closed form. The paper assigns them by a sequential scan that flips the parity of the scanned end by $d_e$, and addition mod 2 does not depend on the order of the scan. "The cut capacity of an odd minimum cut-set is less than one" is stated as "some odd cut has capacity less than one"; the two agree, and the formulation avoids a minimum over a possibly empty family.

Two trivializing formalizations are ruled out: $G(\bar x,d)$ is constructed, not an arbitrary labelled graph assumed to satisfy (3.8); and no infimum over odd cuts is taken, since a real sInf of an empty family is $0$ and would make the right side true when no odd cut exists.

Contributions welcome: proofs of the milestones, lemmas on cut capacities of symmetric weight functions on finite types, and parity bookkeeping for labelled node sets.

Selected references

• M. W. Padberg, M. R. Rao, Odd Minimum Cut-Sets and b-Matchings, Mathematics of Operations Research 7(1), 67–80, 1982. https://doi.org/10.1287/moor.7.1.67
• J. Edmonds, E. L. Johnson, Matching: a well-solved class of integer linear programs, in Combinatorial Structures and Their Applications, Gordon and Breach, 89–92, 1970; reprinted in Combinatorial Optimization — Eureka, You Shrink!, LNCS 2570, 27–30, 2003. https://doi.org/10.1007/3-540-36478-1_3
• R. E. Gomory, T. C. Hu, Multi-terminal network flows, Journal of the SIAM 9(4), 551–570, 1961. https://doi.org/10.1137/0109047
• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, Journal of Research of the National Bureau of Standards 69B, 125–130, 1965. https://doi.org/10.6028/jres.069B.013
• A. N. Letchford, G. Reinelt, D. O. Theis, Odd minimum cut sets and b-matchings revisited, SIAM Journal on Discrete Mathematics 22(4), 1480–1487, 2008. https://doi.org/10.1137/060664793

Motivation

Edmonds showed that the convex hull of the matchings of a graph is described by the degree constraints together with the blossom inequalities, one for every odd set of nodes (Edmonds 1965). There are exponentially many of them, so any cutting-plane method for matching and b-matching problems must answer a separation question: given a fractional point, find a violated blossom inequality or certify that none exists. Padberg and Rao (1982) reduced this question to a purely graph-theoretic one, the odd minimum cut-set problem, and solved that problem in polynomial time with a single Gomory–Hu computation. The same subroutine underlies separation for many other odd-set constraints (for example the 2-matching and comb-type constraints of the travelling salesman polytope), and later work refined its running time (Letchford, Reinelt and Theis 2008).

This mission covers Section 1 of the paper: the combinatorial theorem about odd cuts, independent of matchings. A companion mission covers the reduction from capacitated b-matching separation (Section 3).

Setting

Let $G = (V, E)$ be a finite undirected graph without loops and multiple edges, with edge weights $c_e \ge 0$. Write $c_{ij}$ for the weight of the edge $[i, j]$, with $c_{ij} = c_{ji}$, and $c_{ij} = 0$ if there is no such edge. For $W \subseteq V$ the cut-set $(W : V - W)$ is the set of edges with exactly one end in $W$, and its capacity is

$$c(W : V - W) = \sum_{i \in W} \sum_{j \in V - W} c_{ij}.$$

A nonempty set $V_1 \subseteq V$ of nodes is labelled odd, the rest even. For $U \subseteq V$ the label $\lambda(U)$ is odd if $|U \cap V_1|$ is odd, and even otherwise; $\lambda(\emptyset)$ is even. The paper assumes throughout that $\lambda(V)$ is even, i.e. $|V_1|$ is even. A cut-set $(U : V - U)$ is odd if $\lambda(U)$ is odd, and an odd minimum cut-set is a solution $X$ of

$$c(X : V - X) = \min\{ c(U : V - U) : U \subseteq V,\ \lambda(U) \text{ odd} \}. \qquad (1.1)$$

A cut-set $(M : V - M)$ is a minimum cut-set with respect to all pairs of odd nodes if it separates two odd nodes and no cut-set separating two odd nodes has smaller capacity.

A cut-tree $G_T = (N, F)$ for the odd nodes is the output of the Gomory–Hu algorithm applied to all pairs of odd nodes (Gomory and Hu 1961). Each tree node contains exactly one odd node and possibly some even ones, so $N$ is identified with $V_1$, and each node $v$ of $G$ belongs to one tree node $\pi(v)$. Removing a tree edge $f = [r, s]$ splits $G_T$ into two subtrees; the nodes of $G$ in the tree nodes of the $r$-side subtree form a set $M$, and the weight of $f$ is $d_f = c(M : V - M)$. The defining property (Hu, Theorem 9.2) is that for every tree edge $f = [r, s]$ the cut-set $(M : V - M)$ is a minimum cut-set of $G$ separating $r$ and $s$. The cardinality of a subtree is its number of tree nodes.

Formalization targets

Goal: Theorem 1.1 (p. 70)

For every cut-tree $G_T$ of $G$ for the odd nodes:

1. some edge of $G_T$ decomposes it into two subtrees of odd cardinality; and
2. if $f^* = [r, s]$ is such an edge of minimum weight among all such edges, and $M$ is the $r$-side shore of $f^*$, then

$$c(M : V - M) = \min\{ c(U : V - U) : U \subseteq V,\ \lambda(U) \text{ odd} \}.$$

Because $|N| = |V_1|$ is even, the two subtrees have the same parity, so the condition is checked on one side.

Milestones

• Lemma 1.1 (p. 68). If $(M : V - M)$ is a minimum cut-set with respect to all pairs of odd nodes, there is an odd minimum cut-set $(X : V - X)$ with $X \subseteq M$ or $X \subseteq V - M$.
• Section 1, p. 70. If $f^*$ has minimum weight among all edges of $G_T$, its shore $M$ gives a minimum cut-set with respect to all pairs of odd nodes.

Significance

Theorem 1.1 turns problem (1.1), a minimization over exponentially many odd sets, into $|V_1| - 1$ maximum-flow computations followed by a scan of the tree edges. Combined with Section 3 of the paper, this gives a polynomial separation algorithm for the blossom inequalities of b-matching polytopes, and hence, by the equivalence of separation and optimization, a polynomial-time route to weighted b-matching through linear programming. The odd-cut routine is also used for separating the odd-set constraints of other polytopes.

The theorem has been proved since 1982 and is textbook material. What this mission adds is a machine-checked proof on a precise encoding of cut-trees. As far as the platform's corpus shows, neither the Gomory–Hu cut-tree property nor any odd-cut theorem has been formalized in Lean; Mathlib has trees and reachability in simple graphs but no cut-tree theory.

Difficulty

The obvious argument fails at the minimum. Every tree-edge shore separates two odd nodes, so a minimum-weight odd-splitting edge certainly yields an odd cut, but showing that no odd set $U$, however it cuts across the tree nodes, has smaller capacity requires relating an arbitrary odd $U$ to a tree edge whose shore is also odd and whose endpoints $U$ separates. The cut-tree only certifies minimality for cuts separating the two ends of a tree edge; an odd set $U$ may split many tree nodes and cross many shores at once, and nothing in the cut-tree property speaks about parity. Parity bookkeeping between odd labels in $G$ and odd cardinality of subtrees is the other place where care is needed: the two notions agree only because each tree node holds exactly one odd node.

Formalization scope

The graph is a weight function c : V → V → ℝ on a Fintype V, with hypotheses that it is symmetric and nonnegative; a missing edge has weight 0 and the diagonal never enters a cut. Node sets are Finset V and $V - W$ is the complement Wᶜ. The odd nodes form a Finset odd with odd.Nonempty and Even odd.card on every statement. The cut-tree is a SimpleGraph on the subtype {v // v ∈ odd} together with a map π : V → {v // v ∈ odd}; IsOddCutTree requires that the graph is a tree, that π fixes every odd node, and the Gomory–Hu minimality for every tree edge. The tree-edge weight $d_f$ is computed from the shore, not supplied as data. Minimality is always stated as ≤ against every competitor; no real infimum is taken.

The existence of a cut-tree (the Gomory–Hu theorem) is a hypothesis-side object and is not part of this mission; the theorems hold for every tree satisfying the cut-tree property. A statement in which the cut-tree assumption already says that the chosen edge's shore is an odd minimum cut, or in which "odd minimum cut" is minimized only over tree-edge shores, would make Theorem 1.1 definitional; both are ruled out, since IsOddMinCut ranges over every node set with odd label.

A complete development needs: submodularity-type identities for cut capacities (reusable for any cut problem), the structure of fundamental cuts of a tree (the two sides of a removed edge are complementary and the parities of $U \cap V_1$ along tree edges combine), and Lemma 1.1. Proofs of the milestones, alternative arguments for the goal that avoid the recursion, and a formal Gomory–Hu existence theorem are all welcome contributions.

Selected references

• M. W. Padberg and M. R. Rao, Odd Minimum Cut-Sets and b-Matchings, Mathematics of Operations Research 7(1), 67–80, 1982. https://doi.org/10.1287/moor.7.1.67
• R. E. Gomory and T. C. Hu, Multi-Terminal Network Flows, Journal of the SIAM 9(4), 551–570, 1961. https://doi.org/10.1137/0109047
• T. C. Hu, Integer Programming and Network Flows, Addison-Wesley, 1969 (Chapter 9, Theorem 9.2).
• J. Edmonds, Maximum Matching and a Polyhedron with 0,1-Vertices, Journal of Research of the National Bureau of Standards 69B, 125–130, 1965. https://doi.org/10.6028/jres.069B.013
• A. N. Letchford, G. Reinelt and D. O. Theis, Odd Minimum Cut Sets and b-Matchings Revisited, SIAM Journal on Discrete Mathematics 22(4), 1480–1487, 2008. https://doi.org/10.1137/060664793

Motivation

Algorithmic mechanism design asks for algorithms whose inputs are held by self-interested agents: the designer can pay the agents, and must choose payments so that each agent's own interest leads it to reveal what the algorithm needs. Nisan and Ronen introduced the framework with task scheduling on unrelated machines as the running example (Nisan–Ronen 2001). In the basic model, where payments depend only on what the agents declare, they showed that no truthful mechanism approximates the optimal make-span within a factor below 2, and that the natural mechanism only reaches a factor $n$.

Their Section 5 changes the information available: in a mechanism with verification the payments may also depend on the times in which the tasks were actually performed. With this extra information, an exact optimizer becomes a strongly truthful mechanism (Theorem 5.1, the Compensation-and-Bonus mechanism). Exact scheduling on unrelated machines is NP-hard, so the question is whether an approximation algorithm can take the optimizer's place. Theorem 5.6 of the paper shows that plugging a non-optimal algorithm into Compensation-and-Bonus destroys truthfulness in general. Theorem 5.9, the subject of this mission, shows that for the bounded problem a specific approximation scheme, the rounding algorithm of Horowitz and Sahni (1976), can be combined with a modified payment rule to give a truthful mechanism whose outcome is within a factor $1+\varepsilon$ of optimal.

Setting

There are $n$ agents and $k$ tasks. Agent $i$ needs time $t^i_j$ for task $j$; the vector $t = (t^i_j)$ is the type vector, and agent $i$ alone knows its row $t^i$. In the bounded scheduling problem (Definition 33) there are fixed numbers $0 < a < b$ with $a \le t^i_j \le b$ for all $i, j$, and every declaration lies in the same range. An allocation $x$ assigns each task to one agent; $x^i$ is the set of tasks of agent $i$.

A strategy of agent $i$ has two parts: a declaration $d^i \in [a,b]^k$, and an execution, which for each decision $x$ of the mechanism specifies the actual time $\tilde t_j \ge t^i_j$ in which agent $i$ performs each task $j \in x^i$. The mechanism chooses $x = x(d)$ from the declarations alone and afterwards observes the actual times $\tilde t$. The objective is the make-span with actual times,

$$g(x,\tilde t) = \max_i \sum_{j \in x^i} \tilde t_j .$$

Agent $i$ receives a payment $p^i$ and has utility $p^i - \sum_{j \in x^i} \tilde t_j$.

The corrected time vector of agent $i$ keeps agent $i$'s actual times on its own tasks and the other agents' declarations elsewhere: $\mathrm{corr}^i(x,d,\tilde t)_j = \tilde t_j$ for $j \in x^i$ and $d^l_j$ for $j \in x^l$, $l \ne i$. For a step $\delta > 0$, $\hat r = \delta\lceil r/\delta\rceil$ rounds $r$ up to a multiple of $\delta$, and $\hat g(x,\tau) = g(x,\hat\tau)$.

The rounding mechanism (Definition 34) allocates with an algorithm that exactly solves the problem with rounded declarations $\hat d$, and pays

$$p^i = \sum_{j\in x^i}\tilde t_j \;-\; \hat g\big(x, \mathrm{corr}^i(x, d, \tilde t)\big).$$

The first term, the compensation, uses exact actual times; the second, the bonus, uses rounded quantities.

A strategy is dominant if it is a best response to every declarations and executions of the others. The mechanism is truthful if every agent has a dominant strategy that declares its true type.

Formalization targets

Goal: Theorem 5.9 without running time

For every $\varepsilon > 0$, every $0 < \delta \le \varepsilon a$ and every allocation algorithm solving the rounded problem exactly, the rounding mechanism is truthful, and at every profile of dominant strategies from the class named in the proof (declarations with the true rounded values, executions whose rounded times equal the rounded true times),

$$g\big(x(d),\tilde t\big) \le (1+\varepsilon)\, g(y,t) \quad \text{for every allocation } y .$$

Milestones

1. The solution of the rounded problem is a $(1+\varepsilon)$-approximation: $g(x,\hat t) \le g(y,\hat t)\ \forall y$ implies $g(x,t) \le (1+\varepsilon) g(y,t)\ \forall y$.
2. After rounding, $\hat g$ is the make-span, $\hat g(x,\mathrm{corr}^*(x,d)) = g(x,\hat d)$, and each agent's utility equals its rounded bonus.
3. Every strategy with the true rounded values is dominant.
4. When all agents follow such strategies, the outcome is a $(1+\varepsilon)$-approximation.
5. Truth-telling with minimal execution is dominant; hence the mechanism is truthful.

Significance

The result shows that verification does more than make exact optimization truthful: it lets a polynomial-time approximation scheme be implemented in dominant strategies, provided the bonus is computed on the same rounded instance the algorithm optimizes. This contrasts with Theorem 5.6, where an arbitrary approximation algorithm inside Compensation-and-Bonus is not truthful, and with the factor-2 lower bound of the basic model. The principle it illustrates is that the payments must reward exactly the objective the algorithm optimizes.

The paper gives only a proof sketch. Formalizing it makes the argument's hypotheses explicit: which rounding step suffices, what the allocation algorithm must satisfy, and over which strategy profiles the approximation guarantee holds. No machine-checked version of this theorem or of the Compensation-and-Bonus argument is known to exist.

Difficulty

The sketch reduces the theorem to "arguments similar to those in 5.1", but the rounded setting departs from Theorem 5.1 in two ways. Rounding is many-to-one, so an agent's declaration and execution are pinned down only up to their rounded values, and the algorithm's optimality holds only for the rounded instance. Consequently the claim that the strategies with the true rounded values are the only dominant ones does not survive arbitrary tie-breaking: an agent that is always favoured on ties can overstate its rounded time by one step without ever losing, and two such lies at one profile can push the make-span above the $(1+\varepsilon)$ bound. The approximation guarantee therefore has to be stated for the strategy class the proof identifies, not derived from dominance alone. The remaining steps require exact bookkeeping of rounding across sums and of the corrected time vectors, which a proof sketch leaves implicit.

Formalization scope

• Agents are Fin n with [NeZero n], tasks Fin k; allocations are functions Fin k → Fin n; the make-span is a Finset.sup' over agents. Types and declarations satisfy a ≤ t i j ≤ b with 0 < a < b; actual times are only bounded below by the true times.
• roundUp δ r = δ * ⌈r / δ⌉. The statement holds for every $\delta \in (0,\varepsilon a]$, which covers the intended choice $\delta = \varepsilon a$; the paper leaves $\delta$ as "a function of $a$ and $\varepsilon$".
• The Horowitz–Sahni dynamic program is not formalized. The allocation algorithm is a parameter with the hypothesis that it solves the rounded problem exactly; ties are arbitrary, and the goal holds for every such algorithm. Running time ("polynomial time") is out of scope, and with it the role of the upper bound $b$, which is kept as part of the problem.
• An execution is a function of the decision (Definition 18). Dominance quantifies over all declarations in $[a,b]$ and all executions of the others.
• The payment uses the allocation $x(d)$ in the bonus. Definition 34 prints $x(\hat t)$; since the rounding algorithm rounds the declarations itself, $x(d)$ is the allocation actually computed. The hat on $\mathrm{corr}$ is absorbed by $\hat g$.
• The goal's approximation part is restricted to dominant profiles of the class named in the proof, because the unrestricted form (Definition 3, every dominant profile) is false for some tie-breaking rules; an explicit two-agent, one-task instance is recorded in the goal's Formalization Note.
• A formalization that measures the approximation with declared rather than actual times, lets the allocation read the true types, or states the approximation only at the truthful profile while claiming the general form, does not formalize this theorem.

Useful infrastructure: lemmas on Int.ceil rounding of finite sums and on Finset.sup' monotonicity, and a reusable model of mechanisms with verification. Proofs of the milestones in any order are welcome.

Selected references

• N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
• E. Horowitz, S. Sahni, Exact and Approximate Algorithms for Scheduling Nonidentical Processors, Journal of the ACM 23 (1976) 317–327. https://doi.org/10.1145/321941.321951