← All papers
First page of Quantum unique ergodicity and the critical crossover for 1-d Gaussian band matrices

Quantum unique ergodicity and the critical crossover for 1-d Gaussian band matrices

Promit Ghosal, Guillaume Remy

math.PR Nov 11, 2026 · v1 math-ph math.SP
Main theorems were autoformalized in Lean 4 by AxiomProver, giving a roughly 1.0-million-line development that uses only Lean's standard axioms.
We consider an $N\times N$ complex Gaussian random band matrix in one dimension with band width of order $W$, in the periodic block form of Yau and Yin. The $N$ sites are split into $n=N/W$ blocks of size $W$ on a ring, and the entries are nonzero only within a block and between adjacent blocks. The conjectured localization–delocalization transition occurs at $W\sim\sqrt N$. We prove quantum unique ergodicity for bulk eigenvectors at every deterministic rank whenever $W^2/N\to\infty$, with no power or logarithmic separation between $W^2$ and $N$. At the threshold $N/W^2\toτ\in(0,\infty)$, we show that the rescaled bulk eigenvalues and the block-mass profiles of their eigenvectors (the probability measures on the circle placing at $k/n$ the squared norm of the eigenvector on block $k$) converge jointly to a unique law. This law is encoded by a random entire function whose zeros give the limiting eigenvalues, and its derivatives there give the limiting profile integrals. The law of this function is determined by the Dorokhov–Mello–Pereyra–Kumar (DMPK) diffusion of the unitary class. In the critical law, the profiles have strictly positive variance against every nonconstant smooth test function, so they are not concentrated on the uniform profile. As $τ\to0$ this variance vanishes and the local spectrum tends to the sine process. As $τ\to\infty$ it tends to a Poisson process where both limits taken after the critical one. The critical family thus interpolates between the delocalized and localized regimes, confirming for this model the prediction of Fyodorov and Mirlin that at $W^2\asymp N$ the joint law of eigenvalues and eigenvectors depends only on $N/W^2$. The full content of this work has been autoformalized in Lean4 by AxiomProver.

The paper studies 1-d complex Gaussian random band matrices in the Yau–Yin periodic block form, where a localization–delocalization transition is conjectured at band width W sqrt(N). The goals are to prove quantum unique ergodicity for bulk eigenvectors when W^2/N → ∞, and to describe the joint eigenvalue/eigenvector law at the critical scaling N/W^2 → τ.

An exact change-of-variables formula is derived for the eigenpair at a fixed rank by exposing a fresh GUE block on two adjacent blocks and taking a Schur complement. Further tools control boundary resolvent traces, counting fluctuations, and conditional eigenvector moments. The critical limit law is encoded by a random entire function whose law is governed by the DMPK diffusion. AxiomProver autoformalized the whole argument, including the cited results, in Lean 4.

Quantum unique ergodicity holds at every deterministic bulk rank with no power or logarithmic separation between W^2 and N. At criticality, eigenvalues and block-mass profiles converge jointly to a unique law that interpolates between the sine process (τ → 0) and a Poisson process (τ → ∞). Theorems 1.1, 1.3 and 1.4 are certified in about 1.0 million lines of Lean using only propext, Classical.choice and Quot.sound.