Papers With

← All papers
First page of The Localization Scale of the Block Anderson Model in One Dimension at Arbitrary Coupling and Volume

The Localization Scale of the Block Anderson Model in One Dimension at Arbitrary Coupling and Volume

Jun Yin

math.PR Nov 6, 2026 · v1 math-ph math.SP
formalization mathlib probability ai-agents
Read PDF arXiv abstract Code
TL;DR
The main localization-length theorem (Theorem 1.4) is formalized in Lean using only Mathlib, with proofs written with AI assistance; a public repository is provided.
Abstract
We study the one-dimensional block Anderson model with independent $W\times W$ Gaussian unitary ensemble potentials and deterministic nearest-neighbor hopping, with hopping-to-disorder ratio $g$. The system consists of $L$ blocks, with total dimension $N=WL$. As $W\to\infty$, we identify the bulk localization length, up to an arbitrarily small power of $W$, with $\min\{N,\max\{W,W^2g^2\}\}$, uniformly for deterministic couplings $g\ge0$ and cycle lengths $L\ge3$. For every fixed $D>0$ and all sufficiently large $W$, the expected fraction of eigenvectors in the selected energy interval satisfying these bounds is at least $1-W^{-D}$. In polynomial volume the bounds hold simultaneously for all eigenvectors in that interval with probability at least $1-W^{-D}$. The localization length is the number of coordinates in the shortest cyclic interval containing at least half of an eigenvector's mass.
Problem

The goal is to determine the bulk localization length of eigenvectors in the one-dimensional block Anderson model. The model has independent W×W GUE onsite blocks and deterministic nearest-neighbor hopping with coupling g. The bound must hold uniformly over couplings g ≥ 0 and cycle lengths L ≥ 3.

Approach

The lower bound combines a deterministic local resolvent comparison with a loop-hierarchy analysis along a characteristic stochastic flow. Transfer-matrix estimates make this analysis uniform for large g. The upper bound uses the fractional-moment method, deriving Green-function decay from transfer-matrix growth and averaging over cells of about g^2 blocks. The main theorem is formalized in Lean relying only on Mathlib, with proofs written using Claude models; differences between the paper and the Lean proof are documented in the repository.

Results

The localization length equals min{N, max{W, W^2 g^2}} up to W^ε factors, for all but a W^{-D} fraction of eigenvectors in the energy interval. In polynomial volume the bound holds simultaneously for all eigenvectors in the interval with high probability. Theorem 1.4 is machine-checked in Lean.