Sharpness conjecture for the lattice three-point bound in dimension 4

A lattice packing in $\mathbb{R}^4$ has density bounded above by the lattice three-point bound, obtained from a semidefinite-programming formulation of the three-point bound. Sharpness conjecture. The second three-point bound for lattice packing is sharp in dimension $4$. This conjecture is motivated by the agreement of the bound with the density of the $D_4$ lattice to five decimal places; the detailed function-theoretic formulation below specifies what a sharp certificate would require.

There exists a Schwartz function $f \colon \mathbb{R}^4 \times \mathbb{R}^4 \to \mathbb{R}$ satisfying $f(0,0)=1$, $\widehat{f}(0,0)=4$, the stated negativity condition away from the origin on the admissible region, $\widehat{f}(x,y)\geq 0$ for all $x,y$, and vanishing on $D_4\times D_4$ and on $D_4^*\times D_4^*$, where $D_4=\{x\in\mathbb{Z}^4:x_1+x_2+x_3+x_4\text{ is even}\}$ and $D_4^*$ is its dual lattice. The existence of such a function would give a sharp certificate for the dimension-$4$ lattice three-point bound.