more constructions (#904)

blueprint/src/chapter/counterexamples.tex

@@ -5,19 +5,19 @@ \chapter{Selected magmas}\label{selected-magmas-chapter}
 \begin{itemize}
   \item All magmas of order at most $4$, up to isomorphism (of which there are $178,985,294$);
   \item All commutative magmas of order $5$, up to isomorphism {\bf determine their count};
-  \item Cyclic groups $\Z/N\Z$ with $2 \leq N \leq 12$ and $x \circ y = ax^2+bxy+cy^2+dx+ey$ for randomly chosen $a,b,c,d,e$.
+  \item Cyclic groups $\Z/N\Z$ with $2 \leq N \leq 12$ and $x \op y = ax^2+bxy+cy^2+dx+ey$ for randomly chosen $a,b,c,d,e$.
   \item There are only $1410$ distinct cancellative magmas of order $5$ (up to isomorphism), and Mace4 can generate all of them in under 20 seconds. A shell script to do this is available \href{https://github.com/zaklogician/equational_theories/tree/cancellative_magmas/scripts/cancellative_magmas}{here}. A magma is cancellative if $xy=xz$ implies $y=z$ and $yx=zx$ implies $y=z$.
 \end{itemize}
 
 
 Some other magmas have been used to establish counterexamples:
 \begin{itemize}
   \item The cyclic group $\Z/6\Z$ with the addition law.
-  \item The natural numbers with law $x \circ y = x+1$.
-  \item The natural numbers with law $x \circ y = xy+1$.
-  \item The reals with $x \circ y = (x+y)/2$.
-  \item The natural numbers with $x \circ x$ equal to $x$ when $x=y$ and $x+1$ otherwise.
-  \item The set of strings with $x \circ y$ equal to $y$ when $x=y$ or when $x$ ends with $yyy$, or $xy$ otherwise (see \href{https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/3102.20does.20not.20imply.203176/near/474656031}{this Zulip thread}).
+  \item The natural numbers with law $x \op y = x+1$.
+  \item The natural numbers with law $x \op y = xy+1$.
+  \item The reals with $x \cirop y = (x+y)/2$.
+  \item The natural numbers with $x \op y$ equal to $x$ when $x=y$ and $x+1$ otherwise.
+  \item The set of strings with $x \op y$ equal to $y$ when $x=y$ or when $x$ ends with $yyy$, or $xy$ otherwise (see \href{https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/3102.20does.20not.20imply.203176/near/474656031}{this Zulip thread}).
   \item Vector spaces ${\mathbb F}_2^n$ over ${\mathbb F}_2$, which obey \Cref{eq1571} (and hence all the subsequent laws mentioned in \Cref{1571_impl}).
   \item Knuth's construction \cite{knuth} of a central groupoid (\Cref{eq168}) as follows.  Let $S$ be a (finite) set with a distinguished element $0$, and a binary operation $*$ such that $x*0=0$ and $0*x=x$   for all $x$, and for each $x,y$ there is a unique $z$ with $x*z=y$.  One can then define a central groupoid on $S \times S$ by defining $(a,b) \op (c,d)$ to equal $(b,c)$ if $c,d \neq 0$; $(b,e)$ if $b*e=c$ is non-zero and $d=0$; and $(a*b,0)$ if $c=0$.  One such example in \cite{knuth} is when $S = \{0,1,2\}$ with $1*1=2*1=2$ and $1*2=2*2=1$.
   \item Cancellative magmas of orders 7 to 9, found by hand-guided search using various solvers.

paper/constructions.tex

@@ -56,17 +56,95 @@ \subsection{Linear models}\label{linear-sec}
 \begin{remark} One can also consider the seemingly more general linear model $x \op y = ax + by$, where the carrier $M$ is now an abelian group, and $a,b$ act on $M$ by homomorphisms, that is to say that they are elements of the endomorphism ring $\mathrm{End}(M)$.  However, this leads to exactly the same varieties \eqref{variety} (where $M$ is now replaced by the endomorphism ring $\mathrm{End}(M)$) and so does not increase the power of the linear model for the purposes of refuting implications.
 \end{remark}
 
+\note{Mention linear immunities}
+
 \subsection{Translation-invariant models}\label{translation-sec}
 
-Translation-invariant magmas (see e.g., this thread for a nice example). Note: any magma with a transitive symmetry will lift to a translation-invariant model, so this helps explain why these are common examples. Also symmetric models could be slightly more likely to obey various laws than general models due to degree of freedom considerations.
+It is natural to look for counterexamples amongst magmas that obey a large number of symmetries.  One such class of counterexamples are \emph{translation-invariant models}, in which the carrier $M$ is a group, and the left translations of this group form isomorphisms of the magma $M$.  In the case of an abelian group $M = (M,+)$, such models take the form
+\begin{equation}\label{xop-add}
+  x \op y = x + f(y-x)
+\end{equation}
+for some function $f \colon M \to M$; in the case of a non-abelian group $M = (M,\cdot)$, such models instead take the form
+\begin{equation}\label{xop-mul}
+x \op y = x f(x^{-1} y).
+\end{equation}
+For such models, the verification of an equational law in $n$ variables corresponds to a functional equation for $f$ in $n-1$ variables, as the translation symmetry allows one to normalize one variable to be the identity (say). This can simplify an implication to the point where an explicit counterexample can be found.
+
+\begin{example}[Abelian example]\label{abex}  For the law $\x \formaleq (\x \op \y) \op ((\x \op \y) \op \y)$ \eqref{eq1648}, we apply the abelian translation-invariant model \eqref{xop-add} with $y=x+h$ to obtain
+\begin{align*}
+  x \op y &= x + f(h) \\
+  (x \op y) \op y &= x + f(h) + f(h-f(h)) \\
+  (x \op y) \op ((x \op y) \op y) &= x + f(h) + f(f(h-f(h)))
+\end{align*}
+so that this law obeys \eqref{eq1648} if and only if the functional equation
+$$f(h) + f(f(h-f(h))) = 0$$
+holds for all $h \in M$.  Similarly, the law $\x \formaleq (\x \op (\x \op \y)) \op \y$ \eqref{eq206} is obeyed if and only if
+$$ f(f(h)) + f(h - f(f(h))) = 0$$
+for all $h \in M$.  One can now check that the function $f \colon \Z \to \Z$ defined by $f(h) \coloneqq - \mathrm{sgn}(h)$ (thus $f(h)$ equals $-1$ when $h$ is positive, $+1$ when $h$ is negative, and $0$ when $h$ is zero) obeys the first functional equation but not the second, thus establishing that $E1648 \not \vdash E206$.
+\end{example}
+
+\begin{example}[Non-abelian example]  We now obtain the opposite refutation $E206 \not \vdash E1648$ to \Cref{abex} using the non-abelian translation-invariant model.  By similar calculations to before, we now seek to find a function $f \colon M \to M$ on a non-abelian group $(M,\cdot)$ that obeys the functional equation
+\begin{equation}\label{206-eq}
+ f(f(h)) f(f(f(h))^{-1} h) = 1
+\end{equation}
+for all $h \in M$, but fails to obey the functional equation
+\begin{equation}\label{1648-eq}
+   f(h) f(f(f(h)^{-1} h)) = 1
+\end{equation}
+for at least one $h \in M$.  Now take $M$ to be the group generated by three generators $a,b,c$ subject to the relations $a^2=b^2=c^2=1$, or equivalently the group of reduced words in $a,b,c$ with no adjacent letters in the word equal.  We define
+$$ f(1) = 1, f(a)=b, f(b) = c, f(c) = a$$
+and then $f(aw)=a$ for any non-empty reduced word $w$ not starting with $a$, and similarly for $b$ and $c$.  The equation \eqref{206-eq} can be checked directly for $h=1,a,b,c$.  If $h=aw$ with $w$ non-empty, reduced, and not starting with $a$, then $f(f(h))^{-1} = f(f(h)) = b$ and $f(f(f(h))^{-1} h) = f(baw) = b$, giving \eqref{206-eq} in this case, and similarly for cyclic permutations. Meanwhile, \eqref{1648-eq} can be checked to fail for $h=a$.
+\end{example}
+
+\note{Mention translation-invariant immunity}
+
+\subsection{The twisting semigroup}\label{twisting-sec}
+
+Suppose one has a magma $M$ obeying a law $E$, that also enjoys some endomorphisms $T, U \colon M \to M$.  Then one can ``twist'' the operation $\op$ by $T,U$ to obtain a new magma operation
+\begin{equation}\label{twist} x \op' y := Tx \op Uy.
+\end{equation}
+If one then tests whether this new operation $\op'$ obeys the same law $E$ as the original operation $\op$, one will find that this will be the case provided that $T,U$ obey a certain set of relations.  The semigroup generated by formal generators $\mathrm{T}, \mathrm{U}$ with these relations will be called the \emph{twisting semigroup} $\operatorname{Twist}_E$ of $E$.  This can be best illustrated with some examples.
 
-Mention translation-invariant immunity
+\begin{example}  We compute the twisting semigroup of $\x \formaleq (\y \op \x) \op (\x \op (\z \op \y))$ \eqref{eq1485}.  We test this law on the operation \eqref{twist}, thus we consider whether
+$$x = (y \op' x) \op' (x \op' (z \op' y))$$
+holds for all $x,y,z \in M$.  Substituting in \eqref{twist} and using the homomorphism property repeatedly, this reduces to
+$$x = (T^2y \op TUx) \op (UTx \op (U^2T z \op U^3y)).$$
+If we impose the conditions $TU=UT$, $T^2 = U^3$, then this equation would follow from \eqref{eq1485} (with $x,y,z$ replaced with $TUx$, $T^2 y$, $U^2 Tz$ respectively).  Thus the twisting semigroup $\operatorname{Twist}_{E1485}$ of \eqref{eq1485} is generated by two generators $\mathrm{T}, \mathrm{U}$ subject to the relations $\mathrm{T} \mathrm{U}=\mathrm{U} \mathrm{T} = 1$, $\mathrm{T}^2 = \mathrm{U}^3$.  This is a cyclic group of order $5$, since the relations can be rewritten as $\mathrm{T}^5 = 1$, $\mathrm{U} = \mathrm{T}^{-1}$.
+
+Now consider $\x \formaleq (\x \op \x) \op (\x \op \x)$ \eqref{eq151}.  Applying the same procedure, we arrive at
+$$x = (T^2 x \op TUx) \op (UT x \op U^2 x)$$
+so the twisting group $\operatorname{Twist}_{E151}$ is generated by two generators $\mathrm{T}, \mathrm{U}$ subject to the relations $\mathrm{T} \mathrm{U}=\mathrm{U} \mathrm{T} = \mathrm{T}^2 = \mathrm{U}^2 = 1$.  This is a cyclic group of order $2$, since the relations can be rewritten as $\mathrm{T}^2 = 1$, $\mathrm{U} = \mathrm{T}$.
+\end{example}
+
+Suppose the twisting semigroup $\operatorname{Twist}_E$ is not a quotient of $\operatorname{Twist}_{E'}$, in the sense that the relations that define $\operatorname{Twist}_{E'}$ are not obeyed by the generators of $\operatorname{Twist}_E$.  Then one can often disprove the implication $E \vdash E'$ by attempting the following procedure.
+\begin{itemize}
+\item First, locate a non-trivial magma $M$ obeying the law $E$.  Then the Cartesian power $M^{\operatorname{Twist}_E}$ of tuples $(x_W)_{W \in \operatorname{Twist}_E}$, with the pointwise magma operation, will also obey $E$.
+\item Furthermore, this Cartesian power admits two endomorphisms $T, U$ defined by
+$$ T (x_W)_{W \in \operatorname{Twist}_E} = (x_{W \mathrm{T}})_{W \in \operatorname{Twist}_E};
+U (x_W)_{W \in \operatorname{Twist}_E} = (x_{W \mathrm{U}})_{W \in \operatorname{Twist}_E},$$
+which obey the relations defining $\operatorname{Twist}_E$.
+\item We now twist the magma operation $\op$ on $M^{\operatorname{Twist}_E}$ by $T,U$ to obtain a new magma operation $\op'$ defined by \eqref{twist}, that will still obey law $E$.
+\item Because $T, U$ will not obey the relations defining $\operatorname{Twist}_{E'}$, it is highly likely that this twisted operation will not obey $E'$, thus refuting the implication $E \vdash E'$.
+\end{itemize}
+
+For instance, a non-trivial finite model for \eqref{eq1485} is given by the finite field $\mathbb{F}_2$ of two elements with the NAND operation $x \op y \coloneqq 1-xy$.  If we twist $\mathbb{F}_2^5$ by the left shift $T(x_i)_{i=1}^5 = (x_{i+1})_{i=1}^5$ and right shift $U(x_i)_{i=1}^5 = (x_{i-1})_{i=1}^5$, where we extend the indices periodically modulo $5$, then the resulting operation
+$$ (x_i)_{i=1}^5 \op' (y_i)_{i=1}^5 \coloneqq (1 - x_{i+1} y_{i-1})_{i=1}^5$$
+on $\mathbb{F}_2^5$ will still obey \eqref{eq1485}, but will not obey \eqref{eq151}, thus showing that $E1485 \not \vdash E151$.  This particular implication does not seem to be easily establishable by any of the other methods discussed in this paper.
+
+\note{Report on how large the twisting semigroups are in practice, and how many implications can be refuted by this method.}
 
 \subsection{Ad hoc constructions}\label{adhoc-sec}
 
+\note{TODO: Expand this sketch}
+
 Tree based constructions, see here.
 
 \subsection{Greedy constructions}\label{greedy-sec}
 
+\note{TODO: Expand this sketch}
+
+Discuss the greedy method in both translation-invariant and non-translation-invariant settings.  Mention how ATPs can be used.
 
 \subsection{Modifying base models}\label{modify-base}
+
+\note{TODO: Expand this sketch}

paper/intro.tex

@@ -58,12 +58,13 @@ \subsection{Outcomes}
 
 More challenging were the $13855357$ ($62.88\%$) implications that were false, $E \not \vdash E'$. Here, the range of techniques needed to refute such implications were quite varied.
 \begin{itemize}
-        \item Syntactic methods, such as observing an ``matching invariant'' of the law $E$ that was not shared by the law $E'$, could be used to obtain some refutations.  For instance, if both sides of $E$ had the same order, but both sides of $E'$ did not, this could be used to syntactically refute $E \vdash E'$.  Similarly, if the law $E$ was confluent, enjoyed a complete rewriting system, or otherwise permitted some understanding of the free magma associated to that law, one could decide the assertions $E \vdash E'$ for all possible laws $E'$, or at least a significant fraction of such laws.  We discuss these methods, and the extent to which they can be automated in \Cref{syntactic-sec}.  One novel such invariant we introduce here is the ``twisting semigroup'' of an equational theory, which gave simple refutations of some otherwise very challenging implications.
+        \item Syntactic methods, such as observing an ``matching invariant'' of the law $E$ that was not shared by the law $E'$, could be used to obtain some refutations.  For instance, if both sides of $E$ had the same order, but both sides of $E'$ did not, this could be used to syntactically refute $E \vdash E'$.  Similarly, if the law $E$ was confluent, enjoyed a complete rewriting system, or otherwise permitted some understanding of the free magma associated to that law, one could decide the assertions $E \vdash E'$ for all possible laws $E'$, or at least a significant fraction of such laws.  We discuss these methods, and the extent to which they can be automated in \Cref{syntactic-sec}.
         \item Small finite magmas, which can be described explicitly by multiplication tables, could be tested by brute force computations to provide a large number of counterexamples to implications, or by ATP-assisted methods. See \Cref{finite-sec}.
         \item Linear models, in which the magma operation took the form $x \op y = ax + by$ for some (commuting or non-commuting) coefficients $a,b$, allowed for another large class of counterexamples to implications, which could be automatically scanned for either by brute force or by Grobner basis type calculations. See \Cref{linear-sec}.
         \item Translation invariant models, in which the magma operation took the form $x \op y = x + f(y-x)$ on an additive group, or $x \op y = x f(x^{-1} y)$ on a non-commutative group, reduce matters to analyzing certain functional equations; see \Cref{translation-sec}.
         \item Greedy methods, in which either the multiplication table $(x,y) \mapsto x \op y$ or the function $f$ determining a translation-invariant model are iteratively constructed by a greedy algorithm subject to a well-chosen ruleset, were effective in resolving many implications not easily disposed of by preceding methods. See \Cref{greedy-sec}.
         \item Starting with a simple base magma $M$ obeying both $E$ and $E'$, and either enlarging it to a larger magma $M' \supset M$, extending it to a magma $N$ with a projection homomorphism $\pi: N \to M$, or modifying the multiplication table on a small number of values, also proved effective when combined with greedy methods. See \Cref{modify-base}.
+        \item To each equation $E$ one can associate a ``twisting semigroup'' $S_E$.  If $S_E$ is larger than $S_{E'}$, then this can often be used to disprove the implication $E \vdash E'$; see \Cref{twisting-sec}.
         \item Some \emph{ad hoc} models based on existing mathematical objects, such as infinite trees, rings of polynomials, or ``Kisielewicz models'' utilizing the prime factorization of the natural numbers, could also handle some otherwise difficult cases.  In some cases, the magma law induced some relevant and familiar structures, such as a directed graph or a partial order, which also helped guide counterexample constructions. See \Cref{adhoc-sec}.
         \item Automated theorem provers were helpful in identifying which simplifying axioms could be added to the magma without jeopardizing the ability to refute the desired implication $E \vdash E'$.
 \end{itemize}

paper/numbering.tex

@@ -47,15 +47,19 @@ \section{Numbering system}\label{numbering-app}
         \x \op \x &\formaleq \y \op\ z \label{eq41}\tag{E41} \\
         \x \op \y &\formaleq \y \op \x & \hbox{(Commutative law)} \label{eq43}\tag{E43} \\
         \x \op \y &\formaleq \z \op \w & \hbox{(Constant law)} \label{eq46}\tag{E46} \\
+        \x &\formaleq (\x \op \x) \op (\x \op \x) \label{eq151}\tag{E151} \\
         \x &\formaleq (\y \op \x) \op (\x \op \z) & \hbox{(Central groupoid law)} \label{eq168}\tag{E168} \\
+        \x &\formaleq (\x \op (\x \op \y)) \op \y \label{eq206}\tag{E206} \\
         \x \op \y &\formaleq \x \op (\y \op \z) \label{eq327}\tag{E327} \\
         \x &\formaleq (\x \op \y) \op \y \label{eq378}\tag{E378} \\
         \x \op \y &\formaleq (\z \op \x) \op \y \label{eq395}\tag{E395} \\
         \x &\formaleq \y \op ( (\z \op (\x \op (\y \op \z)))) & \hbox{(Tarski's axiom)} \label{eq543}\tag{E543} \\
         \x &\formaleq \x \op ((\y \op \z) \op (\x \op \z)) \label{eq854}\tag{E854}\\
         \x &\formaleq \y \op ((\y \op (\x \op \z)) \op \z) \label{eq1117}\tag{E1117} \\
         \x &\formaleq \y \op (((\x \op \y) \op \x) \op \y) \label{eq1286}\tag{E1286} \\
+        \x &\formaleq (\y \op \x) \op (\x \op (\z \op \y)) \label{eq1485}\tag{E1485} \\
         \x &\formaleq (\y \op \z) \op (\y \op (\x \op \z)) & \hbox{(Exp. $2$ abelian groups)} \label{eq1571}\tag{E1571} \\
+        \x &\formaleq (\x \op \y) \op ((\x \op \y) \op \y) \label{eq1648}\tag{E1648} \\
         \x &\formaleq (\y \op \x) \op ((\x \op \z) \op \z) \label{eq1689}\tag{E1689} \\
         \x &\formaleq (\x \op ((\x \op \x) \op \x)) \op \x \label{eq2441}\tag{E2441} \\
         \x \op \y &\formaleq \x \op (\y \op (\x \op \y)) \label{eq3316}\tag{E3316} \\