Counterexample structure (g) — Fixer block: a pointwise form of Tao's row-agreement argument (Lean formalization)

Let $(M,\diamond)$ be a finite magma that satisfies E677 and let $\theta$ be a congruence of $(M,\diamond)$. Let $z\in M$ satisfy $((z\diamond z)\diamond z)\diamond z\ne z$ and $((z\diamond z)\diamond z)\diamond z\;\theta\;z$, and put $s=(z\diamond z)\diamond z$. Then there are $a\ne a'$ in the $\theta$-class of $s$ and $u$ in the $\theta$-class of $z$ with $a\diamond z=a'\diamond z$ and $a\diamond u\ne a'\diamond u$.

So at each point where E255 fails, a counterexample has two rows that agree in one column and differ in another column of the same class. In the other direction: if any two rows from the class of $s$ that agree in column $z$ agree on the whole class of $z$, then E255 holds at $z$.

Attribution. The argument is T. Tao's (ETP Zulip thread "FINITE: 677 -> 255", 2024-12-14). He stated it for extension models $(x,s)\diamond(y,t)=(x\diamond y,s\diamond_{x,y}t)$ over a base that satisfies E255: if left multiplications in one fibre that agree at one point agree everywhere, the right multiplications are injective and E255 follows, "so we need operations $\diamond_{x,y}$ for which left-multiplication by different elements $s,s'$ can agree in some locations but not in others." The step that the rows of the fixer block are pairwise distinct is B. Le Floch's argument for piecewise affine extensions (same thread, 2024-12-14), which Tao's message states for all extension models. This theorem is a pointwise form of Tao's argument: one point $z$, one pair of classes, and a hypothesis on the quotient only at $z$. All classes of $\theta$ have the same size (M. Bonatto and D. Stanovský, arXiv:1902.08980v3).