Right-translation escape with one element outside the left orbit gives a fixer

Open

FiniteMagmaE677.unique_left_orbit_complement_escape_gives_fixer

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

e255e677equational-theoriesfinite-magmaorbit

For an element $x$ , let $O_x=\{L_x^n(x):n\ge 0\}$ be its orbit under the left translation $L_x(z)=x\diamond z$ . Assume E677, assume $x\diamond x\ne x$ , and assume exactly one element $A$ lies outside $O_x$ . If right translation by $x$ sends some element of $O_x$ outside $O_x$ , prove that $x$ has a fixer: there is a $y$ such that $y\diamond x=x$ . No associativity, commutativity, or identity is assumed.

Preamble

import Definitions.Def_FiniteMagmaE677

universe u

Formal statement

theorem FiniteMagmaE677.unique_left_orbit_complement_escape_gives_fixer
    {α : Type u} [Fintype α] (op : α → α → α) (h : FiniteMagmaE677.E677 op)
    (x A : α) (hni : op x x ≠ x)
    (hA_notin : ¬ FiniteMagmaE677.InLeftOrbit op x A)
    (hA_unique : ∀ a : α, ¬ FiniteMagmaE677.InLeftOrbit op x a → a = A)
    (hescape : ∃ a : α,
      FiniteMagmaE677.InLeftOrbit op x a ∧
        ¬ FiniteMagmaE677.InLeftOrbit op x (op a x)) :
    FiniteMagmaE677.HasFixerAt op x := by sorry

Source

Semantic branch target from the finite E677 to E255 formalization: Adam McKenna, The Missing Pair (private repository), revision 4100763b, lean/E677/Spine/Gap1OutsiderCollision.lean, e677_fixer_gap1_of_unique_outsider_right_dip (the repository theorem has no hypothesis x ◇ x ≠ x; this statement adds it). Until 2026-09-29 the branch theorem was e677_fixer_gap1_of_orbit_right_dip in lean/E677/Spine/Gap1Closeout.lean, which is now off the repository's proof spine. Equational Theories Project blueprint, Chapter 13; Bolan et al., arXiv:2512.07087v2, Section 8, Problem 8.1.

View graph