CENTRAL_GROUPOID: Prove Theorem 5.9 (natural central groupoid axiom)

[teorth]

This result of Knuth shows that a certain five-operation law (Equation 26302) is equivalent to being a natural central groupoid. The proof is quite lengthy; a sketch is at https://teorth.github.io/equational_theories/blueprint/sect0004.html#natural-central-groupoid , but one should review the original paper of Knuth (Theorem 5) at https://www.sciencedirect.com/science/article/pii/S0021980070800321 for the full details. But perhaps there is also a more efficient proof.

This would most naturally go into CentralGroupoids.lean. When done, mark the theorem and proof of Theorem 5.9 with \leanok's and an appropriate \lean{} tag.

[ChienYungChi]

claim

[ChienYungChi]

disclaim

[ChienYungChi]

I disclaimed the issue, but below is my partial progress. If the code below is helpful, please feel free to use it.

In Equations.lean:

equation 26302 := x = (y ◇ ((z ◇ x) ◇ w)) ◇ (x ◇ w)

In CentralGroupoids.lean:

import equational_theories.Equations

class NaturalCentralGroupoid (S : Type _) where
  op : (S × S) → (S × S) → (S × S)
  op_eq : ∀ (x1 x2 y1 y2 : S), op (x1, x2) (y1, y2) = (x2, y1)

instance {S : Type*} [NaturalCentralGroupoid S] : Magma (S × S) where
  op := NaturalCentralGroupoid.op

lemma NaturalCentralGroupoid_as_Magma {S : Type*} [NaturalCentralGroupoid S] (x1 x2 y1 y2 : S) : (x1, x2) ◇ (y1, y2) = (x2, y1) := by
  exact NaturalCentralGroupoid.op_eq x1 x2 y1 y2

theorem NaturalCentralGroupoid_implies_Equation26302 (S : Type*) [NaturalCentralGroupoid S]  : Equation26302 (S × S) := by
  intro x y z w
  let (x1, x2) := x
  let (y1, y2) := y
  let (z1, z2) := z
  let (w1, w2) := w
  calc
    (x1, x2)
    _= (y2, x1) ◇ (x2,w1) := by rw [← NaturalCentralGroupoid_as_Magma y2 x1 x2 w1]
    _= ((y1, y2) ◇ (x1, w1)) ◇ (x2,w1) := by rw [← NaturalCentralGroupoid_as_Magma y1 y2 x1 w1]
    _= ((y1, y2) ◇ ((z2,x1) ◇ (w1, w2))) ◇ (x2,w1) := by rw [← NaturalCentralGroupoid_as_Magma z2 x1 w1 w2]
    _= ((y1, y2) ◇ (((z1, z2) ◇ (x1, x2)) ◇ (w1, w2))) ◇ (x2,w1) := by rw [← NaturalCentralGroupoid_as_Magma z1 z2 x1 x2]
    _= ((y1, y2) ◇ (((z1, z2) ◇ (x1, x2)) ◇ (w1, w2))) ◇ ((x1, x2) ◇ (w1, w2)) := by rw [← NaturalCentralGroupoid_as_Magma x1 x2 w1 w2]

[b-mehta]

claim

[b-mehta]

propose #492