All missions

Why the Nesterov–Todd scaling of a second-order cone matters

Conic quadratic (second-order cone) programs are solved in practice by primal-dual interior-point methods. Each iteration solves a Newton system for the central-path equations, and for non-polyhedral cones that system is only guaranteed to be well posed after the problem is scaled: the primal point $x$ and the dual slack $s$ are transformed by a matrix $\Theta W$ chosen from the current iterate. Among the scalings analysed by Monteiro and Tsuchiya (2000), the best complexity bounds are obtained with the Nesterov–Todd (NT) scaling of Nesterov and Todd (1997), which maps $x$ and $s$ to the same point.

Andersen, Roos and Terlaky (2003) describe the conic quadratic interior-point solver of MOSEK. Their Lemma 4.2 gives the NT scaling in closed form for each of the three cone types they use. It is what makes the NT direction cheap: each cone block of $W$ is determined by one vector $w$, and $W$, $W^2$ and their inverses can be applied in time linear in the dimension. For the quadratic cone the formula goes back to Tsuchiya (1999); the paper re-derives it and extends it to the rotated quadratic cone.

Setting

Fix one cone block of dimension $d$. Coordinates are $x = (x_1,\dots,x_d)$, $x_{k:d}$ denotes the subvector of coordinates $k,\dots,d$, and $\|\cdot\|$ is the Euclidean norm. The block is one of

• the positive half-line $\mathbb R_+$ ($d=1$), with $T = Q = 1$;
• the quadratic cone $K^q = \{x : x_1 \ge \|x_{2:d}\|\}$ ($d\ge1$), with $T = I$ and $Q = \operatorname{diag}(1,-1,\dots,-1)$;
• the rotated quadratic cone $K^r = \{x : 2x_1x_2 \ge \|x_{3:d}\|^2,\ x_1,x_2\ge0\}$ ($d\ge2$), with $T$ the identity except for the leading block $\tfrac1{\sqrt2}\begin{bmatrix}1&1\\1&-1\end{bmatrix}$, and $Q$ the matrix with $Q_{12} = Q_{21} = 1$, $Q_{jj} = -1$ for $j\ge3$, and zeros elsewhere.

A scaling matrix (Definition 3.3) is a symmetric positive definite $W$ with $WQW = Q$. For $\theta>0$ the scaled points are $\bar x = \theta W x$ and $\bar s = (\theta W)^{-1}s$. The pair $(\theta, W)$ is an NT scaling of $(x, s)$ when $\bar x = \bar s$, equation (28); equivalently $s = \theta^2W^2x$, equation (29).

Formalization targets

Goal: Lemma 4.2 (p. 15)

For $x, s$ in the interior of the cone:

1. every NT scaling satisfies

$$\theta^2 = \sqrt{\frac{s^TQs}{x^TQx}};\qquad(30)$$

2. with this $\theta$ and

$$w = \frac{\theta^{-1}s + \theta Qx}{\sqrt2\sqrt{x^Ts + \sqrt{x^TQx\,s^TQs}}},\qquad(32)$$

the following matrices $W$ make $(\theta, W)$ an NT scaling: $W = \theta^{-1}(X^{-1}S)^{1/2}$ for $\mathbb R_+$;

$$W = \begin{bmatrix} w_1 & w_{2:d}^T\\ w_{2:d} & I + \frac{w_{2:d}w_{2:d}^T}{1+w_1}\end{bmatrix} = -Q + \frac{(e_1+w)(e_1+w)^T}{1+e_1^Tw}\qquad(31)$$

for $K^q$; and

$$W = -Q + \frac{(Te_1+w)(Te_1+w)^T}{1+e_1^TTw}\qquad(34)$$

for $K^r$. In the last two cases $W^2 = -Q + 2ww^T$, equations (33) and (35).

Milestones

Lemma 3.3 i)–iii) (scaling preserves $x^Ts$ and rescales $x^TQx$, $s^TQs$ by $\theta^{\pm2}$); (30) on its own; the normalization $w_1^2 - \|w_{2:d}\|^2 = 1$ and the square (62) of the arrow form (31); positivity of the radicand of (32); the identity $2\theta^2(w^Tx)^2 = x^Ts + \sqrt{x^TQx\,s^TQs}$ and the formula (32); for the rotated cone, the transport (63) by $T$, the identities $\hat\theta = \theta$ and $\hat w = Tw$, and $TWT = \hat W$. Two companions: Lemma 4.3, $(\theta W)^{-2} = \theta^{-2}QW^2Q$, and Lemma 3.3 iv), that a scaling maps the cone and its interior onto themselves.

Significance

The result. Lemma 4.2 turns the NT scaling, defined implicitly by (28), into explicit data: one scalar $\theta$ and one vector $w$ per cone. Combined with Lemma 4.3 it shows that every product with $W$, $W^2$ or their inverses in the scaled Newton system (27) is a rank-one correction of a signature matrix, which is what the paper's implementation relies on. The rotated-cone formula (34) is the paper's own addition and is what lets rotated cones be handled natively instead of through a change of variables.

Formalizing it. The result is proved on paper; no machine-checked version is known to exist, and the platform has no formalization of second-order-cone scalings. The work is the matrix algebra of the Lorentz group — the signature matrix $Q$, the matrices with $WQW = Q$, and their action on $K^q$ and $K^r$ — which is reusable for every second-order-cone algorithm.

Difficulty

Most of the items are finite-dimensional identities, but they are identities between block matrices of arbitrary size with entries that are nested square roots, and they hold only on the interior of the cone, where the radicands are positive. The derivation in the paper runs backwards: it assumes $W$ has the shape (31) and solves for $w$, taking a square root without fixing its sign. The goal asks for the forward direction — that the displayed $\theta$, $w$, $W$ do satisfy (28) and $W\succ0$ — which needs the normalization $w^TQw = 1$, positive definiteness of $-Q + (e_1+w)(e_1+w)^T/(1+w_1)$, and, for the rotated cone, the reduction to the quadratic cone through $T$ with $TT = I$ and $TQ^rT = Q^q$.

Formalization scope

• Per block. Every statement is made for one cone block. $\Theta$ and $W$ are block diagonal (pp. 11–12), so this is the paper's statement block by block. The cone type is the parameter kind : ConeKind, and vectors are Fin d → ℝ.
• Index base and norms. The paper's $x_1$ is coordinate 0. $\|x_{2:d}\|^2$ is written as a sum of squares (tailSq x 1); Mathlib's norm on Fin d → ℝ, which is the sup norm, is never used.
• Interiors. The interiors are given by strict inequalities. The paper never defines $\operatorname{int}(K)$ concretely; these coincide with the topological interiors.
• Added hypotheses. All are disclosed in the items:
  • the dimension conventions ($d=1$ for $\mathbb R_+$, $d\ge1$ for $K^q$, $d\ge2$ for $K^r$), which the paper leaves implicit;
  • $\theta>0$ in Definition 3.3, which the paper calls positive definite on p. 24;
  • $1+w_1>0$ wherever the page divides by $1+w_1$;
  • $w^Tx>0$ for the last step of the derivation of (32), where the page silently fixes this sign.
