Finite E677 implies E255 under parameterized row transport

Proved

FiniteMagmaE677.e255_of_e677_of_parametrized_row_transport

by omegaestable · Oct 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

conditionale255e677equational-theoriesfinite-magmarow-transport

Let $M$ be a finite type, possibly empty, equipped with an arbitrary total binary operation $*$ . Assume E677,

\forall x,y\in M,\quad y*(x*((y*x)*y))=x,

and the parameterized row-transport condition (PRT),

\forall x,a\in M\;\exists c,e\in M:\quad (a*e)*(c*(x*(x*((a*x)*a))))=(x*e)*x.

Then E255 holds:

\forall x\in M,\quad ((x*x)*x)*x=x.

This is a conditional sufficient criterion for the finite E677-to-E255 implication. The witnesses $c$ and $e$ may depend on both $x$ and $a$ . The PRT condition is an explicit additional hypothesis; it is not asserted to follow from E677, so this result does not settle the unrestricted implication. No associativity, commutativity, or identity element is assumed.

Preamble

import Definitions.Def_FiniteMagmaE677

universe u

Formal statement

theorem FiniteMagmaE677.e255_of_e677_of_parametrized_row_transport {α : Type u} [Fintype α]
    (op : α → α → α)
    (h : FiniteMagmaE677.E677 op)
    (hPRT : ∀ x a : α, ∃ c e : α,
      op (op a e) (op c (op x (op x (op (op a x) a)))) = op (op x e) x) :
    FiniteMagmaE677.E255 op := by sorry

Source

Original conditional result T186 in the E677-to-E255 research, with a self-contained proof. The ambient E677 and E255 laws are those of Chapter 13, Lemma 13.1 of the Equational Theories Project blueprint: https://teorth.github.io/equational_theories/blueprint/677-chapter.html. The PRT premise and this conditional implication are original to this contribution, not claims attributed to the blueprint.

View graph