Linear algebra

Why closed-form ADMM updates matter

The alternating direction method of multipliers (ADMM) solves problems of the form $\min f(x)+g(z)$ subject to $Ax+Bz=c$ by alternating a minimization in $x$, a minimization in $z$ and a dual ascent step. Its practical appeal, as surveyed by Boyd, Parikh, Chu, Peleato and Eckstein in Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers (Foundations and Trends in Machine Learning, 2011, doi:10.1561/2200000016), rests on the fact that each of these minimizations is often trivial to carry out: a projection, a linear solve, or a componentwise formula. Chapter 4 of the book, "General Patterns", catalogues the cases that recur in every later application (lasso, basis pursuit, sparse inverse covariance selection, consensus and sharing problems). This mission formalizes the statements of that chapter, culminating in the identification of the update for an $\ell_1$ penalty with soft thresholding.

Setting

Vectors live in $\mathbb R^n$ with the Euclidean norm $\|\cdot\|_2$. An extended-real-valued function $f:\mathbb R^n\to\mathbb R\cup\{+\infty\}$ is given by its effective domain $\operatorname{dom} f$ and its finite values there. Fix a penalty parameter $\rho>0$, a matrix $A\in\mathbb R^{p\times n}$ and a vector $v\in\mathbb R^p$. The $x$-update of ADMM (p. 25) is

$$x^+=\operatorname*{argmin}_x\Bigl(f(x)+\tfrac{\rho}{2}\|Ax-v\|_2^2\Bigr),$$

where "argmin" denotes a minimizer over $\operatorname{dom} f$. When $A=I$ the right-hand side, as a function of $v$, is the proximity operator $\mathbf{prox}_{f,\rho}(v)$ (§4.1).

The chapter evaluates $x^+$ in four situations:

• $f$ is the indicator function of a closed nonempty convex set $\mathcal C$ ($0$ on $\mathcal C$, $+\infty$ off it); then $x^+$ is the Euclidean projection $\Pi_{\mathcal C}(v)$, the nearest point of $\mathcal C$ to $v$;
• $f(x)=\tfrac12x^TPx+q^Tx+r$ is a convex quadratic, with $P$ symmetric positive semidefinite, possibly restricted to an affine set $\{x\mid Fx=g\}$;
• $f(x)=f_1(x_1)+\cdots+f_n(x_n)$ is componentwise separable and $A^TA$ is diagonal;
• $f(x)=\lambda\|x\|_1=\lambda\sum_i|x_i|$ with $\lambda>0$ and $A=I$.

The soft thresholding operator (§4.4.3, p. 32) is, for $\kappa\ge0$,

$$S_\kappa(a)=\begin{cases}a-\kappa & a>\kappa\\ 0 & |a|\le\kappa\\ a+\kappa & a<-\kappa,\end{cases}$$

applied componentwise to vectors.

Formalization targets

Goal: soft thresholding is the proximity operator of the ℓ1 norm (§4.4.3, p. 32)

For $\lambda>0$, $\rho>0$ and $v\in\mathbb R^n$, a vector $x$ minimizes $\lambda\|x\|_1+\tfrac{\rho}{2}\|x-v\|_2^2$ over $\mathbb R^n$ if and only if

$$x_i=S_{\lambda/\rho}(v_i)\qquad(i=1,\dots,n).$$

The statement gives both that the soft-thresholded vector is a minimizer and that it is the only one.

Milestones

1. Projection (§4.1, p. 26): for $\mathcal C$ closed, nonempty and convex, $\Pi_{\mathcal C}(v)$ exists and is unique, and for every $\rho>0$ the $x$-update of the indicator of $\mathcal C$ is exactly $\Pi_{\mathcal C}(v)$.
2. Nonnegative orthant (§4.1, p. 26): for the indicator of $\mathbf R^n_+$, $x^+=(v)_+$, uniquely.
3. Quadratic update (4.1) (p. 26): if $P+\rho A^TA$ is invertible it is positive definite, and $x^+=(P+\rho A^TA)^{-1}(\rho A^Tv-q)$ is the unique minimizer.
4. Matrix inversion lemma (§4.2.4, p. 28): $(P+\rho A^TA)^{-1}=P^{-1}-\rho P^{-1}A^T(I+\rho AP^{-1}A^T)^{-1}AP^{-1}$ when the inverses exist. This is the Woodbury identity, already proved on the platform, and is referenced rather than re-posed.
5. Equality-constrained quadratic (§4.2.5, p. 29): $x^{k+1}$ minimizes the update over $\{Fx=g\}$ iff some $\nu$ solves the KKT system; when the affine set is nonempty, $x^+$ is an affine function of $v$.
6. Component separability (§4.4.2, p. 31): with $A^TA$ diagonal, the $x$-update splits into $n$ independent scalar minimizations.
7. Positive-part form (p. 32): $S_\kappa(a)=(a-\kappa)_+-(-a-\kappa)_+$.
8. Shrinkage form (4.2) (p. 32): $S_\kappa(a)=(1-\kappa/|a|)_+a$ for $a\ne0$.
9. Scalar update (p. 32): $S_{\lambda/\rho}(v_i)$ is the unique minimizer of $\lambda|t|+\tfrac{\rho}{2}(t-v_i)^2$.

Significance

The results of this chapter are what make ADMM an implementable algorithm rather than a conceptual one. Soft thresholding is the $z$-update of the lasso (§6.4), of distributed $\ell_1$-regularized regression (§8.2) and of sparse inverse covariance selection (§6.5); projections are the updates of every constrained problem in Chapter 5; the linear-system form (4.1) and the KKT system are the updates of least squares and quadratic programming. Every later chapter of the book cites these identities without proof, so a formal library of them is the substrate on which formal statements about specific ADMM instances can be built.

