Quantum Mechanics

Motivation

A known zero-energy vector does not by itself give a uniform positive gap above it. The Laughlin problem asks for a lower bound controlling every competing antisymmetric state. The pinned manuscript supplies the research context.

Setting

At N particles set Q=3(N−1). States are complex functions on finite configurations, with antisymmetry under exchanging particles. The energy is a sum of squared pair-annihilation amplitudes.

Formalization target

The selected goal is OAI.LaughlinGap.thm_main. Its central assertion is

$$\frac1{25}\operatorname{dist}(\psi,\mathbb C\Psi_{\rm L})^2\leq E(\psi).$$

The theorem states that there is a threshold N₀ ≥ 2 such that for every N ≥ N₀ and every antisymmetric complex-valued state ψ on N particles, each with local levels 0,…,Q where Q = 3(N−1), one has (1/25)·d(ψ)² ≤ E(ψ). Here a state assigns a complex number to each configuration a : Fin N → {0,…,Q}, and antisymmetric means that swapping the values at two distinct positions i and j negates ψ. The energy E(ψ) sums, over pairs i<j, over p = 0,…,2Q−2, and over configurations a with a_i = a_j = 0, the squared modulus of the pair amplitude, which is the sum over x,y of pairCoefficient(Q,p,x,y)·ψ(a with a_i replaced by x and a_j by y). The pair coefficient vanishes unless x+y = p+1, in which case it equals (x−y)/√2 times the square root of Q^{(x)}·Q^{(y)}·p! divided by Q·(2Q−2)^{(p)}·x!·y!, where m^{(k)} is the descending factorial. The Laughlin vector is built from the polynomial ∏{i<j}(x{i,0}x_{j,1} − x_{j,0}x_{i,1})³ in variables indexed by particle and a Boolean: its coefficient at the monomial with exponent a_i on x_{i,1} and Q−a_i on x_{i,0} is divided by ∏_i √C(Q,a_i). The quantity d(ψ)² is the infimum over complex c of the sum over configurations of |ψ(a) − c·Laughlin(a)|², the squared distance from ψ to the line spanned by the Laughlin vector, with no normalization of ψ assumed.

Significance and status

The selected goal has constant 1/25 and no normalization requirement on the state. The Fock-space inequality, the earlier 1/100 formulation and the planar endpoint are separate references; they retain their own representations and constants. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The bound must be uniform for all sufficiently large particle numbers and for every state, rather than a variational estimate on a selected excitation.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

Additional published targets are included as separate references:

• OAI.Laughlin.mainTarget_proved (Open).
• OAI.LaughlinFock.thm_fock (Open).
• OAI.Laughlin.planar_gap (Open).

Selected references

• OpenAI, A Fock-space inequality and the Laughlin spectral gap, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.