• Inverses. The matrix inverse is Mathlib's total inverse. The NT predicate always contains $W\succ0$, so (28) never reads the junk value of a singular inverse.
• Reading of Lemma 4.2. The lemma names $\theta$ and $W$ without quantifying them. The goal states (30) for every NT scaling and asserts that the displayed formulas are an NT scaling. It does not claim that the NT scaling is unique, which the paper does not prove.
• Ruling out a trivial formalization. Stating only (30) would allow a version that holds vacuously if no NT scaling existed. Part 2 of the goal is what excludes this, and a sanity check exhibits $\theta = 1$, $W = I$ at $x = s = e_1$ in $K^q$ for $d=2$.

A complete development needs:

• the cone definitions and the matrices $T$, $Q$;
• Mathlib's Matrix.PosDef and Matrix.inv;
• elementary real square-root algebra.

Lemmas about $\{W : W\succ0,\ WQW = Q\}$ (closure under products and inverses, invariance of $K^q$) are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for positive definiteness of (31).

Selected references

• E. D. Andersen, C. Roos, T. Terlaky, On implementing a primal-dual interior-point method for conic quadratic optimization, Mathematical Programming 95 (2003) 249–277; authors' preprint of 18 Dec 2000. https://doi.org/10.1007/s10107-002-0349-3
• Yu. E. Nesterov, M. J. Todd, Self-scaled barriers and interior-point methods for convex programming, Mathematics of Operations Research 22(1) (1997) 1–42. https://doi.org/10.1287/moor.22.1.1
• R. D. C. Monteiro, T. Tsuchiya, Polynomial convergence of primal-dual algorithms for the second-order cone program based on the MZ-family of directions, Mathematical Programming 88(1) (2000) 61–83. https://doi.org/10.1007/PL00011378
• T. Tsuchiya, A convergence analysis of the scaling-invariant primal-dual path-following algorithms for second-order cone programming, Optimization Methods and Software 11–12 (1999) 141–182. https://doi.org/10.1080/10556789908805750
• F. Alizadeh, D. Goldfarb, Second-order cone programming, Mathematical Programming 95 (2003) 3–51. https://doi.org/10.1007/s10107-002-0339-5

Motivation

In a road or communication network, each user picks a route to minimize its own delay, without regard to the delay it imposes on others. The outcome is an equilibrium that is in general not socially optimal: Braess's paradox shows that adding a road can make every user worse off, and Pigou's two-link example shows that selfish users can incur a third more total delay than a central planner would. Transportation science has studied such equilibria since Wardrop (1952) and Beckmann, McGuire and Winsten (1956). The computer-science question of how much is lost, uniformly over all networks, was answered for linear delays by Roughgarden and Tardos in How Bad is Selfish Routing? (FOCS 2000; J. ACM 2002, doi:10.1145/506147.506153). Their bound became the first instance of the price of anarchy for nonatomic routing and the template for a large literature on the inefficiency of equilibria.

Timeline. Wardrop (1952) states the equilibrium principle. Beckmann et al. (1956) and Dafermos–Sparrow (1969) characterize equilibria and optima by convex programs. Koutsoupias and Papadimitriou (1999) introduce the worst-case ratio of equilibrium to optimum. Roughgarden and Tardos (2000/2002) prove the bound $4/3$ for linear latencies, tight by Pigou's example. Roughgarden (2003) and Correa, Schulz and Stier-Moses (2004) extend the analysis to general latency classes.

Setting

A network has finitely many edges $e$ and finitely many routes $P$; a route is the set of edges it uses, recorded by a $0/1$ incidence. There are $k$ commodities; each route serves one commodity $i$, and $\mathcal P_i$ is the set of routes serving $i$. Commodity $i$ has a positive rate $r_i$. A flow assigns a nonnegative amount $f_P$ to each route; it is feasible for $r$ if $\sum_{P\in\mathcal P_i}f_P=r_i$ for every $i$. The edge flow is $f_e=\sum_{P\ni e}f_P$.

Each edge has a linear latency $\ell_e(x)=a_ex+b_e$ with $a_e,b_e\ge0$. The latency of a route is $\ell_P(f)=\sum_{e\in P}\ell_e(f_e)$, and the cost of a flow is

$$C(f)=\sum_P\ell_P(f)\,f_P=\sum_e\ell_e(f_e)\,f_e .$$

A feasible flow is at Nash equilibrium if no small amount of flow on a route $P_1$ can reduce its latency by moving to another route $P_2$ of the same commodity (Definition 2.1); equivalently (Lemma 2.2), every used route of commodity $i$ has minimum latency among the routes in $\mathcal P_i$. A flow is optimal if it is feasible and has minimum cost among feasible flows. The marginal cost of edge $e$ is $\ell^*_e(x)=(x\ell_e(x))'=2a_ex+b_e$, and $L^*_i(f^*)=\min_{P\in\mathcal P_i}\sum_{e\in P}\ell^*_e(f^*_e)$.

The Lean development uses the names pathLatency, cost, IsNashFlow, IsOptimalFlow, linLatency, marginalLatency and minMarginalPathCost for these objects.

Formalization targets

Goal: Theorem 4.5

For every instance with linear latencies $a_e,b_e\ge0$, every Nash flow $f$ and every feasible flow $f^*$,

$$C(f)\le\tfrac43\,C(f^*).$$

This is the paper's $\rho(G,r,\ell)=C(f)/C(f^*)\le4/3$, stated without the ratio.

Milestones

1. Lemma 2.2: Nash flows are exactly the Wardrop flows (for continuous nondecreasing latencies).
2. Lemma 2.3: at a Nash flow, $C(f)=\sum_iL_i(f)\,r_i$, with $L_i(f)$ the common latency of the used routes of commodity $i$.
3. Lemma 4.1(a), (b): Nash and optimal flows for linear latencies, characterized by $\sum_{e\in P}(a_ef_e+b_e)$ and $\sum_{e\in P}(2a_ef^*_e+b_e)$ being minimal on used routes.
4. Corollary 4.2: for $\ell_e(x)=a_ex$, optimal and Nash flows coincide.
5. Lemma 4.3: if $f$ is a Nash flow for $r$ then $f/2$ is optimal for $r/2$, and $\ell^*_P(f/2)=\ell_P(f)$.
6. Lemma 4.4: if $f^*$ is optimal for $r$ and $\delta>0$, every flow feasible for $(1+\delta)r$ costs at least $C(f^*)+\delta\sum_iL^*_i(f^*)\,r_i$.
7. $C(f/2)\ge\frac14C(f)$ (proof of Theorem 4.5).
8. Figure 3: in Pigou's network the Nash flow costs $1$ and the optimal flow $3/4$, so the constant $4/3$ is attained.

Significance

The bound says that, with linear delays, selfish routing never costs more than $4/3$ times the optimum, independently of the network's size and topology and of the number of commodities. It explains why Braess-type phenomena are bounded in magnitude, and it yields consequences for mechanical networks of strings and springs (Corollary 4.6 of the paper). The inequality $C(f)\le\frac43C(f^*)$ for every feasible $f^*$ is the basic input to later work on bicriteria bounds, Stackelberg routing, tolls and the general price-of-anarchy framework.

