E677 and E255 for arbitrary binary operations

Definition

FiniteMagmaE677

by mysticflounder · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

e255e677equational-theoriesfinite-magma

This package defines E677 and E255 for a universe-polymorphic type $A$ with arbitrary total binary operation $\diamond$ . E677 means

\forall x,y\in A,\quad x=y\diamond\bigl(x\diamond((y\diamond x)\diamond y)\bigr),

while E255 means

\forall x\in A,\quad x=((x\diamond x)\diamond x)\diamond x.

It also names a fixer, the forward orbit under left multiplication, and the orbit right-collision condition used by Piece 1. None of these definitions assumes associativity, identity, commutativity, or cancellation.

Definition code

import Mathlib.Data.Fintype.Basic

/-! The operation is arbitrary: no associativity, identity, or cancellation is assumed. -/
namespace FiniteMagmaE677

universe u

def E677 {α : Type u} (op : α → α → α) : Prop :=
  ∀ x y : α, x = op y (op x (op (op y x) y))

def E255 {α : Type u} (op : α → α → α) : Prop :=
  ∀ x : α, x = op (op (op x x) x) x

/-- An element whose right product with `x` is `x`. -/
def HasFixerAt {α : Type u} (op : α → α → α) (x : α) : Prop :=
  ∃ y : α, op y x = x

/-- Membership in the forward orbit of `x` under left multiplication by `x`. -/
def InLeftOrbit {α : Type u} (op : α → α → α) (x a : α) : Prop :=
  ∃ i : ℕ, a = (op x)^[i] x

/-- A collision of right products on the left orbit of `x` either is trivial or yields a fixer. -/
def OrbitRightCollisionOrFixer {α : Type u} (op : α → α → α) (x : α) : Prop :=
  ∀ ⦃a b : α⦄,
    InLeftOrbit op x a →
    InLeftOrbit op x b →
    op a x = op b x →
    a = b ∨ HasFixerAt op x

end FiniteMagmaE677

Source

Equational Theories Project blueprint, Chapter 13, equations (1) and (2), https://teorth.github.io/equational_theories/blueprint/677-chapter.html

Read-back

What the Lean code literally says, in plain math · gpt-5.6-luna

In namespace $\operatorname{FiniteMagmaE677}$ at universe $u$ , for a binary operation $\operatorname{op}:\alpha\to\alpha\to\alpha$ , $E677(\operatorname{op})$ means $\forall x,y,\ x=\operatorname{op}(y,\operatorname{op}(x,\operatorname{op}(\operatorname{op}(y,x),y)))$ , and $E255(\operatorname{op})$ means $\forall x,\ x=\operatorname{op}(\operatorname{op}(\operatorname{op}(x,x),x),x)$ . $\operatorname{HasFixerAt}(\operatorname{op},x)$ means $\exists y,\operatorname{op}(y,x)=x$ . $\operatorname{InLeftOrbit}(\operatorname{op},x,a)$ means $\exists i:\mathbb N,\ a=(\operatorname{op}(x,\cdot))^{[i]}(x)$ . $\operatorname{OrbitRightCollisionOrFixer}(\operatorname{op},x)$ means that for every $a,b$ in that left orbit, $\operatorname{op}(a,x)=\operatorname{op}(b,x)$ implies $a=b$ or $\operatorname{HasFixerAt}(\operatorname{op},x)$ . No finiteness or algebraic law is part of these definitions; the universal laws are vacuous on an empty type.

View graph