Random Matrix Theory

Motivation

Many graph algorithms run in time proportional to the number of edges. A sparsifier of a weighted graph $G$ is a graph $H$ on the same vertices with far fewer edges that approximates $G$ for the purpose at hand, so that the algorithm can be run on $H$ instead. Benczúr and Karger (1996) showed that every graph has a sparsifier with $O(n\log n/\varepsilon^2)$ edges preserving the weight of every cut up to a factor $1\pm\varepsilon$. Spielman and Teng (2004) introduced the stronger spectral notion, in which the Laplacian quadratic form is preserved for every real vector, not only for cut indicators; their sparsifiers had $O(n\log^c n)$ edges for a large constant $c$ and were the first step of their nearly-linear-time solvers for symmetric diagonally dominant linear systems.

Spielman and Srivastava (arXiv:0803.0929, STOC 2008, SIAM J. Comput. 2011) proved that independent sampling of $O(n\log n/\varepsilon^2)$ edges, each edge with probability proportional to its weight times its effective resistance, yields a spectral sparsifier. The result improved both earlier bounds, replaced a recursive partitioning construction by a one-line sampling rule, and made effective resistance a standard tool in graph algorithms. Batson, Spielman and Srivastava (arXiv:0808.0163) later obtained $O(n/\varepsilon^2)$ edges deterministically, by a slower method built on the same matrix $\Pi$.

Setting

Let $G=(V,E,w)$ be a connected weighted undirected graph with $n=|V|$ vertices, $m=|E|$ edges and weights $w_e>0$. Orient every edge arbitrarily, so that it has a head and a tail (distinct vertices).

• The incidence matrix $B\in\mathbb R^{m\times n}$ has $B(e,v)=1$ if $v$ is the head of $e$, $-1$ if $v$ is its tail, and $0$ otherwise; $b_e$ denotes its row for $e$. $W$ is the diagonal $m\times m$ matrix with $W(e,e)=w_e$.
• The Laplacian is $L=B^{\mathsf T}WB$, with quadratic form $x^{\mathsf T}Lx=\sum_e w_e\,(x(\mathrm{head}\,e)-x(\mathrm{tail}\,e))^2$.
• $L^{+}$ is the Moore–Penrose pseudoinverse of $L$: if $L=\sum_{i=1}^{n-1}\lambda_iu_iu_i^{\mathsf T}$ over its nonzero eigenvalues, then $L^{+}=\sum_{i=1}^{n-1}\lambda_i^{-1}u_iu_i^{\mathsf T}$.
• The effective resistance of the edge $e$ is $R_e=b_eL^{+}b_e^{\mathsf T}$: the potential difference across $e$ when a unit current enters at one end and leaves at the other, the edges being resistors of conductance $w_e$.
• $\Pi=W^{1/2}BL^{+}B^{\mathsf T}W^{1/2}$ is an $m\times m$ matrix with $\Pi(e,e)=w_eR_e$.
• Sparsify$(G,q)$ draws $q$ edges independently with replacement, the edge $e$ with probability $p_e=w_eR_e/\sum_f w_fR_f$, and gives $e$ the weight $w_e/(qp_e)$ for each time it is drawn. Its output $H$ has Laplacian $\tilde L=B^{\mathsf T}W^{1/2}SW^{1/2}B$, where $S$ is the random diagonal matrix with $S(e,e)=\#\{\text{draws of }e\}/(qp_e)$.

Formalization targets

Goal: Theorem 1

There are an absolute constant $C$ and a threshold $N_0$ such that, for every $n\ge N_0$, every connected weighted graph on $n$ vertices and every $1/\sqrt n<\varepsilon\le1$, with $q=\lceil 9C^2n\log n/\varepsilon^2\rceil$, with probability at least $1/2$

$$\forall x\in\mathbb R^n:\qquad (1-\varepsilon)\,x^{\mathsf T}Lx\;\le\;x^{\mathsf T}\tilde Lx\;\le\;(1+\varepsilon)\,x^{\mathsf T}Lx .$$

The constant $C$ is left unfixed; the statement asserts the shape $q=O(n\log n/\varepsilon^2)$ with the paper's explicit dependence on $C$.

Milestones

1. Lemma 3 (four parts): $\Pi$ is an orthogonal projection; $\operatorname{im}\Pi=\operatorname{im}W^{1/2}B$; the eigenvalues of $\Pi$ are $1$ with multiplicity $n-1$ and $0$ with multiplicity $m-n+1$; $\Pi(e,e)=\|\Pi(\cdot,e)\|^2$.
2. Lemma 4: for a nonnegative diagonal $S$, $\|\Pi S\Pi-\Pi\Pi\|_2\le\varepsilon$ implies $(1-\varepsilon)x^{\mathsf T}Lx\le x^{\mathsf T}B^{\mathsf T}W^{1/2}SW^{1/2}Bx\le(1+\varepsilon)x^{\mathsf T}Lx$ for all $x$.
3. Lemma 5 (Rudelson–Vershynin): for independent samples $y_1,\dots,y_q$ of a random vector with $\|y\|_2\le M$ and $\|\mathbb E\,yy^{\mathsf T}\|_2\le1$, and $q\ge2$,

$$\mathbb E\Big\|\frac1q\sum_{j=1}^q y_jy_j^{\mathsf T}-\mathbb E\,yy^{\mathsf T}\Big\|_2\le CM\sqrt{\frac{\log q}{q}}\quad\text{whenever the right side is }<1.$$

Significance

Theorem 1 says that every weighted graph is spectrally approximated by a reweighted subgraph with $O(n\log n/\varepsilon^2)$ edges. A spectral approximation preserves cut weights, the eigenvalues of the Laplacian up to $1\pm\varepsilon$, effective resistances, and the condition number of $L$ as a preconditioner, so any algorithm whose output depends on these quantities can run on $H$. Combined with fast approximate computation of effective resistances (the second mission of this series), it gives a nearly-linear-time construction, and it is the sampling step used in Laplacian solvers, in sparsification of sums of rank-one matrices, and in leverage-score sampling for regression, where $w_eR_e$ is exactly the statistical leverage of a row.

The result is proved in the paper; to our knowledge no machine-checked proof exists. This mission formalizes the statement and the paper's proof structure: the linear algebra of $\Pi$ (Lemma 3), the deterministic reduction from quadratic forms to a spectral-norm bound (Lemma 4), and the matrix concentration inequality (Lemma 5), which is the substantive analytic input and is itself a reusable result about sums of independent rank-one matrices.

Difficulty

The deterministic part is linear algebra over the pseudoinverse. The obstacle is concentration: the expected Laplacian of $H$ equals $L$, but bounding the deviation uniformly over all $x\in\mathbb R^n$ is a statement about the spectral norm of a random matrix, and a union bound over a net of directions costs a factor of $n$ in the sample count rather than $\log n$. Scalar Chernoff bounds per cut, which suffice for cut sparsifiers, do not give the spectral statement. Lemma 5 is the matrix inequality that removes this loss, and no inequality of this kind (a concentration bound for the spectral norm of a sum of independent random matrices) is in Mathlib.

Formalization scope

All declarations sit in the namespace EffResSparsify.Sampling.

