Vertical flip preserves magicness

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

The reflection $(i,j)\mapsto(n-1-i,\,j)$ sends rows to rows and columns to columns, so every row and column of the reflected array is a row or column of the original and sums to $S$. The two main diagonals are interchanged: the descending diagonal of the reflected square is the ascending diagonal of the original, and conversely. Since a magic square requires both diagonals to sum to $S$, the reflected array satisfies all the conditions.

Together with the horizontal flip and the transpose, this generates the full dihedral symmetry group of order $8$ of the square, under which the set of magic squares of a fixed line sum is closed — the fact that makes "up to symmetry" counts meaningful.

Formalization Note flipVertical reverses the row index via Fin.rev. Column sums are invariant because $i\mapsto n-1-i$ permutes $\mathrm{Fin}\,n$, and the diagonal swap is proved by the same reindexing.