Functional equation for semi-magic counts at natural shifts

Open

MagicSquares.interior_functional_eq_nat

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

combinatoricsehrhartenumerative-combinatoricsmagic-squares

Let n >= 1 and let p in Q[X] agree with the semi-magic counting function H_{n} on all nonnegative integers. Then for every natural number u,

p(-n-u) = (-1)^{(n-1)^2} p(u).

This is the restriction to natural shifts of the Ehrhart-Macdonald reciprocity law for the Birkhoff polytope. Combined with the shift bijection identifying positive squares of line sum t >= n with ordinary squares of line sum t-n, and with vanishing of both sides for t < n, it yields the full interior reciprocity at positive dilation.

Formalization Note Lean writes rationals as Rat and casts naturals explicitly; the exponent uses truncated natural subtraction, harmless here since 1 <= n.

Preamble

import Mathlib
import Definitions.Def_MagicSquares
open MagicSquares

Formal statement

namespace MagicSquares

theorem interior_functional_eq_nat (n : Nat) (hn : 1 <= n) (p : Polynomial Rat) (hp : forall t : Nat, p.eval (t : Rat) = (semiMagicCount n t : Rat)) (u : Nat) :
    p.eval (-(((n + u : Nat)) : Rat)) = (-1 : Rat) ^ ((n - 1) ^ 2) * p.eval ((u : Rat)) := by sorry

end MagicSquares

Source

R. P. Stanley, Duke Math. J. 40 (1973), 607--632, Ehrhart-Macdonald reciprocity applied to the Birkhoff polytope; E. Ehrhart (1973); M. Beck, M. Cohen, J. Cuomo and P. Gribelyuk, Amer. Math. Monthly 110 (2003), 707--717 (arXiv:math/0201013).

View graph