Convex Optimization

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

Scheduling jobs on unrelated parallel machines to minimize the total weighted completion time, the problem written $R\,|\,|\sum w_jC_j$ in the three-field notation, is one of the basic NP-hard models of machine scheduling. Each job may take a different time on each machine, as when heterogeneous processors, plants or crews serve the same pool of tasks, and the objective rewards finishing important jobs early. For a single machine the problem is solved exactly by Smith's ratio rule (Smith, 1956). With several unrelated machines the problem is strongly NP-hard and the question is how close to the optimum a polynomial-time algorithm can come.

Timeline of the guarantees for $R\,|\,|\sum w_jC_j$:

• Lenstra, Shmoys and Tardos (1990) gave an LP-based 2-approximation for the makespan on unrelated machines; their assignment variables $a_{ij}$ are the ones used here.
• Hall, Schulz, Shmoys and Wein (1997) gave constant-factor approximations for $\sum w_jC_j$ on unrelated machines via time-indexed and interval-indexed LP relaxations.
• Schulz and Skutella (conference version 1999, journal 2002) obtained $3/2+\varepsilon$ by randomized rounding of a time-indexed LP.
• Skutella (J. ACM 2001), the paper of this mission, gave a convex quadratic relaxation in assignment variables alone and a $3/2$-approximation by randomized rounding, with a short analysis.
• Bansal, Srinivasan and Svensson (2016) improved $3/2$ to $3/2-\varepsilon$ for a small constant $\varepsilon>0$; later work lowered the constant further.

Setting

There are $n$ jobs $j\in J$ and $m$ machines $i$. Job $j$ has a weight $w_j\ge 0$ and a processing time $p_{ij}>0$ on machine $i$. A schedule assigns each job to one machine and orders the jobs on every machine; the completion time $C_j$ of a job is the time at which it finishes when each machine works without idle time.

For a fixed assignment, Smith's ratio rule orders each machine optimally. Fix for each machine $i$ the total order $j\prec_i k$ iff $w_j/p_{ij}>w_k/p_{ik}$, ties broken by index. Under an assignment $\sigma$ the completion time of $j$ is

$$C_j(\sigma)=p_{\sigma(j)j}+\sum_{k\prec_{\sigma(j)}j,\ \sigma(k)=\sigma(j)}p_{\sigma(j)k},$$

and the problem is to minimize $\mathrm{val}(\sigma)=\sum_jw_jC_j(\sigma)$ over all assignments.

With $a_{ij}\in\{0,1\}$ indicating that $j$ runs on $i$, the problem is the integer quadratic program (IQP) with objective

$$Z_{QP}(a)=c^Ta+\tfrac12a^TDa,\qquad c_{ij}=w_jp_{ij},$$

where $D$ is symmetric with entry $w_jp_{ik}$ at $((i,j),(i,k))$ for $k\prec_ij$ and zero across machines and on the diagonal. Relaxing $a_{ij}\in\{0,1\}$ to $a\ge 0$ with $\sum_ia_{ij}=1$ gives (QP). Raising the diagonal gives the convex program (CQP), with objective $Z_{CQP}(a)=\tfrac12c^Ta+\tfrac12a^T(D+\operatorname{diag}(c))a$. Adding the lower bound $c^Ta$ gives (CQP′):

$$\min Z\quad\text{s.t.}\quad \textstyle\sum_ia_{ij}=1,\ \ a\ge 0,\ \ Z\ge Z_{CQP}(a),\ \ Z\ge c^Ta .$$

Randomized rounding of a fractional $\bar a$ sends job $j$ to machine $i$ with probability $\bar a_{ij}$, the choices being pairwise independent across jobs, and then orders every machine by $\prec_i$.

Formalization targets

Goal: (CQP′) is a relaxation, and rounding loses at most 3/2

For every instance with $p>0$, $w\ge 0$:

$$\forall\sigma:\ (a^\sigma,\ \mathrm{val}(\sigma))\ \text{is feasible for (CQP′)},$$ $$\forall(\bar a,Z)\ \text{feasible for (CQP′)}:\quad \mathbb E\Bigl[\sum_jw_jC_j\Bigr]\le\tfrac32 Z .$$

