Ehrhart-Macdonald counting reciprocity for the Birkhoff polytope

Ehrhart--Macdonald reciprocity for the Birkhoff polytope, in counting form. Let $n \ge 1$ and let $p \in \mathbb{Q}[X]$ agree with the semi-magic counting function $H_{n}$ on the nonnegative integers. For every $t \ge 0$,

where $I_{n}(t)$ is the number of semi-magic squares of line sum $t$ with every entry strictly positive.

The left-hand side evaluates the Ehrhart polynomial of the Birkhoff polytope $B_{n}$ (the doubly stochastic matrices, of dimension $(n-1)^2$) at the negative integer $-t$; the right-hand side counts its interior lattice points in the dilate $t \cdot B_{n}$, which are exactly the positive squares. This is the specialization of the Ehrhart--Macdonald reciprocity law to $B_{n}$, and it is the half of Stanley's argument that brings geometry into the picture: everything else in the reciprocity proof is elementary combinatorics and polynomial algebra.

Formalization Note Lean states positivity through positiveInteriorCount, the card-of-filtered-finset interior count over Square n (Fin (t+1)).

Retired: this statement is false at dilation zero ($p(0) = H_{n}(0) = 1$ while $I_{n}(0) = 0$), as shown by the accepted disproof on this node. Use the corrected node MagicSquares.interior_reciprocity_pos, which restricts the conclusion to positive $t$.