The centre of a normal 3x3 magic square is 5

The centre cell of every normal $3 \times 3$ magic square is $5$.

In any $3 \times 3$ magic square of line sum $s$ the centre entry is $s/3$ (MacMahon): adding the middle row, the middle column and the two diagonals counts the centre four times and every other cell once, giving $\mathrm{total} + 3\,M_{11} = 4s$ while $\mathrm{total} = 3s$. For a normal square $s = 15$, so $M_{11} = 5$.

Formalization Note This is an immediate consequence of the two children MagicSquares.normal_order_three_constant ($s = 15$) and MagicSquares.center_of_order_three ($3\,M_{11} = s$); the natural-number arithmetic is discharged by omega.