we-solve (beta)

Phys-66 · physics · mathematics · Physics

A Laughlin gap stable under every small bounded scalar perturbation

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For the spherical fermionic $V_1$ pseudopotential at flux $Q=3(N-1)$, are there $\lambda _*,Delta_*>0$ and $N_*$ such that every real bounded measurable scalar phi with $||\phi ||_infinity\leq 1$ and every $|\lambda |\leq \lambda _*$ gives a unique ground state and spectral gap at least $Delta_*$ for $N\geq N_*$, when lambda times the projected one-body scalar potential is added?

Short English statement

For the spherical fermionic $V_1$ pseudopotential at flux $Q=3(N-1)$, are there $\lambda _*,Delta_*>0$ and $N_*$ such that every real bounded measurable scalar phi with $||\phi ||_infinity\leq 1$ and every $|\lambda |\leq \lambda _*$ gives a unique ground state and spectral gap at least $Delta_*$ for $N\geq N_*$, when lambda times the projected one-body scalar potential is added?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Phys-66-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Phys-66

The expanding-sphere Laughlin gap and unique ground state are claimed stable under small bounded projected scalar disorder, uniformly over profiles and particle number. The question retains these same parameters and conventions. Within these assumptions, this is a claimed affirmative answer to the stated question.

A Laughlin gap stable under every small bounded scalar perturbation

OpenAI's claim

OpenAI presents a proof in the selected manuscript. The expanding-sphere Laughlin gap and unique ground state are claimed stable under small bounded projected scalar disorder, uniformly over profiles and particle number.

Mathematical statement of the claimed result

Result 1.
Let $q=3(N-1)$, $U_q$ be the spin-$q/2$ lowest Landau level on a sphere of area $2\pi q$, and \[ H_{N,q}=\sum_{i<j}P_{ij}^{(1)}\quad\text{on }\bigwedge^NU_q, \] where each projector selects pair total spin $q-1$. Perturb by $\lambda\sum_iT_q(\varphi)^{(i)}$, with $T_q(\varphi)=\Pi_qM_\varphi\Pi_q|_{U_q}$. The source claims constants $\lambda_*,\Delta_*>0$, $N_*<\infty$, such that \[ E_1(N,\lambda,\varphi)-E_0(N,\lambda,\varphi)\ge\Delta_* \] for every $N\ge N_*$, bounded real measurable $\varphi$ with $\|\varphi\|_\infty\le1$, and real $|\lambda|\le\lambda_*$. Eigenvalues count multiplicity, so the ground state is unique.

Outline of the argument

A local lowest-Landau-level calculus tracks pinned zeros and weighted observables. Orthogonal branch readout, charge bounds, and rotation averaging control local removal of interaction energy; the unperturbed Fock-space gap then absorbs the bounded perturbation.

Formal verification

For family 269, the documented entries give unperturbed spherical Laughlin and stronger Fock-space gap inequalities. Stability against scalar one-body disorder and uniqueness of the perturbed ground state are not included. The listed Comparator files are Laughlin.lean, LaughlinFock.lean, LaughlinGap.lean, LaughlinPlanar.lean. Named declarations include OAI.Laughlin.mainTarget_proved. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.

Status caveat

OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.

Sources

Go to contribution →