Functional equation for n equal three

Proved

MagicSquares.interior_functional_eq_nat_three

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

combinatoricsehrhartenumerative-combinatoricsmagic-squares

Let p in Q[X] agree with H_3 on all naturals. Then for every natural u,p(-3-u) = (-1)^{4} p(u).Since (3-1)^2 is four the sign is one. H_3 is MacMahon polynomial of degree four, so p equals that polynomial and both sides agree. This is the n equal three case.Formalization Note Lean writes rationals as Rat; n is fixed to three.

Preamble

import Mathlib
import Definitions.Def_MagicSquares
open MagicSquares

Formal statement

namespace MagicSquares

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

end MagicSquares

Source

P. A. MacMahon, Combinatory Analysis Vol II (1916); R. P. Stanley, Duke Math. J. 40 (1973), 607--632, specialized to n equal three.

View graph