The normal members of MacMahon's order-three family

Characterization of the normal squares inside MacMahon's order-three family.

For $(a,c)\in\mathrm{paramSet}\ 5$,

Here normal means the nine entries lie in $[1,9]$ and are pairwise distinct, i.e. they are a permutation of $1,\dots,9$; and

Proof. Normality forces $1\le a\le 9$ and $1\le c\le 9$, since $a=M_{00}$ and $c=M_{02}$ are entries. This leaves $81$ pairs, each of which is a ground instance and is settled by evaluation. The eight surviving pairs are exactly those for which the corner entries $a$ and $c$ are distinct members of $\{2,4,6,8\}$ with $a+c\ne 10$; the pairs with $a+c=10$ are excluded because then $M_{21}=a+c-5=5$ coincides with the centre.

Formalization Note IsNormal is stated with a Function.Injective, which is not decidable as given, so it is first rewritten into an explicit conjunction of entrywise bounds over Fin 3 and pairwise-distinctness of the nine positions. The quantifiers over Fin 3 are then unfolded with Fin.forall_fin_succ before norm_num decides the resulting ground instances. Because the parametrization is over $\mathbb{N}$, entries such as $a+c-5$ and $15-a-c$ truncate at zero, and each instance is evaluated with the truncation in place.