Understanding Finite 1486 Magmas

Stream: Equational

[Matthew Bolan]

I'd really like to find settings for Mace4 (or even Vampire) which let them find the degree 21 1486 magma as efficiently as possible. I know of only 4 "sporadic" 1486 magmas that do not satisfy 168, one of order 11, one of order 13, one of order 18, and one of order 21, and Mace4 cannot find the latter two easily. There might be more of each of these orders, I have not checked exhaustively at all.

[Douglas McNeil]

Mace4 returns hundreds of order 11 nonisomorphic magmas which satisfy 1486 but violate 168 (definitely nonisomorphic because they satisfy different combinations of equations). Anything not impossible must happen somewhere, or whatever the saying is..

In the order 11 magmas I've seen, _given_ an 168 failure 168 always seems to have the same number of failures, as does 817 and 1076, (and 3862/3877/1486 at 0) whereas others like 854 have a wider range of failure points. Not super-scientific given it's not sampling the space uniformly, but I saw similar behaviour when 854/413 hunting exhaustively at low order. I only had a quick look at order 13, but it looks like a similar thing happens.

Which is a roundabout way of saying I don't know if the 1486+ 168 violation magmas mace4 generates differ in interesting ways, only that they differ.

[Matthew Bolan]

They all still look like small perturbations of each other, and they look a little bit like an order 9 central groupoid that has been blown up somehow (not that I can make this precise at all).

[Bruno Le Floch]

Attempt to understand some of the 11-element counterexamples to 1486->168. Consider the $2^{18}$ tables one can get from filling in the following incomplete table with the condition that each empty cell is only allowed to be completed by one of the two values already present in that column. If I didn't mess up these $2^{18}$ magmas obey 1486, and (almost?) all of them violate 168. Here X and Y stand for 9 and 10.

[[0, 0, 0, 1, 1, 1, 2, 2, 2,  ,  ],
 [3, 3,  , 4, 4, 4, 5, 5, 5, 3,  ],
 [6, 6, 0, 7, 7, 7,  , 8, 8, 6, 8],
 [0, 0, 0, 1, 1, 1,  , X, X,  , X],
 [3, 3,  , 4, 4, 4, 5, 5, 5, 3,  ],
 [6, 6,  , 7, 7, 7,  , 8, 8, 6, 8],
 [0, 0, 0, 1, 1, 1, 5, X, X,  , X],
 [3, 3,  , 4, 4, 4, 5, 5, 5, 3,  ],
 [Y, Y, Y, 7, 7, 7,  , 8, 8,  , 8],
 [Y, Y, Y, 7, 7, 7,  , 8, 8, 3, 8],
 [0, 0, 0, 1, 1, 1, 2, 2, 2,  , 8]]

This looks very close indeed to a small modification of the order 9 central groupoid, which would be

[[0, 0, 0, 1, 1, 1, 2, 2, 2],
 [3, 3, 3, 4, 4, 4, 5, 5, 5],
 [6, 6, 6, 7, 7, 7, 8, 8, 8],
 [0, 0, 0, 1, 1, 1, 2, 2, 2],
 [3, 3, 3, 4, 4, 4, 5, 5, 5],
 [6, 6, 6, 7, 7, 7, 8, 8, 8],
 [0, 0, 0, 1, 1, 1, 2, 2, 2],
 [3, 3, 3, 4, 4, 4, 5, 5, 5],
 [6, 6, 6, 7, 7, 7, 8, 8, 8]]

[Matthew Bolan]

I also am of the opinion that the 18x18 one in my message seems to be an order 16 central groupoid that has been blown up somehow.

[Douglas McNeil]

2^18 not being so very big, I checked, and can confirm BLF's claim, FWIW.

[Bruno Le Floch]

A natural conjecture, looking just at the orders that you mentioned, is that there are examples with $n^2+2$ elements and with $n^2+n+1$ elements, corresponding to different blow-ups of the order-$n^2$ central groupoid.

[Matthew Bolan]

I thought about that, but I was hesitant to conjecture it as there aren't any of order 3,6 or 7.

[Matthew Bolan]

Also I think saying "the order $n^2$ " central groupoid is wrong, there should be many non-isomorphic central groupoids. Maybe you mean natural central groupoid? Perhaps the reason why there aren't any of orders 3,6,7 is that the natural central groupoids are too nice to blow up somehow.

[Matthew Bolan]