The result is proved in the paper and in textbooks (Nisan et al., Algorithmic Game Theory, ch. 18). No machine-checked proof is known to exist on Prove2Me or in Mathlib. A formalization produces a checked model of nonatomic routing (route flows, Nash and optimal flows) together with the first-order characterization of optimal flows for convex quadratic costs, both of which are reusable for the other results of the paper and for later routing papers.

Difficulty

The equilibrium bound is not a pointwise inequality between the two flows: the Nash flow $f$ and an arbitrary feasible flow $f^*$ can use entirely different routes. The step that requires real work is the comparison between an optimal flow for the rates $r/2$ and an arbitrary flow for the rates $r$ (Lemma 4.4), which rests on the characterization of optimal flows of a convex program (Lemma 4.1(b)). That characterization is a Karush–Kuhn–Tucker statement over a polytope of route flows; the paper cites it rather than proving it, and Mathlib has no ready-made version. The naive approach, bounding each edge's cost separately, fails because the two flows load different edges.

Formalization scope

• Edges, routes and commodities are Fin J, Fin R, Fin Sd. A route is a $0/1$ column A j r of the incidence; the commodity of route r is s r. The paper's simple paths in a directed graph are one instance, so all statements are a disclosed generalization; copies of one path serving two commodities are two routes.
• Edge flows and feasibility are the published KellyStochasticNetworks.linkFlow and KellyStochasticNetworks.wardropFeasible; the Wardrop condition is KellyStochasticNetworks.IsWardropEquilibrium.
• All rates are positive (0 < rate i), as on p. 6. Linear latencies have $a_e,b_e\ge0$, and only their values at nonnegative arguments matter.
• Definition 2.1 is formalized for distinct routes $P_1\neq P_2$ and $0<\delta\le f_{P_1}$. The literal $P_1=P_2$ would make Nash flows nonexistent, and the literal $\delta=0$ on an unused $P_1$ would force equal latencies on unused routes; both readings would make the theorems vacuous or false.
• Lemmas 2.2 and 2.3 are stated for arbitrary latencies that are nonnegative, nondecreasing and continuous on $[0,\infty)$; continuity replaces differentiability, as the paper's footnote 3 allows.
• The ratio $\rho$ is never formed: $C(f^*)$ may be $0$ and Lean's division returns $0$ there. Every bound is stated as an inequality against every feasible flow.
• $L^*_i$ is a minimum over the nonempty finite set of routes serving $i$; $L_i(f)$ in Lemma 2.3 is stated existentially.
• A trivializing formalization (a Nash definition no flow satisfies, a ratio with junk denominator, or a single-commodity or parallel-link special case) is ruled out by the choices above; Pigou's flow $(0,1)$ is checked to satisfy the formal Nash definition.

Needed infrastructure: the edge/route exchange of summation, the first-order optimality conditions for a convex differentiable function on a product of simplices, and the convexity inequality $x\ell_e(x)\ge y\ell_e(y)+(x-y)\ell^*_e(y)$. Contributions of a general KKT lemma for separable convex costs on flow polytopes are reusable beyond this mission.

Selected references

• T. Roughgarden and É. Tardos, How Bad is Selfish Routing?, Journal of the ACM 49(2), 236–259, 2002. https://doi.org/10.1145/506147.506153
• J. G. Wardrop, Some theoretical aspects of road traffic research, Proc. Institution of Civil Engineers, Part II, 1, 325–378, 1952. https://doi.org/10.1680/ipeds.1952.11259
• M. Beckmann, C. B. McGuire and C. B. Winsten, Studies in the Economics of Transportation, Yale University Press, 1956.
• S. C. Dafermos and F. T. Sparrow, The traffic assignment problem for a general network, J. Research of the National Bureau of Standards 73B(2), 91–118, 1969. https://doi.org/10.6028/jres.073B.010
• E. Koutsoupias and C. Papadimitriou, Worst-case equilibria, STACS 1999, LNCS 1563, 404–413. https://doi.org/10.1007/3-540-49116-3_38
• T. Roughgarden, The price of anarchy is independent of the network topology, J. Computer and System Sciences 67(2), 341–364, 2003. https://doi.org/10.1016/S0022-0000(03)00044-8

Motivation

Many problems in system identification, collaborative filtering, low-dimensional embedding and model reduction ask for the simplest matrix consistent with a set of linear observations, where "simplest" means "of least rank". Given a linear map $\mathcal A:\mathbb R^{m\times n}\to\mathbb R^p$ and a vector $b\in\mathbb R^p$, the affine rank minimization problem is

$$\min_X\ \operatorname{rank}(X)\quad\text{s.t.}\quad \mathcal A(X)=b .$$

This problem is NP-hard in general: it contains the problem of finding the sparsest solution of a linear system as the special case of diagonal matrices. A standard heuristic, popularized in control by Fazel, Hindi and Boyd, replaces the rank by the nuclear norm $\|X\|_*$, the sum of the singular values, which is the convex envelope of the rank on the unit ball of the operator norm. The resulting problem is a semidefinite program and can be solved efficiently.

Recht, Fazel and Parrilo (arXiv:0706.4138, SIAM Review 2010) gave the first general conditions under which this heuristic provably returns the minimum-rank solution. Their argument transfers the compressed sensing theory of Candès and Tao (Decoding by linear programming, 2005) and Candès, Romberg and Tao from sparse vectors and the $\ell_1$ norm to low-rank matrices and the nuclear norm. This mission formalizes the paper's deterministic recovery theorem (Section 3).

Setting

Matrices are real $m\times n$ matrices. For matrices $X,Y$ of the same size, $\langle X,Y\rangle=\operatorname{Tr}(X^{\top}Y)=\sum_{i,j}X_{ij}Y_{ij}$ is the trace inner product. With $\sigma_1(X)\ge\sigma_2(X)\ge\dots\ge0$ the singular values of $X$, the three norms used are the operator norm $\|X\|=\sigma_1(X)$, the Frobenius norm $\|X\|_F=\sqrt{\langle X,X\rangle}=(\sum_i\sigma_i(X)^2)^{1/2}$, and the nuclear norm $\|X\|_*=\sum_i\sigma_i(X)$.

A linear map $\mathcal A:\mathbb R^{m\times n}\to\mathbb R^p$ is given by $p$ measurement matrices $A_1,\dots,A_p$ through $\mathcal A(X)_i=\langle A_i,X\rangle$; $\|\mathcal A(X)\|$ is the Euclidean norm of the vector $\mathcal A(X)\in\mathbb R^p$.

For an integer $r$, the $r$-restricted isometry constant $\delta_r(\mathcal A)$ (Definition 3.1) is the smallest $\delta\ge0$ with

$$(1-\delta)\,\|X\|_F\le\|\mathcal A(X)\|\le(1+\delta)\,\|X\|_F\qquad\text{for every } X \text{ with } \operatorname{rank}X\le r .$$

Fix a matrix $X_0$ of rank at most $r$, put $b=\mathcal A(X_0)$, and consider the nuclear norm minimization problem

$$X^*:=\arg\min_X\ \|X\|_*\quad\text{s.t.}\quad\mathcal A(X)=b. \tag{3.1}$$

