E677 gives a backward recurrence

Open

FiniteMagmaE677.backward_recurrence

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

e255e677equational-theoriesfinite-magma

Let $A$ be finite with arbitrary operation $\diamond$ satisfying E677. For every $x,y\in A$ ,

x=(y\diamond x)\diamond\bigl((y\diamond(y\diamond x))\diamond y\bigr).

This is the backward-recurrence identity of Lemma 13.1(iii).

Preamble

import Definitions.Def_FiniteMagmaE677

universe u

Formal statement

theorem FiniteMagmaE677.backward_recurrence {α : Type u} [Fintype α]
    (op : α → α → α) (h : FiniteMagmaE677.E677 op) (x y : α) :
    x = op (op y x) (op (op y (op y x)) y) := by sorry

Source

Equational Theories Project, online proof blueprint, Chapter 13, Lemma 13.1, https://teorth.github.io/equational_theories/blueprint/677-chapter.html, part (iii)

Read-back

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

For every universe u, finite possibly empty type $\alpha:\mathrm{Type}\,u$ , arbitrary operation $\operatorname{op}:\alpha\to\alpha\to\alpha$ , and hypothesis h saying that every $a,b\in\alpha$ satisfy $a=\operatorname{op}\bigl(b,\operatorname{op}(a,\operatorname{op}(\operatorname{op}(b,a),b))\bigr)$ , for all $x,y\in\alpha$ , $x=\operatorname{op}\bigl(\operatorname{op}(y,x),\operatorname{op}(\operatorname{op}(y,\operatorname{op}(y,x)),y)\bigr)$ . Finiteness is an explicit scope hypothesis but no cardinality bound occurs in the conclusion; there are no free parameters or further algebraic, distinctness, or nonemptiness side conditions.

View graph