The pandiagonal squares of order three: BCCG's P_3

Proved

MagicSquares.pandiagonal_count_three

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

combinatoricsenumerative-combinatoricsmagic-squares

The order-three pandiagonal count. With $P_{n}(t)$ as above, the theorem determines

P_{3}(t)=\binom{t+2}{2}=\frac{t^{2}+3t+2}{2},

a degree-two polynomial that never vanishes: $1,3,6,10,15,21,\dots$ for $t=0,1,2,\dots$ . This is Beck--Cohen--Cuomo--Gribelyuk's $P_{3}$ , and it sits inside their structural theorem that $P_{n}$ is a quasi-polynomial of degree $n^{2}-3n+2$ (which is $2$ at $n=3$ ). Proof. Every pandiagonal $3\times3$ square of line sum $t$ has the form $M_{ij}=g(i+j)$ for a single $g$ defined on $\mathbb{Z}/3$ : the broken-diagonal conditions run the three entries of each wrapped diagonal through the same cyclic pattern, and the line sum is then $g(0)+g(1)+g(2)=t$ . So the count is the number of triples of naturals summing to $t$ , equivalently the number of pairs $(a,b)$ with $a+b\le t$ , which is $\binom{t+2}{2}$ .

Contrast. This is not panMagicCount 3, which asks in addition that the ascending broken diagonals sum to the line sum; that stronger condition leaves only the constant square and gives a count vanishing off multiples of three, $1,0,0,1,0,0,1,\dots$

Preamble

import Mathlib
import Definitions.Def_MagicSquares
import Definitions.Def_MagicSquaresPandiagonal
open MagicSquares

Formal statement

namespace MagicSquares

theorem pandiagonal_count_three (t : ℕ) : pandiagonalCount 3 t = (t + 2).choose 2 := 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).

View graph