The first part makes $Z^*_{CQP'}$ a lower bound on the optimum. The second is Lemma 2.8. Together they are Corollary 2.9 and the value guarantee of the $3/2$-approximation.

Milestones

In attack order:

• Lemma 2.2: $\mathbb E[C_j]=\sum_i(\Pr[j\mapsto i]p_{ij}+\sum_{k\prec_ij}\Pr[j,k\mapsto i]p_{ik})$ for any random assignment.
• Theorem 2.1: rounding a feasible $\bar a$ has expected value exactly $Z_{QP}(\bar a)$.
• Corollary 2.3: (IQP) and (QP) have the same optimum.
• The positive semidefiniteness of $D+\operatorname{diag}(c)$ and Lemma 2.4: $a\mapsto(1-\gamma)c^Ta+\tfrac12a^T(D+2\gamma\operatorname{diag}(c))a$ is convex for all instances iff $\gamma\ge\tfrac12$.
• The identity $Z_{QP}=Z_{CQP}+\tfrac12(c^Ta-a^T\operatorname{diag}(c)a)$ and Theorem 2.6 a), the factor $2$ for (CQP).
• Lemma 2.8, the integrality step of Theorem 2.10, and Corollary 2.11, the bound $(1+c^T\bar a/(2Z))Z$.

Significance

The result gives a $3/2$-approximation for $R\,|\,|\sum w_jC_j$ from a relaxation with only $mn$ variables, without time indexing, so its size does not depend on the processing times. The same convexification, adapted to time slots, yields the factor 2 with release dates (§3 of the paper). The equality of Theorem 2.1 makes the analysis exact: the loss of rounding is exactly the gap between $Z_{QP}$ and the convex objective. The relaxation also bounds the power of preemption (§4), and for identical machines it connects scheduling to Max-$k$-Cut (§6).

All these results are proved in the paper; none is known to be formalized. A formal development adds:

• a checked model of Smith-sequenced assignment schedules;
• the expectation calculus for pairwise independent rounding;
• the positive-semidefiniteness argument of Lemma 2.4;
• a precise statement of what the $3/2$ guarantee says when complexity is set aside.

Difficulty

Two steps resist the obvious approach.

Positive semidefiniteness. $D$ alone is indefinite: two jobs with unit data give the block $\left(\begin{smallmatrix}0&1\\1&0\end{smallmatrix}\right)$. Positive semidefiniteness of $D+\operatorname{diag}(c)$ holds only because the jobs on each machine are ordered by Smith's ratio. A generic matrix argument that ignores this ordering fails, and the "only if" half of Lemma 2.4 needs a specific family of instances.

Exact expectations under pairwise independence. Theorem 2.1 is an equality that uses only the one- and two-job marginals. A proof that silently assumes full independence of the choices proves a different statement. A proof that drops the product condition on pairs is false: with correlated choices the expected value differs from $Z_{QP}$.

Formalization scope

Jobs and machines are Fin n and Fin m; vectors in $\mathbb R^{mn}$ are functions on Fin m × Fin n and $D$ is a Matrix over that type. The order $\prec_i$ is cross-multiplied ($w_jp_{ik}>w_kp_{ij}$, or equality and $j<k$), which equals the page's ratio definition because $p>0$.

Standing assumptions of p. 2 are hypotheses of every theorem: $p_{ij}>0$ and $w_j\ge0$. Hypotheses added relative to the page:

• Corollary 2.11 assumes $Z>0$, which its fraction presupposes;
• the integrality step of Theorem 2.10 assumes integral $p$ and $w$, as the page's proof does.

Optimum. The scheduling optimum $Z^*$ is the minimum of $\mathrm{val}$ over assignments, by Smith's rule (p. 7, cited by the paper, not reproved). "Within a factor $\alpha$ of the optimum" is stated as a bound against the value of every assignment, so no optimum is presupposed.

Rounding. Randomized rounding is any nonnegative weight $\mu$ of total mass 1 on assignments, with $\Pr_\mu[j\mapsto i]=\bar a_{ij}$ and $\Pr_\mu[j\mapsto i,\,k\mapsto h]=\bar a_{ij}\bar a_{hk}$ for $j\ne k$. The product weight satisfies this.

Not formalized. Polynomial running time, solvability of (CQP′) within additive error $\varepsilon$ (ellipsoid method), and derandomization by conditional probabilities. Theorem 2.10 is formalized as the existence of an outcome in the support of the rounding with the $3/2$ guarantee.

Trivializing formalization ruled out. A bound $\mathbb E\le\tfrac32Z$ for an arbitrary number $Z$ says nothing about schedules. The goal therefore also states that every schedule is feasible for (CQP′) at its own value, so $Z$ is a genuine lower bound on the optimum.

Contributions welcome. A complete development needs:

