Linear algebra

Motivation

Many problems in statistics, control and data science minimize a linear objective over a product of small convex sets subject to a few linear equations: $\ell_p$ regression, entropy-regularized transport, and second-order cone programs with small cones. When the number of variables $n$ is much larger than the number of equations $d$, the running time in terms of $d$ decides what is practical.

For linear programs, the Lee–Sidford line of interior point methods replaced the $\sqrt n$ iterations of the classical path-following method with $\widetilde O(\sqrt d)$ iterations.

• 1988. Renegar: $\widetilde O(\sqrt n)$ iterations of path following.
• 2014, 2019. Lee and Sidford (FOCS 2014, arXiv:1910.08033): $\widetilde O(\sqrt d)$ iterations using Lewis weights, for scalar LPs with the logarithmic barrier.
• 2021. van den Brand, Lee, Liu, Saranurak, Sidford, Song, Wang: scalar LPs in time $\widetilde O(nd+d^{5/2})$.
• 2025. Liu, Peng, Tang, Weng, Yang: products of constant-dimensional convex sets with general barriers in time $\widetilde O(nd+d^6\sqrt n)$, with $\sqrt n$ iterations. They note that extending Lee–Sidford to such barriers is open.
• 2026. Zhang and Wright (this manuscript): that extension, in time $\widetilde O(nd+d^{5/2})$.

Setting

The program is

$$\min_{x}\ c^\top x\quad\text{subject to}\quad A^\top x=b,\quad x\in K=K_1\times\dots\times K_m,$$

with $A\in\mathbb R^{n\times d}$, $b\in\mathbb R^d$, $c\in\mathbb R^n$, compact convex $K_i\subset\mathbb R^{n_i}$ and $\sum_in_i=n$.

Each $K_i$ carries a $1$-self-concordant barrier $\phi_i:\operatorname{int}K_i\to\mathbb R$: a convex $C^3$ function that tends to $+\infty$ at the boundary, with $|\nabla^3\phi_i(x)[h,h,h]|\le2\|h\|^3_{\nabla^2\phi_i(x)}$ and $\nabla\phi_i^\top(\nabla^2\phi_i)^{-1}\nabla\phi_i\le1$. Its Fenchel conjugate is $\phi_i^*(y)=\sup_{x\in\operatorname{int}K_i}\langle x,y\rangle-\phi_i(x)$. The algorithm reaches $\phi_i$ and $\phi_i^*$ only through constant-time oracles.

The regularized block Lewis weight of $B\in\mathbb R^{n\times d}$ solves $w=\operatorname{tr}_G(P(W^{1/2-1/p}B))+v$, where $W$ is block diagonal with blocks $w_iI_{n_i}$, $P$ is the orthogonal projection onto the column space, and $\operatorname{tr}_G$ is the vector of block traces. The method follows the central path weighted by $\tau(x)=w(\widetilde C(x,\nabla^2\Phi(x)))$, where $\widetilde C$ is the smoothed preconditioner, the root of $\mathbb E_u[\nabla^2\phi_i(x_i+\sigma M_i^{-1/2}u)^{-1}]$ over the uniform law on the unit ball.

Formalization targets

Goal: Theorem 54, corrected

For every $e>0$ there are one program $P$ of a real RAM with the two oracles, and constants $C,k$, such that for every instance with $d\ge1$, every $\kappa$ bounding $K_i$, $c_i$ and $\|A_i\|_{\mathrm{op}}$ and admitting a feasible $z$ with $B(z_i,1/\kappa)\subseteq K_i$, and every $\delta>0$: with probability at least $1-(n+2)^{-e}$ the run halts within

$$C\,n_{\max}^k\,(nd+d^{5/2})\,(\log(n+d+\kappa+1/\delta+2))^k$$

steps, with an output $x\in K$, $A^\top x=b$ and $c^\top x\le\min c^\top y+\delta$. The manuscript's statement has no feasibility hypothesis and is false on infeasible instances; the corrections are declared on the item.

Milestones

In the order of the proof: the extended program with its start point and transfer (Lemma 49); stability of Lewis weights (Lemma 21); the smoothing estimates (Lemmas 23, 24); one-step stability of $C$, $\tau$, $\mu$ (Lemmas 28, 30, 31); potential change and contraction (Lemmas 34, 20); approximate feasibility and sampling (Lemmas 37, 38); finite-sum smoothing (the display in the proof of Lemma 42); the nearby sequence (Lemmas 51, 52); and exact feasibility with the final gap (Lemma 50). Matrix Bernstein and the bound $\omega<5/2$ are referenced from existing platform theorems.

Significance

The result gives the first $\widetilde O(\sqrt d)$-iteration path following for black-box self-concordant barriers on constant-dimensional blocks, and removes the $\sqrt n$ of the earlier bound, moving the nearly linear time threshold from $n\ge d^{10}$ to $n\ge d^{3/2}$. The smoothed preconditioner replaces the higher-order self-concordance that earlier Lewis-weight analyses need.

The theorem is claimed in an unpublished manuscript; nothing in it is machine-checked. This mission adds block Lewis weights, the Bregman potential and a concrete model of computation with oracles to the platform, and states the main theorem and its key steps. Its corrected statements have counterexamples recorded on the items: Theorem 54, Lemma 37, Lemma 38, Lemma 49. The goal is open as a formal statement, and its proof must also handle points the manuscript leaves to adaptation, such as rank-deficient $A$.

Difficulty

The direct extension of scalar Lewis-weight arguments fails. A block carries one weight but a matrix-valued local geometry, and a small multiplicative change of a general positive definite preconditioner need not change the weights by a small relative amount. The analysis needs a Lipschitz derivative of $\nabla^2\phi^{-1/2}$ along sampled sparse updates, and ordinary self-concordance controls only one derivative of the Hessian: the naive use of $\nabla^2\phi^{-1/2}$ as preconditioner, as in the scalar proof, therefore has no second-order estimate.

A second obstacle is that the time bound rests on lazy data structures against adaptive updates by matrix-valued blocks. A count of iterations does not give the time.

Formalization scope

Coordinates are pairs (block, position). The model is a real RAM with a finite program, rational literals, $+,-,\times,\div,\sqrt{\cdot},\exp,\log$, comparisons, integer pointers, a tape of Gaussian reals, and the two oracles, with charges $(1+n_i)^2$ and $1+n_i$. A primal query outside $\operatorname{int}K_i$ stops the run. There is no floor, sort, or matrix instruction, the program is chosen before the instance, and $K_i$, $\kappa$ and $z$ are not in memory, which rules out a trivial solution by hard-coding or free computation. The minimum is written as $\forall$ feasible $y$, so no junk infimum enters.

Milestones use one constant order: hidden constants for each bound on the block sizes, then $C$, then $C_{\mathrm{Var}}$. They assume $m\ge2$ and full column rank where the page uses $P(\cdot)$. Expectations in one-step lemmas are conditional on the good event of the sampling definition, since $x^{(\mathrm{new})}\in\operatorname{int}K$ is known only there.

The definitions of self-concordant barrier, real RAM and the uniform law on the ball are reused from the platform. Block Lewis weights, mixed norms and the machine are reusable beyond this mission. Contributions welcome: proofs of any milestone, the Lewis-weight existence and uniqueness of Lemma 57, Lemma 3-style Hessian comparisons for the barrier predicate, and data structures in the machine.

Selected references

• P. Zhang, S. Wright, A Fast Lewis-weight Interior Point Method for Linear Optimization over Product-Domain, manuscript, November 2026, sha256 66072000….
• J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Math. Programming 40, 1988. https://doi.org/10.1007/BF01580724
• Y. T. Lee, A. Sidford, Path finding methods for linear programming, FOCS 2014. https://arxiv.org/abs/1312.6677
• Y. T. Lee, A. Sidford, Solving linear programs with Sqrt(rank) linear system solves, 2019. https://arxiv.org/abs/1910.08033
• J. van den Brand, Y. T. Lee, Y. P. Liu, T. Saranurak, A. Sidford, Z. Song, D. Wang, Minimum cost flows, MDPs, and $\ell_1$-regression in nearly linear time for dense instances, STOC 2021. https://arxiv.org/abs/2101.05719
• Y. P. Liu, R. Peng, C. Tang, A. Weng, J. Yang, Adaptive matrix sparsification and applications to empirical risk minimization, 2025. https://arxiv.org/abs/2512.02003

Motivation

Empirical risk minimization (ERM) is a convex optimization problem that covers linear and $\ell_p$ regression, LASSO, logistic regression, support vector machines and quantile regression. Its dual form is

$$\min_{x\in K_1\times\cdots\times K_m,\ A^\top x=b} c^\top x,$$

