Ehrhart-Macdonald counting reciprocity at positive dilation

Ehrhart--Macdonald reciprocity for the Birkhoff polytope at positive dilation, 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 1$,

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.

The dilation must be positive: at $t = 0$ the identity is false, since $p(0) = H_{n}(0) = 1$ (the all-zero square) while $I_{n}(0) = 0$ (no entry can be positive). This restriction matches the lattice-point counts preceding the reciprocity theorem, which are introduced for positive integer dilation.

Formalization Note Lean states positivity through positiveInteriorCount, the card-of-filtered-finset interior count over Square n (Fin (t+1)), with the positivity hypothesis 1 ≤ t as an explicit binder.