Linear algebra

Completed

Operations Research Probability·Captain: mikedeng1

When Is Society Susceptible to Manipulation?: Under Any Principal Interference, Beliefs in a Mixed DeGroot–Bayesian Network Converge Almost Surely to (I − W)⁻¹(BU∞ ⊙ θ)Research Paper

Motivation

Misinformation campaigns target specific people in a social network and rely on the network to spread what they plant. Whether such a campaign can succeed depends on how people combine what they see themselves with what their neighbours believe. Mostagir, Ozdaglar and Siderius (SSRN 3474643; Management Science, 2022, doi:10.1287/mnsc.2021.4265) model a network in which a strategic principal injects slanted news into chosen agents. Some agents are Bayesian and know the truth; the rest are DeGroot agents who average their own news-based opinion with their neighbours' beliefs.

The paper asks when society as a whole can be manipulated. Every later result in it — which agents the principal targets, which networks resist manipulation, how the answer depends on the network's density — is a statement about the agents' long-run beliefs. Its Theorem 2 supplies those beliefs in closed form, and that closed form is the subject of this mission.

DeGroot updating (DeGroot, 1974) and its combination with personal Bayesian updates (Jadbabaie, Molavi, Sandroni and Tahbaz-Salehi, 2012) are standard models of non-Bayesian social learning. Stubborn agents in averaging dynamics were studied by Acemoglu, Como, Fagnani and Ozdaglar (2013). The present model adds a principal who corrupts the signals of targeted agents.

Setting

There are $n$ agents and a binary state $y\in\{S,R\}$ with prior $q=\mathbb P(y=S)\in(0,1)$ . Agent $i$ has a signal quality $p_i\in[1/2,1)$ . At each time $\tau=1,2,\dots$ agent $i$ receives a signal $s_{i,\tau}\in\{S,R\}$ :

Organic news equals the state with probability $p_i$ : $\mathbb P(s_{i,\tau}=S\mid y=S)=\mathbb P(s_{i,\tau}=R\mid y=R)=p_i$ .
The principal fixes an influence state $\hat y$ and an influence strategy $\mathbf x=(x_1,\dots,x_n)\in\{0,1\}^n$ . A targeted agent ( $x_i=1$ ) receives the principal's message $\hat y$ with probability $\lambda^*/(\lambda+\lambda^*)$ and organic news with probability $\lambda/(\lambda+\lambda^*)$ . Here $\lambda>0$ and $\lambda^*>0$ are the intensities of the organic and the principal's news. An untargeted agent receives only organic news.

Agent $i$ 's signals are independent over time. Its personal experience is the posterior it would compute taking every signal at face value. With $z^S_{i,t},z^R_{i,t}$ the numbers of $S$ and $R$ signals among $s_{i,1},\dots,s_{i,t}$ ,

\mathrm{BU}_i(S\mid h_{i,t})=\frac{p_i^{z^S_{i,t}}(1-p_i)^{z^R_{i,t}}q}{p_i^{z^S_{i,t}}(1-p_i)^{z^R_{i,t}}q+p_i^{z^R_{i,t}}(1-p_i)^{z^S_{i,t}}(1-q)},

and $\mathrm{BU}_i(R\mid h_{i,t})=1-\mathrm{BU}_i(S\mid h_{i,t})$ .

A set $B$ of agents is Bayesian. A Bayesian agent knows $y$ and always believes it. Each DeGroot agent $i\notin B$ has weights $\theta_i\ge0$ and $\alpha_{ij}\ge0$ with $\theta_i+\sum_j\alpha_{ij}=1$ . For a state $y'$ , its belief $\pi_{i,t}(y'\mid y)$ follows the DeGroot update

\pi_{i,t+1}=\theta_i\,\mathrm{BU}_i(y'\mid h_{i,t+1})+\sum_{j=1}^n\alpha_{ij}\,\pi_{j,t}.

The influence matrix $\mathbf W$ has zero rows for Bayesian agents and row $(\alpha_{ij})_j$ for DeGroot agents. The vector $\boldsymbol\theta=(\mathbf 1_B,\theta_{m+1},\dots,\theta_n)$ has entry $1$ on Bayesians. The unweighted graph $G^*$ has a link $i\to j$ when $i$ listens to $j$ ; for a DeGroot agent this means $\alpha_{ij}>0$ .

Assumption 1 (pp. 10–11):

(i) $p_i<(\lambda^*+\lambda)/(2\lambda)$ for every agent;
(ii) $G^*$ is strongly connected;
(iii) a DeGroot agent has $\theta_i>0$ exactly when $p_i>1/2$ ;
(iv) some agent has $p_i>1/2$ .

Formalization targets

Goal: Theorem 2 (p. 11)

Under Assumption 1, for every principal action $\mathbf x^*$ , each DeGroot agent's personal experience converges almost surely to a constant $\mathrm{BU}_i(h_{i,\infty}(\mathbf x^*))(y'\mid y)$ , and

\boldsymbol\pi_t(y'\mid y)\xrightarrow{\text{a.s.}}(\mathbf I-\mathbf W)^{-1}\big(\mathrm{BU}(\mathbf h_\infty(\mathbf x^*))(y'\mid y)\odot\boldsymbol\theta\big),

where the Bayesian entries of the vector $\mathrm{BU}(\mathbf h_\infty(\mathbf x^*))$ are the correct belief. The goal does not fix the constants: the paper computes them only later (display (2), p. 12).

Milestones

Lemma 3 (p. 45): the spectral radius of $\mathbf W$ is strictly less than $1$ .
Proof of Theorem 2 (p. 47): $\mathbf I-\mathbf W$ and its DeGroot block $\mathbf I-\mathbf A_{DD}$ are invertible.
§3.2 (p. 11): $\mathrm{BU}_i(h_{i,t})$ converges almost surely to a constant.
Proof of Theorem 2 (p. 47): if $\mathbf u_t\to\mathbf u_\infty$ and $\boldsymbol\pi_{t+1}=\mathbf u_{t+1}+\mathbf W\boldsymbol\pi_t$ , then $\boldsymbol\pi_t\to\boldsymbol\pi_\infty=(\mathbf I-\mathbf W)^{-1}\mathbf u_\infty$ , the solution of $\boldsymbol\pi_\infty=\mathbf u_\infty+\mathbf W\boldsymbol\pi_\infty$ .

Significance

Theorem 2 reduces the paper's manipulation question to linear algebra. A DeGroot agent ends up believing the wrong state exactly when the corresponding entry of $(\mathbf I-\mathbf W)^{-1}(\mathrm{BU}_\infty\odot\boldsymbol\theta)$ crosses a threshold. The principal's targeting problem then becomes a combinatorial problem over $\mathbf x^*$ in which the network enters only through $(\mathbf I-\mathbf W)^{-1}$ . The paper's DeGroot centrality (Proposition 2) and its results on dense and sparse networks all start from this formula.

On formalization: the paper proves Theorem 2, but no machine-checked version exists. The mission's statements also record two places where the written argument needs repair. The text attributes the almost-sure convergence of $\mathrm{BU}_i$ to the martingale convergence theorem, but $\mathrm{BU}_i$ is a face-value posterior and not a martingale under the corrupted signal law. The proof's step from small increments of $\boldsymbol\pi_t$ to convergence of $\boldsymbol\pi_t$ is also not valid as written. Both claims are true under Assumption 1, and a complete development supplies correct arguments. The supporting results — spectral radius below one for a substochastic matrix with leakage reachable from every row, and convergence of linear recursions with convergent input — are reusable beyond this paper.

Difficulty

Two steps resist the obvious arguments.

First, $\mathrm{BU}_i(S\mid h_{i,t})$ is a function of the drift $z^S_{i,t}-z^R_{i,t}$ of a random walk. Its limit exists only if the walk is transient or $p_i=1/2$ . For a targeted agent the walk's step law mixes the principal's message with organic news. For one boundary value of $p_i$ the step has mean zero, the walk is recurrent and $\mathrm{BU}_i$ oscillates forever. Assumption 1(i) excludes exactly that value. A proof must use it; a martingale argument does not apply.

Second, $\mathbf W$ is substochastic but not strictly so: a DeGroot row sums to $1-\theta_i$ , which equals $1$ whenever $p_i=1/2$ . A row-sum bound alone gives $\rho(\mathbf W)\le1$ , not $<1$ . Strict inequality needs every DeGroot agent to reach, in the weighted graph, an agent that leaks weight — a Bayesian or a DeGroot agent with $\theta_i>0$ . This uses the interaction of Assumption 1 (ii), (iii) and (iv), with Bayesian agents' outgoing links playing no role in $\mathbf W$ .

Formalization scope

Agents are Fin n and the Bayesian set is a Finset. Time is discrete, and the history at time $t$ is the signals at times $1,\dots,t$ . The state space is a two-element inductive type. The signals are random variables on a probability space $(\Omega,P)$ . Each agent's sequence is independent over time with the law above; signals of different agents may be dependent. This is deliberate: in the paper all targeted agents receive the same principal stream, so cross-agent independence would exclude the paper's own model. The principal's action is pure ( $\mathbf x^*\in\{0,1\}^n$ ), as §3.2 allows without loss of generality. The DeGroot initial belief can be any value in $[0,1]$ , and the conclusion holds for every such initial belief on one almost-sure event. "Spectral radius" is Mathlib's spectralRadius ℂ of the complexified matrix. $(\mathbf I-\mathbf W)^{-1}$ is Mathlib's matrix inverse; no invertibility hypothesis is added, because Assumption 1 implies it. In the graph $G^*$ , a DeGroot agent's links are exactly its positive weights; Bayesian agents' links are free.

The personal experience is the explicit face-value posterior of the given signal process, and the conclusion of the goal includes its almost-sure convergence to the constants used in the limit. The goal therefore cannot be met by an abstract learning rule or a free limit vector.

A complete development needs:

the strong law of large numbers (available in Mathlib) applied to the signal counts;
a Perron–Frobenius-type spectral bound for substochastic matrices on a strongly connected graph;
convergence of $\boldsymbol\pi_{t+1}=\mathbf u_{t+1}+\mathbf W\boldsymbol\pi_t$ when $\rho(\mathbf W)<1$ .

Contributions of any of these, as standalone lemmas, are welcome.

Selected references

M. Mostagir, A. Ozdaglar, J. Siderius, When Is Society Susceptible to Manipulation?, SSRN preprint 3474643 (version of 2020-06-08); Management Science 68(10), 2022. https://ssrn.com/abstract=3474643, https://doi.org/10.1287/mnsc.2021.4265
M. H. DeGroot, Reaching a Consensus, Journal of the American Statistical Association 69(345), 1974. https://doi.org/10.1080/01621459.1974.10480137
A. Jadbabaie, P. Molavi, A. Sandroni, A. Tahbaz-Salehi, Non-Bayesian Social Learning, Games and Economic Behavior 76(1), 2012. https://doi.org/10.1016/j.geb.2012.06.001
D. Acemoglu, G. Como, F. Fagnani, A. Ozdaglar, Opinion Fluctuations and Disagreement in Social Networks, Mathematics of Operations Research 38(1), 2013. https://doi.org/10.1287/moor.1120.0570

6 thms2 active usersReviewed

Quantum Information Theoretical Computer Science·Captain: mikedeng1

Quantum Singular Value Transformation and Beyond: Exponential Improvements for Quantum Matrix Arithmetics: Singular Value Transformation by Real Polynomials via Alternating Phase ModulationResearch Paper

Motivation

Many quantum algorithms act on a matrix $A$ that is not itself unitary: a Hamiltonian to be simulated, a linear system to be inverted, a projector to be amplified. The standard way to hand such a matrix to a quantum computer is to embed it as a block of a unitary $U$ , so that $A=\widetilde\Pi U\Pi$ for two orthogonal projectors $\Pi,\widetilde\Pi$ . The question is then which functions $f(A)$ can be produced from a few uses of $U$ and $U^\dagger$ .

Gilyén, Su, Low and Wiebe (arXiv:1806.01838, STOC 2019) answered it for polynomials: interleaving $U$ and $U^\dagger$ with phase rotations about $\Pi$ and $\widetilde\Pi$ applies a polynomial to every singular value of $A$ . This quantum singular value transformation (QSVT) recovers Hamiltonian simulation, amplitude amplification, fixed-point search, quantum walks and matrix inversion as instances of one identity, and is now the common language of these algorithms (see the survey of Martyn, Rossi, Tan and Chuang, PRX Quantum 2021).

Timeline.

2016: Low, Yoder and Chuang characterize the single-qubit sequences $e^{i\varphi_0\sigma_z}\prod_j W(x)e^{i\varphi_j\sigma_z}$ , which they call quantum signal processing (QSP) (PRX 2016).
2016–2017: Low and Chuang lift QSP to Hermitian blocks by qubitization (Quantum 2019; PRL 2017).
2018: this paper replaces eigenvalues by singular values, so that arbitrary (even rectangular) blocks are allowed, and removes the earlier constraint $P_\Re(0)=0$ for even degree.

Setting

Let $\mathcal H_U$ be a finite-dimensional complex Hilbert space, $U$ a unitary on it, and $\Pi,\widetilde\Pi$ orthogonal projectors. The projected unitary is $A=\widetilde\Pi U\Pi$ . Put $d=\operatorname{rank}\Pi$ , $\tilde d=\operatorname{rank}\widetilde\Pi$ , $d_{\min}=\min(d,\tilde d)$ . A singular value decomposition of $A$ consists of orthonormal bases $(\psi_i)_{i\le d}$ of $\mathrm{img}\,\Pi$ and $(\tilde\psi_i)_{i\le\tilde d}$ of $\mathrm{img}\,\widetilde\Pi$ and numbers $\varsigma_1\ge\dots\ge\varsigma_{d_{\min}}\ge0$ with

A=\sum_{i=1}^{d_{\min}}\varsigma_i\,|\tilde\psi_i\rangle\langle\psi_i| .

For $f:\mathbb R\to\mathbb C$ , the singular value transformation is $f^{(SV)}(A)=\sum_{i\le d_{\min}}f(\varsigma_i)|\tilde\psi_i\rangle\langle\psi_i|$ when $f$ is odd and $f^{(SV)}(A)=\sum_{i\le d}f(\varsigma_i)|\psi_i\rangle\langle\psi_i|$ when $f$ is even, with $\varsigma_i:=0$ for $i>d_{\min}$ .

The phase operator of a projector is $e^{i\varphi(2\Pi-I)}=e^{i\varphi}\Pi+e^{-i\varphi}(I-\Pi)$ . For $\Phi=(\varphi_1,\dots,\varphi_n)\in\mathbb R^n$ , the alternating phase modulation sequence $U_\Phi$ is the product, from $j=1$ on the left to $j=n$ on the right, of $e^{i\varphi_j(2\widetilde\Pi-I)}U$ when $n-j$ is even and of $e^{i\varphi_j(2\Pi-I)}U^\dagger$ when $n-j$ is odd. On the single-qubit side, $R(x)=\begin{pmatrix}x&\sqrt{1-x^2}\\ \sqrt{1-x^2}&-x\end{pmatrix}$ for $x\in[-1,1]$ , and $\Phi$ is said to realize $P\in\mathbb C[x]$ if $P(x)$ is the top-left entry of $\prod_{j=1}^n e^{i\varphi_j\sigma_z}R(x)$ for every $x\in[-1,1]$ .

In Lean these are ProjUnitarySVD U Proj Projt (the decomposition data), svtOdd/svtEven, phaseRefl, altPhaseSeq, reflR and qspRefl, in the namespace QSVT19.Main.

Formalization targets

Goal: Corollary 18 (singular value transformation by real polynomials)

Let $n\ge1$ and let $P_\Re\in\mathbb R[x]$ have degree $n$ , parity $n \bmod 2$ , and $|P_\Re(x)|\le1$ on $[-1,1]$ . Then there is $\Phi\in\mathbb R^n$ such that for every singular value decomposition of $\widetilde\Pi U\Pi$

