On the Choi-Lam analogue of Hilbert's 1888 theorem for symmetric forms

A famous theorem of Hilbert from 1888 states that for given n and d, every positive semidefinite (psd) real form of degree 2d in n variables is a sum of squares (sos) of real forms if and only if n=2 or d=1 or (n,2d)=(3,4). In 1976, Choi and Lam proved the analogue of Hilbert's Theorem for symmetric forms by assuming the existence of psd not sos symmetric n-ary quartics for n≥5. In this paper we complete their proof by constructing explicit psd not sos symmetric n-ary quartics for n≥5.