# Uniform Laughlin gap and stability under bounded scalar disorder

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

- [Uniform Stability of the Spherical Laughlin Gap](../../preprints/Uniform-Stability-of-the-Spherical-Laughlin-Gap-October-5-2026/uniform-stability-spherical-laughlin-gap.pdf)
- [A Fock-space inequality and the Laughlin spectral gap](../../preprints/A-Fock-space-inequality-and-the-Laughlin-spectral-gap-September-24-2026/A-Fock-space-inequality-and-the-Laughlin-spectral-gap-September-24-2026.pdf)

## Scope

The linked formalization proves the uniform unperturbed gap estimate used in the paper's stability argument for the fermionic Laughlin state at filling $1/3$ on the sphere. At flux $q=3(N-1)$ and all sufficiently large particle numbers $N$, every antisymmetric state has $V_1$ energy at least $1/25$ times its squared distance from the Laughlin ground-state line.

This selected statement is the unperturbed Fock-space inequality. Stability under projected one-body potentials and uniqueness of the perturbed ground state are outside it.

The Laughlin spectral-gap problem asks for a positive gap that remains uniform as the system grows. The formalization includes the finite spherical $V_1$ bound of $1/100$ above the Laughlin state at flux $3(N-1)$ for all sufficiently large particle numbers $N$. It also proves the stronger Fock-space inequality $H_Q^2\ge\gamma H_Q$ for every fixed $0<\gamma<\gamma_*$ and all sufficiently large fluxes $Q$, independently of particle number, where $\gamma_*=4616733319001/10^{14}>1/25$.

For the untruncated planar model, the formalization proves the corresponding inequality at the endpoint $\gamma_*$ on every homogeneous particle sector. These statements use coefficient one for each pair projector.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Uniform unperturbed spherical Laughlin gap inequality | [LaughlinGap.lean](../ComparatorChallenges/LaughlinGap.lean) |
| Uniform Laughlin $V_1$ spectral gap | [Laughlin.lean](../ComparatorChallenges/Laughlin.lean) |
| Uniform Fock-space spectral-gap inequality | [LaughlinFock.lean](../ComparatorChallenges/LaughlinFock.lean) |
| Planar spectral-gap inequality | [LaughlinPlanar.lean](../ComparatorChallenges/LaughlinPlanar.lean) |