Ehrhart-Macdonald reciprocity for the semi-magic counting function

Open

MagicSquares.semi_magic_reciprocity

by Yuxuan Xu · Sep 19, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsehrhartenumerative-combinatoricsmagic-squares

The reciprocity law. Let $n\ge 1$ and let $p\in\mathbb{Q}[X]$ agree with $H_{n}$ on the nonnegative integers. Then $p(-n-t)=(-1)^{n-1}p(t)$ for every integer $t$ . This is the reflection $t\mapsto -n-t$ of the lattice-point count, rescaled by the sign $(-1)^{n-1}$ ; its right-hand side counts the interior of the corresponding polytope, by the Ehrhart--Macdonald reciprocity law. The identity is not visible from the combinatorial definition of $H_{n}$ , which is stated only for nonnegative $t$ .

Preamble

import Mathlib
import Definitions.Def_MagicSquares
open MagicSquares

Formal statement

namespace MagicSquares

theorem semi_magic_reciprocity (n : ℕ) (hn : 1 ≤ n) (p : Polynomial ℚ)
    (hp : ∀ t : ℕ, p.eval (t : ℚ) = (semiMagicCount n t : ℚ)) :
    ∀ t : ℤ, p.eval (((-(n : ℤ) - t : ℤ) : ℚ))
      = (-1 : ℚ) ^ (n - 1) * p.eval ((t : ℤ) : ℚ) := by
  sorry

end MagicSquares

Source

M. Beck, M. Cohen, J. Cuomo and P. Gribelyuk, The number of "magic" squares, cubes and hypercubes, Amer. Math. Monthly 110 (2003), 707--717 (arXiv:math/0201013); E. Ehrhart (1973); R. P. Stanley, Duke Math. J. 40 (1973) 607--632; J. Spencer, Amer. Math. Monthly 87 (1980) 397--399; M. Beck and D. Paxton, The Ehrhart polynomial of the Birkhoff polytope (arXiv:math.CO/0202267).

Read-back

What the Lean code literally says, in plain math · deepseek-v4.1-flash (WorkBuddy blind sub-agent)

Let $n$ be a natural number with $1\le n$ , and let $p\in\mathbb{Q}[X]$ be any polynomial satisfying that for every natural number $t$ , $p(t)=\operatorname{semiMagicCount}(n,t)$ (both sides viewed in $\mathbb{Q}$ ). Then for every integer $t$ ,

p((-n)-t)=(-1)^{\,n-1}\cdot p(t),

where $(-n)-t$ denotes $-n$ minus $t$ (i.e. the integer $-(n+t)$ , with $n$ first coerced to $\mathbb{Z}$ and negated, then subtracting $t$ , and finally lifted to $\mathbb{Q}$ ), and the exponent $n-1$ is the natural-number subtraction (safe because $1\le n$ ). The base $(-1)$ is the rational number $-1$ raised to the natural power $n-1$ . Thus the theorem asserts a symmetry of $p$ under the reflection $t\mapsto -n-t$ , rescaled by the factor $(-1)^{n-1}$ .

Human review

Endorsed by Shuze Chen · Sep 19, 2026
Endorsed by Yuxuan Xu · Sep 19, 2026
Confirmed by the mission captain (proposal self-audit).

View graph