we-solve (beta)

Phys-67 · physics · mathematics · Physics

A size-independent spectral gap above the spherical Laughlin line

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For the spherical $V_1$ pseudopotential $H_{N,Q}$ at flux $Q=3(N-1)$ on $wedge^N$ $U_Q$, is $H_{N,Q}\geq (1/25)(I-P_L,N)$ for every sufficiently large N, where $P_L,N$ projects onto the Laughlin vector $product_{i<j}(u_i$ $v_j-u_j$ $v_i)^3$?

Short English statement

For the spherical $V_1$ pseudopotential $H_{N,Q}$ at flux $Q=3(N-1)$ on $wedge^N$ $U_Q$, is $H_{N,Q}\geq (1/25)(I-P_L,N)$ for every sufficiently large N, where $P_L,N$ projects onto the Laughlin vector $product_{i<j}(u_i$ $v_j-u_j$ $v_i)^3$?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

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

OpenAI claim summary for Phys-67

The spherical fermionic Laughlin $V_1$ model is claimed uniformly gapped at filling $1/3$, with a stronger lower bound on the square of the interaction across the entire lowest-level Fock space. The question retains these same parameters and conventions. Within these assumptions, this is a claimed affirmative answer to the stated question.

A size-independent spectral gap above the spherical Laughlin line

OpenAI's claim

OpenAI presents a proof in the selected manuscript. The spherical fermionic Laughlin $V_1$ model is claimed uniformly gapped at filling $1/3$, with a stronger lower bound on the square of the interaction across the entire lowest-level Fock space.

Mathematical statement of the claimed result

Result 1.
For the lowest-Landau-level pseudopotential $H_{N,Q}=\sum_{i<j}P_{ij}^{(1)}$ on $\bigwedge^NU_Q$, with pair total-spin projector $Q-1$ and coefficient one, the source claims an integer $N_0$ such that \[ H_{N,3(N-1)}\ge\frac1{25}(I-P_{\mathrm L,N})\qquad(N\ge N_0). \] Here $P_{\mathrm L,N}$ projects onto the line spanned by $\prod_{i<j}(u_iv_j-u_jv_i)^3$. Thus the spherical Laughlin line is a unique zero-energy ground space with a size-independent positive excitation gap.

Outline of the argument

Exterior-algebra identities expand the interaction square into spin coefficients. Uniform asymptotic control of these coefficients bounds cross terms against the original interaction, giving a Fock-space inequality independent of particle number and hence the Laughlin gap.

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 →