\documentclass[12pt,oneside,leqno]{amsart}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage[hidelinks]{hyperref}
\usepackage{tikz}
\usetikzlibrary{cd}
\usepackage{mathrsfs}

\newenvironment{nouppercase}{%
  \let\uppercase\relax%
  \renewcommand{\uppercasenonmath}[1]{}}{}

\usepackage{comment}

\makeatletter
\renewcommand{\eqref}[1]{\textup{(\ignorespaces\ref{#1}\unskip\@@italiccorr)}}
\def\maketag@@@#1{\hbox{\m@th\normalfont\bfseries#1}}
\makeatother

% THEOREMS -------------------------------------------------------

\numberwithin{equation}{section}
\numberwithin{figure}{section}

\theoremstyle{plain}
\newtheorem{thm}[equation]{Theorem}
\newtheorem{lemma}[equation]{Lemma}
\newtheorem{cor}[equation]{Corollary}
\newtheorem{prop}[equation]{Proposition}
\newtheorem{example}[equation]{Example}

\theoremstyle{definition}
\newtheorem{definition}[equation]{Definition}
\newtheorem{question}[equation]{Question}
\newtheorem{remark}[equation]{Remark}



% MATH -----------------------------------------------------------
\newcommand{\Q}{\ensuremath \mathbb{Q}}
\newcommand{\R}{\ensuremath \mathbb{R}}
\newcommand{\C}{\ensuremath \mathbb{C}}
\newcommand{\Z}{\ensuremath \mathbb{Z}}
\newcommand{\N}{\ensuremath \mathbb{N}}
\newcommand{\M}{\ensuremath \mathbb{M}}
\newcommand{\F}{\ensuremath \mathbb{F}}

\newcommand\subsetsim{\mathrel{\substack{
  \textstyle\subset\\[-0.2ex]\textstyle\sim}}}

\begin{document}

\section{Handling Equation 63}

Equation 63 is $x=y\diamond (x\diamond (x\diamond y))$.  Work with a carrier set $G$ that is the free group on countably many letters $x_1,x_2,\ldots$.  (If easier, the free abelian group will also work.  I just personally found it easier to work multiplicatively, and so kept track of orders of products.)  Setting $y=hx$ and $a\diamond b=f(ba^{-1})a$, where $f\colon G\to G$ is a function, we are led to the functional equation
\[
f(f^2(h)h^{-1})=h^{-1}.
\]
Think of this as saying that if $(a,b),(b,c)\in f$, then we must have $(ca^{-1},a^{-1})\in f$.

An important initial seed is the following:
\begin{eqnarray*}
E_0 & := & \{(1,x_1),(x_1,x_2),(x_2,1),(x_1^{-1},x_1^{-1}),(x_1x_2^{-1},x_2^{-1}),(x_2^{-1},x_3),(x_3x_2x_1^{-1},x_2x_1^{-1}),\\
 & & \ (x_3,x_1x_2^{-1}),(x_2^{-1}x_3^{-1},x_3^{-1})\}.
\end{eqnarray*}
Define $\mathscr{E}$ as the collection of sets $E\subseteq G^2$ satisfying the following properties.
\begin{itemize}
    \item[(1)] $E$ is finite.
    \item[(2)] $E$ is a function.
    \item[(3)] $E_0\subseteq E$.
    \item[(4)] If $(a,1)\in E$, then $a=x_2$.
    \item[(5)] If $(a,b),(b,c)\in E$, then $(ca^{-1},a^{-1})\in E$.
    \item[(6)] If $(a,b),(a',b),(a^{-1},d)\in E$, then $da\neq a'$.
    \item[(7)] If $(a,b),(a',b),(a^{-1},d),(a'^{-1},d')\in E$, and $da=d'a'$, then $a=a'$.
    \item[(8)] If $(a,b),(a',b),(a^{-1},d),(a'^{-1},d)\in E$, then $a=a'$.
\end{itemize}

\begin{lemma}
For any $E\in \mathscr{E}$ and any $a\in G$, there is an extension $E\subseteq E'\in \mathscr{E}$ where the functional equation holds for $a$.
\end{lemma}
\begin{proof}
{\bf Case 1}: Assume $(a,b)\in E$ for some $b\in G$.

If $b\in {\rm dom}(E)$, then by condition (5) we are already done.  So reduce to the case when $b\notin {\rm dom}(E)$.  Let $a_1,a_2,\ldots, a_n$ be the finite list of first coordinates in $E$ that map to $b$.  In particular, note that this means $a_i\neq 1$ and $a_i\neq q^{-1}$ (for each $i$) by condition (3).  (This, plus the closure condition (5), is the reason we need so many pairs in $E_0$.)  

Let $S$ be the subset of indices $j$ where $(a_j^{-1},d_j)\in E$ for some $d_j\in G$.  Note that $d_j\neq 1$, since $a_j\neq x_2^{-1}$, using condition (4).  Also note that if $j,k\in S$ are distinct, then $d_j\neq d_k$ by condition (8), and also by condition (7) we know $d_ja_j\neq d_ka_k$.

Fix $c$ to be the least generator of $G$ that does not appear anywhere in the reduced forms for the coordinates in $E$.  We then take
\[
E':=E\cup\{(b,c),(ca_i^{-1},a_i^{-1})\}_{i\in [1,n]}\cup\{(d_ja_jc^{-1},a_jc^{-1}\}_{j\in S}.
\]

Conditions (1) and (3) for $E'$ are clear.  For (2), use $d_ja_j\neq d_ka_k$ when $j,k\in S$ are distinct. Next, (4) holds since none of the new pairs ends in $1$ (because $a_i\neq 1$).  A finite check also shows that condition (5) holds (here, we need to use the fact that (6) holds for $E$ to get $da_j\neq a_i$ for any $j\in S$ and $i\in [1,n]$).

Next, (6) holds by considering cases, noting that $c$ is a new generator, and again using $da_j\neq a_i$ (so that $a_ic^{-1}\notin {\rm dom}(E')$), and similarly for (7) and (8).

{\bf Case 2}: Assume $a\notin {\rm dom}(E)$.  If $(y,a)\in E$ for some $y\in G$, then applying Case 1 to $y$, we reduce to the situation when $a\in {\rm dom}(E)$ after all.  Thus, we may assume $a\notin {\rm im}(E)$.  Using $E\cup\{(a,b)\}$, where $b$ is the least generator of $G$ not appearing in the reduced forms for the coefficients of $E$, nor of $a$, we reduce to Case 1 again.
\end{proof}

Equation 1692 is $x=(y\diamond x)\diamond((y\diamond x)\diamond y)$.  The corresponding functional equation is
\[
hf(h)^{-1}=f^2(f(h)^{-1}).
\]
The seed $E_0\cup\{(x_4,x_5),(x_5^{-1},x_6),(x_6,x_7),(x_7x_5,x_5)\}$ is in $\mathscr{E}$ (by a finite check) and fails this new equation.  After extending to a full function, we are done.

\end{document} 