None of these statements is open as a mathematical question: all are classical facts of convex analysis. The book states them without proof (the goal is justified by a reference to subdifferential calculus in Rockafellar's Convex Analysis). This mission poses their formal statements as Lean proof goals. The matrix inversion lemma already has a machine-checked proof on the platform (the Woodbury identity) and is reused. A related but distinct statement, that singular value shrinkage is the proximity operator of the nuclear norm (Cai, Candès and Shen, 2010), is posed separately on the platform and is not this mission's target.

Difficulty

The goal objective $\lambda\|x\|_1+\tfrac{\rho}{2}\|x-v\|_2^2$ is not differentiable, so setting a gradient to zero does not apply; the minimizer sits exactly on the kink of $|\cdot|$ whenever $|v_i|\le\lambda/\rho$. A proof has to handle the three regimes of $S_\kappa$ and must establish global optimality, not only stationarity, together with uniqueness. Passing from the vector problem to the scalar ones requires the separability statement, which is a statement about minimizers of sums over a product domain, not about any particular function. For the quadratic milestones, the difficulty is linear-algebraic: showing that invertibility of $P+\rho A^TA$ forces positive definiteness, and, for the equality-constrained case, that a minimizer exists and depends affinely on $v$ even when $F$ is rank deficient and the KKT matrix is singular.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin n), so ‖·‖ is $\|\cdot\|_2$; matrices are Matrix (Fin p) (Fin n) ℝ acting through Matrix.toEuclideanLin. The conventions committed to are:

• Functions as (domain, values). An extended-real-valued $f$ is a pair: a domain set and a real function on it. An indicator function is (the set, $0$).
• Argmin as a predicate. IsXUpdate, IsProx and IsProjection say "$x$ is a minimizer"; no choice function is used. Where the book says "the solution", the theorems state an equivalence "$x$ is a minimizer $\iff$ $x$ equals the formula", which gives existence and uniqueness at once.
• Explicit hypotheses. $\rho>0$ and $\lambda>0$ (written lam, since λ is a Lean keyword); $\kappa\ge0$ for the soft thresholding identities (implicit in the book, where $\kappa=\lambda/\rho$, and false for $\kappa<0$); $a\ne0$ in (4.2), as on the page; $P$ symmetric positive semidefinite (Matrix.PosSemidef); invertibility of $P+\rho A^TA$ in (4.1); $\mathcal C$ closed, convex and nonempty for the projection; nonemptiness of $\{Fx=g\}$ for the existence part of §4.2.5; $F$ of arbitrary rank.
• ℓ1 norm. $\|x\|_1$ is defined as $\sum_i|x_i|$, separately from the Euclidean norm.
• Separability is stated for a general $A$ with $A^TA$ diagonal, with the scalar problems written out explicitly (the book does not write them).

The trivializing formalization to avoid is stating the goal as the subgradient condition $0\in\lambda\,\partial|\cdot|(x_i)+\rho(x_i-v_i)$, or as agreement of the three formulas for $S_\kappa$: the goal is global minimality and uniqueness of the soft-thresholded vector for the $\ell_1$ objective. Not formalized: the flop counts and caching remarks of §§4.2.1–4.2.4 and the iterative-solver discussion of §4.3, which make no mathematical claim.

Contributions welcome: proofs of any milestone; the general block-separability statement of §4.4.1; a lemma connecting IsProx with Mathlib's orthogonal projection onto complete convex sets.

Selected references

• S. Boyd, N. Parikh, E. Chu, B. Peleato, J. Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers, Foundations and Trends in Machine Learning 3(1), 2011, pp. 1–122. https://doi.org/10.1561/2200000016
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (§23, subdifferentials). https://doi.org/10.1515/9781400873173
• J.-J. Moreau, Proximité et dualité dans un espace hilbertien, Bulletin de la Société Mathématique de France 93, 1965, pp. 273–299. https://doi.org/10.24033/bsmf.1625
• J.-F. Cai, E. J. Candès, Z. Shen, A Singular Value Thresholding Algorithm for Matrix Completion, SIAM Journal on Optimization 20(4), 2010, pp. 1956–1982. https://doi.org/10.1137/080738970

Motivation

Quantum communication and computation often require a receiver to infer which preparation was sent after it has passed through a noisy quantum process. When possible preparations are mixed states, their overlap makes exact identification impossible. A measurement is then judged by its average probability of a correct label. The pretty good measurement gives a concrete measurement from the ensemble itself, without first solving the optimization over all measurements. Barnum and Knill related it to a general reversal operation for noisy dynamics and bounded its error through pairwise state fidelities in their preprint, §V–VI. The bound is useful when the overlaps are easier to estimate than the measurement's success probability.

The present mission addresses the preprint's second main result. The source is arXiv:quant-ph/0004088v2, not the later journal pagination. The preprint also strengthens its Theorem 3 relative to the published text, as its acknowledgment explains; this mission concerns Theorem 5 and the calculation around it.

Setting

An ensemble is a finite family of output density matrices $\hat\rho_j$ with probabilities $p_j\geq0$ satisfying $\sum_jp_j=1$. A density matrix is a positive semidefinite complex matrix with trace one. For each label $j$, fix an orthonormal eigenbasis $v_{ij}$ and nonnegative eigenvalues $\lambda_{ij}$ such that

$$\hat\rho_j=\sum_i\lambda_{ij}|v_{ij}\rangle\langle v_{ij}|, \qquad \sum_i\lambda_{ij}=1.$$

