Ehrhart-Macdonald reciprocity for the Birkhoff polytope

Let $n\ge 1$ and let $p$ be a rational polynomial with $p(t)=H_n(t)$ for every natural $t$. Then for every natural $t\ge 1$, the value of $p$ at $-t$ equals, up to the sign $(-1)^{(n-1)^2}$, the number of interior lattice points of the $t$-fold dilation of the Birkhoff polytope $B_n$.

Here $B_n$ is the set of doubly stochastic matrices (nonnegative real matrices with all row and column sums equal to $1$), formalized as doublyStochastic; its vertices are the permutation matrices by the Birkhoff-von Neumann theorem, so it is an integral polytope of dimension $(n-1)^2$. Its interior lattice points in the $t$-fold dilation are exactly the strictly positive integer matrices with line sum $t$. This is the Ehrhart-Macdonald reciprocity law applied to $B_n$, due to Ehrhart and to Stanley (magic labelings of graphs). It is the geometric input of Stanley's proof: combined with the identification of the interior count with $I_n(t)$, it yields reciprocity at positive dilations.

Formalization Note Lean works with $\mathbb{Q}$-valued matrices and counts with Set.ncard (no finiteness instance needed to state it). The dilation is written with an explicit scaled witness. The hypothesis $1\le t$ is essential: at $t=0$ the left side is $p(0)=H_n(0)=1$ while the interior is empty, so the unqualified statement is false.