I find 1486 magmas interesting enough that I'd like to keep discussing them, but probably a moderator should move this discussion to another thread for us.

[Vlad Tsyrklevich]

You can do it yourself! Click the 3 buttons on the top right of the comments, and 'Move messages'

[Notification Bot]

11 messages were moved here from #Equational > What are the hardest positive implications for an ATP? by Matthew Bolan.

[Bruno Le Floch]

Yes, sorry, I had in mind the natural central groupoid, I'm getting a bit lost in the terminology there. I wrongly thought that there would be some 3,6,7 element examples of 1486 that just accidentally obeyed 168, but that is wrong of course. So my general conjecture was also too quick, one has to add $n\geq 3$.

Here is a construction of a 1486 magma with $n^2+2$ elements for $n\geq 3$ (actually many of them); I don't have any deep understanding of it. Consider a set $S$ with $n\geq 3$ elements, and choose two distinct elements $0,1\in S$. Let $M = S^2 \cup \{X, Y\}$, equipped with an operation $\diamond$ to be defined. The intuition is that $X$ and $Y$ will often occur in positions of the multiplication table where one may expect $(0,1)$ and $(1,0)$, respectively. There is probably a better way to present the construction that makes this idea more manifest.

First, we define $(a,b)\diamond(c,d)$ when $\{c,d\}\neq\{0,1\}$ as follows,

$$\begin{aligned} (a,b) \diamond (c,d) & = (b,c) \text{ if } \{c,d\}\neq\{0,1\} \text{ and } \{b,c\}\neq\{0,1\} , \\ (a,1) \diamond (0,d) & = (1,0) \text{ if } a,d\neq 1 , \\ (1,1) \diamond (0,d) & = Y \text{ if } d\neq 1 , \\ (a,0) \diamond (1,d) & = X \text{ if } a,d\neq 0 , \\ (0,0) \diamond (1,d) & = (0,1) \text{ if } d\neq 0 . \end{aligned}$$

We also define left multiplication by $X$ and $Y$ to coincide with left multiplication by $(1,1)$ and $(0,0)$ respectively, when acting on the same set of $(c,d)$, namely

$$\begin{aligned} X \diamond (c,d) & = (1,c) \text{ if } c\not\in\{0,1\} , \\ X \diamond (1,d) & = (1,1) \text{ if } d\neq 0 , \\ X \diamond (0,d) & = Y \text{ if } d\neq 1 , \\ Y \diamond (c,d) & = (0,c) \text{ if } \{c,d\}\neq\{0,1\} . \end{aligned}$$

This fully specifies all multiplications $x\diamond y$ for $y\neq(0,1),(1,0),X,Y$. The remaining four columns of the multiplication table will be filled in shortly.

Observe that $(a,b)^{\diamond 2} = (b,a)$ except for $(0,1)$ and $(1,0)$ whose squares will be decided later on. We will choose their squares as well as $X^{\diamond 2},Y^{\diamond 2}$ such as to avoid introducing further squares, so that the set of squares in $M$ remains $S^2\setminus\{(0,1),(1,0)\}$. This means that we already know all of the sets $l_x = \{x\diamond(z\diamond z),z\in M\}$:

$$\begin{aligned} l_{(1,1)} = l_X & = \bigl(\{1\}\times (S\setminus\{0\})\bigr) \cup\{Y\} , \\ l_{(0,0)} = l_Y & = \{0\}\times S , \\ l_{(a,0)} & = \bigl(\{0\} \times (S\setminus\{1\})\bigr) \cup\{X\} , \quad \text{ if } a\neq 0 , \\ l_{(a,1)} & = \{1\}\times S \text{ if } a\neq 1 , \\ l_{(a,b)} & = \{b\}\times S \text{ if } b\not\in\{0,1\} . \end{aligned}$$

We also know the cosets $Mx=\{y\diamond x,y\in M\}$ for all $x$ except $(0,1),(1,0),X,Y$:

$$\begin{aligned} M(0,d) & = \{Y\} \cup (S\times\{0\}) \text{ if } d\neq 1 , \\ M(1,d) & = \{X\} \cup (S\times\{1\}) \text{ if } d\neq 0 , \\ M(c,d) & = S\times\{c\} \text{ if } c\not\in\{0,1\} . \end{aligned}$$

