Positive semi-magic squares shift to line sum t - n

Proved

MagicSquares.positive_shift_count

by Tamas Fulop · Sep 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsehrhartenumerative-combinatoricsmagic-squares

The shift bijection between positive and ordinary semi-magic squares. Let $n \ge 1$ and $t \ge n$ . Subtracting the all-ones matrix $J$ gives a bijection between the positive semi-magic squares of line sum $t$ (every entry at least one) and all semi-magic squares of line sum $t - n$ , so that

I_{n}(t) = H_{n}(t - n).

The map is its own inverse up to adding $J$ back: since $J$ itself has every line sum equal to $n$ , subtracting it drops every line sum by exactly $n$ while preserving nonnegativity precisely for the positive squares. This is the elementary combinatorial half of Stanley's reciprocity argument: it converts the geometric interior count supplied by Ehrhart--Macdonald reciprocity into an ordinary value of the counting function, with no polyhedral machinery of its own.

Formalization Note Lean states both sides as cardinals over Square n (Fin (t+1))-style finsets via positiveInteriorCount and semiMagicCount, with t - n the truncated natural subtraction (exact here since $t \ge n$ ).

Preamble

import Mathlib
import Definitions.Def_MagicSquares
import Definitions.Def_MagicSquares_positiveInteriorCount
open MagicSquares

Formal statement

namespace MagicSquares

theorem positive_shift_count (n t : ℕ) (hn : 1 ≤ n) (hnt : n ≤ t) :
    positiveInteriorCount n t = semiMagicCount n (t - n) := by sorry

end MagicSquares

Source

R. P. Stanley, Duke Math. J. 40 (1973), 607--632, interior points of dilates of the Birkhoff polytope via the all-ones shift; M. Beck and D. Paxton, The Ehrhart polynomial of the Birkhoff polytope (arXiv:math.CO/0202267).

View graph