Minimal countermodel to order 4 equations

Stream: Equational

[Jose Brox]

While playing with higher equations in an attempt to better understand 677, I have stumbled upon a model of size 17 that doesn't satisfy any of our nontrivial equations [2, 4694].

Driven by curiosity, I have determined the minimum size that a countermodel "to all our project" needs to have: it is 5 (so low!). With sizes 2-4 Vampire-SAT finds a refutation [EDITED: this was mistaken, smallest size is 3, see below], while with size 5 it finds the model
[[3,2,1,2,4], [4,0,3,0,4], [1,3,2,1,4], [4,0,1,1,2], [2,2,4,1,3]]

https://teorth.github.io/equational_theories/fme/?magma=%5B%5B3%2C2%2C1%2C2%2C4%5D%2C%0A%5B4%2C0%2C3%2C0%2C4%5D%2C%0A%5B1%2C3%2C2%2C1%2C4%5D%2C%0A%5B4%2C0%2C1%2C1%2C2%5D%2C%0A%5B2%2C2%2C4%2C1%2C3%5D%5D%0A

(Mace4 is of no use here, it gets stalled already at size 3.)

Next I have checked "how good" the counterexample is, i.e., up to which number we can go up without finding an equation that satisfies the model. The first satisfied equation is 265437 x = (x * x) * ((x * (x * x)) * (x * x)) :scream:

Curiously, if we change the last element of the model to 4*4 = 2 then we get exactly the same result, while if we change it to4*4 = 1 or 4*4=4 then the first satisfied equation is "only" 19604, x = (x * x) * ((x * (x * x)) * x) (these last computations of model un/satisfaction are made with a Python script produced originally by @Bruno Le Floch for the HN subproject and later modified by me, I hope they are right).

[Jose Brox]

Jose Brox ha dicho:

a countermodel "to all our project"

In order to find it, I have asked Graphiti for the list of maximal (nontrivial) elements in the implication graph (i.e., those having distance 1 to equation 1 $x=x$), of which there are 57, then looked for countermodels to all of them simultaneously, of fixed sizes.

The list of "sinks" of the digraph is
[47, 99, 151, 203, 255, 411, 614, 817, 1020, 1223, 1426, 1629, 1832, 2035, 2238, 2441, 2644, 2847, 3050, 3253, 3456, 3659, 3862, 4065, 4268, 4269, 4270, 4272, 4273, 4275, 4276, 4283, 4284, 4290, 4291, 4293, 4314, 4320, 4321, 4343, 4380, 4583, 4584, 4585, 4587, 4588, 4590, 4591, 4598, 4599, 4605, 4606, 4608, 4629, 4635, 4636, 4658]

[Jose Brox]

Jose Brox ha dicho:

the minimum size that a countermodel "to all our project" needs to have: it is 5 (so low!)

This leads to the question: could this fact be theoretically predicted? (We have order 4, up to 4 variables, etc.). If so, can then we predict how further up the best possible model of size 5 can get us?

[Douglas McNeil]

What about this size 3 magma?

A while back I was looking at "outlaws", magmas which were maximally disobedient, but I thought they'd be rarer than they are. :sweat_smile:

Your idea of tracking how many equations (maybe by dimensions of variable number and order) a counterexample violates may make it more interesting, because then we have something to optimize.

[Terence Tao]

This reminds me of the time Galois theory was used to create "the world's ugliest music". https://www.youtube.com/watch?v=RENk9PK06AQ

[Matthew Bolan]

I was reminded of the whole business with the smallest number not appearing in the OEIS

[Jose Brox]

Douglas McNeil ha dicho:

What about this size 3 magma?

:scream: :scream: Thanks! This shows that I don't know how to use Vampire well yet (it seems that the problem was with the name of the constants I used when imposing size 3 or less).

Douglas McNeil ha dicho:

Your idea of tracking how many equations (maybe by dimensions of variable number and order) a counterexample violates may make it more interesting, because then we have something to optimize.

Your "contender" has an "undefeated streak" of 51174, since the first equation it satisfies is 51176 x * x = ((x * x) * (x * x)) * x, and a "winning percentage"( yield?) of 99.9892% over the first million "combats" (computed in 4min with the Python script).

The size 5 contender in the first message has a winning percentage of 99.9997% over the first million combats (i.e., only 2 nontrivial equations satisfy it!).

[Bruno Le Floch]

Counterexamples to one-variable equations are counterexamples to all multi-variable equations of the same shape. So the first equation satisfied by a given magma will always be univariate, or bivariate and have the same shape on the LHS and RHS (so that replacing y by x would give a tautological equation). For instance, it's very easy to make a counterexample to all equations of the form x=RHS: just take 0*0=1, and then the counterexample will be x=y=...=0.

Conversely, every finite magma obeys some equation obtained by iterating the squaring map $S\colon x\mapsto x\diamond x$: the tuple $(S^k x)_{x\in M}$ can take finitely many values, so there exist $k\neq l$ such that $S^k x=S^l x$ for all $x\in M$. This gives a pretty terrible bound on the equation size, admittedly.

[Jose Brox]

Bruno Le Floch ha dicho:

so there exist k!=l such that S^kx=S^lx for all x∈M

They actually are $k_x$ and $l_x$, but then we can the lcms (and make the exponents even larger :big_smile:).

To get a better bound we'd need to work with nested sequences of the $L,R$ operators.

[Bruno Le Floch]

I initially phrased the argument using lcm, but I finally opted to take the whole tuple $(S^k0,S^k1,\dots)$ of $k$-th squares of all elements in the magma, and notice that this whole tuple can take at most $|M|^{|M|}$ values so it must repeat as a whole. For the same reason the magma obeys an equation with any number $m$ of distinct variables that you like. List in some order all expressions $\mathrm{expr}_k(x_1,\dots,x_m)$ that uses all $m$ variables, so something like $\mathrm{expr}_1(x_1,x_2)=x_1\diamond x_2$, ..., $\mathrm{expr}_6(x_1,x_2)=x_2\diamond(x_1\diamond x_1)$, etc. Then consider for each $k$ the tuple $(\mathrm{expr}_k(x_1,\dots,x_m))_{x_1\in M,\dots,x_m\in M}$. The tuple can take at most $|M|^{|M|^m}$ values, so among the first $|M|^{|M|^m}+1$ expressions, two of them coincide, namely we found some $m$-variable equation satisfied by the magma.

[Jose Brox]

Bruno Le Floch ha dicho:

but I finally opted to take the whole tuple

Oh right, those are tuples, not sets! I see the parentheses now :+1: