Shrinking the size-232 magma for law 1518 to size 15

Stream: Equational

[Bruno Le Floch]

Some time back, at #Equational > Austin pairs @ 💬, @Terence Tao found a 522-element magma satisfying law 1518 x = (y◇y) ◇ (x◇(y◇x)) but not 47 x = x◇(x◇(x◇x)) and some other single variable laws (817, …), then he reduced it to size 232, small enough for Lean verification.

In a finite magma satisfying 1518, the squaring map S:x ↦ x◇x is bijective and left multiplications are bijective. Under these conditions, the various single-variable laws of interest (47, 817, …) are all equivalent to each other and to S(S(S(x))) = x so clearly the cycle lengths of S are important. Playing around with partial models I found that many of them were consistent with S being an automorphism. Lo and behold, the very simple Mace4 script

assign(selection_measure, 1).
formulas(sos).
x=(y*y)*(x*(y*x)).
(x*y)*(x*y)=(x*x)*(y*y).
0*(0*(0*0))!=0.
end_of_list.

provides a 15-element magma that nicely replaces the previous huge magma, refuting 1518→47 and friends. A separate mace4 run with no conditions shows that there is no countermodel of 1518→47 of size ≤13, so size 15 is close to optimal.

[Matthew Bolan]

Does that now make the order $65$ model for $1076 \to 2294$ the current largest used finite magma in the project?

[Vlad Tsyrklevich]

Great find! Shall we replace the size 232 magma in the repo with this one? It seems like a reasonable thing to do--I don't know if we care to replace every finite counterexample magma with smaller versions but replacing a computationally intensive one seems like a definite improvement.

[Bruno Le Floch]

@Vlad Tsyrklevich I made a pull request shortly before posting here, sorry I forgot to mention it. It is now merged to main.

@Matthew Bolan Yes, the next biggest is the one you mention. It seems to come from some cohomological construction so there is some chance that it is optimal, probably not worth seeking a smaller example.

[Bruno Le Floch]

Let me document here how I ruled out models of sizes ≤13 for not(1518→47). It's not a naive Mace4 run, which would be too slow. We are seeking a finite countermodel so it is useful to work out consequences of 1518+finiteness. Law 1518 implies $L_{S(y)}$ surjective, hence bijective (by finiteness). Law 1518 also implies $S(x)\diamond x = S(x)$ so if $S(x)=S(y)$ we find $S(x)\diamond x=S(x)=S(y)=S(y)\diamond y=S(x)\diamond y$ which by bijectivity of $L_{S(x)}$ yields $x=y$. Therefore, $S$ is injective hence bijective. Since every element is a square, bijectivity of left multiplications $L_{S(y)}$ becomes bijectivity of all left multiplications.

Here is a Mace4 input file that takes around a minute to rule out sizes up to 12 and an hour for size 13, presumably 5 days for size 14 given the observed scaling.

assign(selection_order, 2).
assign(selection_measure, 1).
formulas(sos).
x=(y*y)*(x*(y*x)).
x*y=x*z -> y=z.
S(x) = x*x.
S(y)=S(z) -> y=z.
end_of_list.
formulas(goals).
0*(0*(0*0))=0.
end_of_list.

[Jose Brox]

Since $L_{S(y)}$ is bijective, we can substitute $x\to (y*y)*x$ then cancel $y*y$ on the left to get the additional Austin consequence

x = ((y*y)*x)*(y*((y*y)*x)).

Putting this one together with the others you mentioned, we get size 12 in 2.5s and size 13 in 94s. Size 14 is running right now :)

[Jose Brox]

Size 14 exhausted in 6700s (less than 2h).

This confirms that @Bruno Le Floch's model for 1518 anti 47 has minimum size 15.

Here is the Mace4 script for completeness:

%with 2,1,no
%size 11: 0.1s
%size 12: 2.5s
%size 13: 94s
%size 14: 6700s

formulas(sos).
x = (y * y) * (x * (y * x)) #label(1518).
x = ((y*y)*x)*(y*((y*y)*x)) #label(1518finiteconsequence).
x*y = x*z -> y=z #label(leftmultinjective).
x*x = y*y -> x=y  #label(squaringinjective).
end_of_list.
formulas(goals).
x=x*(x*(x*x)) #label(47).
end_of_list.

[Bruno Le Floch]

For what it's worth, after around one CPU-week, Jose got a list of all countermodels of size 15. There are 6 non-isomorphic countermodels. For all of them the squaring map has a 12-cycle and either a 3-cycle or three fixed points. These last three elements always form a submagma N⊂M. For all six countermodels there is a bijection f of order 12 (the order-12 cycle of the squaring map, plus an order-3 cyclic permutation of the last three elements) such that f(x◇y)=f(x)◇f(y) for all pairs (x,y)∉N². In particular all of them have at least ℤ/4ℤ symmetry.

[Bruno Le Floch]

For reference, here is a list of all of the large finite counterexamples (size ≥14) we use (in files with names equational_theories/Generated/All4x4Tables/Refutation*.lean). I've indicated "(cohom)" for those obtained by the cohomological method, namely linear extensions of base models (themselves typically linear).

• A quasigroup of size 65 (cohom) that satisfies E1076 and refutes implications to E2294, E4435.