Formalization targets

Goal: Theorem 3.3

If $r\ge1$ and $\delta_{5r}(\mathcal A)<\tfrac1{10}$, then $X^*=X_0$; precisely,

$$\forall X\in\mathbb R^{m\times n}:\quad \mathcal A(X)=\mathcal A(X_0)\ \text{ and }\ \|X\|_*\le\|X_0\|_*\ \Longrightarrow\ X=X_0 .$$

The statement holds for every linear map, every $m,n,p$ and every $X_0$ of rank at most $r$. The constant $1/10$ is the paper's; the paper notes (p. 14) that its derivation is chosen for simplicity and is not optimal.

Milestones, in the paper's order

1. Theorem 3.2 (p. 12): if $\delta_{2r}<1$, then $X_0$ is the only matrix of rank at most $r$ with $\mathcal A(X)=b$.
2. (2.1) (p. 6): $\|X\|\le\|X\|_F\le\|X\|_*\le\sqrt r\,\|X\|_F\le r\,\|X\|$ whenever $\operatorname{rank}X\le r$.
3. Lemma 2.3 (p. 9): if $AB^{\top}=0$ and $A^{\top}B=0$, then $\|A+B\|_*=\|A\|_*+\|B\|_*$.
4. Lemma 3.4 (pp. 12–13): every $B$ splits as $B=B_1+B_2$ with $\operatorname{rank}B_1\le2\operatorname{rank}A$, $AB_2^{\top}=0$, $A^{\top}B_2=0$ and $\langle B_1,B_2\rangle=0$.
5. (3.3)–(3.4) (p. 13): for the error $R=R_0+R_c$ of a minimizer, $\|R_c\|_*\le\|R_0\|_*$.
6. (3.5)–(3.6) (p. 13): a matrix splits into pairwise orthogonal pieces of rank at most $3r$ whose Frobenius norms, from the second piece on, sum to at most $\|M\|_*/\sqrt{3r}$.
7. Monotonicity (p. 12): $\delta_r\le\delta_{r'}$ for $r\le r'$.
8. (3.7) (p. 14): $\|\mathcal A(R)\|\ge\big((1-\delta_{5r})-\tfrac9{11}(1+\delta_{3r})\big)\|R_0\|_F$, with a positive factor whenever $9\delta_{3r}+11\delta_{5r}<2$.

Significance

Theorem 3.3 is a deterministic certificate: it separates the question "does nuclear norm minimization recover low-rank matrices?" into a property of the measurement map alone, with an absolute constant independent of $m$, $n$, $r$ and $p$. Section 4 of the same paper then shows that random maps with i.i.d. Gaussian or Bernoulli entries satisfy $\delta_{5r}<1/10$ with high probability once $p$ is of order $r(m+n)\log(mn)$, so a matrix with $mn$ entries is determined by far fewer measurements than entries and is found by a semidefinite program.

The theorem is proved in the paper, and the sparse-vector analogue has been formalized on this platform (HighDimProb.SparseRecovery.rip_implies_exact_recovery, from Vershynin's textbook; CandesTao.Decoding.decoding_by_lp). The matrix version is not formalized. A machine-checked proof needs the basic theory of singular values for rectangular real matrices (the norm comparisons (2.1), additivity of the nuclear norm, the triangle inequality for the nuclear norm, and block decompositions via the singular value decomposition), most of which Mathlib lacks in this form. That infrastructure is reusable for every nuclear-norm result on the platform.

Difficulty

For sparse vectors the analogous proof splits the error vector by its support, and every step is coordinatewise. For matrices there is no common basis: the error $R$ and the target $X_0$ have different singular vectors, and the restricted isometry inequality controls only matrices of low rank. The first obstacle is therefore to split $R$ into a piece of rank at most $2\operatorname{rank}X_0$ and a piece whose row and column spaces are orthogonal to those of $X_0$, so that the nuclear norm is additive. The second is that the triangle inequality, additivity and the norm chain (2.1) for the nuclear norm are themselves nontrivial statements about singular values. Applying the restricted isometry inequality directly to $R$ fails, because $R$ need not have low rank.

Formalization scope

• Matrices are Matrix (Fin m) (Fin n) ℝ; rank is Matrix.rank; transpose is Xᵀ. The norms and the inner product are opNorm, frobeniusNorm, nuclearNorm and traceInner of the published module HighDimStat_MatrixRank_Core, which defines the nuclear norm as the sum of the square roots of the eigenvalues of $X^{\top}X$.
• The map $\mathcal A$ is given by Xs : Fin p → Matrix (Fin m) (Fin n) ℝ and evaluated by observationOp; measNorm Xs X is $\|\mathcal A(X)\|$.
• ripConst Xs r is the infimum of the admissible $\delta\ge0$; the set is nonempty and closed, so the infimum is attained. It is defined for every $r$, not only $1\le r\le m$, since the goal uses $\delta_{5r}$. The paper's normalization $m\le n$ is not assumed.
• The goal assumes $\operatorname{rank}X_0\le r$ rather than $=r$ (equivalent by monotonicity of $\delta$). Its conclusion quantifies over all feasible $X$ with $\|X\|_*\le\|X_0\|_*$, so it does not depend on a choice of arg min. A formalization that fixes some minimizer unrelated to $b$, or only asserts the existence of a minimizer equal to $X_0$, would be trivial and is excluded.
• Milestone (3.5)–(3.6) is stated existentially, listing the properties of the singular value blocks that the proof uses, because Mathlib has no ordered rectangular singular value decomposition. Milestone (3.7) makes explicit the orthogonality $\langle R_0,R_1\rangle=0$ that the paper uses silently.

Welcome contributions: a rectangular SVD with ordered singular values, the triangle inequality and duality for nuclearNorm, and the attainment and monotonicity lemmas for ripConst.

Selected references

• B. Recht, M. Fazel, P. A. Parrilo, Guaranteed Minimum-Rank Solutions of Linear Matrix Equations via Nuclear Norm Minimization, SIAM Review 52(3), 471–501, 2010. https://doi.org/10.1137/070697835 ; preprint arXiv:0706.4138v1. https://arxiv.org/abs/0706.4138
• E. J. Candès, T. Tao, Decoding by Linear Programming, IEEE Trans. Inform. Theory 51(12), 2005. https://doi.org/10.1109/TIT.2005.858979
• E. J. Candès, J. Romberg, T. Tao, Stable Signal Recovery from Incomplete and Inaccurate Measurements, Comm. Pure Appl. Math. 59(8), 2006. https://doi.org/10.1002/cpa.20124
• M. Fazel, Matrix Rank Minimization with Applications, PhD thesis, Stanford University, 2002.
• R. Vershynin, High-Dimensional Probability, Cambridge University Press, 2018, §10.5. https://doi.org/10.1017/9781108231596

Motivation

The support vector machine (SVM) is a linear classifier trained by minimising a regularised hinge loss. For training sets with millions of examples, solving the SVM problem to high accuracy by interior-point or dual decomposition methods is too slow, and what is needed is an algorithm whose cost per iteration does not grow with the number of examples. Pegasos (Primal Estimated sub-GrAdient SOlver for SVM), introduced by Shalev-Shwartz, Singer and Srebro in 2007 and analysed in its final form by Shalev-Shwartz, Singer, Srebro and Cotter in Mathematical Programming (2011, doi:10.1007/s10107-010-0420-4), is a stochastic sub-gradient method on the primal SVM objective with step size $1/(\lambda t)$. Its analysis showed that the number of iterations needed for accuracy $\epsilon$ is $\tilde O(1/(\lambda\epsilon))$, independent of the training-set size, and the method became a standard baseline for large-scale linear SVM training.

The analysis rests on a logarithmic-regret bound for online gradient descent on strongly convex functions, due to Hazan, Agarwal and Kale (Machine Learning 69, 2007), which the paper re-proves for non-smooth functions as its Lemma 1 and then applies to the Pegasos iterates in its Theorem 1.

Setting

A training set consists of $m$ examples $(x_i, y_i)$, $i\in[m]$, with $x_i\in\mathbb R^n$ and labels $y_i\in\{+1,-1\}$. The hinge loss of a weight vector $w$ on $(x,y)$ is $\ell(w;(x,y)) = \max\{0,\,1 - y\langle w, x\rangle\}$. For a regularisation parameter $\lambda>0$, the SVM objective (Eq. (1)) is

$$f(w) = \frac\lambda2\|w\|^2 + \frac1m\sum_{i=1}^m \ell(w;(x_i,y_i)),$$

and $w^\star$ denotes a minimiser of $f$ (Eq. (9)). For a mini-batch $A$ of $k\ge1$ example indices, the instantaneous objective (Eq. (7)) is

$$f(w;A) = \frac\lambda2\|w\|^2 + \frac1k\sum_{i\in A}\ell(w;(x_i,y_i)).$$

Mini-batch Pegasos (Fig. 2 of the paper) starts at $w_1 = 0$. At each round $t = 1, 2, \dots$ it receives a mini-batch $A_t$, forms the sub-gradient

$$\nabla_t = \lambda w_t - \frac1k\sum_{i\in A_t}\mathbb 1\bigl[y_i\langle w_t, x_i\rangle < 1\bigr]\,y_i x_i \qquad (8)$$

of $f(\cdot;A_t)$ at $w_t$, and sets $w_{t+1} = w_t - \eta_t\nabla_t$ with $\eta_t = 1/(\lambda t)$. Optionally it then applies the projection step (6), $w_{t+1}\leftarrow\min\{1,(1/\sqrt\lambda)/\|w_{t+1}\|\}\,w_{t+1}$, which maps $w_{t+1}$ to the closest point of the Euclidean ball of radius $1/\sqrt\lambda$. A function $g$ is $\lambda$-strongly convex if $g(w) - \frac\lambda2\|w\|^2$ is convex, and $v$ is a sub-gradient of a convex $g$ at $w_0$ if $g(w) - g(w_0)\ge\langle v, w - w_0\rangle$ for every $w$.

In the Lean development these objects are svmObj, instObj, subgrad, projBall and run in the namespace Pegasos.Analysis; the hinge loss is UnderstandingML.hingeLoss, sub-gradients are UnderstandingML.IsSubgradient, and "$z$ is the projection of $v$ onto $B$" is LogRegretOCO.OGD.IsProj B v z.

Formalization targets

Goal: Theorem 1

Assume $\|x_i\|\le R$ for every $i$, and set $c = (\sqrt\lambda + R)^2$ when the projection step is performed and $c = 4R^2$ when it is not. Then for every sequence of mini-batches and every $T\ge3$,

$$\frac1T\sum_{t=1}^T f(w_t;A_t) \;\le\; \frac1T\sum_{t=1}^T f(w^\star;A_t) + \frac{c\,(1+\ln T)}{2\lambda T}.$$

The constants are the paper's and are stated exactly; a version with a single constant for both variants, or with an unspecified constant, is a weaker theorem.

Milestones

1. Eq. (10): for $\lambda$-strongly convex $g$ with sub-gradient $v$ at $w$, $\langle w - u, v\rangle\ge g(w) - g(u) + \frac\lambda2\|w-u\|^2$.
2. Eq. (11): one projected step satisfies $\langle w_t - u,\nabla_t\rangle\le\frac{\|w_t-u\|^2 - \|w_{t+1}-u\|^2}{2\eta_t} + \frac{\eta_t}2G^2$ (an already-proved platform theorem, stated with a factor 2).
3. Lemma 1: projected sub-gradient steps $\eta_t = 1/(\lambda t)$ on $\lambda$-strongly convex $f_t$ with $\|\nabla_t\|\le G$ satisfy $\frac1T\sum f_t(w_t)\le\frac1T\sum f_t(u) + \frac{G^2(1+\ln T)}{2\lambda T}$ for all $u\in B$.
4. The vector (8) is a sub-gradient of $f(\cdot;A)$; $f(\cdot;A)$ is $\lambda$-strongly convex; the projection step (6) is the projection onto the ball of radius $1/\sqrt\lambda$.
5. The gradient bounds: $\|\nabla_t\|\le\sqrt\lambda + R$ with projection; Eq. (13), $w_{t+1} = \frac1{\lambda t}\sum_{i\le t}v_i$, and $\|\nabla_t\|\le 2R$ without.
6. $\|w^\star\|\le 1/\sqrt\lambda$.

Significance

Theorem 1 is the deterministic core of every guarantee in the paper. Taking expectations over uniformly random mini-batches turns its left side into the expected objective of the iterates and its right side into $f(w^\star)$ plus the rate, which yields the $\tilde O(1/(\lambda\epsilon))$ iteration bound and, via Markov-type arguments, the high-probability bounds of the later sections. Because the bound holds for every sequence of mini-batches, it is also an online-learning regret bound for the sequence of instantaneous objectives.

The result is proved in the paper and is classical. To our knowledge it has no machine-checked proof. Formalizing it produces a verified logarithmic-regret lemma for non-smooth strongly convex sub-gradient descent with an arbitrary closed convex feasible set (the platform currently has the twice-differentiable version with a bounded feasible set), a verified sub-gradient calculus for the regularised hinge loss, and an exact treatment of the Pegasos iteration including both the projected and unprojected variants.

Difficulty

The obvious argument applies Lemma 1 with $B$ the ball of radius $1/\sqrt\lambda$ in both variants and $G$ the sup of $\|\nabla_t\|$ over that ball. This fails twice. Without the projection step the iterates are not confined to that ball, so a separate argument (the closed form (13)) is needed to bound them, and it gives the different constant $4R^2$. With projection, Lemma 1 requires the comparator $w^\star$ to lie in the ball, and $\|w^\star\|\le1/\sqrt\lambda$ is not implied by the elementary comparison $f(w^\star)\le f(0)\le1$, which only gives $\|w^\star\|\le\sqrt{2/\lambda}$; the paper obtains the sharp radius through duality. In Lemma 1 itself, the telescoping only closes because the step size $1/(\lambda t)$ is matched exactly to the strong-convexity modulus; any off-by-one in the step indexing breaks the cancellation.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin n), examples are indexed by Fin m, labels are real numbers with the hypothesis $y_i\in\{+1,-1\}$, and $\lambda>0$, $k\ge1$ are hypotheses. A mini-batch is a $k$-tuple Fin k → Fin m: an injective tuple is a subset of size $k$ as in Fig. 2, a non-injective one is the multi-set with repetitions the paper also allows. The theorem is stated for every sequence of mini-batches A : ℕ → Fin k → Fin m; no probability space appears, because the proof never uses that the batches are random. Iterations are 1-based: run … 1 = 0, the step producing $w_{t+1}$ uses $\eta_t = 1/(\lambda t)$ and the batch $A_t$ only, and index 0 is unused. The variant is selected by a Boolean flag, and $c$ depends on it. $w^\star$ is any $w$ with $f(w^\star)\le f(w)$ for all $w$, minimising the full objective (1), not the instantaneous ones. Strong convexity is the paper's own definition, convexity of $g - \frac\lambda2\|\cdot\|^2$. At $w = 0$ the projection formula is evaluated with Lean's $a/0 = 0$, which gives the intended value $0$. The paper's display (12) has two printed slips (the sign of the $v_t$ term and $x_t$ for $x_i$); the Lean states the correct update, and Eq. (13) is correct as printed.

A trivializing formalization is ruled out: the goal is stated for the concrete iteration run, not for an abstract sequence assumed to be sub-gradient steps or projections, and those facts are separate milestones.

A complete development needs the sub-differential sum rule for a convex function plus a quadratic, convexity of the hinge loss, the variational characterisation of the projection onto a ball, the harmonic-sum bound $\sum_{t\le T}1/t\le1+\ln T$, and a proof of $\|w^\star\|\le1/\sqrt\lambda$ (through duality or a direct optimality argument). Lemma 1 and the sub-gradient lemmas are reusable for any strongly convex stochastic sub-gradient method. Proofs of any milestone, and alternative proofs of the bound on $\|w^\star\|$ that avoid the dual problem, are welcome.

Selected references

• S. Shalev-Shwartz, Y. Singer, N. Srebro, A. Cotter, Pegasos: primal estimated sub-gradient solver for SVM, Mathematical Programming Ser. B 127 (2011) 3–30. https://doi.org/10.1007/s10107-010-0420-4
• E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69 (2007) 169–192. https://doi.org/10.1007/s10994-007-5016-8
• S. Shalev-Shwartz, Y. Singer, N. Srebro, Pegasos: primal estimated sub-gradient solver for SVM, ICML 2007. https://doi.org/10.1145/1273496.1273598

Motivation

Scheduling jobs on identical parallel machines to minimize the total weighted completion time $\sum_j w_jC_j$, the problem $P\,|\,|\sum w_jC_j$, is one of the basic NP-hard problems of machine scheduling. On a single machine it is solved by Smith's ratio rule (Smith 1956); with several machines the only hard decision is which jobs share a machine. Section 6 of M. Skutella's paper Convex quadratic and semidefinite programming relaxations in scheduling (J. ACM 48 (2001)) observes that this decision is a graph partitioning problem: the cost of a schedule is, up to a constant, the weight of the edges that a partition of a weighted complete graph does not cut. Minimizing $\sum_j w_jC_j$ on $m$ machines is therefore equivalent to Max-$m$-Cut on that graph, and the paper shows that the equivalence preserves approximation in a quantified way.

The reduction explains, from the graph side, why semidefinite rounding works for two machines: with the 0.878-approximation for MaxCut of Goemans and Williamson (1995) it gives a 1.122-approximation for $P2\,|\,|\sum w_jC_j$ (Corollary 6.2 of the paper). For general $m$, the uniform random partition is both a $(1-1/m)$-approximation for Max-$m$-Cut and randomized rounding of the optimum of the convex quadratic relaxation (CQP).

Setting

There are $n$ jobs $J=\{1,\dots,n\}$ and $m\ge 1$ identical machines. Job $j$ has a processing time $p_j>0$ and a weight $w_j\ge 0$. Smith's order $\prec$ puts $j\prec k$ when $w_j/p_j>w_k/p_k$, ties broken by index. An assignment $\sigma:J\to\{1,\dots,m\}$ is a partition $J_1,\dots,J_m$ of the jobs; each machine processes its jobs in the order $\prec$ without idle time, so the completion time of $j$ is

$$C_j(\sigma)=p_j+\sum_{k\prec j,\ \sigma(k)=\sigma(j)}p_k .$$

The value of $\sigma$ is $\sum_j w_jC_j(\sigma)$, and $Z^*$ is the minimum value over all assignments.

The graph $G_J$ is the complete graph on $J$ in which the edge $\{j,k\}$ with $k\prec j$ has weight $c(jk)=w_jp_k$; $c(E_J)$ is its total weight. A partition induces the $m$-cut $E_{\mathrm{cut}}$, the edges whose endpoints lie in different parts, of weight $c(E_{\mathrm{cut}})$; $Z^*_{\mathrm{cut}}$ is the maximum weight of an $m$-cut.

The convex quadratic relaxation (CQP) of §2.2, specialised to identical machines, has variables $a_{ij}\ge 0$ with $\sum_i a_{ij}=1$ and objective $Z_{CQP}(a)=\sum_j w_jC_j$ where

$$C_j=\sum_{i=1}^m a_{ij}\Big(\frac{1+a_{ij}}{2}\,p_j+\sum_{k\prec j}a_{ik}\,p_k\Big)\qquad(11).$$

Its optimum value is $Z^*_{CQP}$.

Formalization targets

Goal: Theorem 6.1

For $\rho\le 1$, any assignment $\sigma$ whose $m$-cut weighs at least $\rho\cdot Z^*_{\mathrm{cut}}$ satisfies

$$\sum_j w_jC_j(\sigma)\le\big(\rho+m(1-\rho)\big)\,Z^* .$$

That is, a $\rho$-approximation algorithm for Max-$m$-Cut translates into a $(\rho+m(1-\rho))$-approximation algorithm for $Pm\,|\,|\sum w_jC_j$. The constant $\rho$ is a parameter, so the goal does not depend on the best known cut algorithm.

Milestones

1. (36): for every partition, $c(E_J)=\sum_j w_jC_j-\sum_j w_jp_j+c(E_{\mathrm{cut}})$.
2. Lemma 2.5: $\bar a_{ij}=1/m$ is an optimum of (CQP), unique when the ratios $w_j/p_j$ are pairwise different and positive.
3. (37): $Z^*\ge Z^*_{CQP}=\frac1m c(E_J)+\big(\frac12+\frac1{2m}\big)\sum_j w_jp_j$.
4. (38): $Z^*_{\mathrm{cut}}\le\frac{m-1}{m}c(E_J)+\big(\frac12-\frac1{2m}\big)\sum_j w_jp_j$.
5. Theorem 2.6 b) (supplementary): assigning each job independently and uniformly at random has expected value at most $\big(\frac32-\frac1{2m}\big)Z^*$.

