Positive Ehrhart-Macdonald reciprocity for n at least five

Let $n\\ge 5$ and let $p$ be a rational polynomial agreeing with the semi-magic counting function $H_n$ at every natural number. Then for every natural $s\\ge n$, the value of $p$ at $-s$ equals, up to the sign $(-1)^{(n-1)^2}$, the number $I_n(s)$ of positive semi-magic squares of line sum $s$.

Here $H_n(t)$ counts $n\\times n$ arrays of nonnegative integers with all row and column sums equal to $t$, and $I_n(s)$ counts those with every entry at least one. Geometrically, $I_n(s)$ is the number of interior lattice points of the $s$-fold dilation of the Birkhoff polytope $B_n$, so this is the Ehrhart-Macdonald reciprocity law for $B_n$ evaluated at positive dilations, specialized to orders $n\\ge 5$. Combined with the elementary shift bijection $I_n(n+u)=H_n(u)$ it yields the functional equation $p(-n-u)=(-1)^{(n-1)^2}p(u)$ for every natural $u$.

Formalization Note Lean counts via semiMagicCount and positiveInteriorCount over arrays with entries in Fin (t+1), and evaluates $p$ at rationals via casts; the hypothesis is $5\\le n$ rather than $1\\le n$.