OAI.Laughlin.mainTarget_proved

The theorem states that the defined proposition MainTarget holds, a spectral-gap-type bound for N particles each with Q+1 basis levels (a_i in {0,...,Q}). A state is a complex function ψ on configurations a: Fin N → Fin(Q+1), and it is antisymmetric if exchanging the entries of a at any two distinct positions i and j negates ψ. The energy of ψ is the sum over pairs i<j and over p from 0 to 2Q-2 of the squared norms of pair amplitudes, restricted to configurations with a_i = a_j = 0. The pair amplitude at (i,j,p) is the sum over levels x,y of a coefficient c_p(x,y) times ψ with a_i replaced by x and a_j replaced by y, where c_p(x,y) vanishes unless x+y = p+1, and then equals (x-y)/√2 times a square root of a ratio of descending factorials and factorials in Q, x, y and p. The Laughlin vector is built from the polynomial, in spinor variables X(i,false), X(i,true), equal to the product over i<j of the cube of the bracket X(i,false)X(j,true) - X(j,false)X(i,true). Its value at a is the coefficient of the monomial with exponent a_i on X(i,true) and Q-a_i on X(i,false), divided by the product over i of √binomial(Q,a_i). The squared distance to the Laughlin vector is the infimum over complex scalars c of the sum over configurations of |ψ(a) - c·Laughlin(a)|². MainTarget asserts that there is N₀ ≥ 2 such that for every N ≥ N₀, with Q = 3(N-1), every antisymmetric state ψ satisfies (1/100) times its squared distance to the Laughlin vector at most its energy. This is stated as an admitted theorem, not a verified proof.