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

Motivation

Robust control repeatedly meets linear matrix inequalities that must hold for every value of an unknown, norm-bounded matrix. A typical instance is

$$C + EFG + G^\top F^\top E^\top < 0 \quad\text{for all } F \text{ with } F^\top F \leqslant \bar F,$$

where $F$ collects model uncertainty or noise. Such a condition quantifies over infinitely many matrices and cannot be checked directly. Petersen's lemma (Petersen and Hollot, Automatica 1986; Petersen, Systems & Control Letters 1987) replaces it by a single inequality in one scalar multiplier $\lambda>0$. The lemma is a standard tool in the design of quadratically stabilizing controllers for uncertain systems, and it was recently used for controller design from noisy data (Bisoffi, De Persis and Tesi, arXiv:2109.12175).

H. J. van Waarde, M. K. Camlibel, J. Eising and H. L. Trentelman (arXiv:2203.12959v3, 2023; SIAM J. Control Optim.) develop a theory of quadratic matrix inequalities (QMIs) and prove matrix versions of the S-lemma. In §4.5.3 they show that both the strict and the non-strict Petersen lemma follow from their matrix S-lemmas (Theorems 4.10 and 4.7) by a suitable choice of the two quadratic forms. This mission formalizes that derivation.

Timeline. Petersen and Hollot (1986) and Petersen (1987) state the lemma for stabilization of uncertain linear systems. Bisoffi, De Persis and Tesi (arXiv 2021) use strict and non-strict versions for data-driven stabilization. van Waarde, Camlibel, Eising and Trentelman (2023, Proposition 4.16) recover both versions from matrix S-lemmas.

Setting

All matrices are real. For a symmetric matrix $A$, $A \geqslant 0$ ($A>0$) means positive semidefinite (definite), and $A \leqslant B$ means $B-A\geqslant0$; the notation includes symmetry. $A^\dagger$ is the Moore–Penrose pseudo-inverse and $\bar F^{1/2}$ the positive semidefinite square root of $\bar F\geqslant0$.

Quadratic matrix inequalities. A symmetric $\Pi \in \mathbb S^{q+r}$ is partitioned into blocks $\Pi_{11}$ ($q\times q$), $\Pi_{12}$, $\Pi_{21}$, $\Pi_{22}$ ($r\times r$). Its solution sets are

$$\mathcal Z_r(\Pi)=\Big\{Z\in\mathbb R^{r\times q}: \begin{bmatrix}I_q\\ Z\end{bmatrix}^\top \Pi \begin{bmatrix}I_q\\ Z\end{bmatrix}\geqslant 0\Big\},$$

and $\mathcal Z_r^+(\Pi)$ is defined in the same way with $>0$. The generalized Schur complement is $\Pi\,|\,\Pi_{22}=\Pi_{11}-\Pi_{12}\Pi_{22}^\dagger\Pi_{21}$, and the class $\boldsymbol\Pi_{q,r}$ consists of the $\Pi$ with $\Pi_{22}\leqslant0$, $\Pi\,|\,\Pi_{22}\geqslant0$ and $\ker\Pi_{22}\subseteq\ker\Pi_{12}$.

Petersen's data. Fix $C\in\mathbb R^{n\times n}$ symmetric, $E\in\mathbb R^{n\times p}$, $\bar F\in\mathbb R^{q\times q}$ with $\bar F\geqslant0$, and $G\in\mathbb R^{q\times n}$. The uncertainty set is $\mathcal F=\{F\in\mathbb R^{p\times q}: F^\top F\leqslant\bar F\}$. Display (4.17) defines

$$M=\begin{bmatrix}-C&-E\\-E^\top&0\end{bmatrix},\qquad N=\begin{bmatrix}G^\top\bar FG&0\\0&-I\end{bmatrix}.$$

In this proposition the letters $q,r$ of the QMI section become $n,p$, so $\mathcal Z_p(N)\subseteq\mathbb R^{p\times n}$.

Formalization targets

