Bijection between semi-magic squares and normalized parameters

The map

is a bijection from the normalized coefficient vectors — six nonnegative integers summing to $t$ with $\min(x,y,z)=0$ — onto the $3\times3$ semi-magic squares of line sum $t$. Consequently

Surjectivity and injectivity are exactly the two halves of sm3_canonical; what is left is the bookkeeping that turns a bijection of carriers into an equality of Finset.cards. Two coercions have to be handled explicitly. First, semiMagicCount 3 t counts arrays with entries in Fin (t+1), so the forward map must be read into that finite type — legitimate because every entry of a semi-magic square of line sum $t$ is at most $t$. Second, sm3Count t counts functions Fin 6 → Fin (t+1), and the bound is again lossless because the six coefficients sum to $t$.

Formalization Note Both directions therefore need a Finset.card_bij with an explicit proof that the round trip is the identity on each side.