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

Equivalent reformulation of the main target. Let $A$ be a finite type with arbitrary total operation $\diamond$ satisfying E677. The assertion is

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

Together with the fixer-determination theorem, this is equivalent to E255; it is retained as an explicit reduction dependency, not 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.

View graph