P_\Re^{(SV)}(\widetilde\Pi U\Pi)=\bigl(\langle+|\otimes\Pi'\bigr)\bigl(|0\rangle\langle0|\otimes U_\Phi+|1\rangle\langle1|\otimes U_{-\Phi}\bigr)\bigl(|+\rangle\otimes\Pi\bigr),

with $\Pi'=\widetilde\Pi$ for odd $n$ and $\Pi'=\Pi$ for even $n$ . The only constraints on $P_\Re$ are those that are necessary; no degree-dependent constant appears.

Milestones

Lemma 6, Theorem 5, Theorem 4 (first claim): sum-of-squares factorization and the characterization of which polynomials, and which real parts, arise from QSP.
Corollary 8: every $P$ meeting four explicit conditions is realized by some $\Phi\in\mathbb R^d$ in the reflection form; Corollary 10: every $P_\Re$ as in the goal is $\Re[P]$ for such a $P$ .
Definition 11 (existence of the decomposition), Table 2 (orthonormality of the spanning vectors of Definition 12), Lemma 14 (the block decomposition of $U$ into one- and two-dimensional pieces).
Theorem 17: if $\Phi$ realizes $P$ , then $P^{(SV)}(\widetilde\Pi U\Pi)=\widetilde\Pi U_\Phi\Pi$ for odd $n$ and $\Pi U_\Phi\Pi$ for even $n$ .
Lemma 9 (optional): explicit phases realizing the Chebyshev polynomial $T_d$ .

Significance

The result. Corollary 18 says that every real polynomial of degree $n$ , of definite parity and bounded by $1$ on $[-1,1]$ , can be applied to the singular values of $\widetilde\Pi U\Pi$ with $n$ uses of $U$ and $U^\dagger$ and one ancilla qubit. Every application in §3.4–§5 of the paper (fixed-point amplitude amplification, singular vector transformation, the pseudoinverse, Hamiltonian simulation, Gibbs sampling) is this corollary applied to a suitable approximating polynomial, so a formal proof makes all of them conditional only on polynomial approximation bounds.

Formalizing it. The result is proved in the paper; none of the statements of this mission has a machine-checked proof on the platform. A formal development would provide reusable infrastructure absent from Mathlib: singular value decompositions over sub-spaces, the two-dimensional invariant-subspace decomposition of a projected unitary (a quantitative form of Jordan's lemma), and the polynomial characterization of single-qubit QSP. Theorem 3 of the paper, the $W(x)$ form of the QSP characterization, is already posed on the platform as QAlgorithms.Childs.qsp_characterization; Corollary 8 depends on it.

Difficulty

The obvious argument for Theorem 17 is "restrict $U_\Phi$ to each two-dimensional subspace and read off the QSP product". Making that rigorous means proving that the subspaces of Definition 12 are pairwise orthogonal, invariant under every factor of $U_\Phi$ , and that $U$ acts on each pair of bases by exactly the reflection $R(\varsigma_i)$ , including the degenerate blocks with $\varsigma_i\in\{0,1\}$ , the one-dimensional blocks $\mathcal H_i^R,\mathcal H_i^L$ where $U_\Phi$ contributes a phase $e^{\pm i\varphi_0}$ , and the complement $\mathcal H_\perp$ . The polynomial side is harder still: Lemma 6 factors a nonnegative even polynomial through its multiset of complex roots, grouping roots in $(0,1)$ , in $[1,\infty)$ , on the imaginary axis and in the open quadrant, while tracking degree and parity. Neither step reduces to a library lemma, and an argument that works only for Hermitian $A$ , or only when $\Pi=\widetilde\Pi$ , proves a different theorem.

Formalization scope

$\mathcal H_U$ is ι → ℂ for a Fintype ι with the inner product star v ⬝ᵥ w; operators are Matrix ι ι ℂ; "unitary" is U ∈ Matrix.unitaryGroup ι ℂ; "orthogonal projector" is IsStarProjection. The projectors are named Proj, Projt because Π is Lean notation. Indices are 0-based.
A singular value decomposition is the structure ProjUnitarySVD U Proj Projt of data: orthonormal families with $\Pi=\sum_i|\psi_i\rangle\langle\psi_i|$ , $\widetilde\Pi=\sum_i|\tilde\psi_i\rangle\langle\tilde\psi_i|$ , nonnegative non-increasing $\varsigma$ , and (17). The goal is posed for every such decomposition, with $\Phi$ chosen first; the Definition 11 milestone shows that one exists. $\varsigma_i\le1$ is a consequence and is not assumed.
$f^{(SV)}$ is the sum over the decomposition (Definition 16), never the right-hand side of (32) or (33); a formalization that defines it by an operator expression trivializes the goal.
$e^{i\varphi(2\Pi-I)}$ is written $e^{i\varphi}\Pi+e^{-i\varphi}(I-\Pi)$ , equal to the matrix exponential for an idempotent $\Pi$ . The ancilla of (33) is the first tensor factor.
$e^{i\varphi\sigma_z}$ and the parity predicate are the published definitions of QAlgorithms_Defs_Hamiltonian. "deg ≤ k − 1" is degree < k and "parity $k-1$ " is parity $k+1$ , avoiding natural-number subtraction.
Printed slips that affect statements:
- Corollary 10 omits $\Re[P]=P_\Re$ ; it is restored, as used in the proof of Corollary 18.
- Corollary 8 and Corollary 18 are false for degree $0$ (a constant $e^{i\alpha}$ , respectively a constant $c\neq1$ ); both are posed with $d\ge1$ , $n\ge1$ .
- Theorem 17's " $P$ and $\Phi$ as in Corollary 8" is read as (14), the only property its proof uses.
- Lemma 14's (25)–(28) index the $\mathcal H^L$ blocks by $[d]\setminus[r]$ ; this is read as $[\tilde d]\setminus[r]$ , as in (24).
Contributions welcome: proofs of any milestone, general lemmas on SVDs of compressions $\widetilde\Pi U\Pi$ , and a proof of the platform's open QSP characterization.

Selected references

A. Gilyén, Y. Su, G. H. Low, N. Wiebe, Quantum singular value transformation and beyond: exponential improvements for quantum matrix arithmetics, arXiv:1806.01838v1, 2018; STOC 2019. https://arxiv.org/abs/1806.01838
G. H. Low, T. J. Yoder, I. L. Chuang, Methodology of resonant equiangular composite quantum gates, Physical Review X 6, 041067, 2016. https://doi.org/10.1103/PhysRevX.6.041067
G. H. Low, I. L. Chuang, Optimal Hamiltonian simulation by quantum signal processing, Physical Review Letters 118, 010501, 2017. https://doi.org/10.1103/PhysRevLett.118.010501
G. H. Low, I. L. Chuang, Hamiltonian simulation by qubitization, Quantum 3, 163, 2019. https://doi.org/10.22331/q-2019-07-12-163
J. M. Martyn, Z. M. Rossi, A. K. Tan, I. L. Chuang, Grand unification of quantum algorithms, PRX Quantum 2, 040203, 2021. https://doi.org/10.1103/PRXQuantum.2.040203

13 thms2 active usersReviewed

Completed

Machine Learning Statistics·Captain: mikedeng1

A Robust Spectral Clustering Algorithm for Sub-Gaussian Mixture Models with Outliers 2: Spectral Rounding Without Outliers Gives Σ|S_k|/n_k ≤ 64(2+ε)‖X⁰ − X̂‖₁/n²minResearch Paper

Motivation

Spectral clustering recovers group labels from a similarity matrix: compute its leading eigenvectors, embed each point as a row of the eigenvector matrix, and cluster the rows with k-means. It is a standard last step of convex-relaxation methods for clustering, which first estimate a clustering matrix $X$ (with $X_{ij} = 1$ when $i$ and $j$ belong to the same cluster) and then have to turn the estimate back into labels.

Srivastava, Sarkar and Hanasusanto (arXiv:1912.07546v3; Operations Research 71(1), 2023) estimate $X$ by a linear program on a thresholded Gaussian kernel and then round it this way (Algorithm 1, steps 3–4). Their Theorem 2 controls the error of the rounding step in terms of the $\ell_1$ error of the estimate. The argument follows Lei and Rinaldo (Ann. Statist. 43(1), 2015), who analysed spectral clustering for stochastic block models with a polynomial-time $(1+\epsilon)$ -approximate k-means step, combined with the Davis–Kahan theorem in the form of Yu, Wang and Samworth (Biometrika 102(2), 2015). The same pattern, "matrix estimation error ⇒ eigenvector error ⇒ misclassification count", recurs throughout the analysis of SDP and spectral methods for community detection and mixture models.

Setting

There are $n$ points and $r$ clusters. A fixed labelling $\varphi : [n] \to [r]$ gives clusters $C_k = \{i : \varphi(i) = k\}$ of sizes $n_k \ge 1$ , and $n_{\min} = \min_k n_k$ . The true clustering matrix is $X^0_{ij} = 1$ if $\varphi(i) = \varphi(j)$ and $0$ otherwise. Its scaled membership matrix is

U^0 = Z^0\,\mathrm{Diag}(1/\sqrt{n_1},\dots,1/\sqrt{n_r}),\qquad U^0_{ik} = \begin{cases} 1/\sqrt{n_k} & \varphi(i) = k,\\ 0 & \text{otherwise.}\end{cases}

The estimate $\hat X \in \mathbb R^{n\times n}$ is any symmetric matrix with entries in $[0,1]$ . Spectral rounding takes a matrix $\hat U \in \mathbb R^{n\times r}$ of orthonormal eigenvectors of $\hat X$ for its $r$ largest eigenvalues (ties broken arbitrarily), and runs k-means on the rows of $\hat U$ . A membership matrix $\Theta \in \mathbb M_{n,r}$ is a $\{0,1\}$ -matrix with exactly one $1$ per row; a pair $(\hat\Theta, \hat B)$ with $\hat B \in \mathbb R^{r\times r}$ is a $(1+\epsilon)$ -approximate k-means solution on the rows of $\hat U$ if

\|\hat U - \hat\Theta\hat B\|_F^2 \le (1+\epsilon)\min_{\Theta\in\mathbb M_{n,r},\, B\in\mathbb R^{r\times r}}\|\hat U - \Theta B\|_F^2 .

Let $O$ be an optimal rotation, an orthogonal $r\times r$ matrix minimising $\|\hat U - U^0O\|_F$ . With $v_i$ and $\bar v_i$ the rows of $U^0O$ and $\hat\Theta\hat B$ , the misclassified set of cluster $k$ is

\mathcal S_k = \Big\{ i \in C_k : \|\bar v_i - v_i\| \ge \tfrac{1}{2\sqrt{n_k}} \Big\}.

Norms: $\|A\|_1 = \sum_{i,j}|A_{ij}|$ (entrywise), $\|A\|_F^2 = \sum_{i,j}A_{ij}^2$ .

Formalization targets

Goal: Theorem 2, (15), without outliers

For every $\hat X$ , $\hat U$ , $(\hat\Theta,\hat B)$ and optimal $O$ as above and every $\epsilon > 0$ ,

\sum_{k\in[r]}\frac{|\mathcal S_k|}{n_k} \;\le\; 64(2+\epsilon)\,\frac{\|X^0 - \hat X\|_1}{n_{\min}^2}.

Milestones

Davis–Kahan (Theorem 3, case $s=1$ ): an eigengap $g$ of a symmetric $\Sigma$ below its top $r$ eigenvalues gives an orthogonal $\hat O$ with $\|U - \hat U\hat O\|_F \le 2^{3/2}\|\hat\Sigma - \Sigma\|_F/g$ .
Eigenstructure of $X^0$ : $U^0$ consists of top- $r$ eigenvectors of $X^0$ with eigenvalues $n_1,\dots,n_r$ , and $X^0$ vanishes on the orthogonal complement, so the eigengap is $n_{\min}$ .
(G.6)(iii): $\|A - B\|_F^2 \le \|A - B\|_1$ for matrices with entries in $[0,1]$ .
(G.6): $\|\hat U - U^0 O\|_F^2 \le 8\|\hat X - X^0\|_1/n_{\min}^2$ .
Lemma 5, (G.4) (Lei–Rinaldo): for $V = \Theta^*B^*$ and a $(1+\epsilon)$ -approximate k-means solution on any $\hat V$ , $\sum_k |\mathcal S_k|\delta_k^2 \le 4(4+2\epsilon)\|V - \hat V\|_F^2$ .
Centre separation: the rows of $B^* = \mathrm{Diag}(1/\sqrt{n_k})O$ satisfy $\|b^*_l - b^*_k\| = \sqrt{1/n_k + 1/n_l}$ .

Companion: permutation recovery

If $64(2+\epsilon)\|X^0 - \hat X\|_1/n_{\min}^2 \le 1$ , the k-means labels agree with $\varphi$ up to one permutation of $[r]$ on every point outside $\bigcup_k\mathcal S_k$ .

Significance

Inequality (15) separates the analysis of the algorithm into an estimation part (how close $\hat X$ is to $X^0$ in $\ell_1$ , Theorem 1 of the paper) and a purely deterministic rounding part. Any estimator of the clustering matrix with entries in $[0,1]$ — the Robust-LP, the SDP relaxations of Peng–Wei or Amini–Levina, a thresholded kernel — inherits a misclassification bound from its $\ell_1$ error through this one statement, with an explicit constant. The companion statement shows that the sets $\mathcal S_k$ really are the misclassified points.

The result is proved on paper; none of it is formalized. Mathlib has the spectral theorem for Hermitian matrices but no eigenspace perturbation bound of Davis–Kahan type, and the platform has no k-means approximation lemma for membership matrices. A machine-checked Davis–Kahan theorem in Frobenius norm and a machine-checked Lei–Rinaldo lemma are reusable well beyond this paper: they are the two standard ingredients of every spectral clustering guarantee for block models and mixtures.

Difficulty

The k-means part is elementary but bookkeeping-heavy: the comparison point in the $(1+\epsilon)$ bound must be a feasible k-means solution, which is why the true embedding $U^0O$ has to factor as a membership matrix times a centre matrix. The main obstacle is the Davis–Kahan step. The naive route through individual eigenvectors fails when eigenvalues of $\hat X$ or of $X^0$ are repeated (here $X^0$ has eigenvalue $n_k$ with multiplicity whenever cluster sizes coincide), and only the subspace is stable; the bound must be stated up to an orthogonal matrix and proved for the whole eigenspace, with no ordering or separation assumption on the eigenvalues of $\hat X$ .

Formalization scope

Points are Fin n, clusters Fin r, matrices Matrix ι κ ℝ; the norms are explicit sums, not Mathlib's matrix norm instances. The labelling $\varphi$ is fixed; membership matrices are encoded by assignments $a : [n]\to[r]$ , and " $\le (1+\epsilon)\min$ " by " $\le (1+\epsilon)\cdot$ the cost of every assignment and every centre matrix". "Top- $r$ eigenvectors" is variational: orthonormal columns, eigenvector equations, and every Rayleigh quotient on the orthogonal complement at most each selected eigenvalue. $n_{\min}$ is a finite minimum and requires $r \ge 1$ .

Departures from the printed text, each disclosed in the item concerned:

No outliers ( $m = 0$ ). The printed Theorem 2 allows outliers; it is false for $m \ge 1$ , because the outlier rows of $U^0$ are zero, so the true embedding is not k-means feasible and Lemma 5 does not apply. A counterexample with two clusters of size $M > 256$ , one isolated outlier and $\epsilon = 2$ violates (15).
No probability, no $\bar\epsilon$ , no separation condition. (15) is deterministic in $\|X^0 - \hat X\|_1$ ; the printed probabilistic hypotheses only feed Theorem 1 into the permutation claim.
The printed $n_{\min} > r$ is replaced by the weaker $n_k \ge 1$ .
Davis–Kahan is stated for the leading eigenspace ( $s = 1$ ), the only case used.
In Lemma 5 the thresholds are required to satisfy $\delta_k \ge 0$ , which the page leaves implicit; for a negative $\delta_k$ the bound (G.4) fails at $\hat V = V$ .

The goal quantifies over every optimal rotation $O$ , not over some orthogonal matrix chosen afterwards (which could make $\mathcal S_k$ empty), and over every top-eigenvector matrix and every approximate k-means solution; a formalization that fixes $\hat U$ to good eigenvectors, compares only against the true labels, or drops the eigenvalue-dominance clause (allowing bottom eigenvectors) proves a different and partly false statement.

Contributions welcome: Davis–Kahan in Frobenius norm for symmetric real matrices (general $s$ included), the Lei–Rinaldo lemma in full, and the eigenstructure of block-constant matrices.

Selected references

P. R. Srivastava, P. Sarkar, G. A. Hanasusanto, A Robust Spectral Clustering Algorithm for Sub-Gaussian Mixture Models with Outliers, arXiv:1912.07546v3, 2021; Operations Research 71(1), 2023. https://arxiv.org/abs/1912.07546
J. Lei, A. Rinaldo, Consistency of spectral clustering in stochastic block models, Annals of Statistics 43(1), 215–237, 2015. https://doi.org/10.1214/14-AOS1274
Y. Yu, T. Wang, R. J. Samworth, A useful variant of the Davis–Kahan theorem for statisticians, Biometrika 102(2), 315–323, 2015. https://doi.org/10.1093/biomet/asv008
C. Davis, W. M. Kahan, The rotation of eigenvectors by a perturbation. III, SIAM Journal on Numerical Analysis 7(1), 1–46, 1970. https://doi.org/10.1137/0707001

8 thms2 active usersReviewed

Completed

Optimization·Captain: mikedeng1

A Robust Spectral Clustering Algorithm for Sub-Gaussian Mixture Models with Outliers 3: Binary PSD Rank-r Lifting (4) Is Equivalent to Robust Cluster Assignment (3)Research Paper

Why this formulation matters

Clustering separates observations into groups whose members resemble one another. In kernel clustering, a matrix $K$ records a similarity score for each pair of observations, and an assignment seeks groups with high total within-group similarity. Real data can also contain outliers, observations that should not be assigned to any cluster. Srivastava, Sarkar, and Hanasusanto use a binary assignment program that permits those unassigned observations and then express the same exact problem through a matrix of pairwise co-memberships. The relationship is stated as Proposition 1 of their preprint. It is the algebraic starting point for the tractable relaxations introduced immediately after the proposition in §3.

The two exact programs have different variables. The assignment program describes each observation's cluster directly. The lifted program records whether each pair belongs to the same cluster. The latter representation makes positive semidefiniteness and rank explicit, and it is the one the paper relaxes to obtain its semidefinite program. A precise equivalence matters because a relaxation of the wrong feasible set would no longer be a relaxation of the stated assignment problem.

The two finite matrix programs

Let $N$ be the number of observations and $r$ the number of available clusters. A binary assignment matrix $Z\in\{0,1\}^{N\times r}$ has one row per observation and one column per cluster. In formulation (3), each row sums to at most one. A row with one nonzero entry assigns its observation to that cluster; a zero row leaves the observation unassigned. Thus the same matrix represents both inliers and outliers. Cluster sizes need not be equal, and unused cluster columns are allowed.

The clustering matrix $X=ZZ^\top$ has one row and column per observation. Its entry $X_{ij}$ is one when observations $i$ and $j$ share a cluster and zero otherwise, including when either observation has a zero assignment row. Formulation (4) asks instead for an $N\times N$ matrix $X$ whose entries lie in $\{0,1\}$ , that is positive semidefinite, and whose rank is at most $r$ . The rank bound limits the number of distinct nonzero cluster directions. Positive semidefiniteness is a property of the full real matrix, including its symmetry; it is not merely a condition on its diagonal.

Let $K\in\mathbb R^{N\times N}$ be the similarity matrix, $\gamma\in\mathbb R$ a penalty parameter, and $E_N$ the all-ones $N\times N$ matrix. The entrywise Frobenius inner product is $\langle A,B\rangle=\sum_{i,j}A_{ij}B_{ij}$ . The programs maximize, respectively, $\langle K-\gamma E_N,ZZ^\top\rangle$ over feasible $Z$ and $\langle K-\gamma E_N,X\rangle$ over feasible $X$ . Both have a feasible zero matrix, even at the boundary values $N=0$ and $r=0$ .

Formalization targets

The goal is Proposition 1, stated with its factor and rotation. If $X^*$ is an optimal matrix for (4), there must exist $G\in\mathbb R^{N\times r}$ and an orthogonal $O\in\mathbb R^{r\times r}$ such that $Z^*=GO$ is feasible and optimal for (3), with

X^*=GG^\top,\qquad \langle K-\gamma E_N,Z^*Z^{*\top}\rangle =\langle K-\gamma E_N,X^*\rangle.

Here “feasible and optimal” includes the zero-one entry condition, the row-sum bound, and comparison with every feasible assignment matrix. The objective identity alone would say little: once the Gram factorization and orthogonality hold, it follows algebraically. The substantive result is the existence of an assignment-compatible rotation of a factor of every lifted optimum.

The milestone list follows the five claims in Appendix B of the preprint: lifting a feasible assignment to a feasible $X$ without changing its value; factoring a rank-bounded positive semidefinite $X$ through $r$ columns; classifying factor rows as zero or unit vectors; showing that distinct nonzero rows are orthogonal; and rotating those rows into assignment coordinates. These statements address both directions of the feasible-set correspondence used by Proposition 1.

What the result supplies

The proposition says that the matrix constraints in (4) describe the same exact clustering choices as the assignment constraints in (3), up to a choice of orthogonal coordinates for the factor. A lifted optimum therefore represents an assignment optimum rather than merely a matrix with the same numerical objective. Conversely, an assignment can always be lifted to a matrix accepted by (4). The paper can then drop the binary or rank constraints to obtain relaxations while keeping a clear exact program as their reference point; see §3 of the preprint.

The proposition is proved in the source paper. This mission seeks a machine-checked proof of that known claim and reusable finite-matrix results about binary positive semidefinite Gram matrices. In particular, the factorization and row-structure milestones can be used beyond spectral clustering whenever a zero-one Gram matrix appears with a rank bound. The Lean declarations here are proposed statements; their sorry proofs remain for solvers to complete.

Where the difficulty lies

The forward implication is immediate once a valid assignment matrix is given: its Gram matrix is positive semidefinite and has rank at most the number of cluster columns. The reverse implication carries the mathematical work. Positive semidefiniteness and low rank alone produce a real factor, but the factor need not have zero-one entries. A generic factor rotation also need not yield one-hot rows. The zero-one condition on every Gram entry is what constrains the relative positions of the nonzero rows strongly enough to recover assignment directions. The result must work when several observations share a direction, when some rows vanish, and when fewer than $r$ clusters are occupied.

Formalization scope

The formalization uses Mathlib matrices indexed by Fin N and Fin r over $\mathbb R$ . Feasibility of (3) is entrywise membership in $\{0,1\}$ together with row sums at most one. Feasibility of (4) is entrywise membership in $\{0,1\}$ , Matrix.PosSemidef, and Matrix.rank ≤ r. The objectives use the explicit sum of entrywise products, so no operator norm or alternate matrix inner product enters the statement. Global optimality is defined by comparison against the corresponding whole feasible set. The factor $G$ has exactly $r$ columns, and the rotation belongs to the real orthogonal group of dimension $r$ .

The paper obtains $K$ from a Gaussian kernel and takes $\gamma\in(0,1)$ for the clustering application. Proposition 1 and Appendix B use only the displayed algebraic programs, so the formal statement permits arbitrary real $K$ and $\gamma$ . No probability model, symmetry assumption on $K$ , positive dimension assumption, or nonempty-cluster condition is needed. The boundary cases $N=0$ and $r=0$ retain their literal meanings. The formalization cannot assume that a feasible $X$ is already block diagonal or is already a Gram matrix of a binary assignment; that is the conclusion being established.

Useful contributions include proofs of the five Appendix B milestones, a finite-dimensional factorization theorem with the prescribed number of columns, and the rotation theorem that handles repeated or zero rows. These pieces should share the stated definitions so that the eventual proof of Proposition 1 uses precisely formulations (3) and (4).

Selected references

P. R. Srivastava, P. Sarkar, and G. A. Hanasusanto, A Robust Spectral Clustering Algorithm for Sub-Gaussian Mixture Models with Outliers, Operations Research 71(1), 2023; arXiv:1912.07546v3, §3, Proposition 1 and Appendix B.

7 thms2 active usersReviewed

Optimization Quantum Information Theoretical Computer Science·Captain: mikedeng1

Optimization by Decoded Quantum Interferometry 1: The Semicircle Law — the Optimal Degree-ℓ DQI State Satisfies ⟨s⟩/m → (√(μ(1−ρ)) + √(ρ(1−μ)))² When 2ℓ + 1 < d⊥Research Paper

Motivation

Decoded quantum interferometry (DQI) is a quantum algorithm, introduced by Jordan, Shutty, Wootters, Zalcman, Schmidhuber, King, Isakov, Khattar and Babbush (arXiv:2408.08292), that turns an approximate optimization problem over a finite field into a decoding problem for a linear code. It applies to max-LINSAT: given linear constraints over $\mathbb F_p$ , satisfy as many of them as possible. For structured instances such as optimal polynomial intersection the authors find DQI reaching approximation ratios that no known polynomial-time classical algorithm reaches, which makes it one of the few concrete candidates for a quantum advantage in optimization.

Whether DQI is useful on an instance depends on one number: the expected fraction of constraints satisfied by the string it outputs. Theorem 4.1 of the paper computes this number, in the limit of many constraints, for the best DQI state of a given degree. Every comparison of DQI with classical algorithms in the paper (simulated annealing, Prange's algorithm, the OPI and max-XORSAT benchmarks) is a comparison against this formula, and the follow-up analysis of imperfect decoders (Theorem 10.1) is a perturbation of it.

Setting

Fix a prime $p$ . A max-LINSAT instance is a matrix $B\in\mathbb F_p^{m\times n}$ with rows $\mathbf b_1,\dots,\mathbf b_m$ and subsets $F_1,\dots,F_m\subseteq\mathbb F_p$ ; constraint $i$ asks that $\mathbf b_i\cdot\mathbf x\in F_i$ (Definition 2.1). Throughout, $m>n$ and every $F_i$ has the same size $r\in\{1,\dots,p-1\}$ . Put $f_i(a)=+1$ if $a\in F_i$ and $-1$ otherwise, and

f(\mathbf x)=\sum_{i=1}^m f_i(\mathbf b_i\cdot\mathbf x),\qquad s(\mathbf x)=\#\{i:\mathbf b_i\cdot\mathbf x\in F_i\}.

For a real polynomial $P$ of degree at most $\ell$ , the DQI state is $|P(f)\rangle=\sum_{\mathbf x\in\mathbb F_p^n}P(f(\mathbf x))|\mathbf x\rangle$ , normalized so that $\sum_{\mathbf x}P(f(\mathbf x))^2=1$ . Measuring it in the computational basis returns $\mathbf x$ with probability $P(f(\mathbf x))^2$ , so the expected number of satisfied constraints is

\langle s\rangle=\sum_{\mathbf x}P(f(\mathbf x))^2\,s(\mathbf x),

and $\langle s^{(m,\ell)}\rangle_{\rm opt}$ is its supremum over all such $P$ .

The dual code is $C^\perp=\{\mathbf d\in\mathbb F_p^m:B^T\mathbf d=0\}$ and $d^\perp$ is the least Hamming weight of a nonzero codeword. The condition $2\ell+1<d^\perp$ says that syndromes of errors of weight up to $\ell$ (and a little more) determine the error.

The analysis passes through rescaled constraint functions $g_i=(f_i-\bar f)/\varphi$ with Fourier transforms $\tilde g_i$ , the elementary symmetric polynomials $P^{(k)}$ evaluated at the $g_i(\mathbf b_i\cdot\mathbf x)$ , and the $(\ell+1)\times(\ell+1)$ symmetric tridiagonal matrix $A^{(m,\ell,d)}$ with diagonal $0,d,2d,\dots,\ell d$ and off-diagonal entries $a_k=\sqrt{k(m-k+1)}$ , at $d=(p-2r)/\sqrt{r(p-r)}$ .

Formalization targets

Goal: Theorem 4.1 (the semicircle law)

Fix $p$ , $r$ and $\mu\ge0$ . For any sequence of instances with $m\to\infty$ , $\ell/m\to\mu$ and $2\ell+1<d^\perp$ , writing $\rho=r/p$ ,

\lim\frac{\langle s^{(m,\ell)}\rangle_{\rm opt}}{m}=\begin{cases}\big(\sqrt{\mu(1-\rho)}+\sqrt{\rho(1-\mu)}\big)^2,&\rho\le1-\mu,\\ 1,&\text{otherwise.}\end{cases}

For $\rho=\tfrac12$ the curve is $\tfrac12+\sqrt{\mu(1-\mu)}$ , a semicircle, which gives the theorem its name.

Milestones

The normalization of the rescaled $g_i$ , (37)–(40).
Lemma A.1: under a common quadratic identity, $P(x_1+\dots+x_m)$ is a fixed linear combination of elementary symmetric polynomials.
The counting identity (68), $\sum_{|\mathbf y|=k}|\tilde g(\mathbf y)|^2=\binom mk$ , and the Fourier picture (65) of the DQI state.
Lemma 9.1 (norm $=\|\mathbf w\|^2$ when $2\ell<d^\perp$ ) and Lemma 9.2 (the expected count is $\frac{mr}p+\frac{\sqrt{r(p-r)}}p\mathbf w^TA^{(m,\ell,d)}\mathbf w$ when $2\ell+1<d^\perp$ ).
The finite-size identity (131): $\langle s^{(m,\ell)}\rangle_{\rm opt}/m=\rho+\sqrt{\rho(1-\rho)}\,\lambda_{\max}^{(m,\ell,d)}/m$ .
Lemma 9.3, $\lambda_{\max}^{(m,\ell,d)}/m\to\mu d+2\sqrt{\mu(1-\mu)}$ , with its lower half (114) and the Gershgorin bound (129).
The algebra (132) and (136)–(137) that produce the closed form.

Significance

The result. Theorem 4.1 makes DQI's performance a closed-form function of two numbers, $r/p$ and $\ell/m$ , and moves every question about an instance into coding theory: how large a $d^\perp$ the instance's dual code has, and whether it can be decoded efficiently up to $\ell$ errors. The OPI advantage claim of the paper, the comparison with Prange's algorithm on max-XORSAT, and the imperfect-decoding bound of Theorem 10.1 all start from this formula. The finite-size identity (131) is also useful on its own: it gives the exact optimum for any instance, not only in the limit.

Formalizing it. The theorem is proved in the paper; to our knowledge no part of it has been machine-checked. A formalization would check the Fourier bookkeeping of §8.2.1 and §9 (normalizations $\sqrt{p^{n-k}\binom mk}$ , character sums over $\mathbb F_p$ ), the claim that every degree- $\ell$ DQI state is a combination of the $|P^{(k)}\rangle$ and conversely, and the eigenvalue asymptotics of the tridiagonal matrix. Two points of the printed text need care and are stated correctly here: Lemma 9.2 writes its decomposition in the $f_i$ where the normalization requires the rescaled $g_i$ , and the "otherwise $=1$ " branch of Theorem 4.1 is argued only briefly on p. 34.

Difficulty

The algebraic steps are finite but long, and every one carries a normalization that a careless formalization gets wrong. The asymptotic step is the main obstacle. Lemma 9.3 needs a lower bound on $\lambda_{\max}$ from a test vector of growing width and a matching upper bound from Gershgorin's theorem, and the upper bound holds only under $d\ge-(m-2\ell)/\sqrt{\ell(m-\ell)}$ , which is exactly the regime $\rho\le1-\mu$ . In the other regime that hypothesis fails and the Gershgorin bound overshoots, so the limit $1$ needs a separate argument; the observation that $\langle s\rangle_{\rm opt}$ "increases in $r$ ", printed on p. 34, does not give it at fixed $p$ and $r$ . A second difficulty is that $\langle s\rangle_{\rm opt}$ is a supremum over polynomials, while Lemma 9.2 is a statement about weight vectors $\mathbf w$ ; identifying the two needs both directions of Lemma A.1's correspondence and the normalization of Lemma 9.1.

Formalization scope

All objects live in the namespace DQI.Semicircle and one definitions file. $\mathbb F_p$ is ZMod p with [Fact p.Prime]; vectors are Fin n → ZMod p; constraints are indexed by Fin m from $0$ . $\omega_p^a=\exp(2\pi i\,a/p)$ is computed from the representative of $a$ in $\{0,\dots,p-1\}$ . Polynomials are real with natDegree ≤ ℓ; weight vectors are real. The optimum $\langle s\rangle_{\rm opt}$ is the real supremum over exactly the normalized polynomials of degree at most $\ell$ evaluated at $f(\mathbf x)$ ; its set is nonempty (constant polynomials) and bounded by $m$ . The dual-distance condition is "every nonzero $\mathbf d$ with $B^T\mathbf d=0$ has weight $>t$ "; $d^\perp$ is never an infimum, and $m>n$ (the paper's standing assumption) guarantees a nonzero codeword, so the condition forces $2\ell<m$ . $\lambda_{\max}$ is the supremum of the real spectrum. The limit " $m\to\infty$ with $\ell/m$ fixed" is any sequence of instances with $m_j\to\infty$ and $\ell_j/m_j\to\mu$ , with $p$ and $r$ fixed along it. Convergence of the ratio includes irrational $\mu$ with integer sizes.

Added hypotheses, all disclosed in the items: Lemma 9.2 decomposes in the $g_i$ rather than the printed $f_i$ ; (129) assumes $\ell\ge1$ to avoid dividing by $\sqrt0$ ; Lemma 9.3 imposes its hypothesis on $d$ only when $\ell_j\ge1$ ; (114) is stated as a $\liminf$ with an explicit $\varepsilon$ .

A formalization that replaces $\langle s\rangle_{\rm opt}$ by a supremum over all states (which gives $1$ ), drops "nonzero" from the distance condition (which makes it unsatisfiable), or states the goal at a single $m$ is not this theorem and is ruled out by the definitions above.

Needed infrastructure: Fourier analysis on $\mathbb F_p^n$ (character orthogonality, Parseval), elementary symmetric polynomials and their reduction modulo a quadratic, Rayleigh quotients and Gershgorin discs for real symmetric matrices, and elementary limits. The tridiagonal-matrix bounds and the quadratic-reduction lemma are reusable beyond DQI. Proofs of any milestone, alternative arguments for the "otherwise" branch, and sharper finite- $m$ bounds on $\lambda_{\max}$ are welcome.

Selected references

S. P. Jordan, N. Shutty, M. Wootters, A. Zalcman, A. Schmidhuber, R. King, S. V. Isakov, T. Khattar, R. Babbush, Optimization by Decoded Quantum Interferometry, arXiv:2408.08292v5, 2025. https://arxiv.org/abs/2408.08292
S. Gershgorin, Über die Abgrenzung der Eigenwerte einer Matrix, Izv. Akad. Nauk SSSR, Ser. Fiz.-Mat. 6, 749–754, 1931.
R. G. Gallager, Low-Density Parity-Check Codes, IRE Trans. Inform. Theory 8(1), 21–28, 1962. https://doi.org/10.1109/TIT.1962.1057683

14 thms2 active usersReviewed

Linear Optimization Theoretical Computer Science·Captain: mikedeng1

A Strongly Polynomial Algorithm for Linear Exchange Markets II: A Z₊-Matrix Polyhedron P_M Lies Between an M2VPI Polyhedron and Its Scaling by B²Research Paper

Motivation

In a linear exchange market every agent owns one divisible good and has linear utilities over all goods; an equilibrium is a price vector at which every agent can spend its budget on goods that maximize utility per unit of money, and all goods are sold. Computing such an equilibrium in strongly polynomial time, with a number of arithmetic operations bounded by a polynomial in the number of agents alone, was an open question until Garg and Végh (arXiv:1809.06266; Operations Research, 2023). Their algorithm alternates two kinds of phases. One identifies "revealed" edges that appear in every equilibrium (the subject of mission I of this series). The other computes good starting prices for the current set of revealed edges by solving a linear program whose constraint matrix has a special sign structure.

No strongly polynomial algorithm is known for that linear program. Systems in which every inequality has at most one positive and at most one negative coefficient, by contrast, are strongly polynomially solvable (Megiddo, 1983; Hochbaum and Naor, 1994). The paper bridges the gap with Theorem 6.4: a polyhedron given by a $Z_+$ -matrix is sandwiched between a monotone two-variable-per-inequality polyhedron and its scaling by an explicit factor $B^2$ . This mission formalizes that theorem and the lemmas of §7 that prove it. It is a statement about matrices and polyhedra only; no market notions enter.

Setting

Matrices are rational. For integers $k, t \ge 0$ a matrix $M \in \mathbb{Q}^{k\times t}$ is a $Z_+$ -matrix, written $M \in \mathcal{Z}_+(k,t)$ , if every off-diagonal entry is nonpositive and every column sum is nonnegative:

M_{ij} \le 0 \quad (i \ne j), \qquad \sum_{i=1}^k M_{ij} \ge 0 \quad (j \in [t]).

For a non-square matrix the diagonal entries are the $M_{ii}$ with $1 \le i \le \min\{k,t\}$ . Square $Z_+$ -matrices are exactly the transposes of weighted Laplacians of directed graphs, or such transposes with one row and column deleted.

$\mathcal{M}_2(m,t)$ is the set of $m\times t$ rational matrices with at most one positive and at most one negative entry in every row. A system $\bar M x \le \bar b$ with $\bar M \in \mathcal{M}_2(m,t)$ is a monotone two-variable-per-inequality system (M2VPI).

For $M \in \mathcal{Z}_+(k,t)$ and $b \in \mathbb{Q}^k$ with $b > 0$ , the polyhedron of interest is

P_M = \{x \in \mathbb{R}^t : Mx \le b,\ x \ge 0\}.

Write $\ell$ for the number of nonzero entries of $M$ , $\alpha P = \{\alpha x : x \in P\}$ for $\alpha > 0$ , and

B = \frac{\sum_{j=1}^k b_j}{\min_{i\in[k]} b_i}.

In §7 the right-hand side is called $\gamma$ instead of $b$ , and $\lambda_i = \sum_{j\ne i}\gamma_j$ .

The proof works with a square $M \in \mathcal{Z}_+(t,t)$ with positive diagonal. Its digraph $([t],H)$ has an arc $ij$ whenever $M_{ij} < 0$ . $D_i$ is the set of vertices reachable from $i$ (including $i$ ), and $M^{(i)}$ is the submatrix of the rows $M_j$ , $j \in D_i$ . The vertices split into $T_1$ (at most one outgoing arc), $T_2$ (at least two arcs and $\operatorname{rk} M^{(i)} = |D_i|$ ) and $T_3$ (at least two arcs and $\operatorname{rk} M^{(i)} < |D_i|$ ).

Formalization targets

Goal: Theorem 6.4 (p. 15)

For $M \in \mathcal{Z}_+(k,t)$ with $k \ge 1$ and $\ell$ nonzero entries, and $b \in \mathbb{Q}^k$ with $b > 0$ , there are $\ell' \le \ell$ , $\bar M \in \mathcal{M}_2(\ell',t)$ and $\bar b \in \mathbb{Q}^{\ell'}$ with

P_M \subseteq \{x \in \mathbb{R}^t : \bar Mx \le \bar b,\ x \ge 0\} \subseteq B^2 P_M.

Milestones (§7, pp. 16–23)

Lemma 7.1: for $M \in \mathcal{Z}_+(t,t)$ and $\bar p \ge 0$ with $M\bar p \le \gamma$ , $\ M\bar p \ge -\lambda \ge -(B-1)\gamma$ .
Lemma 7.2: the Gaussian elimination of the proof, run on $T \in \mathcal{Z}_+(\ell,t)$ , returns $T' = YT$ with $Y \ge 0$ , $T'$ upper triangular with diagonal entries in $\{0,1\}$ and nonpositive off-diagonal entries, and $T'_{kk} = 1$ whenever some $T_{ik} < 0$ with $i > k$ .
Claim 7.3(iii): for $i \in T_3$ , $M_i$ is a linear combination of $\{M_h : h \in D_i \setminus\{i\}\}$ .
Lemma 7.4(i): for $i \in T_2\cup T_3$ there is a unique $q^{(i)} \in \mathbb{R}^t_+$ with $M_\ell q^{(i)} = 0$ ( $\ell \in D_i\setminus\{i\}$ ), $q^{(i)}_i = 1$ and $q^{(i)}_\ell = 0$ off $D_i$ .
Lemma 7.4(iv) and (iii): points $r^{(i)} \in P_M$ tight on $D_i\setminus\{i\}$ (for $i \in T_3$ ) and on $D_i$ with $r^{(i)}_i = \kappa(i)$ (for $i \in T_2$ ).
Claim 7.5: $\kappa(i)\,M_i q^{(i)} \le B\gamma_i$ for $i \in T_2$ .
The reduced case (§7, p. 16): Theorem 6.4 for square $M$ with positive diagonal.

Significance

Theorem 6.4 turns an LP over a $Z_+$ constraint matrix, for which no strongly polynomial algorithm is known, into an M2VPI system that is strongly polynomially solvable, at the price of a factor $B^2$ . In the exchange-market algorithm $B \le n$ , so the starting prices of each phase come within a factor $n^2$ of optimal (the proof of Theorem 3.7, p. 15). That bound is what lets the potential argument advance in a polynomial number of phases. The construction is not specific to markets: any LP of the form $\max \sum_i x_i$ over $P_M$ with $M$ a $Z_+$ -matrix, which includes LPs over transposed weighted Laplacians of directed graphs, inherits the same approximation.

The result is proved in the paper; to our knowledge none of it has been machine-checked. A formalization produces a checked proof of the sandwich. It also produces reusable facts about Gaussian elimination on $Z_+$ -matrices (Lemma 7.2), which hold for any matrix whose off-diagonal entries are nonpositive and whose column sums are nonnegative.

Difficulty

The obvious approach, deleting all but two variables from each inequality of $P_M$ , fails: the dropped negative terms make the resulting system either too weak or invalid. The paper instead derives one new constraint per arc $ij$ of $H$ , as a nonnegative combination of the inequalities $M\bar p \ge -\lambda$ . Finding it requires an ordering of $D_i$ in which every vertex but $i$ has an in-neighbour placed after it, and an elimination on the permuted submatrix whose penultimate row has exactly two nonzero entries. The reverse containment $\{\bar M\bar p \le \bar b\} \subseteq B^2P_M$ is the hard direction. It splits by whether the rows on $D_i$ are linearly independent ( $T_2$ ) or not ( $T_3$ ), and the $T_2$ case needs the extra constraint $\bar p_i \le \kappa(i)$ and the comparison of entries of the elimination multipliers $Y^{(ij)}$ in Claim 7.5. Every step relies on a sign invariant of the elimination that Lemma 7.2 proves by induction.

Formalization scope

Indices are 0-based (Fin k, Fin t); the paper's $[n] = \{1,\dots,n\}$ . Matrices $M$ , $\bar M$ and right-hand sides $b$ , $\bar b$ , $\gamma$ are rational (ℚ), as on p. 15, and act on real vectors $x \in \mathbb{R}^t$ through the cast. A diagonal entry of a rectangular matrix is one whose two indices agree as natural numbers. $B^2P_M$ is the image $\{B^2x : x \in P_M\}$ . $B$ is defined for $k \ge 1$ only, and every statement using it assumes $k \ge 1$ (resp. $t \ge 1$ ).

Not formalized: the running time $O(\ell(\min\{k,t\})^3)$ and the polynomial bound on the encoding size of $\bar M$ , $\bar b$ in Theorem 6.4. The goal is the existence statement that the construction (13) witnesses. The standing assumptions of §7 ( $\gamma > 0$ ; positive diagonal after the reduction) appear as hypotheses of the milestones that live in that setting.

Lemma 7.2 is stated about the specific elimination of the proof (p. 17), defined explicitly; an existential "there is $Y \ge 0$ " form would be nearly trivial, since $Y = 0$ satisfies all but one clause. In the goal, $\bar M$ must have at most one positive and at most one negative entry per row, and $\ell' \le \ell$ . Dropping either requirement makes the goal weaker than the paper's theorem.

$\kappa(i)$ , defined in (12) through the elimination for an arbitrarily chosen arc, is restated intrinsically as the $i$ -th entry of $(M_{D_i,D_i})^{-1}\gamma_{D_i}$ , a number the paper shows equal (proof of Lemma 7.4(iii)). It is used only for $i \in T_2$ , where that block is invertible. Claim 7.3(i)–(ii) and Lemma 7.4(ii), which concern the elimination output for a particular arc, are not milestones.

A complete development needs the elimination and its invariants, reachability in a finite digraph, ranks of row submatrices, and the construction (13). The elimination lemmas are reusable for any $Z_+$ -matrix. Contributions are welcome on any milestone, on the reduction from rectangular $M$ to the square positive-diagonal case, and on the two containments of the reduced case.

Selected references

J. Garg and L. A. Végh, A strongly polynomial algorithm for linear exchange markets, arXiv:1809.06266v3, 2022; Operations Research, 2023. https://arxiv.org/abs/1809.06266
N. Megiddo, Towards a genuinely polynomial algorithm for linear programming, SIAM Journal on Computing 12(2), 1983. https://doi.org/10.1137/0212022
D. S. Hochbaum and J. Naor, Simple and fast algorithms for linear and integer programs with two variables per inequality, SIAM Journal on Computing 23(6), 1994. https://doi.org/10.1137/S0097539793251876
R. W. Cottle and A. F. Veinott, Jr., Polyhedral sets having a least element, Mathematical Programming 3, 1972. https://doi.org/10.1007/BF01584975

11 thms2 active usersReviewed

Information Theory Quantum Error Correction Quantum Information·Captain: mikedeng1

Reversing quantum dynamics with near-optimal quantum and classical fidelity I: The Reversal Operation Attains at Least the Square of the Optimal Average Entanglement FidelityResearch Paper

Motivation

Quantum error correction and quantum communication both ask the same question: after a known noise process $\mathcal A$ has acted on a quantum system, how well can its effect be undone? For a given noise model the best recovery is the solution of a semidefinite program, which gives a number but no structure and no formula. Barnum and Knill showed in 2000 that a single, explicit recovery map, built from $\mathcal A$ and the input state alone, is always close to the best one: its fidelity is at least the square of the optimal fidelity (arXiv:quant-ph/0004088). The map they use is now usually called the Petz recovery map or transpose channel; Petz had introduced it in operator-algebraic work on sufficiency (Petz 1986; Petz 1988). Near-optimality results of this kind underlie approximate quantum error correction and the later theory of recoverability in quantum information.

Timeline.

1986–1988, D. Petz: the map $\rho^{1/2}\mathcal A^\dagger(\mathcal A(\rho)^{-1/2}\,\cdot\,\mathcal A(\rho)^{-1/2})\rho^{1/2}$ characterizes when a channel can be reversed exactly on a family of states.
2002, Barnum and Knill (J. Math. Phys. 43, 2097; doi:10.1063/1.1459754): in the published version, the reversal operation achieves at least the square of the optimal entanglement fidelity for a single input state.
arXiv v2 of the same paper (the source of this mission): the published Eq. (34) had dropped the ensemble weights; with that corrected, the bound holds for the average entanglement fidelity of any ensemble of commuting density matrices (Acknowledgments, p. 14).

Setting

A finite-dimensional quantum system is described by complex $n\times n$ matrices; $X^\dagger$ is the conjugate transpose, and a density matrix is a positive semidefinite matrix of trace one. A completely positive map $\mathcal A$ is given by a finite decomposition $\mathcal A\sim\{A_i\}_i$ of matrices and acts by

\mathcal A(X)=\sum_iA_iXA_i^\dagger .

It is trace-preserving if $\sum_iA_i^\dagger A_i=I$ and trace-nonincreasing if $\sum_iA_i^\dagger A_i\le I$ in the Loewner order. The composite $\mathcal R\mathcal A$ has decomposition $\{R_kA_i\}_{(k,i)}$ .

For a state $\rho$ the paper defines the reversal operation

\mathcal R_{\mathcal A,\rho}\sim\{\rho^{1/2}A_i^\dagger\,\mathcal A(\rho)^{-1/2}\}_i,

under the standing assumption that $\mathcal A(\rho)$ has full support. Here $X^{-1/2}$ is the generalized inverse square root: invert the square roots of the non-zero eigenvalues and keep the zero eigenvalues.

Fidelities are measured by the entanglement fidelity $F_e(\rho,\mathcal K)=\sum_k|\operatorname{tr}K_k\rho|^2$ of a map $\mathcal K\sim\{K_k\}_k$ and, for an ensemble $E=\{p_l,\rho_l\}_l$ (weights $p_l\ge0$ summing to one, density matrices $\rho_l$ ), by the average entanglement fidelity

\bar F_e(E,\mathcal K)=\sum_lp_lF_e(\rho_l,\mathcal K).

When $\rho=\sum_ip_i|i\rangle\langle i|$ in an orthonormal eigenbasis, the classical fidelity is $F_{\mathrm{cl}}(\rho,\mathcal K)=\sum_ip_i\langle i|\mathcal K(|i\rangle\langle i|)|i\rangle$ , the average entanglement fidelity of the ensemble of eigenstates.

Formalization targets

Goal: Theorem 3 (p. 7)

Let $\mathcal A$ be trace-preserving, $E=\{p_l,\rho_l\}_l$ an ensemble of pairwise commuting density matrices, $\rho=\sum_lp_l\rho_l$ , and assume $\mathcal A(\rho)$ has full support. Then for every trace-preserving completely positive $\mathcal R$ ,

\bar F_e(E,\mathcal R_{\mathcal A,\rho}\mathcal A)\;\ge\;\bar F_e(E,\mathcal R\mathcal A)^2 .

Milestones

The milestones follow the paper's proof:

Lemma 1 (p. 7): $\mathcal R_{\mathcal A,\rho}$ depends only on the map $\mathcal A$ , not on its decomposition.
(14)–(15) (p. 7): after replacing $R_k$ by $P_CR_k$ ( $P_C$ the support projector of $\rho$ ), which leaves $\bar F_e$ unchanged and makes $\mathcal R$ trace-nonincreasing, each $R_k=\rho^{1/2}B_k^\dagger\mathcal A(\rho)^{-1/2}$ , and $\mathcal B(\rho)\le\mathcal A(\rho)$ .
(28)–(32) (p. 9): $\sum_lp_l\sum_i|\operatorname{tr}\rho_lR^l_iB^l_i|^2\le\sum_lp_l\sum_{i,j}\operatorname{tr}R^l_iB^l_j\rho_lB_j^{l\dagger}R_i^{l\dagger}$ .
(33)–(34) (p. 9): that sum equals $\operatorname{tr}\mathcal R(\mathcal B(\rho))\le\operatorname{tr}\mathcal R(\mathcal A(\rho))\le1$ .

Two companions are also posed: Proposition 2, $\mathcal R_{\mathcal A,\rho}(\mathcal A(\rho))=\rho$ , and Corollary 4, $F_{\mathrm{cl}}(\rho,\mathcal R\mathcal A)\le\sqrt{F_{\mathrm{cl}}(\rho,\mathcal R_{\mathcal A,\rho}\mathcal A)}$ and $F_e(\rho,\mathcal R\mathcal A)\le\sqrt{F_e(\rho,\mathcal R_{\mathcal A,\rho}\mathcal A)}$ .

Significance

The result. Theorem 3 says that the error $1-\bar F_e$ of the reversal operation is at most twice the optimal error, since $(1-\eta)^2\ge1-2\eta$ . It gives a closed-form recovery whose performance is within a factor two in error of the semidefinite optimum, for every noise process and every commuting ensemble. Taking the ensemble of eigenstates of $\rho$ (Corollary 4) gives the same guarantee for classical information sent through a quantum channel; the companion mission (II of this series) applies the construction to state discrimination, where the reversal operation is the pretty good measurement.

Formalizing it. The result is proved on paper; none of it has a machine-checked proof that we know of. The mission asks for the full argument: the decomposition independence of the reversal map, the reduction to the support of $\rho$ , the singular-value change of decomposition (17)–(18), the chain (19)–(26) of Cauchy–Schwarz inequalities, and the normalization (27)–(34). It also fixes in Lean the arXiv v2 statement (commuting ensembles), which is stronger than the published one.

Difficulty

The obvious approach is to compare $\mathcal R_{\mathcal A,\rho}$ with an optimal $\mathcal R$ term by term. That fails: the fidelity of $\mathcal R\mathcal A$ is a sum of squared traces mixing the decompositions of $\mathcal R$ and $\mathcal A$ , and no termwise inequality relates it to the fidelity of $\mathcal R_{\mathcal A,\rho}\mathcal A$ . The paper first rewrites every recovery in the shape of the reversal map, then chooses, for each ensemble member separately, new decompositions of $\mathcal A$ and $\mathcal B$ that diagonalize a coefficient matrix; making that choice legitimate needs the unitary freedom of Kraus decompositions, which Mathlib does not have. The commutation $[\rho,\rho_l]=0$ is used to move fractional powers of $\rho$ and $\rho_l$ past each other inside traces; without commutation the authors do not know whether the theorem holds (p. 10).

Formalization scope

Matrices are Matrix n n ℂ over a finite type n with decidable equality; Loewner order, square roots and functional calculus come from Mathlib (open scoped MatrixOrder). The map $X\mapsto\sum_iA_iXA_i^\dagger$ is the published PeresTerno.krausUpdate, referenced, not redefined.
Maps are unbundled Kraus families over arbitrary finite index types. The recovery $\mathcal R$ in Theorem 3 ranges over every finite family with $\sum_kR_k^\dagger R_k=I$ .
$X^{-1/2}$ is cfc (fun x => (Real.sqrt x)⁻¹) X, the generalized inverse; Mathlib's junk matrix inverse is not used. The support projector is the functional calculus of the indicator of $x\ne0$ .
$F_e$ is defined by the formula (8), which the paper derives from its purification definition. $F_{\mathrm{cl}}$ takes an orthonormal eigenbasis and weights as data, with $\rho=\sum_ip_i|i\rangle\langle i|$ as a hypothesis.
Standing hypotheses, all from the paper: $\mathcal A$ trace-preserving (§II's noise model); $\mathcal A(\rho)$ positive definite (full support, p. 7); the ensemble is a probability vector of pairwise commuting density matrices with $\rho=\sum_lp_l\rho_l$ .
In (34) the page prints $\operatorname{tr}\mathcal R(\mathcal A(\rho))=1$ ; after the replacement $R_k\mapsto P_CR_k$ the map is only trace-nonincreasing, so the milestone states $\le1$ .
Trivializing encodings are ruled out: the reversal family is the literal formula (12) for the given $\mathcal A$ and the ensemble's own $\rho$ , and the fidelity of a composite map is (8) applied to the composite decomposition $\{R_kA_i\}$ , never the right-hand side of the proof's chain.
Infrastructure a complete development needs, reusable beyond this mission: the unitary freedom of Kraus decompositions, the singular value decomposition of a complex square matrix, the trace Cauchy–Schwarz inequality for Hilbert–Schmidt products, and functional-calculus identities such as $\rho^{1/2}\rho^{-1/2}=P_C$ . Contributions of any of these as separate theorems are welcome. The pure-state, measurement form $P_{\mathrm{opt}}^2\le P_{\mathrm{PGM}}\le P_{\mathrm{opt}}$ is already posed on the platform as QAlgorithms.Arunachalam.barnumKnill and is not repeated here.

Selected references

H. Barnum, E. Knill, Reversing quantum dynamics with near-optimal quantum and classical fidelity, arXiv:quant-ph/0004088v2. https://arxiv.org/abs/quant-ph/0004088
H. Barnum, E. Knill, same title, J. Math. Phys. 43, 2097 (2002). https://doi.org/10.1063/1.1459754
D. Petz, Sufficient subalgebras and the relative entropy of states of a von Neumann algebra, Commun. Math. Phys. 105, 123–131 (1986). https://doi.org/10.1007/BF01212345
D. Petz, Sufficiency of channels over von Neumann algebras, Quart. J. Math. 39, 97–108 (1988). https://doi.org/10.1093/qmath/39.1.97
B. Schumacher, Sending entanglement through noisy quantum channels, Phys. Rev. A 54, 2614 (1996). https://doi.org/10.1103/PhysRevA.54.2614
R. A. Horn, C. R. Johnson, Matrix Analysis, Cambridge University Press (1985), §7.3. https://doi.org/10.1017/CBO9780511810817

7 thms2 active usersReviewed

Information Theory Quantum Error Correction·Captain: mikedeng1

Quantum LDPC Codes with Positive Rate and Minimum Distance Proportional to n^{1/2}: The Hypergraph Product of a Full-Rank [n,k,d] Parity-Check Matrix with Itself Is an [[n²+(n−k)², k², d]] CSS CodeResearch Paper

Motivation

Quantum computers need error correction, and the codes that are cheapest to run in hardware are quantum low-density parity-check (LDPC) codes: every check involves a bounded number of qubits, and every qubit takes part in a bounded number of checks. For a long time the only well-understood quantum LDPC codes were surface codes such as Kitaev's toric code, whose minimum distance grows like the square root of the length but which encode a fixed number of qubits, so their rate tends to zero. Tillich and Zémor (arXiv:0903.0566; IEEE Transactions on Information Theory, 2014; preliminary version ISIT 2009) gave the first general construction of quantum LDPC codes with positive rate and minimum distance proportional to $\sqrt N$ , from any classical LDPC code. Their hypergraph product became the standard building block of the field.

Timeline.

1996: Calderbank–Shor and Steane introduce CSS codes, quantum codes built from two classical binary codes (quant-ph/9512032, quant-ph/9601029).
1997: Kitaev's toric code: LDPC, distance $\Theta(\sqrt N)$ , dimension 2 (quant-ph/9707021).
2009: Tillich and Zémor: the hypergraph product, with positive rate and distance $\Theta(\sqrt N)$ (this mission).
2020–2021: distance beyond $\sqrt N$ for quantum LDPC codes: $\sqrt N\log N$ by Evra, Kaufman and Zémor (arXiv:2004.07935); $N^{3/5}$ up to polylogarithmic factors by Hastings, Haah and O'Donnell (arXiv:2009.03921).
2022: Panteleev and Kalachev construct asymptotically good quantum LDPC codes, using lifted products that generalize the hypergraph product (arXiv:2111.03654).

Setting

All codes are binary linear codes, subspaces of $\mathbb F_2^{\iota}$ for a finite coordinate set $\iota$ . The Hamming weight $|x|$ of $x$ is its number of nonzero coordinates. The minimum distance $d(\mathcal C)$ of a code is the least weight of a nonzero codeword, with the convention $d(\{0\})=\infty$ .

A Tanner graph $\mathcal G=\mathcal T(V,C,E)$ is the bipartite graph of a parity-check matrix $H\in\mathbb F_2^{C\times V}$ : the variable nodes $V$ index the columns, the check nodes $C$ index the rows, and $c\sim v$ iff $H_{cv}=1$ . Its code is $\mathcal C=\ker H$ . The transpose Tanner graph $\mathcal G^T$ is that of $H^T$ , and its code $\mathcal C^T=\ker H^T$ is the transpose code. It depends on the matrix $H$ , not only on $\mathcal C$ .

A CSS code is a pair $(\mathcal C_X,\mathcal C_Z)$ of codes of the same length $N$ with $\mathcal C_Z^\perp\subseteq\mathcal C_X$ . Its quantum dimension and quantum minimum distance are

k_Q=\dim(\mathcal C_X/\mathcal C_Z^\perp),\qquad d_Q=\min(d_X,d_Z),\quad d_X=\min\{|x|:x\in\mathcal C_X\setminus\mathcal C_Z^\perp\},

with $d_Z$ defined symmetrically and $\min\emptyset=\infty$ .

Given $H_1\in\mathbb F_2^{C_1\times V_1}$ and $H_2\in\mathbb F_2^{C_2\times V_2}$ with Tanner graphs $\mathcal G_1,\mathcal G_2$ , the code $\mathcal Q(\mathcal G_1\times\mathcal G_2)$ has qubits $(V_1\times V_2)\sqcup(C_1\times C_2)$ and check matrices

H_X=\big(H_1\otimes I_{V_2}\ \big|\ I_{C_1}\otimes H_2^T\big),\qquad H_Z=\big(I_{V_1}\otimes H_2\ \big|\ H_1^T\otimes I_{C_2}\big),

with $\mathcal C_X=\ker H_X$ and $\mathcal C_Z=\ker H_Z$ . Write $k_i=\dim\mathcal C_i$ , $k_i^T=\dim\mathcal C_i^T$ , $d_i=d(\mathcal C_i)$ and $d_i^T=d(\mathcal C_i^T)$ .

Formalization targets

Goal: Theorem 1 (p. 3)

Let $H$ be a full-rank $(n-k)\times n$ parity-check matrix of an $[n,k,d]$ code. The code $\mathcal Q(\mathcal G\times\mathcal G)$ built from two copies of its Tanner graph is a CSS code with

N=n^2+(n-k)^2,\qquad k_Q=k^2,\qquad d_Q=d,

and each row of $H_X$ and $H_Z$ has weight $i+j$ , with $i$ a row weight and $j$ a column weight of $H$ .

General results

Proposition 14 (dimension): $k_Q=k_1k_2+k_1^Tk_2^T$ for any two Tanner graphs.
Theorem 15 (distance): $d_Q\ge m:=\min(d_1,d_2,d_1^T,d_2^T)$ , with $d_Q=m$ whenever $d_i=m$ and $d_{3-i}\ne\infty$ , or $d_i^T=m$ and $d_{3-i}^T\ne\infty$ , for some $i\in\{1,2\}$ .

The milestones follow the paper. They are Proposition 4 (validity), eq. (4), Fact 12 and Propositions 9, 10, 13 (product codes and transposes), which lead to Proposition 14. Then come eq. (17), the weight claim and Lemma 16 (lower bound), and the two claims of p. 17 and Lemma 17 (upper bound), which lead to Theorem 15. The degree count of p. 11 gives the row weights.

Significance

The result. The construction needs no orthogonality between the input codes: any two parity-check matrices give a valid CSS code. Its parameters are read off the classical inputs. A family of classical LDPC codes with fixed rate and linear distance therefore gives quantum LDPC codes with fixed rate and distance $\Theta(\sqrt N)$ , and sparse inputs give sparse stabilizers. The toric code is the special case where both inputs are cycle graphs. The hypergraph product is also the base case of the later homological and lifted-product constructions, and the source of the standard decoding and fault-tolerance results for these codes.

Formalizing it. The theorem is proved in the paper; what is missing is a machine-checked proof. The platform holds the toric code's distance and dimension (ToricCode.toric_distance, ToricCode.toric_homologyRank), but over its own chain complex, not over a general construction. This mission produces a reusable layer: Tanner graphs as binary matrices, CSS dimension and distance with the $\infty$ convention, product codes, and the parameters of the hypergraph product for arbitrary finite index sets.

Difficulty

The dimension count is linear algebra once the codes $\ker H_X^T$ and $\ker H_Z^T$ have been identified with product codes. The obstacle is the distance. Lower bounds on the minimum weights of $\mathcal C_X$ and $\mathcal C_Z$ themselves are useless: $\mathcal C_Z^\perp\subseteq\mathcal C_X$ contains the rows of $H_Z$ , which have constant weight, so the minimum weight of $\mathcal C_X$ is bounded by a constant. Any bound of order $\min(d_1,d_2,d_1^T,d_2^T)$ must use the definition of $d_X$ over $\mathcal C_X\setminus\mathcal C_Z^\perp$ and show that every low-weight codeword of $\mathcal C_X$ is degenerate, i.e. lies in $\mathcal C_Z^\perp$ . The upper bound needs an explicit codeword of $\mathcal C_X$ outside $\mathcal C_Z^\perp$ , and showing that it is not in $\mathcal C_Z^\perp$ requires an argument of its own.

Formalization scope

Lean represents a Tanner graph by its matrix H : Matrix C V (ZMod 2) over arbitrary finite index types. The code is ker H, the transpose code is ker Hᵀ, and the dual code is CodingTheory.dualCode from the published definition CodingTheory. Hamming weight is Mathlib's hammingNorm. Minimum distances live in ℕ∞, where the empty infimum is ⊤, the paper's $\infty$ . $k_Q$ is the dimension of the quotient of $\mathcal C_X$ by $\mathcal C_Z^\perp\cap\mathcal C_X$ . In $H_X$ and $H_Z$ the qubits are ordered $(V_1\times V_2)\sqcup(C_1\times C_2)$ , as on p. 18. A product code is a set of $\iota_1\times\iota_2$ matrices whose columns (fixed second coordinate) lie in the first code. The general results are stated without nonemptiness assumptions; they hold for empty index sets.

Theorem 1 has two disclosed differences from the page:

It adds the hypothesis $k\le n$ , which is implicit in " $[n,k,d]$ ". Without it the matrix has no rows and the dimension claim fails.
It drops the word "LDPC", a property of families of codes. Its finite content is the row-weight clause, which is kept.

"There is a construction" is formalized as the paper's construction, the hypergraph product of $H$ with itself.

Several encodings would trivialize the statements and are excluded: an $\mathbb N$ -valued minimum distance that is $0$ on the zero code; $d_X$ taken over $\mathcal C_X\setminus\{0\}$ instead of $\mathcal C_X\setminus\mathcal C_Z^\perp$ ; $k_Q$ computed by truncated natural subtraction; an existential "there is a code with these parameters"; and the transpose code replaced by the dual code.

A complete development needs ranks and kernels of Kronecker products over $\mathbb F_2$ , dimensions of product codes (Proposition 9, not in Mathlib), and the restriction of Tanner graphs to induced subgraphs. The product-code and CSS layers are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for Proposition 14 via the Künneth formula.

Selected references

J.-P. Tillich and G. Zémor, Quantum LDPC codes with positive rate and minimum distance proportional to the square root of the blocklength, IEEE Transactions on Information Theory 60(2), 2014; preprint arXiv:0903.0566v2. https://arxiv.org/abs/0903.0566 , https://doi.org/10.1109/TIT.2013.2292061
A. R. Calderbank and P. W. Shor, Good quantum error-correcting codes exist, Physical Review A 54, 1996. https://arxiv.org/abs/quant-ph/9512032
A. M. Steane, Multiple particle interference and quantum error correction, Proceedings of the Royal Society A 452, 1996. https://arxiv.org/abs/quant-ph/9601029
A. Yu. Kitaev, Fault-tolerant quantum computation by anyons, Annals of Physics 303, 2003. https://arxiv.org/abs/quant-ph/9707021
F. J. MacWilliams and N. J. A. Sloane, The Theory of Error-Correcting Codes, North-Holland, 1977, Ch. 18 §2 (product codes).
S. Evra, T. Kaufman and G. Zémor, Decodable quantum LDPC codes beyond the √n distance barrier using high-dimensional expanders, FOCS 2020. https://arxiv.org/abs/2004.07935
M. B. Hastings, J. Haah and R. O'Donnell, Fiber bundle codes: breaking the N^{1/2} polylog(N) barrier for quantum LDPC codes, STOC 2021. https://arxiv.org/abs/2009.03921
P. Panteleev and G. Kalachev, Asymptotically good quantum and locally testable classical LDPC codes, STOC 2022. https://arxiv.org/abs/2111.03654
N. P. Breuckmann and J. N. Eberhardt, Quantum low-density parity-check codes, PRX Quantum 2, 2021. https://arxiv.org/abs/2103.06309

18 thms2 active usersReviewed

Quantum Information Theoretical Computer Science·Captain: mikedeng1

Learning Stabilizer States by Bell Sampling: Algorithm 1 Identifies an n-Qubit Stabilizer State from 5n+2 Copies, Failing with Probability at Most 2⁻ⁿResearch Paper

Motivation

Determining an unknown quantum state of $n$ qubits to good accuracy requires, in general, a number of copies of the state exponential in $n$ ; this follows from Holevo's theorem. One way around this barrier is to restrict the class of states. Stabilizer states are the natural candidate: they are the states produced from $|0^n\rangle$ by Clifford circuits, they underlie quantum error-correcting codes, measurement-based computation and randomized benchmarking, and there are $2^{\Theta(n^2)}$ of them, so $\Omega(n)$ copies are necessary to identify one.

Timeline.

Aaronson and Gottesman (2008, Identifying stabilizer states, talk, http://pirsa.org/08080052/) described a procedure identifying an unknown stabilizer state from $O(n^2)$ copies with single-copy measurements, and a variant using $O(n)$ copies with measurements collective across all copies.
Low (2009, arXiv:0907.2833) showed that a Clifford unitary can be identified from $O(n^2)$ uses, or $O(n)$ with access to its inverse.
Rocchetto (2017, arXiv:1705.00345) showed that stabilizer states are PAC-learnable efficiently.
Montanaro (2017, arXiv:1707.04012) gave the algorithm of this mission: $O(n)$ copies, collective measurements on at most two copies at a time, failure probability exponentially small in $n$ . Zhao, Pérez-Delgado and Fitzsimons obtained a related $O(n)$ -copy algorithm for graph states independently (arXiv:1510.03742).

Bell sampling became a standard tool after this paper, for instance in stabilizer testing (Gross, Nezami and Walter, arXiv:1712.08628), so a machine-checked version of its analysis is a reusable base.

Setting

A state of $n$ qubits is a vector $\psi:\{0,1\}^n\to\mathbb C$ ; its complex conjugate $\psi^*$ is taken entrywise in the computational basis. The paper uses the four $2\times2$ matrices

\sigma_{00}=\begin{pmatrix}1&0\\0&1\end{pmatrix},\ \sigma_{01}=\begin{pmatrix}0&1\\1&0\end{pmatrix},\ \sigma_{10}=\begin{pmatrix}1&0\\0&-1\end{pmatrix},\ \sigma_{11}=\sigma_{10}\sigma_{01}=\begin{pmatrix}0&1\\-1&0\end{pmatrix},

which are the Pauli matrices up to the factor $-i$ on $\sigma_{11}$ . For a string $s\in\{0,1\}^{2n}$ , $\sigma_s=\sigma_{s_1s_2}\otimes\cdots\otimes\sigma_{s_{2n-1}s_{2n}}$ ; strings are added bitwise, $s\oplus t$ .

The Bell basis of $\mathbb C^4$ is $|\sigma_{00}\rangle=\frac1{\sqrt2}(|00\rangle+|11\rangle)$ , $|\sigma_{01}\rangle=\frac1{\sqrt2}(|01\rangle+|10\rangle)$ , $|\sigma_{10}\rangle=\frac1{\sqrt2}(|00\rangle-|11\rangle)$ , $|\sigma_{11}\rangle=\frac1{\sqrt2}(|01\rangle-|10\rangle)$ . Bell sampling on $2n$ qubits $A_1,\dots,A_n,B_1,\dots,B_n$ measures each pair $A_iB_i$ in the Bell basis and returns a string $r\in\{0,1\}^{2n}$ . On two copies $|\psi\rangle|\psi\rangle$ (first copy on the $A$ 's) the outcome $r$ has probability $p_\psi(r)=|\langle\sigma_r|\,\psi\otimes\psi\rangle|^2$ .

A stabilizer state is $\psi=U|0^n\rangle$ for a Clifford unitary $U$ (a unitary normalising the Pauli group). Its stabilizer set $T(\psi)\subseteq\mathbb F_2^{2n}$ is the set of strings $t$ for which $\psi$ is an eigenvector of $\sigma_t$ , i.e. those $\sigma_t$ that lie in the stabilizer group of $\psi$ up to a phase.

Algorithm 1. Bell-sample two fresh copies to get $r_0$ ; repeat $2n$ times to get $r_1,\dots,r_{2n}$ ; find a basis $B$ of $\operatorname{span}\{r_i\oplus r_0\}$ ; for each element of $B$ measure one copy of $\psi$ in the eigenbasis of the corresponding (Hermitian) Pauli matrix $M$ to learn whether $M|\psi\rangle=+|\psi\rangle$ or $-|\psi\rangle$ . It uses $5n+2$ copies.

Formalization targets

Goal: Theorem 1, explicit form

For every $n$ and every $n$ -qubit stabilizer state $\psi$ , with the $2n+1$ Bell samples independent,

\Pr\bigl[\operatorname{span}\{r_i\oplus r_0:1\le i\le 2n\}=T(\psi)\bigr]\ \ge\ 1-2^{-n},

and for every basis $b_1,\dots,b_n$ of $T(\psi)$ with Hermitian Paulis $M_j$ , each $M_j\psi=\pm\psi$ and every vector with the same eigenvalues under all $M_j$ is a scalar multiple of $\psi$ . Together: Algorithm 1 identifies $\psi$ except with probability at most $2^{-n}$ .

Milestones

$\sigma_s\sigma_t=\pm\sigma_{s\oplus t}$ .
Lemma 2: $p_\psi(r)=|\langle\psi|\sigma_r|\psi^*\rangle|^2/2^n$ .
The Bell-sampling probabilities of a unit vector sum to $1$ .
For a stabilizer state, $|\psi^*\rangle=c\,\sigma_{10}^{\otimes S}|\psi\rangle$ with $|c|=1$ .
Eqn (1): $p_\psi(r)=|\langle\psi|\sigma_r\sigma_{10}^{\otimes S}|\psi\rangle|^2/2^n$ .
$T(\psi)$ is an $n$ -dimensional subspace of $\mathbb F_2^{2n}$ .
$\langle\psi|\sigma_t|\psi\rangle=0$ for $t\notin T(\psi)$ .
$p_\psi$ is uniform on a coset $\{t\oplus s:t\in T\}$ .
For two independent outcomes, $r_1\oplus r_2$ is uniform on $T$ .
$T$ and the signs on a basis of $T$ determine $\psi$ up to a scalar.
$2n$ uniform samples of an $n$ -dimensional $\mathbb F_2$ -space fail to span it with probability at most $2^{-n}$ .

Significance

The theorem gives a learning algorithm whose copy complexity $O(n)$ is optimal and whose measurements are simple: one Bell measurement on corresponding qubits of two copies. Its analysis isolates a structural fact about stabilizer states, that Bell sampling on two copies produces a uniformly random element of a coset of the stabilizer subspace, which is the engine of later work on stabilizer testing and on learning states with few non-Clifford gates.

The result is proved in the paper; no machine-checked proof of it is known. A complete formalization adds: the stabilizer formalism in a form usable from the definition " $U|0^n\rangle$ for a Clifford $U$ " (the subspace $T$ , its dimension, vanishing expectations off $T$ , determination by signs); the conjugation identity, which the paper takes from a normal form cited from the literature; and the probabilistic bookkeeping of the algorithm with its exact constants.

Difficulty

The probability calculations (Lemma 2, eqn (1), the union bound) are finite sums. The difficulty lies in the stabilizer structure. The platform's definition of a stabilizer state is the image of $|0^n\rangle$ under a Clifford unitary; from it one must derive that the strings whose $\sigma_t$ fixes $\psi$ up to phase form an $n$ -dimensional subspace, that all other Pauli expectations vanish, and that $\psi^*$ differs from $\psi$ by a diagonal Pauli. The paper obtains the last fact from the Dehaene–De Moor normal form $\psi\propto\sum_{x\in A}i^{\ell(x)}(-1)^{q(x)}|x\rangle$ , a cited theorem whose proof is not on the page; formalizing either that normal form or a direct substitute is the central step. The natural shortcut, treating $T$ as given with "uniform outcomes on $T$ " as a hypothesis, proves only the counting lemma and is ruled out below.

Formalization scope

States are StabilizerRank.QState n = (Fin n → Bool) → ℂ and stabilizer states are StabilizerRank.IsStabilizerState (published platform definition, referenced). Qubit $i$ is coordinate $i$ , false $=0$ .
Strings $\{0,1\}^{2n}$ are encoded as Fin n → ZMod 2 × ZMod 2, coordinate $i$ the pair $(s_{2i-1},s_{2i})$ of qubit $i$ ; $\oplus$ is +.
$\sigma_{11}$ is the page's $\begin{pmatrix}0&1\\-1&0\end{pmatrix}$ , not the Pauli $Y$ . The "corresponding Pauli matrix" of step 5 is the Hermitian $(-i)^{\#\{i:t_i=11\}}\sigma_t$ ; the page does not fix this phase.
The Bell outcome law is the Born rule with $\psi(x)\psi(y)$ the amplitude of $|\psi\rangle|\psi\rangle$ at $|x\rangle_A|y\rangle_B$ .
Algorithm 1 is modelled by its outcome law: the $2n+1$ samples are independent (fresh copies), and an event has probability $\sum \mathbf 1_E\,p_\psi(r_0)\prod_i p_\psi(r_i)$ . Step 5 is deterministic once a basis of $T$ is known, and is stated as a property of every such basis.
The explicit constants of p. 2 replace " $O(n)$ " and "exponentially small": $2n+1$ Bell samples, success probability at least $1-2^{-n}$ (the page's "fails with probability at most $2^{-n}$ ", in a form that a mis-normalised outcome law cannot satisfy). The count $5n+2$ and "at most two copies at a time" are properties of the model, not separate clauses. The running time $O(n^3)$ is not formalized.
Lemma 2 is stated for every vector, not only unit vectors (the identity is homogeneous). The conjugation identity carries a unit phase $c$ , which the page omits. " $\langle\psi|M|\psi\rangle=0$ for $M\notin G$ " is stated for strings outside $T$ .
Ruled out: $T$ as a hypothesis (it is always computed from $\psi$ ), dropping the reference sample $r_0$ or the independence of the samples, a degenerate outcome law, and reading "identifies" as "the samples span $T$ " without the sign step.

Needed infrastructure: Kronecker-product manipulations of $\sigma_s$ indexed by bit strings, the Bell basis as an orthonormal basis of $(\mathbb C^2\otimes\mathbb C^2)^{\otimes n}$ , the stabilizer formalism over $\mathbb F_2^{2n}$ , and counting hyperplanes of finite $\mathbb F_2$ -spaces. The stabilizer-formalism layer and the union bound are reusable beyond this mission. Contributions to any milestone are welcome, in particular direct proofs of milestones 4, 6 and 7 from the Clifford definition.

Selected references

A. S. Holevo, Bounds for the quantity of information transmitted by a quantum communication channel, Problems of Information Transmission 9:177–183, 1973.
D. Gross, S. Nezami and M. Walter, Schur–Weyl duality for the Clifford group with applications: property testing, a robust Hudson theorem, and de Finetti representations, Comm. Math. Phys. 385:1325–1393, 2021. https://arxiv.org/abs/1712.08628
A. Montanaro, Learning stabilizer states by Bell sampling, arXiv preprint, 2017. https://arxiv.org/abs/1707.04012
S. Aaronson and D. Gottesman, Identifying stabilizer states, PIRSA talk, 2008. http://pirsa.org/08080052/
R. Low, Learning and testing algorithms for the Clifford group, Phys. Rev. A 80:052314, 2009. https://arxiv.org/abs/0907.2833
A. Rocchetto, Stabiliser states are efficiently PAC-learnable, arXiv preprint, 2017. https://arxiv.org/abs/1705.00345
L. Zhao, C. Pérez-Delgado and J. Fitzsimons, Fast graph operations in quantum computation, Phys. Rev. A 93:032314, 2016. https://arxiv.org/abs/1510.03742
J. Dehaene and B. De Moor, Clifford group, stabilizer states, and linear and quadratic operations over GF(2), Phys. Rev. A 68:042318, 2003. https://arxiv.org/abs/quant-ph/0304125
M. Van den Nest, Classical simulation of quantum computation, the Gottesman–Knill theorem, and slightly beyond, Quantum Inf. Comput. 10:258, 2010. https://arxiv.org/abs/0811.0898
S. Aaronson, The learnability of quantum states, Proc. R. Soc. A 463:3089, 2007. https://arxiv.org/abs/quant-ph/0608142

14 thms2 active usersReviewed

Completed

Statistics·Captain: Lucas

Local Distance Network (H0DN 2026): generalized least squares behind the H0 consensusResearch Paper

Motivation

The Hubble constant $H_0$ is the present expansion rate of the Universe. Its value measured locally with distance-ladder methods disagrees with the value inferred from the early Universe under the standard $\Lambda$ CDM model (the Hubble tension). The H0DN Collaboration (A&A 708, A166, 2026) combined geometric distances, Cepheids, the tip of the red giant branch, Miras, carbon stars, Type Ia and Type II supernovae, surface brightness fluctuations, the fundamental plane, Tully–Fisher relations and megamasers into a single Local Distance Network, reporting the baseline value $H_0=73.50\pm0.81\ \mathrm{km\,s^{-1}\,Mpc^{-1}}$ .

That number comes from one statistical step. All equations of the network are linear (or linearized) in the parameters, the measurement errors are correlated, and the parameters are obtained by generalized least squares with a non-diagonal covariance matrix (Appendix B of the paper). The paper relies on three mathematical facts: the covariance-weighted solution is the Best Linear Unbiased Estimator (Aitken 1935); weighting by the inverse covariance gives the lowest variance among weighted least-squares solutions; and replacing the inverse of a singular covariance matrix by its Moore–Penrose inverse (Penrose 1956) is "completely equivalent to analytically making sure that only linearly independent equations are used". This mission formalizes exactly those facts.

Timeline of the mathematics used:

Gauss (1820s): least squares gives minimum-variance linear unbiased estimates for uncorrelated errors of equal variance.
Aitken (1935): extension to correlated errors with a known covariance matrix, i.e. generalized least squares.
Penrose (1955–1956): the generalized inverse characterized by the four Penrose equations, and its use for best approximate solutions of linear equations.

Setting

The data vector $Y\in\mathbb R^{m}$ has one entry per equation of the network (host-distance, host-group, calibrator and Hubble-flow equations; $m=255$ in the baseline). The parameter vector $X\in\mathbb R^{n}$ collects host distance moduli, group distance moduli, reference absolute magnitudes and $\log_{10}H_0$ . The coefficient matrix $A\in\mathbb R^{m\times n}$ gives the theory prediction $AX$ , and the data have covariance matrix $C\in\mathbb R^{m\times m}$ .

For a symmetric positive-definite weight matrix $W$ the quadratic form of Eq. (B.2) is

Q(X)=(Y-AX)^{\mathsf T}W(Y-AX),

and $W=C^{-1}$ gives the $\chi^2$ of Eq. (B.1). When $A$ has full column rank, the GLS estimator matrix is $L_W=(A^{\mathsf T}WA)^{-1}A^{\mathsf T}W$ and the GLS estimate is $\hat X_W=L_WY$ . A linear estimator $LY$ has covariance $LCL^{\mathsf T}$ . A matrix $P$ is a Moore–Penrose inverse of $M$ if $MPM=M$ , $PMP=P$ , and $MP$ and $PM$ are symmetric.

In the network the $m$ equations are built from only $k$ distinct measurements ( $k=183$ in the baseline): $Y=BZ$ with $Z\in\mathbb R^{k}$ the vector of distinct measurements, of positive-definite covariance $S$ , and $B$ of full column rank. Then $C=BSB^{\mathsf T}$ is singular whenever $m>k$ .

Formalization targets

Goal: the $\chi^2$ solution is BLUE

For $Y=AX_0+\varepsilon$ with $\mathbb E\varepsilon=0$ , $\operatorname{Cov}(\varepsilon)=C\succ0$ and $A$ of full column rank, the estimate $\hat X=L_{C^{-1}}Y$ is unbiased, and for every $L$ such that $LY$ is unbiased for every true parameter, and every $v\in\mathbb R^n$ ,

\operatorname{Var}(v^{\mathsf T}\hat X)\le\operatorname{Var}(v^{\mathsf T}LY).

Milestones

Eq. (B.2): $\hat X_W$ minimizes $Q$ .
Unbiasedness: $L_WA=I$ .
Parameter covariance: $L_{C^{-1}}CL_{C^{-1}}^{\mathsf T}=(A^{\mathsf T}C^{-1}A)^{-1}$ .
Variance propagation: $\operatorname{Var}(v^{\mathsf T}LY)=v^{\mathsf T}LCL^{\mathsf T}v$ .
Aitken, matrix form: $LA=I\Rightarrow LCL^{\mathsf T}-(A^{\mathsf T}C^{-1}A)^{-1}\succeq0$ .
Optimal weight: $L_WCL_W^{\mathsf T}-L_{C^{-1}}CL_{C^{-1}}^{\mathsf T}\succeq0$ for every $W\succ0$ .
Penrose: the Moore–Penrose inverse exists and is unique.
Appendix B.2: if $Y=BZ$ , $C=BSB^{\mathsf T}$ , $A=BA_0$ and $P$ is a Moore–Penrose inverse of $C$ , then $(Y-AX)^{\mathsf T}P(Y-AX)=(Z-A_0X)^{\mathsf T}S^{-1}(Z-A_0X)$ for all $X$ , and the two GLS estimates coincide.

Numerical claims of the paper

With the tension $T(x,\sigma_x;y,\sigma_y)=|x-y|/\sqrt{\sigma_x^2+\sigma_y^2}$ between independent measurements:

Abstract (2): relative uncertainties $0.809/73.499$ and $0.697/73.994$ (Table 4, V00 and V99) round to $1.1\%$ and $0.9\%$ .
Abstract (6): $T(73.50,0.81;\,67.24,0.35)$ rounds to $7.1$ .
Abstract (6): $T(73.50,0.81;\,68.51,0.58)$ rounds to $5.0$ .
Sect. 5.2.4: $T(73.994,0.697;\,67.24,0.35)$ and $T(73.656,0.713;\,67.24,0.35)$ (Table 4, V99 and V99A) round to $8.7$ and $8.1$ .

Significance

The result itself. These statements are what makes the reported $H_0$ and its error bar meaningful as statistical quantities: the estimate is unbiased, its reported uncertainty is the covariance $(A^{\mathsf T}C^{-1}A)^{-1}$ , no other linear unbiased combination of the same data is more precise, and the pseudoinverse shortcut used in the public code neither adds nor removes information compared with an explicit reduction to independent equations. The same facts underlie every covariance-weighted combination of correlated measurements.

Formalizing it. All of these results are classical and proved in the statistics literature. This mission adds machine-checked versions stated in the form used by the paper, including the pseudoinverse equivalence of Appendix B.2, which the paper states without proof. The astrophysical inputs (data selection, linearization, the numerical value of $H_0$ ) are outside the scope of formal proof.

Difficulty

Each statement is classical, but the formal versions are not one-liners. The goal connects measure-theoretic expectation, variance and covariance with matrix algebra: variances of linear combinations of square-integrable random variables must be expanded through bilinearity of covariance before a Loewner-order inequality applies. The pseudoinverse equivalence fails without the full-column-rank hypothesis on $B$ , and has to handle a singular $C$ for which $C^{-1}$ does not exist. Existence of the Moore–Penrose inverse needs a spectral or rank-factorization argument; it is not available as a ready-made matrix operation.

Formalization scope

Everything is over $\mathbb R$ with arbitrary finite index types. "Full column rank" is stated as injectivity of $X\mapsto AX$ . Positive (semi)definiteness uses Mathlib's Matrix.PosDef / Matrix.PosSemidef, which include symmetry. Mathlib's matrix inverse returns $0$ on singular matrices; every statement that uses $(A^{\mathsf T}WA)^{-1}$ carries hypotheses under which that matrix is invertible. The Moore–Penrose inverse is a predicate (the four Penrose equations), and the uniqueness milestone makes it a well-defined object. The probabilistic goal assumes only mean zero, finite second moments and a given covariance matrix (no Gaussianity). Unbiasedness of the competing estimator is required for every value of the true parameter, which rules out estimators that are unbiased only at one parameter value.

The numerical items check only the arithmetic from the published central values and uncertainties to the quoted significances and percentages; "rounds to $a$ " is stated as $a-0.05\le\cdot<a+0.05$ (or the corresponding percentage interval). They say nothing about whether the inputs are correct.

The shared definitions (quadratic form, GLS estimator, estimator covariance, Moore–Penrose predicate) can be reused for any weighted least-squares development. Contributions are welcome on all milestones, as well as on a reusable construction of the matrix pseudoinverse.

Selected references

H0DN Collaboration (S. Casertano et al.), The Local Distance Network: A community consensus report on the measurement of the Hubble constant at ∼1% precision, A&A 708, A166, 2026. https://doi.org/10.1051/0004-6361/202557993
A. C. Aitken, On least squares and linear combination of observations, Proc. Royal Soc. Edinburgh 55, 42, 1935 (as cited in Appendix B of the paper above).
R. Penrose, On best approximate solutions of linear matrix equations, Math. Proc. Camb. Philos. Soc. 52, 17, 1956 (as cited in Appendix B.2 of the paper above).

15 thms2 active usersReviewed

Completed

Condensed Matter Physics Mathematical Physics Quantum Information+2·Captain: Alien60

Seiberg–Seifnashri–Shao 2024: Non-invertible Kramers–Wannier symmetry on the Ising chainResearch Paper

Motivation

Kramers–Wannier duality was found in 1941 as a map between the high- and low-temperature phases of the two-dimensional Ising model (Kramers–Wannier 1941). In its quantum form it exchanges the transverse field $X_j$ and the nearest-neighbour coupling $Z_{j-1}Z_j$ of the transverse-field Ising chain, and it fixes the critical point. In conformal field theory it is implemented by a topological defect line (Fröhlich–Fuchs–Runkel–Schweigert 2004), the prototypical non-invertible symmetry: its fusion with itself is a sum of operators, not a single invertible one (Shao, TASI lectures 2023).

On a finite periodic chain the duality cannot be a unitary operator, because it maps the $\mathbb Z_2$ -even sector to itself and annihilates the odd sector. Seiberg–Shao 2023 and Seiberg–Seifnashri–Shao 2024 wrote the exact lattice operator $\mathsf D$ on the tensor-product Hilbert space $(\mathbb C^2)^{\otimes L}$ . They showed that its algebra closes only after the lattice translation is included: $\mathsf D^2=(1+\eta)T^{-1}$ . This is a lattice relation that a fusion category does not describe, since the continuum fusion rule $\mathcal N^2=1+\eta$ appears only at low energy. The same identity drives the LSM-type constraint proved in that paper.

Timeline. 1941: Kramers and Wannier find the duality of the 2D Ising model. 2004: Fröhlich, Fuchs, Runkel and Schweigert realise it as a conformal defect. 2016: Aasen–Mong–Fendley construct the lattice defects. 2023–2024: Seiberg, Seifnashri and Shao find the exact operator algebra on the tensor-product Hilbert space, including the translation factor.

Setting

Fix $L\ge1$ qubits on a ring, with site indices in $\mathbb Z/L$ (Fin L with modular arithmetic). A computational-basis state is labelled by a configuration $s=(s_0,\dots,s_{L-1})\in(\mathbb Z/2)^L$ (Config L). Operators are complex $2^L\times2^L$ matrices indexed by configurations (Op L). Write $\operatorname{sgn}(a)=(-1)^a$ .

Pauli operators. $X_j|s\rangle=|s+e_j\rangle$ flips spin $j$ (pauliX), and $Z_j|s\rangle=(-1)^{s_j}|s\rangle$ (pauliZ).
$\mathbb Z_2$ symmetry. $\eta=\prod_j X_j$ flips every spin (eta).
Translation. $T|s\rangle=|s'\rangle$ with $s'_k=s_{k-1}$ (transl), so that $TX_jT^{-1}=X_{j+1}$ .
Kramers–Wannier operator (kwD):

\langle t|\,\mathsf D\,|s\rangle \;=\; 2^{-L/2}\,(-1)^{\sum_{k} t_k\,(s_k+s_{k+1})}.

This explicit formula is the definition used throughout. Relations (1.5) together with $\mathsf D\eta=\mathsf D$ determine $\mathsf D$ up to a scalar, and (1.4) fixes the scalar up to a sign. Every statement below is invariant under $\mathsf D\mapsto-\mathsf D$ , so this is the operator of Seiberg–Seifnashri–Shao in that paper's normalisation (footnote 1). Its equality with their matrix-product presentation (2.64) is not formalised here.

Formalization targets

Goal: the non-invertible fusion rule (eqs. (1.4), (2.65), (F.18))

\mathsf D^2=(1+\eta)\,T^{-1}\qquad\text{for every }L\ge1 .

Milestones

Invertible algebra (eqs. (1.1)–(1.3), (2.10), (2.65)): $\eta^2=1$ , $T\eta=\eta T$ , $T^L=1$ , $TX_jT^{-1}=X_{j+1}$ , $TZ_jT^{-1}=Z_{j+1}$ , $\eta X_j=X_j\eta$ , $\eta Z_j=-Z_j\eta$ .
Duality on $X$ (eq. (1.5)): $\mathsf D X_j=Z_{j-1}Z_j\,\mathsf D$ .
Duality on $ZZ$ (eq. (1.5)): $\mathsf D Z_{j-1}Z_j=X_{j-1}\,\mathsf D$ .
Absorbing $\eta$ (eqs. (1.4), (2.65)): $\mathsf D\eta=\eta\mathsf D=\mathsf D$ .
Translation and adjoint (eq. (2.65), Table 1): $T\mathsf D=\mathsf DT$ and $\mathsf D^\dagger=\mathsf DT$ .
Non-invertibility (§1.1): $\mathsf D$ is not a unit, and $\ker\mathsf D\neq0$ .

Significance

The result. The goal identity is the defining relation of the lattice Kramers–Wannier symmetry. Together with milestones 4–5 it shows that $\mathsf D/\sqrt2$ restricted to the $\eta$ -even sector squares to a translation, so $\mathsf D$ is a square root of $T^{-1}$ there. The paper uses this to derive its LSM-type constraint, and also to show that the lattice symmetry is not a fusion category, because the continuum rule $\mathcal N^2=1+\eta$ only emerges at low energy. Milestones 2–3 are the lattice Kramers–Wannier map on $\mathbb Z_2$ -invariant operators, so $\mathsf D$ commutes with the critical Ising Hamiltonian $H=-\sum_j(Z_{j-1}Z_j+X_j)$ .

Formalizing it. The identities are proved in the physics literature by tensor-network manipulations ((F.14)–(F.18)) and checked numerically, but none of this is machine-checked. This mission produces a reusable Lean setup for qubit chains: Pauli strings on $(\mathbb Z/2)^L$ , $\mathbb Z_2$ and translation symmetries, and an exact non-invertible operator with its full operator algebra for every chain length. No mission on the platform or file in Mathlib currently formalizes a non-invertible lattice symmetry.

Difficulty

Each identity is easy to check for a fixed small $L$ by brute force. The content is that it holds for all $L$ at once, on a $2^L$ -dimensional space. The difficulty is bookkeeping with periodic indices: sums over $(\mathbb Z/2)^L$ of characters $(-1)^{\langle t,\,\cdot\rangle}$ , reindexing $k\mapsto k\pm1$ in Fin L (including $L=1$ , where $k+1=k$ , and $L=2$ , where $k+1=k-1$ ), and the exact normalisation $2^{-L/2}$ , so that the right-hand side carries no stray factor $2^L$ . The goal also involves the matrix inverse $T^{-1}$ , so a proof must establish that $T$ is invertible rather than rely on Lean's junk value.

Formalization scope

Representation. Operators are Matrix (Fin L → ZMod 2) (Fin L → ZMod 2) ℂ; products are matrix products; $T^{-1}$ is Mathlib's matrix inverse (transl L)⁻¹; $\dagger$ is conjTranspose. Every theorem assumes [NeZero L], i.e. $L\ge1$ .
Conventions committed to. $Z_j=(-1)^{s_j}$ on basis states, translation to the right ( $s'_k=s_{k-1}$ ), and $\mathsf D$ normalised by $2^{-L/2}$ as in eqs. (1.4)/(2.65). Other conventions (left translation, unnormalised $\mathsf D$ ) change the statements to $T$ instead of $T^{-1}$ or add a factor $2^L$ ; the conventions here reproduce the paper's equations verbatim.
No trivialisation. kwD is an explicit formula, not a hypothesis. The goal fixes both sides completely, and milestone 1 pins the translation convention against eq. (2.10).
Out of scope. The defect Hamiltonians, the MPO presentation (2.64) itself, the $\mathbb Z_2$ - and duality-twisted operators of §§2.3.3–2.3.4, and the LSM constraint of §4.
Reusable. Pauli operators, translation and $\eta$ on qubit chains; character-sum lemmas over $(\mathbb Z/2)^L$ . Contributions of general Mathlib lemmas on Walsh–Hadamard-type sums are welcome.

Selected references

H. A. Kramers, G. H. Wannier, Statistics of the Two-Dimensional Ferromagnet. Part I, Phys. Rev. 60, 252–262 (1941). doi:10.1103/PhysRev.60.252
J. Fröhlich, J. Fuchs, I. Runkel, C. Schweigert, Kramers–Wannier duality from conformal defects, Phys. Rev. Lett. 93, 070601 (2004). arXiv:cond-mat/0404051
D. Aasen, R. S. K. Mong, P. Fendley, Topological Defects on the Lattice I: The Ising model, J. Phys. A 49, 354001 (2016). arXiv:1601.07185
N. Seiberg, S.-H. Shao, Majorana chain and Ising model – (non-invertible) translations, anomalies, and emanant symmetries, SciPost Phys. 16, 064 (2024). arXiv:2307.02534
S.-H. Shao, What's Done Cannot Be Undone: TASI Lectures on Non-Invertible Symmetries (2023). arXiv:2308.00747
Source: N. Seiberg, S. Seifnashri, S.-H. Shao, Non-invertible symmetries and LSM-type constraints on a tensor product Hilbert space, SciPost Phys. 16, 154 (2024). arXiv:2401.12281

8 thms2 active usersReviewed

Completed

Dynamical Systems·Captain: Lucas

Dynamic Stochastic General Equilibrium I: The Taylor Principle and DeterminacyTextbook

Motivation

Dynamic stochastic general equilibrium (DSGE) models are the standard framework used by central banks and fiscal authorities for policy analysis and forecasting (Wikipedia overview). The models used for monetary-policy analysis are built from three interrelated blocks — demand, supply and a monetary-policy rule — that jointly determine output, inflation and the nominal interest rate. The canonical small-scale instance is the three-equation New Keynesian model (Woodford 2003; Galí 2008; Clarida, Galí and Gertler 1999).

A basic question about such a model is whether it pins down a unique equilibrium path at all. If many bounded paths solve the model, the model makes no definite prediction and expectations can become self-fulfilling. The answer for the three-equation model is the Taylor principle: the interest-rate rule must respond to inflation strongly enough.

Timeline. Blanchard and Kahn (1980) gave the eigenvalue-counting criterion for existence and uniqueness of bounded solutions of linear rational-expectations models. Kydland and Prescott (1982) started the real-business-cycle/DSGE programme. Rotemberg and Woodford (1997) introduced the New Keynesian DSGE framework. Bullard and Mitra (2002) derived the explicit determinacy condition $\kappa(\phi_\pi - 1) + (1-\beta)\phi_y > 0$ for the model with a contemporaneous Taylor rule, presented in textbook form by Galí (2008, Ch. 3).

Setting

Time is discrete, $t = 0, 1, 2, \dots$ . All variables are deviations from the zero-inflation steady state: $y_t$ is the output gap, $\pi_t$ inflation, and $i_t$ the nominal interest rate. The parameters are $\sigma > 0$ (inverse elasticity of intertemporal substitution), $\beta \in (0,1)$ (discount factor), $\kappa > 0$ (slope of the Phillips curve), and the policy coefficients $\phi_\pi, \phi_y \ge 0$ .

A triple of real sequences $(y, \pi, i)$ is an equilibrium if for every $t$

\begin{aligned} y_t &= y_{t+1} - \tfrac{1}{\sigma}(i_t - \pi_{t+1}) && \text{(demand: dynamic IS curve)}\\ \pi_t &= \beta \pi_{t+1} + \kappa y_t && \text{(supply: New Keynesian Phillips curve)}\\ i_t &= \phi_\pi \pi_t + \phi_y y_t && \text{(monetary policy: Taylor rule).} \end{aligned}

The demand equation is the log-linearised consumption Euler equation, which equates marginal utility of consumption today with discounted marginal utility tomorrow. The model is determinate if the zero path is its only equilibrium in which $y$ , $\pi$ and $i$ all stay bounded.

Formalization targets

Goal: the Taylor principle

For $\sigma > 0$ , $0 < \beta < 1$ , $\kappa > 0$ , $\phi_\pi, \phi_y \ge 0$ :

\text{the model is determinate} \iff \kappa(\phi_\pi - 1) + (1 - \beta)\phi_y > 0 .

Milestones

Consumption Euler equation. At an interior optimum of the two-period consumption–saving problem, $u'(c_0) = \beta(1+r)u'(c_1)$ .
State-space form. For $\sigma, \beta \ne 0$ , the model is equivalent to $(y_{t+1}, \pi_{t+1})^\top = M(y_t, \pi_t)^\top$ together with the Taylor rule, for an explicit $2\times2$ matrix $M$ .
Equilibria are parametrised by initial conditions. Each $(y_0, \pi_0)$ determines exactly one equilibrium.
Schur–Cohn test. For real $T$ and $D > 0$ , both roots of $z^2 - Tz + D$ have modulus $> 1$ iff $D > 1$ and $|T| < 1 + D$ .
Blanchard–Kahn lemma. For a real square matrix $M$ , the only bounded solution of $x_{t+1} = Mx_t$ is zero iff every complex eigenvalue of $M$ has modulus $> 1$ .

Significance

The result itself. The Taylor principle is the standard criterion for whether an interest-rate rule yields a well-defined equilibrium in New Keynesian models, and it is the first property checked when a policy rule is proposed. The determinacy region it describes is the starting point for the analysis of optimal policy and of learnability (Bullard and Mitra 2002).

Formalizing it. The result is classical and proved on paper. This mission formalizes the known argument. The mission produces a reusable Lean definition of the basic New Keynesian model, a general lemma on bounded orbits of linear recursions (which applies to any linear rational-expectations model with only forward-looking variables), and a formal Schur–Cohn criterion for real quadratics.

Difficulty

The economic content is elementary, but the obvious argument skips the hardest step. Textbook treatments state "determinacy holds iff both eigenvalues lie outside the unit circle" without proof, and the equivalence between "no nonzero bounded solution" and an eigenvalue condition has to be established for real sequences while the eigenvalues may be complex. In particular the converse direction needs a real bounded solution built from a complex eigenvector, and the boundary case of eigenvalues on the unit circle must come out on the non-determinate side. The parameter translation also has to handle complex-conjugate eigenvalues, not only real ones.

Formalization scope

Sequences are functions $\mathbb N \to \mathbb R$ ; the model is the deterministic (shock-free) version, so there are no expectation operators. Stochastic shocks do not change the determinacy condition, but that extension is outside the scope of this mission.
"Bounded" means a single real bound for all $t$ ; determinacy requires $y$ , $\pi$ and $i$ to be bounded. Boundedness of $i$ follows from that of $y$ and $\pi$ , so this adds no restriction.
Division is Lean's total division; every statement that divides by $\sigma$ or $\beta$ assumes they are nonzero (or positive).
Eigenvalues are complex roots of the characteristic polynomial of the complexified matrix.
The goal is not trivial: the zero path is always an equilibrium, determinacy is a genuine uniqueness claim, and the parameter hypotheses are satisfiable (e.g. $\sigma = 1$ , $\beta = 0.99$ , $\kappa = 0.1$ , $\phi_\pi = 1.5$ , $\phi_y = 0.5$ ).
All declarations live in the namespace DSGE. Contributions of general linear-recursion and polynomial-root lemmas are welcome.

Selected references

Wikipedia, Dynamic stochastic general equilibrium. https://en.wikipedia.org/wiki/Dynamic_stochastic_general_equilibrium
O. J. Blanchard and C. M. Kahn, The Solution of Linear Difference Models under Rational Expectations, Econometrica 48(5), 1980. https://doi.org/10.2307/1912186
F. E. Kydland and E. C. Prescott, Time to Build and Aggregate Fluctuations, Econometrica 50(6), 1982. https://doi.org/10.2307/1913386
R. Clarida, J. Galí and M. Gertler, The Science of Monetary Policy: A New Keynesian Perspective, Journal of Economic Literature 37(4), 1999. https://doi.org/10.1257/jel.37.4.1661
J. Bullard and K. Mitra, Learning about Monetary Policy Rules, Journal of Monetary Economics 49(6), 2002. https://doi.org/10.1016/S0304-3932(02)00144-7
M. Woodford, Interest and Prices: Foundations of a Theory of Monetary Policy, Princeton University Press, 2003.
J. Galí, Monetary Policy, Inflation, and the Business Cycle, Princeton University Press, 2008 (Chapter 3).

7 thms2 active usersReviewed

Control Theory Convex Optimization Optimization·Captain: mikedeng1

Quadratic Matrix Inequalities with Applications to Data-Based Control V: A Reduced LMI in P Alone and an Explicit Data-Based Stabilizing GainResearch Paper

Motivation

Data-driven control asks for a controller computed directly from measured trajectories of an unknown system, without first identifying a model. When the measurements are corrupted by noise, many systems explain the same data, and a controller is acceptable only if it works for all of them. Van Waarde, Camlibel, Eising and Trentelman (arXiv:2203.12959) model the noise by a quadratic matrix inequality (QMI). The set of systems consistent with the data is then itself the solution set of a QMI, and the design question becomes whether one QMI implies another. Their Theorem 5.1 gives a necessary and sufficient linear matrix inequality (LMI) for the existence of a common stabilizing controller, with no rank or Slater-type assumption on the data. It improves van Waarde, Camlibel, Mesbahi, IEEE TAC 2022, Thm. 14, which needed a generalized Slater condition.

The LMI of Theorem 5.1 has size $4n+m+1$ and $\tfrac{n(n+1)}{2}+nm+1$ unknowns. Section 5.2 of the paper removes the controller variable: Theorem 5.3 gives an LMI of size $4n+1$ in the Lyapunov matrix $P$ and one scalar $\beta$ , and then writes a stabilizing controller as a closed-form expression in $P$ and the data. This mission formalizes that reduction and the Section 3 results on QMI solution sets that it rests on.

Setting

All matrices are real. $\mathbb S^k$ is the set of symmetric $k\times k$ matrices, $A\ge 0$ ( $A>0$ ) means symmetric positive semidefinite (definite), and $A^\dagger$ is the Moore–Penrose pseudo-inverse. For $\Pi\in\mathbb S^{q+r}$ , partitioned with $\Pi_{11}$ of size $q\times q$ and $\Pi_{22}$ of size $r\times r$ ,

\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}\ge 0\Big\},

and $\mathcal Z_r^+(\Pi)$ is the same set with $>0$ . The generalized Schur complement is $\Pi\,|\,\Pi_{22} = \Pi_{11}-\Pi_{12}\Pi_{22}^\dagger\Pi_{21}$ , and $\boldsymbol\Pi_{q,r}$ is the class of $\Pi\in\mathbb S^{q+r}$ with $\Pi_{22}\le 0$ , $\Pi\,|\,\Pi_{22}\ge 0$ and $\ker\Pi_{22}\subseteq\ker\Pi_{12}$ . For $W\in\mathbb R^{q\times p}$ , $\mathcal Z_r(\Pi)W = \{ZW : Z\in\mathcal Z_r(\Pi)\}$ and $\Pi_W = \mathrm{diag}(W,I_r)^\top\,\Pi\,\mathrm{diag}(W,I_r)$ .

Data. An unknown system $x(t+1) = A_sx(t)+B_su(t)+w(t)$ produces $X = [x(0)\cdots x(T)]$ and $U_- = [u(0)\cdots u(T-1)]$ ; $X_-$ and $X_+$ are the first and last $T$ columns of $X$ . The noise matrix $W_- = [w(0)\cdots w(T-1)]$ is unknown but satisfies $W_-^\top\in\mathcal Z_T(\Phi)$ for a given $\Phi\in\boldsymbol\Pi_{n,T}$ . The consistent systems are

\Sigma = \{(A,B) : X_+ = AX_-+BU_-+W_-\ \text{for some}\ W_-^\top\in\mathcal Z_T(\Phi)\}.

The data are informative for quadratic stabilization if there are $K$ and $P>0$ with $P-(A+BK)P(A+BK)^\top>0$ for all $(A,B)\in\Sigma$ .

Formalization targets

Goal: Theorem 5.3

With $\Theta = \Phi_{12}+X_+\Phi_{22}$ and $V = [X_-;\,U_-]$ : the data are informative if and only if some $P>0$ , $\beta>0$ satisfy

P-\beta I-[I\ X_+]\Phi[I\ X_+]^\top+\Theta V^\top(V\Phi_{22}V^\top)^\dagger V\Theta^\top\ge 0,\qquad \begin{bmatrix}P-\beta I&0\\0&-P\end{bmatrix}-\begin{bmatrix}I&X_+\\0&-X_-\end{bmatrix}\Phi\begin{bmatrix}I&X_+\\0&-X_-\end{bmatrix}^\top\ge 0,

and then

K = \big(U_-(\Phi_{22}+\Theta^\top\Gamma^\dagger\Theta)X_-^\top\big)\big(X_-(\Phi_{22}+\Theta^\top\Gamma^\dagger\Theta)X_-^\top\big)^\dagger,\qquad \Gamma = P-\beta I-[I\ X_+]\Phi[I\ X_+]^\top,

stabilizes every $(A,B)\in\Sigma$ . Under $\Phi_{22}<0$ and $\operatorname{rank}V = n+m$ the same holds with strict inequalities, $\beta = 0$ , and $(V\Phi_{22}V^\top)^{-1}$ . The goal states all four parts.

Milestones

Lemma A.1: $A^\top A\le B^\top B$ iff $A = SB$ with $S^\top S\le I$ (and the strict version), with $S = AB^\dagger$ .
Lemma A.2: the solutions of $AM = B$ .
Theorem 3.3: all solutions of a QMI, $Z = -\Pi_{22}^\dagger\Pi_{21}+((-\Pi_{22})^\dagger)^{1/2}S(\Pi|\Pi_{22})^{1/2}+(I-\Pi_{22}^\dagger\Pi_{22})T$ .
Theorems 3.4 and 3.5: $\mathcal Z_r(\Pi)W = \mathcal Z_r(\Pi_W)$ and its strict analogue.
Corollaries 3.6 and 3.7: a QMI solution with $ZW = Y$ exists iff $Y\in\mathcal Z_r(\Pi_W)$ .
Theorem 5.1: informativity iff the LMI in $(P,L,\beta)$ is feasible, with $K = LP^{-1}$ .

Significance

Theorem 5.3 separates the computation of a Lyapunov matrix from the computation of the controller. The LMI drops from size $4n+m+1$ to $4n+1$ and loses the $nm$ entries of $L$ . A controller then follows from $P$ by one explicit formula, with no second optimization. The noise class $\boldsymbol\Pi_{n,T}$ covers energy bounds, bounds on individual samples, noise confined to a known subspace, and exact data, so the result applies where earlier conditions requiring $\Phi_{22}<0$ or a Slater point fail.

The Section 3 results are general facts about QMIs: an explicit parameterization of all solutions, also when the solution set is unbounded, and the identification of the image of a solution set under a linear map. They are reusable wherever QMIs appear in robust control: Petersen's lemma, the elimination lemma, dissipativity analysis.

All results are proved in the paper, with the exception of the proof of Theorem 3.5, which is only described as similar to that of Theorem 3.4. None is formalized. The work here is the formal development: a pseudo-inverse calculus for real matrices, generalized Schur complements, matrix square roots in the Loewner order, and the block-matrix identities of Section 5.

Difficulty

The QMI reformulation of the stabilization problem is short. The difficulty lies in degenerate matrices. $\Pi_{22}$ is typically singular, so every step works with pseudo-inverses, kernel inclusions and generalized Schur complements, and identities that are routine for invertible blocks need range conditions. The closed-form gain (5.10) comes from a block pseudo-inverse formula for a positive semidefinite matrix whose blocks may all be singular, and checking it requires tracking which ranges contain which. The strict statements need a separate argument: a strict inequality $A^\top A<B^\top B$ does not pass to $W^\top A^\top AW<W^\top B^\top BW$ without full column rank of $W$ , which is why Theorem 3.5 and Corollary 3.7 assume it.

The first idea, to eliminate $L$ from (5.5) by completing the square, runs into the same singular blocks: the minimizing $L$ involves pseudo-inverses of data-dependent matrices whose ranges are not controlled by the LMI alone.

Formalization scope

Lean conventions:

Index sets are arbitrary finite types, so $q$ , $r$ , $p$ are cardinalities. The data dimensions $n$ , $m$ , $T$ are natural numbers, with $X$ an $n\times(T+1)$ matrix.
$A\ge 0$ is Mathlib's PosSemidef (which includes symmetry); $A>0$ is PosDef.
$A^\dagger$ is defined as the matrix satisfying the four Penrose conditions, which exists and is unique. Mathlib's A⁻¹, which returns $0$ on singular matrices, appears only in (5.11a) and in $K = LP^{-1}$ , where the matrices are invertible.
Square roots are CFC.sqrt in the Loewner order. Kernel inclusions are stated on vectors. Full column rank of $W\in\mathbb R^{q\times p}$ is rank W = p.

The statements of Theorems 5.1 and 5.3 carry the hypothesis that the data were generated by some $(A_s,B_s)$ , i.e. $\Sigma\neq\emptyset$ ; the paper assumes this when it says the data are generated by (2.1) with noise model (2.3). Without it, informativity holds vacuously and the equivalences fail. "Stabilizing gain" is asserted with the $P$ of the LMI: the Lyapunov inequality $P-(A+BK)P(A+BK)^\top>0$ and $(A+BK)^k\to 0$ for every $(A,B)\in\Sigma$ . Corollaries 3.6 and 3.7 print the hypothesis $\ker\Pi_{22}\subseteq\ker\Pi_{21}$ , which is dimensionally impossible; it is read as $\ker\Pi_{22}\subseteq\ker\Pi_{12}$ . The printed dimensions in Lemma A.2 are corrected to those its formula requires.

A formalization in which Σ may be empty, or in which $A^\dagger$ is replaced by the total inverse, would make the goal vacuous or false. Both are ruled out above.

Theorem 5.1 is restated here as a milestone. It is also the goal of the companion mission IV, and solvers may prove it there.

Reusable infrastructure is welcome as separate contributions: uniqueness and the basic identities of the matrix pseudo-inverse; the generalized Schur complement criterion for positive semidefiniteness of a block matrix; Douglas-type factorization (Lemma A.1); square roots of positive semidefinite matrices commuting with pseudo-inverses.

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 (the version cited here). https://arxiv.org/abs/2203.12959
H. J. van Waarde, M. K. Camlibel, M. Mesbahi, From noisy data to feedback controllers: nonconservative design via a matrix S-lemma, IEEE Trans. Automat. Control, 67 (2022), pp. 162–175. https://doi.org/10.1109/TAC.2020.3047577
H. J. van Waarde, J. Eising, H. L. Trentelman, M. K. Camlibel, Data informativity: a new perspective on data-driven analysis and control, IEEE Trans. Automat. Control, 65 (2020), pp. 4753–4768. https://doi.org/10.1109/TAC.2020.2966717
D. S. Bernstein, Matrix Mathematics, 2nd ed., Princeton University Press, 2009. https://doi.org/10.1515/9781400833344

12 thms2 active usersReviewed

Control Theory Convex Optimization Optimization·Captain: mikedeng1

Quadratic Matrix Inequalities with Applications to Data-Based Control II: Matrix Finsler's Lemma — Z⁰ᵣ(N) ⊆ Zᵣ(M) iff M − αN ⪰ 0 for Some α ≥ 0Research Paper

Motivation

Finsler's lemma (P. Finsler, 1937) states that for symmetric matrices $M,N\in\mathbb S^n$ , the quadratic form $x^\top Mx$ is positive on every nonzero $x$ with $x^\top Nx=0$ if and only if $M-\alpha N>0$ for some real $\alpha$ . Together with the S-lemma of Yakubovich it is one of the basic tools for converting a statement about all vectors satisfying a quadratic constraint into a single linear matrix inequality (LMI) in a multiplier, which can then be checked by semidefinite programming. Both results are used throughout robust control, where uncertainty is described by quadratic constraints.

In data-driven control the unknown object is a matrix, not a vector: the system matrices $(A,B)$ consistent with noisy measurements form a set of the form

\mathcal Z_r(N)=\Big\{Z\in\mathbb R^{r\times q}:\begin{bmatrix}I\\ Z\end{bmatrix}^\top N\begin{bmatrix}I\\ Z\end{bmatrix}\geqslant0\Big\},

and a controller has to work for every element of such a set. H. J. van Waarde, M. K. Camlibel, J. Eising and H. L. Trentelman (arXiv:2203.12959, SIAM J. Control Optim. 2023) develop matrix-valued versions of the S-lemma and of Finsler's lemma for exactly this purpose. Their matrix S-lemma (Theorem 4.7) requires a Slater-type condition: $N$ must have a positive eigenvalue. This mission concerns the complementary case in which $N$ has no positive eigenvalue, where the inequality defining $\mathcal Z_r(N)$ degenerates into an equality and a Finsler-type statement is needed.

Setting

All matrices are real. For a symmetric matrix $A$ , $A\geqslant0$ ( $A>0$ ) means positive semidefinite (definite); $A\leqslant0$ means $-A\geqslant0$ . $A^\dagger$ is the Moore–Penrose pseudo-inverse, the unique matrix $X$ with $AXA=A$ , $XAX=X$ and $AX$ , $XA$ symmetric.

Fix integers $q\geqslant1$ and $r\geqslant0$ . A symmetric matrix $M\in\mathbb S^{q+r}$ is partitioned as

M=\begin{bmatrix}M_{11}&M_{12}\\ M_{21}&M_{22}\end{bmatrix},

with $M_{11}$ of size $q\times q$ and $M_{22}$ of size $r\times r$ , and likewise $N$ . For $Z\in\mathbb R^{r\times q}$ write $F_M(Z):=\begin{bmatrix}I\\ Z\end{bmatrix}^\top M\begin{bmatrix}I\\ Z\end{bmatrix}\in\mathbb S^q$ , and define

\mathcal Z_r(M)=\{Z: F_M(Z)\geqslant0\},\qquad \mathcal Z_r^0(N)=\{Z: F_N(Z)=0\}.

The generalized Schur complement is $M\,|\,M_{22}:=M_{11}-M_{12}M_{22}^\dagger M_{21}$ , and the class $\boldsymbol\Pi_{q,r}$ consists of the symmetric $M$ with $M_{22}\leqslant0$ , $M\,|\,M_{22}\geqslant0$ and $\ker M_{22}\subseteq\ker M_{12}$ . For $N\in\boldsymbol\Pi_{q,r}$ , the condition $N\,|\,N_{22}=0$ is equivalent to $N$ having no positive eigenvalue; then $\mathcal Z_r(N)=\mathcal Z_r^0(N)$ . Finally, set

\Theta:=\begin{bmatrix}I\\ -N_{22}^\dagger N_{21}\end{bmatrix}^\top M\begin{bmatrix}I\\ -N_{22}^\dagger N_{21}\end{bmatrix}=F_M(-N_{22}^\dagger N_{21}).\qquad(4.4)

Formalization targets

Goal: Theorem 4.8 (Matrix Finsler's lemma), p. 12

First, if $M-\alpha N\geqslant0$ for some $\alpha\in\mathbb R$ , then $\mathcal Z_r^0(N)\subseteq\mathcal Z_r(M)$ . Second, if $M,N\in\boldsymbol\Pi_{q,r}$ , $N\,|\,N_{22}=0$ and $\ker\Theta\subseteq\ker(M\,|\,M_{22})$ , then

\mathcal Z_r^0(N)\subseteq\mathcal Z_r(M)\iff\exists\,\alpha\geqslant0:\ M-\alpha N\geqslant0 .

Milestones (proof of Theorem 4.8, pp. 12–13)

If $\mathcal Z_r^0(N)\subseteq\mathcal Z_r(M)$ , then $\ker N_{22}\subseteq\ker M_{22}$ .
With $T:=\begin{bmatrix}I&0\\ -N_{22}^\dagger N_{21}&I\end{bmatrix}$ , $T^\top NT=\operatorname{diag}(0,N_{22})$ and

T^\top(M-\alpha N)T=\begin{bmatrix}\Theta&M_{12}-N_{12}N_{22}^\dagger M_{22}\\ M_{21}-M_{22}N_{22}^\dagger N_{21}&M_{22}-\alpha N_{22}\end{bmatrix}.\qquad(4.6)

If $\ker M_{22}\subseteq\ker M_{12}$ , then with $D:=M_{22}^\dagger M_{21}-N_{22}^\dagger N_{21}$ , $\Theta=M\,|\,M_{22}+D^\top M_{22}D$ and $M_{22}D=M_{21}-M_{22}N_{22}^\dagger N_{21}$ (4.7a–b).
$\Theta\geqslant0$ and $\ker(M\,|\,M_{22})=\ker\Theta\cap\ker(M_{21}-M_{22}N_{22}^\dagger N_{21})$ .
$T^\top(M-\alpha N)T\geqslant0$ if and only if

M_{22}-\alpha N_{22}-(M_{21}-M_{22}N_{22}^\dagger N_{21})\,\Theta^\dagger\,(M_{12}-N_{12}N_{22}^\dagger M_{22})\geqslant0.\qquad(4.8)

Some $\alpha\geqslant0$ satisfies (4.8), and then $M-\alpha N\geqslant0$ .

A companion item formalizes Example 4.9 (p. 13): for $N=\begin{bmatrix}-1&1\\1&-1\end{bmatrix}$ and $M=\begin{bmatrix}1&0\\0&-1\end{bmatrix}$ all hypotheses except the one on $\Theta$ hold, the inclusion holds, and no $\alpha\geqslant0$ works.

Significance

The theorem turns an inclusion between two sets of matrices, a statement quantified over infinitely many $Z$ , into feasibility of a scalar-multiplier LMI. In the paper it is one of four matrix S-lemma variants (Theorems 4.7, 4.8, 4.10, 4.11) that together cover the cases arising in data-based control: whether the data-consistent set $\mathcal Z_r(N)$ has a Slater point, and whether the conclusion is non-strict or strict. Theorem 4.8 is the variant for noise models whose quadratic description has no interior, for instance exact equality constraints on the noise. Example 4.9 shows that the kernel hypothesis on $\Theta$ is genuinely needed, so the statement marks the boundary of when the lossless reduction holds.

The paper gives a complete proof. No machine-checked proof of this theorem, of the matrix S-lemma, or of Finsler's lemma in matrix form is known to exist, in Lean or elsewhere. Formalizing it produces reusable infrastructure: the Moore–Penrose pseudo-inverse of real matrices with its Penrose identities, the generalized Schur complement criterion for positive semidefiniteness of a block matrix, and congruence manipulations of $2\times2$ block matrices, none of which is currently in Mathlib in this form.

Difficulty

The "if" direction is a one-line computation. For the "only if" direction the classical vector Finsler lemma is not directly applicable: it concerns vectors $x$ with $x^\top Nx=0$ , while the hypothesis here only controls matrices $Z$ with $F_N(Z)=0$ , which is a much smaller family when $q>1$ , and the conclusion is non-strict. The natural first idea, applying the vector S-lemma, fails because $N$ has no positive eigenvalue, so its Slater condition is violated. Instead one must exploit the structure of $\boldsymbol\Pi_{q,r}$ : the pseudo-inverse appears because $N_{22}$ and $M_{22}$ are typically singular, and every manipulation must track kernels and ranges exactly.

Formalization scope

The blocks are indexed by arbitrary finite types ι (size $q$ ) and κ (size $r$ ); a matrix in $\mathbb S^{q+r}$ is Matrix (ι ⊕ κ) (ι ⊕ κ) ℝ, its blocks are toBlocks₁₁ etc., and $\mathbb R^{r\times q}$ is Matrix κ ι ℝ. $A\geqslant0$ is Mathlib's PosSemidef, which includes symmetry. The pseudo-inverse is defined by Hilbert's choice among matrices satisfying the four Penrose conditions; since such a matrix exists and is unique, this is the pseudo-inverse and not a junk value. Kernel inclusions are stated with matrix–vector products.

One hypothesis is added and disclosed: $q\geqslant1$ (Nonempty ι) in the second statement of Theorem 4.8 and in the milestones that need it. The proof picks a nonzero vector of $\mathbb R^q$ , and at $q=0$ the equivalence is false ( $r=1$ , $N=[0]$ , $M=[-1]$ ). The first statement keeps a real multiplier of any sign; the second requires $\alpha\geqslant0$ , as printed. The hypothesis $N\,|\,N_{22}=0$ together with $N\in\boldsymbol\Pi_{q,r}$ makes $\mathcal Z_r^0(N)$ nonempty, so the inclusion is never vacuous; a formalization in which $\mathcal Z_r^0(N)$ could be empty, or in which $N_{22}^\dagger$ were replaced by the inverse (which is $0$ on singular blocks in Lean), would not be this theorem.

Needed infrastructure: existence and uniqueness of the Moore–Penrose pseudo-inverse (needed to work with the definition at all), symmetry of $A^\dagger$ for symmetric $A$ , the generalized Schur complement criterion for $\begin{bmatrix}A&B\\B^\top&C\end{bmatrix}\geqslant0$ , and positive semidefiniteness under congruence by an invertible matrix. These lemmas are reusable beyond this mission and contributions of them are welcome, as are proofs of the companion Example 4.9.

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
P. Finsler, Über das Vorkommen definiter und semidefiniter Formen in Scharen quadratischer Formen, Comment. Math. Helv. 9 (1937), 188–192. https://doi.org/10.1007/BF01258188
I. Pólik, T. Terlaky, A survey of the S-lemma, SIAM Review 49 (2007), 371–418. https://doi.org/10.1137/S003614450444614X
H. J. van Waarde, J. Eising, H. L. Trentelman, M. K. Camlibel, Data informativity: a new perspective on data-driven analysis and control, IEEE Trans. Automat. Control 65 (2020), 4753–4768. https://doi.org/10.1109/TAC.2020.2966717

9 thms2 active usersReviewed

Completed

Combinatorics Graph Theory·Captain: mikedeng1

Three Conjectures in Extremal Spectral Graph Theory 2: For Large n, K₂ + Pₙ₋₂ Is the Unique Planar Graph on n Vertices of Maximum Spectral Radius (Boots–Royle / Cao–Vince Conjecture)Research Paper

Motivation

The spectral radius of a graph, the largest eigenvalue of its adjacency matrix, measures how densely and how unevenly the edges of the graph are distributed. Asking which graph in a class maximizes it is a spectral analogue of the extremal question "which graph in the class has the most edges". For planar graphs the question has a long history in spectral graph theory, going back at least to Schwenk and Wilson. It also arose in geography, where the spectral radius serves as a measure of the connectivity of planar networks. To compare real networks with a theoretical upper bound, geographers wanted the planar graph of maximum spectral radius (arXiv:1606.01916v2, p. 3).

Timeline, as recorded by Tait and Tobin (pp. 1–3):

1978, Schwenk and Wilson: early study of the eigenvalues of planar graphs.
1991, Boots and Royle, and independently 1993, Cao and Vince: conjecture that the planar graph on $n \ge 9$ vertices of maximum spectral radius is $P_2 + P_{n-2}$ (Conjecture 1 of the paper). The conjecture is false for $n \in \{7, 8\}$ , so some lower bound on $n$ is necessary (p. 2).
1988–2000: successive improvements of the upper bound on the spectral radius of planar graphs, by Hong (1988, 1995, 1998), Cao and Vince (1993), Guiduli (1996) and Ellingham and Zha (2000). These bounds do not identify the extremal graph.
2010, Dvořák and Mohar: an upper bound on the spectral radius of planar graphs of given maximum degree.
Guiduli and Hayes were reported by Ellingham and Zha to have proved the conjecture for large $n$ . The preprint never appeared (p. 3).
2017, Tait and Tobin: proof of the conjecture for all sufficiently large $n$ (Theorem 15).

Setting

All graphs are finite and simple. A graph on $n$ vertices has vertex set $\{0, 1, \dots, n-1\}$ . Its adjacency matrix $A(G)$ is the $n \times n$ real matrix with entry $1$ in position $(u, w)$ when $u \sim w$ and $0$ otherwise. Its eigenvalues are real, and the largest is the spectral radius $\lambda_1(G)$ .

A graph is planar if it can be drawn in the plane with vertices as distinct points and edges as simple arcs joining their ends, such that an arc meets no vertex other than its ends and two arcs meet only at common ends.

For graphs $G$ and $H$ on disjoint vertex sets, the join $G + H$ is the graph on the union of the two vertex sets that keeps every edge of $G$ and of $H$ and adds every edge between a vertex of $G$ and a vertex of $H$ . Write $K_2$ for a single edge, $P_m$ for the path on $m$ vertices, and $K_2 + P_{n-2}$ for their join: two adjacent vertices, both joined to every vertex of a path on the remaining $n - 2$ vertices. The paper also writes it $P_2 + P_{n-2}$ .

A planar graph $G$ on $n$ vertices is a planar spectral maximizer if $\lambda_1(G') \le \lambda_1(G)$ for every planar graph $G'$ on the same $n$ vertices.

The milestones refer to a leading eigenvector $\mathbf v$ of a maximizer, scaled so that every entry is positive and the largest entry is $1$ , and to a vertex $x$ with $\mathbf v_x = 1$ . For a parameter $\varepsilon > 0$ they use the sets $L = \{z : \mathbf v_z > \varepsilon\}$ and $S = V(G) \setminus L$ , the edge counts $e(X)$ (edges inside $X$ ) and $e(X, Y)$ (edges between $X$ and $Y$ ), and a second vertex $w$ with $\mathbf v_w > 1 - 24\varepsilon$ that is adjacent to all but $94\varepsilon n$ vertices of $S$ .

Formalization targets

Goal: Theorem 15

\exists N_0\ \forall n \ge N_0\ \forall G \text{ on } n \text{ vertices}: \quad G \text{ is a planar spectral maximizer} \iff G \cong K_2 + P_{n-2}.

The threshold $N_0$ is not fixed. The paper proves the statement only for $n$ beyond an unspecified bound, and the conjecture's bound $n \ge 9$ remains open. The equivalence encodes "the unique maximizer is $K_2 + P_{n-2}$ ": every maximizer is isomorphic to it, and it is itself a maximizer.

Milestones, in the order of the proof

If $H$ is a proper spanning subgraph of a connected graph $G$ , then $\lambda_1(H) < \lambda_1(G)$ (§1.2, already proved on the platform).
A planar graph on $n \ge 3$ vertices has no $K_{3,3}$ subgraph and at most $3n - 6$ edges, and each of its bipartite subgraphs has at most $2n - 4$ edges (p. 8).
Lemma 8: $\sqrt{2n-4} < \lambda_1 < \sqrt{6n}$ .
The counts $|L| \le 3\sqrt{2n-4}/\varepsilon$ , $e(S, L) \le 2n - 4$ , $e(S) \le 3n - 6$ , $e(L) \le 9\sqrt{2n-4}/\varepsilon$ (p. 8).
Lemma 9: $\sum_{z \in L} \mathbf v_z \le \varepsilon\sqrt{2n-4} + 18/\varepsilon$ and $\sum_{z \in S} \mathbf v_z \le (1 + 3\varepsilon)\sqrt{2n-4}$ .
Eq. (7): $\sum_{y \sim u,\, y \in S} \mathbf v_y \ge (\mathbf v_u - \varepsilon)\sqrt{2n-4} - 18/\varepsilon$ for $u \in L$ .
Lemma 10: $\mathbf v_z > 1/\sqrt{6n}$ for every vertex $z$ .
$|\{y \in S : y \not\sim x\}| \le 14\varepsilon n$ (p. 10).
Lemma 11: a vertex $w \in L$ , $w \ne x$ , with $\mathbf v_w > 1 - 24\varepsilon$ and $|\{y \in S : y \not\sim w\}| \le 94\varepsilon n$ .
Lemma 12: $\mathbf v_u < 1/10$ for every $u \notin \{x, w\}$ .
Lemma 13: $x \sim w$ .
Lemma 14: every vertex other than $x$ and $w$ is adjacent to both.
A planar graph with two distinct vertices adjacent to all other vertices is a spanning subgraph of $K_2 + P_{n-2}$ (proof of Theorem 15, p. 13).

Significance

The result. Theorem 15 settles the Boots–Royle / Cao–Vince conjecture for all large $n$ . It identifies the planar graph of maximum spectral radius exactly, so the theoretical upper bound that the geographic application asks for is $\lambda_1(K_2 + P_{n-2})$ . Along the way, Lemmas 8–14 describe the eigenvector of the extremal graph: two vertices carry almost all of the eigenvector weight, and every other entry is below $1/10$ . The same method proves the outerplanar analogue (Theorem 7, the companion mission of this series).

Formalizing it. The theorem is proved on paper and has no machine-checked proof. Formalizing it needs several pieces that are absent from Mathlib or the platform and are reusable: the edge bound $3n - 6$ and the bipartite bound $2n - 4$ for topologically planar graphs, the non-planarity of $K_{3,3}$ and $K_5$ and of their subdivisions, Rayleigh-quotient comparison of spectral radii, and the face structure of maximal planar graphs. Each milestone is a self-contained target.

Difficulty

Counting edges does not separate the candidates. A maximizer can be taken to be a maximal planar graph, so it has exactly $3n - 6$ edges. Every maximal planar graph on $n$ vertices has the same number of edges, and the standard lower bound $\lambda_1 \ge 2|E|/n$ is the same for all of them. The extremal graph is pinned down only through its eigenvector. One has to show that the weight concentrates on two vertices, which are then forced to be adjacent to each other (Lemma 13) and to every other vertex (Lemma 14). Lemma 13 is the step specific to planarity. It uses the triangular faces of a maximal planar graph to find an edge switch that keeps the graph planar. In the formal setting, planarity is topological, so every planarity fact of the argument (the edge counts, the $K_{3,3}$ and $K_5$ obstructions, the faces of a triangulation) has to be derived from the drawing.

Formalization scope

Graphs are SimpleGraph (Fin n). " $G$ is $K_2 + P_{n-2}$ " is a graph isomorphism G ≃g bookPath n, where bookPath n lives on Fin 2 ⊕ Fin (n - 2). It is not an equality on a fixed labelling.
$\lambda_1$ is the published WangKangXue.SpectralTuran.specRad, the largest eigenvalue of the real adjacency matrix.
Planarity is the published topological RobertsonSeymour1986.GM5.IsPlanar: a drawing by simple arcs. It is not replaced by $K_5$ / $K_{3,3}$ -minor-freeness or by an edge count, either of which would change the class the maximum ranges over.
Extremality is IsSpecMax IsPlanar G: $G$ is planar and $\lambda_1(G') \le \lambda_1(G)$ for every planar $G'$ on Fin n. Every milestone from Lemma 8 to Lemma 14 assumes it. These lemmas are false for an arbitrary planar graph, so a statement that drops the hypothesis, or replaces it by a property implying the conclusion, is not acceptable.
The eigenvector is universally quantified: every $\mathbf v$ with $A\mathbf v = \lambda_1 \mathbf v$ , all entries positive, all entries at most $1$ , and every $x$ with $\mathbf v_x = 1$ . Such a vector exists because the maximizer is connected (Perron–Frobenius). A statement that only asserts the existence of some eigenvector is weaker and is ruled out.
Quantifiers. "For $n$ sufficiently large" is $\exists N\ \forall n \ge N$ , and $N$ may depend on $\varepsilon$ . Milestones 4–8 hold for every $\varepsilon > 0$ . Lemmas 11–14 hold for $0 < \varepsilon < \varepsilon_0$ with an unspecified $\varepsilon_0$ , because the paper chooses $\varepsilon$ small. The quantifier on $\varepsilon$ is always outermost, so $\varepsilon$ never depends on $n$ or $G$ . Lemmas 12–14 hold for every vertex $w$ satisfying the conclusion of Lemma 11 (the predicate IsSecondHub), with the constants $24$ and $94$ .
Added hypotheses. $n \ge 3$ in the planar facts and in Lemma 8, where the paper's standing " $n$ large enough" is needed only to that extent. The page names the vertex of Lemma 12 $v$ , the same letter as the eigenvector; it is renamed $u$ . Lemma 14's set $A$ is stated in unfolded form.
Infrastructure that a complete development needs: Euler's formula for topologically planar graphs, the non-planarity of $K_{3,3}$ and $K_5$ , Perron–Frobenius for connected graphs, and the Rayleigh quotient. Proofs of the planar facts (milestone 2) are reusable well beyond this mission. Contributions toward any of them are welcome.

Selected references

M. Tait and J. Tobin, Three conjectures in extremal spectral graph theory, J. Combin. Theory Ser. B (2017). Preprint arXiv:1606.01916v2. https://arxiv.org/abs/1606.01916, DOI https://doi.org/10.1016/j.jctb.2017.04.006
B. N. Boots and G. F. Royle, A conjecture on the maximum value of the principal eigenvalue of a planar graph, Geographical Analysis 23(3) (1991), 276–282.
D. Cao and A. Vince, The spectral radius of a planar graph, Linear Algebra Appl. 187 (1993), 251–257.
A. J. Schwenk and R. J. Wilson, On the eigenvalues of a graph, in: Selected Topics in Graph Theory, Academic Press, 1978, 307–336.
Hong Yuan, A bound on the spectral radius of graphs, Linear Algebra Appl. 108 (1988), 135–139.
M. N. Ellingham and X. Zha, The spectral radius of graphs on surfaces, J. Combin. Theory Ser. B 78(1) (2000), 45–56.
Z. Dvořák and B. Mohar, Spectral radius of finite and infinite planar graphs and of graphs of bounded genus, J. Combin. Theory Ser. B 100(6) (2010), 729–739.

Bibliographic data as given in the bibliography of Tait and Tobin (pp. 21–23).

21 thms2 active usersReviewed

Completed

Combinatorics Graph Theory·Captain: mikedeng1

Three Conjectures in Extremal Spectral Graph Theory 1: For Large n, K₁ + Pₙ₋₁ Is the Unique Outerplanar Graph on n Vertices of Maximum Spectral Radius (Cvetković–Rowlinson Conjecture)Research Paper

Motivation

The spectral radius $\lambda_1(G)$ of a graph $G$ , the largest eigenvalue of its adjacency matrix, is a standard measure of how densely and how centrally a graph is connected. A classical theme of spectral graph theory asks, for a natural family of graphs, which member of the family on $n$ vertices maximizes $\lambda_1$ . For planar graphs this question was raised by geographers comparing road and transport networks, and for outerplanar graphs it was posed by Cvetković and Rowlinson in their 1990 survey of the largest eigenvalue of a graph, where they relate it to the study of subfamilies of Hamiltonian graphs.

Conjecture (Cvetković–Rowlinson, 1990). The outerplanar graph on $n$ vertices of maximum spectral radius is $K_1 + P_{n-1}$ .

Timeline:

1990. Cvetković and Rowlinson state the conjecture (Linear and Multilinear Algebra 28).
1990. Rowlinson makes partial progress, on the index of certain outerplanar graphs (Ars Combinatoria 29).
1993. Cao and Vince work on the spectral radius of planar graphs and the related conjecture (Linear Algebra Appl. 187).
2001. Zhou, Lin and Hu study the spectral radius of Hamiltonian planar and outerplanar graphs (Tsinghua Science and Technology 6).
2017. Tait and Tobin prove the conjecture for all sufficiently large $n$ (arXiv:1606.01916, J. Combin. Theory Ser. B, doi:10.1016/j.jctb.2017.04.006), Theorem 7.

This mission formalizes Section 2 of Tait and Tobin.

Setting

All graphs are finite and simple. An $n$ -vertex graph $G$ has vertex set $V(G) = \{0, \dots, n-1\}$ , adjacency matrix $A(G)$ , and spectral radius $\lambda_1(G)$ , the largest eigenvalue of the real symmetric matrix $A(G)$ . Write $d_u$ for the degree of a vertex $u$ and $N(u)$ for its neighbourhood.

A plane drawing of $G$ places the vertices at distinct points of $\mathbb R^2$ and each edge as a simple arc between its ends; an arc passes through no other vertex, and two arcs meet only at a common end. The union of the vertex points and arcs is a compact set, so its complement has exactly one unbounded connected component, the outer face. A graph is outerplanar if it has a plane drawing in which every vertex lies on the boundary of the outer face.

The join $G + H$ of two graphs is their disjoint union together with all edges between them. The fan $K_1 + P_{n-1}$ is a single vertex joined to every vertex of a path on $n-1$ vertices; it is outerplanar and has $2n-3$ edges.

An outerplanar graph $G$ on $n$ vertices is a spectral maximizer if $\lambda_1(G') \le \lambda_1(G)$ for every outerplanar graph $G'$ on the same $n$ vertices.

Several milestones refer to a Perron vector: an eigenvector $\mathbf v$ of $A(G)$ for $\lambda_1$ with all entries positive, normalized so that its maximum entry is $1$ , together with a vertex $x$ with $\mathbf v_x = 1$ . For a connected graph such a vector exists by the Perron–Frobenius theorem.

Formalization targets

Goal: Theorem 7

There is $N$ such that for every $n \ge N$ and every graph $G$ on $n$ vertices,

G \text{ is an outerplanar spectral maximizer} \iff G \cong K_1 + P_{n-1}.

The forward direction is the paper's Theorem 7; the converse says that the fan is the maximizer, as the conjecture reads. The threshold $N$ is left unspecified, as in the paper.

Milestones

The milestones follow the proof in Section 2, in order:

a strict subgraph of a connected graph has strictly smaller $\lambda_1$ (already proved on the platform);
an outerplanar graph on $n \ge 2$ vertices has at most $2n-3$ edges and no $K_{2,3}$ subgraph;
Lemma 3: for $n \ge 3$ a spectral maximizer has $\lambda_1 > \sqrt{n-1}$ ;
Lemma 4: $d_u > \mathbf v_u n - 11\sqrt n$ for every vertex $u$ ;
Lemma 5: for $n$ large, $d_x > n - 11\sqrt n$ and $\mathbf v_u < C_1/\sqrt n$ for every $u \ne x$ , with an absolute constant $C_1$ ;
Lemma 6: for $n$ large, $\sum_{z\in B}\mathbf v_z < C_2/\sqrt n$ , where $B = V(G)\setminus(N(x)\cup\{x\})$ ;
for $n$ large, $B = \emptyset$ : $x$ is adjacent to every other vertex;
an outerplanar graph with a vertex adjacent to all others is a spanning subgraph of $K_1 + P_{n-1}$ .

Significance

The theorem settles, for all large $n$ , a conjecture that had been open since 1990 and had resisted several partial attacks. The same paper settles, in the same framework, the planar analogue (the Boots–Royle and Cao–Vince conjecture, $K_2 + P_{n-2}$ ) and a conjecture on spectral irregularity. The outerplanar case is the shortest of the three.

On the formal side, the result is proved on paper but has no machine-checked proof. Completing the mission produces a formal theory of outerplanar plane drawings (edge bound, $K_{2,3}$ -freeness, outerplanarity of the fan), eigenvector estimates for extremal graphs, and the full extremal theorem. The edge bound and the $K_{2,3}$ exclusion are reusable for any later work on outerplanar or series–parallel graphs. Determining the exact threshold $N$ , or proving the statement for every $n \ge 2$ , would be a strengthening beyond the paper.

Difficulty

There are two separate difficulties. The first is topological: the facts about outerplanar graphs that the spectral argument uses (at most $2n-3$ edges, no $K_{2,3}$ subgraph, no cycle in $G - x$ when $x$ dominates, outerplanarity of the fan) are folklore on paper but require a Jordan-curve-type argument about plane drawings, of which Mathlib currently contains very little. The second is spectral: the edge-switching step that proves $B = \emptyset$ compares $\lambda_1$ of two graphs through the Rayleigh quotient, and needs a positive Perron vector and the variational characterization of the largest eigenvalue for symmetric matrices. A purely combinatorial edge-maximization argument does not work: the fan is not the only outerplanar graph with $2n-3$ edges, so maximizing the number of edges does not identify the spectral maximizer.

Formalization scope

Graphs are SimpleGraph (Fin n); $\lambda_1$ is the published WangKangXue.SpectralTuran.specRad, the largest eigenvalue of G.adjMatrix ℝ.
Outerplanarity is topological: a published RobertsonSeymour1986.GM5.PlaneDrawing with every vertex point in the closure of the unbounded component of the complement of the drawing. It is not replaced by a forbidden-minor characterization; such characterizations are theorems about outerplanarity, and would change which graphs compete in the maximization.
Extremality is IsSpecMax IsOuterplanar G: $G$ is outerplanar and no outerplanar graph on the same vertex set has larger $\lambda_1$ . It is never weakened to a comparison with the fan.
" $G$ is $K_1 + P_{n-1}$ " is a graph isomorphism G ≃g fan n, with the fan on Fin 1 ⊕ Fin (n - 1).
Perron-vector statements quantify over every positive eigenvector for $\lambda_1$ with maximum entry $1$ and every vertex $x$ with $\mathbf v_x = 1$ ; existential quantification over $\mathbf v$ would be weaker.
"For some absolute constant" is an existential quantifier placed before the threshold, the graph and the vector; "for $n$ sufficiently large" is ∃ N, ∀ n ≥ N.
Added hypotheses, each forced by a degenerate case: $n \ge 2$ for the edge bound (the bound $2n-3$ is negative below), $n \ge 3$ for Lemma 3 (it fails for $n = 2$ , where the maximizer $K_2$ has $\lambda_1 = 1 = \sqrt{n-1}$ ).

A complete development needs the Perron–Frobenius theorem for symmetric nonnegative matrices and the Rayleigh quotient characterization of $\lambda_1$ , both of general use; the theory of outerplanar drawings; and the counting arguments of the lemmas. Contributions to any of these layers are welcome, as are independent proofs of the outerplanar facts from the drawing definition.

Selected references

M. Tait and J. Tobin, Three conjectures in extremal spectral graph theory, J. Combin. Theory Ser. B (2017), https://doi.org/10.1016/j.jctb.2017.04.006; preprint arXiv:1606.01916v2, https://arxiv.org/abs/1606.01916
D. Cvetković and P. Rowlinson, The largest eigenvalue of a graph: a survey, Linear and Multilinear Algebra 28 (1990), 3–33.
P. Rowlinson, On the index of certain outerplanar graphs, Ars Combinatoria 29 (1990), 221–225.
D. Cao and A. Vince, The spectral radius of a planar graph, Linear Algebra Appl. 187 (1993), 251–257.
J. Zhou, C. Lin and G. Hu, Spectral radius of Hamiltonian planar graphs and outerplanar graphs, Tsinghua Science and Technology 6 (2001), 350–354.

12 thms2 active usersReviewed

Control Theory Dynamical Systems Graph Theory·Captain: mikedeng1

Synchronization via Pinning Control on General Complex Networks II: Componentwise LMIs on the Strongly Connected Components Globally Synchronize a Pinned Network with a Directed Spanning TreeResearch Paper

Motivation

Networks of identical dynamical systems coupled along a directed graph model power grids, sensor and robot swarms, neural populations and coupled oscillators. A basic control question is how to steer every node of such a network onto a prescribed reference trajectory by acting directly on only a few nodes. This is pinning control: feedback is injected at a small set of pinned vertices, and the coupling has to carry the reference signal to the rest of the network.

For undirected or strongly connected networks, criteria for pinning synchronization go back to Wang and Chen (2002) and Chen, Liu and Lu (2007), and the first mission of this series treats the strongly connected case of Yu, Chen, Lü and Kurths (2013). Many networks of interest are not strongly connected: information flows down a hierarchy of groups, and the minimal requirement for the reference to reach every node is that the network, with the reference added as a virtual leader, contains a directed spanning tree rooted at the leader. Section 4 of that paper gives a criterion for this general case that splits into one condition per strongly connected component. This mission formalizes that criterion, Theorem 4.5, with the lemmas its proof uses and three corollaries.

Setting

There are $N$ vertices with states $x_i(t)\in\mathbb R^n$ . The coupling configuration matrix $G\in\mathbb R^{N\times N}$ has $G_{ij}\ge0$ for $i\ne j$ , where $G_{ij}>0$ records a connection from vertex $j$ to vertex $i$ , and zero row sums, $G_{ii}=-\sum_{j\ne i}G_{ij}$ . Given a function $f:\mathbb R^n\times\mathbb R_+\to\mathbb R^n$ , a coupling strength $c$ , an inner coupling matrix $\Gamma\in\mathbb R^{n\times n}$ and pinning 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,

where the reference $s$ solves $\dot s=f(s,t)$ . The network is globally synchronized when $x_i(t)-s(t)\to0$ for every vertex and every pair of solutions.

The nonlinearity is controlled by Assumption 1: there is a matrix $K$ with $(x-y)^{\mathsf T}(f(x,t)-f(y,t))\le(x-y)^{\mathsf T}K\Gamma(x-y)$ for all $x,y$ and $t\ge0$ . Throughout §4 the paper also assumes that $K$ and $\Gamma$ commute, that $\Gamma$ is positive definite, and puts $\theta=\lambda_{\max}((K+K^{\mathsf T})/2)\ge0$ .

The vertices split into strongly connected components $V_1,\dots,V_M$ . In the Frobenius normal form the components are ordered so that no edge goes from a later component to an earlier one, which makes $G$ block lower triangular. For each component $j$ the mission uses three matrices:

$\widetilde G_j$ , the diagonal block of $G-\mathrm{diag}(d)$ on $V_j$ ;
$A_j$ , the within-component part of $G$ with zero row sums;
$\widetilde\Pi_j=\mathrm{diag}(\Pi_j)$ , where $\Pi_j$ is a positive vector with $\Pi_j^{\mathsf T}A_j=0$ .

In Lean, component membership is a map blk : Fin N → Fin M, and Fin M carries the Frobenius order.

Formalization targets

Goal: Theorem 4.5

If, for every component $j$ ,

2\theta\widetilde\Pi_j+c\bigl(\widetilde\Pi_j\widetilde G_j+\widetilde G_j^{\mathsf T}\widetilde\Pi_j\bigr)<0, \tag{4.8}

then the controlled network with a directed spanning tree is globally synchronized.

Milestones

The θ bound (p. 1402). Commutation and $\Gamma>0$ turn Assumption 1 into $(x-y)^{\mathsf T}(f(x,t)-f(y,t))\le\theta(x-y)^{\mathsf T}\Gamma(x-y)$ .
Lemma 2.13. The strict Schur complement test for a symmetric block matrix.
Lemma 4.4. If $\widetilde\Pi_j\widetilde G_j+\widetilde G_j^{\mathsf T}\widetilde\Pi_j<0$ on every diagonal block of a block lower-triangular $\overline G$ , then positive block weights $\Delta_j$ exist with $\Delta\widetilde\Pi\overline G+\overline G^{\mathsf T}\widetilde\Pi\Delta<0$ .
(4.10). Along solutions, $V=\sum_j\Delta_j\widetilde e_j^{\mathsf T}\widetilde\Pi_j\widetilde e_j$ satisfies $\dot V\le e^{\mathsf T}\{[\Delta\widetilde\Pi(c\overline G+\theta I_N)+(c\overline G+\theta I_N)^{\mathsf T}\widetilde\Pi\Delta]\otimes\Gamma\}e$ .

Companions

Corollary 4.7: the same conclusion under $\theta\widetilde\Pi_j+c(\overline A_j-\widetilde\Pi_jC_j-\widetilde\Pi_j\overline D_j)<0$ , which separates the outer in-degrees $C_j$ from the pinning gains $\overline D_j$ .
Corollary 4.8 (i): an explicit coupling-strength threshold under Assumption 2.
Corollary 4.9: partial synchronization of the first components.

Significance

Theorem 4.5 replaces a single $Nn\times Nn$ matrix inequality for the whole network with $M$ inequalities, one of the size of each component. In practice the test runs component by component down the Frobenius order: decide which components need pinning, choose gains for each one separately, and get synchronization of the whole network. Corollary 4.7 makes this explicit in terms of the outer in-degrees: a component with no incoming edges from earlier components has to be pinned (Remark 4), while a component that receives enough weight from upstream needs no control. These conditions underlie the pinning scheme algorithm of §5 of the paper.

On the formal side, as far as a search of the platform and of Mathlib shows, none of these results is machine-checked. Mathlib has the positive semidefinite Schur complement and irreducible nonnegative matrices, but not the strict Schur complement, block-diagonal Lyapunov scaling, or Lyapunov arguments for networked ODEs with Kronecker-structured couplings. The mission produces, beyond the paper's theorem:

a reusable strict Schur complement lemma;
a block-triangular diagonal-stability lemma;
a template for Lyapunov estimates on coupled networks in Lean.

Difficulty

The obvious argument is to take one Lyapunov function weighted by a positive left null vector of the whole coupling matrix, as in the strongly connected case. Here it fails: the coupling matrix of a network that is not strongly connected has no positive left null vector, and condition (4.8) is local to each component. The central step is the passage from blockwise to global negative definiteness (Lemma 4.4). Condition (4.8) says nothing about the off-diagonal blocks that couple a component to earlier ones, and a block lower-triangular matrix whose symmetrized diagonal blocks are negative definite need not have a negative definite symmetric part; the component weights $\Delta_j$ have to be found so that those couplings are dominated, which is a quantitative statement about Schur complements. Turning the resulting matrix inequality into convergence of the trajectories then needs a differential inequality on $[0,\infty)$ , a Kronecker-product definiteness argument with $\Gamma$ , and the commutation of $K$ and $\Gamma$ to reach the θ bound.

Formalization scope

States are Fin n → ℝ and matrices are indexed by Fin N, Fin n, or the subtype of one component's vertices. Solutions are functions on ℝ that satisfy their ODE on $[0,\infty)$ through HasDerivWithinAt … (Set.Ici 0). "For any initial conditions" means for every pair of solutions $(s,x)$ ; existence of solutions is not claimed. Convergence is componentwise, which agrees with every norm on $\mathbb R^n$ . "Positive definite" is Mathlib's Matrix.PosDef, which includes symmetry, and $X<0$ is (-X).PosDef. $\lambda_{\max}$ is the least Rayleigh bound, IsLamMax, never a supremum of a possibly empty set.

The vertices are not permuted into Frobenius form. The hypotheses say instead that:

every component is nonempty;
every component is strongly connected inside itself;
every edge between components points forward in the order;
every vertex is reachable from a pinned vertex.

The weights $\Pi_j$ are tied to the paper's object by $\Pi_j^{\mathsf T}A_j=0$ . The standing assumptions of p. 1402 (Assumption 1, $K\Gamma=\Gamma K$ , $\theta=\lambda_{\max}((K+K^{\mathsf T})/2)\ge0$ , $\Gamma>0$ ) are hypotheses of every goal-level statement. The goal does not assume the weights $\Delta_j$ , the bound (4.10), or definiteness of a whole-network matrix; it assumes only (4.8) on each component, so it cannot be trivialized by assuming its own conclusion. For $n=0$ the $\lambda_{\max}$ hypothesis cannot be met, so that degenerate dimension is excluded.

The pages contain three misprints. (4.10) has " $-c$ " in its third line and " $++$ " in its last; the last line, with a single $+$ , is formalized. Corollary 4.9 ranges " $i=1,\dots,N$ " where the component range is meant.

A complete development needs a Gronwall-type decay lemma on $[0,\infty)$ , the strict Schur complement, definiteness of Kronecker products, and the square root of a positive definite matrix commuting with matrices that commute with it. Each of these is reusable well beyond this mission, and contributions to any of them are welcome, as are proofs of the milestones in any order.

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(6) (2007), 1317–1326. https://doi.org/10.1109/TCSI.2007.895383
S. Boyd, L. El Ghaoui, E. Feron, V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994. https://doi.org/10.1137/1.9781611970777
R. A. Brualdi, H. J. Ryser, Combinatorial Matrix Theory, Cambridge University Press, 1991. https://doi.org/10.1017/CBO9781107325708

7 thms2 active usersReviewed

Completed

Algebraic Topology Combinatorics·Captain: mikedeng1

Isoperimetric Inequalities in Simplicial Complexes 1: For a Finite d-Complex with a Complete Skeleton, the Spectral Gap Is at Most the Cheeger Constant, λ(X) ≤ h(X)Research Paper

Motivation

For a finite graph, the Cheeger constant measures how hard it is to cut the vertex set into two pieces, and the spectral gap of the graph Laplacian measures how fast random walks mix. The two Cheeger inequalities (Dodziuk 1984; Alon and Milman 1985; Alon 1986) bound each quantity by a function of the other, and they underlie the theory of expander graphs, with uses in derandomization, error-correcting codes and the analysis of Markov chains.

High-dimensional expanders extend this theory from graphs to simplicial complexes. Linial and Meshulam (2006) and Gromov (2010) introduced combinatorial and topological notions of expansion for complexes; the spectral side is Eckmann's discrete Hodge theory (1944), in which each dimension carries its own Laplacian. Parzanchevski, Rosenthal and Tessler (arXiv:1207.0638, Combinatorica 2015) defined a $d$ -dimensional Cheeger constant $h(X)$ through partitions of the vertices into $d+1$ blocks and proved the analogue of the upper Cheeger inequality, $\lambda(X)\le h(X)$ , for complexes with a complete skeleton. This mission formalizes that theorem.

Setting

Let $V=\{0,1,\dots,n-1\}$ and $d\ge1$ . A finite $d$ -complex with a complete skeleton $X$ on $V$ consists of all subsets of $V$ with at most $d$ elements together with a set $X^d$ of $(d+1)$ -element subsets, the $d$ -cells. A set of $j+1$ vertices is a $j$ -cell; $X^{d-1}$ is therefore the set of all $d$ -element subsets.

Each cell is oriented by the increasing order of its vertices, $\sigma=[\sigma_0,\dots,\sigma_j]$ with $\sigma_0<\dots<\sigma_j$ . The space $\Omega^{j}$ of $j$ -forms consists of the real functions on $j$ -cells, with inner product

\langle f,g\rangle=\sum_{\sigma\in X^{j}}f(\sigma)g(\sigma).

The co-boundary $\partial_d^*:\Omega^{d-1}\to\Omega^d$ and the boundaries $\partial_d:\Omega^d\to\Omega^{d-1}$ , $\partial_{d-1}:\Omega^{d-1}\to\Omega^{d-2}$ are

(\partial_d^*f)(\tau)=\sum_{i=0}^d(-1)^i f(\tau\setminus\tau_i),\qquad (\partial_j g)(\sigma)=\sum_{v\sim\sigma}g([v,\sigma_0,\dots,\sigma_{j-1}]),

where $v\sim\sigma$ means that $v\notin\sigma$ and $\{v\}\cup\sigma$ is a cell, and $[v,\sigma_0,\dots]$ equals $(-1)^k$ times the increasingly oriented cell when $v$ has $k$ smaller vertices in $\sigma$ . The upper Laplacian is $\Delta^+=\partial_d\partial_d^*$ on $\Omega^{d-1}$ , and $Z_{d-1}=\ker\partial_{d-1}$ is the space of $(d-1)$ -cycles.

The spectral gap is the least eigenvalue of $\Delta^+$ on the cycles (Definition 2.1):

\lambda(X)=\min\operatorname{Spec}\big(\Delta^+|_{Z_{d-1}}\big).

For sets $A_0,\dots,A_d\subseteq V$ , let $F(A_0,\dots,A_d)$ be the set of $d$ -cells with exactly one vertex in each $A_i$ . The Cheeger constant is (Definition 1.1)

h(X)=\min_{V=\coprod_{i=0}^dA_i}\frac{n\cdot|F(A_0,\dots,A_d)|}{|A_0|\cdot|A_1|\cdots|A_d|},

the minimum over partitions of $V$ into nonempty sets $A_0,\dots,A_d$ . For $d=1$ , $Z_0$ is the space of functions summing to zero, $\Delta^+$ is the graph Laplacian, and $h$ is the usual Cheeger constant $\min_{A}\,n|E(A,\bar A)|/(|A||\bar A|)$ .

Formalization targets

Goal: Theorem 1.2 (Cheeger Inequality)

\lambda(X)\le h(X)

for every finite $d$ -complex $X$ with a complete skeleton on $n\ge d+1$ vertices.

Milestones

The chain-complex identity $\partial_{d-1}\partial_d=0$ (p. 6).
The form $f$ of (4.1), built from a partition, is a $(d-1)$ -cycle (p. 12).
$\partial_d^*$ is the adjoint of $\partial_d$ : $\langle\partial_dg,f\rangle=\langle g,\partial_d^*f\rangle$ (p. 6).
Rayleigh's principle (4.2): $\lambda(X)\langle f,f\rangle\le\langle\Delta^+f,f\rangle=\langle\partial_d^*f,\partial_d^*f\rangle$ for $f\in Z_{d-1}$ (p. 12).
$\langle f,f\rangle=n\prod_{i=0}^d|A_i|$ for the form (4.1) (p. 13).
(4.3): $|(\partial_d^*f)(\sigma)|$ equals $n$ for $\sigma\in F(A_0,\dots,A_d)$ and $0$ for the other $d$ -cells (p. 13).
$\langle\partial_d^*f,\partial_d^*f\rangle=n^2|F(A_0,\dots,A_d)|$ (p. 14).

Milestones 2 and 5–7 hold for every partition, not only a minimizing one.

Significance

The result. Theorem 1.2 shows that a large spectral gap forces every partition of the vertices into $d+1$ blocks to be crossed by many $d$ -cells, so spectral information certifies combinatorial expansion of a complex. The paper uses it with the spectral analysis of Gundert and Wagner to show that Linial–Meshulam random complexes $X(d,n,C\log n/n)$ have Cheeger constant of order $\log n$ for large $C$ (Corollary 1.3). The paper also shows that the converse direction fails: a triangulation of the Möbius strip has $h(X)=1\tfrac14$ but $\lambda(X)=0$ , so no lower bound of the form $C\cdot h(X)^m\le\lambda(X)$ holds.

Formalizing it. The theorem is proved in the paper; to our knowledge no machine-checked proof exists. A formal proof requires a signed simplicial chain complex with explicit orientations, the adjoint relation between boundary and co-boundary, and a Rayleigh-quotient bound for a symmetric operator on an invariant subspace. These are the basic tools for any further formal work on spectral high-dimensional expansion, including the Mixing Lemma of the same paper (the companion mission of this series).

Difficulty

The graph proof plugs a two-valued test function into the Rayleigh quotient. In dimension $d$ the test vector must be a $(d-1)$ -cycle, and an indicator of a block is not one. The paper's form (4.1) assigns to a $(d-1)$ -cell whose vertices meet $d$ distinct blocks the size of the missing block, with the sign of a permutation of the blocks. Showing that this form is a cycle and that its co-boundary has absolute value exactly $n$ on $F(A_0,\dots,A_d)$ and $0$ elsewhere is a case analysis over how the vertices of a cell fall into blocks, and every case depends on the orientation signs. A convention error in any of the operators or in the form makes one of these identities fail. A second, smaller difficulty is that $\lambda(X)$ is a minimum over the spectrum on a subspace, so the Rayleigh bound must be proved for $\Delta^+$ restricted to $Z_{d-1}$ , which it preserves.

Formalization scope

Vertices are Fin n; a complex is a structure holding its $d$ -cells as Finset (Finset (Fin n)), each of size $d+1$ ; the complete skeleton is built into the type. Complexes without $d$ -cells are allowed.
Forms are EuclideanSpace ℝ over the subtype of $k$ -element vertex sets, so no form is supported on sets of the wrong size. $\Omega^d$ is modelled on all $(d+1)$ -element sets; $\partial_d^*$ vanishes off $X^d$ and $\partial_d$ ignores values there.
Orientation is by the order of Fin n; the sign of vertex $v$ in cell $\tau$ is $(-1)^{\#\{w\in\tau:w<v\}}$ . Boundary and co-boundary are both defined by their formulas; their adjointness is milestone 3.
The spectral gap is not defined by sInf. The goal states that some eigenvalue $\mu$ of $\Delta^+$ on $Z_{d-1}$ (a nonzero cycle $f$ with $\Delta^+f=\mu f$ ) is at most the Cheeger ratio of every partition, which is equivalent to $\lambda(X)\le h(X)$ . A partition is a family A : Fin (d+1) → Finset (Fin n) of nonempty, pairwise disjoint sets covering the vertices.
Added hypotheses: $d\ge1$ (the Laplacians act on $\Omega^{d-1}$ ) and $n\ge d+1$ (presupposed by the paper, since $h$ minimizes over partitions into $d+1$ nonempty sets; for $n\le d$ the cycle space is $0$ ).
Ruled out: forms supported off the $d$ -element sets (they would be spurious cycles with eigenvalue $0$ ), an eigenvalue set read through sInf (empty sets give $0$ ), unsigned boundaries (for which $\partial\partial\ne0$ ), cocycles $\ker\partial_d^*$ in place of cycles $\ker\partial_{d-1}$ (on which $\Delta^+$ is zero), and arbitrary disjoint families in place of partitions (empty blocks give ratio $0$ ).
Needed infrastructure: sign bookkeeping for faces of sorted finsets, the spectral theorem for symmetric operators on a finite-dimensional inner product space restricted to an invariant subspace (Mathlib's LinearMap.IsSymmetric), and counting cells by blocks of a partition. The chain-complex and adjointness lemmas are reusable in any formal development of simplicial Hodge theory; contributions there are welcome.

Selected references

O. Parzanchevski, R. Rosenthal, R. J. Tessler, Isoperimetric inequalities in simplicial complexes, Combinatorica 35 (2015). arXiv:1207.0638v3, doi:10.1007/s00493-014-3002-x
B. Eckmann, Harmonische Funktionen und Randwertaufgaben in einem Komplex, Comment. Math. Helv. 17 (1944), no. 1, 240–255.
N. Alon, V. D. Milman, λ₁, isoperimetric inequalities for graphs, and superconcentrators, J. Combin. Theory Ser. B 38 (1985), 73–88. doi:10.1016/0095-8956(85)90092-9
N. Linial, R. Meshulam, Homological connectivity of random 2-complexes, Combinatorica 26 (2006), 475–487. doi:10.1007/s00493-006-0027-9
A. Gundert, U. Wagner, On Laplacians of random complexes, Proceedings of the 2012 Symposium on Computational Geometry, ACM, 2012, 151–160.
M. Gromov, Singularities, expanders and topology of maps. Part 2: From combinatorics to topology via algebraic isoperimetry, Geom. Funct. Anal. 20 (2010), no. 2, 416–526.

10 thms2 active usersReviewed

Completed

Numerical Analysis Optimization·Captain: mikedeng1

Optimization-Based Algorithms for Tensor Decompositions: Canonical Polyadic Decomposition, Decomposition in Rank-(Lr, Lr, 1) Terms, and a New Generalization 1: Block Structure of the Gramian JᴴJResearch Paper

Motivation

Tensor decompositions express a multiway array as a sum of simple terms. The canonical polyadic decomposition (CPD) writes an $N$ -th order tensor $\mathcal T\in\mathbb C^{I_1\times\cdots\times I_N}$ as a sum of $R$ outer products of vectors; block term decompositions replace each rank-one term by a term of higher multilinear rank. These models are used in signal processing, blind source separation and telecommunications, and are computed numerically by minimizing a least-squares misfit.

Sorber, Van Barel and De Lathauwer (SIAM J. Optim. 23(2), 2013) introduce the (rank- $L_r\circ$ rank-1) block term decomposition (BTD), which contains both the CPD and the rank- $(L_r,L_r,1)$ BTD as special cases, and develop optimization algorithms for it: nonlinear conjugate gradient and quasi-Newton methods built on the complex gradient, and Gauss–Newton and Levenberg–Marquardt methods built on the Jacobian. For the second family the central object is the Gramian $J^{\mathrm H}J$ of the Jacobian $J$ of the residual. Theorem 4.5 of the paper gives its exact block structure, and that structure is what lets the methods run without ever forming $J$ .

Setting

Fix $N = P + Q$ modes with dimensions $I_1,\dots,I_N$ , a number of terms $R$ , and block sizes $L_1,\dots,L_R$ ; put $R' = \sum_r L_r$ . The BTD approximates $\mathcal T$ by

\sum_{r=1}^R\Big(\sum_{r'} a^{(1)}_{r'}\circ\cdots\circ a^{(P)}_{r'}\Big)\circ\big(c^{(1)}_r\circ\cdots\circ c^{(Q)}_r\big),

where the inner sum runs over the $L_r$ columns of block $r$ . Here $A^{(p)} = [a^{(p)}_1\cdots a^{(p)}_{R'}]\in\mathbb C^{I_p\times R'}$ and $C^{(q)} = [c^{(q)}_1\cdots c^{(q)}_R]\in\mathbb C^{I_{P+q}\times R}$ .

The paper reads this as a structured CPD in $R'$ rank-one terms. The first $P$ factor matrices are the $A^{(p)}$ , and the last $Q$ are

A^{(P+q)} = C^{(q)}\cdot E,

where $E = \mathrm{diag}(1_{1\times L_1},\dots,1_{1\times L_R})\in\mathbb R^{R\times R'}$ copies column $r$ of $C^{(q)}$ into the $L_r$ columns of block $r$ . The residual tensor is

\mathcal F_{\mathrm{BTD}} = \sum_{c=1}^{R'} a^{(1)}_c\circ\cdots\circ a^{(N)}_c - \mathcal T,

and the unknowns are $z = (\mathrm{vec}A^{(1)},\dots,\mathrm{vec}A^{(P)},\mathrm{vec}C^{(1)},\dots,\mathrm{vec}C^{(Q)})$ . The Jacobian $J = \partial\,\mathrm{vec}(\mathcal F_{\mathrm{BTD}})/\partial z^{\mathrm T}$ is the complex (holomorphic) derivative: $\mathcal F_{\mathrm{BTD}}$ is a polynomial in $z$ , not in $\bar z$ .

Three auxiliary matrices enter the answer. The first is $W^\sigma = \ast_{m\notin\sigma}A^{(m)\mathrm H}A^{(m)}$ , the Hadamard product of the Gramians of the factor matrices outside a mode set $\sigma$ , with entries $w^\sigma_{r_1r_2}$ . The second is $F^{(q)} = E\otimes\mathbb I_{I_{P+q}}$ , which satisfies $\mathrm{vec}(C^{(q)}E)^{\mathrm T} = \mathrm{vec}(C^{(q)})^{\mathrm T}F^{(q)}$ (Proposition 4.1). The third is the block diagonal $\Sigma = \mathrm{diag}(\mathbb I_{I_1R'},\dots,\mathbb I_{I_PR'},F^{(1)},\dots,F^{(Q)})$ .

Formalization targets

Goal: Theorem 4.5

For every tensor $\mathcal T$ and every $z$ ,

J^{\mathrm H}J = \Sigma\cdot\big[\Pi^{(n_1,n_2)}\big]_{n_1,n_2=1}^N\cdot\Sigma^{\mathrm T},

\Pi^{(n_1,n_2)} \triangleq \Big(\tfrac{\partial\,\mathrm{vec}\mathcal F}{\partial\,\mathrm{vec}(A^{(n_1)})^{\mathrm T}}\Big)^{\mathrm H}\Big(\tfrac{\partial\,\mathrm{vec}\mathcal F}{\partial\,\mathrm{vec}(A^{(n_2)})^{\mathrm T}}\Big) = \begin{cases}W^{\{n\}}\otimes\mathbb I_{I_n} & n=n_1=n_2,\\ \big[w^{\{n_1,n_2\}}_{r_1r_2}\,a^{(n_1)}_{r_2}a^{(n_2)\mathrm H}_{r_1}\big]_{r_1,r_2} & \text{otherwise.}\end{cases}

The goal has two parts, and both are required. The first is that the Gramian of the CPD Jacobian equals the explicit block matrix. The second is the factorization through $\Sigma$ .

Milestones

The columns of the CPD Jacobian are rank-one tensors: $\partial\mathcal F/\partial a^{(n)}_{ir} = a^{(1)}_r\circ\cdots\circ e^{(n)}_i\circ\cdots\circ a^{(N)}_r$ .
Diagonal blocks: inner products $w^{\{n\}}_{r_1r_2}\delta_{ij}$ , hence the block $w^{\{n\}}_{r_1r_2}\mathbb I_{I_n}$ .
Off-diagonal blocks: inner products $w^{\{n_1,n_2\}}_{r_1r_2}a^{(n_1)}_{ir_2}\overline{a^{(n_2)}_{jr_1}}$ , hence the rank-one block $w^{\{n_1,n_2\}}_{r_1r_2}a^{(n_1)}_{r_2}a^{(n_2)\mathrm H}_{r_1}$ .
Proposition 4.1: the vec identity for $C^{(q)}E$ and the chain rule (4.3b) for the Jacobian columns of $C^{(q)}$ .
The blocks of $J^{\mathrm H}J$ that involve some $C^{(q)}$ are $\Pi F^{(q)\mathrm T}$ , $F^{(q)}\Pi$ and $F^{(q_1)}\Pi F^{(q_2)\mathrm T}$ , i.e. $J^{\mathrm H}J = \Sigma\,(J_{\mathrm{CPD}}^{\mathrm H}J_{\mathrm{CPD}})\,\Sigma^{\mathrm T}$ .

Significance

With Theorem 4.5, $J^{\mathrm H}J$ is determined by the factor matrices and the small Gramians $A^{(n)\mathrm H}A^{(n)}$ . For a hypercubical CPD this takes $O(NR^2)$ extra memory instead of the $O(N^2R^2I^2)$ of a dense Gramian. Theorem 4.6 of the paper then turns the same structure into a matrix–vector product in $O(NR^2I)$ operations, which is what inexact Gauss–Newton and Levenberg–Marquardt steps solved by preconditioned conjugate gradients require. The block-diagonal part $\Pi^{(n,n)} = W^{\{n\}}\otimes\mathbb I$ also gives the block Jacobi preconditioner of the paper's §4.2. For the CPD, expressions for the Gramian were already studied in chemometrics (the paper cites G. Tomasi's 2006 thesis for this); Theorem 4.5 states the block structure in closed form and extends it to the structured BTD through $\Sigma$ .

The result is proved in the paper. As far as a search of Prove2Me and Mathlib shows, nothing about CPD or BTD Jacobians has been formalized. This mission produces a machine-checked proof of the block structure, starting from an explicit model of the decomposition and an honest complex derivative. That model (outer products, the structured CPD, $E$ , $\Sigma$ , the Hadamard-Gramian products) can be reused for the paper's cogradient theorem and for other tensor algorithms.

Difficulty

The identity is finite-dimensional, but no single step reduces it to a known lemma. First, $J$ is a genuine derivative of a multilinear polynomial map in $\sum_n I_nR'$ complex variables, so each entry has to be computed from the derivative of a sum of products. Second, $J^{\mathrm H}J$ is a sum over all $\prod_n I_n$ multi-indices. Turning it into the product of Gramians in $W^\sigma$ means exchanging a sum of products with a product of sums while one or two modes are held fixed, with the conjugates landing on crossed column indices ( $a^{(n_1)}_{r_2}$ , $\bar a^{(n_2)}_{r_1}$ ). Third, the structured factor matrices $A^{(P+q)} = C^{(q)}E$ are not unknowns. The derivative with respect to $C^{(q)}$ has to go through the chain rule and the vec–Kronecker identity, and $\Sigma$ 's rows and columns are indexed by different sets.

Formalization scope

All objects are defined in TensorBTD.Gramian.Setting, with the following conventions.

Modes and columns. The $N$ modes are Fin P ⊕ Fin Q (mode $p$ is Sum.inl (p-1) and mode $P+q$ is Sum.inr (q-1)), so all indices are 0-based. The $R'$ columns are Σ r : Fin R, Fin (L r) in lexicographic order, which is the order of (3.5).
Tensors and residuals. A tensor is a function of the multi-index. The residual is defined entrywise as a sum of outer products. The paper's (3.8) is its mode- $n$ unfolding.
Vectorization and Kronecker products. Vectorized indices are (column, row) pairs, Mathlib's column-major Matrix.vec. This is the paper's Definition 2.5 with its misprint $(i+(j-1)J)$ corrected to $(i+(j-1)I)$ . Kronecker products are Mathlib's ⊗ₖ.
Jacobian. The Jacobian is defined column by column as the complex derivative deriv of $t\mapsto G(x+te_\beta)$ at $0$ . It is not defined by its closed form, and it is not a real derivative.
The unstructured CPD. $\Pi^{(n_1,n_2)}$ differentiates with respect to $A^{(n)}$ for every $n$ , including $n>P$ , where $A^{(n)}$ is not an unknown. It is therefore taken as the Jacobian of the unstructured CPD residual in $R'$ terms, with all $N$ factor matrices free, evaluated at the factor matrices of $z$ . This is how the paper's proof uses it.

There are no hypotheses. The paper's assumptions that $P, Q\ge 1$ and its qualifiers "nonzero" and "rank- $L_r$ " are not used in Section 4, so they are dropped. This is a generalization: $Q = 0$ gives the plain CPD in $R'$ terms.

A goal that took the closed form of $\Pi$ as the definition, or that defined $J$ entrywise by the outer-product formula of milestone 1, would only state a sum identity. Both are ruled out: $J$ is a derivative, and the goal asserts that the Gramian of the CPD Jacobian equals the closed form. A misprint in the proof's closing paragraph, $F^{(q)}\Pi^{(p,P+q)}$ for the $(P+q,p)$ block, is corrected in Lean to $F^{(q)}\Pi^{(P+q,p)}$ .

Useful Mathlib infrastructure includes Matrix.vec, Matrix.kroneckerMap, Matrix.blockDiagonal', Finset.prod_univ_sum and the derivative rules for finite products (HasDerivAt.finset_prod). General lemmas welcome as contributions: derivatives of multilinear maps along coordinate directions, the sum–product exchange over Fintype.piFinset, and the chain rule for a Jacobian composed with a linear map.

Selected references

L. Sorber, M. Van Barel, L. De Lathauwer, Optimization-Based Algorithms for Tensor Decompositions: Canonical Polyadic Decomposition, Decomposition in Rank- $(L_r,L_r,1)$ Terms, and a New Generalization, SIAM J. Optim. 23(2), 695–720, 2013. https://doi.org/10.1137/120868323
T. G. Kolda, B. W. Bader, Tensor Decompositions and Applications, SIAM Review 51(3), 455–500, 2009. https://doi.org/10.1137/07070111X
L. De Lathauwer, Decompositions of a Higher-Order Tensor in Block Terms — Part II: Definitions and Uniqueness, SIAM J. Matrix Anal. Appl. 30(3), 1033–1066, 2008. https://doi.org/10.1137/070690729
L. Sorber, M. Van Barel, L. De Lathauwer, Unconstrained Optimization of Real Functions in Complex Variables, SIAM J. Optim. 22(3), 879–898, 2012. https://doi.org/10.1137/110832124

7 thms2 active usersReviewed

Combinatorics Markov Chain Theoretical Computer Science·Captain: mikedeng1

High Order Random Walks: Beyond Spectral Gap 2: On a Two-Sided λ-Local Spectral Expander, Spec(M⁺_k) ⊆ {1} ∪ ⋃_j [(k+1−j)/(k+2) ± √(k+1)·ε_k/(k+2)] and Eigenvectors Lie Near U^j_kResearch Paper

Motivation

High-dimensional expanders are simplicial complexes whose local structure forces global mixing. Random walks on their $k$ -dimensional faces, the high order random walks, are used to analyse sampling algorithms: the bases-exchange walk on the bases of a matroid is such a walk, and its spectral analysis by Anari, Liu, Oveis Gharan and Vinzant (arXiv:1811.01816) settled the Mihail–Vazirani conjecture on counting matroid bases. Agreement tests and PCP constructions use the same walks (Dinur–Kaufman, FOCS 2017).

Most of these applications use only the second eigenvalue of the walk. Kaufman and Oppenheim (arXiv:1707.02799v3) observe that this eigenvalue cannot be very small, because of natural obstructions such as cochains pulled up from lower dimensions, and ask instead for the whole spectrum and the structure of the eigenvectors. For complexes whose links have both small second eigenvalue and bounded-below smallest eigenvalue (two-sided local spectral expanders), they show that the spectrum of the walk on $k$ -faces clusters around $k+1$ explicit values, each cluster corresponding to cochains built from a lower dimension.

Timeline. Garland (1973, doi:10.2307/1970833) introduced the localization method relating global cohomology to spectra of links. Kaufman and Mass (ITCS 2017, arXiv:1604.02947) defined high order random walks and bounded their second eigenvalue. Oppenheim (Discrete Comput. Geom. 2018, arXiv:1709.04431) developed the local spectral expansion framework and its trickle-down theorem. Kaufman and Oppenheim gave the decomposition theorems this mission formalizes; arXiv v3 (2021) corrects an error of the published version. Alev and Lau (arXiv:2001.02827) later improved the one-sided bounds.

Setting

Let $X$ be a pure $n$ -dimensional finite simplicial complex on a vertex set $V$ : a finite family of finite subsets of $V$ , closed under subsets, in which every face lies in a face with $n+1$ vertices. $X(k)$ is the set of faces with $k+1$ vertices, and $X(-1)=\{\emptyset\}$ . A weight is a function $m:X\to(0,\infty)$ with $m(\tau)=\sum_{\sigma\in X(k+1),\,\tau\subseteq\sigma}m(\sigma)$ for $\tau\in X(k)$ , $k\le n-1$ .

A $k$ -cochain is a function $\phi:X(k)\to\mathbb R$ ; the space $C^k(X)$ carries the inner product $\langle\phi,\psi\rangle=\sum_{\sigma\in X(k)}m(\sigma)\phi(\sigma)\psi(\sigma)$ . $C^k_0(X)$ is the subspace of cochains orthogonal to the constants.

The signless differential $d_k:C^k\to C^{k+1}$ is $d_k\phi(\sigma)=\sum_{\tau\subset\sigma,\,\tau\in X(k)}\phi(\tau)$ , and $d_k^*$ is its adjoint.
The upper random walk $M^+_k$ on $X(k)$ stays at $\tau$ with probability $\frac1{k+2}$ and moves to $\tau'$ with probability $\frac{m(\tau\cup\tau')}{(k+2)m(\tau)}$ when $\tau\cup\tau'\in X(k+1)$ ; equivalently $d_k^*d_k=(k+2)M^+_k$ .
The link of $\tau$ is $X_\tau=\{\eta:\ \eta\cap\tau=\emptyset,\ \tau\cup\eta\in X\}$ with weight $m_\tau(\eta)=m(\tau\cup\eta)$ . On its vertices, $(M')^+_{\tau,0}$ is the non-lazy walk; $\mu_\tau$ and $\nu_\tau$ are its second largest and smallest eigenvalues.
$X$ is a two-sided $\lambda$ -local spectral expander if $-\lambda\le\nu_\tau$ and $\mu_\tau\le\lambda$ for every face $\tau$ of dimension $-1,\dots,n-2$ .

For $0\le k\le n-1$ the paper defines subspaces of $C^k_0(X)$ : $V^0_0=C^0_0$ ; for $k\ge1$ , $V^j_k=d_{k-1}\cdots d_j(C^j_0)$ for $j<k$ and $V^k_k=\ker d^*_{k-1}$ ; and $U^0_k=V^0_k$ , $U^j_k=V^j_k\cap(V^{j-1}_k)^\perp$ for $0<j<k$ , $U^k_k=V^k_k$ . With $\varepsilon_0=\lambda$ and $\varepsilon_k=2k(1+2k\sqrt k)\varepsilon_{k-1}+(k+1)\lambda$ , $P_{U}$ denotes the weighted orthogonal projection onto $U$ .

Formalization targets

Goal: Theorem 5.9 (p. 22)

If $\varepsilon_k\le\frac{1}{2(1+2(k+1)\sqrt{k+1})}$ for $0\le k\le n-2$ and $\varepsilon_{n-1}<\frac1{2\sqrt n}$ , then for $0\le k\le n-1$

\operatorname{Spec}(M^+_k)\subseteq\{1\}\cup\bigcup_{j=0}^{k}\Big[\tfrac{k+1-j}{k+2}-\tfrac{\sqrt{k+1}}{k+2}\varepsilon_k,\ \tfrac{k+1-j}{k+2}+\tfrac{\sqrt{k+1}}{k+2}\varepsilon_k\Big],

and an eigenvector $\phi\in C^k_0$ whose eigenvalue lies in the $j$ -th interval satisfies $\|\phi-P_{U^j_k}\phi\|\le\frac{\sqrt{k+1}\varepsilon_k}{1-\sqrt{k+1}\varepsilon_k}\|\phi\|$ .

Milestones

the localization identities (Lemma 3.6, Corollary 3.7, Propositions 4.1, 4.2) and the two-sided bound of Lemma 4.3;
Lemma 5.1 and the orthogonal decomposition $C^k_0(X)=U^k_k\oplus\cdots\oplus U^0_k$ (§5.3);
Theorem 5.6: $\|d^*_kd_kP_{U^j_k}\phi-(k+1-j)P_{U^j_k}\phi\|\le\varepsilon_k\|P_{U^j_k}\phi\|$ ;
Corollary 5.8: the same for $M^+_k$ , with $\frac{k+1-j}{k+2}$ and $\frac{\varepsilon_k}{k+2}$ .

Significance

The result. Theorem 5.9 describes the spectrum of $M^+_k$ , not only its second eigenvalue. The eigenvalue $\frac{k+1-j}{k+2}$ is the one carried by cochains pulled up from dimension $j$ , so it explains which cochains are shrunk slowly by the walk and which quickly. It is the two-sided counterpart of the paper's one-sided mixing bound (Theorem 5.4, the subject of the first mission in this series). It gives approximate eigenspaces explicitly, which a mixing-time analysis or an agreement-test analysis can use in place of a bound on a single eigenvalue.

Formalizing it. No machine-checked development of simplicial-complex random walks, Garland's method, or local spectral expansion is known to exist; Mathlib has simplicial complexes in a geometric sense but no weighted cochain calculus. The mission produces the cochain calculus of §2–§4 together with the spectral statements of §5.3. The statements are those of the arXiv v3 preprint. They are published results but have not been formalized.

Difficulty

The obvious route would show that the spaces $U^j_k$ are exact eigenspaces. That holds for the complete complex but not in general: $d^*d$ maps $U^j_k$ only approximately into itself, and the error has to be controlled through every lower dimension at once. Theorem 5.6 is an induction on $k$ in which the error $\varepsilon_{k-1}$ of dimension $k-1$ enters dimension $k$ multiplied by norms of $d^*_{k-1}d_{k-1}$ and its square root. Controlling these factors on the correct subspaces, rather than on all of $C^{k-1}$ , is the delicate step: $d^*_{k-1}d_{k-1}=(k+1)M^+_{k-1}$ has norm $k+1$ on $C^{k-1}(X)$ , attained on the constants, and the bound needed is on the complement of the constants. Passing from Corollary 5.8 to the spectral statement of Theorem 5.9 needs the intervals to be disjoint and the eigenvector to be split along the orthogonal decomposition.

Formalization scope

Encoding. Faces are Finset V and $X$ is a Finset (Finset V); faces are indexed by their number of vertices (cells X (k + 1) is $X(k)$ ). Cochains are functions Finset V → ℝ, and every operator vanishes off $X$ .
Supports. Subspaces, eigenvectors and orthogonal complements consist of functions supported on $X(k)$ (Supp X (k + 1)). Without this, a function living off the faces would have norm $0$ , would be an eigenvector with eigenvalue $0$ , and would make the spectral statement false; a formalization without supports is ruled out for this reason.
Weights and adjoints. The weight is strictly positive on faces. $d^*$ is defined by its explicit formula, and Lemma 3.6 states that this formula is the adjoint.
Expansion. The eigenvalue conditions on links are stated in Rayleigh form on the weighted complement of the constants, $|\langle(M')^+_{\tau,0}g,g\rangle|\le\lambda\|g\|^2$ ; this encodes $-\lambda\le\nu_\tau$ and $\mu_\tau\le\lambda$ and needs no connectivity. Definition 1.2 is followed where Definition 4.4 misprints the two-sided clause.
Projections. $P_U\phi$ is characterised relationally (IsWProj: $u\in U$ and $\phi-u\perp U$ ) instead of by an operator. On these finite-dimensional subspaces it exists and is unique.
Indices and constants. $\varepsilon_k$ is eps lam k, with the recursion shifted by one index. $k$ is quantified inside each conclusion, and $\varepsilon_{n-1}$ is written without natural subtraction. The statements follow the printed constants of arXiv v3.

A complete development needs finite-dimensional weighted inner-product spaces of cochains, Garland localization, Courant–Fischer for self-adjoint operators on these spaces, and orthogonal projections onto images of iterated differentials. The cochain calculus and the localization identities are reusable for any weighted simplicial complex, and the first mission of this series needs the same objects. Proofs of the localization identities, of the decomposition, and of any milestone are welcome, as are proofs of the results with weaker hypotheses.

Selected references

T. Kaufman, I. Oppenheim, High Order Random Walks: Beyond Spectral Gap, arXiv:1707.02799v3, 2021. https://arxiv.org/abs/1707.02799
H. Garland, p-adic curvature and the cohomology of discrete subgroups of p-adic groups, Annals of Mathematics 97, 1973. https://doi.org/10.2307/1970833
T. Kaufman, D. Mass, High dimensional random walks and colorful expansion, ITCS 2017. https://arxiv.org/abs/1604.02947
I. Oppenheim, Local spectral expansion approach to high dimensional expanders Part I: Descent of spectral gaps, Discrete & Computational Geometry 59, 2018. https://arxiv.org/abs/1709.04431
N. Anari, K. Liu, S. Oveis Gharan, C. Vinzant, Log-concave polynomials II: high-dimensional walks and an FPRAS for counting bases of a matroid, STOC 2019. https://arxiv.org/abs/1811.01816
V. L. Alev, L. C. Lau, Improved analysis of higher order random walks and applications, STOC 2020. https://arxiv.org/abs/2001.02827

15 thms2 active usersReviewed

Combinatorics Markov Chain Theoretical Computer Science·Captain: mikedeng1

High Order Random Walks: Beyond Spectral Gap 1: On a One-Sided λ-Local Spectral Expander, ‖M⁺_k φ‖ ≤ ((k+1)/(k+2) + (k+1)λ/2)‖φ‖ for Every k-Cochain φ Orthogonal to the ConstantsResearch Paper

Motivation

A high dimensional expander is a simplicial complex whose local structure forces global expansion. The high order random walks on such a complex move from a $k$ -face to a $k$ -face through a common $(k+1)$ -face. They were studied for their connection to agreement tests in probabilistically checkable proofs (Dinur–Kaufman 2017; Kaufman–Mass 2017), and they later became a tool for sampling. Anari, Liu, Oveis Gharan and Vinzant (arXiv:1811.01816) used the mixing bound of this mission to prove the Mihail–Vazirani conjecture: the bases-exchange walk of every matroid mixes rapidly.

Timeline:

1973. Garland (Ann. of Math. 97) shows that spectral gaps in the links of a complex control its cohomology. Inner products are localized to links; this is now called Garland's method.
2017. Kaufman and Mass (arXiv:1604.02947) bound the second eigenvalue of the high order walks on complexes with well-expanding links. Dinur and Kaufman obtain the optimal bound under a two-sided spectral gap in the links, as Kaufman–Oppenheim explain.
2018. Oppenheim (Discrete Comput. Geom. 59) shows how spectral gaps descend from top-dimensional links to lower ones ("trickling down").
2017–2021. Kaufman and Oppenheim (arXiv:1707.02799v3) obtain the optimal mixing bound under a one-sided gap only: negative eigenvalues of the links do not matter. This is the target of this mission.

Setting

Let $V$ be a type of vertices. A pure $n$ -dimensional finite simplicial complex $X$ is a finite family of finite subsets of $V$ that is closed under subsets, has faces of at most $n+1$ elements, and has every face contained in a face of exactly $n+1$ elements. A face with $k+1$ elements is a $k$ -face; $X(k)$ is the set of $k$ -faces, and $X(-1)=\{\emptyset\}$ .

A weight function is a map $m$ from the faces of $X$ to $(0,\infty)$ that is balanced: for $-1\le k\le n-1$ and $\tau\in X(k)$ ,

m(\tau)=\sum_{\sigma\in X(k+1),\ \tau\subseteq\sigma}m(\sigma).

A $k$ -cochain is a function $\phi:X(k)\to\mathbb R$ . The cochains carry the inner product $\langle\phi,\psi\rangle=\sum_{\sigma\in X(k)}m(\sigma)\phi(\sigma)\psi(\sigma)$ and the norm $\|\cdot\|$ . The cochains orthogonal to the constants form $C^k_0(X,\mathbb R)=\{\phi:\sum_{\sigma\in X(k)}m(\sigma)\phi(\sigma)=0\}$ .

The upper random walk $M^+_k$ acts on $k$ -cochains by

M^+_k\phi(\tau)=\frac{1}{k+2}\,\phi(\tau)+\sum_{\tau'\in X(k),\ \tau\cup\tau'\in X(k+1)}\frac{m(\tau\cup\tau')}{(k+2)\,m(\tau)}\,\phi(\tau').

It stays put with probability $1/(k+2)$ , and otherwise moves to a neighbouring $k$ -face with probability proportional to the weight of their union.

The link of a face $\tau$ is $X_\tau=\{\eta\in X:\eta\cap\tau=\emptyset,\ \tau\cup\eta\in X\}$ , weighted by $m_\tau(\eta)=m(\tau\cup\eta)$ . On the vertices of $X_\tau$ , the non-lazy upper walk $(M')^+_{\tau,0}=2M^+_{\tau,0}-I$ is the weighted random walk on the 1-skeleton of the link. Let $\mu_\tau$ be its second largest eigenvalue. $X$ is a one-sided $\lambda$ -local spectral expander if $\mu_\tau\le\lambda$ for every face $\tau$ of dimension $-1,\dots,n-2$ . The empty face is included, and its link is $X$ itself.

Formalization targets

Goal: Theorem 5.4 (p. 17)

Let $0\le\lambda\le1$ and let $X$ be a one-sided $\lambda$ -local spectral expander. Then for every $0\le k\le n-1$ and every $\phi\in C^k_0(X,\mathbb R)$ ,

\|M^+_k\phi\|\le\Big(\frac{k+1}{k+2}+\frac{k+1}{2}\,\lambda\Big)\|\phi\|.

Milestones

They follow the paper's proof order:

Lemma 3.6 and Corollary 3.7: the adjoint $d^*$ of the signless differential $d$ , and the factorizations $d^*d=(k+2)M^+_k$ , $dd^*=(k+1)M^-_k$ .
Proposition 4.1 (1)–(3), Garland's localization identities, and Proposition 4.2:

\|d\phi\|^2=\|d^*\phi\|^2+\|\phi\|^2+\sum_{\tau\in X(k-1)}\langle (M')^+_{\tau,0}(I-M^-_{\tau,0})\phi_\tau,\phi_\tau\rangle .

Lemma 4.3, which bounds the link terms by $(k+1)\mu\|\phi\|^2$ .
Lemma 5.1.
Theorem 5.2 (the Decomposition Theorem).
Corollary 5.3, in its general and its one-sided form:

\|d\phi\|^2\le\sum_{j=0}^{k}\Big(k+1-j+\frac{(k+j+2)(k+1-j)}{2}\lambda\Big)\|\phi^j\|^2,\qquad \|\phi\|^2=\sum_{j=0}^k\|\phi^j\|^2.

Significance

The result. The coefficient $\frac{k+1}{k+2}$ is the baseline in the paper's mixing bound, and the bound is optimal up to the $O(\lambda)$ term. It needs a gap on one side only: links may have eigenvalues near $-1$ . This matters in two places. The links of a matroid's independence complex are only one-sided expanders, so the matroid application needs exactly this case. And the links of Ramanujan complexes are one-sided expanders, so this bound gives optimal mixing on them; the two-sided bound of Dinur–Kaufman does not apply to them.

Formalizing it. The theorem is proved on paper; the Lean statements in this mission are proof targets. Completing the mission would give machine-checked proofs of the mixing bound, Garland's localization identities, and the Decomposition Theorem, built on definitions of weighted simplicial complexes, links, and their random walks. Lemma 4.3 and Corollary 5.3 are stated with a correction: as printed they are false when a link eigenvalue bound is negative (see Formalization scope).

Difficulty

The obvious argument fails. The tempting route bounds the second eigenvalue of $M^+_k$ directly from the link spectra, by induction on $k$ . But $M^+_k$ has large eigenvalues near $\frac{k+1-j}{k+2}$ for every $j$ , coming from cochains of the form $d\psi$ with $\psi$ of lower degree. A single spectral-gap estimate cannot separate these levels from one another. The paper instead splits $\phi$ into contributions from every degree $j\le k$ ; this is the Decomposition Theorem, and each piece is controlled separately. Formally, the main costs are:

the double-counting behind Proposition 4.1 (Appendix A, pp. 28–29);
a square root of a positive self-adjoint operator on a weighted finite-dimensional space (Theorem 5.2);
the bookkeeping of degrees and links.

Formalization scope

Faces are Finset V. $X$ is a Finset (Finset V), and $X(k)$ is cells X (k + 1): faces are indexed by their number of vertices. Cochains are functions Finset V → ℝ that are read only on the relevant faces. Every operator is zero off $X$ . The weight is positive on faces; the paper writes $\mathbb R^+$ , and $m$ appears in denominators. Every goal-level statement carries the standing assumption of §2: $X$ is pure $n$ -dimensional and $m$ is a weight. Orthogonality to the constants is always weighted by $m$ (or by $m_\tau$ in a link).

The adjoint $d^*$ is defined by its explicit formula; that it is the adjoint is Lemma 3.6. The eigenvalue condition $\mu_\tau\le\lambda$ is stated in Rayleigh form: $\langle (M')^+_{\tau,0}g,g\rangle\le\lambda\|g\|^2$ for every $g$ on the vertices of $X_\tau$ that is $m_\tau$ -orthogonal to the constants. It is equivalent to the eigenvalue form even for disconnected links. A Rayleigh bound over all $g$ , constants included, would be unsatisfiable for $\lambda<1$ and would make the goal vacuous; it is ruled out. The predicate quantifies over every face of dimension $-1$ to $n-2$ , including $\emptyset$ .

Corrections, all disclosed in the items:

Lemma 4.3 is stated with a bound $\mu\ge\max(\mu_k,0)$ . The printed version with $\mu_k<0$ fails already for the complete graph on three vertices.
Corollary 5.3 accordingly takes $\mu_i\ge0$ and $\lambda\ge0$ . Its two formal statements retain the page's assumption that every link of dimension at least one is connected, including $X$ itself.
The proof of Theorem 5.4 ends with $(k+1)\lambda$ ; the statement's $\frac{k+1}{2}\lambda$ is formalized.

Welcome contributions: proofs of any milestone. Reusable lemmas on finite weighted inner products, on double counting over faces of a Finset (Finset V), and on links are useful beyond this mission; the companion mission on two-sided expanders uses the same objects.

Selected references

T. Kaufman, I. Oppenheim, High Order Random Walks: Beyond Spectral Gap, arXiv:1707.02799v3, 2021. https://arxiv.org/abs/1707.02799
N. Anari, K. Liu, S. Oveis Gharan, C. Vinzant, Log-concave polynomials II: High-dimensional walks and an FPRAS for counting bases of a matroid, STOC 2019. https://arxiv.org/abs/1811.01816
H. Garland, p-adic curvature and the cohomology of discrete subgroups of p-adic groups, Ann. of Math. 97:375–423, 1973. https://doi.org/10.2307/1970781
T. Kaufman, D. Mass, High dimensional random walks and colorful expansion, ITCS 2017. https://arxiv.org/abs/1604.02947
I. Oppenheim, Local spectral expansion approach to high dimensional expanders Part I: Descent of spectral gaps, Discrete Comput. Geom. 59(2):293–330, 2018. https://arxiv.org/abs/1709.04431

13 thms2 active usersReviewed

Mathematical Physics Quantum Information·Captain: mikedeng1

Quantum Algorithm for Simulating Real Time Evolution of Lattice Hamiltonians 2: Strictly Local Lieb–Robinson Bound ‖[A_X(t),B_Y]‖ ≤ 2‖A‖‖B‖|X|(2ζ₀|t|)^ℓ/ℓ! with ℓ = ⌊dist(X,Y)⌋Research Paper

Motivation

Simulating the time evolution $e^{-iHt}$ of a many-body Hamiltonian is one of the main proposed uses of quantum computers. For a Hamiltonian $H = \sum_X h_X$ whose terms act on small, nearby groups of sites of a lattice, Haah, Hastings, Kothari and Low give a quantum algorithm whose gate count is nearly linear in the space-time volume $n t$ , and show that this is optimal up to logarithmic factors. The algorithm decomposes $e^{-iHt}$ into evolutions of overlapping blocks, and the error of each step is controlled by a Lieb–Robinson bound: in a locally interacting system, an operator evolved for time $t$ stays, up to a superexponentially small error, inside a region whose size grows linearly with $t$ .

Lieb–Robinson bounds go back to Lieb and Robinson (1972), who proved a finite propagation speed for quantum spin systems. Hastings (2004), Nachtergaele and Sims (2006) and Hastings and Koma (2006) gave the commutator form used today and applied it to the decay of correlations in gapped ground states. Appendix C of the paper re-derives the bound in a self-contained way. Section C.4 treats strictly local interactions, where every term is supported on a set of diameter at most $1$ , and obtains a bound with an explicit factor $(2\zeta_0|t|)^\ell/\ell!$ . This mission formalizes that bound.

Setting

Let $\Lambda$ be a finite set of sites with a metric $\mathrm{dist}$ . Every site carries $\mathbb{C}^q$ , and operators act on $\bigotimes_{x \in \Lambda} \mathbb{C}^q$ ; all norms $\|\cdot\|$ are operator norms. An operator is supported on $X \subseteq \Lambda$ if it has the form $m \otimes \mathbb{1}_{\Lambda \setminus X}$ . For finite sets of sites, $\mathrm{dist}(X, Y) = \min_{x \in X, y \in Y} \mathrm{dist}(x, y)$ , $\mathrm{diam}(X) = \max_{x, x' \in X} \mathrm{dist}(x, x')$ , and $X \sim Y$ means $X \cap Y \ne \emptyset$ .

A Hamiltonian is a family $(h_X)_{X \subseteq \Lambda}$ of Hermitian operators, $h_X$ supported on $X$ , with $H = \sum_{X \subseteq \Lambda} h_X$ ; for a region $\Omega$ , $H_\Omega = \sum_{Z \subseteq \Omega} h_Z$ . The Heisenberg evolution of an operator $O$ is $O(t; J) = e^{iJt} O e^{-iJt}$ , and $O(t) = O(t; H)$ . The interaction is strictly local if $h_X = 0$ whenever $\mathrm{diam}(X) > 1$ , and its strength is measured by

\zeta_0 = \max_{x \in \Lambda} \sum_{Q \ni x} |Q|\, \|h_Q\| .

The proof works with two auxiliary quantities attached to a fixed operator $B$ supported on $Y$ :

C_B(X, t) = \sup_{A \in \mathcal{A}_X,\ \|A\| \le 1} \|[A(t), B]\|, \qquad D_B(X, t) = \|[h_X(t), B]\|,

where $\mathcal{A}_X$ is the algebra of operators supported on $X$ . A tuple $(Z_1, \dots, Z_k)$ is linked from $X$ if $X \sim Z_1 \sim \cdots \sim Z_k$ .

Formalization targets

Goal: display (48)

For $A$ supported on $X$ , $B$ supported on $Y$ , $\ell = \lfloor \mathrm{dist}(X, Y) \rfloor$ and every real $t$ ,

\|[A(t), B]\| \le 2\,\|A\|\,\|B\|\,|X|\,\frac{(2\zeta_0|t|)^{\ell}}{\ell!} .

Milestones

The elementary bounds (28): $C_B(Z, 0) \le 2\|B\|\delta_{Z \sim Y}$ , $C_B(Z, t) \le 2\|B\|$ , and the same for $D_B$ with an extra factor $\|h_Z\|$ .
The integral inequality (24): $C_B(X, t) \le C_B(X, 0) + \sum_{Z \sim X} 2\int_0^{|t|} D_B(Z, s)\, ds$ .
The closed recursion (42): $C_B(X, t) \le C_B(X, 0) + 2\sum_{Z : X \sim Z} \|h_Z\| \int_0^{|t|} C_B(Z, s)\, ds$ .
The truncated iteration (44): $C_B(X, t) \le 2\|B\| \frac{(2|t|)^\ell}{\ell!} \sum_{Z_1, \dots, Z_\ell : \text{linked}} \prod_j \|h_{Z_j}\|$ .
The counting bounds (45)–(46): $\sum_{Q : P \sim Q \sim S} \|h_Q\| \le \zeta_0 \sum_{p \in P} \delta_{\mathrm{dist}(p, S) \le 1}$ and its weighted, distance-tracking companion.
Lemma 5, eq. (4) = (49): $\|O_X(t; H) - O_X(t; H_\Omega)\| \le |X|\,\|O_X\|\,(2\zeta_0|t|)^\ell/\ell!$ with $\ell = \lfloor \mathrm{dist}(X, \Lambda \setminus \Omega) \rfloor$ , under the added hypothesis $\mathrm{dist}(X, \Lambda \setminus \Omega) \ge 1$ .

The goal is (48) rather than Lemma 5 because (48) is proved in full on pp. 26–27, while Lemma 5 is obtained "by manipulation analogous to Eq. (39)" and is false as printed when $\ell = 0$ .

Significance

The bound (48) states that commutators with distant operators are suppressed by a factor that, at fixed $t$ , decays faster than any exponential in the distance. The same factor controls Lemma 5, which is what the decomposition lemmas of the paper (Lemma 6 and its corollaries) use to bound the error of replacing a global evolution by evolutions of overlapping blocks; that in turn gives the paper's gate counts. Bounds of this type also underlie the exponential clustering of correlations in gapped ground states and the quasi-adiabatic continuation technique.

The results are proved in the literature and in this paper. A search of the local Prove2Me prior-art index found no matching formal statement for this finite spin-system bound. The mission seeks a machine-checked proof of the strictly local bound with its explicit constant, together with reusable infrastructure: operators supported on subsets of a tensor product of matrix algebras, their Heisenberg evolution, and an integral inequality for commutator growth.

Difficulty

The obvious argument expands $A(t) = \sum_k (it)^k \mathrm{ad}_H^k(A)/k!$ and notes that the first $\ell$ nested commutators with $B$ vanish. This does not give the stated bound: the norm of $\mathrm{ad}_H^k(A)$ grows like $k!$ times the number of growing clusters of terms, and the tail of the series is not controlled by its leading term. The explicit factor $(2\zeta_0|t|)^\ell/\ell!$ , with no exponential prefactor, requires precise control of the time-dependent supremum $C_B(Z,s)$ and the combinatorics of linked chains. A second difficulty is Lemma 5, whose printed form is false at $\ell = 0$ and whose proof in the paper is a one-line reference to an analogous computation.

Formalization scope

Sites are an arbitrary finite metric space $\Lambda$ ([Fintype Λ] [MetricSpace Λ]); operators are matrices Matrix (Λ → Fin q) (Λ → Fin q) ℂ in the product basis, with the same local dimension $q$ at every site. This generalizes the paper's qubits on a lattice in $\mathbb{R}^D$ . The norm is the $L^2$ operator norm (Matrix.Norms.L2Operator), never the entrywise or Frobenius norm. SupportedOn X M states $M = m \otimes \mathbb{1}$ entrywise, and is not vacuous: a nonzero operator on a single site satisfies it, and only scalars are supported on $\emptyset$ . The Hamiltonian is time-independent and sums over every subset of $\Lambda$ ; strict locality is the hypothesis $1 < \mathrm{diam}(X) \Rightarrow h_X = 0$ on the terms. The constant $\zeta_0$ is carried as an upper bound of the site sums $\sum_{Q \ni x} |Q|\,\|h_Q\|$ , which is equivalent to the paper's maximum for these monotone bounds; no bound $\|h_X\| \le 1$ is assumed. $\mathrm{dist}(X, Y)$ is a minimum over nonempty sets and $0$ if a set is empty, $\ell$ is its natural-number floor, and $C_B$ is a real supremum over a nonempty set bounded by $2\|B\|$ . The integral milestones (24) and (42) are stated for $t \ge 0$ ; the goal, (44) and Lemma 5 hold for every real $t$ . Lemma 5 carries one disclosed added hypothesis, $\mathrm{dist}(x, y) \ge 1$ for $x \in X$ , $y \notin \Omega$ , without which it is false.

None of the statements is trivialized: the goal mentions neither $C_B$ nor linked sums, its norm is the operator norm, the integrals are of continuous functions on compact intervals, the supremum is over a nonempty bounded set, and no disjointness of $X$ and $Y$ is assumed, so it covers $\ell = 0$ as well.

A complete development needs the derivative of $t \mapsto e^{iHt} A e^{-iHt}$ , unitarity of $e^{iHt}$ for Hermitian $H$ , commutation of operators with disjoint supports, Grönwall-type iteration of integral inequalities, and the simplex-volume identity $\int_{\Delta^k} dt = |t|^k/k!$ . The support and evolution layer is reusable for any lattice-system result. Contributions that prove the milestones in order, or that develop the support calculus independently, are welcome.

Selected references

J. Haah, M. B. Hastings, R. Kothari, G. H. Low, Quantum algorithm for simulating real time evolution of lattice Hamiltonians, SIAM J. Comput. (2021); arXiv:1801.03922v4 (2020). https://arxiv.org/abs/1801.03922
E. H. Lieb, D. W. Robinson, The finite group velocity of quantum spin systems, Comm. Math. Phys. 28 (1972) 251–257. https://doi.org/10.1007/BF01645779
M. B. Hastings, Lieb–Schultz–Mattis in higher dimensions, Phys. Rev. B 69 (2004) 104431. https://arxiv.org/abs/cond-mat/0305505
B. Nachtergaele, R. Sims, Lieb–Robinson bounds and the exponential clustering theorem, Comm. Math. Phys. 265 (2006) 119–130. https://arxiv.org/abs/math-ph/0506030
M. B. Hastings, T. Koma, Spectral gap and exponential decay of correlations, Comm. Math. Phys. 265 (2006) 781–804. https://arxiv.org/abs/math-ph/0507008

10 thms2 active usersReviewed

Computational Geometry Machine Learning·Captain: mikedeng1

Turning Big Data into Tiny Data: Constant-Size Coresets for k-Means, PCA, and Projective Clustering I: The Rank-m SVD Truncation Plus Its Residual Preserves the Cost of Every j-Dimensional ShapeResearch Paper

Motivation

Large data sets make clustering and subspace fitting expensive because a candidate solution must be evaluated against every input point. A dimensionality reduction replaces the data by a lower-rank matrix whose costs approximate those of the original input for an entire class of candidate solutions. Feldman, Schmidt, and Sohler study reductions that retain enough information for $k$ -means, principal component analysis, and projective clustering. Their journal paper identifies a rank truncation and one residual scalar that preserve the fitting cost of every shape lying in a low-dimensional linear subspace Feldman, Schmidt, and Sohler (2020), Theorem 22.

The published article also records that some coreset sizes in its 2013 conference version were incorrect. This mission uses the 2020 journal statement and its page numbering throughout. The authors cite earlier SVD-based approximations to $k$ -means on p. 613, while their Theorem 22 gives a uniform cost guarantee for arbitrary nonempty shapes contained in a $j$ -dimensional subspace Feldman, Schmidt, and Sohler (2020), pp. 603, 613, 620.

Setting

The input is a real matrix $A\in\mathbb R^{n\times d}$ . Its $n$ rows are points in $\mathbb R^d$ . For a nonempty set of candidate locations or shapes $C\subseteq\mathbb R^d$ , let $\operatorname{dist}(a_i,C)$ be the infimum of Euclidean distances from row $a_i$ to points of $C$ . The shape cost is

\operatorname{dist}^2(A,C)=\sum_{i=1}^{n}\operatorname{dist}(a_i,C)^2.

The set $C$ need not be closed and need not be a subspace. For example, it can be a finite set of cluster centers. The restriction is that all of its points lie in some linear subspace of dimension $j$ . This matches the paper's shape class in §5; the affine case is treated separately Feldman, Schmidt, and Sohler (2020), pp. 619–620.

Fix a singular value decomposition $A=U\Sigma V^T$ , where $U$ and $V$ are orthogonal and the diagonal entries of the rectangular matrix $\Sigma$ are nonnegative and nonincreasing. The entry $\sigma_i$ is indexed from one. The rank- $m$ truncation $A^{(m)}=U\Sigma^{(m)}V^T$ keeps the first $m$ diagonal entries and sets the rest to zero. Its squared Frobenius residual is $\Delta=\|A-A^{(m)}\|_F^2$ . The corrected cost of $C$ is $\operatorname{dist}^2(A^{(m)},C)+\Delta$ Feldman, Schmidt, and Sohler (2020), Definition 1 and §2.

Formalization targets

Linear subspace estimates

The milestones first record the matrix Pythagorean identity, the $j\sigma_{m+1}^2$ projection and residual bounds, and the lower bound on the cost of a linear $j$ -subspace. They then state the residual-corrected approximation in Corollary 16:

\|AY\|_F^2\le\|A^{(m)}Y\|_F^2+\Delta\le(1+\varepsilon)\|AY\|_F^2, \qquad m\ge\lceil j/\varepsilon\rceil+j-1.

Here $Y$ has $d-j$ orthonormal columns spanning the complement of the candidate subspace. Corollary 20, Corollary 21, and display (9) connect these linear estimates to costs of general sets $C$ Feldman, Schmidt, and Sohler (2020), pp. 604, 613–615, 619–620.

Goal: uniform shape-cost preservation

The goal is Theorem 22. For $1\le j\le d-1$ , $0<\varepsilon\le1$ , and $\lceil8j/\varepsilon^2\rceil-1\le m\le\min\{n,d\}-1$ , every nonempty $C$ contained in a linear $j$ -dimensional subspace satisfies

\left|\bigl(\operatorname{dist}^2(A^{(m)},C)+\|A-A^{(m)}\|_F^2\bigr) -\operatorname{dist}^2(A,C)\right| \le\varepsilon\operatorname{dist}^2(A,C).

The quantifier over $C$ makes this a guarantee for every admissible candidate on the same reduced data, rather than a statement about one selected optimum Feldman, Schmidt, and Sohler (2020), Theorem 22, p. 620.

Significance

The theorem preserves objective values after replacing $A$ by a rank- $m$ matrix and one number. For a fixed $j$ and accuracy parameter, the rank threshold depends on $j$ and $\varepsilon$ , with no direct dependence on the number of points $n$ or ambient dimension $d$ except the upper bound on feasible $m$ . In the paper, the result leads to a guarantee for $k$ -means candidates, since $k$ centers span a linear subspace of dimension at most $k$ Feldman, Schmidt, and Sohler (2020), Corollary 23, p. 621.

The result is proved in the paper, but this mission's Lean theorems are posed with sorry; they do not yet have machine-checked proofs. A completed development would connect a reusable rectangular SVD model, matrix projection identities, infimum distances to arbitrary nonempty sets, and a uniform cost inequality. The SVD definition is already published in the platform library; the row-cost and singular-value conventions here supply the interface needed for this paper Feldman, Schmidt, and Sohler (2020), §§2, 3, 5.

Difficulty

The linear subspace bound compares a projection cost with a tail sum of squared singular values. The paper recalls that fact in §3 without proving it, so the formal development needs a suitable singular-value inequality or a derivation from existing matrix approximation results. For general shapes $C$ , a bound on the cost of one linear subspace does not by itself control the distance from each projected point to every point of $C$ . The remaining milestones state the projection error, the squared-distance perturbation bound, and the Pythagorean cost split that address that gap Feldman, Schmidt, and Sohler (2020), pp. 613, 619–621.

The proof printed after Theorem 22 invokes earlier corollaries under a stronger rank threshold than the theorem states. The mission keeps the printed theorem threshold, whose claim remains valid; a formal proof must bridge that discrepancy Feldman, Schmidt, and Sohler (2020), pp. 620–621.

Formalization scope

Matrices are Matrix (Fin n) (Fin d) ℝ, and rows are points of EuclideanSpace ℝ (Fin d). Squared Frobenius norm is an explicit finite sum of squared entries. Shape cost sums squared Metric.infDist values over rows. Since Mathlib assigns a real default value to distance from the empty set while the paper assigns infinity, every theorem about a general shape $C$ requires C.Nonempty. This is the page's own requirement for Theorem 22 and Corollary 21, and is also needed for display (9).

The SVD and its truncation use the published ProjLikeRetr.FixedRank.IsSVD and truncSVD. Every SVD statement quantifies over an arbitrary valid triple $(U,\Sigma,V)$ ; tied singular values do not fix a unique truncation. The local $\sigma_i$ is one-based, while truncSVD m keeps zero-based diagonal positions below $m$ . Orthonormal columns of $X$ satisfy $X^TX=I$ , their orthogonal complement has $d-j$ columns, and projection in ambient coordinates is $AXX^T$ . Theorem 22 quantifies over arbitrary nonempty $C$ contained in a linear $j$ -subspace; it does not restrict $C$ to subspaces or replace linear containment by affine containment.

The integer inequalities in Lean use additive forms such as $\lceil8j/\varepsilon^2\rceil\le m+1$ to avoid truncated natural-number subtraction. The theorem retains the printed $m$ threshold, including the proof gap described above. Running-time clauses are outside the mission's mathematical statements. Contributions are welcome toward the singular-value lower bound, the projection and infimum-distance identities, and the final uniform inequality; the matrix and distance definitions are reusable in the companion affine-subspace mission.

Selected references

Dan Feldman, Melanie Schmidt, and Christian Sohler, Turning Big Data into Tiny Data: Constant-Size Coresets for k-Means, PCA, and Projective Clustering, SIAM Journal on Computing 49(3):601–657, 2020. DOI: 10.1137/18M1209854.

11 thms2 active usersReviewed

Completed

Numerical Analysis Optimization Theoretical Computer Science·Captain: mikedeng1

Low Rank Approximation and Regression in Input Sparsity Time 2: Sketched Multiple-Response Regression Is (1 + 4ε)-Optimal in Squared Error If the Sketch Embeds the Subspace and Approximates ProductsResearch Paper

Motivation

Least-squares regression, $\min_X\|AX-B\|_F$ for a tall matrix $A\in\mathbb R^{n\times d}$ with $n\gg d$ , is among the most frequently solved problems in numerical computation. Direct methods (QR or SVD) cost $O(nd^2)$ time, which is prohibitive when $n$ is in the millions. Sketching replaces the problem by a much smaller one: choose a matrix $S\in\mathbb R^{t\times n}$ with $t\ll n$ , form $SA$ and $SB$ , and solve $\min_X\|S(AX-B)\|_F$ instead. The question is when the solution of the small problem is nearly optimal for the original one.

Clarkson and Woodruff, Low Rank Approximation and Regression in Input Sparsity Time (STOC 2013; JACM 2017), showed that a very sparse random sketch (one non-zero per column, the CountSketch matrix) can be applied in time proportional to the number of non-zero entries of $A$ and still yields $(1+\varepsilon)$ -approximate regression and low-rank approximation. §7 of that paper isolates the deterministic part of the argument: two conditions on a fixed sketch $S$ that guarantee a near-optimal solution, whatever distribution produced $S$ .

Timeline. Sarlós (FOCS 2006) introduced sketch-and-solve regression with fast Johnson–Lindenstrauss transforms. Drineas, Mahoney, Muthukrishnan and Sarlós (Numer. Math. 2011) stated the structural conditions for single-response regression (their Lemma 1); Theorem 36 of Clarkson–Woodruff generalizes it to multiple responses. Clarkson and Woodruff then supplied the sparse sketches meeting the conditions in input-sparsity time.

Setting

All matrices are real. For a vector $v$ let $\|v\|_2^2=\sum_iv_i^2$ ; for a matrix $M$ let $\|M\|_F^2=\sum_{i,j}M_{ij}^2$ . Fix $A\in\mathbb R^{n\times d}$ of rank at most $r$ , a right-hand side $B\in\mathbb R^{n\times d'}$ and a sketch $S\in\mathbb R^{t\times n}$ . Let $C(A)=\{Ax\}$ be the column space and $U\in\mathbb R^{n\times k}$ a matrix with orthonormal columns ( $U^\top U=I$ ) spanning $C(A)$ .

$Y^*$ is a least-squares minimizer: it minimizes $\|AY-B\|_F^2$ (problem (8)).
$\tilde Y$ is a sketched minimizer: it minimizes $\|S(AY-B)\|_F^2$ (problem (7)).
$S$ is a subspace embedding for $A$ with parameter $\eta$ if $\bigl|\|SAx\|_2^2-\|Ax\|_2^2\bigr|\le\eta\|Ax\|_2^2$ for every $x$ .
$S$ satisfies the approximate matrix multiplication event (Lemma 32) for a pair $(U,W)$ with error parameter $e$ if $\|U^\top S^\top SW-U^\top W\|_F^2\le e^2\|U\|_F^2\|W\|_F^2$ .

Formalization targets

Goal: Theorem 36 (p. 24)

If $S$ is a subspace embedding for $A$ with $0\le\eta\le1/2$ and satisfies the event of Lemma 32 for $(U,B-AY^*)$ with error parameter $\sqrt{\varepsilon/r}$ , then every sketched minimizer satisfies

\|A\tilde Y-B\|_F^2\le(1+4\varepsilon)\|AY^*-B\|_F^2 .

This is the explicit form the paper's proof establishes; the printed $(1+\epsilon)$ bound on norms follows after rescaling $\varepsilon$ .

Milestones

Fact 34 (Pythagorean theorem): $C^\top D=0\Rightarrow\|C+D\|_F^2=\|C\|_F^2+\|D\|_F^2$ .
Fact 35 (normal equations): $C^-D$ is a minimizer; every minimizer $X^*$ satisfies $C^\top(CX^*-D)=0$ and $\|CX-D\|_F^2=\|C(X-X^*)\|_F^2+\|CX^*-D\|_F^2$ .
Lemma 37: for $A$ with orthonormal columns, $\|A(\tilde Y-Y^*)\|_F\le2\sqrt\varepsilon\|B-AY^*\|_F$ .
Theorem 39 (affine embeddings, an independent companion result of §7.5): under an embedding with parameter $\varepsilon\le1/2$ and the event of Lemma 32 with parameter $\varepsilon/\sqrt r$ , $\|S(AX-B)\|_F^2-\|S\tilde B\|_F^2$ equals $\|AX-B\|_F^2-\|\tilde B\|_F^2$ up to $\pm2\varepsilon\|AX-B\|_F^2$ for all $X$ , and $\|S(AX-B)\|_F^2=(1\pm3\varepsilon)\|AX-B\|_F^2$ if $S$ also preserves $\|\tilde B\|_F^2$ to $1\pm\varepsilon$ .

Significance

Theorem 36 separates the algorithm design for sketched regression from its correctness proof: any random construction (CountSketch, subsampled randomized Hadamard transforms, leverage-score sampling, Gaussian matrices) yields a $(1+O(\varepsilon))$ -approximate regression solver once it is shown to satisfy the two conditions with constant probability. Clarkson and Woodruff use it for their input-sparsity-time regression algorithm (Theorem 38) and, through Theorem 39 and affine embeddings, for low-rank approximation. The same conditions recur throughout the randomized numerical linear algebra literature (see Woodruff's survey Sketching as a Tool for Numerical Linear Algebra, 2014).

The results are proved in the paper (§7.3, §7.5 and Appendix A, p. 37). To our knowledge none has a machine-checked proof. Formalizing them produces a reusable, distribution-free layer of sketching theory: the probabilistic statements about specific sketches can then be proved separately and composed with it.

Difficulty

The obvious argument applies the subspace embedding to the residual $A\tilde Y-B$ , but that vector does not lie in $C(A)$ , so an embedding of $C(A)$ alone says nothing about it; embedding $C(A)$ augmented with the columns of $B$ instead costs a sketch dimension that grows with $d'$ . The hypotheses of Theorem 36 control the optimal residual $B-AY^*$ only through the approximate-product condition, which is far weaker than norm preservation, and the difficulty is to transfer that control to the sketched solution (Lemma 37) with the constants $2\sqrt\varepsilon$ and $1+4\varepsilon$ . A second obstacle is the passage from a general $A$ of rank at most $r$ to an orthonormal basis $U$ of $C(A)$ : it changes $\|A\|_F$ , which is why the approximate-product condition is stated for $U$ .

Formalization scope

Matrices are Matrix (Fin m) (Fin n) ℝ; squared norms are explicit sums sqNorm and frobSq; the column space is the range of Matrix.mulVecLin; rank is Matrix.rank. Everything is deterministic: $S$ is an arbitrary fixed matrix and no probability space appears. The committed conventions are:

The subspace embedding is in squared form. In Theorem 36 and Lemma 37 its parameter $\eta$ plays the paper's $\epsilon_0^2$ (so $\epsilon_0\le1/\sqrt2$ becomes $\eta\le1/2$ ), which is how the proof of Lemma 37 (p. 37) uses it; in Theorem 39 the parameter is $\varepsilon$ itself, as that proof uses it.
" $S$ satisfies Lemma 32" is the event inside the probability, for the pair $(U,B-AY^*)$ (resp. $(U,\tilde B)$ ) that the proofs use, with $\le$ in place of the printed $<$ (a weaker hypothesis).
$\tilde Y$ , $Y^*$ , $X^*$ are arbitrary minimizers; "the solution" need not be unique. The Moore–Penrose inverse is specified by the four Penrose equations.
$r\ge1$ guards $\varepsilon/r$ and $\varepsilon/\sqrt r$ ; " $n>d$ " (§7) concerns running times and is not assumed.

A trivializing formalization is ruled out: $\tilde Y$ is never defined as $Y^*$ , the approximate-product hypothesis is an inequality and not the exact identity $U^\top S^\top S(B-AY^*)=0$ , $\eta$ is non-negative, and the goal is stated for general $A$ of rank at most $r$ , not only for orthonormal $A$ . The hypotheses are jointly satisfiable (for instance $S=I$ ).

A complete development needs the Frobenius inner product and its Pythagorean identity, the normal equations for matrix least squares, the existence of the Moore–Penrose inverse, and the spectral-norm bound for a symmetric matrix from its quadratic form; all are reusable beyond this mission. Proofs of any milestone, and alternative arguments for Theorem 36, are welcome.

Selected references

K. L. Clarkson and D. P. Woodruff, Low Rank Approximation and Regression in Input Sparsity Time, arXiv:1207.6365v4, 2013; J. ACM 64(6), 2017. https://arxiv.org/abs/1207.6365
P. Drineas, M. W. Mahoney, S. Muthukrishnan and T. Sarlós, Faster Least Squares Approximation, Numerische Mathematik 117(2), 2011. https://arxiv.org/abs/0710.1435
T. Sarlós, Improved Approximation Algorithms for Large Matrices via Random Projections, FOCS 2006. https://doi.org/10.1109/FOCS.2006.37
D. P. Woodruff, Sketching as a Tool for Numerical Linear Algebra, Foundations and Trends in Theoretical Computer Science 10(1–2), 2014. https://arxiv.org/abs/1411.4357

7 thms2 active usersReviewed

Numerical Analysis Probability Theoretical Computer Science·Captain: mikedeng1

Low Rank Approximation and Regression in Input Sparsity Time 1: A Sparse Embedding Matrix with O((r/ε)⁴ log²(r/ε)) Rows Is a (1 ± ε) Subspace Embedding for a Rank-r Matrix with Probability 9/10Research Paper

Motivation

Many matrix algorithms spend most of their time reading their input. A matrix with few nonzero entries should admit routines whose cost scales with that number, rather than with the product of its dimensions. Clarkson and Woodruff study random maps that compress a matrix before a regression or low rank approximation calculation while retaining the geometric information those calculations need. Their sparse embedding has one nonzero entry per input coordinate, so applying it to a sparse matrix can be charged to the matrix's nonzero entries. The probability guarantee for its geometry is Theorem 11 of the preprint, the target of this mission.

The paper proves further results for faster regression and low rank approximation after sketching. Those applications use the subspace guarantee as an input. This mission concentrates on that guarantee and the statements in §3 that support it. The source is the 5 April 2013 arXiv version; theorem and page labels below refer to that version.

Setting

Fix a real matrix $A\in\mathbb R^{n\times d}$ of rank $r$ . Its column space is $C(A)=\{Ax:x\in\mathbb R^d\}$ . A map $S:\mathbb R^n\to\mathbb R^t$ is a subspace embedding for $A$ when it approximately preserves the length of every vector in $C(A)$ simultaneously. The dimension $r$ , rather than the number of rows $n$ , controls the size required of the compressed space.

Here $S$ is the sparse embedding matrix $\Phi D$ . Each input coordinate $i$ independently chooses one bucket $h(i)\in[t]$ uniformly. The binary matrix $\Phi$ has a $1$ at $(h(i),i)$ and zero elsewhere in column $i$ . Independently, $D$ is diagonal with a fair sign $+1$ or $-1$ at each coordinate. Thus the output in bucket $j$ is the signed sum of input coordinates assigned to $j$ . The probability in this mission is over the joint, uniform choice of all bucket assignments and signs, with $A$ fixed in advance. This is the construction in §2, p. 7.

For an orthonormal basis matrix $U\in\mathbb R^{n\times r}$ of $C(A)$ , the leverage score of row $i$ is $u_i=\sum_{j=1}^r U_{ij}^2$ . A threshold $T>0$ separates light coordinates, with $u_i\le T$ , from heavy coordinates, with $u_i>T$ . The paper describes this split after sorting rows by leverage; the threshold description selects the same coordinates and keeps the input's original order. The bucket event $E_h$ bounds the sum of light leverage scores assigned to each bucket. The heavy event $E_B$ says that distinct heavy coordinates receive distinct buckets. These are properties of $h$ alone; the later concentration statements take probability over the independent signs after fixing a suitable $h$ .

Formalization targets

Sparse subspace embedding

There is an absolute constant $C>0$ such that for every $A$ of rank $r\ge1$ , every $0<\varepsilon\le1/2$ , and every integer $t\ge C(r/\varepsilon)^4\log^2(r/\varepsilon)$ ,

\Pr_{h,D}\!\left[ \forall y\in C(A),\quad \bigl|\|\Phi Dy\|_2^2-\|y\|_2^2\bigr| \le\varepsilon\|y\|_2^2 \right]\ge\frac9{10}.

The event contains the universal quantifier over $y$ : one draw must work for the whole column space. The squared-norm estimate implies the norm formulation printed in Theorem 11, p. 11 on this range of $\varepsilon$ . The paper gives its proof in §3, pp. 7–11.

Supporting targets

The milestone list follows the paper's statements: a coordinate bound from §3.1; the weighted bucket estimate of Lemma 2; light-coordinate concentration in Lemma 3; the collision and exact-preservation statement of Lemma 5; the heavy-light cross-term estimate in Lemma 6; fixed-vector preservation in Lemma 7; and the passage to the whole subspace in Lemma 8. Their distinct probability spaces matter. Lemmas 2 and 5 concern bucket assignments, Lemmas 3, 6, and 7 concern signs for a fixed suitable assignment, and Lemma 8 is a general statement about a random linear map.

Significance

Theorem 11 gives a single compact random matrix that retains the Euclidean geometry of every vector in a specified rank- $r$ column space with probability at least $9/10$ . It supports sketch-and-solve algorithms: a computation performed on $\Phi DA$ can use a much smaller row dimension while reasoning about the original column space. The construction also has exactly one nonzero per column, the structural fact behind its input-sparsity running time. The running-time bound is stated in the paper, but this mission's Lean target concerns the mathematical norm guarantee.

The paper already proves the theorem; the open work here is a machine-checked development of its statement and proof. The finite probability model, explicit squared norms, leverage scores, and bucket events can support later formalizations of other sparse sketching results. No machine-checked proof of Theorem 11 is claimed by this proposal. A complete development may reuse proved concentration inequalities from Mathlib or the platform, but the cited inequalities need their hypotheses checked against the finite-sign and weighted-bucket models used here.

Difficulty

A fixed-vector estimate does not itself imply that one random sketch works for all vectors of an uncountable subspace: the quantifier cannot simply be moved through the probability. Collisions also have different effects on high- and low-leverage coordinates. Heavy coordinates need a no-collision event; light coordinates can share buckets only while their total bucket weight remains controlled. The paper's statements keep these events and probability spaces separate. The final whole-subspace claim requires a uniform estimate whose failure probability accounts for the dimension $r$ .

Formalization scope

Vectors are functions Fin n → ℝ, matrices are finite real matrices, and $\|v\|_2^2$ and $\|M\|_F^2$ are explicit sums of coordinate squares. The sample space is the product of all bucket maps and all Boolean sign assignments, with counting probability. Every theorem with a freely chosen bucket count assumes $t>0$ ; otherwise a Fin 0 sample space could make division by its cardinality meaningless. The theorem's size threshold forces this automatically when $r\ge1$ and $0<\varepsilon\le1/2$ . Matrix rank is Mathlib's matrix rank.

The formalization fixes $0<\varepsilon\le1/2$ in Theorem 11. The upper bound prevents the logarithmic size expression from degenerating near $r=\varepsilon=1$ , and $r\ge1$ keeps its logarithm and division meaningful. Positive $T$ and $W$ are explicit where needed; Lemma 6 restricts $\delta_C\le e^{-1}$ . The heavy/light split uses leverage thresholds rather than a row permutation, and constants described as absolute are quantified before every dimension, matrix, error, and failure parameter. In particular, Theorem 11's event quantifies over all $x$ inside the probability, while Lemma 7 fixes $y$ before sampling signs. These choices exclude degenerate distributions, vacuous error ranges, and a fixed-vector claim masquerading as the goal.

The refined $t$ clause at the end of Theorem 11 is left out: its printed $s^2/30$ conflicts with the proof's collision requirement $30s^2$ , and its threshold parameter is not fixed in the claim. Lemma 1 and the cited Hanson–Wright moment result, Theorem 4, are proof tools outside this proposal's milestone set. Contributions that formalize those tools faithfully, prove the bucket and sign estimates, or connect the finite model to existing probability libraries are useful for the goal.

Selected references

Kenneth L. Clarkson and David P. Woodruff, Low Rank Approximation and Regression in Input Sparsity Time, arXiv:1207.6365v4, 2013. Preprint.

9 thms2 active usersReviewed

Missions

When Is Society Susceptible to Manipulation?: Under Any Principal Interference, Beliefs in a Mixed DeGroot–Bayesian Network Converge Almost Surely to (I − W)⁻¹(BU∞ ⊙ θ)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 11)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Quantum Singular Value Transformation and Beyond: Exponential Improvements for Quantum Matrix Arithmetics: Singular Value Transformation by Real Polynomials via Alternating Phase ModulationResearch Paper

Motivation

Setting

Formalization targets

Goal: Corollary 18 (singular value transformation by real polynomials)

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Robust Spectral Clustering Algorithm for Sub-Gaussian Mixture Models with Outliers 2: Spectral Rounding Without Outliers Gives Σ|S_k|/n_k ≤ 64(2+ε)‖X⁰ − X̂‖₁/n²minResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2, (15), without outliers

Milestones

Companion: permutation recovery

Significance

Difficulty

Formalization scope

Selected references

A Robust Spectral Clustering Algorithm for Sub-Gaussian Mixture Models with Outliers 3: Binary PSD Rank-r Lifting (4) Is Equivalent to Robust Cluster Assignment (3)Research Paper

Why this formulation matters

The two finite matrix programs

Formalization targets

What the result supplies

Where the difficulty lies

Formalization scope

Selected references

Optimization by Decoded Quantum Interferometry 1: The Semicircle Law — the Optimal Degree-ℓ DQI State Satisfies ⟨s⟩/m → (√(μ(1−ρ)) + √(ρ(1−μ)))² When 2ℓ + 1 < d⊥Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.1 (the semicircle law)

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Strongly Polynomial Algorithm for Linear Exchange Markets II: A Z₊-Matrix Polyhedron P_M Lies Between an M2VPI Polyhedron and Its Scaling by B²Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6.4 (p. 15)

Milestones (§7, pp. 16–23)

Significance

Difficulty

Formalization scope

Selected references

Reversing quantum dynamics with near-optimal quantum and classical fidelity I: The Reversal Operation Attains at Least the Square of the Optimal Average Entanglement FidelityResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3 (p. 7)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Quantum LDPC Codes with Positive Rate and Minimum Distance Proportional to n^{1/2}: The Hypergraph Product of a Full-Rank [n,k,d] Parity-Check Matrix with Itself Is an [[n²+(n−k)², k², d]] CSS CodeResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 3)

General results

Significance

Difficulty

Formalization scope

Goal: the $\chi^2$ solution is BLUE