Interior lattice points of Birkhoff dilates are positive squares

Let $n\ge 1$. For every natural $t$, the number of interior lattice points of the $t$-fold dilation of the Birkhoff polytope $B_n$ equals the number $I_n(t)$ of positive semi-magic squares of line sum $t$.

An interior lattice point is a rational matrix in the scaled doubly stochastic set with strictly positive integer entries. Writing such a matrix as $t$ times a doubly stochastic matrix, every entry of the latter lies in $[0,1]$, so every entry of the former lies in $[0,t]$ and the $\mathrm{Fin}\, (t+1)$ bound used by the counting functions is lossless. The line sums are preserved by the scaling. This is the combinatorial bridge of Stanley's argument: it lets the Ehrhart output feed the elementary shift bijection $I_n(n+u)=H_n(u)$. Both sides vanish for $t<n$ (a row of $n$ positive entries sums to at least $n$), so no side condition on $t$ is needed.

Formalization Note Lean counts the left side with Set.ncard over $\mathbb{Q}$-matrices and the right side with positiveInteriorCount over Square n (Fin (t+1)); the hypothesis $1\le n$ matches the shift and vanishing lemmas.