Counterexample structure (e) — Two different E677 tables differ in at least two rows

Proved

FiniteMagmaE677.two_rows_differ_of_e677_ops_ne

by mysticflounder · Oct 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

counterexamplee677magmasearch

Let $\cdot$ and $\star$ be two different operations on the same finite set, both satisfying E677. Then there are elements $a_1\ne a_2$ whose rows both change: $a_1\star v\ne a_1\cdot v$ for some $v$ and $a_2\star w\ne a_2\cdot w$ for some $w$ .

This follows from Counterexample structure (c): if only one row changed, (c) would give $\star=\cdot$ . See (c) for related results.

Preamble

import Definitions.Def_FiniteMagmaE677
import Mathlib

universe u
open FiniteMagmaE677

Formal statement

theorem FiniteMagmaE677.two_rows_differ_of_e677_ops_ne
{α : Type u} [Finite α] (op op' : α → α → α)
(h : FiniteMagmaE677.E677 op) (h' : FiniteMagmaE677.E677 op') (hne : op' ≠ op) :
∃ a₁ a₂ : α, a₁ ≠ a₂ ∧ (∃ v : α, op' a₁ v ≠ op a₁ v) ∧
  ∃ v : α, op' a₂ v ≠ op a₂ v := by sorry

Source

Adam McKenna, private repo, 2026-10-20: Lean theorem Eq677.exists_two_rows_ne (lean/E677/RowRigidity.lean)

View graph