Fixer existence: an equivalent form of the main target

Open

FiniteMagmaE677.fixer_exists

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

e255e677equational-theoriesfinite-magma

Fixer-existence form of the main target. Let $\alpha$ be a finite type with an arbitrary total operation $\diamond$ satisfying E677. The assertion is

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

For finite E677 magmas this is the same obligation as E255 (blueprint Lemma 13.2): E255 at $x$ supplies the fixer $(x\diamond x)\diamond x$ , and from any fixer $y$ of $x$ the fixer-determination theorem gives $y=(x\diamond x)\diamond x$ , hence E255 at $x$ . It is retained as an explicit reduction dependency, not as a smaller milestone.

Preamble

import Definitions.Def_FiniteMagmaE677

universe u

Formal statement

theorem FiniteMagmaE677.fixer_exists {α : Type u} [Fintype α] (op : α → α → α)
    (h : FiniteMagmaE677.E677 op) (x : α) : ∃ y : α, op y x = x := by sorry

Source

Matthew Bolan et al., The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale, arXiv:2512.07087v2 (December 16, 2025), Section 8, Problem 8.1, https://arxiv.org/html/2512.07087v2

Read-back

What the Lean code literally says, in plain math · gpt-5.6-luna

For every universe u, finite possibly empty type $\alpha:\mathrm{Type}\,u$ , arbitrary operation $\operatorname{op}:\alpha\to\alpha\to\alpha$ , and hypothesis h saying that every $a,b\in\alpha$ satisfy $a=\operatorname{op}\bigl(b,\operatorname{op}(a,\operatorname{op}(\operatorname{op}(b,a),b))\bigr)$ , every $x\in\alpha$ has at least one $y\in\alpha$ such that $\operatorname{op}(y,x)=x$ ; the statement asserts existence only, and if $\alpha$ is empty its universal quantification over x is vacuous.

Human review

Endorsed by Shuze Chen · Sep 10, 2026
Endorsed by mysticflounder · Sep 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph