Horizontal flip preserves magicness

Proved

MagicSquares.flipHorizontal_preserves_magic

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

combinatoricsmagic-squares

Horizontal reflection. Reversing the order of the columns of a magic square again gives a magic square, with the same line sum.

This is the mirror image of the vertical flip: $(i,j)\mapsto(i,\,n-1-j)$ sends columns to columns and rows to rows, and interchanges the two main diagonals. All lines therefore still sum to $S$ .

Formalization Note flipHorizontal reverses the column index via Fin.rev. Row sums are invariant by reindexing; the two diagonals are swapped.

Preamble

import Mathlib
import Definitions.Def_MagicSquares
import Definitions.Def_MagicSquaresTransforms

Formal statement

namespace MagicSquares

theorem flipHorizontal_preserves_magic {n : ℕ} {α : Type*} [AddCommMonoid α]
    (M : Square n α) (s : α) (hM : IsMagic M s) :
    IsMagic (flipHorizontal M) s := by sorry

end MagicSquares

Source

Beck, Cohen, Cuomo & Gribelyuk, The number of ``magic'' squares, cubes and hypercubes, Amer. Math. Monthly 110 (2003), 707--717; arXiv:math/0201013v3.

View graph