The vanishing list of the semi-magic counting polynomial

Proved

MagicSquares.semi_magic_vanishing

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

combinatoricsehrhartenumerative-combinatoricsmagic-squares

The vanishing list. Let $n\ge 1$ and let $p\in\mathbb{Q}[X]$ agree with $H_{n}$ on the nonnegative integers. Then $p$ vanishes at the negative integers $-1,-2,\dots,-(n-1)$ : for every integer $k$ with $1\le k\le n-1$ we have $p(-k)=0$ . This is the statement that the polytope has no interior lattice points on the relevant dilates, and it is the second identity of the goal. At $n=1$ the condition is vacuous.

Preamble

import Mathlib
import Definitions.Def_MagicSquares
open MagicSquares

Formal statement

namespace MagicSquares

theorem semi_magic_vanishing (n : ℕ) (hn : 1 ≤ n) (p : Polynomial ℚ)
    (hp : ∀ t : ℕ, p.eval (t : ℚ) = (semiMagicCount n 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$ , and let $p\in\mathbb{Q}[X]$ be any polynomial satisfying $p(t)=\operatorname{semiMagicCount}(n,t)$ in $\mathbb{Q}$ for every natural number $t$ . Then for every integer $k$ , the implication

1\le k \quad\text{and}\quad k\le n-1 \;\Longrightarrow\; p(-k)=0

holds, where $n-1$ in the upper bound is the integer subtraction (the natural $n$ coerced to $\mathbb{Z}$ , then decremented by $1$ ). In other words, $p$ vanishes at the negative integers $-k$ for each integer $k$ satisfying $1\le k\le n-1$ . Edge case: when $n=1$ , the upper bound becomes $k\le 0$ , which together with $1\le k$ is impossible, so the implication is vacuously true for every $p$ and asserts no actual vanishing.

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