Motivation

An equation for a magma constrains a binary operation without assuming that it is associative, commutative, or has an identity. Which laws imply which others, over all magmas or over finite magmas only, is the question the Equational Theories Project studies at scale. Restricting the underlying set to be finite can change the answer: a structural argument may depend on the fact that a surjective self-map of a finite set is injective.

The project's December 2025 paper reports the finite implication from E677 to E255 as unresolved, while reporting a counterexample to the implication when infinite magmas are allowed. The paper also tentatively conjectures that a finite counterexample exists. This mission makes the affirmative implication its formal target and also accepts a rigorous refutation of the complete finite statement.

This mission treats the universal target as open. Supporting structural facts and conditional reductions are separately identified, so that progress on one does not assert completion of the target.

Setting

A magma here is a type $\alpha$ with a total binary operation $\diamond:\alpha\times\alpha\to\alpha$. Parentheses specify the order of evaluation throughout; no reassociation is permitted. The condition E677 means

$$\forall x,y\in\alpha,\quad x=y\diamond\bigl(x\diamond((y\diamond x)\diamond y)\bigr).$$

The condition E255 means

$$\forall x\in\alpha,\quad x=((x\diamond x)\diamond x)\diamond x.$$

These are the two laws used in Chapter 13 of the project blueprint. For a fixed element $y$, the left translation (left multiplication) map is $L_y(x)=y\diamond x$. A fixer of $x$ is an element $y$ with $y\diamond x=x$; it acts on $x$ from the left. This definition concerns one element $x$; it does not require $y$ to act as an identity on every element. The left orbit of $x$ is the forward orbit $x,L_x(x),L_x^2(x),\ldots$ of $x$ under its own left translation.

Formalization targets

The supporting targets expose the relevant distinction between a constraint on a possible fixer and the existence of a fixer. For every finite $\alpha$ satisfying E677, the first supporting statement is

$$\forall y\in\alpha,\quad L_y\text{ is bijective}.$$

The second supporting statement determines any fixer:

$$\forall x,y\in\alpha,\quad y\diamond x=x\ \Longrightarrow\ y=(x\diamond x)\diamond x.$$

The third supporting statement is the backward recurrence

$$\forall x,y\in\alpha,\quad x=(y\diamond x)\diamond\bigl((y\diamond(y\diamond x))\diamond y\bigr).$$

These three statements are blueprint Lemma 13.1(i)–(iii) and are Proved on this platform. The following fixer-existence assertion is the same obligation as E255 under E677 and finiteness (blueprint Lemma 13.2); it is a reduction node, not a milestone:

$$\forall x\in\alpha,\quad\exists y\in\alpha,\quad y\diamond x=x.$$

The mission goal is

$$\forall\text{ finite magmas }\alpha,\quad \operatorname{E677}(\alpha)\ \Longrightarrow\ \operatorname{E255}(\alpha).$$

For finite E677 magmas, E255 at $x$ supplies the fixer $(x\diamond x)\diamond x$; from any fixer $y$ of $x$, Lemma 13.1(ii) gives $y=(x\diamond x)\diamond x$ and hence E255 at $x$. Each direction is one line, so fixer existence is not a strictly weaker milestone.