with $A\in\mathbb R^{n\times d}$ and compact convex sets $K_i\subseteq\mathbb R^{n_i}$ of constant dimension. The same form captures the minimum enclosing ball problem of computational geometry, a long-studied primitive in support vector machines and computer graphics (Liu et al., §1.1–§1.2). In statistics the interesting regime is tall: many more data points than dimensions, $n\gg d$, with $A$ dense. There the input has size $nd$, so a running time near $nd$ is what one can hope for.

Timeline, as cited by the source:

• 1994: Nesterov and Nemirovskii, interior point methods from self-concordant barriers (NN94).
• 2019: Lee, Song and Zhang solve the form above in time $n^{\max\{\omega,2+1/6\}}$, transferring the square-regime linear programming bound to ERM with a robust central path of $\tilde O(\sqrt n)$ iterations (arXiv:1905.04447).
• 2020: van den Brand, Lee, Sidford and Song solve tall dense linear programs in nearly linear time, on the Lee–Sidford $\tilde O(\sqrt d)$-iteration method (arXiv:2002.02304).
• 2021: van den Brand et al. reach $\tilde O(nd+d^{2.5})$ for tall linear programs (arXiv:2101.05719). Neither the Lee–Sidford method nor Vaidya's volumetric barrier is known to extend to general ERM.
• 2021–2022: for tall ERM with constant $n_i$, Dong, Lee and Ye obtain $\tilde O(nd^2)$ and Gu and Song $\tilde O(nd^{(\omega+1)/2})$ (as cited on p.5 of the source).
• 2026: Liu, Peng, Tang, Weng and Yang, this source, $\tilde O(nd+d^6\sqrt n)$: the first bound with leading term $nd$ for ERM, a question open since 2019 (p.5).

Setting