• Graphs. A structure WGraph V E with orientation maps head, tail : E → V, weights w : E → ℝ, and the fields head e ≠ tail e (no loops) and 0 < w e. Parallel edges are allowed; nothing in §3 uses simplicity. Connectivity is a separate hypothesis on the underlying simple graph and includes $V\ne\emptyset$. In Theorem 1 the vertex type is Fin n; the edge type is an arbitrary finite type.
• Pseudoinverse. $L^{+}$ is the matrix of the published Moore–Penrose pseudoinverse HarmonicGames.Decomposition.pinv of $x\mapsto Lx$ on Euclidean $\mathbb R^V$; it equals the spectral formula above and is the gauge-fixed inverse, never "some solution of $Lx=y$".
• Sampling. $p_e$ is defined as $w_eR_e/\sum_f w_fR_f$; the identity $\sum_f w_fR_f=n-1$ is part of the proof. An outcome of Sparsify is a sequence in $E^q$ with probability $\prod_i p_{s_i}$, and probabilities and expectations are finite sums over $E^q$, with no measure theory.
• Norms and logarithms. $\|\cdot\|_2$ is the $\ell_2$ operator norm on matrices (Matrix.Norms.L2Operator); vector norms in Lemma 5 are Euclidean; $\log$ is natural (the base is absorbed into $C$).
• Constants. In Theorem 1, $\exists C>0,\ \exists N_0,\ \forall n\ge N_0$ precede the graph and $\varepsilon$; the sample count is $\lceil 9C^2n\log n/\varepsilon^2\rceil$, rounded up because the printed value is not an integer. In Lemma 5, $\exists C>0$ precedes the dimension, the distribution, $M$ and $q$.
• Corrected statement. Lemma 5 as printed, with right side $\min(CM\sqrt{\log q/q},1)$, is false (at $q=1$ the bound is $0$). The formal milestone is Rudelson and Vershynin's own Theorem 3.1: $q\ge2$, and the bound $a=CM\sqrt{\log q/q}$ holds when $a<1$. It is stated for finitely supported distributions, which is all Theorem 1 uses. Theorem 1 applies it with $a\le\varepsilon/2$, so the correction does not affect the goal.
• Not a trivialization. Theorem 1 does not take Lemma 5, a bound on $\mathbb E\|\Pi S\Pi-\Pi\|_2$, or a free sample count as a hypothesis; a statement with any of these, or with "$\exists q$" in place of $\lceil 9C^2n\log n/\varepsilon^2\rceil$, is a different theorem.

Reusable beyond this mission: the weighted Laplacian with its pseudoinverse and effective resistances, and Lemma 5, which applies to any sampling scheme for sums of rank-one matrices (leverage-score sampling, column subset selection). Contributions toward a matrix Chernoff or Rudelson-type inequality in Mathlib are welcome.

Selected references

• D. A. Spielman, N. Srivastava, Graph Sparsification by Effective Resistances, arXiv:0803.0929v4, 2009; SIAM J. Comput. 40(6), 2011. https://arxiv.org/abs/0803.0929, https://doi.org/10.1137/080734029
• M. Rudelson, R. Vershynin, Sampling from large matrices: an approach through geometric functional analysis, J. ACM 54(4), 2007. https://doi.org/10.1145/1255443.1255449
• M. Rudelson, Random vectors in the isotropic position, J. Funct. Anal. 164(1), 1999. https://doi.org/10.1006/jfan.1998.3384
• A. A. Benczúr, D. R. Karger, Approximating s-t minimum cuts in Õ(n²) time, STOC 1996. https://doi.org/10.1145/237814.237827
• D. A. Spielman, S.-H. Teng, Spectral sparsification of graphs, SIAM J. Comput. 40(4), 2011 (arXiv:0808.4134). https://arxiv.org/abs/0808.4134
• J. Batson, D. A. Spielman, N. Srivastava, Twice-Ramanujan sparsifiers, SIAM J. Comput. 41(6), 2012 (arXiv:0808.0163). https://arxiv.org/abs/0808.0163

Motivation

An Ising spin system probes a quadratic form only on cube vertices. The source asks whether random orthogonal eigenvectors allow its pressure to be determined by the limiting eigenvalue distribution at every positive temperature. The source is OpenAI's September 2026 manuscript.

Setting

The pressure is the normalized logarithm of the average Boltzmann weight under the uniform spin prior. Eigenvectors are Haar orthogonal, and the deterministic empirical eigenvalue laws converge weakly to a compactly supported probability law. The variational formula uses an edge-extended spectral transform.

Formalization targets

$$\mathbb E P_N(\beta)\to\mathcal V_\beta,\qquad P_N(\beta)\to\mathcal V_\beta\ \text{almost surely}\qquad(\beta>0).$$

For a spin system on N Ising spins σ ∈ {−1,1}^N, the rotated pressure for eigenvalues λ₁,…,λ_N, an orthogonal rotation U and a field c is (1/N) times the log of the average over all 2^N spin configurations of exp(H(σ)), where H(σ) = (1/2)∑ᵢ λᵢ (Uσ)ᵢ² + ∑ᵢ cᵢσᵢ. The theorem states that, for any probability space (Ω,P), random N×N orthogonal matrices U_N that are measurable and whose laws are right-invariant under multiplication (Haar-type), and any deterministic eigenvalue arrays (eig_N,i), the following holds under these assumptions: ν is a probability measure on ℝ whose support lies in [a,b] and contains both a and b; for every ε>0, eventually in N all eigenvalues lie in [a−ε,b+ε]; the empirical spectral laws (1/N)∑ᵢ δ_{eig_N,i} converge weakly to ν; and the inverse temperature β is strictly positive. Then, with eigenvalues β·eig_N,i, rotation U_N(ω)⁻¹ and zero external field, the expected rotated pressure ∫ pressure dP converges as N → ∞, and the pressure itself converges for P-almost every ω, in both cases to the real part of the variational functional of the measureR transform of the β-rescaled law of ν, evaluated at the edge β·b.

The goal is OAI.InvariantIsing.positive_temperature_pressure_unconditional. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

• gaussianPattern ground limit unconditional.
• gaussianPattern norm limits unconditional.
• gaussianPattern pressure limit unconditional.
• ground state limit unconditional.
• limiting pressure of extreme limits unconditional.
• limiting wasserstein field pressure of extreme limits unconditional.
• random field pressure tendsto ae unconditional.
• random pressure limit unconditional.
• random pressure tendsto ae unconditional.
• random pressure tendsto in measure unconditional.

Significance

The selected goal is the all-positive-temperature zero-field pressure theorem. The attached results also cover field laws, random spectra, Gaussian-pattern pressure and ground energy, and related norm limits under their stated assumptions. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Weak spectral convergence does not control rare extreme eigenvalues. The explicit no-outlier condition is essential to the selected statement’s comparison with the limiting spectral functional.

Formalization scope

The spin prior is uniform probability, and temperature is implemented by multiplying eigenvalues by $\beta$. The no-outlier condition holds eventually within every enlargement of the limiting support interval. Almost-sure convergence and expectation convergence are both conclusions; other attached variants keep their own uniform-integrability and field hypotheses.

