Small orders (7) — Every E677 magma with 7 elements has an idempotent

Proved

FiniteMagmaE677.exists_idempotent_of_card_seven

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

e677finite-modelidempotentmagmasmall-order

Every magma with 7 elements that satisfies E677 has an idempotent: if an operation $\diamond$ on $\{0,\dots,6\}$ satisfies $x=y\diamond(x\diamond((y\diamond x)\diamond y))$ for all $x,y$ , then $x\diamond x=x$ for some $x$ .

This is the hypothesis h7 of Counterexample structure (h), (i) and (j), with the same Lean type. (i) uses no other small-order fact.

Prior work (ETP Zulip thread "FINITE: 677 -> 255"): D. McNeil (2024-12-07) reported two non-isomorphic E677 magmas of order 7. J. Brox (2025-03-26) gave the two isomorphism classes of E677 magmas of order 7. B. Reinke (2026-05-15) reported, from an enumeration, that all E677 magmas of order 7 are linear. S. Chuks-Onah (2026-05-16, SAT) found at least 60 distinct E677 tables of order 7, each with exactly one idempotent.

Preamble

import Definitions.Def_FiniteMagmaE677
import Mathlib

open FiniteMagmaE677

Formal statement

theorem FiniteMagmaE677.exists_idempotent_of_card_seven :
∀ op : Fin 7 → Fin 7 → Fin 7, FiniteMagmaE677.E677 op → ∃ x : Fin 7, op x x = x := by sorry

Source

Adam McKenna, private repo, 2026-10-26: Lean proof generated by experiments/analysis/small-order-lean-2026-10-26/gen_idem.py (statement of hasIdempotentOfCard_seven, lean/E677/SmallOrderSeven.lean)

View graph