# Localization and delocalization in the Anderson model

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Pure-Point Spectrum for the Two-Dimensional Anderson Model at Every Positive Disorder](../../preprints/Pure-Point-Spectrum-for-the-Two-Dimensional-Anderson-Model-at-Every-Positive-Disorder-September-23-2026/paper.pdf)

## Scope

The linked formalization proves a supporting spectral statement for the nearest-neighbor Anderson operator on $\mathbb Z^2$. For every disorder strength $h>0$ with independent site potentials uniform on $[-h,h]$, it constructs the bounded self-adjoint operator almost surely and identifies its spectrum as the real interval $[-4-h,4+h]$.

This selected statement identifies the spectral set. It does not assert the pure-point spectral type claimed in the accompanying paper.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Almost-sure spectrum of the planar Anderson operator | [PlanarAndersonSpectrum.lean](../ComparatorChallenges/PlanarAndersonSpectrum.lean) |