The equation 1486 $x=(y\diamond x)\diamond(x\diamond(z\diamond z))$ imposes that any product in $(Mx)\diamond(l_x)$ be equal to $x$. For the most part this is a consistency check (which I performed now), but it also gives us some new entries:

$$\begin{aligned} Y \diamond (0,1) & = (0,0) , \\ (a,0) \diamond (0,1) & = (0,0) \quad a\in S , \\ (a,b) \diamond (1,0) & = (b,1) \text{ if } a\in S, b\not\in\{0,1\} , \\ (a,b) \diamond X & = (b,0) \text{ if } a\in S, b\not\in\{0,1\} , \\ X \diamond Y & = (1,1) , \\ (a,1) \diamond Y & = (1,1) \quad a\in S . \end{aligned}$$

At this stage I checked the equation 1486 for all $x$ except the four values $(0,1),(1,0),X,Y$.

We continue the process: applying the equation we successively (some of the later lines arise due to earlier ones here) get

$$\begin{aligned} (0,0) \diamond (1,0) & = (0,1) , \\ (a,1) \diamond X & = (1,0) \text{ if } a\neq 1 , \\ (a,0) \diamond Y & = X , \text{ if } a\neq 0 , \\ (1,1) \diamond (0,1) & = Y , \\ X \diamond (0,1) & = Y , \\ Y \diamond (1,0) & = (0,1) . \end{aligned}$$

Together with the previous bunch of equations, this gives some elements in the cosets $Mx$ for $x=(0,1),(1,0),X,Y$. On the other hand, these cosets may not be too big because any product $(Mx)\diamond(l_x)$ has to be equal to $x$ and we have already filled most of the multiplication table. By inspection, we find the lower and upper bounds on these cosets coincide and are

$$\begin{aligned} M(0,1) & = \{Y,(0,0)\} , \\ M(1,0) & = (S\setminus\{1\})\times \{1\} , \\ MX & = (S\setminus\{0\})\times\{0\} , \\ MY & = \{X,(1,1)\} . \end{aligned}$$

We must fix the remaining entries $x\diamond y$ within these allowed values, and with the added condition that squares of $(0,1),(1,0),X,Y$ have to be in the set of squares that we prescribed in the first place. In particular, $(0,1)\diamond(0,1)$ has to be in the two-element set $M(0,1)$, and it cannot be $Y$ because that is not supposed to be a square. Thus $(0,1)\diamond(0,1)=(0,0)$. Continuing in this way we find

$$\begin{aligned} & (0,1) \diamond (0,1) = (0,0) , \qquad (1,0) \diamond (1,0) \in (S\setminus\{0,1\})\times\{1\} , \\ & X \diamond X \in (S\setminus\{0,1\})\times\{0\} , \qquad Y \diamond Y = (1,1) , \end{aligned}$$

with $(n-2)^2$ choices. The non-squares have slightly fewer constraints and should be chosen as

$$\begin{aligned} (a,1) \diamond (0,1) & \in \{Y,(0,0)\} \text{ for } a\neq 1 , \\ (a,b) \diamond (0,1) & \in \{Y,(0,0)\} \text{ for } a\in S, b\not\in\{0,1\} , \\ (a,0) \diamond (1,0) & \in (S\setminus\{1\})\times \{1\} \text{ for } a\neq 0 , \\ (a,1) \diamond (1,0) & \in (S\setminus\{1\})\times \{1\} \text{ for } a\in S , \\ X \diamond (1,0) & \in (S\setminus\{1\})\times \{1\} , \\ (a,0)\diamond X & \in (S\setminus\{0\})\times\{0\} \text{ for } a\in S , \\ (1,1)\diamond X & \in (S\setminus\{0\})\times\{0\} , \\ Y\diamond X & \in (S\setminus\{0\})\times\{0\} , \\ (0,0)\diamond Y & \in \{X,(1,1)\} , \\ (a,b)\diamond Y & \in \{X,(1,1)\} \text{ for } b\neq 0,1 . \end{aligned}$$

I think this amounts to $2^{n^2-2} (n-2)^2 (n-1)^{3n+2}$ magmas. But I think this is far from all magmas of that size obeying 1486. I also suspect that for large enough $n$ there are ways to add more than two elements, basically by picking several pairs instead of just $0,1\in S$.

[Jose Brox]

Matthew Bolan ha dicho:

I'd really like to find settings for Mace4 (or even Vampire) which let them find the degree 21 1486 magma as efficiently as possible.

