Functional equation for n at least five
OpenMagicSquares.interior_functional_eq_nat_ge_fivecombinatoricsehrhartenumerative-combinatoricsmagic-squares
Let n >= 5 and p in Q[X] agree with H_n on all naturals. Then for every natural u,p(-n-u) = (-1)^{(n-1)^2} p(u).This is the remaining hard core after the n equal one through four cases, which are proved via explicit polynomials. Combined with those cases by splitting on n, it yields the general natural-shift functional equation.Formalization Note Lean writes rationals as Rat; hypothesis is 5 <= n, stronger than 1 <= n.
Preamble
import Mathlib import Definitions.Def_MagicSquares open MagicSquares
Formal statement
namespace MagicSquares
theorem interior_functional_eq_nat_ge_five (n : Nat) (hn : 5 <= n) (p : Polynomial Rat) (hp : forall t : Nat, p.eval (t : Rat) = (semiMagicCount n t : Rat)) (u : Nat) :
p.eval (-(((n + u : Nat)) : Rat)) = (-1 : Rat) ^ ((n - 1) ^ 2) * p.eval ((u : Rat)) := by sorry
end MagicSquaresSource
R. P. Stanley, Duke Math. J. 40 (1973), 607--632; E. Ehrhart (1973); M. Beck et al., Amer. Math. Monthly 110 (2003), 707--717 (arXiv:math/0201013), remaining core n at least five.