The shared definitions are supplied by InvariantIsing. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, All-temperature pressure for orthogonally invariant Ising spin glasses, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Sample covariance matrices are the basic object of multivariate statistics: principal component analysis, signal detection and factor models all start from the eigenvalues of $S = \frac1M\sum_{k=1}^M \vec y_k \vec y_k^{\,*}$ computed from $M$ samples of an $N$-dimensional vector. When $N$ is comparable to $M$, the eigenvalues of $S$ no longer approximate those of the population covariance $\Sigma$. The question is then whether a few large population eigenvalues ("spikes") are visible in the sample spectrum at all, and how the top sample eigenvalue fluctuates when they are.

Baik, Ben Arous and Péché (Ann. Probab. 33 (2005) 1643–1697) answered this for complex Gaussian samples. They found a sharp threshold $1+\gamma^{-1}$, where $\gamma^2 = M/N$, now called the BBP phase transition. This mission formalizes the supercritical half of the answer, Theorem 1.1(b).

Timeline.

• 2000–2001: Johansson (Comm. Math. Phys. 209, 2000) and Johnstone (Ann. Statist. 29) proved that for $\Sigma = I$ the largest eigenvalue, centred at $(1+\gamma^{-1})^2$ and scaled by $M^{2/3}$, has the Tracy–Widom law. Johansson treated the complex case, Johnstone the real case.
• 2005: Baik, Ben Arous and Péché treated $\Sigma$ with finitely many eigenvalues different from $1$. Spikes at or below $1+\gamma^{-1}$ give $M^{2/3}$ fluctuations with limit laws $F_k$ (part (a), a separate mission of this series). Spikes above $1+\gamma^{-1}$ give $\sqrt M$ fluctuations with limit $G_k$ (part (b)).
• 2006: Baik and Silverstein (J. Multivariate Anal. 97) located the outlying eigenvalue for general, non-Gaussian samples. Bai and Yao (Ann. IHP 44, 2008) obtained Gaussian fluctuations of the outliers for general samples.

Setting

Let $g_{kj}$, $1 \le k \le M$, $1 \le j \le N$, be independent standard complex Gaussians: $g = a + ib$ with $a, b$ independent real normal variables of mean $0$ and variance $1/2$. Fix a unitary matrix $U$ and positive population eigenvalues $\ell_1, \dots, \ell_N$. The samples are

$$\vec y_k = U\,\mathrm{diag}(\sqrt{\ell_1},\dots,\sqrt{\ell_N})\,\vec g_k,$$

which are independent mean-zero complex Gaussian vectors with covariance $\Sigma = U\,\mathrm{diag}(\ell)\,U^*$. The sample covariance matrix is $S = \frac1M\sum_k \vec y_k\vec y_k^{\,*}$, and $\lambda_1$ is its largest eigenvalue.

The regime has $M, N \to \infty$ with $M/N = \gamma^2$ and $\gamma$ in a compact subset of $[1,\infty)$. A fixed number $r$ of the $\ell_j$ differ from $1$. For some $1 \le k \le r$ the top $k$ coincide, $\ell_1 = \cdots = \ell_k$, with common value in a compact subset of $(1+\gamma^{-1},\infty)$. The others, $\ell_{k+1},\dots,\ell_r$, lie in a compact subset of $(0,\ell_1)$.

The limit law is the finite GUE distribution. Let $Z_k = \int_{\mathbb R^k}\prod_{i<j}|\xi_i-\xi_j|^2\prod_i e^{-\xi_i^2/2}\,d\xi$. Then

$$G_k(x) = \frac1{Z_k}\int_{(-\infty,x]^k}\prod_{1\le i<j\le k}|\xi_i-\xi_j|^2\prod_{i=1}^k e^{-\xi_i^2/2}\,d\xi_1\cdots d\xi_k,$$

which is the law of the largest eigenvalue of a $k\times k$ Gaussian unitary ensemble matrix (Definition 1.2).

Formalization targets

Goal: Theorem 1.1(b)

$$\mathbb P\left(\Big(\lambda_1 - \Big(\ell_1 + \frac{\ell_1\gamma^{-2}}{\ell_1-1}\Big)\Big)\cdot\frac{\sqrt M}{\sqrt{\ell_1^2 - \ell_1^2\gamma^{-2}/(\ell_1-1)^2}} \le x\right) \longrightarrow G_k(x)\qquad\text{for every } x \in \mathbb R.$$

Companion: Corollary 1.1(b)

$$\lambda_1 - \ell_1\Big(1 + \frac{\gamma^{-2}}{\ell_1-1}\Big) \longrightarrow 0 \quad\text{in probability.}$$

Milestones

The milestones follow the proof in §4, in attack order:

• the critical points of the phase $f$, (218)–(219);
• the contour estimates, Lemmas 4.1 and 4.2;
• the uniform kernel asymptotics, Proposition 4.1;
• the Hermite-polynomial identities (287), (295), (288) and (292);
• the closed form (299) of the limiting kernel $K_2$;
• the Fredholm-determinant representation of $G_k$, Lemma 1.1:

$$G_k(x) = \det\big(1 - \mathbf H^{(k)}_x\big),\qquad H^{(k)}(u,v) = \frac{c_{k-1}}{c_k}\,\frac{p_k(u)p_{k-1}(v) - p_{k-1}(u)p_k(v)}{u-v}\,e^{-(u^2+v^2)/4}.$$

Here $p_n$ are the orthonormal polynomials for the weight $e^{-x^2/2}$ and $c_n$ their leading coefficients.

Significance

The result. Below the threshold the top eigenvalue sticks to the bulk edge $(1+\gamma^{-1})^2$. Above it, Theorem 1.1(b) and Corollary 1.1(b) show that $\lambda_1$ separates from the bulk to the explicit location $\ell_1(1+\gamma^{-2}/(\ell_1-1))$. Its fluctuations shrink from order $M^{-2/3}$ to order $M^{-1/2}$, and their law is the top eigenvalue of a $k\times k$ GUE, with $k$ the multiplicity of the spike. This gives:

• a detection threshold for spiked signals in high dimension;
• the centring and scaling of tests based on the top sample eigenvalue;
• the first instance of a $k$-dependent family of finite-GUE limits in a spiked model.

Formalizing it. The result is proved in the paper and is not open. Nothing in this mission has a machine-checked proof yet. A complete development would include:

• the first formal statements of the spiked complex Wishart model;
• the GUE law $G_k$ and its Fredholm representation;
• a uniform steepest-descent analysis with explicit contours.

The two contour lemmas (4.1, 4.2) and the Hermite identities are elementary and are footholds. Proposition 4.1 and Lemma 1.1 are substantial. The paper does not prove Lemma 1.1 but cites it as a standard result of random matrix theory (its references [28, 41]).

Difficulty

The obvious route is to diagonalise the sample matrix, write down the eigenvalue density and take a limit. That density involves the Harish-Chandra–Itzykson–Zuber integral. Its large-$N$ limit is not accessible directly, because the spike enters through a determinant with $N$ nearly coincident columns.

The paper instead starts from an exact Fredholm-determinant formula (Proposition 2.1, posed in mission 1 of this series). In it the kernel factors into two contour integrals $\mathcal H$ and $\mathcal J$ with phase $f(z) = -\mu(z-q) + \log z - \gamma^{-2}\log(1-z)$. Above the threshold the two factors are governed by different points. $\mathcal J$ has a nondegenerate saddle at $\pi_1 = \ell_1^{-1}$. For $\mathcal H$ the natural saddle $1/(\mu\pi_1)$ lies beyond the pole at $\pi_1$, so the contour must be deformed through a pole of order $k$, and the leading term is a residue rather than a saddle contribution. The estimates must hold uniformly in $\gamma$ and in the remaining spikes, and the convergence must be strong enough (Hilbert–Schmidt) to pass to Fredholm determinants.