Significance

The result. Theorem 6.1 makes Max-$m$-Cut algorithms usable for scheduling with an explicit loss: a cut algorithm with ratio $\rho$ close to $1$ yields a schedule within $1+m(1-\rho)$ of optimal. For $m=2$ and the Goemans–Williamson ratio $0.878$ the guarantee is $1.122$, better than the $5/4$ of Theorem 2.6 b) and the $1.2752$ of the paper's semidefinite rounding in §5. In the other direction, (38) bounds the maximum cut of $G_J$ by the scheduling lower bound $Z^*_{CQP}$, which is how a relaxation for scheduling becomes a bound for a cut problem. The problem itself is better understood today: $P\,|\,|\sum w_jC_j$ has a polynomial-time approximation scheme (Skutella and Woeginger 2000), and a fully polynomial one for fixed $m$ (Sahni 1976). The reduction remains of interest as a structural identity between the two problems and as the source of the closed-form relaxation bound (37).

Formalizing it. All statements are proved in the paper; none is known to have a machine-checked proof. The mission produces a formal model of identical-machine scheduling under Smith's rule, of the weighted graph $G_J$ and its $m$-cuts, and of (CQP) for identical machines, together with the closed-form optimum of (CQP) (Lemma 2.5), which is the basis of the $\frac32-\frac1{2m}$ guarantee of Theorem 2.6 b).