An ERM instance consists of $m$ blocks with $1\le n_i\le C_K$, $n=\sum_in_i$, a matrix $A\in\mathbb R^{n\times d}$, vectors $b\in\mathbb R^d$, $c\in\mathbb R^n$, and a bound $\kappa$. Each compact convex $K_i\subseteq[-\kappa,\kappa]^{n_i}$ is accessed only through a self-concordant barrier $\phi_i:\operatorname{int}K_i\to\mathbb R$: a convex function that tends to $+\infty$ at the boundary and satisfies $|\phi_i'''[h,h,h]|\le2\phi_i''[h,h]^{3/2}$ and $\phi_i'[h]^2\le\nu_i\phi_i''[h,h]$. An oracle returns $\phi_i$, $\nabla\phi_i$ and $\nabla^2\phi_i$ at a point of $\operatorname{int}K_i$. The entries of $A,b,c$ are at most $\kappa$ and $A^\top A\succeq\kappa^{-1}I$.

The leverage score of a row $a_i$ of $A$ is $\tau_i=a_i^\top(A^\top A)^{-1}a_i$. A family of overestimates $\tilde\tau_i\ge\tau_i$ with small sum tells one how to sample rows so that the sampled Gram matrix approximates $A^\top A$ in the Loewner order. A batch is a set of row insertions and deletions given at once; the adversary is adaptive when it sees the published $\tilde\tau$ before choosing the next batch.

Formalization targets

Goal: Theorem 1, pp.6–7 (corrected)

For every $C_K$ and $c>0$ there are one program $P$ of a randomized real-arithmetic oracle machine and constants $C,k$ such that for all admissible instances and all $\varepsilon>0$, with probability at least $1-(n+2)^{-c}$, $P$ halts within

$$C\,(nd+d^6\sqrt n)\,\big(\log(n+d+\kappa+1/\varepsilon+2)\big)^k$$

units of work with an $x$ satisfying $x_i\in K_i$ for all $i$, $A^\top x=b$, and $c^\top x\le\varepsilon+c^\top y$ for all feasible $y$.

Admissibility adds two hypotheses to the printed theorem: a feasible $z$ with $B(z_i,1/\kappa)\subseteq K_i$, and given start points $w_i$ with $B(w_i,1/\kappa)\subseteq K_i$. As printed, an infeasible instance meets every hypothesis.

Theorem 3, p.7

Leverage score overestimates under $Q$ adaptive batches of row updates of total size $O(n)$, with $\kappa^{-1}I\preceq A^\top A\preceq\kappa I$ throughout: $\tilde\tau_i\ge\tau_i$, $\sum_i\tilde\tau_i\le\tilde O(d)$, total work $\tilde O(nd+Qd^6)$.

Milestones

The analysis of one interior point step (Lemmas 4.10, 4.11, 4.13, 4.7), the stability of the iterates (Lemma 4.15), the sampling of the step (Lemma 6.3), the matrix sampling lemma (Lemma 2.3, corrected), the decremental estimates (Lemmas 5.1, 5.3, 5.5, 5.6, the last two corrected), the Hessian comparisons (Lemmas C.2, C.3) and the final point (Lemma 6.4).

Significance

The result. The bound is nearly linear in the input size when $A$ is dense and $n\ge d^{10}$. It extends nearly-linear tall linear programming to general ERM with blocks of constant dimension, and it yields the first nearly-linear algorithm for minimum enclosing ball with logarithmic dependence on $\varepsilon$ (Corollary 1.1). Theorem 3 is of independent interest: earlier dynamic leverage score structures handle graph Laplacians or matrices of the form $A^\top DA$ for a fixed $A$.

Formalizing it. The source is an unpublished manuscript, and no part of this is machine-checked. The statement of Theorem 1 has been corrected, so a formal proof of the corrected form would also settle what the printed one should say. The mission adds to the platform a concrete machine model for interior point running times, a block ERM vocabulary, and the first formal statement of an adaptive sparsifier. Status: the source argues all of it, and [LSZ19, Lemmas D.2, D.3] and [Nes98] are cited rather than proved there.

Difficulty

An inserted row has no history, so it cannot be sketched in advance: the standard approach of maintaining a fixed matrix under a changing diagonal does not apply. A heavy-hitter data structure queried directly on this sequence fails, because the interior point method chooses its next updates after seeing the sparsifier sampled from the published estimates, so the structure's inputs depend on its own randomness. An obvious alternative, recomputing all leverage scores in each of the $\tilde O(\sqrt n)$ iterations, costs about $\sqrt n\cdot nd$. A second obstacle is that the iterate $x$ itself is not $\ell_2$-stable under subsampling, so the number of updates to its approximation does not follow from a bound on the step size.

Formalization scope

Machine. One finite instruction list on the published real RAM core (SmaleNinth.RAMInstr), extended with integer pointers, $\sqrt{\cdot}$, $\exp$, a Gaussian tape and the barrier oracle; rational literals only; unit cost; no logarithm, floor, sort or matrix instruction. An oracle call outside $\operatorname{int}K_i$ faults. The program and constants are chosen before the instance, so nothing can be hard-coded: a per-instance program, a function-valued instruction or a real literal would trivialize the claim.

Conventions. Blocks are consecutive coordinates. The barrier predicate is the published IsNuSelfConcordantBarrier, the line form of Definition 3.1, with $\nu_i\le C_K$. The minimum is a bound against every feasible point. Failure probabilities are explicit, and bad events are bounded in outer measure. Adversaries and policies are measurable. Theorem 1's accuracy $\varepsilon$, the small constant $\varepsilon$ of §4 and $\epsilon_{\mathrm{checker}}$ of §5 are distinct. Item-level corrections and readings are listed in each statement.

Infrastructure and contributions. A complete development needs self-concordance calculus (Dikin ellipsoid, Hessian stability), matrix Bernstein, Johnson–Lindenstrauss (already on the platform), a dynamic heavy hitter, and a real-RAM implementation layer. All except the last are reusable beyond this mission. Proofs of any milestone are welcome, as are intermediate lemmas such as Lemmas 4.8, 4.9, 4.12, 5.7 and C.1, and sharper forms of the time bound.

Selected references

• Y. P. Liu, R. Peng, C. Tang, A. Weng, J. Yang, Adaptive Matrix Sparsification with Applications to Empirical Risk Minimization and Computational Geometry, manuscript, 2026 (the source, sha256 7a66a27b…; no public link).
• Y. T. Lee, Z. Song, Q. Zhang, Solving empirical risk minimization in the current matrix multiplication time, COLT 2019. https://arxiv.org/abs/1905.04447
• J. van den Brand, Y. T. Lee, A. Sidford, Z. Song, Solving tall dense linear programs in nearly linear time, STOC 2020. https://arxiv.org/abs/2002.02304
• J. van den Brand, Y. T. Lee, D. Nanongkai, R. Peng, T. Saranurak, A. Sidford, Z. Song, D. Wang, Bipartite matching in nearly-linear time on moderately dense graphs, FOCS 2020. https://arxiv.org/abs/2009.01802
• J. van den Brand, Y. T. Lee, Y. P. Liu, T. Saranurak, A. Sidford, Z. Song, D. Wang, Minimum cost flows, MDPs, and $\ell_1$-regression in nearly linear time for dense instances, STOC 2021. https://arxiv.org/abs/2101.05719
• M. B. Cohen, Y. T. Lee, C. Musco, C. Musco, R. Peng, A. Sidford, Uniform sampling for matrix approximation, ITCS 2015. https://arxiv.org/abs/1408.5099
• Y. Nesterov, A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791

Motivation

Many engineered and natural systems are networks of identical dynamical units coupled through a directed interaction graph: arrays of oscillators, power grids, sensor and multi-agent networks, gene regulatory circuits. A basic control question for such a network is how to force every unit onto a prescribed reference trajectory (an equilibrium, a periodic orbit or a chaotic solution of a single unit) by acting on only a few of them. Applying a feedback controller to a small fraction of the vertices and letting the coupling spread its effect is called pinning control. It was introduced for scale-free networks by Wang and Chen (2002), shown to work with a single controller on undirected networks by Chen, Liu and Lu (2007), and turned into checkable criteria for undirected networks by Yu, Chen and Lü (2009).

Directed networks are harder. Earlier criteria for directed networks (Zhou, Lu and Lü 2008; Song and Cao 2010) were stated through the symmetric part $G+G^T$ of the coupling matrix, which may have eigenvalues with positive real part even when the network synchronizes, so they lose the structural information of the graph. Yu, Chen, Lü and Kurths (SIAM J. Control Optim., 2013) replaced the standard quadratic Lyapunov function by one weighted with the positive left null vector of the coupling matrix. This mission formalizes their main criterion for strongly connected networks (§3 of the paper) together with the matrix-theoretic lemmas it rests on (§2).

Setting

The network has $N$ vertices with states $x_i(t)\in\mathbb R^n$. A coupling matrix $G=(G_{ij})\in\mathbb R^{N\times N}$ has $G_{ij}\ge 0$ for $i\ne j$ ($G_{ij}>0$ means a connection from vertex $j$ to vertex $i$) and zero row sums, $G_{ii}=-\sum_{j\ne i}G_{ij}$. The network is strongly connected if any vertex can be reached from any other by a directed path; $G$ is irreducible if no simultaneous permutation of rows and columns brings it to block lower-triangular form $\begin{pmatrix}\tilde G_{11}&0\\\tilde G_{21}&\tilde G_{22}\end{pmatrix}$ with square diagonal blocks of sizes $m$ and $N-m$, $1\le m\le N-1$. The in-degree of vertex $i$ is $k_i^{\mathrm{in}}=\sum_{j\ne i}G_{ij}$.

Each vertex runs the dynamics $\dot x=f(x,t)$ for a continuously differentiable $f:\mathbb R^n\times\mathbb R_+\to\mathbb R^n$. A reference trajectory $s$ solves $\dot s=f(s,t)$. With coupling strength $c$, inner coupling matrix $\Gamma\in\mathbb R^{n\times n}$ and control gains $d_i\ge0$ (vertex $i$ is pinned when $d_i>0$), the controlled network is

$$\dot x_i=f(x_i,t)+c\sum_{j=1}^N G_{ij}\Gamma x_j-c\,d_i\Gamma(x_i-s),\qquad i=1,\dots,N.$$

It is globally synchronized if $x_i(t)-s(t)\to0$ for every $i$, every reference trajectory and every solution. The vector field satisfies Assumption 1 if, for a constant matrix $K$,

$$(x-y)^T\bigl(f(x,t)-f(y,t)\bigr)\le(x-y)^TK\Gamma(x-y)\qquad\forall x,y\in\mathbb R^n,\ t\ge0 .$$

For positive weights $\xi_1,\dots,\xi_N$ put $\Xi=\operatorname{diag}(\xi)$, $D=\operatorname{diag}(d)$ and $\widehat G=\tfrac12(\Xi G+G^T\Xi)$.

Formalization targets

Goal: Theorem 3.1 (p. 1402)

Let $f$ satisfy Assumption 1 with $\Gamma$ symmetric, let $G$ be a strongly connected coupling matrix, and let $\xi$ be positive with $\widehat G$ having zero row sums (the weights of Lemma 2.12). If

$$\Xi\otimes\frac{K\Gamma+\Gamma^TK^T}{2}+c\,\widehat G\otimes\frac{\Gamma+\Gamma^T}{2}-c\,(\Xi D)\otimes\frac{\Gamma+\Gamma^T}{2}<0,$$

then the controlled network is globally synchronized.

Milestones

The path to the goal follows the paper: Lemma 2.5 (irreducible $\iff$ strongly connected), Lemma 2.9 ($\rho(A)=\|A\|_\infty$ for nonnegative $A$ with constant row sums), Lemma 2.8 (Perron–Frobenius, already on the platform), Lemma 2.11 (a positive vector $x$ with $G^Tx=0$), Lemma 2.12 (the weights $\Xi$), and the derivative estimate (3.4) for $V=\tfrac12\sum_i\xi_ie_i^Te_i$, $e_i=x_i-s$:

$$\dot V\le e^T\bigl[\Xi\otimes(K\Gamma)+c(\widehat G-\Xi D)\otimes\Gamma\bigr]e .$$

Companion results

Lemma 2.7, Lemma 2.10, and, under the paper's standing assumptions ($K\Gamma=\Gamma K$, $\theta=\lambda_{\max}(\tfrac{K+K^T}{2})\ge0$) with $\Gamma$ positive definite: Corollary 3.2 (the $N\times N$ condition $\theta\Xi+c(\widehat G-\Xi D)<0$ suffices), Corollary 3.3 (i) (an explicit coupling threshold $c>\lambda_{\max}(\theta\Xi)/|\lambda_{\max}(\widehat G-\Xi D)|$), and Corollary 3.4 (the necessary conditions $d_i>\theta/c-k_i^{\mathrm{in}}$ at pinned and $k_i^{\mathrm{in}}>\theta/c$ at unpinned vertices).

Significance

The criterion reduces global synchronization of an $nN$-dimensional nonlinear system to one linear matrix inequality in the data $(G,\Gamma,K,c,D)$, and the corollaries reduce it further to an $N\times N$ inequality and to explicit bounds. Corollary 3.4 turns this into a pinning rule: vertices whose in-degree is below $\theta/c$ must be controlled. Weighting by the left null vector of $G$ is the device that later work on directed consensus and pinning reuses; Lemmas 2.11 and 2.12 isolate it as a statement about Metzler matrices.

The paper's results are proved on paper; none of them has a machine-checked proof that this mission is aware of. A formalization adds three things: a corrected statement of Theorem 3.1 (see the scope section), a Lean library of directed-network matrix facts (irreducibility in the permutation form, its equivalence with strong connectivity, positive left null vectors, the weighted symmetrization $\widehat G$), and a reusable Lyapunov argument for linearly coupled networks with Kronecker-structured quadratic forms.

Difficulty

The obvious first idea, the unweighted Lyapunov function $\tfrac12\sum_ie_i^Te_i$, produces the symmetric part of $G$, which for a directed network need not be negative semidefinite; this is exactly the defect of earlier criteria. The weights must come from a positive left null vector of $G$, whose existence is a Perron–Frobenius statement that needs irreducibility, hence the graph–matrix equivalence of Lemma 2.5. The analytic part needs a derivative of $V$ along solutions on $[0,\infty)$, the conversion of a sum over vertices into a Kronecker quadratic form, and the passage from a negative definite form to convergence of every error component. On the Mathlib side, irreducibility in the paper's permutation sense, spectral radius through characteristic roots, and largest eigenvalues of symmetric matrices all have to be connected to existing API.

Formalization scope

States are Fin n → ℝ and matrices are indexed by Fin N, Fin n and, for Kronecker products, by pairs (i, a) with $(A\otimes B)_{(i,a),(j,b)}=A_{ij}B_{ab}$; the stacked error uses the same order. Convergence (2.7) is stated with the neighbourhood filter of $0$ in $\mathbb R^n$, which does not depend on the norm. Derivatives are taken within $[0,\infty)$. Pinning is encoded by $d_i>0$ instead of the paper's reordering of the first $l$ vertices. "$M<0$" is positive definiteness of $-M$ (Mathlib PosDef, which includes symmetry); every matrix compared with $0$ is symmetric by construction. $\lambda_{\max}(A)$ of a symmetric matrix is the least $r$ with $v^TAv\le r\,v^Tv$ for all $v$; $\rho(A)$ is the largest modulus of a complex characteristic root. Global synchronization quantifies over every reference solution and every network solution; existence of solutions is not asserted.

Added hypotheses, each disclosed in the item: $\Gamma^T=\Gamma$ in Theorem 3.1 and (3.4), because the printed theorem allows any $\Gamma$ and is then false (a directed 3-cycle with $\Gamma=\begin{pmatrix}1&3\\-3&1\end{pmatrix}$ satisfies (3.2) but its error grows); $c>0$ in Corollary 3.4; at least one pinned vertex in Corollary 3.3 (i); $N\ge1$ in Lemma 2.10. The weights $\Xi$ are not arbitrary: Theorem 3.1 and the corollaries require $\widehat G$ to have zero row sums, which for a coupling matrix is equivalent to $G^T\xi=0$. Assuming the derivative bound (3.4), negative definiteness of $\widehat G-\Xi D$ or decay of $V$ in the goal would trivialize it and is excluded.

The mission needs: graph reachability for matrices with nonnegative off-diagonal entries; Perron–Frobenius for irreducible nonnegative matrices (referenced from the platform); Gershgorin-type bounds; Kronecker products and positive definiteness; and calculus of quadratic forms along solutions. The matrix lemmas (2.5, 2.7, 2.9–2.12) are reusable beyond this mission. Proofs of any item, and alternative proofs of the milestones, are welcome. Corollary 3.3 (ii) is not posed.

Selected references

• W. Yu, G. Chen, J. Lü, J. Kurths, Synchronization via pinning control on general complex networks, SIAM J. Control Optim. 51(2) (2013), 1395–1416. https://doi.org/10.1137/100781699
• X. F. Wang, G. Chen, Pinning control of scale-free dynamical networks, Physica A 310 (2002), 521–531. https://doi.org/10.1016/S0378-4371(02)00772-0
• T. Chen, X. Liu, W. Lu, Pinning complex networks by a single controller, IEEE Trans. Circuits Syst. I 54 (2007), 1317–1326. https://doi.org/10.1109/TCSI.2007.895383
• J. Zhou, J. Lu, J. Lü, Pinning adaptive synchronization of a general complex dynamical network, Automatica 44 (2008), 996–1003. https://doi.org/10.1016/j.automatica.2007.08.016
• W. Yu, G. Chen, J. Lü, On pinning synchronization of complex dynamical networks, Automatica 45 (2009), 429–435. https://doi.org/10.1016/j.automatica.2008.07.016
• Q. Song, J. Cao, On pinning synchronization of directed and undirected complex dynamical networks, IEEE Trans. Circuits Syst. I 57 (2010), 672–680. https://doi.org/10.1109/TCSI.2009.2024971
• R. Olfati-Saber, R. M. Murray, Consensus problems in networks of agents with switching topology and time-delays, IEEE Trans. Automat. Control 49 (2004), 1520–1533. https://doi.org/10.1109/TAC.2004.834113
• R. A. Horn, C. R. Johnson, Matrix Analysis, Cambridge University Press, 1985. https://doi.org/10.1017/CBO9780511810817
• R. A. Brualdi, H. J. Ryser, Combinatorial Matrix Theory, Cambridge University Press, 1991. https://doi.org/10.1017/CBO9781107325708

Motivation

The asymptotic rank of a tensor measures how cheaply many copies of it can be computed together. For the triangle graph tensor it is the matrix multiplication exponent: $\log_2\tilde R_{\mathbb F}(\mathsf{GT}_2(K_3))=\omega_{\mathbb F}$ over every field $\mathbb F$ (Bürgisser–Clausen–Shokrollahi 1997, Prop. 15.1). Graph tensors extend this object from three parties to $n$: one tensor leg per vertex and an identity matrix on every edge. They model multilinear computation with several inputs and networks of pairwise entanglement, and their asymptotic rank and subrank were studied systematically by Christandl, Vrana and Zuiddam (2019). Allowing a different dimension on every edge gives weighted graph tensors (Christandl–Gesmundo–Michałek–Zuiddam 2021, §2.3), which include rectangular matrix multiplication.

Timeline of the results this mission builds on:

• 1988: Strassen's spectral duality expresses asymptotic rank as a maximum over the asymptotic spectrum (Strassen 1988; see Wigderson–Zuiddam 2026).
• 2017: Vrana and Christandl give the minimum-cut formula for the asymptotic subrank of weighted graph tensors (VC17).
• 2019: Christandl, Vrana and Zuiddam bound the edge exponent of complete graphs by $\log_7(9/2)<0.773$ over $\mathbb C$ for $n\ge4$ and ask whether $\log_2\tilde R(\mathsf{GT}_2(K_{2m}))$ equals the maximum cut (CVZ19, Questions 1.3.1–1.3.2).
• 2026: OpenAI's polynomial-multiplication method gives $\omega_{\mathbb C}\le 9/4$; Amanov, van den Berg and Zuiddam extend it to every field (ABZ26).
• 2026: Zhou extends the method from three legs to $n$ legs and to all weighted graph tensors over every field (arXiv:2610.34273), the source of this mission.

Setting

Fix a field $\mathbb F$ and an integer $n\ge2$. A dimension matrix is a symmetric $n\times n$ matrix $Q$ of positive integers with $Q_{i,i}=1$. The edge tensor $E^{(q)}_{i,j}$ is the $n$-leg tensor $\sum_{a<q}e_a\otimes e_a$ on legs $i,j$, with a one-dimensional factor on every other leg. The weighted graph tensor is the Kronecker product of the edge tensors,

$$\mathsf{WT}(Q)=\bigotimes_{1\le i<j\le n}E^{(Q_{i,j})}_{i,j},$$

whose leg $v$ has dimension $D_v=\prod_jQ_{v,j}$. For a graph $G$, $\mathsf{GT}_q(G)=\mathsf{WT}(Q)$ with $Q_{i,j}=q$ on edges and $1$ elsewhere. The rank $R_{\mathbb F}(T)$ is the least $r$ with $T\preceq I_n(r)$ (restriction to the diagonal tensor), and $\tilde R_{\mathbb F}(T)=\lim_NR_{\mathbb F}(T^{\otimes N})^{1/N}$.

The logarithmic edge-weight matrix is $W_{i,j}=\log_2Q_{i,j}$. For a nonempty proper vertex set $S$, $\mathrm{cut}_W(S)=\sum_{i<j,\ |\{i,j\}\cap S|=1}W_{i,j}$, and $\mathrm{MaxCut}(W)$ is the largest cut weight. With $J$ the all-one matrix and $\mathrm{COP}_n$ the cone of copositive matrices ($a^{\mathsf T}Xa\ge0$ for all $a\ge0$), the path-strengthened completely positive bound is

$$U^\Delta_{\mathrm{CP}}(W)=\max\Big\{\sum_{i<j}W_{i,j}P_{i,j}:\ P=P^{\mathsf T},\ P_{i,i}=0,\ P\ge0,\ J-2P\in\mathrm{COP}_n,\ P_{i,j}\le P_{i,k}+P_{k,j}\Big\},$$

the path inequalities ranging over all distinct $i,j,k$.

Formalization targets

Goal: Theorem 1.2

$$\mathrm{MaxCut}(W)\ \le\ \log_2\tilde R_{\mathbb F}\big(\mathsf{WT}(Q)\big)\ \le\ U^\Delta_{\mathrm{CP}}(W)$$

for every field $\mathbb F$, every $n\ge2$ and every dimension matrix $Q$. The statement fixes no characteristic, no $n$ and no edge dimension.

Milestones

1. Cut lower bound: the flattening rank across $S$ is $2^{\mathrm{cut}_W(S)}$ (Lemma A.3), hence $\mathrm{MaxCut}(W)\le\log_2\tilde R$, with equality for bipartite support (Proposition A.4).
2. Spectral formula: Strassen duality (Theorem 2.20); a spectral point $\phi$ is determined on weighted graph tensors by its edge weights $P^{(\phi)}_{i,j}\in[0,1]$ (Lemma 2.25); and $\log_2\tilde R(\mathsf{WT}(Q))=\Gamma_{\mathbb F}(W)=\max_\phi\sum_{i<j}W_{i,j}P^{(\phi)}_{i,j}$ (Lemma 2.28).
3. Complete graphs: polynomial multiplication has asymptotic rank $1+\sum_j(a_j-1)$ (Lemma 3.2); the entropy inequality (Corollary 3.5); the symmetric spectral profile is normalized, discretely concave and satisfies shifted tripling (Lemmas 4.2, 4.5, 4.8); diagonal growth (Lemma 4.9); and $\lfloor n^2/4\rfloor\le\log_2\tilde R_{\mathbb F}(\mathsf{GT}_2(K_n))\le n^2/4$ (Theorem 4.10 = Theorem 1.1).
4. Conic constraints: $J-2P^{(\phi)}$ is copositive (Lemma 5.1, eq. (8)) and $P^{(\phi)}$ satisfies the path inequalities (Lemma 5.4).

Significance

For $Q$ with entries $2$ on the edges of a graph $G$, the goal bounds $\log_2\tilde R(\mathsf{GT}_2(G))$ between the maximum cut and an explicit conic program, over every field. Theorem 4.10 settles the [CVZ19] maximum-cut question for even complete graphs, $\log_2\tilde R(\mathsf{GT}_2(K_{2m}))=m^2$, and gives edge exponents below $2/3$ for $n\ge5$, against the previous $0.7723$. For $K_3$ it contains $\omega\le9/4$ over every field. Every feasible $P$ for $U^\Delta_{\mathrm{CP}}$, and every completely positive cover, is a checkable certificate for an upper bound on asymptotic rank.

The results are proved on paper in the source, which cites Strassen's duality without proof. No statement about graph tensors, weighted graph tensors or asymptotic rank of tensors of order above three is on the platform; the abstract duality theorem is formalized inside the published mme_duality development, and $\omega_{\mathbb C}\le9/4$ exists as a separate platform theorem. A formal proof would add the first machine-checked bound for higher-order graph tensors and a verified link between the asymptotic spectrum and copositive programming.

Difficulty

The lower bound is a flattening argument. The upper bound is not: a bound of the form $\phi(\mathsf{WT}(Q))\le2^{U}$ must hold for every spectral point, and the spectrum is known only abstractly. The obvious route, bounding the rank of $\mathsf{WT}(Q)$ or of its powers by an explicit decomposition, gives at best $\sum_{i<j}W_{i,j}$ and cannot reach $n^2/4$ for $K_n$. The paper instead constrains $P^{(\phi)}$ through the complete-graph estimate, whose proof needs a separation construction on $n-2$ shared legs at linear cost, an interpolation resource of asymptotic rank $D$ over every field (including small finite fields, where Lagrange interpolation is unavailable), two polynomial degenerations, and a growth argument on a profile symmetrized over all $n!$ leg permutations. The passage from $K_A$ to arbitrary weights then needs vertex grouping and a continuity argument from integer to real vertex weights.

Formalization scope

Tensors are the published MME.TensorObj (finite-dimensional leg spaces and an element of their tensor product), with Kronecker sum and product, restriction, rank, asymptotic rank $\inf_{N\ge1}R(T^{\otimes N})^{1/N}$ (which the paper shows equals the limit), flattening rank, degeneration and leg permutations from the published MME library. Spectral points are the published monotone semiring homomorphisms on the tensor semiring modulo mutual restriction. $\mathsf{WT}(Q)$ is defined in product coordinates: leg $v$ is indexed by tuples $(\lambda_{v,j})_j$ instead of mixed-radix numbers, a relabeling within each leg. Vertices are $\mathrm{Fin}\,n$, sums are over unordered pairs $i<j$, $\log_2$ is Real.logb 2, and the entropy in Corollary 3.5 is natural. $\mathrm{MaxCut}$, $\Gamma_{\mathbb F}$ and $U^\Delta_{\mathrm{CP}}$ are real suprema of nonempty bounded families, equal to the paper's maxima.

Copositivity is not positive semidefiniteness: requiring $J-2P\succeq0$ gives a smaller program whose relation to $\Gamma_{\mathbb F}$ the paper leaves open. The path inequalities range over all distinct triples, including non-edges, and the sums are not doubled over ordered pairs.

New definitions in the mission: dimension matrices, $\mathsf{WT}$, edge and graph tensors, cuts, $U^\Delta_{\mathrm{CP}}$, spectral edge weights, $\Gamma_{\mathbb F}$, asymptotic restriction, polynomial multiplication tensors, the profile, and aligned partial direct sums (stated as a predicate). A complete proof needs, beyond the milestones, a concrete bridge between the platform's abstract Strassen duality and MME.tensorAsymptoticRank, Fekete-type limits for Kronecker powers, the separation theorem (Theorem 3.4), and the degenerations of Lemmas 4.4 and 4.7. The edge-tensor, flattening and polynomial-multiplication layers are reusable for other graph-tensor and matrix-multiplication missions. Proofs of any milestone, of intermediate lemmas posed by solvers, and of the duality bridge are welcome.

Selected references

• H. Zhou, Asymptotic Rank of Weighted Graph Tensors via Completely Positive Covers, arXiv:2610.34273, 2026. https://arxiv.org/abs/2610.34273
• V. Strassen, The asymptotic spectrum of tensors, J. reine angew. Math. 384 (1988) 102–152. https://doi.org/10.1515/crll.1988.384.102
• M. Christandl, P. Vrana, J. Zuiddam, Asymptotic tensor rank of graph tensors: beyond matrix multiplication, Computational Complexity 28 (2019) 57–111. https://doi.org/10.1007/s00037-018-0172-8
• M. Christandl, P. Vrana, J. Zuiddam, Universal points in the asymptotic spectrum of tensors, J. Amer. Math. Soc. 36 (2023) 31–79. https://doi.org/10.1090/jams/996
• A. Wigderson, J. Zuiddam, Asymptotic spectra: theory, applications, and extensions, Bull. Amer. Math. Soc. 63 (2026) 199–331. https://doi.org/10.1090/bull/1880
• P. Vrana, M. Christandl, Entanglement distillation from Greenberger–Horne–Zeilinger shares, Comm. Math. Phys. 352 (2017) 621–627. https://doi.org/10.1007/s00220-017-2861-6
• M. Christandl, F. Gesmundo, M. Michałek, J. Zuiddam, Border rank nonadditivity for higher order tensors, SIAM J. Matrix Anal. Appl. 42 (2021) 503–527. https://doi.org/10.1137/20M1357366
• A. Amanov, M. van den Berg, J. Zuiddam, Multiplying matrices via polynomials: exposition and barriers, arXiv:2610.30054, 2026. https://arxiv.org/abs/2610.30054
• P. Bürgisser, M. Clausen, M. A. Shokrollahi, Algebraic Complexity Theory, Springer, 1997. https://doi.org/10.1007/978-3-662-03338-8

Why conductance of hypergraphs needs a spectral bound

The conductance of a graph measures its worst bottleneck: the smallest ratio of the weight crossing a cut to the volume of the smaller side. Cheeger's inequality for graphs, proved by Alon and Milman (JCTB 1985) and Alon (Combinatorica 1986), bounds conductance on both sides by an eigenvalue. Since an eigenvalue is computable and a minimum over cuts is not obviously so, this connection underlies spectral partitioning and the analysis of expanders and of random walks.

Many networks have interactions among more than two nodes, and hypergraphs model them. There the choice of operator matters. Banerjee (Linear Algebra Appl. 2021) introduced the matrix used here and obtained $\phi_h(H)\le(\Upsilon_H-1)\sqrt{(2-\nu_2(H))\nu_2(H)}$ for connected $H$, whose upper bound grows with the rank. Chan, Louis, Tang and Zhang (JACM 2018) obtained $\gamma_2/2\le\phi_h(H)\le\sqrt{2\gamma_2}$, but for the eigenvalue $\gamma_2$ of a nonlinear diffusion operator, not of a fixed matrix. Kamal and Bagchi's STOC 2027 submission states a bound for the fixed matrix with no rank in the upper side.

Setting: hypergraphs, conductance, and the normalized Laplacian

A hypergraph is $H=(V_H,E_H,w_H)$: a set $V_H$ of $n$ vertices, hyperedges $E_H\subseteq 2^{V_H}$, none of size one, and weights $w_H(e)\in[0,\infty)$. The degree of $u$ is $d_H(u)=\sum_{e\ni u}w_H(e)$, the volume of $S$ is $\mathrm{vol}_H(S)=\sum_{v\in S}d_H(v)$, and the rank $\Upsilon_H$ is the largest hyperedge size. $H$ is connected if any two vertices are joined by a sequence of hyperedges whose consecutive members intersect. A 2-graph has all hyperedges of size two.

For $\emptyset\subsetneq S\subsetneq V_H$, the edge boundary $\partial_h(S)$ is the set of hyperedges meeting both $S$ and $V_H\setminus S$, and

$$\phi_h(S)=\frac{\sum_{e\in\partial_h(S)}w_H(e)}{\min(\mathrm{vol}_H(S),\mathrm{vol}_H(V_H\setminus S))},\qquad \hat\phi_h(S)=\frac{\sum_{e\in\partial_h(S)}\frac{w_H(e)}{|e|-1}|e\cap S||e\cap(V_H\setminus S)|}{\min(\mathrm{vol}_H(S),\mathrm{vol}_H(V_H\setminus S))}.$$

The conductance $\phi_h(H)$ and the diffusion conductance $\hat\phi_h(H)$ are the minima of these over all such $S$. On a 2-graph the two agree and are written $\phi_g$.

The adjacency matrix has $A_H[u,v]=\sum_{e\supseteq\{u,v\}}w_H(e)/(|e|-1)$ for $u\ne v$ and zero diagonal. With $D_H=\mathrm{diag}(d_H)$, the Laplacian is $L_H=D_H-A_H$, the normalized Laplacian is $\mathcal L_H=D_H^{-1/2}L_HD_H^{-1/2}$, and $\nu_1(H)\le\nu_2(H)\le\dots\le\nu_n(H)$ are its eigenvalues.

The AE graph $G_H$ replaces each hyperedge $e$ by a clique with edge weights $w_H(e)/(|e|-1)$, adding weights over repeated pairs.

Formalization targets

Goal: Theorem 4.1

For every connected hypergraph $H$,

$$\frac{\nu_2(H)}{\Upsilon_H}\le\phi_h(H)\le\sqrt{2\nu_2(H)}.$$

Both sides are the goal, for every rank and all weights in $[0,\infty)$.

Milestones

In proof order: the quadratic form (5) of $L_H$; the Rayleigh characterization (7) of $\nu_2$; the classical inequality for 2-graphs,

$$\frac{\nu_2(G)}{2}\le\phi_g(G)\le\sqrt{2\nu_2(G)};$$

Lemma 3.3 ($H$ and $G_H$ have identical $A$, $L$, $\mathcal L$); the bound (12) on $\phi_g(G_H)$; Lemma 3.4 ($\phi_g(T)=\hat\phi_h(T)$ on $G_H$); the bound

$$\frac{\nu_2(H)}{2}\le\hat\phi_h(H)\le\sqrt{2\nu_2(H)};\tag{13}$$

and the comparisons (1) and (2),

$$\phi_h(H)\le\hat\phi_h(H)\le\frac{\Upsilon_H}{2}\phi_h(H).$$

What the result gives

The result. For a fixed symmetric matrix, the upper bound on conductance loses no factor depending on the rank, which improves Banerjee's bound for connected hypergraphs in that respect. The paper uses this bound for its applications: a family of hypergraph expanders, higher-order inequalities, and spectral partitioning. Those applications are outside this mission.

The formalization. This mission gives the platform a hypergraph Laplacian, a hypergraph conductance and a hypergraph Cheeger statement. None of the mission's statements has a machine-checked proof yet. The paper is a submission, and its Theorem 3.1 is cited rather than proved there. The platform has a proved Cheeger inequality for irreducible reversible Markov chains, MarkovMixing.cheeger_inequality, attached as a reference item. It is stated in other vocabulary and does not state Theorem 3.1. A proof must translate it, and must separately handle hypergraphs that are connected but not irreducible as chains.

Where the difficulty lies

The obvious first idea is to apply graph Cheeger to a clique expansion and read off $\phi_h$. That fails, because no clique expansion's cut weight equals the numerator of $\phi_h$: a crossing hyperedge counts once in $\phi_h$, but $|e\cap S||e\setminus S|/(|e|-1)$ times in $\hat\phi_h$. The factor varies with the cut, between $1$ and $|e|/2$. So the spectral bound attaches to $\hat\phi_h$, and any statement about $\phi_h$ must pay a comparison that is lossy on one side only. Equality in Lemma 3.3 is also not free of care: the degree identity $\sum_vA_H[u,v]=d_H(u)$ depends on the excluded singleton hyperedges.

The main analytic content is the classical inequality for 2-graphs. Its weighted statement here also covers graphs with zero weights, where the chain is reducible and the Markov chain theorem above does not apply as stated.

Formalization scope

Vertices are a finite type $V$ with $2\le|V|$. Hyperedges form a Finset (Finset V), so there are no parallel hyperedges, and weights are a function read only on hyperedges. The empty hyperedge is allowed, as on the page, and enters no sum. All of $|e|-1$ are real subtractions.

Weights may vanish, so a connected $H$ can have a vertex of degree $0$ or be disconnected in weight. No positivity is assumed. In those cases $D_H^{-1/2}$ has entry $1/\sqrt0=0$ and a set's conductance is $0/0=0$, both Lean conventions on inputs the page leaves undefined. Then $\nu_2(H)=0=\phi_h(H)$. Connectedness ignores weights, and a zero-weight hyperedge counts for the rank.

$\nu_2$ is the published AlonMilman.PropertyT.lambda1, the second-smallest eigenvalue with multiplicity of a real symmetric matrix. Minima over sets are real infima over the finite subtype of proper nonempty subsets, and the minima in (7) are stated with IsLeast over nonzero vectors. The AE graph is in merged form, so it is again a hypergraph with all hyperedges of size 2. A pair of total weight $0$ stays an edge, which keeps it connected.

A trivializing reading is ruled out: $\nu_2$ is not at a junk value, since it is the true second-smallest eigenvalue and is nonnegative, so the square root is meaningful.

A complete development needs Rayleigh–Ritz for $\mathcal L_H$, the finite-sum identities behind Lemmas 3.3 and 3.4, the connectedness of $G_H$, and the 2-graph inequality, whether through the Markov route or directly. The hypergraph layer is reusable for the paper's other results. Contributions on any milestone are welcome.

Selected references

• N. Alon, V. D. Milman, λ₁, isoperimetric inequalities for graphs, and superconcentrators, Journal of Combinatorial Theory, Series B 38(1):73–88, 1985. https://doi.org/10.1016/0095-8956(85)90092-9
• N. Alon, Eigenvalues and expanders, Combinatorica 6(2):83–96, 1986. https://doi.org/10.1007/BF02579166
• A. Banerjee, On the spectrum of hypergraphs, Linear Algebra and its Applications 614:82–110, 2021. https://doi.org/10.1016/j.laa.2020.01.012
• T-H. H. Chan, A. Louis, Z. G. Tang, C. Zhang, Spectral properties of hypergraph Laplacian and approximation algorithms, Journal of the ACM 65(3):1–48, 2018. https://doi.org/10.1145/3178123
• R. Kamal, A. Bagchi, A Cheeger Inequality for Hypergraphs and Its Applications, STOC 2027 submission. https://arxiv.org/abs/2609.16286

Why measurement disturbance matters

Measuring a quantum system generally changes it. A qubit prepared in $|0\rangle$ and measured along the $X$ axis is left in $|+\rangle$ or $|-\rangle$, each with probability one half, and the original state is lost. The same qubit measured along the $Z$ axis returns its outcome with certainty and is left untouched. The gentle measurement lemma turns this intuition into an inequality: if one outcome of a measurement is very likely on a state, recording that outcome barely disturbs the state.

This bound is used throughout quantum Shannon theory. A decoder for classical communication over a quantum channel performs a sequence of measurements on the same received state, one test per candidate message, and it must know that the tests which pass leave the state almost intact for the tests that follow. The packing lemma, the covering lemma, the Holevo–Schumacher–Westmoreland theorem and the quantum union bound all rely on it. The ensemble version formalized here is the form that enters those coding arguments, where the disturbance must be controlled on average over a codebook rather than for one state.

The mission covers §§9.2–9.5 of M. M. Wilde, From Classical to Quantum Shannon Theory (arXiv:1106.1445v8), the fourth mission of a series that formalizes this textbook chapter by chapter.

Timeline. The lemma goes back to A. Winter's coding theorems (IEEE Trans. Inf. Theory 45, 1999), stated with the constant $\sqrt{8\varepsilon}$; the book proves it with the sharper constant $2\sqrt\varepsilon$ (Lemmas 9.4.1–9.4.3). Uhlmann's characterization of fidelity through purifications dates from 1976 (Rep. Math. Phys. 9); the relations between fidelity and trace distance are due to C. A. Fuchs and J. van de Graaf (IEEE Trans. Inf. Theory 45, 1999).

Setting

All Hilbert spaces are finite-dimensional, and all alphabets are finite. Operators on a space $\mathcal H$ of dimension $d$ are $d\times d$ complex matrices.

• A density operator $\rho$ is a positive semi-definite operator of trace one; it describes the state of a quantum system.
• The trace norm of an operator $M$ is $\|M\|_1=\operatorname{Tr}\sqrt{M^\dagger M}$, the sum of its singular values. The quantity $\|\rho-\sigma\|_1$ ranges over $[0,2]$ for density operators.
• A measurement operator is an operator $\Lambda$ with $0\le\Lambda\le I$; the probability that it detects the state $\rho$ is $\operatorname{Tr}\{\Lambda\rho\}$. Its positive square root is written $\sqrt\Lambda$.
• After the outcome $\Lambda$ is detected, the state becomes the post-measurement state $\rho'=\sqrt\Lambda\rho\sqrt\Lambda/\operatorname{Tr}\{\Lambda\rho\}$.
• An ensemble $\{p_X(x),\rho_x\}$ is a probability distribution $p_X$ on a finite alphabet $\mathcal X$ together with density operators $\rho_x$; its average density operator is $\rho=\sum_x p_X(x)\rho_x$.
• A purification of $\rho_A$ is a vector $|\psi\rangle_{RA}$ on a reference system $R$ and the system $A$ with $\operatorname{Tr}_R\{|\psi\rangle\langle\psi|_{RA}\}=\rho_A$.
• The fidelity of two density operators is $F(\rho,\sigma)=\|\sqrt\rho\sqrt\sigma\|_1^2$.
• For a channel $\mathcal N$ with Kraus operators $\{K_m\}$, $\mathcal N(X)=\sum_m K_mXK_m^\dagger$, the entanglement fidelity is $F_e(\rho,\mathcal N)=\langle\psi|(\mathrm{id}_R\otimes\mathcal N)(\psi_{RA})|\psi\rangle$ for a purification $|\psi\rangle_{RA}$ of $\rho$.

Formalization targets

Goal: gentle measurement for ensembles (Lemma 9.4.3, p. 279)

For an ensemble $\{p_X(x),\rho_x\}$ with average $\rho$, a positive semi-definite $\Lambda\le I$ and $\varepsilon\in[0,1]$ with $\operatorname{Tr}\{\rho\Lambda\}\ge1-\varepsilon$,

$$\sum_x p_X(x)\,\bigl\|\rho_x-\sqrt\Lambda\,\rho_x\,\sqrt\Lambda\bigr\|_1\le2\sqrt\varepsilon .$$

Milestones

1. Theorem 9.2.1 (Uhlmann). For purifications $|\varphi^\rho\rangle,|\varphi^\sigma\rangle$ on a common reference system, $\max_U|\langle\varphi^\rho|U_R\otimes I_A|\varphi^\sigma\rangle|^2=\|\sqrt\rho\sqrt\sigma\|_1^2$.
2. Lemma 9.2.1 (monotonicity). $F(\rho_{AB},\sigma_{AB})\le F(\rho_A,\sigma_A)$; already proved on the platform in root-fidelity form.
3. Lemma 9.4.1 (gentle measurement). If $\operatorname{Tr}\{\Lambda\rho\}\ge1-\varepsilon$, then $\|\rho-\rho'\|_1\le2\sqrt\varepsilon$.
4. Lemma 9.4.2 (gentle operator). Under the same hypothesis, $\|\rho-\sqrt\Lambda\rho\sqrt\Lambda\|_1\le2\sqrt\varepsilon$.
5. Theorem 9.5.1. $F_e(\rho,\mathcal N)=\sum_m|\operatorname{Tr}\{\rho K_m\}|^2$.

Lemma 9.4.2 is the one-element case of the goal. Lemma 9.4.1 compares $\rho$ with the normalized post-measurement state instead.

Significance

The result. The goal is the version of gentle measurement that coding theorems actually call: a decoder test $\Lambda$ that accepts the average output state with high probability changes the individual codeword states by at most $2\sqrt\varepsilon$ on average. Without it, the analysis of sequential decoding and of the packing lemma (later in this series) has no control on how earlier tests damage the state seen by later ones. Uhlmann's theorem and the Kraus formula for the entanglement fidelity are the two standard tools for computing fidelities of states and channels, and they are reused across the remaining chapters.

Formalizing it. All results here are proved in the book, so the remaining work is to formalize the known proofs. The platform already has gentle measurement statements with the weaker constant $\sqrt{8\varepsilon}$ (one of them proved), and Uhlmann's theorem in root-fidelity form with a supremum (proved). The constant $2\sqrt\varepsilon$, the ensemble version, the attainment of the maximum in Uhlmann's theorem and the Kraus formula for $F_e$ are not yet machine-checked anywhere on the platform. The relation $1-\sqrt F\le\frac12\|\rho-\sigma\|_1\le\sqrt{1-F}$ (Theorem 9.3.1) and the fact that a measurement achieves the fidelity (Theorem 9.2.2) are open goals of other missions and are not posed again here.

Difficulty

The step that does not go through directly is the passage from one state to an ensemble. Applying Lemma 9.4.2 to each $\rho_x$ separately needs a lower bound on each $\operatorname{Tr}\{\Lambda\rho_x\}$, and the hypothesis bounds only the average. The individual bounds can be poor for some $x$, so the per-state lemma cannot be applied with a fixed $\varepsilon$. What is needed is a bound on each $\|\rho_x-\sqrt\Lambda\rho_x\sqrt\Lambda\|_1$ in terms of $1-\operatorname{Tr}\{\Lambda\rho_x\}$ that remains useful after averaging, which is a matter of the shape of the per-state inequality, not of its constant.

For the single-state lemmas, the obstacle is the constant: the triangle-inequality argument that gives $\sqrt{8\varepsilon}$ loses a factor $\sqrt2$, and reaching $2\sqrt\varepsilon$ requires a sharper operator inequality. In Lean, the matrix square root, the trace norm and Hilbert–Schmidt Cauchy–Schwarz inequalities all have to be handled through the continuous functional calculus, where Mathlib's library for trace-class estimates is thin. Uhlmann's theorem needs the polar decomposition and the characterization of the trace norm as a maximum over unitaries.

Formalization scope

Operators are complex matrices Matrix n n ℂ over a finite index type; a vector on $R\otimes A$ is a function on r × a (reference first, Mathlib's Kronecker convention). The trace norm is the published WildeQIT.traceNorm, unhalved; square roots are CFC.sqrt. The condition $0\le\Lambda\le I$ is positive semidefiniteness of $\Lambda$ and of $I-\Lambda$. Traces that are real for positive operators, such as $\operatorname{Tr}\{\Lambda\rho\}$, are taken as real parts of complex traces. Distributions are the published WildeQIT.FinDist, and channels the published Kraus-form WildeQIT.QChannel. The maximum in Uhlmann's theorem is stated as IsGreatest: it is attained, not only a supremum. Lemma 9.4.1 assumes $\operatorname{Tr}\{\Lambda\rho\}\ne0$, which excludes only the case where the book's $\rho'$ is undefined.

No statement is trivialized by a degenerate case: every hypothesis is satisfied by $\rho=\Lambda=I$ on a one-dimensional space with $\varepsilon=0$, and the constant $2\sqrt\varepsilon$ is that of the book, not the weaker $\sqrt{8\varepsilon}$.

A complete development needs the operator inequality $\sqrt\Lambda\ge\Lambda$ for $0\le\Lambda\le I$, the Hilbert–Schmidt Cauchy–Schwarz inequality, the triangle inequality and convexity of the trace norm, and concavity of the square root. These lemmas are reusable well beyond this mission. Contributions of any of them, or of the polar-decomposition and trace-norm duality results behind Uhlmann's theorem, are welcome.

Selected references

• M. M. Wilde, From Classical to Quantum Shannon Theory, arXiv:1106.1445v8, 2019, §§9.2–9.5. https://arxiv.org/abs/1106.1445v8
• A. Winter, Coding theorem and strong converse for quantum channels, IEEE Trans. Inf. Theory 45(7), 1999. https://doi.org/10.1109/18.796385
• A. Uhlmann, The "transition probability" in the state space of a ∗-algebra, Rep. Math. Phys. 9(2), 1976. https://doi.org/10.1016/0034-4877(76)90060-4
• C. A. Fuchs, J. van de Graaf, Cryptographic distinguishability measures for quantum-mechanical states, IEEE Trans. Inf. Theory 45(4), 1999. https://doi.org/10.1109/18.761271

Motivation

A spectral function is an extended-real-valued function $g$ on the space $\mathbf S^n$ of real symmetric $n\times n$ matrices that is orthogonally invariant: $g(U^\top XU)=g(X)$ for every orthogonal $U$. Eigenvalue optimization, semidefinite programming, matrix completion and low-rank regularization all lead to such functions: the largest eigenvalue, the nuclear norm of a symmetric matrix, the indicator of the positive semidefinite cone, $-\log\det$. Every spectral function factors as $g=\theta\circ\lambda$, where $\lambda(X)$ is the vector of eigenvalues in nonincreasing order and $\theta:\mathbb R^n\to[-\infty,\infty]$ is symmetric, i.e. invariant under permutations of coordinates (Lewis, Convex analysis on the Hermitian matrices).

A long line of work shows that properties of $\theta$ transfer to $g$: convexity and the subdifferential (Lewis 1996), differentiability (Lewis 1996), twice differentiability (Lewis–Sendov 2001), and second-order expansions of eigenvalues (Torki 2001). Second-order optimality conditions for nonsmooth problems need more: the second subderivative of $g$ and the regularity property, parabolic regularity, that makes it computable and makes $g$ twice epi-differentiable (Mohammadi–Mordukhovich–Sarabi, Parabolic regularity in geometric variational analysis, Trans. Amer. Math. Soc. 374, 2021). A. Mohammadi and E. Sarabi, Parabolic Regularity of Spectral Functions (arXiv:2301.04240v3, 2024; Mathematics of Operations Research, 2025) prove that parabolic regularity also passes between $\theta$ and $g$.

Setting

$\mathbf S^n$ carries $\langle X,Y\rangle=\operatorname{tr}(XY)$. $\lambda(X)=(\lambda_1(X)\ge\dots\ge\lambda_n(X))$; $O^n(X)$ is the set of orthogonal $U$ with $X=U\operatorname{Diag}(\lambda(X))U^\top$. If $\mu_1>\dots>\mu_r$ are the distinct eigenvalues of $X$, the blocks are $\alpha_m=\{i\mid\lambda_i(X)=\mu_m\}$, and $U_{\alpha_m}$ is the matrix of the columns of $U$ indexed by $\alpha_m$. The eigenvalue map has one-sided derivatives $\lambda'(X;H)$ and $\lambda''(X;H,W)$ along parabolic curves $X+tH+\tfrac12t^2W$.

For $f:\mathbf X\to[-\infty,\infty]$ on a finite-dimensional Hilbert space, finite at $\bar x$:

• the subderivative $\mathrm df(\bar x)(w)=\liminf_{t\downarrow0,w'\to w}(f(\bar x+tw')-f(\bar x))/t$;
• the second subderivative $\mathrm d^2f(\bar x,\bar v)(w)=\liminf_{t\downarrow0,w'\to w}\Delta^2_tf(\bar x,\bar v)(w')$, with $\Delta^2_tf(\bar x,\bar v)(w)=(f(\bar x+tw)-f(\bar x)-t\langle\bar v,w\rangle)/\tfrac12t^2$;
• the parabolic subderivative $\mathrm d^2f(\bar x)(w\,|\,z)$, the same kind of liminf along $\bar x+tw+\tfrac12t^2z'$;
• the critical cone $K_f(\bar x,\bar v)=\{w\mid\mathrm df(\bar x)(w)=\langle\bar v,w\rangle\}$.

A convex $f$ is parabolically regular at $\bar x$ for $\bar v\in\partial f(\bar x)$ if every finite value $\mathrm d^2f(\bar x,\bar v)(w)$ is attained along some $t_k\downarrow0$, $w_k\to w$ with $\|w_k-w\|=O(t_k)$ (Definition 5.1). Parabolic epi-differentiability asks that the parabolic subderivative be a full limit along every $t_k\downarrow0$.

Formalization targets

Goal: Theorem 5.8

Let $g=\theta\circ\lambda$ be locally Lipschitz continuous relative to its domain, lower semicontinuous and convex. (a) If $Y\in\partial g(X)$ and $\theta$ is parabolically regular at $\lambda(X)$ for $\lambda(Y)$ and parabolically epi-differentiable at $\lambda(X)$, then $g$ is parabolically regular at $X$ for $Y$, and for every $H\in K_g(X,Y)$ and $U\in O^n(X)\cap O^n(Y)$

$$\mathrm d^2g(X,Y)(H)=\mathrm d^2\theta(\lambda(X),\lambda(Y))(\lambda'(X;H))+2\sum_{m=1}^r\big\langle\Lambda(Y)_{\alpha_m\alpha_m},U_{\alpha_m}^\top H(\mu_mI-X)^\dagger HU_{\alpha_m}\big\rangle .$$

(b) If $g$ is parabolically epi-differentiable and parabolically regular at $X$, then $\theta$ is parabolically regular at $\lambda(X)$.

Milestones

• Fan's inequality (2.3) (already proved on the platform) and the distance identities (1.3), (3.5).
• Eigenvalue expansions: Propositions 2.1, 2.2 with (2.13), and Corollary 2.3.
• First order: the subdifferential (Proposition 3.4), the subderivative chain rule (Theorem 3.5), and tangent cones of spectral sets (Corollary 3.6).
• Parabolic: second-order tangent sets (Theorem 4.3), domains of parabolic subderivatives (Proposition 4.6), the parabolic chain rule (Theorem 4.7), and $\mathbf P^n_{X,H}$-symmetry (Proposition 4.8).
• §5: the characterization of parabolic regularity (Proposition 5.2, corrected), the lower estimate (5.1) (Proposition 5.3), the critical cone (Proposition 5.4), the attaining matrix $\widehat W$ (Proposition 5.6), and the domain of $\mathrm d^2g(X,Y)$ (Proposition 5.7).

Significance

Theorem 5.8(a) gives an explicit second subderivative for every convex spectral function whose symmetric part is parabolically regular, for example every polyhedral $\theta$ (Corollary 5.9 of the paper). This yields second-order necessary and sufficient optimality conditions for $\min\varphi(X)+g(X)$ and, through the results of Mohammadi–Sarabi (SIAM J. Optim. 30, 2020), twice epi-differentiability of $g$ and proto-differentiability of $\partial g$. The curvature term $2\sum_m\langle\cdot,\cdot\rangle$ recovers the known formula $-2\langle Y,HX^\dagger H\rangle$ for the positive semidefinite cone as a special case.

The theorem is proved in the paper; none of it is formalized. Formalizing it adds a library of second-order variational analysis on a general space (parabolic subderivatives, second subderivatives, parabolic regularity) and second-order perturbation theory of eigenvalues, both absent from Mathlib. Proposition 5.2 as printed is false (see Difficulty), so the mission also records the corrected statement.

Difficulty

The eigenvalue map is not twice differentiable where eigenvalues coalesce, so the standard composite chain rules of Mohammadi–Sarabi (2020), which need a twice differentiable inner map, do not apply. The paper replaces differentiability with Torki's parabolic expansion (Proposition 2.2), whose second-order term depends on a choice of eigenvector bases $Q_m$ inside each eigenvalue block. The upper bound of Theorem 5.8(a) needs a direction $\widehat W$ attaining the infimum of the parabolic subderivative. Building it (Proposition 5.6) requires a minimizer sorted inside each block $\beta^m_j$ and a choice of $Q_m$ adapted to $Y$ (5.22).

A natural first idea is to prove (5.20), $\mathrm d^2g(X,Y)(H)=\inf_W\{\mathrm d^2g(X)(H|W)-\langle Y,W\rangle\}$, and conclude by Proposition 5.2. This does not work: the implication "(b) ⇒ (a)" of Proposition 5.2 is false. The convex function $f(x,y)=x^2+x^4/y$ ($y>0$), $f(0,0)=0$ satisfies (b) at $\bar x=0$, $\bar v=0$, but at $w=(1,0)$ the infimum is not attained and $f$ is not parabolically regular. Attainment at $\widehat W$ is what is needed.

Formalization scope

• $\mathbf S^n$ is the published SunNLSDP.Equiv.SymMat (Fin n), with entrywise inner product equal to $\operatorname{tr}(XY)$; $\lambda$ is the published ModernConvex.Spectral.eigVec; $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Indices are 0-based.
• Functions take values in EReal. Wherever the paper assumes $f(\bar x)$ finite, the definitions subtract the real $f(\bar x)$, and $\partial f(\bar x)=\emptyset$ when $f(\bar x)$ is infinite.
• Convexity is that of the epigraph, with no properness bundled.
• $\lambda'$ and $\lambda''$ are one-sided limits, whose existence is a milestone (Corollary 2.3).
• $Z^\dagger$ is the Moore–Penrose inverse (functional calculus).
• The curvature sum is written per index, $\sum_i\lambda_i(Y)(U^\top H(\lambda_i(X)I-X)^\dagger HU)_{ii}$, a regrouping of the block sum.
• The formula holds for every $U\in O^n(X)\cap O^n(Y)$.

Two trivializations are ruled out by the definitions. Parabolic regularity keeps both the recovery-sequence requirement and the bound $\|w_k-w\|=O(t_k)$. All liminfs range over $\mathbf S^n$, not over all matrices.

The development needs variational analysis on a general inner-product space (reusable for any composite or matrix problem) and second-order eigenvalue perturbation theory. Proofs of any milestone, of the cited results (Propositions 2.1, 2.2, 3.4, 4.6), and of the corrected Proposition 5.2 are welcome.

Selected references

• A. Mohammadi, E. Sarabi, Parabolic Regularity of Spectral Functions, arXiv:2301.04240v3, 2024; Mathematics of Operations Research, 2025. https://arxiv.org/abs/2301.04240
• A. S. Lewis, Convex analysis on the Hermitian matrices, SIAM J. Optim. 6:164–177 (1996). https://doi.org/10.1137/0806009
• A. Mohammadi, B. S. Mordukhovich, M. E. Sarabi, Parabolic regularity in geometric variational analysis, Trans. Amer. Math. Soc. 374:1711–1763 (2021).
• A. S. Lewis, H. S. Sendov, Twice differentiable spectral functions, SIAM J. Matrix Anal. Appl. 23:368–386 (2001). https://doi.org/10.1137/S089547980036838X
• M. Torki, Second-order directional derivatives of all eigenvalues of a symmetric matrix, Nonlinear Anal. 46:1133–1150 (2001).
• A. Mohammadi, E. Sarabi, Twice epi-differentiability of extended-real-valued functions with applications in composite optimization, SIAM J. Optim. 30:2379–2409 (2020).
• R. T. Rockafellar, R. J-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3