Formalization scope

Model. Complex Gaussian samples with mean zero and no centring. $S = \frac1M\sum_k\vec y_k\vec y_k^{\,*}$, with the factor $1/M$. $\Sigma = U\,\mathrm{diag}(\ell)\,U^*$ for every unitary $U$. This is the model of the paper's (59), (61) and Proposition 2.1; the introduction's mentions of $1/N$, of centring and of the real density (1) are inconsistent with those formulas. $\lambda_1$ is the supremum of the eigenvalues of the Hermitian matrix $S$, and probabilities are measures of sets of sample arrays.

Regime. The regime is in sequence form:

• $N_n \to \infty$ and $\gamma_n = \sqrt{M_n/N_n} \in [1,\gamma_0]$;
• $1+\gamma_n^{-1}+c \le \ell_1 = \cdots = \ell_k \le C$;
• $c \le \ell_j \le \ell_1 - c$ for $k < j \le r$;
• $\ell_j = 1$ for $j > r$.

The fixed margins $c, C$ encode the compact subsets whose open ends move with $\gamma$. Convergence is pointwise in $x$.

Analytic conventions.

• The Fredholm determinant is the Fredholm series $\sum_n\frac{(-1)^n}{n!}\int_{(x,\infty)^n}\det[K(u_i,u_j)]$.
• $H^{(k)}$ takes its continuous diagonal value.
• $p_n = \mathrm{He}_n/((2\pi)^{1/4}\sqrt{n!})$ with Mathlib's probabilists' Hermite polynomials, equal to the paper's (31).
• The closed contours $\Gamma$, $\Sigma$ in $\mathcal H$, $\mathcal J$ are explicit circles satisfying the paper's constraints.
• $\Sigma_\infty$ is the imaginary axis.
• Residues of $a^{-k}\varphi(a)$ are Taylor coefficients.

Ruled-out trivialisations. Five shortcuts would make the statements trivial, and none is available:

• division by zero on the kernel diagonal is replaced by the diagonal value;
• the Fredholm series is shown to be $1$ on the zero kernel, so it is not identically junk;
• the conditionally convergent real form of contour integrals is not used;
• $\Sigma$ is not specialised to a diagonal matrix;
• the regime is shown satisfiable in a sorry-free check.

Infrastructure. The needed infrastructure is the complex Wishart model, eigenvalues of random Hermitian matrices, Fredholm determinants of integral operators, and contour integrals with uniform estimates. The Hermite and Fredholm layers can be reused for any orthogonal-polynomial ensemble. Contributions welcome:

• proofs of the elementary milestones ((218)–(219), (287), (295), (288), (292), (299), Lemmas 4.1, 4.2);
• Lemma 1.1 via Christoffel–Darboux and Andréief;
• the operator-theoretic step from Hilbert–Schmidt convergence of kernels to convergence of Fredholm series.

Selected references

• J. Baik, G. Ben Arous, S. Péché, Phase transition of the largest eigenvalue for nonnull complex sample covariance matrices, Ann. Probab. 33(5) (2005) 1643–1697. https://doi.org/10.1214/009117905000000233
• K. Johansson, Shape fluctuations and random matrices, Comm. Math. Phys. 209 (2000) 437–476. https://doi.org/10.1007/s002200050027
• I. M. Johnstone, On the distribution of the largest eigenvalue in principal components analysis, Ann. Statist. 29 (2001) 295–327. https://doi.org/10.1214/aos/1009210544
• J. Baik, J. W. Silverstein, Eigenvalues of large sample covariance matrices of spiked population models, J. Multivariate Anal. 97 (2006) 1382–1408. https://doi.org/10.1016/j.jmva.2005.08.003
• Z. Bai, J. Yao, Central limit theorems for eigenvalues in a spiked population model, Ann. Inst. H. Poincaré Probab. Statist. 44 (2008) 447–474. https://doi.org/10.1214/07-AIHP118

Motivation

Random growth models and random matrices share limit laws. The first exact instance was found by Johansson (Shape fluctuations and random matrices, Comm. Math. Phys. 2000), who showed that the last passage time of a lattice model with geometric or exponential weights has the law of the largest eigenvalue of a Laguerre (complex Wishart) random matrix. Baik, Ben Arous and Péché (Ann. Probab. 33 (2005)) extended the identity to weights whose rate depends on the row. On the matrix side this is a sample covariance matrix with a general population covariance $\Sigma$; on the growth side it is a corner growth model, or a series of exponential queues, with inhomogeneous service rates.

The identity is the reason the paper's main result, the phase transition of the largest sample eigenvalue as a few population eigenvalues ("spikes") cross the critical value $1 + \gamma^{-1}$, is also a theorem about last passage percolation and tandem queues. In the queueing reading, a spike is a slow server, and the phase transition describes how slow a few servers must be before they change the centring and the fluctuation scale of the exit time.

Timeline:

• 2000, Johansson: equal rates; the geometric and exponential last passage time has the law of the largest Laguerre eigenvalue (his Proposition 1.4 is the case $\pi_1 = \cdots = \pi_N$ of (307)).
• 2001, Baryshnikov and, independently, Gravner, Tracy and Widom: the tandem-queue and GUE-minor descriptions of the same object.
• 2005, Baik, Ben Arous and Péché: row-dependent rates $\pi_i$ (Proposition 6.1), via the Robinson–Schensted–Knuth (RSK) formula for geometric weights (310) and a scaling limit.

Setting

Last passage time. Attach a real weight $X(i,j)$ to every site of the grid $\{1,\ldots,N\}\times\{1,\ldots,M\}$. An up/right path from $(1,1)$ to $(N,M)$ is a sequence of $N+M-1$ sites starting at $(1,1)$, ending at $(N,M)$, each step adding $(1,0)$ or $(0,1)$. The last passage time is

$$L(N,M) = \max_{\pi:(1,1)\nearrow(N,M)} \sum_{(i,j)\in\pi} X(i,j). \qquad (306)$$

Exponential environment. Given positive numbers $\pi_1,\ldots,\pi_N$, the $X(i,j)$ are independent and $X(i,j)$ is exponential of mean $1/(\pi_iM)$, i.e. density $\pi_iMe^{-\pi_iMx}$ on $x\ge0$. All $M$ sites of row $i$ share one rate.

Sample covariance matrix. Let $g_{kj}$, $1\le k\le M$, $1\le j\le N$, be independent standard complex Gaussians (real and imaginary parts independent $N(0,1/2)$). For a unitary $U$ and $\ell_j = \pi_j^{-1}$ (308), the samples $\vec y_k = U\,\mathrm{diag}(\sqrt{\ell_j})\,g_k$ are mean-zero complex Gaussian vectors with covariance $\Sigma = U\,\mathrm{diag}(\ell)\,U^*$, and

$$S = \frac1M\sum_{k=1}^M \vec y_k\vec y_k^{\,*}, \qquad \lambda_1 = \text{largest eigenvalue of } S.$$

