\documentclass{article}
\usepackage[T1]{fontenc}
\usepackage{amsmath,amssymb,amsthm}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newcommand{\op}{\mathop{\diamond}}
\begin{document}

\title{Human-understandable proof of\\ 650 $\implies$ $x \op y = x$}
\author{Bruno Le Floch}
\date{May 19, 2025}
\maketitle

\begin{theorem}[650 $\implies$ 4]
  Equation 650 $x = x \op (y \op ((z \op x) \op y))$ implies Equation 4 $x = x \op y$.
\end{theorem}

Throughout the proof, free variables in the various equations are arbitrary elements of the magma, for instance $(y \op x) \op x = y \op x$ stands for $\forall x \, \forall y \, (y \op x) \op x = y \op x$, unless a particular assignment has been specified (in terms of other variables).
We introduce the notation
\begin{align}
  f(x,y) & = x \op (y \op x) , &   g(x,y) & = f(x, y \op x) = x \op ((y \op x) \op x) , \\
  x^2 & = x \op x , & x^3 & = x^2 \op x , \qquad x_3 = x \op x^2 .
\end{align}
The proof consists of showing many intermediate results of the form $A \op B = A$ where $A$ and $B$ are various expressions, with the aim of making them more and more decoupled from each other as the proof progresses.  We begin with five easy identities involving simply $f$ and/or $g$ with no nesting, used throughout the proof.  Then we show idempotence $f(u,v)^2 = f(u,v)$ for suitable $v$ in~\eqref{lemma_F_fidem}, leading us to the result $(x \op y) \op g(x, z) = x \op y$ \eqref{lemma_G_projg}.  We then build towards a proof of Equation 58, $x \op (y \op (z \op x)) = x$, through a collection of intermediate results that are then enough to prove Equation 4, $x = x \op y$, and finish the proof.

\begin{lemma}[Easy identities on products of $f$ and $g$]
  \begin{align}
    \label{lemma_A} x \op f(y, z \op x) & = x , \\
    \label{lemma_B} x \op (z \op x)_3 & = x , \\
    \label{lemma_C_ff} f(x, y \op w) \op f(z, w) & = f(x, y \op w) , \\
    \label{lemma_D_ff} y \op w = y & \implies f(x, y) \op f(z, w) = f(x, y) , \\
    \label{lemma_E_gf} g(x, y) \op f(z, x) & = g(x, y) .
  \end{align}
\end{lemma}

\begin{proof}
  The first identity is just Equation 650 in disguise.
  The second is obtained by taking $y = z \op x$ in the first and noting that $f(z \op x, z \op x) = (z \op x)_3$.
  The third is the main identity with $(x,y,z) \to (f(x, y \op w), z, w)$ and using $w \op f(x, y \op w) = w$ to simplify the last part of the right-hand side.
  The fourth is a rewriting of the third, which proves very useful in the following, as it tells us the product of two rather general $f(\_, \_)$.
  The fifth is a special case of the third with $w=x$, using that $f(x, y \op x) = g(x, y)$.  It allows us to rewrite some products of $g(\_, \_)$ times $f(\_, \_)$.
\end{proof}

\begin{lemma}[Projection for multiplication by $g$]
  \begin{align}
    \label{lemma_F_fidem} f(v,w) = v & \implies f(u,v)^2 = f(u,v) , \\
    \label{lemma_G_projg} (x \op y) \op g(x, z) & = x \op y .
  \end{align}
\end{lemma}

\begin{proof}
  Select some arbitrary element $a_0$ of the magma (say, $a_0=u$) and calculate.
  In the first two steps we manipulate the second operand of $f(u,v) \op f(u,v)$ to convert it to $f(f(u,v),\_)$, then we apply \eqref{lemma_D_ff} to the resulting product of~$f$.  Specifically, the first application of~\eqref{lemma_D_ff} uses that $f(v,w)=v$, and the second one that $v \op f(a_0, w\op v) = v$ by the main identity~\eqref{lemma_A}:
  \begin{equation}
    \begin{aligned}
      f(u,v)^2
      & \overset{\eqref{lemma_D_ff}}{=}
        f(u,v) \op \bigl(f(u,v) \op f(a_0, w \op v)\bigr)
      \\
      & \overset{\eqref{lemma_C_ff}}{=}
        f(u,v) \op \Bigl(f(u,v) \op \bigl(f(a_0, w \op v) \op f(u,v)\bigr) \Bigr)
        \overset{\eqref{lemma_D_ff}}{=}
        f(u,v) .
    \end{aligned}
  \end{equation}
  We now establish \eqref{lemma_G_projg}.  Denote $u=f(y,x)$, $v=g(x,z)$ and $w=(z \op x) \op x$.
  By \eqref{lemma_E_gf}, $v = v \op f(\_, x)$.  We use this in two ways.
  First, since $u=f(y,x)$ we have $v = v \op u$.
  Second, we get $v = v \op f(w, x) = v \op (w \op v) = f(v,w)$, which serves as a premise to \eqref{lemma_F_fidem}, so that $f(u,v)^2 = f(u,v)$.
  Simplifying $f(u,v) = u \op (v \op u) = u \op v$, we have the idempotence $(u \op v)^2 = u \op v$.
  We insert this property into \eqref{lemma_B} to get $v = v \op (u \op v)_3 = v \op (u \op v) = f(v,u)$.
  It is then easy to conclude:
  \begin{equation}
    (x \op y) \op v = (x \op y) \op f(v,u) \overset{\eqref{lemma_A}}{=} x \op y ,
  \end{equation}
  where in the second step we used that $u = f(y,x) = y \op (x \op y)$.
