BCCG Theorem 1: the counting polynomial of semi-magic squares

Open

MagicSquares.semi_magic_polynomial

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

combinatoricsehrhartenumerative-combinatoricsmagic-squares

Goal. For every order $n\ge 1$ there is a polynomial $p\in\mathbb{Q}[X]$ which, simultaneously, has degree exactly $(n-1)^{2}$ , agrees with the counting function $H_{n}$ at every nonnegative integer, satisfies the reciprocity law $p(-n-t)=(-1)^{n-1}p(t)$ for every integer $t$ , and vanishes at $-1,-2,\dots,-(n-1)$ . This is Theorem 1 of Beck--Cohen--Cuomo--Gribelyuk, proved by Ehrhart and by Stanley in 1973 and given an elementary proof by Spencer in 1980. It separates the semi-magic squares from the magic, symmetric and pandiagonal classes, whose counting functions are quasi-polynomials rather than polynomials.

Preamble

import Mathlib
import Definitions.Def_MagicSquares
open MagicSquares

Formal statement

namespace MagicSquares

theorem semi_magic_polynomial (n : ℕ) (hn : 1 ≤ n) :
    ∃ p : Polynomial ℚ,
      p.natDegree = (n - 1) ^ 2 ∧
        (∀ t : ℕ, p.eval (t : ℚ) = (semiMagicCount n t : ℚ)) ∧
          (∀ t : ℤ, p.eval (((-(n : ℤ) - t : ℤ) : ℚ))
            = (-1 : ℚ) ^ (n - 1) * p.eval ((t : ℤ) : ℚ)) ∧
            (∀ k : ℤ, 1 ≤ k → k ≤ (n : ℤ) - 1 → p.eval (-(k : ℚ)) = 0) := 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$ . Then there exists a polynomial $p\in\mathbb{Q}[X]$ satisfying all of the following simultaneously:

its natural degree equals $(n-1)^2$ , where $n-1$ is the natural-number subtraction (so $p$ is necessarily non-zero of ordinary degree $(n-1)^2$ );
for every natural number $t$ , $p(t)=\operatorname{semiMagicCount}(n,t)$ in $\mathbb{Q}$ ;
for every integer $t$ , $p((-n)-t)=(-1)^{\,n-1}\,p(t)$ , where $(-n)-t$ is $-n$ minus $t$ (lifted to $\mathbb{Q}$ ) and the exponent $n-1$ is natural subtraction;
for every integer $k$ , if $1\le k$ and $k\le n-1$ (integer subtraction) then $p(-k)=0$ .

Here $\operatorname{semiMagicCount}(n,t)$ counts the $n\times n$ arrays over $\operatorname{Fin}(t+1)$ (entries integers $0,\dots,t$ ) whose every row and column sums to $t$ . When $n=1$ the stated degree is $0$ , the reciprocity factor is $(-1)^0=1$ , and the vanishing condition is vacuously true.

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