Counterexample structure (m) — A minimum counterexample has no abelian congruence other than equality

Let $(M,\diamond)$ be a finite E677 magma that fails E255 at a point $z$, that is, $q(z)\ne z$ with $q(z)=((z\diamond z)\diamond z)\diamond z$. Suppose that $M$ has minimum order: every E677 operation on $\{0,\dots,n-1\}$ with $n<|M|$ satisfies E255.

A congruence $\theta$ of $M$ is abelian when it satisfies the term condition $C(\theta,\theta;0)$: for every term function $p$ of arity $k+1$ (a map $M^{k+1}\to M$ given by a $\diamond$-term), all $x\,\theta\,y$ and all $c_1\,\theta\,d_1,\dots,c_k\,\theta\,d_k$,

Theorem. Every abelian congruence of $M$ is the equality relation.

Use in a counterexample search. In the normal form of Counterexample structure (k), the congruence generated by $(z,q(z))$ is the least congruence other than equality (the monolith). By this theorem the monolith is not abelian, and $M$ is not an abelian algebra (take $\theta$ universal). For example, $M$ is not an affine extension $(x,s)\diamond(y,t)=(x\diamond y,\ \alpha_{x,y}s+\beta_{x,y}t+c_{x,y})$ over an abelian group with at least two elements, with endomorphisms $\alpha_{x,y},\beta_{x,y}$: there "same first coordinate" is an abelian congruence (by induction on terms; not part of the Lean theorem). ETP blueprint Lemma 13.4 already excludes these extensions; the theorem needs no such coordinates.

Proof idea. Only the term $x_1\diamond x_0$ is used. For this term, the term condition says: two $\theta$-related rows that agree in a column $t$ agree in every column $\theta$-related to $t$. If $\theta$ relates two distinct elements, then $M/\theta$ is a smaller E677 magma, so it satisfies E255, and $q(z)\,\theta\,z$. Counterexample structure (g) then gives two $\theta$-related rows that agree in column $z$ and differ in a column $\theta$-related to $z$.

Prior work. The term condition is standard (R. Freese and R. McKenzie, Commutator Theory for Congruence Modular Varieties, Definitions 3.2 and 5.3; with one distinguished variable as in M. Bonatto and D. Stanovský, arXiv:1902.08980v3). The step from an abelian congruence to row agreement is Lemma 5.1 of Bonatto and Stanovský (arXiv:1902.08980v3): in every left quasigroup (a finite E677 magma is one, by Lemma 13.1(i)), $C(\alpha,\beta;0)$ implies that $\mathrm{Dis}_\beta$ acts $\alpha$-semiregularly. With $\alpha=\beta=\theta$ and the displacements $L_sL_{s'}^{-1}$ for $s\mathrel{\theta}s'$, this gives row agreement. The step from row agreement to E255 is T. Tao's argument (ETP Zulip thread "FINITE: 677 -> 255", 2024-12-14). With these two steps and minimality, the theorem is a short corollary. B. Le Floch (same thread, 2024-12-14) proved that the affine extensions above satisfy E255 when the base does (ETP blueprint Lemma 13.4). S. Chuks-Onah (same thread, June 2026) proposed to exclude a minimal counterexample through its monolith $\mu$ by Lemma 13.4 when the step $M\to M/\mu$ is affine; one step of his argument that it is affine was not proved. On 2026-06-20 he wrote, with no proof, that an abelian displacement group $\mathrm{Dis}_\mu$ makes the monolith step affine, so that the linear-extension lemma applies. No earlier proof of the theorem was found in the ETP blueprint, the ETP paper (arXiv:2512.07087v2), the ETP Zulip thread up to 2026-10-14, Freese–McKenzie, Burris–Sankappanavar, or papers on left quasigroups and racks; his claim of 2026-06-20, with the lemma above, would give it. The new content is a proof, checked in Lean.

Formalization Note The hypotheses h, hmin, z, hz, r, hr and hcompat are those of Counterexample structure (b), so the theorem applies directly to the output of (k). A term function of arity $k+1$ is a function p : (Fin (k + 1) → α) → α that satisfies every predicate T that holds at the projections fun v => v i and is closed under pointwise op. The tuple $(x,c_1,\dots,c_k)$ is Fin.cons x c, and the term condition is habel.