An orbit right-collision forces a fixer

Open

FiniteMagmaE677.orbit_right_collision_or_fixer

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

e255e677equational-theoriesfinite-magma

Open structural subproblem (Piece 1). Let $A$ be finite with arbitrary operation $\diamond$ satisfying E677, and fix $x\in A$ . If two elements $a,b$ in the forward orbit $x,L_x(x),L_x^2(x),\ldots$ satisfy $a\diamond x=b\diamond x$ , then either $a=b$ or there is a fixer $y\diamond x=x$ . This is an orbit-local collision principle; it does not assert fixer existence for every $x$ .

Preamble

import Definitions.Def_FiniteMagmaE677

universe u

Formal statement

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

Source

Mission-defined structural subproblem; public E677/E255 definitions and background: 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

For every universe- $u$ type $\alpha$ equipped with a Fintype instance, every binary operation $\operatorname{op}:\alpha\to\alpha\to\alpha$ , every proof $h:E677(\operatorname{op})$ , and every $x:\alpha$ , $\operatorname{OrbitRightCollisionOrFixer}(\operatorname{op},x)$ holds. Thus, for any two left-orbit elements of $x$ with equal right products by $x$ , either they are equal or $x$ has a fixer. For an empty finite type, there is no possible $x$ , so the theorem's outer assertion is vacuous.

View graph