Difficulty

The bookkeeping identity (36) and the final chain of inequalities are finite-sum manipulations. The substance is Lemma 2.5: that the uniform vector $\bar a$ minimizes the quadratic objective (11) over the product of simplices. The objective is not separable, since the term $\sum_{k\prec j}a_{ik}p_k$ couples jobs through Smith's order, and its convexity on the feasible region (the positive semidefiniteness established in Lemma 2.4 of the paper) is the fact on which optimality and, with distinct positive ratios, uniqueness rest. The relaxation half of (37), that $Z^*_{CQP}$ is at most the value of every schedule, needs the observation that $Z_{CQP}$ evaluated at the 0/1 vector of an assignment equals the value of that assignment.

Formalization scope

Jobs are Fin n and machines Fin m, 0-based; Smith's order is cross-multiplied ($w_jp_k>w_kp_j$, or equality and $j<k$), equal to the ratio definition because $p>0$. Assignments are functions Fin n → Fin m, and every machine is sequenced by $\prec$; by Smith's rule (p. 7 of the paper, a classical result it cites) this loses no optimality, so $Z^*$ is the minimum over assignments and is never a primitive: "within factor $\alpha$ of $Z^*$" is stated against the value of every assignment. Likewise "weight at least $\rho\cdot Z^*_{\mathrm{cut}}$" is stated as $\rho\,c(E_{\mathrm{cut}}(\tau))\le c(E_{\mathrm{cut}}(\sigma))$ for every assignment $\tau$, so no supremum of an empty or unbounded set can enter. The edge weight is attached to the ordered pair $(j,k)$ with $k\prec j$ and is zero on the other orientation, so each edge of $G_J$ is counted once. Standing hypotheses on every theorem: $p_j>0$, $w_j\ge 0$ (p. 2 of the paper) and $m>0$ (needed for $1/m$). Theorem 6.1 keeps the page's $\rho\le 1$.