How much time did you need to find the size 21 model?

I have run some experiments with Mace4, changing search parameters and choosing between 168 and its two equivalent identities. The best combination seems to be selection_order 2, selection_measure 1, skolems_last checked, against the original 168. With this setting, a model of size 13 was found in 1439s (CPU time). I started a search in size 21 with these parameters, it has run already for 3h without finding any.

Of course, the search could be shorter if we know or impose some other property of the model. For now I'm just using brute force.

[Matthew Bolan]

It took my copy of vampire around an hour and a half.

[Matthew Bolan]

Let me amend that statement. To find any order 21 model took my vampire just shy of 900 seconds. To find the model which refuted the remaining implications is what took an hour and a half.

[Bruno Le Floch]

FWIW, the first 37 million (I stopped the run) 11-element example magmas obeying 1486 (no need to impose not(168) since the size is not a square) have exactly 7 distinct squares, consistent with changing two of the squares in a 9-element central groupoid.

[Jose Brox]

Bruno Le Floch ha dicho:

no need to impose not(168) since the size is not a square)

Yeah, I noticed that later (just me being dumb on autopilot). Probably it doesn't affect the time much, but I'm running it again without anti 168.

[Jose Brox]

Matthew Bolan ha dicho:

To find the model which refuted the remaining implications is what took an hour and a half.

Can you please repeat which those implications are?

[Matthew Bolan]

3877

[Matthew Bolan]

fof(eq1486, axiom,
X=m(m(Y,X),m(X,m(Z,Z)))
).
fof(eq3877, conjecture,
m(X,X)=m(m(Y, m(X,X)),X)
).

[Matthew Bolan]

I ran it with vampire -sa fmb -fmbss 21 1486to3877.p -t 200000

[Bruno Le Floch]

Can you share some order 13, 18, 21 examples of 1486 magmas? If we have more examples of modified central groupoids we may be better able to understand the modification. I'm having trouble getting them with mace4 runs, I'm probably just being impatient.

[Matthew Bolan]

All the ones I know were shared here: https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Austin.20pairs/near/484348920

[Matthew Bolan]

Oh, and this one of course: https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Austin.20pairs/near/484819108

[Matthew Bolan]

I've only managed to find examples of degree > 13 with Vampire. I think I've only found the degree 13 examples with Mace4 in the presence of some additional assumptions.

[Matthew Bolan]

And there may well be examples of orders between 13 and 21 that I didn't find, my search was not exhaustive for these orders.

[Matthew Bolan]

There also might be more for 1486 (or its dual) in the github from Daniel Weber's original vampire run.

[Jose Brox]

Matthew Bolan ha dicho:

3877

Nothing, Mace4 has run for 9000s in one configuration and for 5000s in another without finding any 1486 counterexamples to 3877 of size 21 :melting_face: .

[Bruno Le Floch]

An observation about all 1486 magmas that have been shared, and a also satisfied by a partial construction that I haven't finished: the sets $\ell_x = \{x\diamond(z\diamond z)\mid z\in M\}$ have the same size for all $x\in M$: size $3$ for magmas with $9,11,13$ elements, and size $4$ for magmas with $16,18,21$ elements.

Note that if $x,y\in\ell_z$ then by equation 1486 we have $z = (?\diamond z)\diamond x\in M\diamond x$ and likewise $z\in M\diamond y$. Then equation 1486 tells us $x = z\diamond(x\diamond w^{\diamond 2})$ and $y = z\diamond(y\diamond v^{\diamond 2})$ for any $v,w$, so we have $\ell_x\cap\ell_y=\emptyset$, namely the union $\bigcup_{x\in\ell_z}\ell_x$ is a disjoint union. In particular, if my observation about the sizes of $\ell_z$ is correct, then $|\ell_z|^2\leq |M|$.

Another easy result is that for any $z$, the disjoint union $\bigcup_{x\in\ell_z}\ell_x = \{(z\diamond w^2)\diamond v^2\mid v,w\in M\}$ contains all squares. Indeed, take $v=w^2$ and see that $(z\diamond w^2)\diamond v^2 = (z\diamond w^2)\diamond(w^2\diamond(w\diamond w)) = w^2$ by the equation.

I suspect there should be a way to get the equality of all $|\ell_z|$ this using a linear algebra argument similar to the one for 168, but I didn't manage.