• linearity of expectation over a finite weight on assignments;
• the computation of Lemma 2.2;
• a positive-semidefiniteness criterion via principal minors or a direct sum-of-squares decomposition of $a^T(D+\operatorname{diag}(c))a$;
• convexity of quadratic forms with PSD matrices.

The rounding calculus and the PSD lemma are reusable for §§3–4 of the same paper. Alternative proofs of Lemma 2.4 are 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
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46, 1990. https://doi.org/10.1007/BF01585745
• L. A. Hall, A. S. Schulz, D. B. Shmoys, J. Wein, Scheduling to minimize average completion time: off-line and on-line approximation algorithms, Mathematics of Operations Research 22(3), 1997. https://doi.org/10.1287/moor.22.3.513
• A. S. Schulz, M. Skutella, Scheduling unrelated machines by randomized rounding, SIAM Journal on Discrete Mathematics 15(4), 2002. https://doi.org/10.1137/S0895480199357078
• N. Bansal, A. Srinivasan, O. Svensson, Lift-and-round to improve weighted completion time on unrelated machines, STOC 2016. https://doi.org/10.1145/2897518.2897572

Motivation

Semidefinite programs optimize a linear objective while requiring an affine matrix to be positive semidefinite. They include familiar linear and quadratic optimization models and arise in engineering and combinatorial optimization. Vandenberghe and Boyd's survey develops their duality theory and describes interior point methods that work with primal and dual matrices simultaneously. The question in this mission is quantitative: if a method lowers a particular potential by a fixed amount at each step, how quickly does its primal-dual objective gap shrink? Vandenberghe and Boyd, pp. 49, 76–77.

The paper uses the potential to combine two kinds of progress. One term records the size of the duality gap; another records how far the current matrices are from a central pair. Decreasing the gap alone does not ensure the matrices remain well positioned for the next step, so the potential accounts for both quantities. Theorem 5.1 turns a per-step decrease in this scalar into an explicit bound on the gap after $k$ steps. The theorem concerns any sequence meeting that decrease condition; it does not prescribe a particular search direction or step-selection algorithm. Vandenberghe and Boyd, pp. 76–77.

Setting

Fix a vector $c\in\mathbb R^m$ and symmetric real $n\times n$ matrices $F_0,F_1,\ldots,F_m$. For $x\in\mathbb R^m$, define the affine matrix

$$F(x)=F_0+\sum_{i=1}^{m}x_iF_i.$$

The primal problem minimizes $c^Tx$ subject to $F(x)\succeq0$. A dual-feasible matrix $Z$ satisfies $Z\succeq0$ and $\operatorname{Tr}(F_iZ)=c_i$ for every $i=1,\ldots,m$. Here $\succeq0$ means positive semidefinite; $\succ0$ means positive definite. The pair $(x,Z)$ is strictly feasible if both $F(x)\succ0$ and $Z\succ0$, with the dual equations still satisfied. Section 4 also assumes that $F_1,\ldots,F_m$ are linearly independent. Vandenberghe and Boyd, pp. 49, 63, 70.

For a feasible pair, the duality gap is the difference between the primal objective $c^Tx$ and the dual objective $-\operatorname{Tr}(F_0Z)$. Equation (32) identifies it as

$$\eta=c^Tx+\operatorname{Tr}(F_0Z)=\operatorname{Tr}(F(x)Z).$$

For a strictly feasible pair, define the deviation from centrality and the potential by

$$\psi(x,Z)=-\log\det(F(x)Z)+n\log\eta-n\log n,$$ $$\varphi(x,Z)=\nu\sqrt n\,\log\eta+\psi(x,Z),\qquad \nu\ge1.$$

The logarithm is natural. The matrix size $n$ determines the $\sqrt n$ factor; it is distinct from the number $m$ of decision variables. These are the explicit formulas on p. 76, where the paper also expresses $\psi$ through a central pair. Vandenberghe and Boyd, pp. 64, 75–76.

Formalization targets

The first milestones establish the gap identity, the expanded determinant formula for $\varphi$, and nonnegativity of $\psi$ with its stated equality condition. The final milestone bounds the gap by the potential:

$$\eta\le\exp\!\left(\frac{\varphi(x,Z)}{\nu\sqrt n}\right).$$

For the goal, let $(x^{(j)},Z^{(j)})$, $j=0,\ldots,k$, be strictly feasible pairs and suppose a fixed $\delta>0$ gives the decrease stated in equation (56) at every step $j<k$:

$$\varphi(x^{(j+1)},Z^{(j+1)})\le\varphi(x^{(j)},Z^{(j)})-\delta.$$