Schur functions and geometric weights. For a partition $\lambda$, the Schur function $s_\lambda(x)$ is the sum over semistandard Young tableaux $T$ of shape $\lambda$ of $\prod_{c}x_{T(c)}$. A geometric variable of parameter $q\in[0,1)$ has $\mathbb P(Y = k) = (1-q)q^k$.

Formalization targets

Goal: Proposition 6.1

For $1\le N\le M$, positive $\pi_1,\ldots,\pi_N$ and every unitary $U$,

$$\mathbb P\big(L(N,M)\le x\big) = \mathbb P\big(\lambda_1(M,N)\le x\big) \qquad \text{for all } x\in\mathbb R. \qquad (309)$$

The two sides are defined independently: one by a maximum over lattice paths of exponential weights, the other by the spectrum of a Gaussian random matrix.

Milestones

1. The recurrence (313): for every array of weights and every site with $a, b\ge2$,

$$L(a,b) = \max\{L(a-1,b), L(a,b-1)\} + X(a,b).$$

2. The Cauchy identity (311): $\sum_\lambda s_\lambda(x)s_\lambda(y) = \prod_{i,j}(1-x_iy_j)^{-1}$ for $x_i,y_j\ge0$, $x_iy_j<1$.
3. The geometric formula (310): for independent geometric weights $Y(i,j)$ of parameter $x_iy_j$, $x_i,y_j\in[0,1)$,

$$\mathbb P\big(G(N,M)\le n\big) = \prod_{i,j}(1-x_iy_j)\sum_{\lambda:\lambda_1\le n}s_\lambda(x)s_\lambda(y).$$

4. The exponential formula (307): for $M\ge N$ and distinct $\pi_i$,

$$\mathbb P\big(L(N,M)\le x\big) = \frac1C\int_{[0,x]^N}\frac{\det(e^{-M\pi_i\xi_j})}{V(\pi)}V(\xi)\prod_{j}\xi_j^{M-N}\,d\xi.$$

Significance

The proposition makes every distributional statement about $\lambda_1$ in the paper a statement about last passage percolation with row-dependent rates: the $F_k$ (generalised Tracy–Widom) fluctuations at the critical spike value, the Gaussian fluctuations above it, and the fixed-dimension limit. Through (312)–(313) it also covers the exit time of $M$ customers from $N$ exponential servers in series, an operations research object. The geometric formula (310) is the entry point of the RSK method for exactly solvable growth models.

These results are proved in the literature; the paper cites (310) and (311) and derives (307) from them by a limit. None of them is machine-checked as far as this series knows. Formalizing them requires a Lean development of Schur functions, the Cauchy identity and the RSK correspondence on matrices with nonnegative integer entries, and of the Wishart eigenvalue density, each reusable well beyond this mission.

Difficulty

The recurrence (313) is elementary. Everything else is not. The geometric formula (310) needs the RSK bijection between nonnegative integer matrices and pairs of semistandard tableaux of the same shape, together with Schensted's theorem that the first row of the shape is the last passage time; neither is in Mathlib. The passage from (310) to (307) is a scaling limit $x_i = 1 - M\pi_i/L$, $n = xL$, $L\to\infty$, in which a sum over partitions must converge to a multiple integral. The matrix side needs the joint eigenvalue density of a complex Wishart matrix with general $\Sigma$, which uses the Harish-Chandra–Itzykson–Zuber integral. A direct coupling of the two sides is not known; the identity is an equality of laws, proved by computing both.

Formalization scope

The development lives in the namespace SpikedWishart.LastPassage. Conventions:

• Sites and indices are 0-based; the paper's $(1,1)$ and $(N,M)$ are $(0,0)$ and $(N-1,M-1)$, and $N, M\ge1$.
• $L$ is defined as the maximum over paths (306), never by the recurrence (313), so (313) is a genuine statement.
• The exponential law is Mathlib's expMeasure with rate $\pi_iM$.
• The sample model is mean zero, uncentred, with factor $1/M$ and $\mathbb E|g|^2 = 1$; this is the model of (59), (61) and (307), and the page's centring by the sample mean and $S = (1/N)XX^*$ are printed slips. The covariance is $U\,\mathrm{diag}(\pi^{-1})U^*$ for every unitary $U$; specialising to diagonal $\Sigma$ would prove a special case.
• $N\le M$ is a disclosed addition to the goal, matching the page's "for $M\ge N$" in (307).
• Proposition 6.1 prints $L(M,N)$; the object is (306)'s $L(N,M)$.
• Schur functions are the tableau sum with variables extended by zero. The Cauchy identity is stated with the exponent $-1$ that the page omits. In (307) the constant $C$ is the integral of the same integrand over $(0,\infty)^N$, and the $\pi_i$ are distinct so that $V(\pi)\ne0$; the goal has no distinctness hypothesis.

A formalization in which either side of (309) is defined through the other, or through (307), would be trivial and is excluded: both laws are defined from scratch. Contributions are welcome on RSK and Schur function infrastructure, on the Wishart density, and on the measurability of $\lambda_1$.

Selected references