Three open sub-goals come from the case split in the accepted reduction sketches for the fixer-existence node. Sub-goal 1 is orbit-local: for a fixed $x$, if two elements of the left orbit of $x$ have equal right products by $x$, then they are equal or $x$ has a fixer. Sub-goal 2 concerns the case of exactly one element $A$ outside the left orbit of $x$, with $x$ having no fixer: a right-translation collision $c\diamond x=A\diamond x$ between an orbit point $c$ and $A$ must propagate to the orbit successor $x\diamond c$. Sub-goal 3 assumes $x\diamond x\ne x$ and at least two elements outside the left orbit: if right translation by $x$ sends an orbit point outside the orbit, then $x$ has a fixer. Sub-goal 3 is not a smaller case of the goal. If it holds for every finite E677 magma, the mission goal follows by a product construction (milestone "Sub-goal 3 support (a)"), and the mission goal gives Sub-goal 3 because E255 at $x$ supplies the fixer $(x\diamond x)\diamond x$. So a proof of Sub-goal 3 alone proves the goal, and a route through Sub-goals 1 and 2 still needs Sub-goal 3. The D4 milestones specialize Sub-goal 1 to a left orbit of exact period four; D4.0, D4.1, D4.2 and D4.4a–e are Proved, and the series is open at D4.3 and its five branch closeouts D4.3a–e. One conditional result (E677 together with conjugacy-closed left translations implies E255; Padilla, 2026) is Proved on this platform. The milestone "Alternative resolution — a finite E677 counterexample to E255" (theorem finite_counterexample) is the disproof target. The sixteen milestones "Counterexample structure (a)–(p)" are constraints on a counterexample and rules for a counterexample search, all Proved; (h)–(j) take small-order facts as hypotheses, and the milestones "Small orders (4)" and "Small orders (7)" prove two of them. None of the sixteen is a disproof. None of the displayed statements restricts the cardinality to a tested range.

In the authors' repository, Sub-goal 1 is called Piece 1, the unique-outsider case containing Sub-goal 2 is called Gap 1, and the case of Sub-goal 3 is called Gap ≥ 2; those names appear in some theorem sources and file names.

Significance

A resolution determines whether this particular law gains E255 as a consequence upon restriction to finite carriers. An affirmative proof must cover every finite cardinality, every operation on each carrier, and every assignment of the universally quantified elements. A finite counterexample must supply an operation that satisfies every instance of E677 while failing E255 at some element.

The formal package provides small, reusable statements of the two laws, the left translation property, and the fixer constraint. Keeping these statements separate allows their precise hypotheses and conclusions to be checked individually. In particular, the second supporting result says what a fixer must be when one exists; the fixer-existence formulation records the additional mathematical content needed to ensure existence.

Difficulty

The left translation conclusion concerns maps with the left input fixed. The fixer-existence formulation instead asks about the image of the map $y\mapsto y\diamond x$, with its right input fixed. No assumption in the formal goal makes these two maps interchangeable. Bijectivity of every left translation map alone does not state that a fixer exists.

Because the implication fails for infinite magmas, E255 is not an equational consequence of E677, so any proof must use finiteness in an essential way. The blueprint's linear and linear-extension constructions cannot produce a finite counterexample (blueprint Lemmas 13.3 and 13.4); community members have formalized on this platform the scalar-coefficient case of the linear lemma, the Type I and Type II affine families, and the linear-extension lemma (see the discussion thread).

Likewise, checking a collection of finite operation tables does not quantify over arbitrary finite cardinalities. Such computation does not discharge the goal submitted here. Any proof must justify every use of finiteness and retain the displayed parenthesization of the laws.

Formalization scope

The representation uses an arbitrary universe-polymorphic type, an explicit binary operation, and a Fintype instance for finite targets. Passing the operation explicitly avoids importing a separate magma package or imposing algebraic typeclass laws. The predicates E677 and E255 themselves do not assume finiteness; each theorem states its own finite-carrier hypothesis.

Empty carriers are included. Both laws hold vacuously on them; the pointwise fixer statement is also vacuous because there is no element $x$. Consequently an empty carrier cannot refute the main goal. Nonempty carriers of every finite size are included without further assumptions. There is no associativity, commutativity, idempotence, identity element, or cancellation hypothesis hidden in the representation.

The definition bundle FiniteMagmaE677 provides E677, E255, HasFixerAt (existence of a fixer of $x$), InLeftOrbit (membership in the left orbit of $x$) and OrbitRightCollisionOrFixer. Three further bundles, FiniteMagmaE677_seventh_element_growth, FiniteMagmaE677_d4_first_return and FiniteMagmaE677_sswap_renewal, hold the period-four packet types used by the D4 milestones.

