The determinantal complexity of the $4\times 4$ permanent is 15

The best known lower bound on the determinantal complexity of the $4\times4$ permanent is 10. In this short note, I prove that this value is exactly 15: the $4\times4$ permanent is the determinant of a $15\times15$ matrix of affine linear forms, and cannot be that of any smaller matrix. To do so, I must establish both a lower and upper bound. To establish the upper bound, I use Grenet's construction of size $2^n-1$. Hence that construction is optimal at $n=4$ (and $n=3$). This now constitutes the first knwon exact value of the determinantal complexity of the permanent at $n=4$. Only the value at $n=3$ was exactly known, prior to this note. The general quadratic bound only gives 8 for $n=4$. To establish the lower bound, I work from a normal form at a zero of the permanent. In the first row (and column) of the normal form, the linear forms vanish on a linear space inside the singular locus of the permanent. A hessian inequality bounds the size of the matrix in terms of that space. Then, a matrix of sie 14 foces the space into any of nine corordinate types. The forcing is either up to symmetry, or else into a family that degenerates to one of them. I then rule out every case. All involved computations are exact. In respect of the claim, I have made all certificates public. The proof is short and easy to follow. This note is hand-written by the human author.