Not formalized: polynomial running time, the phrase "approximation algorithm" beyond the value bound it asserts, and the semidefinite results of §5 and Corollary 6.2. A trivializing reading, such as stating the cut condition against a junk-valued supremum or replacing $Z^*$ by a free variable, is excluded by the encodings above.

The development needs only finite sums over Fin types and real arithmetic; the model of identical-machine scheduling under Smith's rule and the closed form of (CQP) are reusable for other results on $P\,|\,|\sum w_jC_j$. Proofs of the milestones, alternative proofs of Lemma 2.5 (the KKT argument the paper mentions, or Goemans' symmetrization argument it gives), and a proof of Theorem 2.6 b) are all welcome.

Selected references

• M. Skutella, Convex quadratic and semidefinite programming relaxations in scheduling, Journal of the ACM 48(2), 2001. https://doi.org/10.1145/375827.375840
• W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3, 1956. https://doi.org/10.1002/nav.3800030106
• M. X. Goemans and D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, Journal of the ACM 42(6), 1995. https://doi.org/10.1145/227683.227684
• A. Frieze and M. Jerrum, Improved approximation algorithms for MAX k-CUT and MAX BISECTION, Algorithmica 18, 1997. https://doi.org/10.1007/BF02523689
• M. Skutella and G. J. Woeginger, A PTAS for minimizing the total weighted completion time on identical parallel machines, Mathematics of Operations Research 25(1), 2000. https://doi.org/10.1287/moor.25.1.63.15212
• S. Sahni, Algorithms for scheduling independent tasks, Journal of the ACM 23(1), 1976. https://doi.org/10.1145/321921.321934

Motivation

Retailers in many categories accept returns of products that are not defective: a consumer buys, learns whether the product suits them, and may send it back for a refund. Returns of this kind are a large cost item in retailing, and the refund a retailer offers is an operational decision on a par with its price and its stocking quantity. Xuanming Su, Consumer Returns Policies and Supply Chain Performance (SSRN 1020451, version of August 2008; published in Manufacturing & Service Operations Management 11(4), 2009, doi:10.1287/msom.1080.0240), studies this decision first for a single seller and then in a supply chain.

This mission formalizes the supply chain part, Section 5 of the paper. A classical result of supply chain contracting is that a manufacturer can align a retailer's ordering decision with the interest of the whole chain by a buy-back contract, which pays the retailer a credit for unsold units (Cachon, Supply Chain Coordination with Contracts, 2003). Su shows that once the retailer also sets a consumer returns policy, the standard buy-back no longer coordinates, and identifies three contracts that do. The companion mission (mission 1 of this series) formalizes the single-seller results of Sections 3–4, in particular Proposition 2, which gives the supply chain optimum used here.

Setting

A consumer who buys at price $p$ learns a valuation $V$, drawn independently from a law $\nu$ with finite mean $\mu = EV$, and then either keeps the product or returns it for the refund $r$. Keeping is optimal when $V \ge r$. Write

$$\bar G(r) = \mathbb P(V \ge r), \qquad G(r) = \mathbb P(V < r),$$

for the probabilities of keeping and returning. A consumer's expected utility from buying is $E\max(V,r)$, which is therefore the reservation price: all consumers buy if $p \le E\max(V,r)$ and none buys otherwise (the demand rule (6)). Market demand $X \ge 0$ has distribution function $F$ and $\bar F = 1 - F$; a stock $q \ge 0$ sells $E\min(X,q)$ in expectation when consumers buy, and nothing when they do not. Write $S(p,q,r)$ for these expected sales. The production cost is $c$, leftover and returned units are salvaged at $s$, and $0 \le s < c < \mu$.

The total supply chain profit is

$$\Pi_T(p,q,r) = [(p-s)\bar G(r) + (p-r)G(r)]\,S(p,q,r) - (c-s)q. \tag{15}$$

A manufacturer sells to a retailer, who sets $p$, $q$ and (except in Proposition 4) $r$. The contracts are:

• standard buy-back $(w,b)$: wholesale price $w$, credit $b$ per leftover unit; the retailer earns (14);
• differentiated buy-back $(w,b,l)$: credit $b$ per unsold unit and $b-l$ per returned unit; the retailer earns