Status (2026-10-27 UTC). Proved on this platform: Lemma 13.1(i)–(iii), the Sub-goal 1, Sub-goal 2 and Sub-goal 3 support lemmas, D4.0, D4.1, D4.2, D4.4a–e, the conditional conjugacy-closure theorem, Counterexample structure (a)–(p), Small orders (4) and (7), and three further conditional theorems by omegaestable (existential row transport, parametrized row transport, left-parameter transport; see the discussion thread). Open: Sub-goals 1–3, D4.3 with D4.3a–e, and the counterexample target. Community members have also formalized the blueprint's 496-element non-right-cancellative E677 magma (see the discussion thread).

Welcome contributions: a proof of any open sub-goal or D4.3 branch (a proof of Sub-goal 3 proves the goal; see the milestone "Sub-goal 3 support (a)"); a proof sketch that reduces an open leaf to new lemmas; a concrete operation table on Fin n proving finite_counterexample, which would make the main theorem false.

Results in the captain's private repository that are not on this platform

Results that are Proved on this platform are not repeated here. Readers cannot open the captain's private repository, so each statement is given in full. PROVEN means a complete proof, in the form stated. BOUNDED means a SAT-solver result for one encoded finite structure: each UNSAT result used here has a DRAT proof that drat-trim accepted (unverified C code, not a kernel-checked proof). EMPIRICAL means a computation over finite data, with no certificate.

Not ported

A port of these results to this platform is a long job.

1. Finite facts for Counterexample structure (h) and (j), and $|M|=35$ or $|M|\ge 40$. PROVEN (Lean; axioms propext, Classical.choice, Quot.sound). No E677 magma has order 6; every E677 magma of order 8 has an idempotent; every E677 magma of order 9 that satisfies E255 has an idempotent. Each proof is a case split on the cells of the table with a relabelling rule, made by the captain's own generator (3,724, 45,338 and 16,809 nodes; 2.97 MB, 6.0 MB and 1.8 MB of Lean). With Small orders (4) and (7), the facts for orders 6 and 8 remove, in the repository, the last finite hypotheses of (h). (j) takes the order-9 fact without E255, which has no Lean proof. Let $M$ be a minimum counterexample, $z$ a point where E255 fails, $q(z)=((z\diamond z)\diamond z)\diamond z$, and $\theta$ a non-universal congruence that relates $z$ and $q(z)$. Since $q(z)\ne z$, $M/\theta$ has fewer elements than $M$, and it satisfies E677, so it satisfies E255; so the order-9 fact with E255 is enough: $|M|=35$ or $|M|\ge 40$, with no finite hypothesis. Earlier sources for these facts: Counterexample structure (h) and (j). Source: the captain's private repository, revision a21faf52, lean/E677/SmallOrderSix.lean, lean/E677/SmallOrderEight.lean, lean/E677/FiniteCertificates/OrderEightIdem/, lean/E677/SmallOrderE255.lean, lean/E677/SmallOrderNine255.lean, lean/E677/FiniteCertificates/OrderNineIdem255/ and lean/E677/SmallOrderBounds255.lean.

