Small orders (4) — No E677 magma has 4 elements

Proved

FiniteMagmaE677.no_e677_of_card_four

by mysticflounder · Oct 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

e677finite-modelmagmasmall-order

No magma with 4 elements satisfies E677: for every operation $\diamond$ on $\{0,1,2,3\}$ there are $x,y$ with $x\ne y\diamond(x\diamond((y\diamond x)\diamond y))$ .

This is the hypothesis h4 of Counterexample structure (h), with the same Lean type.

Prior work (ETP Zulip thread "FINITE: 677 -> 255"): I. Tencer (2024-12-07) reported that no E677 magma has order 2, 3, 4 or 6. S. Chuks-Onah (2026-05-01) reported the same for these orders.

Preamble

import Definitions.Def_FiniteMagmaE677
import Mathlib

open FiniteMagmaE677

Formal statement

theorem FiniteMagmaE677.no_e677_of_card_four :
∀ op : Fin 4 → Fin 4 → Fin 4, ¬ FiniteMagmaE677.E677 op := by sorry

Source

Adam McKenna, private repo, 2026-10-26: Lean theorem noE677OfCard_four (lean/E677/SmallOrderFour.lean), RUP certificates replayed as Lean proofs

View graph