\end{proof}

\begin{lemma}[Towards Equation 58]
  \begin{align}
    \label{lemma_H_eq58_g} x \op (g(y, z) \op (y \op x)) & = x , && \text{(restricted version of equation 58)} , \\
    \label{lemma_I_zx2} x \op \bigl((y \op (z \op x)) \op (z \op x)\bigr) & = x , && \text{(equation 58 with duplicated $z \op x$)} , \\
    \label{lemma_J_move_proj} y \op (z \op x) = y \implies x \op y & = x , && \text{(equation 4 under a condition)} , \\
    \label{lemma_K_idem} (y \op x) \op x & = y \op x , && \text{(right-multiplication idempotent)} , \\
    \label{lemma_L_cube} x^3 & = x^2 , && \text{(cubes are squares)} , \\
    \label{eq58} x \op (y \op (z \op x)) & = x , && \text{(equation 58)} ,
  \end{align}
\end{lemma}

\begin{proof}
  Our main aim here is to prove Equation 58, \eqref{eq58}.  We begin with a special case~\eqref{lemma_H_eq58_g} involving~$g$ instead of a general element of the magma, then a version of the equation where $z \op x$ is duplicated.  It is then simplified using a convenient deduplication identity~\eqref{lemma_K_idem} (Equation 378).

  Let us begin.  For the first identity, we use \eqref{lemma_G_projg} with $x,y$ swapped to transform the product of $g(y, z)$ and $y \op x$ into a call to~$f$, and we then simplify using the main equation~\eqref{lemma_A},
  \begin{equation}
    x \op \bigl(g(y, z) \op (y \op x)\bigr)
    \overset{\eqref{lemma_G_projg}}{=}
    x \op \Bigl(g(y, z) \op \bigl((y \op x) \op g(y, z)\bigr) \Bigr)
    \overset{\eqref{lemma_A}}{=} x .
  \end{equation}
  The second one is a more tricky calculation.
  The basic idea is that \eqref{lemma_G_projg} and \eqref{lemma_H_eq58_g} both involve the product of some $w \op u$ and $g(w, y)$ in different orders, so we can get leverage from making these two factors equal: set $u = (y \op w) \op w$ so that $w \op u = g(w, y)$.  One gets
  \begin{equation}
    u \overset{\eqref{lemma_H_eq58_g}}= u \op (w \op u)^2
    \overset{\eqref{lemma_G_projg}} = u \op (w \op u) = f(u, w) .
  \end{equation}
  Then, by taking $w = z \op x$ and applying the main equation, we deduce
  \begin{equation}
    x \op u = x \op f(u, z \op x) = x , \qquad
    \text{for } u = \bigl(y \op (z \op x)\bigr) \op (z \op x) ,
  \end{equation}
  which is the desired identity \eqref{lemma_I_zx2}.

  The rest of the proof is very straightforward.  If $y \op (z \op x) = y$ then the left-hand side of \eqref{lemma_I_zx2} simplifies all the way down to $x \op y$, thus \eqref{lemma_J_move_proj} holds.  Then, by \eqref{lemma_H_eq58_g} we have $\exists w, x \op (w \op (y \op x))$, so we can apply \eqref{lemma_J_move_proj} with $(x,y)$ replaced by $(y \op x, x)$, which yields exactly \eqref{lemma_K_idem}, the idempotence of right-multiplication.  A particular case used later is that cubes are the same as squares, as stated in \eqref{lemma_L_cube}.  Finally, idempotence of right-multiplication simplifies \eqref{lemma_I_zx2} to the desired Equation 58, \eqref{eq58}.
\end{proof}

\begin{lemma}[Equation 4]
  \begin{equation}\label{eq4}
    x \op y = x ,
  \end{equation}
\end{lemma}

\begin{proof}
  At this point, we know enough about the operation to conclude.
  From \eqref{lemma_G_projg} with $z=x$ we have $(x \op y) \op g(x, x) = x \op y$, which takes the form of the premise of \eqref{lemma_J_move_proj} applied to $(x^2, x \op y, x)$ since $g(x, x) = x \op x^3 = x \op x^2$ by \eqref{lemma_L_cube}.  We learn that $x^2 \op (x \op y) = x^2$.  We then calculate as follows,
  \begin{equation}
    x \op y \overset{\eqref{eq58}}{=} x \op (y \op (x^2 \op (x \op y)))
    = x \op (y \op x^2) \overset{\eqref{eq58}}{=} x . \qedhere
  \end{equation}
\end{proof}

Once we have the left-projection law \eqref{eq4}, Equation 4, all the consequences are immediately found by direct computation, for instance Equation 448 holds, $x = x \op (y \op (z \op (x \op z)))$.

\end{document}