The eigenpair index $i$ runs over a finite output basis $O$; zero eigenvalues are allowed. The input labels form a finite basis $J$. A label distribution is represented by $\rho=\sum_jp_j|j\rangle\langle j|$.

The paper's classicizing channel $A$ has Kraus operators $A_{ij}=\sqrt{\lambda_{ij}}|v_{ij}\rangle\langle j|$. Acting on an input matrix $X$, its value is $A(X)=\sum_{i,j}A_{ij}X A_{ij}^{\dagger}$. In particular, its output on $\rho$ is $\rho_{\mathrm{out}}=\sum_jp_j\hat\rho_j$. The paper assumes $\rho_{\mathrm{out}}$ has full support when it writes its reversal operation. For a general Kraus family $A_a$, that operation has operators

$$(R_{A,\rho})_a=\rho^{1/2}A_a^\dagger A(\rho)^{-1/2}.$$

The inverse square root is spectral: invert nonzero eigenvalues and leave zero eigenvalues at zero. With full support, it is the usual inverse square root.

For an input label $j$, classical fidelity is the chance that the composite operation returns the same label. Averaging gives

$$F_{\mathrm{cl}}(\rho,K)= \sum_jp_j\langle j|K(|j\rangle\langle j|)|j\rangle.$$

The Bures–Uhlmann fidelity used here is the unsquared quantity $F_{\mathrm{BU}}(\sigma,\tau)=\operatorname{tr}\sqrt{\sqrt\sigma\,\tau\,\sqrt\sigma}$. For the classicizing channel, the reversal operation realizes the pretty good measurement, as shown by equation (36) and the discussion after equation (37) in the preprint, p. 10.

Formalization targets

Recovery error

The goal, in the reading established by the paper's proof, is

$$F_{\mathrm{cl}}(\rho,R_{A,\rho}A) \geq 1-\sum_{\substack{i,j\in J\\i\ne j}} \sqrt{p_ip_j}\,F_{\mathrm{BU}}(\hat\rho_i,\hat\rho_j).$$

The sum is over ordered pairs; each unordered pair of distinct labels is counted twice. The coefficient is exactly one. The goal applies to every finite ensemble with the spectral data above and a full-support output. It does not fix the number of labels or the dimension of the output.

The milestones are the reversal formula (36), the classical-fidelity identities in (38), the unit squared Frobenius norm (40), the diagonal-block expression (41), the off-diagonal trace-norm identity following (42), and the two-block estimate of Lemma 6. They record the paper's mathematical statements and keep the attack path tied to the authors' displayed results.

Significance

The result bounds a measurement's probability of error using only pairwise similarities of the possible output states and their prior probabilities. For nearly distinguishable states, the weighted fidelity sum is small, so this particular measurement succeeds with high probability. The theorem therefore gives a usable guarantee for a specified recovery procedure, rather than only asserting that some procedure exists. In the preprint, §VII, Barnum and Knill describe quantum-information applications of such recovery bounds.

The mathematical result is already proved in the paper, subject to the correction explained below. The formalization work is to make the mixed-state channel, its recovery, the finite-dimensional spectral conventions, and the block-matrix norm estimate precise in Lean. The published Prove2Me definitions for Kraus updates and trace norm supply reusable starting points. A complete proof of this mission would add a checked mixed-state pretty-good-measurement bound; the local statements here compile as open theorems, and no proof is claimed.

Difficulty

The obvious pairwise-overlap estimate does not by itself express the error of the recovery channel. The recovery's classical fidelity is initially a channel evaluation on basis states, while the bound uses trace norms of blocks of a Gram matrix. The key obstacle is controlling the off-diagonal Frobenius mass of the positive square root of that Gram matrix by the trace norms of the corresponding blocks of the Gram matrix itself. Lemma 6 states the needed two-block comparison, including rectangular blocks. The matrix dimension and block labels must remain consistent when it is applied across a larger array.

Formalization scope

All systems and index sets are finite, with matrices over $\mathbb C$ and real probabilities. A general completely positive map is represented by an unbundled finite family of Kraus matrices. The classicizing family has rectangular matrices from the input-label space to the output space; the reversal has matrices in the opposite direction. Composite Kraus families are indexed by pairs. The classical fidelity is defined from the channel action in equation (10); the goal does not define it using the desired overlap bound. The reversal is defined by equation (12) for a general family, so its specialized formula remains a theorem.

The spectral hypotheses include nonnegative probabilities and eigenvalues, unit sums, and orthonormal eigenvectors. Full support of $\rho_{\mathrm{out}}$ is an explicit hypothesis wherever the reversal appears, following page 7. Empty input or output types cannot satisfy the normalized data together with these hypotheses. The Bures–Uhlmann expression is the unsquared trace of a positive square root; using the squared fidelity would change the constant and is outside this mission. Lemma 6 is independent of the ensemble and can be reused for finite block-matrix estimates. Contributions to the spectral identities, the array equalities, and the block-norm argument are welcome.

Equation (39) prints the square of the optimal success probability on its left. The first line of (38) compares that quantity with the recovery fidelity in the opposite direction to Corollary 4. The proof on pages 12–13 concludes the displayed bound for $F_{\mathrm{cl}}(\rho,R_{A,\rho}A)$. This mission states that proved conclusion and records the printed discrepancy in its item and audit notes.

Selected references

• Howard Barnum and Emanuel Knill, Reversing quantum dynamics with near-optimal quantum and classical fidelity, arXiv:quant-ph/0004088v2, 2000/2026 version. arXiv
• Howard Barnum and Emanuel Knill, Reversing quantum dynamics with near-optimal quantum and classical fidelity, Journal of Mathematical Physics 43 (2002), 2097–2106. DOI