• J. Baik, G. Ben Arous, S. Péché, Phase transition of the largest eigenvalue for nonnull complex sample covariance matrices, Ann. Probab. 33(5):1643–1697, 2005. https://doi.org/10.1214/009117905000000233
• K. Johansson, Shape fluctuations and random matrices, Comm. Math. Phys. 209:437–476, 2000. https://doi.org/10.1007/s002200050027
• Y. Baryshnikov, GUEs and queues, Probab. Theory Related Fields 119:256–274, 2001. https://doi.org/10.1007/PL00008760
• J. Gravner, C. A. Tracy, H. Widom, Limit theorems for height fluctuations in a class of discrete space and time growth models, J. Stat. Phys. 102:1085–1132, 2001. https://doi.org/10.1023/A:1004879725949
• R. P. Stanley, Enumerative Combinatorics, Vol. 2, Cambridge University Press, 1999 (the paper's reference [36] for the Cauchy identity). https://doi.org/10.1017/CBO9780511609589

Motivation

Sample covariance matrices are the basic object of multivariate statistics: principal component analysis, factor models and signal detection all start from the eigenvalues of $S=\frac1M\sum_{k=1}^M\vec y_k\vec y_k^{\,*}$ built from $M$ observations of $N$ variables. When $N$ is comparable to $M$, the largest eigenvalue $\lambda_1$ of $S$ is no longer a consistent estimate of the largest population eigenvalue, and the question of when a "spike" in the population covariance is visible in $\lambda_1$ becomes a question about the law of $\lambda_1$ at large $M,N$.

Timeline.

• 2000–2001: for null covariance $\Sigma=I$, Johansson (complex samples, arXiv:math/9903134) and Johnstone (real samples, doi:10.1214/aos/1009210544) showed that $\lambda_1$, centred at $(1+\gamma^{-1})^2$ and scaled by $M^{2/3}$, converges to a Tracy–Widom law.
• 2003: Péché (reference [31] of the 2005 paper) showed that finitely many population eigenvalues below $2$ (at $M=N$) leave this limit unchanged.
• 2005: Baik, Ben Arous and Péché (doi:10.1214/009117905000000233), for complex Gaussian samples, located the threshold exactly at $1+\gamma^{-1}$ and identified the limit laws on both sides and at the threshold. This transition is now called the BBP phase transition.

This mission formalizes the critical and subcritical side of that transition, Theorem 1.1(a) of the 2005 paper.

Setting

Let $g=a+ib$ with $a,b$ independent real normal variables of mean $0$ and variance $1/2$: a standard complex Gaussian. Let $G=(g_{kj})$, $1\le k\le M$, $1\le j\le N$, be i.i.d. standard complex Gaussians. Fix an $N\times N$ unitary matrix $U$ and positive reals $\ell_1,\dots,\ell_N$, the population eigenvalues, and put $\Sigma=U\,\mathrm{diag}(\ell)\,U^*$. The samples are $\vec y_k=U\,\mathrm{diag}(\sqrt{\ell_j})\,\vec g_k$, mean-zero complex Gaussian vectors with covariance $\Sigma$. The sample covariance matrix is $S=\frac1M\sum_k\vec y_k\vec y_k^{\,*}$ and $\lambda_1$ is its largest eigenvalue. Write $\gamma=\sqrt{M/N}\ge1$.

The limit laws are built from the Airy function $\mathrm{Ai}(u)=\frac1{2\pi}\int e^{iua+ia^3/3}\,da$, integrated along a contour from $\infty e^{5i\pi/6}$ to $\infty e^{i\pi/6}$, and the Airy kernel

$$A(u,v)=\int_0^\infty\mathrm{Ai}(u+z)\,\mathrm{Ai}(z+v)\,dz .$$

For $m\ge1$, $s^{(m)}(u)=\frac1{2\pi}\int e^{iua+ia^3/3}(ia)^{-m}\,da$ (with the pole $a=0$ above the contour) and $t^{(m)}(v)=\frac1{2\pi}\int e^{iva+ia^3/3}(-ia)^{m-1}\,da$. The Fredholm determinant of a kernel $K$ on $L^2((x,\infty))$ is its Fredholm series

$$\det(1-K)=\sum_{n\ge0}\frac{(-1)^n}{n!}\int_{(x,\infty)^n}\det[K(u_i,u_j)]_{i,j=1}^n\,du ,$$

and

$$F_k(x)=\det\Big(1-A-\sum_{m=1}^k s^{(m)}\otimes t^{(m)}\Big)_{L^2((x,\infty))}.$$

$F_0$ is the GUE Tracy–Widom distribution and $F_1=F_{\rm GOE}^2$.

Formalization targets

Goal: Theorem 1.1(a)

Fix integers $0\le k\le r$. Let $M,N\to\infty$ with $\gamma\in[1,\gamma_0]$, and suppose $\ell_{r+1}=\dots=\ell_N=1$, $\ell_1=\dots=\ell_k=1+\gamma^{-1}$ and $\ell_{k+1},\dots,\ell_r$ stay in a compact subset of $(0,1+\gamma^{-1})$. Then for every real $x$,

$$\mathbb P\Big(\big(\lambda_1-(1+\gamma^{-1})^2\big)\frac{\gamma}{(1+\gamma)^{4/3}}M^{2/3}\le x\Big)\to F_k(x).$$

The goal leaves $U$ arbitrary and allows $\gamma$ to vary inside $[1,\gamma_0]$ along the sequence. A companion item states Corollary 1.1(a): $\lambda_1-(1+\gamma^{-1})^2\to0$ in probability.

Milestones

1. The Airy equation and the identity of the two forms (11), (12) of the Airy kernel.
2. Lemma 3.3: $F_k$ is well defined, and $s^{(m)}$ has the closed form (203).
3. The eigenvalue density (61) and Andréief's identity (65).
4. Hankel's formula (75).
5. Proposition 2.1: the exact identity $\mathbb P(\lambda_1\le\xi)=\det(1-K_{M,N})_{L^2((\xi,\infty))}$ for a double contour integral kernel.
6. The double critical point (109), (111) of the phase function $f(z)=-\mu(z-q)+\log z-\gamma^{-2}\log(1-z)$.
7. The descent Lemmas 3.1 and 3.2 along explicit contour pieces.
8. Proposition 3.1: convergence of the rescaled contour integrals $\mathcal H,\mathcal J$ at rate $M^{-1/3}$ with exponential tails.
9. The kernel identity (200).

Significance

Theorem 1.1(a) shows that $1+\gamma^{-1}$ is the exact threshold. Spikes strictly below it do not change the Tracy–Widom limit of $\lambda_1$. $k$ spikes exactly at it produce a new family of limit laws $F_k$ on the same $M^{2/3}$ scale. Together with part (b), where $\lambda_1$ separates and fluctuates on the scale $M^{-1/2}$, it gives the first complete description of the transition. It is the reference point for spiked-model results on detection limits in PCA, for the real case (Bloemendal–Virág, Mo) and for finite-rank perturbations of Wigner matrices (Péché, Féral–Péché).

The paper's proof is complete and has been in the literature since 2005. No part of it is machine-checked. The mission produces:

• a formal statement of the theorem;
• formal definitions of the Airy function by its contour integral, of the Airy kernel and of Fredholm determinants as Fredholm series;
• the exact finite-$N$ determinantal formula of Proposition 2.1;
• the uniform steepest-descent estimates;
• formal statements of the classical identities used along the way (Andréief, Hankel).

Difficulty

The obvious approach is to compute the law of $\lambda_1$ from the eigenvalue density, which is explicit (61). It fails because the density is an $N$-fold integral whose integrand is a signed determinant, so no direct limit exists. The paper converts it into a Fredholm determinant of a double contour integral kernel. Two steps then carry the difficulty.

First, the steepest-descent analysis. With $k$ spikes at $1+\gamma^{-1}$, the poles of the integrand sit exactly at the double critical point $p_c=\gamma/(\gamma+1)$ of the phase function. The contour cannot pass through the critical point and must enclose these poles, so it has to be routed at distance of order $M^{-1/3}$ to the left of $p_c$. All estimates must be uniform in $\gamma$ and in the remaining spikes.

Second, the passage from kernel convergence to convergence of Fredholm determinants. It needs bounds strong enough to control every term of the Fredholm series, which is what the exponential tails in Proposition 3.1 provide. The functions $s^{(m)}$ grow polynomially, so even the finiteness of $F_k$ (Lemma 3.3) needs an argument.

Formalization scope

Lean encoding:

• Samples are mean-zero with $\mathbb E\,\vec y\vec y^{\,*}=\Sigma$, $S=\frac1M\sum_k\vec y_k\vec y_k^{\,*}$, and there is no centring by the sample mean. This is the model of the paper's (59) and Proposition 2.1. The printed text on p. 1645 differs in three slips.
• $\Sigma=U\,\mathrm{diag}(\ell)\,U^*$ ranges over every unitary $U$.
• $\lambda_1$ is the largest eigenvalue of the Hermitian matrix $S$.
• The asymptotic regime is written with sequences $M_n,N_n$, $N_n\to\infty$ and $\gamma_n\in[1,\gamma_0]$. "In a compact subset of $(0,1+\gamma^{-1})$" is read with a fixed margin $c$: $c\le\ell_j\le1+\gamma_n^{-1}-c$.
• Indices are $0$-based.
• Exponents $2/3$, $4/3$, $1/3$ are real powers of positive reals.
• $F_k$ is defined as the Fredholm series of the kernel $A+\sum_m s^{(m)}\otimes t^{(m)}$, the paper's (201). The paper proves that this equals its Definition 1.1.
• Contour integrals are Bochner integrals along two-ray broken lines, where the integrands decay like $e^{-t^3/3}$. Closed contours are circles with real centres.

Trivializing formalizations ruled out:

• The Airy kernel is defined by (12), never by the divided difference (11), whose diagonal would be the junk value $0$.
• Ai is never written as the real integral $\frac1\pi\int_0^\infty\cos(t^3/3+ut)\,dt$, which is not Lebesgue integrable and would be $0$.
• A non-summable Fredholm series would be $0$, so summability is a milestone.
• The goal quantifies over every unitary $U$ and every admissible sequence, so it does not specialize $\Sigma$. Its hypotheses are satisfiable, for example by $M_n=N_n$, $\ell\equiv1$, $r=k=0$.

Infrastructure needed and reusable:

• the Airy function and its decay;
• trace-class or Hadamard-bound control of Fredholm series;
• the complex Wishart eigenvalue density, which needs the Harish-Chandra–Itzykson–Zuber integral;
• Andréief's identity;
• steepest-descent estimates for contour integrals.

The Fredholm-determinant layer and the Airy function are reusable in any Tracy–Widom result. Andréief's identity and Hankel's formula are reusable well beyond random matrices.

Contributions welcome: proofs of any milestone, and lemmas that bound Fredholm series by Hadamard's inequality.

Selected references

• J. Baik, G. Ben Arous, S. Péché, Phase transition of the largest eigenvalue for nonnull complex sample covariance matrices, Ann. Probab. 33(5) (2005), 1643–1697. https://doi.org/10.1214/009117905000000233
• K. Johansson, Shape fluctuations and random matrices, Comm. Math. Phys. 209 (2000), 437–476. https://arxiv.org/abs/math/9903134
• I. M. Johnstone, On the distribution of the largest eigenvalue in principal components analysis, Ann. Statist. 29 (2001), 295–327. https://doi.org/10.1214/aos/1009210544
• C. A. Tracy, H. Widom, Level-spacing distributions and the Airy kernel, Comm. Math. Phys. 159 (1994), 151–174. https://arxiv.org/abs/hep-th/9211141
• C. Andréief, Note sur une relation entre les intégrales définies des produits des fonctions, Mém. Soc. Sci. Phys. Nat. Bordeaux 2 (1883), 1–14.

Motivation

The eigenvalues of a large non-Hermitian random matrix are hard to study directly. For Hermitian matrices, the empirical spectral distribution (ESD) is controlled by the resolvent and the Stieltjes transform, both stable under small perturbations. For non-Hermitian matrices no such tool exists: eigenvalues can move a long way under tiny perturbations, and the moment method fails because moments do not determine a measure on $\mathbb C$. The route that works, going back to Girko (1984) and used by Bai (1997), Götze–Tikhomirov (2007), Pan–Zhou (2007) and Tao–Vu (2008), passes through logarithmic determinants. The identity $\frac1n\log|\det(A-zI)|=\int\log|w-z|\,d\mu_A(w)$ links the ESD $\mu_A$ to a scalar quantity. That scalar is computable from the singular values of $A-zI$, which are eigenvalues of a Hermitian matrix.

Tao and Vu, with an appendix by Krishnapur (Ann. Probab. 38 (2010) 2023–2065), turn this link into an exact criterion. Theorem 1.15 of that paper states that the ESD of a normalized i.i.d. random matrix converges to a measure $\mu$ if and only if the normalized log-determinants converge to the logarithmic potential of $\mu$ for almost every $z$. The same holds for a regularized version built from the singular values. This mission formalizes Theorem 1.15 and the main steps of its proof (§8 and Appendix A of the published article).

Setting

Let $x$ be a complex random variable with $\mathbf E x=0$ and $\mathbf E|x|^2=1$, and let $(x_{ij})_{i,j\ge1}$ be independent copies of $x$ on a probability space $(\Omega,\mathbf P)$. For each $n$, $X_n=(x_{ij})_{1\le i,j\le n}$. Let $M_n$ be deterministic $n\times n$ complex matrices with

$$\text{(1.3)}\qquad\sup_n\frac1{n^2}\|M_n\|_2^2<\infty,\qquad\|M\|_2^2=\sum_{i,j}|m_{ij}|^2,$$

and put $A_n=M_n+X_n$.

For $A\in M_n(\mathbb C)$ with eigenvalues $\lambda_1,\dots,\lambda_n$, counted with algebraic multiplicity, the ESD is $\mu_A=\frac1n\sum_i\delta_{\lambda_i}$. Its singular values are $\sigma_1(A)\ge\dots\ge\sigma_n(A)\ge0$. A sequence of random measures $\mu_n$ converges in probability to a deterministic $\mu$ if, for every continuous compactly supported $f:\mathbb C\to\mathbb R$, $\int f\,d\mu_n-\int f\,d\mu$ tends to $0$ in probability. It converges almost surely if, with probability one, $\int f\,d\mu_n\to\int f\,d\mu$ for all such $f$ at once. The logarithmic potential of a measure $\mu$ is $z\mapsto\int\log|w-z|\,d\mu(w)$.

Hypothesis (1.4) states that, for almost every $z$, the ESDs of the deterministic matrices $(\frac1{\sqrt n}M_n-zI)(\frac1{\sqrt n}M_n-zI)^*$ converge to a limit.

In Lean everything lives in the namespace UnivESD.LogDet. The ESD is esd, the one-based singular value is sv, logPotential is the logarithmic potential, and ConvInProb/ConvAS/ESDConvInProb/ESDConvAS are the modes of convergence. IIDArray is the entry model, HSBound is (1.3), shiftA M xs z n ω is $\frac1{\sqrt n}A_n-zI$, and Cond14 is (1.4).

Formalization targets

Goal: Theorem 1.15

Let $\mu$ be a probability measure on $\mathbb C$ with $\int|z|^2\,d\mu<\infty$. The following are equivalent:

1. $\mu_{\frac1{\sqrt n}A_n}\to\mu$ in probability;
2. for a.e. $z$, $\displaystyle\frac1n\log\Big|\det\big(\tfrac1{\sqrt n}A_n-zI\big)\Big|\to\int_{\mathbb C}\log|w-z|\,d\mu(w)$ in probability;
3. for a.e. $z$ there are $\varepsilon_n>0$, $\varepsilon_n\to0$, with

$$\frac1n\log\det\Big(\big(\tfrac1{\sqrt n}A_n-zI\big)\big(\tfrac1{\sqrt n}A_n-zI\big)^*+\varepsilon_nI\Big)\to2\int_{\mathbb C}\log|w-z|\,d\mu(w)$$

in probability.

Under (1.4) the same equivalence holds with almost sure convergence throughout.

Milestones, in the order the proof uses them

• (8.1): for a.e. $z$, $w\mapsto\log|w-z|$ is $\mu$-integrable.
• Lemma A.3 (Weyl's comparison for products): $\prod_{j\le J}|\lambda_j|\le\prod_{j\le J}\sigma_j(A)$ and $\prod_{j\ge J}\sigma_j(A)\le\prod_{j\ge J}|\lambda_j|$.
• (8.3): $\mathbf P(\sigma_{n-i}\le ci/n)=O(\exp(-n^{0.01}))$ for $2n^{0.99}\le i\le n-1$.
• (8.2): $\frac1n\sum_{i=1}^n\big(\log\sqrt{\sigma_i^2+\varepsilon_n}-\log\sigma_i\big)\to0$ almost surely.
• p. 2057: almost surely, eventually, $\frac1n\sum_{(1-\kappa)n<i\le n}\log\frac1{\sigma_i}\le O(\kappa\log\frac1\kappa)$, and the same bound for $\log\frac1{|\lambda_i|}$.

Significance

Theorem 1.15 reduces convergence of a non-Hermitian ESD to a family of scalar limit statements. Each of these can be attacked through Hermitian tools, because the regularized log-determinant in (iii) is a smooth functional of the singular values. Corollary 1.16 of the paper derives from it a practical criterion: the ESD converges to $\mu$ once the singular value distributions of $\frac1{\sqrt n}A_n-zI$ converge for a.e. $z$ to laws $\eta_z$ with $\int\log t\,d\eta_z=2\int\log|w-z|\,d\mu$. With the universality principle (Theorem 1.5, the companion mission) and Mehta's computation for complex Gaussian matrices, this yields the circular law for i.i.d. matrices with finite variance.

The theorem is proved in the source. To our knowledge neither it nor any of its milestones has a machine-checked proof. Mathlib has the ingredients for the objects (characteristic polynomials and their roots, LinearMap.singularValues, the strong law of large numbers) but not the results. A formal proof would give the platform its first verified bridge between eigenvalue and singular value asymptotics. Lemma A.3 alone, Weyl's multiplicative majorization, is a standard linear-algebra fact absent from Mathlib.

Difficulty

Two things make the obvious argument fail. First, $\log$ is unbounded at $0$. Vague convergence of $\mu_{\frac1{\sqrt n}A_n}$ controls $\int f\,d\mu_n$ only for continuous compactly supported $f$, while $\log|w-z|$ has a singularity at $w=z$ and grows at infinity. Passing between (i) and (ii) therefore requires uniform control of the eigenvalues (and singular values) near $0$ after the shift: the contribution of the smallest ones must vanish. Second, eigenvalues are not stable under perturbation, so this control cannot be read off the eigenvalues. It has to come from the singular values, through a lower-tail bound on $\sigma_{n-i}$ that is exponentially small in a power of $n$, and through a deterministic inequality transferring bounds from singular values to eigenvalues. The smallest singular values ($i$ below $n^{0.99}$) need a separate polynomial lower bound (the paper's Lemma 4.1, posed in the companion mission). The tail bound in its printed form is false at that end of the range.

Formalization scope

Conventions committed to in Lean:

• The ESD is $n^{-1}$ times the sum of Dirac masses over the root multiset of the characteristic polynomial, so multiplicities are kept. Test functions are real-valued, continuous and compactly supported. Almost sure ESD convergence uses one null set for all test functions.
• The matrices $X_n$ are the top-left corners of one infinite i.i.d. array. In-probability statements do not depend on how the $X_n$ are coupled across $n$, but almost-sure statements do, and the paper's proof applies the strong law to this array. The limit in (1.4) is required to be a probability measure, which is equivalent under (1.3).
• The second-moment condition on $\mu$ is Integrable (‖w‖²) μ. The logarithmic potential is a Bochner integral, which is $0$ when not integrable; by (8.1) this happens only for a null set of $z$, which "for a.e. $z$" ignores.
• Real.log 0 = 0. In (ii), a singular matrix would contribute $0$ instead of $-\infty$; for this model the determinant is almost surely nonzero eventually. Every milestone with $\log\sigma_i$ or $\log|\lambda_i|$ carries positivity of those quantities in its conclusion.
• Singular values are one-based (sv A i is Mathlib's singularValues (i-1)). Eigenvalue enumerations are Fin n-indexed, and the paper's $\lambda_i$ is index $i-1$.
• The paper's $O(\cdot)$ constants are existential and fixed before $n$. In the $\kappa\log(1/\kappa)$ bounds the constant is fixed before $\kappa$; a $\kappa$-dependent constant would make the bounds empty.

Disclosed corrections to the printed text:

1. (iii)'s matrix. Theorem 1.15 prints a mis-bracketed product, and (1.8) prints $(C+\varepsilon_nI)(C^*+\varepsilon_nI)$. The Lean uses $CC^*+\varepsilon_nI$ with $C=\frac1{\sqrt n}A_n-zI$, the matrix of (8.2) and of the proof of Corollary 1.16.
2. (8.3)'s range. It is printed for $1\le i\le n-n^{0.99}$, which is false for small $i$: for Gaussian entries and $M_n=0$, $n\sigma_{n-1}$ has a non-degenerate limit law. It is posed on $2n^{0.99}\le i\le n-1$, the range the proof covers and the use needs.
3. Lemma A.3, second inequality. It is posed for $1\le J\le n$, since $\sigma_0$ is undefined. The eigenvalues are ordered $|\lambda_1|\ge\dots\ge|\lambda_n|$, not $|\lambda_1|\le\dots\le|\lambda_n|$ as printed: the printed order is a slip. With it, both inequalities are weaker than Weyl's and cannot support the use on p. 2057, which orders the eigenvalues decreasingly. The decreasing order implies the printed form.
4. (8.2) and (8.1). (8.2) is stated for every deterministic $\varepsilon_n>0$ with $\varepsilon_n\to0$; the proof uses nothing else. (8.1) is stated as $\mu$-integrability plus local integrability of $z\mapsto\int|\log|w-z||\,d\mu(w)$.

A trivializing formalization is ruled out by construction. The goal mentions only $A_n$ and $\mu$. The proof's comparison ensemble $B_n=\sqrt n\,\mathrm{diag}(\lambda_i)$ is not a hypothesis. No statement takes a log-potential or a log-determinant as an input that could be fixed to make it hold.

The companion mission (Theorem 1.5, universality) poses Theorem 2.1 (the replacement principle), Lemma 1.7 (tightness) and Lemma 4.1 (least singular value), which the proof here also uses. They are not restated here. Once that mission is published they belong here as references. Contributions are welcome on the linear-algebra layer (Lemma A.3, multiplicative Weyl majorization), the Fubini argument of (8.1), and the singular-value tail bound (8.3). These are reusable well beyond this paper.

Selected references

• T. Tao, V. Vu (appendix by M. Krishnapur), Random matrices: Universality of ESDs and the circular law, Ann. Probab. 38(5) (2010) 2023–2065. https://doi.org/10.1214/10-AOP534 (source of this mission; published version).
• V. L. Girko, The circular law, Teor. Veroyatnost. i Primenen. 29 (1984) 669–679. https://doi.org/10.1137/1129095
• Z. D. Bai, Circular law, Ann. Probab. 25(1) (1997) 494–529. https://doi.org/10.1214/aop/1024404298
• F. Götze, A. Tikhomirov, The circular law for random matrices, Ann. Probab. 38(4) (2010) 1444–1491. https://doi.org/10.1214/09-AOP522
• T. Tao, V. Vu, Random matrices: the circular law, Commun. Contemp. Math. 10(2) (2008) 261–307. https://doi.org/10.1142/S0219199708002788
• H. Weyl, Inequalities between the two kinds of eigenvalues of a linear transformation, Proc. Natl. Acad. Sci. USA 35 (1949) 408–411. https://doi.org/10.1073/pnas.35.7.408