Goal: Proposition 4.16 (Petersen's lemma)

(a) The robust strict inequality holds if and only if a single multiplier exists:

$$\big(\forall F\in\mathcal F:\ C+EFG+G^\top F^\top E^\top<0\big)\iff \exists\,\lambda>0:\ C+\lambda EE^\top+\lambda^{-1}G^\top\bar FG<0.$$

(b) If $E\neq0$, $\bar F>0$ and $G\neq0$, the same equivalence holds with $\leqslant 0$ in place of $<0$ on both sides.

Milestones

1. Lemma A.1 (p. 26): $A^\top A\leqslant B^\top B$ if and only if $A=SB$ for some contraction $S$ ($S^\top S\leqslant I$); the strict version under full column rank of $B$; and $S=AB^\dagger$ is such a factor.
2. Set identity (p. 17): $\{FG: F\in\mathcal F\}=\{S\bar F^{1/2}G: S^\top S\leqslant I\}=\{H: H^\top H\leqslant G^\top\bar FG\}$.
3. Reformulation (4.17) (p. 17): the strict robust inequality is $\mathcal Z_p(N)\subseteq\mathcal Z_p^+(M)$, the non-strict one is $\mathcal Z_p(N)\subseteq\mathcal Z_p(M)$, and $N\in\boldsymbol\Pi_{n,p}$ with $N_{22}<0$.
4. Theorem 4.10 (strict matrix S-lemma, p. 13): for $N\in\boldsymbol\Pi_{q,r}$ with $N_{22}<0$, $\mathcal Z_r(N)\subseteq\mathcal Z_r^+(M)$ iff $M-\alpha N>0$ for some $\alpha\geqslant0$.
5. Theorem 4.7 (matrix S-lemma, p. 12): for $N\in\boldsymbol\Pi_{q,r}$ with a positive eigenvalue, $\mathcal Z_r(N)\subseteq\mathcal Z_r(M)$ iff $M-\alpha N\geqslant0$ for some $\alpha\geqslant0$.
6. Schur-complement step (p. 17): for $\alpha>0$, $M-\alpha N>0$ iff $-C-\alpha G^\top\bar FG-\alpha^{-1}EE^\top>0$, together with the non-strict analogue.
7. Slater condition (p. 17): $\bar F>0$ and $G\neq0$ imply that $N$ has a positive eigenvalue.

Significance

The result itself. Petersen's lemma converts a semi-infinite family of matrix inequalities into one inequality that is jointly an LMI after a Schur complement. In controller synthesis this makes robust quadratic stabilization against norm-bounded uncertainty a convex feasibility problem. The derivation in this paper places the lemma inside a general theory: Petersen's lemma becomes the special case of the matrix S-lemmas for the pair $(M,N)$ of (4.17), and the hypotheses $E\neq0$, $\bar F>0$, $G\neq0$ of the non-strict version become exactly the Slater condition of Theorem 4.7.

Formalizing it. All results here are proved in the paper. None of them, and no matrix S-lemma, has a machine-checked proof on this platform. The mission produces formal statements and proofs of Petersen's lemma in both forms, of the contraction factorization Lemma A.1, and of the strict and non-strict matrix S-lemmas, which are reused by the data-driven stabilization results of the same paper (Theorems 5.1 and 5.3).

Difficulty

The "if" directions are routine: a multiplier certificate yields the robust inequality by completing a square. The difficulty is the converse, which needs a lossless S-lemma for matrix-valued quadratic forms. The scalar S-lemma rests on the convexity of the joint range of two quadratic forms (Dines' theorem). It does not apply directly to matrix inequalities, and the reduction of Section 4.2 from the matrix case to the vector case is the main obstacle. A second, smaller obstacle is the non-strict case: an equivalence with $\leqslant 0$ is false without a Slater-type condition, and the formal statement has to carry $E\neq0$, $\bar F>0$ and $G\neq0$ exactly where the paper does. Petersen's lemma does not follow from a pointwise choice of $F$. The quantifier over $\mathcal F$ must first become a QMI in $H=FG$, which is what Lemma A.1 provides.

Formalization scope

Matrices are Mathlib Matrix over ℝ. In the goal the sizes are Fin n, Fin p, Fin q. In the S-lemmas the two block index types are arbitrary finite types, and a partitioned matrix is a matrix over the sum type. $X<0$ is (−X).PosDef and $X\leqslant0$ is (−X).PosSemidef; both include symmetry, as the paper's notation does. $F^\top F\leqslant\bar F$ is (F̄ − FᵀF).PosSemidef. The multiplier $\lambda$ is required positive, so $\lambda^{-1}$ is the true inverse. The pseudo-inverse is the unique matrix satisfying the four Penrose conditions, selected by Hilbert's ε, and the square root is Mathlib's CFC.sqrt under the scoped matrix order. "At least one positive eigenvalue" refers to the eigenvalues of the symmetric matrix $N$. "Full column rank" is B.rank = q.

Two choices differ from a literal transcription, and both are disclosed in the items. The strict "Moreover" of Lemma A.1 carries no rank hypothesis, because $A^\top A<B^\top B$ already forces full column rank. The Schur step includes its non-strict analogue, which the paper uses implicitly ("the proof of statement (b) is analogous").

A trivializing formalization is excluded. The quantifier in the goal ranges over every $F\in\mathbb R^{p\times q}$ with $F^\top F\leqslant\bar F$, not over a fixed $F$ or over $H$. Part (b)'s extra hypotheses are not added to part (a), and the sanity instance $n=p=q=1$, $C=-3$, $E=G=\bar F=1$ satisfies every hypothesis and both multiplier conditions at $\lambda=1$.

A complete development needs: Loewner-order calculus and Schur complements for block matrices; Moore–Penrose pseudo-inverse identities; positive semidefinite square roots; the scalar S-lemma (Dines' theorem); and the reduction from matrix to vector QMIs. The S-lemmas and Lemma A.1 are reusable well beyond this mission. Proofs of any milestone, and of the auxiliary results of §4.1–4.2 (Lemmas 4.1–4.5, Theorem 4.6) as supporting theorems, are welcome.

Selected references

• H. J. van Waarde, M. K. Camlibel, J. Eising and H. L. Trentelman, Quadratic matrix inequalities with applications to data-based control, SIAM J. Control Optim., 2023; preprint arXiv:2203.12959v3. https://arxiv.org/abs/2203.12959v3
• I. R. Petersen, A stabilization algorithm for a class of uncertain linear systems, Systems & Control Letters 8 (1987) 351–357 (reference [35] of the paper).
• I. R. Petersen and C. V. Hollot, A Riccati equation approach to the stabilization of uncertain linear systems, Automatica 22 (1986) 397–411 (reference [36] of the paper).
• A. Bisoffi, C. De Persis and P. Tesi, Data-driven control via Petersen's lemma, preprint, 2021. https://arxiv.org/abs/2109.12175
• H. J. van Waarde, M. K. Camlibel and M. Mesbahi, From noisy data to feedback controllers: nonconservative design via a matrix S-lemma, IEEE Trans. Automat. Control 67 (2022) 162–175 (reference [54] of the paper).

Motivation

Quadratic matrix inequalities (QMIs) describe sets of matrices rather than sets of vectors. They appear whenever an unknown matrix is constrained by a quadratic bound: in robust control, where an uncertain block of a system is only known to lie in a norm ball or a sector, and in data-driven control, where the system matrices $(A, B)$ of a linear system $x(t+1) = Ax(t) + Bu(t) + w(t)$ are unknown and the measured data, corrupted by noise satisfying a quadratic bound, only pin them down to a set defined by a QMI.

H. J. van Waarde, M. K. Camlibel, J. Eising and H. L. Trentelman (arXiv:2203.12959, SIAM J. Control Optim. 2023) develop a systematic theory of such sets, culminating in matrix versions of the S-lemma and of Finsler's lemma and in data-based stabilization tests. Before any of that can be used, one has to know when the set of matrices satisfying a QMI is nonempty, convex, bounded, has interior points, or contains strict and boundary solutions. Section 3.1 of the paper answers these questions in terms of the blocks of the matrix defining the QMI. This mission formalizes that section, Theorem 3.2, together with the Schur complement identities (3.2)–(3.4) on which it rests.

Setting

All matrices are real. Fix integers $q, r \ge 0$. For a matrix $A$, the Moore–Penrose pseudo-inverse $A^\dagger$ is the unique matrix $X$ with

$$AXA = A,\quad XAX = X,\quad (AX)^\top = AX,\quad (XA)^\top = XA.$$

$\mathbb S^n$ is the set of symmetric $n\times n$ matrices; for $A \in \mathbb S^n$, $A \ge 0$ and $A > 0$ mean positive semidefinite and positive definite, $A \le 0$, $A < 0$ the negative versions, and $A \ge B$ means $A - B \ge 0$ (the Loewner order).

A matrix $\Pi \in \mathbb S^{q+r}$ is always partitioned as

$$\Pi = \begin{bmatrix}\Pi_{11} & \Pi_{12}\\ \Pi_{21} & \Pi_{22}\end{bmatrix},\qquad \Pi_{11}\in\mathbb R^{q\times q},\ \Pi_{22}\in\mathbb R^{r\times r},\ \Pi_{21} = \Pi_{12}^\top .$$

For $Z \in \mathbb R^{r\times q}$ the QMI is

$$\begin{bmatrix} I_q\\ Z\end{bmatrix}^\top \Pi \begin{bmatrix} I_q\\ Z\end{bmatrix} \ge 0,$$

with solution set $\mathcal Z_r(\Pi)$. Replacing $\ge 0$ by $> 0$ or $= 0$ gives the sets $\mathcal Z_r^+(\Pi)$ of strict solutions and $\mathcal Z_r^0(\Pi)$ of solutions of the quadratic matrix equation. The generalized Schur complement is

$$\Pi\,|\,\Pi_{22} := \Pi_{11} - \Pi_{12}\Pi_{22}^\dagger\Pi_{21},$$

and the class $\boldsymbol\Pi_{q,r}$ (equation (3.5) of the paper) consists of the $\Pi \in \mathbb S^{q+r}$ with

$$\Pi_{22} \le 0,\qquad \Pi\,|\,\Pi_{22} \ge 0,\qquad \ker\Pi_{22} \subseteq \ker\Pi_{12}.$$

In Lean these are pinv, qmiForm, ZSet, ZPlus, ZZero, schur and InPi in the namespace QuadMatIneq.Basic.

Formalization targets

Goal: Theorem 3.2

For $\Pi \in \boldsymbol\Pi_{q,r}$:

• (a) $\mathcal Z_r(\Pi)$ is nonempty and convex;
• (b) for $q \ge 1$, $\mathcal Z_r(\Pi)$ is bounded if and only if $\Pi_{22} < 0$;
• (c) $\mathcal Z_r(\Pi)$ has nonempty interior if and only if $\Pi_{22} = 0$ or $\Pi\,|\,\Pi_{22} > 0$;
• (d) $\mathcal Z_r^+(\Pi) \ne \varnothing$ if and only if $\Pi\,|\,\Pi_{22} > 0$;
• (e) $\mathcal Z_r^0(\Pi) \ne \varnothing$ if and only if $\operatorname{rank}\Pi_{22} \ge \operatorname{rank}(\Pi\,|\,\Pi_{22})$.

Milestones

For $\Pi \in \mathbb S^{q+r}$ with $\Pi_{22} \le 0$ and $\ker\Pi_{22}\subseteq\ker\Pi_{12}$:

• (3.2): $\ker\Pi_{22}\subseteq\ker\Pi_{12} \iff \Pi_{12}\Pi_{22}\Pi_{22}^\dagger = \Pi_{12}$, and

$$\Pi = \begin{bmatrix} I_q & \Pi_{12}\Pi_{22}^\dagger\\ 0 & I_r\end{bmatrix}\begin{bmatrix}\Pi\,|\,\Pi_{22} & 0\\ 0 & \Pi_{22}\end{bmatrix}\begin{bmatrix} I_q & 0\\ \Pi_{22}^\dagger\Pi_{21} & I_r\end{bmatrix};$$

• (3.3): $\begin{bmatrix} I_q\\ Z\end{bmatrix}^\top \Pi \begin{bmatrix} I_q\\ Z\end{bmatrix} = \Pi\,|\,\Pi_{22} + (Z + \Pi_{22}^\dagger\Pi_{21})^\top\Pi_{22}(Z + \Pi_{22}^\dagger\Pi_{21})$;
• (3.4): $\Pi\,|\,\Pi_{22}$ is the value at $Z = -\Pi_{22}^\dagger\Pi_{21}$ and dominates the value at every $Z$ in the Loewner order;
• the claim after (3.4): $\mathcal Z_r(\Pi) \ne\varnothing$ if and only if $\Pi\,|\,\Pi_{22}\ge 0$;
• Theorem 3.2(b), (c), (e) as separate items.

Significance

Theorem 3.2 turns geometric questions about a set of matrices into finite checks on the blocks of $\Pi$: semidefiniteness, definiteness, vanishing and a rank comparison. In the data-driven setting of the paper, $\mathcal Z_r(\Pi)$ (after transposition) is the set of noise samples, and hence of systems, consistent with the data; part (b) decides when that set is compact, part (c) when it has interior, and (a) guarantees convexity, which is what allows linear matrix inequalities to be used over it. The identities (3.2)–(3.4) are used throughout the rest of the paper, in the matrix S-lemma, the matrix Finsler lemma and the parametrization of solution sets.

The result and its proof appear in the paper; this mission produces machine-checked versions. Mathlib has the Schur complement for invertible blocks and positive semidefiniteness, but no Moore–Penrose pseudo-inverse for matrices and nothing on QMI solution sets. To the knowledge of this mission no formalization of these statements exists.

Difficulty

The obvious argument is the classical Schur complement, which requires $\Pi_{22}$ to be invertible. Here $\Pi_{22}$ is only negative semidefinite, and the singular case is exactly where the interesting behaviour lives: the solution set is unbounded precisely when $\Pi_{22}$ has a kernel, and $\Pi_{22} = 0$ gives the whole space. Working with the pseudo-inverse requires the range and kernel identities of $\Pi_{22}^\dagger$ for a symmetric matrix and the kernel inclusion $\ker\Pi_{22}\subseteq\ker\Pi_{12}$ at every step. Part (c) needs a topological argument about the interior in $\mathbb R^{r\times q}$, and part (e) needs a factorization of one positive semidefinite matrix through another of possibly different size, which is a rank argument rather than an identity.

Formalization scope

• Matrices are indexed by arbitrary finite types: $\iota$ with $|\iota| = q$ and $\kappa$ with $|\kappa| = r$, so $\Pi$ is a matrix over $\iota \oplus \kappa$ and its blocks are Mathlib's toBlocks₁₁, …, toBlocks₂₂. Nothing assumes $q, r \ge 1$ except part (b).
• $A^\dagger$ is defined by Classical.epsilon over the four Penrose conditions. Since a solution exists and is unique, this is the pseudo-inverse and not a default value; the total inverse A⁻¹, which is $0$ on singular matrices, is not used anywhere.
• $\ge 0$ and $> 0$ are Mathlib's PosSemidef and PosDef, which include symmetry, matching the paper's convention that definiteness is only asserted for symmetric matrices. $\Pi\in\mathbb S^{q+r}$ is IsHermitian.
• Kernel inclusions are written $\forall v,\ \Pi_{22}v = 0 \Rightarrow \Pi_{12}v = 0$.
• "Bounded" means entrywise bounded, which is equivalent to boundedness in any norm on $\mathbb R^{r\times q}$. The interior is taken in $\mathbb R^{r\times q}$ with its Euclidean topology, not relative to an affine hull.
• Part (b) carries the hypothesis $q \ge 1$. For $q = 0$ the space $\mathbb R^{r\times 0}$ is a single point, so the solution set is bounded for every $\Pi$, including those with singular $\Pi_{22}$, and (b) as printed fails. The other parts are stated without it and hold for $q = 0$ and for $r = 0$.
• The trivializing formalizations are excluded: the pseudo-inverse is not a junk inverse, the class $\boldsymbol\Pi_{q,r}$ is inhabited (e.g. $\Pi = \operatorname{diag}(1, -1)$ and $\Pi = \operatorname{diag}(1, 0)$ for $q = r = 1$), and the identities (3.2)–(3.4) are stated with the paper's exact block layouts.

Infrastructure needed and reusable beyond this mission: the existence and uniqueness of the matrix pseudo-inverse with its basic identities ($(A^\dagger)^\top = (A^\top)^\dagger$, $AA^\dagger$ is the orthogonal projector onto the range), and the generalized Schur complement identities. Contributions of these as separate lemmas are welcome.

Selected references

• H. J. van Waarde, M. K. Camlibel, J. Eising, H. L. Trentelman, Quadratic matrix inequalities with applications to data-based control, SIAM J. Control Optim., 2023; preprint arXiv:2203.12959v3. https://arxiv.org/abs/2203.12959
• D. S. Bernstein, Matrix Mathematics: Theory, Facts, and Formulas, 2nd ed., Princeton University Press, 2009 (reference [4] of the paper, for eigenvalue and pseudo-inverse facts). https://doi.org/10.1515/9781400833344
• F. Zhang (ed.), The Schur Complement and Its Applications, Springer, 2005. https://doi.org/10.1007/b105056