Functional equation for n equal two

Proved

MagicSquares.interior_functional_eq_nat_two

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

combinatoricsehrhartenumerative-combinatoricsmagic-squares

Let p in Q[X] agree with H_2 on all naturals. Then for every natural u,p(-2-u) = (-1)^{1} p(u).Since (2-1)^2 is one the sign is minus one. H_2(t) is t plus one, so p is X plus one and both sides equal minus one minus u. This is the n equal two case, used with the one, three, four and n at least five cases.Formalization Note Lean writes rationals as Rat; n is fixed to two.

Preamble

import Mathlib
import Definitions.Def_MagicSquares
open MagicSquares

Formal statement

namespace MagicSquares

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

end MagicSquares

Source

R. P. Stanley, Duke Math. J. 40 (1973), 607--632; M. Beck et al., Amer. Math. Monthly 110 (2003), 707--717 (arXiv:math/0201013), specialized to n equal two.

View graph