∑math20

Mathematical physics · Result 269

Uniform Laughlin gap and stability under bounded scalar disorder

2 papersLean

Proves the fermionic Laughlin spectral-gap conjecture for the full V1 interaction at filling 1/3 on the round sphere. The unique ground state remains uniformly gapped under sufficiently weak bounded real scalar one-body potentials projected to the lowest Landau level. Both the gap and disorder threshold are uniform over all sufficiently large particle numbers and all normalized potential profiles.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 2

First page of Uniform Stability of the Spherical Laughlin Gap

Uniform Stability of the Spherical Laughlin Gap

OpenAI · October 5, 2026

We prove that the fermionic Laughlin V1 Hamiltonian at filling 1/3 on expanding round spheres retains a unique ground state and a uniform spectral gap under sufficiently weak bounded real scalar one-body potentials projected to the lowest Landau level. With coefficient one for each pair projector and Laughlin flux \(q=3(N-1)\), the gap and perturbation threshold are uniform for all sufficiently large particle numbers and all potential profiles of supremum norm at most one. The result uses the uniform unperturbed Fock-space gap and gives existential constants.

Read PDF Download Source

Cite
@misc{OAI:Uniform-Stability-of-the-Spherical-Laughlin-Gap-October-5-2026,
  author = {{OpenAI}},
  title = {{Uniform Stability of the Spherical Laughlin Gap}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Uniform-Stability-of-the-Spherical-Laughlin-Gap-October-5-2026/uniform-stability-spherical-laughlin-gap.pdf}{OAI:Uniform-Stability-of-the-Spherical-Laughlin-Gap-October-5-2026}},
  year = {2026}
}
First page of A Fock-space inequality and the Laughlin spectral gap

A Fock-space inequality and the Laughlin spectral gap

OpenAI · September 24, 2026

We prove the spherical fermionic Laughlin spectral-gap conjecture for the full V1 interaction. With coefficient one for each pair projector, the gap above the Laughlin state at filling 1/3 on the round sphere is at least 1/25 for all sufficiently large systems. More generally, \(H_Q^2\ge\gamma H_Q\) for some fixed \(\gamma\gt 1/25\) on the entire lowest-Landau-level Fock space for all sufficiently large flux Q, independently of particle number.

Read PDF Download Source

Cite
@misc{OAI:A-Fock-space-inequality-and-the-Laughlin-spectral-gap-September-24-2026,
  author = {{OpenAI}},
  title = {{A Fock-space inequality and the Laughlin spectral gap}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/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}{OAI:A-Fock-space-inequality-and-the-Laughlin-spectral-gap-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

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

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

ResultComparator statement
Uniform unperturbed spherical Laughlin gap inequalityLaughlinGap.lean
Uniform Laughlin \(V_1\) spectral gapLaughlin.lean
Uniform Fock-space spectral-gap inequalityLaughlinFock.lean
Planar spectral-gap inequalityLaughlinPlanar.lean

Scope note on GitHub →