\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*{SepProb}{Separativity Problem}
\newtheorem*{MainThm0}{Separativity via Unit-regularity}
\newtheorem*{MainThm1}{Diagonalizing Invertible Matrices}
\newtheorem*{MainThm2}{Diagonalizing over Separative Regular Rings}
\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}}

\DeclareMathOperator{\End}{End}
\DeclareMathOperator{\Hom}{Hom}
\DeclareMathOperator{\im}{im}
\DeclareMathOperator{\coim}{coim}
\DeclareMathOperator{\coker}{coker}
\DeclareMathOperator{\supp}{supp}
\DeclareMathOperator{\ann}{ann}
\DeclareMathOperator{\suit}{suit}
\DeclareMathOperator{\idem}{idem}
\DeclareMathOperator{\U}{U}
\DeclareMathOperator{\Nil}{Nil}
\DeclareMathOperator{\reg}{reg}
\DeclareMathOperator{\FP}{FP}

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

\begin{document}

\section{Another combinatorial nonimplication}

We will prove that Equation 1076, which is $x=y\diamond((x\diamond(x\diamond y))\diamond y)$, does not generally imply Equation 3, which is $x=x\diamond x$.  It was more convenient for me to work with a linearization of the form $x\diamond y=x+f(h)$ where $h=y-x$.

Working out the linearization of Equation 1076, we find
\begin{eqnarray*}
x & = & y\diamond((x\diamond [x+f(h)])\diamond y)\\
  & = & y \diamond([x+f^2(h)]\diamond y)\\
  & = & y\diamond [x+f^{2}(h)+f(h-f^{2}(h))]\\
  & = & x+h+f(f(h-f^2(h))-(h-f^2(h))),
\end{eqnarray*}
and so we want to choose $f$ satisfying the functional equation
\[
f[f(h-f^2(h))-(h-f^2(h))]=-h.
\]
On the other hand, the linearization of Equation 3 leads us to want $f(0)\neq 0$.

We take our carrier set to be a free abelian group $A$ on $\aleph_0$ generators.  ({\bf Note}:  One could just as well take $\aleph_1$ generators, if the initial seed needed to be infinite.)

Let $\mathscr{E}$ be the collection of sets $E\subseteq A^2$ where the following properties holds.
\begin{itemize}
    \item[(1)] $E$ is finite.
    \item[(2)] $E$ is a function (i.e., no element of $A$ occurs as the first coordinate of two different ordered pairs in $E$).
    \item[(3)] There are enough pairs in $E$ so that treating $E$ as a partial definition of $f$, the functional equation holds when $h=0$.
    \item[(4)] If $(a,b),(b,c)\in E$, then $(a-c,d),(-a+c+d,-a)\in E$ for some $d\in A$. (Thus, once we know that $E$ defines both $f(a)$ and $f^2(a)$, the functional equation holds when $h=a$.)
\end{itemize}

We partially order $\mathscr{E}$ under set inclusion.  The set $\mathscr{E}$ is nonempty, by noting $\{(0,0)\}\in \mathscr{E}$.  Alternatively, taking $p,q,r,s\in A$ to be independent generators, one can quickly check that
\[
E_0:=\{(0,p),(p,q),(-q,r),(q+r,0),(-p+q+r,s),(p-q-r+s,-q-r)\}
\]
also belongs to $\mathscr{E}$.  We will primarily work with extensions of $E_0$ in $\mathscr{E}$, in order to guarantee that $f(0)\neq 0$.

\begin{lemma}
For each $E\in \mathscr{E}$ and for each $z\in A$, there is an extension $E\subseteq E'\in \mathscr{E}$ where $E'$ satisfies the functional equation when $h=z$.
\end{lemma}
\begin{proof}
{\bf Case 1}:  Assume that $z$ is the first coordinate of some pair in $E$.

Fix $b$ to be the (unique, by condition (2)) second coordinate.  If $b$ is the first coordinate of some pair in $E$, then by condition (4), the functional equation already holds for $z$ by taking $E'=E$.  So, for the rest of this case, assume that $b$ is not a first coordinate of any pair.

Since $E$ is finite by (1), $b$ appears as the second coordinate of only finitely many pairs.  Fix $a_1,\ldots, a_n$ to be the list of the distinct first coordinates for such pairs.  (So one of the $a_i$ is $z$.)  Note that none of these $a_i$ is zero, by condition (3), since $f^2(a_i)$ is not defined.

For each integer $i\in [1,n]$, the element $-a_i\in A$ can appear as the first coordinate in at most one ordered pair in $E$.  Let $S$ be the set of indices where there is such a pair, and for each $i\in S$ fix $b_i'$ to be the unique element where $(-a_i,b_i')\in E$.  Let $T=\{i\in S\, :\, b_i'=0\}$.

Now, let $c$, $d_i$ ($i\in [1,n]$), and $e_j$ ($j\in S-T$) be a set of independent generators of $A$ that do not appear anywhere in the support of $E$.  We take
\begin{eqnarray*}
E' & := & E\cup\{(b,c)\}\cup\{(a_i-c,d_i),(-a_i+c+d_i,-a_i)\}_{i\in [1,n]}\\ 
    &   & \quad \cup \{(-a_j-b_j'+c+d_j,e_j),(a_j+b_j'-c-d_j+e_j,a_j-c-d_j)\}_{j\in S-T}\\
    &   & \quad\cup\{(-c-d_k,a_k-c-d_k)\}_{k\in T}.
\end{eqnarray*}

A finite check verifies each of the conditions, showing that $E'\in \mathscr{E}$ and that $E'$ satisfies the functional for each $a_i$ (hence for $z$).

{\bf Case 2}: Assume that $z$ is not the first coordinate of some pair in $E$.

If $z$ appears as the second coordinate of some pair in $E$, say $(z',z)$, by applying Case 1 to $z'$, we can extend $E$ to a new set $F$ so that the functional equation holds for $z'$.  Now, $z$ appears as a first coordinate of a pair in $F$, so using Case 1 again we can extend $F$ so that the functional equation holds for $z$.

If $z$ doesn't appear as either a first or a second coordinate, then by adding a new pair $(z,z')$, where $z'$ is any element of $A$ not appearing in the support of $E$, we again reduce to Case 1.
\end{proof}

We are now essentially done.  Well-ordering $A$, with order type $\omega$, we may recursively guarantee that there is an $\omega$ chain in $\mathscr{E}$, with $E_0$ at the bottom, where each element of $A$ becomes a first coordinate somewhere in the chain.  The union of such a chain is the needed complete $f$.

\end{document} 