Motivation

Link-based ranking of web pages rests on a small number of linear-algebraic facts. Kleinberg's HITS algorithm (Hyperlink-Induced Topic Search), introduced in Kleinberg 1999, assigns each page of a hyperlinked collection two scores: an authority score, high for pages that many good hubs point to, and a hub score, high for pages that point to many good authorities. The scores are computed by a simple alternating iteration, and the paper's justification for using them is a convergence theorem: the iteration settles, and its limits are the principal eigenvectors of two symmetric matrices built from the link structure. HITS, together with PageRank (Brin–Page 1998), founded the study of link analysis, and the eigenvector characterization is what later work on the stability and uniqueness of such rankings starts from (for example Ng–Zheng–Jordan 2001 and Farahat et al. 2006).

This mission formalizes that convergence theorem, §3 of the paper, together with the steps of its proof.

Setting

A collection of $n$ hyperlinked pages is a directed graph $G=(V,E)$ with $V=\{p_1,\dots,p_n\}$; an edge $(p,q)\in E$ means that page $p$ links to page $q$. Its adjacency matrix $A$ is the $n\times n$ matrix with $A_{ij}=1$ if $(p_i,p_j)\in E$ and $A_{ij}=0$ otherwise. Self-links are allowed.

Each page $p$ carries an authority weight $x^{\langle p\rangle}$ and a hub weight $y^{\langle p\rangle}$, collected into vectors $x,y\in\mathbb R^n$. Two operations update them:

$$\mathcal I:\ x^{\langle p\rangle}\leftarrow\sum_{q:(q,p)\in E}y^{\langle q\rangle},\qquad \mathcal O:\ y^{\langle p\rangle}\leftarrow\sum_{q:(p,q)\in E}x^{\langle q\rangle}.$$

Normalizing a vector rescales it so that its squares sum to $1$.

The procedure Iterate$(G,k)$ starts from $x_0=y_0=z=(1,\dots,1)$. In round $i=1,\dots,k$ it applies $\mathcal I$ to $y_{i-1}$, obtaining $x_i'$; applies $\mathcal O$ to $x_i'$, obtaining $y_i'$; and normalizes $x_i'$ and $y_i'$ to get $x_i$ and $y_i$. It returns $(x_k,y_k)$.

For a real symmetric matrix $M$, list its eigenvalues with multiplicity in order of decreasing absolute value, $\lambda_1(M),\lambda_2(M),\dots,\lambda_n(M)$. The paper's standing Assumption (†) is

$$|\lambda_1(M)|>|\lambda_2(M)|,$$

so that the eigenspace of $\lambda_1(M)$ is a line. A principal eigenvector $\omega_1(M)$ is a unit vector spanning that line; it is determined up to sign.

Formalization targets

Goal: Theorem 3.2 with the limits of Theorem 3.1

Assume (†) for $A^{\top}A$ and for $AA^{\top}$. Then there are $x^*,y^*\in\mathbb R^n$ with

$$x_k\to x^*,\qquad y_k\to y^*,$$ $$A^{\top}A\,x^*=\lambda_1(A^{\top}A)\,x^*,\quad AA^{\top}y^*=\lambda_1(AA^{\top})\,y^*,\quad \|x^*\|_2=\|y^*\|_2=1.$$

The authority scores converge to the principal eigenvector of the co-citation matrix $A^{\top}A$, and the hub scores to that of the bibliographic coupling matrix $AA^{\top}$.

Milestones: the proof of Theorem 3.1

1. The operations are linear: $\mathcal I(y)=A^{\top}y$ and $\mathcal O(x)=Ax$.
2. Closed forms: for $k\ge1$, $x_k$ is the unit vector along $(A^{\top}A)^{k-1}A^{\top}z$ and $y_k$ the unit vector along $(AA^{\top})^kz$.
3. Normalized power iteration: for symmetric $M$ with positive dominant simple eigenvalue and $v$ not orthogonal to $\omega_1(M)$, $M^kv/\|M^kv\|$ converges to a principal eigenvector.
4. A symmetric matrix with non-negative entries satisfying (†) has a principal eigenvector with non-negative entries.
5. $z$ is not orthogonal to $\omega_1(AA^{\top})$.
6. If $\lambda_1(A^{\top}A)\ne0$, then $A^{\top}z$ is not orthogonal to $\omega_1(A^{\top}A)$.
7. Theorem 3.1: $(x_k)$ and $(y_k)$ converge.

A companion item states Proposition 6.1 (§6): $AA^{\top}$ and $A^{\top}A$ have the same characteristic polynomial, and $A$ maps each eigenvector of $A^{\top}A$ with nonzero eigenvalue to an eigenvector of $AA^{\top}$ with the same eigenvalue.

Significance

The theorem turns a heuristic, mutually reinforcing update into a well-defined object: the HITS scores of a graph are the principal eigenvectors of $A^{\top}A$ and $AA^{\top}$, independent of the number of rounds run, and computable by any eigenvector algorithm. It also locates where the definition is fragile: when (†) fails, the limit depends on the starting vector, which is the starting point of the later stability analyses cited above.

The result has been proved since 1999; its proof in the paper is a short appeal to the power method and to a Perron-type non-negativity fact. What this mission adds is a machine-checked version of the whole chain, from the combinatorial update rules on a directed graph to the spectral characterization, with the hypotheses made explicit. Two generic power-method theorems are already proved on the platform (Trefethen–Bau, Lecture 27) and are included as references; to our knowledge no formalization of HITS, of Assumption (†), or of the non-negativity of principal eigenvectors of non-negative symmetric matrices exists in Mathlib or on the platform.