$$\Pi_R(p,q,r) = [(p-b)\bar G(r) + (p-r-l)G(r)]\,S(p,q,r) - (w-b)q; \tag{31}$$

• direct-to-manufacturer returns with a buy-back $(w,b)$: consumers return to the manufacturer, who sets $r$; the profits are (19) and (21);
• sales rebate $(w,u)$: a rebate $u$ per unit sold, returned or not; the retailer earns (25).

The supply chain optimum, from Proposition 2 of the paper, is

$$p^{SC} = E\max(V,s), \qquad \bar F(q^{SC}) = \frac{c-s}{E\max(V,s)-s}, \qquad r^{SC} = s.$$

Formalization targets

Goal: Proposition 3 (p. 16)

For $\phi \in [0,1]$ and $\bar\phi = 1-\phi$, the differentiated buy-back

$$w = \phi c + \bar\phi\,E\max(V,s), \qquad b = \phi s + \bar\phi\,E\max(V,s), \qquad b - l = s$$

makes the supply chain optimum a retailer optimum and gives the retailer the share $\phi$:

$$\Pi_R(p,q,r) \le \Pi_R(p^{SC},q^{SC},r^{SC}) \ \ \forall p, r,\ q \ge 0, \qquad \Pi_R(p^{SC},q^{SC},r^{SC}) = \phi\,\Pi_T(p^{SC},q^{SC},r^{SC}),$$

and the contract is implementable: $w \ge b$, $l \ge 0$, $b - l \ge s$.

Milestones

1. Under a standard buy-back the retailer's optimal refund is $r^* = b$ (Sec. 5.1, p. 15).
2. Under (31) the retailer's optimum is $p^* = E\max(V,b-l)$, $\bar F(q^*) = (w-b)/(E\max(V,b-l)-b)$, $r^* = b-l$ (proof of Proposition 3, p. 27).
3. Under (16)–(18), $w - b = \phi(c-s)$ and $E\max(V,b-l) - b = \phi[E\max(V,s)-s]$ ((32)–(33)).
4. At $(E\max(V,s), q, s)$ the retailer earns $\phi\,\Pi_T$ ((34)–(39)).
5. Retailer plus manufacturer profit under direct returns is $\Pi_T$ (Sec. 5.3, p. 17).
6. Proposition 4: with direct-to-manufacturer returns and the buy-back (22)–(23), the chain optimum is a Nash equilibrium between retailer and manufacturer, with retailer share $\phi$.
7. Proposition 5: the sales rebate $u = \frac{E\max(V,s)-s}{c-s}(w-c)$ makes the chain optimum a retailer optimum.
8. With a rebate paid on kept units only, the retailer's optimal refund is $r^* = s - u < s$ (Sec. 5.4, p. 19).

Significance

The results separate what a contract must observe in order to coordinate a chain with consumer returns: either the manufacturer distinguishes returned from unsold units (Propositions 3 and 4), or it observes sales (Proposition 5). The negative results (milestones 1 and 8) show why the standard buy-back and a kept-only rebate fail: each distorts the retailer's refund away from the salvage value. These statements are proved in the paper by short arguments; none of them has, to the knowledge of this mission, a machine-checked proof. Formalizing them yields a reusable model of a newsvendor with an endogenous price and refund under valuation uncertainty, and a checked account of the coordination conditions, including the boundary cases ($\phi = 0$, atoms in the valuation law) that the paper does not discuss.

Difficulty

Each result combines two optimizations, and neither is routine at the generality of the formal statements. The first is over price and refund jointly: the demand rule makes every profit discontinuous in $p$ and $r$, and the refund problem must be solved for an arbitrary valuation law, where atoms make the tie rule at $V = r$ matter. The second is a newsvendor problem in $q$ for an arbitrary demand law: the paper writes the optimal stock as $\bar F^{-1}$ of a fractile, which presumes a continuous, strictly increasing $F$, whereas here $F$ may jump or be flat and the optimal stock is any solution of the fractile equation. The obvious reduction, "the retailer's profit is $\phi\,\Pi_T$, so its maximizer is the chain's", is not available: that identity holds only at the chain's price and refund, and away from them the retailer's profit is not proportional to $\Pi_T$. In Proposition 4 the manufacturer's deviation to a refund below $s$ acts on the consumers' purchase decision, and the paper's remark that no one then buys is false when $V \ge s$ almost surely, so that case needs its own argument.

Formalization scope

Prices, refunds, costs, quantities and profits are real numbers. The valuation law $\nu$ is a probability measure on $\mathbb R$ with integrable identity (a strict generalization of the paper's density $g$); $\bar G(r) = \nu([r,\infty))$ and $G(r) = \nu((-\infty,r))$, matching the rule "keep iff $V \ge r$". The demand law $D$ is a probability measure on $\mathbb R$ with $D((-\infty,0)) = 0$, and $E\min(X,q)$ is SupplyChainTheory.expSales from the published module SupplyChainTheory_contracts. Every profit includes the demand rule (6): without it, (15) and (31) are unbounded in $p$. Optimization is over all real $p$ and $r$ and all $q \ge 0$, nonnegative stocks and demand being the paper's setting; with negative stocks the profits are unbounded. Optimality of the paper's closed-form triple is claimed, never uniqueness, and "induces the retailer to maximize supply chain profit" is stated as "the chain-optimal triple is a retailer optimum"; that the triple maximizes $\Pi_T$ is Proposition 2, formalized in mission 1, and not restated. The optimal stock is any solution of the fractile equation, and no continuity of $D$ is assumed. The Nash equilibrium of Proposition 4 is written as the two best-response inequalities. Proposition 5 adds the hypothesis $w \ge s$, implied by the paper's range $w \ge c$ (p. 19) and necessary: for $w < s$ the retailer's profit is unbounded. The kept-only rebate of Sec. 5.4 has no printed formula; its profit is (24) with the rebate removed from the returned-units term. Printed page numbers equal PDF page numbers throughout the source. A formalization in which the retailer's profit is defined as $\phi\,\Pi_T$, or in which the optimization is restricted to $r = s$, would make the goal trivial and is excluded: (31) is stated with free $w$, $b$, $l$, and the contract enters only through hypotheses.

The model module (SuReturns.Coordination.Model) restates the single-seller objects of mission 1 in this sub-namespace. Contributions welcome: proofs of the two optimization steps as reusable lemmas (the refund step for a general valuation law and the newsvendor step for an arbitrary demand law), which serve every milestone here.

Selected references

• X. Su, Consumer Returns Policies and Supply Chain Performance, SSRN working paper 1020451, version of August 2008. https://ssrn.com/abstract=1020451 ; published in Manufacturing & Service Operations Management 11(4), 2009. https://doi.org/10.1287/msom.1080.0240
• G. P. Cachon, Supply Chain Coordination with Contracts, in Handbooks in Operations Research and Management Science, vol. 11, 2003. https://doi.org/10.1016/S0927-0507(03)11006-7
• B. A. Pasternack, Optimal Pricing and Return Policies for Perishable Commodities (the buy-back contract), Marketing Science 4(2), 1985. https://doi.org/10.1287/mksc.4.2.166