Seven exact-base table entries force E255 at a point

Proved

FiniteMagmaE677.exact_base_rows_give_fixer

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

e255e677equational-theoriesfinite-magmaorbit

Let $(\alpha,\diamond)$ be a finite magma satisfying E677: for all $p,q\in\alpha$ ,

p=q\diamond\bigl(p\diamond((q\diamond p)\diamond q)\bigr).

Let $x,A,c_1,c_3,c_4\in\alpha$ satisfy the seven table entries

$x\diamond x=c_1$ ;
$x\diamond c_3=c_4$ ;
$c_1\diamond x=c_4$ ;
$A\diamond(A\diamond x)=A$ ;
$A\diamond A=c_1$ ;
$A\diamond x=c_3$ ;
$c_3\diamond c_3=c_1$ .

Then E255 holds at $x$ :

((x\diamond x)\diamond x)\diamond x=x.

The seven entries are the exact-base pattern observed at orbit size six with one element $A$ outside the left orbit of $x$ , where $c_n$ denotes the $n$ -th point of that orbit. The theorem shows that the pattern alone forces a fixer of $x$ , namely $(x\diamond x)\diamond x$ , with no orbit, period, or outsider-uniqueness hypothesis. It closes every finite E677 context in which these seven entries occur.

Formalization Note The five elements are arbitrary; no distinctness among them is assumed. The names $c_1,c_3,c_4$ record their role in the orbit-size-six pattern and are not tied to an orbit in the statement.

Preamble

import Definitions.Def_FiniteMagmaE677

universe u

Formal statement

theorem FiniteMagmaE677.exact_base_rows_give_fixer
    {α : Type u} [Fintype α] (op : α → α → α) (h : FiniteMagmaE677.E677 op)
    (x A c1 c3 c4 : α)
    (hxx : op x x = c1)
    (hxc3 : op x c3 = c4)
    (hc1x : op c1 x = c4)
    (hA_Ax : op A (op A x) = A)
    (hAA : op A A = c1)
    (hAx : op A x = c3)
    (hc3c3 : op c3 c3 = c1) :
    op (op (op x x) x) x = x := by sorry

Source

Supporting lemma for the finite E677 to E255 formalization, mission 508ccd7b-8791-4bdf-883c-9a44bd760881; Equational Theories Project blueprint, Chapter 13, https://teorth.github.io/equational_theories/blueprint/677-chapter.html; Bolan et al., arXiv:2512.07087v2, Section 8, Problem 8.1.

View graph