Poisson statistics for one-dimensional Anderson--Bernoulli Schrödinger operators

Core Contribution

The paper proves Poisson local eigenvalue statistics for the 1D discrete Anderson model with Bernoulli (and general bounded nonconstant iid) potentials, at every fixed nonzero coupling and at every energy in the interior of the almost-sure spectrum. After unfolding by the integrated density of states (IDS), the local process converges to a unit-intensity Poisson process. This closes a long-standing gap. Minami's estimate gives Poisson statistics for potentials with bounded densities, but it fails for atomic laws. Bourgain's Bernoulli result covers only small couplings with arithmetic conditions on λ, and it needs a smooth IDS and bounded Furstenberg densities. The earlier diffusion-based results (Molchanov, Allez–Dumaz, Kotani–Nakano) rely on Brownian structure.

The technical novelty is a phase coordinate H(θ) built from the inverse-chain stationary CDF. It gives an exact constant conditional drift π·ΔN for the lifted phase difference of two coupled transfer-matrix phases at nearby energies. Combined with Le Page-type fractional-moment contraction on projective space and an occupation bound, this yields a uniform exponential crossing law (Laplace transform 1/(1+s)). Renewal and block-splitting arguments then give joint Poisson counts across disjoint windows. Residual pinning and Sturm oscillation convert crossing counts into eigenvalue counts. The method needs no Minami estimate, no regularity of the IDS beyond continuity and strict monotonicity, and no density of states.

Methodological Rigor

The argument is a coherent chain of lemmas with explicit uniformity tracking. I checked the logic of the central steps and found it plausible:

Strict IDS monotonicity at Bernoulli bulk energies is proved directly. The paper also claims a Lean 4 end-to-end formalization, including Furstenberg's positivity theorem. If that claim holds, correctness confidence is very high. This is unusual for analytic probability and is a notable methodological contribution in itself. The AI-assisted workflow (GPT-6) is disclosed.

Caveats: the proof is qualitative, with no rates. Compact neighborhoods and uniformity are handled in prose, which would be easier to check with the formalization. The IDS-unfolded statement is clean, but the linear-scaling version needs a finite positive derivative at E. That derivative may fail for Bernoulli at large coupling, where the IDS can be singular continuous. The paper acknowledges this.

Potential Impact

This resolves what was a recognized open problem: Poisson statistics for the Anderson–Bernoulli model in 1D at all couplings. The model's atomic law was the standard obstruction to Minami-type arguments. The technique, an exact-drift phase coordinate plus uniform crossing laws, is new and may transfer to:

Higher-dimensional Bernoulli localization has recently progressed, but the method here is intrinsically 1D (transfer matrices, Sturm oscillation, circle dynamics), so it does not directly address the higher-dimensional open problem. Applications are purely mathematical-physics. Impact is concentrated in random Schrödinger operators, spectral statistics, and random matrix products on the circle.

The Lean formalization of a nontrivial analysis/probability theorem, including a Furstenberg-type statement proved internally, may also shape how such results are presented and verified, a meta-level contribution.

Timeliness & Relevance

The paper is timely given the renewed interest in Anderson–Bernoulli localization (Ding–Smart, Li–Zhang, Li–Liu–Zhang) and in Poisson statistics beyond Minami's framework (Bourgain; Hislop–Nakano). The AI-assisted formal-verification angle is highly topical.

Strengths

Limitations

Overall

This is a strong, definitive result in mathematical physics that settles a recognized open problem with a new and potentially reusable technique, backed by machine-checked verification. It is a niche field, but within it the work is likely to be well cited and to be treated as the definitive answer for 1D Bernoulli Poisson statistics.