2. Period-four refinements of D4.2. PROVEN (Lean; axioms propext, Classical.choice, Quot.sound). A repository theorem refines the five branches of the D4.2 first-return packet and keeps every case. Write $q=c_2\diamond x$. In the R-through-one branch (the repository's name), each outcome is a fixer of $x$, a strict decrease of a finite contact budget, a new $L_x$-cycle disjoint from the elements already accounted for (with its exact size), or a closed trace of $L_q^{-1}$ that is reduced to two phase-contact families. In the two unswapped S branches, each outcome is a fixer of $x$, a decrease by one of the number of unmarked phases on the $L_x$-cycle of $q$, or a new disjoint $L_x$-cycle with its exact size. These results do not close D4.3 or any of D4.3a–e, because the outcomes are not yet combined into one state with a strictly decreasing well-founded measure. A port needs the repository's library of period-four packets. Source: the captain's private repository, revision 4100763b, lean/E677/Spine/Piece1D4RefinedFirstReturn.lean, e677_d4_q_refinedFirstReturnPacket_of_firstReturnPacket.

Not formalized

These results have only solver or computation evidence, and no Lean proof, and no milestone on this platform uses them as hypotheses.

3. A counterexample has at least 11 elements. BOUNDED. Every E677 magma with at most 10 elements satisfies E255. No E677 magma has order 2, 3, 4, 6 or 8: order 4 is Small orders (4), order 6 is in item 1, and orders 2, 3 and 8 are BOUNDED (earlier sources in Counterexample structure (h)). Every E677 magma of order 5, 7 or 9 is right-cancellative; then each right translation $y\mapsto y\diamond x$ is a bijection, so $x$ has a fixer, and Lemma 13.1(ii) gives E255 at $x$. At order 10, a point $x$ at which E255 fails has no fixer, so $x$ is not in its own column $\{y\diamond x\}$; a search for such a table, split into 67 cases by the cycle type of $L_x$ (the length $l\ge 2$ of the left orbit of $x$, and the cycle lengths of $L_x$ on the other $10-l$ elements), is UNSAT in each case. Earlier reports: the sources listed in Counterexample structure (h)–(j) for the E677 magmas of orders 2–4 and 6–9, among them a Lean proof for order 6 by J. Hyun. Without certificates (ETP Zulip thread "FINITE: 677 -> 255"): J. Brox (Mace4) reports no counterexample of order 9 (2024-12-10), none of order at most 10 (2025-01-10), no E677 magma of order 10 (2025-01-12) and no counterexample of order 11 (2025-03-12); B. Le Floch (2024-12-22, Mace4) reports none of order at most 9; J. Hyun (2025-01-09, CaDiCaL) none of order 5 to 8; S. Chuks-Onah (2026-05-01, Z3) none of order 5 or 6, and (2026-05-16, SAT) none of order 5 or 7; R. Schneider (2026-05-15, own search program) and B. Subercaseaux (2026-05-15, SAT) none of order at most 11. S. Chuks-Onah (2026-06-20, CaDiCaL) also reports that E677 with a failure of E255 is UNSAT at orders 7 and 8, with DRAT lemma counts for orders 5 to 7 and no stated proof check. The new content here is DRAT certificates that drat-trim accepted, for every order up to 10. Source: the captain's private repository, revision dd2ee3e5, experiments/analysis/rc-small-orders-2026-10-19/ and experiments/analysis/rc-cubes-2026-10-19/; for orders 2, 3 and 8, experiments/analysis/idempotent-free-small-orders-2026-10-21/ and experiments/analysis/ti-groups-2026-10-19/ (section "Order 8 and 10 check").

4. Order 35 is excluded and the order is at least 45, for a minimum counterexample with a non-universal congruence that relates $z$ and $q(z)$. EMPIRICAL (exhaustive searches with the captain's own programs, no certificate, no Lean; order 35: two independent audits; the facts for orders 10–12: one independent audit, which for order 12 reproduced all but 4 of 22,644 subtrees; the order-7 census: no separate audit). Let $M$, $z$, $q(z)$ and $\theta$ be as in item 1. If $|M|=35$, Counterexample structure (i) and Small orders (7) give that $M/\theta$ has 7 elements and an idempotent and that the classes have 5 elements; then $M/\theta$ is isomorphic to $x\diamond y=4x+3y$ or to $x\diamond y=4x+y$ on $\mathbb{F}_7$ (J. Brox, ETP Zulip thread "FINITE: 677 -> 255", 2025-03-26; the captain's own census of order 7 agrees). Result: no finite E677 magma with a congruence onto one of these two magmas with 5-element classes fails E255. T. Tao (same thread, 2024-12-13) proposed the extensions $(x,s)\diamond(y,t)=(4x+3y,\ s\diamond_{x,y}t)$; the result covers them. So $|M|\ne 35$, and with item 1, $|M|\ge 40$. The class of an idempotent of $M/\theta$ is an E677 magma, so by item 1 the classes do not have 6 elements; the order-8 fact of item 3 gives $|M/\theta|\ne 8$, which excludes $|M|=40=8\cdot 5$. With two more facts (every E677 magma of order 10 has an idempotent; every E677 magma of order 11 that satisfies E255 has an idempotent), an $M/\theta$ without an idempotent has at least 12 elements. So $|M|\ge 45$. Two further facts exclude $|M|=48$ ($|M/\theta|=12$, classes of 4) and $|M|=50$ ($|M/\theta|=10$, classes of 5): every E677 magma of order 12 that satisfies E255 has an idempotent, and no E677 magma of order 10 satisfies E255. So up to order 50, only $|M|=45$ ($9\cdot 5$) and $|M|=49$ ($7\cdot 7$) remain. At order 45, $M/\theta$ is isomorphic to $x\diamond y=x+\beta y$ on $\mathbb{F}_9=\mathbb{F}_3(i)$, $i^2=-1$, $\beta=2+i$ (the only E677 magma of order 9: J. Brox, same thread, 2025-01-10; the captain's own census agrees), and the classes have 5 elements; this case is open. J. Brox reported that no E677 magma has order 10 (item 3), which is stronger than the order-10 facts above. Source: the captain's private repository, revision a21faf52, docs/current/e677-coverage-matrix-2026-10-19.md (the row "Proper μ, any" that begins "|B| ≥ 35", and the rows "Proper μ, |B| = 35" and "Proper μ, |B| = 45"), experiments/analysis/order35-q1-orbits23-2026-10-27/, experiments/analysis/order35-orbits023-2026-10-27/, experiments/analysis/order10-idempotent-2026-10-27/ and experiments/analysis/order45-q9-2026-10-27/.

5. Extensions and row changes of the order-31 magma $x\diamond y=5x-4y+1$ on $\mathbb{F}_{31}$. Call it $Q_{31}$. It has no idempotent, and it is the smallest known E677 magma without an idempotent; every known E677 magma without an idempotent has order divisible by 31 (EMPIRICAL). So $Q_{31}$ is the smallest known candidate quotient in Counterexample structure (j). BOUNDED results:

• No E677 magma has a congruence with quotient $Q_{31}$ and classes of 2 or 3 elements.
• No E677 magma with a congruence with quotient $Q_{31}$ and classes of 4 elements fails E255.
• In the family $(u,s)\diamond(w,t)=(5u-4w+1,\ s+h_{w-u}(t-s))$ on $\mathbb{F}_{31}\times\mathbb{F}_5$, with permutations $h_d$ of $\mathbb{F}_5$, no E677 member fails E255.
• An E677 operation on $\mathbb{F}_{31}$ that fails E255 differs from $Q_{31}$ in at least 20 rows and at least 40 cells.

B. Le Floch (ETP Zulip thread "FINITE: 677 -> 255", 2024-12-13) found $5x-4y+c$ mod 31 as the one linear E677 model in which $c$ cannot be removed, and R. Schneider (same thread, 2025-11-21) noted that $Q_{31}$ has no idempotent. T. Tao (same thread, 2024-12-13) proposed the extensions $(x,s)\diamond(y,t)=(x\diamond y,\ s\diamond_{y-x}t)$ of $Q_{31}$. B. Reinke (same thread, 2025-11-07) encoded them for z3 and wrote that he thought he could exclude classes of fewer than 4 elements (no certificate). The first result above covers all extensions with classes of 2 or 3 elements, not only these; the third result is the case of Tao's extensions with fibre operations $s+h(t-s)$. Source: the captain's private repository, revision dd2ee3e5, experiments/analysis/gap2-monolith-m3-2026-10-17/ (§2, §6), experiments/analysis/pro-counterexample-audit-2026-10-20/ (cyclic-section-19375/, construction-19350/) and experiments/analysis/idempotent-free-2026-10-19/.

6. Tables with an automorphism of prime order, orders 12–21. BOUNDED, incomplete. Let $\alpha$ be an automorphism of prime order $p$ of an E677 magma of order $n$, $12\le n\le 21$, with $f$ fixed points, and let $z$ be a point with no fixer. The fixed points of $\alpha$ form a submagma, so an E677 magma of order $f$; by item 3, $f\notin\{2,3,4,6,8\}$. The search covers $f\in\{0,1,5,7,9,11\}$. If $\alpha$ fixes $z$, the fixed points form an E677 magma of order $f$ that fails E255 at $z$; this is excluded for $f\le 9$ by item 3, and for $f=11$ 4 shapes $(n,p,f)$ are UNSAT and 7 were not run. If $z$ is in a cycle of $\alpha$, 26 shapes are UNSAT (all 9 shapes with $p\ge 11$, and 17 shapes with $p\le 7$); 14 shapes are UNKNOWN after 3600 s, and 40 were not run. Not covered: the shapes with $f=0$ and one cycle ($n=p\in\{13,17,19\}$, translation-invariant tables on $\mathbb{Z}_n$), fixed-point count 10, and fixed-point counts of at least 12. Earlier searches without certificates (ETP Zulip thread "FINITE: 677 -> 255"): R. Schneider (2025-11-20 and 2025-11-21) searched the tables with the automorphism $(0)(1\,2\,\dots\,n-1)$ up to $n=31$ and found only right-cancellative ones (the shapes with $f=1$ and one cycle); B. Reinke (2025-11-21) noted that the fixed points form a submagma and found no table with one cycle and 5 fixed points of order at most 25 other than order 5 (the shapes with $f=5$ and one cycle), and (2025-11-26) noted that in a minimum counterexample only the identity automorphism fixes the failing point. Source: the captain's private repository, revision dd2ee3e5, experiments/analysis/symmetric-simple-2026-10-20/.

7. A refuted intermediate statement. EMPIRICAL (exhaustive check of one explicit table, run twice with independent encodings; not kernel-checked). Let $S(x)$ be the closure of the left orbit of $x$ under $z\mapsto z\diamond x$. The repository's gate CP asserted: in a finite E677 magma, if the hypotheses of Sub-goal 3 hold at $x$ and $z\mapsto z\diamond x$ is not injective on $S(x)$, then the left orbit of $x$ has minimal period $7$. Let $K$ be the 7-element E677 magma of Sub-goal 3 support (a) (file db/7/1 of the public collection memoryleak47/eq677), and let $M$ be the E677 magma of order $77$ in file db/77/65 of the same collection. In $M\times K$ (order $539$; E677 checked on all $539^2$ pairs), the point $(0,0)$ satisfies these hypotheses, and its left orbit has minimal period $\operatorname{lcm}(7,6)=42$. The point $(0,0)$ has the fixer $(76,4)$, so this is not a counterexample to E255, and it refutes CP only in the form without a no-fixer hypothesis. Source: the captain's private repository, revision 4100763b, docs/current/dead-ends/gap-ge-2.md, entry D7-6.

8. $\Phi(x)=(x\diamond x)\diamond x$ is not injective in general. EMPIRICAL. In the 2026-09-27 snapshot of the community database (4091 tables), every table satisfies E255, and $\Phi$ is not injective in 1107 of them; the smallest such order is $7$. In one table of order 7, row 6 is the identity row, so $6$ is a fixer of every $x$ and Lemma 13.1(ii) gives $\Phi(x)=6$ for every $x$. So global injectivity of $\Phi$ is not a usable intermediate target. Source: the captain's private repository, revision 4100763b, docs/professor-phi-injectivity.md, correction of 2026-10-14.

Selected references

• Matthew Bolan et al., The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale, arXiv:2512.07087v2 (December 16, 2025), paper.
• The Equational Theories Project contributors, Equational Theories, online proof blueprint, Chapter 13, equations (1)–(2) and Lemmas 13.1–13.4, chapter, accessed September 7, 2026 and October 13, 2026.
• J. I. Padilla (GitHub: omegaestable), Prove E677 implies E255 under left translation conjugacy closure, Equational Theories Project pull request #1518, 2026 (closed without merge by its author on 2026-10-13; the theorem is Proved on this platform), pull request.
• Lean Zulip, channel "Equational", thread "FINITE: 677 -> 255", thread.