Difficulty

The obvious argument — "the power method converges" — is only half of the proof. The power method converges from a start vector that has a nonzero component along the dominant eigenvector, and the start vectors here are fixed: $z$ for the hubs and $A^{\top}z$ for the authorities. Showing that they are not orthogonal to the principal eigenvectors needs a Perron-type fact (the principal eigenvector of a non-negative symmetric matrix can be chosen non-negative), which in turn needs that the dominant eigenvalue is the spectral radius itself and not its negative. For the authorities the start vector is $A^{\top}z$, not $z$, and the argument must also use $\lambda_1(A^{\top}A)\ne0$: when $A^{\top}A$ has a zero dominant eigenvalue the iterates are $0$. A second difficulty is the passage from the rescaled power iterates $\lambda_1^{-k}M^kv$ of the referenced platform theorem to the normalized iterates of the algorithm, and from a statement on an abstract inner product space to one about matrices on $\mathbb R^n$.

Formalization scope

Pages are Fin n; the link relation is a decidable relation E : Fin n → Fin n → Prop; adjMatrix E is the real 0/1 matrix (Mathlib's SimpleGraph.adjMatrix is undirected and loopless and is not used). The operations $\mathcal I$, $\mathcal O$ are defined as neighbour sums, not as matrix products, so that milestone 1 has content. normalize v divides by the Euclidean norm and sends $0$ to $0$; no statement is true only because of that convention. hitsIter E k is $(x_k,y_k)$, with the $\mathcal O$ step applied to the unnormalized $x_k'$ as on the page. Convergence is in the product topology of $\mathbb R^n$.

Assumption (†) is encoded as Dagger M: an eigenvalue $\lambda_1$ with one-dimensional eigenspace, $|\mu|<|\lambda_1|$ for every other eigenvalue $\mu$, and $\lambda_1\ne0$. The last clause is the paper's own reading ("as dictated by Assumption (†)", p. 11); without it, the one-page graph with no link satisfies (†) vacuously and Theorem 3.2 fails. Theorems 3.1 and 3.2 assume (†) for both $A^{\top}A$ and $AA^{\top}$, as the paper does. "The principal eigenvector" is a predicate, IsPrincipalEigenvector, true of both unit vectors in the principal eigenspace. Added hypotheses, each disclosed in its item: $\lambda_1>0$ in the power-iteration milestone (the claim fails for $\lambda_1<0$; it costs nothing for the positive semidefinite $A^{\top}A$, $AA^{\top}$); the closed form is stated for $k\ge1$. The non-negativity of $x^*,y^*$ is true but not part of Theorem 3.2 and is not asserted.

A formalization in which $\mathcal I$ and $\mathcal O$ are matrix products by definition, or in which Theorem 3.1 alone is the goal (a sequence converging to $0$ would satisfy it), is ruled out: the goal pairs convergence with membership of the limit in the principal eigenspace as a unit vector.

Useful infrastructure, reusable beyond this mission: normalized power iteration for real symmetric matrices, and the non-negativity of the principal eigenvector of a non-negative symmetric matrix under a simple dominant eigenvalue. Contributions of either, and of the bridge between Matrix.toLin'-eigenspaces and Matrix.IsHermitian.eigenvalues, are welcome.

Selected references

• J. M. Kleinberg, Authoritative sources in a hyperlinked environment, Journal of the ACM 46(5):604–632, 1999. https://doi.org/10.1145/324133.324140
• S. Brin and L. Page, The anatomy of a large-scale hypertextual Web search engine, Computer Networks and ISDN Systems 30:107–117, 1998. https://doi.org/10.1016/S0169-7552(98)00110-X
• A. Y. Ng, A. X. Zheng and M. I. Jordan, Stable algorithms for link analysis, Proc. SIGIR 2001, 258–266. https://doi.org/10.1145/383952.384003
• A. Farahat, T. LoFaro, J. C. Miller, G. Rae and L. A. Ward, Authority rankings from HITS, PageRank, and SALSA: existence, uniqueness, and effect of initialization, SIAM J. Sci. Comput. 27(4):1181–1201, 2006. https://doi.org/10.1137/S1064827502412875
• L. N. Trefethen and D. Bau III, Numerical Linear Algebra, SIAM, 1997, Lecture 27. https://doi.org/10.1137/1.9780898719574

Motivation

Nonlinear programming algorithms are routinely advertised as finding a local minimum. Most of them only certify first-order conditions (a KKT point), and the natural next question is whether a given feasible point is in fact a local minimum. For smooth problems where the Hessian is nonsingular this is a second-order test, but in the degenerate case the test itself becomes a combinatorial question about a quadratic form restricted to a cone.

K. G. Murty and S. N. Kabadi (Math. Programming 39 (1987) 117–129) showed that this question is intractable already in its simplest instance: deciding whether $x = 0$ is a local minimum of a quadratic form $x^{\mathsf T}Dx$ on the nonnegative orthant is NP-complete, and so is deciding whether a square integer matrix is copositive. The paper is the standard reference for the hardness of copositivity testing, which matters for copositive programming, for second-order optimality checks in constrained optimization, and for the complexity of local search in nonconvex optimization.

Setting

Let $D$ be a real square matrix of order $n$ and $Q(x) = x^{\mathsf T}Dx$. The matrix $D$ is copositive if $Q(x) \ge 0$ for every $x \ge 0$ (coordinatewise). The paper considers the quadratic program

$$\text{(7)}\qquad \text{minimize } Q(x) \quad \text{subject to } x \ge 0,$$

and the following questions, each phrased so that "yes" is the interesting answer:

• Problem 1. Is $x = 0$ not a local minimum of (7)?
• Problem 2. Is $Q$ not bounded below on $\{x \ge 0\}$?
• Problem 3. Is there an $x \ge 0$ with $Q(x) < 0$ (is $D$ not copositive)?
• Problem 4. Given $a_0 > 0$, is there an $x \ge 0$ with $e^{\mathsf T}x = a_0$ and $Q(x) < 0$? Here $e$ is the all-ones vector.
• Problems 11, 12. With $h(u) = (u_1^2, \dots, u_n^2)\,D\,(u_1^2, \dots, u_n^2)^{\mathsf T}$, the objective of the unconstrained problem (15): is $u = 0$ not a local minimum of $h$ on $\mathbb R^n$, and is $h$ not bounded below?

The source problem is subset sum (Problem 5): given positive integers $d_0; d_1, \dots, d_n$, is there $y \in \{0,1\}^n$ with $\sum_j d_j y_j = d_0$? Let $l$ be the total number of digits in the data. The paper fixes an integer $\delta > 4\big(d_0\sum_j d_j\big)^2 n^3$ and a rational $\varepsilon$ with $0 < \varepsilon < 2^{-nl^2}$, and defines functions of $2n$ nonnegative variables $(y, s)$:

$$f_1(y,s) = \Big(\sum_j d_j y_j - d_0\Big)^2 + \delta\sum_j (y_j + s_j - 1)^2 + \sum_j y_j s_j,$$

$f_2 = f_1 + 2d_0\sum_j d_j y_j(1 - y_j)$, a homogeneous quadratic $f_4$ that agrees with $f_2$ on the set

$$P = \Big\{(y,s) : y \ge 0,\ s \ge 0,\ \sum_j (y_j + s_j) = n\Big\},$$

and $f_5 = f_4 - (\varepsilon/n^2)\big(\sum_j (y_j + s_j)\big)^2$. The function $f_5$ is a quadratic form $x^{\mathsf T}Mx$ in $x = (y, s) \in \mathbb R^{2n}$; the symmetric matrix $M$, with entries computed explicitly from $d_0, d, \delta, \varepsilon$, is the output of the reduction.

Formalization targets

Goal: the reduction is correct

For positive integer data $d_0; d_1, \dots, d_n$ and $\delta, \varepsilon$ as above, with $M$ the matrix of $f_5$, the following are equivalent:

$$\text{subset sum is solvable} \iff \text{P1}(M) \iff \text{P2}(M) \iff \text{P3}(M) \iff M \text{ not copositive} \iff \text{P4}(M, n) \iff \text{P11}(M) \iff \text{P12}(M).$$

This is the mathematical content of Theorems 1–3 and §4: a polynomially computable map from subset sum instances to matrices under which every one of these questions has the answer of the subset sum instance.

Milestones along the paper's chain

1. Problems 5 and 6 are equivalent: subset sum is solvable iff some $(y,s) \in P$ has $f_1 \le 0$.
2. Problems 6 and 7 are equivalent ($f_1$ vs. $f_2$ on $P$).
3. Problems 7 and 8 are equivalent ($f_2$ vs. $f_4$ on $P$).
4. Lemma 2: for an integer symmetric $D$ of size $L$, the minimum of $Q$ over $[0,1]^n$ is $0$ or at most $-2^{-L}$.
5. Problems 8 and 9 are equivalent: $\exists\,(y,s)\in P$ with $f_4 \le 0$ iff $\exists\,(y,s)\in P$ with $f_5 < 0$.
6. Problem 9 is a special case of Problem 4: $f_5(y,s) = x^{\mathsf T}Mx$, and Problem 9 is Problem 4 for $(M, a_0 = n)$.
7. Problems 3 and 4 are equivalent, for any $D$ and $a_0 > 0$.
8. Problems 1 and 2 are equivalent to Problem 3, for any $D$.
9. Problems 11 and 12 are equivalent to Problems 1 and 2, for any $D$.

Significance

The result. The equivalence shows that checking local optimality of a feasible point, checking boundedness of a quadratic objective on a cone, and checking copositivity are all at least as hard as subset sum, hence NP-hard. Through (15) the same holds for local minimality and boundedness of a quartic polynomial with no constraints at all. These facts are the standard justification for why nonconvex solvers settle for KKT points, and the copositivity part underlies the hardness of copositive programming.

The formalization. The paper's claims are proved, and have been cited for decades, but the proof as printed is a sketch: several steps are stated as "clearly" or "it can be verified", and one step of the proof of Theorem 1 (p. 125) is false as written. The inequality $(\delta/2)(y_j + s_j - 1)^2 + 2d_0 d_j y_j(1 - y_j) \ge 0$ for $y_j > 1$ fails for $y_j$ slightly above $1$, and the pointwise implication "$f_2 \le 0 \Rightarrow f_1 \le 0$ on $P$" has an explicit counterexample. The equivalence of Problems 6 and 7 itself survives numerical checks. A machine-checked proof of the goal settles the correctness of the reduction with the paper's own constants. No machine-checked proof of these statements exists on the platform.

Difficulty

The combinatorial direction (a subset sum solution gives a point with $f_5 < 0$) is a computation. The converse direction carries the content, in two places.

First, passing from $f_1$ to $f_2$ trades the linear penalty for a quadratic one. This is harmless on the box $0 \le y \le 1$ but not for $y_j > 1$, where $2d_0d_jy_j(1-y_j)$ is negative. The printed argument handles this coordinate by coordinate and is wrong there; a correct argument has to show that no point of $P$ with $f_2 \le 0$ exists unless a point with $f_1 \le 0$ does, which requires a global use of the size of $\delta$.

Second, passing from $f_4 \le 0$ to $f_5 < 0$ requires a quantitative gap: if $f_4 > 0$ on $P$ then $\min_P f_4 \ge \varepsilon$ with $\varepsilon$ of only polynomially many bits. Lemma 2 provides such a gap for the unit box and integer matrices, but $P$ is not the box and $f_4$ has rational coefficients, so the lemma does not apply verbatim.

The remaining equivalences (Problems 1, 2, 3, 4, 11, 12 for a fixed matrix) follow from homogeneity of the quadratic form and the substitution $x_j = u_j^2$, and are routine.

Formalization scope

The data $d_0, d_j, \delta$ are natural numbers and $\varepsilon$ is rational; all are cast to $\mathbb R$ in $f_1, \dots, f_5$ and $M$. The index $j = 1, \dots, n$ is Fin n, and the $2n$ variables of $M$ are indexed by Fin n ⊕ Fin n with $x =$ Sum.elim y s. Standing hypotheses: $d_j > 0$ and $d_0 > 0$ (the paper's "all positive integers"); $\delta > 4(d_0\sum_j d_j)^2n^3$ in $\mathbb N$; $\varepsilon > 0$ and $\varepsilon \cdot 2^{nl^2} < 1$ in $\mathbb Q$. The size $l$ counts decimal digits. Problem 1 is local minimality relative to the orthant, Problem 11 is unconstrained local minimality, both in the Euclidean topology. Lemma 2 is stated for integer symmetric $D$ (as §4 of the paper says, "as before … symmetric"), with $L$ Schrijver's encoding size, since the paper does not define "the size of $D$"; the "optimum is $0$ or $\le -2^{-L}$" is stated as a disjunction without an infimum. The milestones on $f_2, f_4, f_5$ over $P$ assume $n \ge 1$, which the paper assumes tacitly; the goal needs no such hypothesis.

Not formalized: membership in NP (Lemma 1), the polynomial-time computability of $M$ and its encoding size, the NP-completeness of subset sum (cited by the paper from Garey–Johnson), Theorem 4, and any of the words "NP-complete" or "NP-hard". The platform's complexity layer (Turing machines over bitstrings) has no subset sum problem and no encoding of rational matrices. The matrix $M$ has rational entries; a positive integer multiple of it is the integer matrix of Theorem 3, has the same answer to every question, and the rescaling is not formalized. The §3 standing assumption "D is not PSD" is not imposed; the constructed matrix can be PSD and the equivalence holds regardless.

The goal is about the explicit matrix $M$, whose entries are given in the definitions; it is not about "some matrix whose quadratic form is $f_5$", and the constants $\delta$ and $\varepsilon$ are the paper's explicit bounds, not "sufficiently large" or "for some $\varepsilon$". A formalization that quantifies existentially over the matrix or the precision would be trivially true and is ruled out.

Contributions welcome: proofs of the matrix identity and the homogeneity arguments (milestones 6–9), a proof of Lemma 2 (which needs a Cramer/Hadamard bound on basic solutions of the linear complementarity system (9)), and a correct proof of the $f_1 \leftrightarrow f_2$ step. The copositivity definitions and milestones 7–9 are reusable for any later work on copositive programming.

Selected references

• K. G. Murty and S. N. Kabadi, Some NP-complete problems in quadratic and nonlinear programming, Mathematical Programming 39 (1987) 117–129. https://doi.org/10.1007/BF02592948
• M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979 (subset sum, problem [SP13]).
• A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986 (encoding sizes, §2.1).

Motivation

A max-XORSAT instance asks for a binary assignment that satisfies as many parity constraints as possible. A matrix specifies the parity check in each constraint, while a second binary vector specifies the desired parity. The objective can be written as the number of satisfied constraints minus the number violated, so an assignment with a high objective value is also a good approximate solution. Jordan and coauthors study decoded quantum interferometry (DQI), a way to sample candidate assignments by encoding a weighted superposition of error patterns and then decoding their syndromes. Their ideal-state analysis assumes that low-weight errors have distinct syndromes. Real decoders can succeed on many errors even when this uniqueness condition fails, which makes the theorem in this mission relevant to the algorithmic regime beyond the guaranteed decoding radius. Jordan et al., §§8.1 and 10.

The paper's 2024 preprint introduced DQI for linear constraint satisfaction and related optimization problems. Its revised 2025 version studies the effect of decoder failures on the measured objective in Theorem 10.1. This mission uses that revision, arXiv:2408.08292v5, and isolates the first inequality of equation (172). The same section supplies explicit identities for the norm of the postselected state and for its objective matrix, making the theorem a bounded campaign of finite combinatorics and linear algebra. Jordan et al., §10, pp. 35–43.

Setting

Fix integers $m,n\ge0$ and a binary matrix $B\in\mathbb F_2^{m\times n}$. Its $i$th row defines a parity $b_i\cdot x$ of an assignment $x\in\mathbb F_2^n$. For a binary vector $v\in\mathbb F_2^m$, the objective is

$$f_v(x)=\sum_{i=1}^{m}(-1)^{b_i\cdot x+v_i}.$$

An error pattern $y\in\mathbb F_2^m$ has syndrome $B^\top y$ and Hamming weight $|y|$. The weight-$k$ shell $E_k$ contains all errors with $|y|=k$. Choose $0\le\ell\le m$ and real weights $w_0,\ldots,w_\ell$. The ideal syndrome-space state in equation (140) sums $(-1)^{v\cdot y}|B^\top y\rangle$ over each $E_k$, multiplied by $w_k/\sqrt{\binom m k}$. Jordan et al., equations (140) and (171).

A deterministic decoder $\mathrm{dec}:\mathbb F_2^n\to\mathbb F_2^m$ guesses an error from its syndrome. It correctly identifies $y$ when $\mathrm{dec}(B^\top y)=y$. Write $D_k\subseteq E_k$ for the correctly identified errors and $F_k=E_k\setminus D_k$ for the failures. The shell failure rate is $\varepsilon_k=|F_k|/\binom m k$, and $\varepsilon=\max_{0\le k\le\ell}\varepsilon_k$. Postselecting successful decoding leaves the unnormalized state $\widetilde P_D(f)$ formed by replacing each $E_k$ in the ideal state with $D_k$. Apply the binary Hadamard transform, divide by the resulting norm, measure $x$, and evaluate $f_v(x)$. Denote this measured expectation by $\langle f_v\rangle$. Jordan et al., §10.3, pp. 39–40.

Formalization targets

Theorem 10.1: the averaged objective

Let $N=\sum_{k=0}^{\ell}w_k^2(1-\varepsilon_k)$ be the squared norm of the postselected state. The goal, for $N>0$ and uniform $v\in\mathbb F_2^m$, is

$$\mathbb E_v\langle f_v\rangle\ge \frac{w^\top A^{(m,\ell,0)}w-2\varepsilon(m+1)w^\top w}{N}.$$

The matrix $A^{(m,\ell,0)}$ is the symmetric tridiagonal matrix in equation (70): its diagonal is zero and its entries adjacent to the diagonal are $a_k=\sqrt{k(m-k+1)}$. This is the first inequality of (172), with the decoder's actual failure fractions in $N$ and the worst shell failure rate in the correction. It has no minimum-distance hypothesis. Jordan et al., Theorem 10.1, pp. 39–40.

Supporting targets

The milestone list includes the norm identity of Lemma 10.4, the ideal and postselected objective matrices of Lemmas 10.2 and 10.5, the normalized expectation identity in (179), the averaged matrix identities of Lemmas 10.3 and 10.6, and the error-matrix bound of Lemma 10.7. A separate companion item records the second comparison printed in (172) under an explicit sign condition; without that condition, the printed comparison can fail. Jordan et al., §10, pp. 36–43.

Significance

The result assigns a quantitative cost to decoding errors. It says how the measured max-XORSAT objective changes when some error patterns are lost during postselection, while permitting a code whose low-weight errors share syndromes. Consequently the theorem addresses the setting in which practical decoding succeeds often but exact distance-based uniqueness is unavailable. The denominator also records the survival probability of the weighted state, so the bound keeps the actual normalization visible. Jordan et al., §10, pp. 35 and 39–43.

A complete formalization would provide reusable definitions for binary syndrome decoding, shellwise failure rates, real-amplitude states, normalized measurement expectations, and finite objective matrices. The paper proves the result on paper; this mission asks for machine-checked proofs of the stated goal and its milestones. The formal development would also document exactly which part of equation (172) requires an additional sign assumption. No proof is claimed by the draft statements themselves.

Difficulty

When two errors have the same syndrome, the ideal syndrome state can combine their amplitudes, so its norm need not equal $w^\top w$. Postselection changes which errors remain, and the measured objective depends on the normalized state for each $v$. Replacing that normalized expectation with the objective of an average state would change the claim. The proof must keep the decoder fixed while $v$ varies and must control the error matrix uniformly over every real weight vector. The printed second inequality of (172) adds a separate sign issue: a smaller positive denominator reverses the expected comparison when the numerator is negative. Jordan et al., equations (161), (171)–(172), (179)–(182).

Formalization scope

Lean uses ZMod 2 for bits, Fin m and Fin n for zero-based coordinates, functions for binary vectors, and Matrix for $B$. The decoder is one function of the syndrome, independent of $v$. Hamming shells, correct and failed decoding sets, and $\varepsilon_k$ are computed from that function. Weights and amplitudes are real. The postselected state uses the factor $1/\sqrt{\binom m k}$; the Hadamard transform uses $1/\sqrt{2^n}$. The average over $v$ is the sum over all $2^m$ vectors divided by $2^m$. The tridiagonal entries compute $m-k$ in the reals, preserving the square-root formula at the boundary.

Two domain conditions are made explicit. The bound $\ell\le m$ rules out absent weight shells, for which Lean would otherwise assign zero to division by $\binom m k=0$. The condition $N>0$ rules out a zero postselected state, whose normalized expectation would likewise be assigned a meaningless zero by total real division. The goal ranges over every binary matrix, every fixed deterministic decoder, and every real weight vector satisfying those conditions. It states the expectation of the explicit postselected state after a Hadamard transform, rather than an unconstrained expectation variable.

The supporting development needs finite character sums, Hamming-shell cardinalities, matrix quadratic forms, and an operator bound for a symmetric real matrix. These components can serve other finite decoding and quantum-state calculations. Contributions proving the seven cited milestones or the goal are within scope. The circuit's resource accounting, asymptotic equation (173), and numerical decoder studies are outside this mission.

Selected references

• S. P. Jordan, N. Shutty, M. Wootters, A. Zalcman, A. Schmidhuber, R. King, S. V. Isakov, T. Khattar, and R. Babbush, Optimization by Decoded Quantum Interferometry, arXiv:2408.08292v5, 2025 revision of the 2024 preprint. arXiv