The goal theorem, Theorem 5.1, says that for $0<\varepsilon<1$ and

$$k\ge\frac{\nu\sqrt n\log(1/\varepsilon)+\psi(x^{(0)},Z^{(0)})}{\delta},$$

one has the boundary-correct gap estimate

$$\operatorname{Tr}(F(x^{(k)})Z^{(k)})\le\varepsilon\operatorname{Tr}(F(x^{(0)})Z^{(0)}).$$

The paper prints a strict inequality in the last display. Its stated non-strict threshold permits equality, as explained under Formalization scope. Vandenberghe and Boyd, p. 77, (56) and Theorem 5.1.

Significance

The theorem converts a local numerical guarantee into a global bound on an optimization certificate. Because the gap is the difference between primal and dual objectives, shrinking it gives a quantitative measure of progress toward optimality for every strictly feasible iterate. The expression records the dependence on matrix size, desired relative gap, starting deviation, and guaranteed potential decrease. It leaves the mechanism that achieves the decrease open, so different potential reduction methods can use the same conclusion. Vandenberghe and Boyd, pp. 64, 76–77.

The target here is a machine-checked statement and proof of this known 1996 result, together with its four supporting facts. The draft declarations compile as statements; their proofs remain open. A complete development would make the determinant, trace, positive-definiteness, and sequence reasoning reusable for other matrix optimization arguments. It would also record the boundary correction precisely rather than carrying forward a strict sign that fails at equality.

Difficulty

The substantive matrix claim is $\psi(x,Z)\ge0$. The product $F(x)Z$ need not be symmetric, even though both factors are positive definite, so directly applying a result about symmetric matrix eigenvalues to the product is not automatic. The nonnegativity and its equality case must respect the positivity and determinant conventions used by the explicit formula. The later exponential bound and iteration statement depend on those facts and on keeping each logarithm in its positive domain. Vandenberghe and Boyd, p. 76.

Formalization scope

Lean uses Fin m for the $m$ variable matrices, indexed from zero, with $F_0$ as a separate argument; Fin n indexes matrix rows and columns. Matrix.IsHermitian represents real symmetry. Matrix.PosSemidef and Matrix.PosDef represent the paper's matrix inequalities $\succeq0$ and $\succ0$, including symmetry. The matrix size satisfies $n\ge1$. Traces, determinants, natural logarithms, and $\sqrt n$ are the corresponding Mathlib operations. All statements involving $\psi$ or $\varphi$ require strict feasibility, so the real logarithm's default value on nonpositive inputs cannot decide a theorem. The paper's linearly independent $F_1,\ldots,F_m$ are an explicit hypothesis on the Section 4 and 5 statements. Vandenberghe and Boyd, pp. 49, 70, 76–77.

The definition of $\psi$ uses the explicit second formula on p. 76. The central pair in the preceding formula is not represented; its existence is introduced on p. 75 without a proof there. The p. 76 prose describes $\psi\ge0$ for feasible pairs, but its finite real logarithmic formula and the potential reduction iterates use strictly feasible pairs. The milestone states that domain explicitly. In Theorem 5.1 strict feasibility is assumed for the iterates $j=0,\ldots,k$ and equation (56) for the steps $j<k$ only, so the statement covers a method that stops after $k$ steps. The fixed $\delta$ is positive, and $\nu\ge1$ and $0<\varepsilon<1$ are explicit.

The paper's strict conclusion is false at its own inclusive threshold. Take $m=n=1$, $F_0=0$, $F_1=c=Z^{(j)}=1$, $x^{(j)}=e^{-j}$, $\nu=\delta=1$, and $\varepsilon=e^{-1}$. Then $\psi=0$, each decrease is exactly one, and at $k=1$ the gap equals $\varepsilon$ times its initial value. The goal therefore uses $\le$, the strongest statement valid at the printed threshold. This correction is recorded in the theorem's description and moderation notes. Vandenberghe and Boyd, p. 77, Theorem 5.1.

A complete proof needs Mathlib's matrix order, determinant and trace identities, logarithm and exponential facts, and an arithmetic-geometric mean statement for positive eigenvalues. Matrix lemmas and the deviation inequality are welcome contributions alongside the final sequence bound. The definitions preserve the paper's full potential and feasible domain; replacing $\psi$ by zero or dropping the $\sqrt n$ factor would change the target.

Selected references

• Lieven Vandenberghe and Stephen Boyd, Semidefinite Programming, SIAM Review 38(1), 49–95, 1996. DOI: 10.1137/1038003.