Bernhard Reinke writes:

I think I have a sketch for an example of a magma satisfying 206 but not 1648. I use the translation invariant approach, but for a non-commutative group: let $$ G $$ the free product of three cyclic groups of order 2. If we have the alphabet $$ A = \{a,b,c\} $$ then we can identify $$ G $$ with the reduced words in $$ A $$ that have no subwords of the form $$ aa, bb, cc $$.

Our magma will be defined on G and will satisfy

x ◇ y = x f(x^{-1}y)

where $$ f \colon G \rightarrow \{1, a, b, c\} $$.

Then the RHS of 206 is

(x ◇ (x ◇ y)) ◇ y = (x ◇ (x f(x^{-1}y)) ◇ y = (x f(f(x^{-1} y))) ◇ y = x  f(f(x^{-1} y)) f( (f(f(x^{-1} y))^{-1} x^{-1} y)

Setting $$ z = x^{-1} y $$, we get that 206 is equivalent to $$ f(f(z)) f ( f(f(z))^{-1} z) = 1 $$. Under the assumption that $$f$$ maps to $$\{1, a, b, c\}$$ (so $$ f(z) = f(z)^{-1} $$), this simplifies to

f(f(z)) = f( f(f(z)) z)

I claim the following f satisfies this: we set

f(1) = 1, f(a) = b, f(b) = c, f(c) = a

now, if $$w$$ is a nonempty reduced word not starting in $$a$$, we set $$ f(aw) = a $$, cyclically symmetric for reduced words starting in b and and c. Let us check that this satisfies $$f(f(z)) = f( f(f(z)) z)$$:

It is clear that $$ f(f(1)) = f( f(f(1)) 1) = 1 $$.

We have $$ f(f(a)) = f(b) = c$$, and $$f(f(f(a))a) = f(ca) = c$$.

For $$w$$ is a nonempty reduced word not starting in $$a$$, we have $$ f(f(aw)) = f(a) = b, so f( f(f(aw)) aw) = f(baw) = b$$. The rest follows by symmetry.

I think 1648 translates to $$ f(z)f(f((f(z))^{-1} z)) = 1 $$ this is not satisfied, as $$ f(a) f(f( (f(a))^{-1} a) = b f(f(ba)) = b f(b) = bc \not= 1 $$.

I hope I haven't made any computational mistakes (this is in fact my second try, :sweat_smile: ), would someone like to check whether this makes sense? I don't think I would be able to formalize this in Lean myself.

Implementation notes

This contains a self-contained development of the free product of three copies of the two-element group, by defining reduced words, a reduction function, and deriving enough API for it. In the end we define our magma of interest directly, so this free product group is not explicitly defined.

The development can easily be generalized to more than three copies if needed, just swap out Fin 3.

@[reducible, inline]

abbrev ThreeC2.W : Type

Free words over three generators

Equations

• ThreeC2.W = List (Fin 3)

def ThreeC2.IsRed (w : ThreeC2.W) : Prop

Reduced words do not have the same element adjacent to each other

Equations

• ThreeC2.IsRed w = ∀ (i : ℕ) (h : i + 1 < List.length w), w[i] ≠ w[i + 1]

@[simp]

theorem ThreeC2.IsRed_nil : ThreeC2.IsRed []

@[simp]

theorem ThreeC2.IsRed_singleton (x : Fin 3) : ThreeC2.IsRed [x]

theorem ThreeC2.IsRed_reverse (w : ThreeC2.W) : ThreeC2.IsRed (List.reverse w) → ThreeC2.IsRed w

@[simp]

theorem ThreeC2.IsRed_reverse_iff (w : ThreeC2.W) : ThreeC2.IsRed (List.reverse w) ↔ ThreeC2.IsRed w

theorem ThreeC2.IsRed_uncons {x : Fin 3} {ys : List (Fin 3)} (h : ThreeC2.IsRed (x :: ys)) : ThreeC2.IsRed ys

theorem ThreeC2.IsRed_cons {y x : Fin 3} {ys : List (Fin 3)} (hne : y ≠ x) (h : ThreeC2.IsRed (x :: ys)) : ThreeC2.IsRed (y :: x :: ys)

theorem ThreeC2.IsRed_not_repeated {ys : List (Fin 3)} {x : Fin 3} {xs : List (Fin 3)} : ¬ThreeC2.IsRed (ys ++ x :: x :: xs)

The reduction function, nicely concrete and executable (for by decide later) and somewhat efficient (not that that matters).

def ThreeC2.red (w : ThreeC2.W) : ThreeC2.W

Equations

• ThreeC2.red w = ThreeC2.red.go [] w

def ThreeC2.red.go (ys xs : ThreeC2.W) : ThreeC2.W

Equations

• ThreeC2.red.go x [] = List.reverse x
• ThreeC2.red.go [] (x_2 :: xs) = ThreeC2.red.go [x_2] xs
• ThreeC2.red.go (y :: ys) (x_2 :: xs) = if x_2 = y then ThreeC2.red.go ys xs else ThreeC2.red.go (x_2 :: y :: ys) xs

def ThreeC2.red.go_aux (ys xs : ThreeC2.W) (h : ThreeC2.IsRed ys) : ThreeC2.W

Equations

• ThreeC2.red.go_aux x✝ [] x = List.reverse x✝
• ThreeC2.red.go_aux [] (x_3 :: xs) x_4 = ThreeC2.red.go_aux [x_3] xs ⋯
• ThreeC2.red.go_aux (y :: ys) (x_3 :: xs) h = if heq : x_3 = y then ThreeC2.red.go_aux ys xs ⋯ else ThreeC2.red.go_aux (x_3 :: y :: ys) xs ⋯

def ThreeC2.red.go_induct (motive : (x : ThreeC2.W) → ThreeC2.W → ThreeC2.IsRed x → Prop) (case1 : ∀ (ys : ThreeC2.W) (x : ThreeC2.IsRed ys), ThreeC2.IsRed ys → motive ys [] x) (case2 : ∀ (x : Fin 3) (xs : List (Fin 3)) (x_1 : ThreeC2.IsRed []), ThreeC2.IsRed [] → motive [x] xs ⋯ → motive [] (x :: xs) x_1) (case3 : ∀ (ys : List (Fin 3)) (x : Fin 3) (xs : List (Fin 3)) (h : ThreeC2.IsRed (x :: ys)), ThreeC2.IsRed (x :: ys) → motive ys xs ⋯ → motive (x :: ys) (x :: xs) h) (case4 : ∀ (y : Fin 3) (ys : List (Fin 3)) (x : Fin 3) (xs : List (Fin 3)) (h : ThreeC2.IsRed (y :: ys)) (h_1 : ¬x = y), ThreeC2.IsRed (y :: ys) → motive (x :: y :: ys) xs ⋯ → motive (y :: ys) (x :: xs) h) (ys xs : ThreeC2.W) (h : ThreeC2.IsRed ys) : motive ys xs h

Equations

• ThreeC2.red.go_induct = ThreeC2.red.go_aux.induct

@[simp]

theorem ThreeC2.red_nil : ThreeC2.red [] = []

@[simp]

theorem ThreeC2.red_singleton (x : Fin 3) : ThreeC2.red [x] = [x]

@[simp]

theorem ThreeC2.red_duoton_succ (x : Fin 3) : ThreeC2.red [x, x + 1] = [x, x + 1]

@[simp]

theorem ThreeC2.red_duoton_succ_succ (x : Fin 3) : ThreeC2.red [x + 1 + 1, x] = [x + 1 + 1, x]

@[simp]

theorem ThreeC2.red_IsRed (w : ThreeC2.W) : ThreeC2.IsRed (ThreeC2.red w)

theorem ThreeC2.red_IsRed.go (ys xs : ThreeC2.W) (h : ThreeC2.IsRed ys) : ThreeC2.IsRed (ThreeC2.red.go ys xs)

theorem ThreeC2.red_length_le (w : ThreeC2.W) : List.length (ThreeC2.red w) ≤ List.length w

theorem ThreeC2.red_length_le.go (w v : ThreeC2.W) : List.length (ThreeC2.red.go w v) ≤ List.length w + List.length v

theorem ThreeC2.red.go_length_le (ys xs : ThreeC2.W) : List.length ys ≤ List.length (ThreeC2.red.go ys xs) + List.length xs

@[simp]

theorem ThreeC2.red_eq_of_IsRed {w : ThreeC2.W} (h : ThreeC2.IsRed w) : ThreeC2.red w = w

theorem ThreeC2.red_eq_of_IsRed.go (ys : List (Fin 3)) (xs : ThreeC2.W) (h : ThreeC2.IsRed (ys.reverse ++ xs)) : ThreeC2.red.go ys xs = ys.reverse ++ xs

@[simp]

theorem ThreeC2.red_red (w : ThreeC2.W) : ThreeC2.red (ThreeC2.red w) = ThreeC2.red w

theorem ThreeC2.red_reduce {ys : List (Fin 3)} {x : Fin 3} {xs : List (Fin 3)} : ThreeC2.red (ys ++ x :: x :: xs) = ThreeC2.red (ys ++ xs)

We can reduce anywhere in a term. This is essentially a proof of confluence

theorem ThreeC2.red_reduce.go {x : Fin 3} {xs : List (Fin 3)} (zs ys : ThreeC2.W) (h : ThreeC2.IsRed zs) : ThreeC2.red.go zs (ys ++ x :: x :: xs) = ThreeC2.red.go zs (ys ++ xs)

@[simp]

theorem ThreeC2.rev_red (w : ThreeC2.W) : List.reverse (ThreeC2.red w) = ThreeC2.red (List.reverse w)

theorem ThreeC2.rev_red.go (ys xs : ThreeC2.W) (h : ThreeC2.IsRed ys) : List.reverse (ThreeC2.red.go ys xs) = ThreeC2.red (List.reverse xs ++ ys)

@[simp]

theorem ThreeC2.red_append_red_right (w v : ThreeC2.W) : ThreeC2.red (w ++ ThreeC2.red v) = ThreeC2.red (w ++ v)

theorem ThreeC2.red_append_red_right.go (w ys xs : ThreeC2.W) : ThreeC2.red (w ++ ThreeC2.red.go ys xs) = ThreeC2.red (w ++ List.reverse ys ++ xs)

@[simp]

theorem ThreeC2.red_append_red_left (w v : ThreeC2.W) : ThreeC2.red (ThreeC2.red w ++ v) = ThreeC2.red (w ++ v)

@[simp]

theorem ThreeC2.red_append_inv (w v : ThreeC2.W) : ThreeC2.red (List.reverse w ++ (w ++ v)) = ThreeC2.red v

@[simp]

theorem ThreeC2.red_rev_self (w : ThreeC2.W) : ThreeC2.red (List.reverse w ++ w) = []

@[simp]

theorem ThreeC2.red_append_inv_right (w v : ThreeC2.W) : ThreeC2.red (w ++ (List.reverse v ++ v)) = ThreeC2.red w

theorem ThreeC2.red_append_nil_iff_eq_inv (w v : ThreeC2.W) (hw : ThreeC2.IsRed w) (hv : ThreeC2.IsRed v) : ThreeC2.red (w ++ v) = [] ↔ w = List.reverse v

The crucial step towards cancellation.

theorem ThreeC2.red_append_nil_iff_eq_inv.go (v : ThreeC2.W) (hv : ThreeC2.IsRed v) (ys : List (Fin 3)) (xs : ThreeC2.W) (hxs : ThreeC2.IsRed (ys.reverse ++ xs)) : ThreeC2.red.go ys (xs ++ v) = [] → ys.reverse ++ xs = List.reverse v

theorem ThreeC2.red_append_nil_iff_eq_inv.go2 (ys xs : ThreeC2.W) (hxs : ThreeC2.IsRed xs) : ThreeC2.red.go ys xs = [] → ys = xs

theorem ThreeC2.red_append_nil_iff (w v : ThreeC2.W) : ThreeC2.red (w ++ v) = [] ↔ ThreeC2.red w = List.reverse (ThreeC2.red v)

theorem ThreeC2.red_eq_red_iff_red_append_nil (w v : ThreeC2.W) : ThreeC2.red w = ThreeC2.red v ↔ ThreeC2.red (List.reverse w ++ v) = []

@[simp]

theorem ThreeC2.red_append_inj (w v : ThreeC2.W) (h : ThreeC2.IsRed w) : w = ThreeC2.red (w ++ v) ↔ ThreeC2.red v = []

def ThreeC2.f : ThreeC2.W → ThreeC2.W

The f function that we use to define the monoid of interest

Equations

• ThreeC2.f [] = []
• ThreeC2.f [x_1] = [x_1 + 1]
• ThreeC2.f (x_1 :: head :: tail) = [x_1]

@[simp]

theorem ThreeC2.red_f (w : ThreeC2.W) : ThreeC2.red (ThreeC2.f w) = ThreeC2.f w

@[simp]

theorem ThreeC2.rev_f (w : ThreeC2.W) : List.reverse (ThreeC2.f w) = ThreeC2.f w

theorem ThreeC2.ff_fff (z : ThreeC2.W) (h : ThreeC2.IsRed z) : ThreeC2.f (ThreeC2.f z) = ThreeC2.f (ThreeC2.red (ThreeC2.f (ThreeC2.f z) ++ z))

The crucial relation of that function

@[reducible, inline]

abbrev ThreeC2.M : Type

The carrier for our magma: reduced words

Equations

• ThreeC2.M = { x : ThreeC2.W // ThreeC2.IsRed x }

instance ThreeC2.inst : Magma ThreeC2.M

The magma instance

Equations

• One or more equations did not get rendered due to their size.

theorem ThreeC2.M.Satisfies206 : Equation206 ThreeC2.M

theorem ThreeC2.M.Refutes1648 : ¬Equation1648 ThreeC2.M

theorem ThreeC2.Fact : ∃ (G : Type) (x : Magma G), Equation206 G ∧ ¬Equation1648 G

def ThreeC2.g : ThreeC2.W → ThreeC2.W

We use a variant of the above construction to show that 1841 does not imply 203. We use as the underlying magma M × Bool

Equations

• ThreeC2.g [] = [1]
• ThreeC2.g (x_1 :: __) = [x_1]

@[simp]

theorem ThreeC2.g_nil : ThreeC2.g [] = [1]

@[simp]

theorem ThreeC2.gg_nil : ThreeC2.g (ThreeC2.g []) = [1]

theorem ThreeC2.g_ne_nil (w : ThreeC2.W) : ThreeC2.g w ≠ []

@[simp]

theorem ThreeC2.red_g (w : ThreeC2.W) : ThreeC2.red (ThreeC2.g w) = ThreeC2.g w

@[simp]

theorem ThreeC2.rev_g (w : ThreeC2.W) : List.reverse (ThreeC2.g w) = ThreeC2.g w

@[simp]

theorem ThreeC2.f_nil_iff (w : ThreeC2.W) : ThreeC2.f w = [] ↔ w = []

theorem ThreeC2.ff_gff (z : ThreeC2.W) (h : ThreeC2.IsRed z) (ineq : z ≠ []) : ThreeC2.f (ThreeC2.f z) = ThreeC2.g (ThreeC2.red (ThreeC2.f (ThreeC2.f z) ++ z))

two variants of the main crucial relation

theorem ThreeC2.fg_gfg (z : ThreeC2.W) (h : ThreeC2.IsRed z) : ThreeC2.f (ThreeC2.g z) = ThreeC2.g (ThreeC2.red (ThreeC2.f (ThreeC2.g z) ++ z))

@[reducible, inline]

abbrev ThreeC2.M2 : Type

Equations

• ThreeC2.M2 = { x : ThreeC2.W × Bool // ThreeC2.IsRed x.1 }

instance ThreeC2.inst2 : Magma ThreeC2.M2

Equations

• One or more equations did not get rendered due to their size.

theorem ThreeC2.M2.Satisfies1841 : Equation1841 ThreeC2.M2

theorem ThreeC2.M2.Refutes203 : ¬Equation203 ThreeC2.M2

theorem ThreeC2.Fact2 : ∃ (G : Type) (x : Magma G), Equation1841 G ∧ ¬Equation203 G