• A left quasigroup of size 36 (cohom) that satisfies E1, E411, E503, and no other law of order up to 4. The left quasigroup obtained by changing ◇ to its left-division operation (cohom) satisfies E1, E411, E476, E3862 instead, and no other law of order up to 4.

• A quasigroup of size 35 (cohom) that satisfies E1516 and a few single-variable laws, and is used to refute the implication to E1489.

• A magma of size 32 satisfying E1485 but not E151, E1427, E1429, E2087, E2124, E3456, E3862. Obtained by the twisting semigroup technique, from 5 copies of the NAND magma.

• A quasigroup of size 25 (cohom) refuting the implication from E1110 to E1629. (It was the second cohomological construction, after an E879 magma of size 12.)

• A magma of size 24 refuting the implication from E854 to E1045. A magma of size 21 refuting the implication from E854 to E3316, E3925. A magma of size 19 refuting the implication from E854 to E413.

• A magma of size 21 refuting the implication from E1486 to E3862. Another magma of size 21 refuting the implications from E1486 to E151 and many others. Another one refuting the implications from E2126 to E151 and many others. Even though E1486 and E2126 are dual to each other, the magmas being used there are not opposite magmas. As I remember it, size 21 models of E1486 are very flexible.

• A magma of size 17 whose left and right cosets all have 10 elements, satisfying E3545 and its obvious consequences but no other law of order ≤4. Also its opposite magma. This appears to be the largest found purely by an ATP, specifically Vampire: see https://github.com/teorth/equational_theories/commit/5e30571e998e54cf101a8fe5f43afb501ad91e27

• The left quasigroup of size 15 discussed here (with right cosets of size 5) refuting implications from E1518 to E47 etc.

[Bruno Le Floch]

Schematically, the largest models are cohomological models and the E1485 twisted semigroup model that are human-understandable, then some complicated models of the flexible laws E854 and E1486 obtained by a combination of humans and ATPs, and then some models of sizes 17 and 15 found by ATPs.

[Matthew Bolan]

A small comment, but the order 12 refutation of E879 to E4065 at #Equational > Austin pairs @ 💬 is certainly a cohomological construction, and predates the example refuting E1110 to E1629

[Bruno Le Floch]

Thanks for the correction! The E879 came up 12 hours before the E1110 model, I hadn't scrolled up high enough in the conversation.

[Bruno Le Floch]

The 17-element magma obeying E3545 and its consequences but no other law is confusing me, because it was found by Vampire, but it is not of minimal size. There is actually a 13-element magma with the same properties found instantaneously by Mace4, and for individual implications 12 elements is enough.

Mace4 code for 3545

assign(selection_measure, 1).
formulas(sos).
x*y=y*((x*x)*x) #label(3545).
end_of_list.
formulas(goals).
x*x=(x*(x*x))*x #label(3862).
x=(x*(x*x))*(x*x) #label(1832).
end_of_list.

[Bruno Le Floch]

The 21-element models of E1486 are only useful to refute E3862, E3877, E3918, E3955, E3993 (which all imply E3862). For all other non-implications from E1486 there is a 11-element countermodel.

EDIT: A 10min Mace4 run shows that there is no counterexample to the implication from E1486 to E3862 of size ≤14.

[Matthew Bolan]

My recollection is that a lot of the larger vampire found models used to come from a large automated run Daniel Weber did, which used a modification of what Vampire does in its casc_sat mode, with parts not relevant for our case removed. That didn't try the sizes in order (I think it tries sizes 1-11, and then starts checking sizes more like 21), and would time out sizes after some time, so it very well could have missed a size 12 model.

[Bruno Le Floch]

Ah, I think this discussion leads to a precise version of a question that was asked at some point, of "how many finite magmas do we need for all finite anti-implications". For each E, what is the smallest magma satisfying E and that violates every E' (up to order 4) that isn't implied by E in finite models. For E3545 my Mace4 runs show that the smallest such magma has size 13. For E4 (projection) or E895 (Boolean group) it has size 2.

[Bruno Le Floch]

For lack of a better name, let me call "N-perfect E countermodel" a magma satisfying E (and its consequences of course), and no other law of order up to N. Here are the laws for which we know the minimal-size one. I only include lowest representatives of equivalence classes and duals.

• 4-perfect E1 countermodel: minimum size 3;

• ∞-perfect E2 countermodel: trivial magma since it has to obey E2 and every law;

• 4-perfect E3 countermodel: minimum size 3;

• ∞-perfect E4 countermodel: x◇y=x on a 2-element carrier;

• 4-perfect E8 countermodel: minimum size 3

• 4-perfect E9 countermodel: minimum size 4, but I only checked by hand that the lists given by the Finite Magma Explorer for this magma and Equation Explorer for law 9 were the same so it's getting tedious and error-prone.

• 4-perfect E879 countermodel: the size 12 cohomological magma showing that E879 does not imply E4065 is actually 4-perfect, and sizes ≤11 are ruled out by a 10h Mace4 run imposing bijectivity of left multiplications.

• ∞-perfect E895 countermodel: (ℤ/2ℤ,+).

• 4-perfect E1518 countermodel: five models of size 15, in Jose's list above they are the first four models and the last one.

• 4-perfect E3545 countermodel: size 13 is minimal, basically one of the non-implications requires a size 12 model, which is almost 4-perfect except for that it obeys one law that it shouldn't; adding one more element fixes that.

I should not explore this further, but at least the question seems to make sense and be solvable for many laws.