One Branch in the
Equational Theories Project

Equation 677 looks like it was generated by a random process: a = b ◇ (a ◇ ((b ◇ a) ◇ b)). Seventeen characters, one operation, and 34 mathematicians spent 2025 mapping out what it implies.

That paper is the Equational Theories Project (arXiv:2512.07087). It asks, for each pair of the 4694 equations in its scope, whether one implies the other. Automated provers handle most of the landscape. I've been working in one small corner of it.

A magma is a set with a binary operation and nothing else. No commutativity, no associativity, no identity element, just a rule for combining any two elements into a third. An E677 magma is one where a = b ◇ (a ◇ ((b ◇ a) ◇ b)) holds for every pair a, b.

The ETP asks: what else must an E677 magma satisfy? What structure does that identity force?

One approach is to study the left-multiplication map. Fix an element x. Define L_x(z) = x ◇ z. In a finite magma, applying L_x repeatedly starting from x must eventually cycle. The length of that cycle (the orbit depth) is a structural property of x.

The d=6 case is elements where L_x, starting from x, cycles through exactly six distinct values before returning. You get x, c1, c2, c3, c4, c5, and then x again.

Most of my work has been in the d=6 gap-1 regime, a further structural condition on how elements outside the 6-cycle interact with the orbit under the E677 constraint.

The gap-1 classifier I've been building in Lean 4 enumerates all the cases that come up. Fix an outsider element A, one not in {x, c1, c2, c3, c4, c5}. The classifier walks through every possible behavior for A relative to the orbit.

The exact-base branch is the case where three rows hold on A:

• A ◇ A = c1 (A composed with itself lands at the first non-trivial orbit element)
• A ◇ x = c3 (A composed with x lands at the exact midpoint of the 6-cycle)
• c3 ◇ c3 = c1 (the classifier shows this is forced by the first two, but the proof packages it explicitly)

The name comes from A ◇ x landing at c3, which sits exactly halfway around the orbit. Three rows. Minimal. That's the packet.

Under the d=6 context plus those three rows, the proof establishes: c4 ◇ x = x.

That translates to: ((x ◇ x) ◇ x) ◇ x = x. The fourth left-iterate of x under L_x returns to x. In terms of the orbit: the arrow from c4 points directly back to x, not forward to c5.

Without them, c4 might point anywhere the E677 law allows. The hypotheses close the gap.

The proof goes through three lemmas, each one picking specific values for a and b in the E677 identity, recognizing a previously established fact in the nesting, and closing with left cancellation.

Lemma 1: c3 ◇ c1 = x. From A ◇ x = c3 and the gap-1 row A ◇ (A ◇ x) = A, we get A ◇ c3 = A. Apply E677 with b = A, a = c3: the nesting gives (A ◇ c3) ◇ A = A ◇ A = c1, so c3 = A ◇ (c3 ◇ c1). Since A ◇ x = c3 also holds, left cancellation by A gives c3 ◇ c1 = x.

Lemma 2: c1 ◇ c4 = c3. Apply E677 with b = c3, a = c1. By Lemma 1, c3 ◇ c1 = x, so x ◇ c3 = c4 by the orbit definition. This gives c1 = c3 ◇ (c1 ◇ c4). Since c3 ◇ c3 = c1, left cancellation gives c1 ◇ c4 = c3.

Lemma 3: c4 ◇ x = x. Apply E677 with b = c1, a = c4. By Lemmas 1 and 2, the nesting simplifies to c4 = c1 ◇ (c4 ◇ x). The orbit gives c1 ◇ x = c4. Left cancellation by c1 gives c4 ◇ x = x.

The proof lives in D6ExactBasePacket.fixer in lean/E677/D6Publication.lean. The structure packages the three rows alongside the d=6 context:

structure D6ExactBasePacket (alpha : Type u) [Magma' alpha] [Fintype alpha] where
  ctx : D6Gap1Context alpha
  hAA : ctx.A * ctx.A = ctx.c1
  hA0 : ctx.A * ctx.x = ctx.c3
  hT1 : ctx.c3 * ctx.c3 = ctx.c1

Running lean_verify on D6ExactBasePacket.fixer returns the axiom footprint: {propext, Classical.choice, Quot.sound}. Those are the standard Lean axioms, present in every Lean proof. The theorem doesn't depend on any sorry.

That matters because the larger gap-1 classifier still has sorry declarations in branches I haven't finished. Isolating this result in its own import chain (D6Publication → D6Isolated → D6CoreMinimal → Basic, with no gap-1 dispatcher) means it can be verified independently.