Collecting interesting finite magmas

Stream: Equational

[Terence Tao]

It was pointed out in equational#175 that the finite magma (Z/6Z,+) could be used to rule out any implication in which the hypothesis has each variable occur the same number of times on both sides, but the conclusion does not. This magma is not in the list of magmas of order up to 4 that we are already using to generate anti-implications, and scaling up to magmas of order 5 is computationally infeasible. So perhaps what we should do is collect a list of "interesting" finite magmas of order larger than 4 that we could place in a text file that an automated script could run to prune the list of outstanding implications. The first addition to this list would be (Z/6Z,+). Are there any other small finite magmas that would plausibly be useful for anti-implications? For instance, finite examples of central groupoids (Equation168) would be interesting additions. I have created equational#180 for this, but in the meantime we could list interesting examples of finite magmas here.

[Terence Tao]

The commutative magmas of order 5 might also be brute forceable especially if one quotients out by isomorphism

[Terence Tao]

Another class of interest might be random magmas of order 5 that are idempotent, x = x * x, as these are more likely to obey certain classes of laws that involve idempotence than a completely random magma, and so would eliminate a different demographic of implications than the completely random ones.

[Nicholas Carlini]

Enumerating all 5x5 idempotent magmas might be beyond what my code can do currently (there are 5^20 idempotent magmas, 20,000x the size of all 4x4 magmas). I don't think it's completely beyond reach though: I have ideas for how to make my script at least 10x faster, maybe 100x. But not yet. (Random search, as you suggest, could still be interesting.)

What is definitely possible to start with is enumerating all commutative magmas. That's just 5^15, only 7 times more than the number of 4x4 magmas. Going from all 3x3 magmas to all 4x4 magmas increased the number of refutations from 9.7m to 13.8m, so I have hope going to 5x5 will bring some nice gains.

[Joachim Breitner]

Could your took also be used to investigate a specific 6x6 magma, running it on all equations? It seems that Terry would like to include specific magmas. So maybe your tool could have a variant where you give it one specific table?

[Joachim Breitner]

It looks my rather crude lean command for exploring magma can handle (Z/6Z,+), with

calculate_facts (Fin 6) (⟨fun x y => x + y⟩) by decide

Will add this to SmallMagmas.lean.

[Joachim Breitner]

https://github.com/teorth/equational_theories/pull/189. Did not check if it contains any new antiimplications.

[Nicholas Carlini]

I checked previously and it will not, two of the polynomials from the FinitePoly refutation cover this one

[Joachim Breitner]

Hmm, ok. Still nice to have it in the small examples files, given that it’s a “natural” magma

[Terence Tao]

Another natural magma class are the vector spaces F_2^n over the field of two elements, with the + operation. Such spaces obey 1571 (the law of an abelian group of exponent 2) and a bunch of other related laws, but fail others. Right now there are 579 implications out of 1571 that are open, so hopefully this class will close off a bunch of them, and maybe some other implications as well.

[Terence Tao]

Another example is the 9-element "non-natural central groupoid" A_2 on Fin 3 × Fin 3 from Knuth's paper https://www.sciencedirect.com/science/article/pii/S0021980070800321?ref=cra_js_challenge&fr=RR-1 , which should create some antiimplications from 168. First define a preliminary operation * on Fin 3 by setting x * 0 = 0, 0 * x = x, 1 * 1 = 2 * 1 = 2, 1 * 2 = 2 * 2 = 1. Then (a,b) ◇ (c,d) is defined to equal

• (b,c) if c, d are non-zero;
• (b,e) if b*e=c is non-zero and d is zero;
• (a*b,0) if c=0

If I transcribed Knuth's example correctly, this should obey 168, but fail some of the 42 unknown implications from 168. Knuth's paper has a few other 9-element magmas somewhat like this, which between them (and the positive results in that paper) should resolve all the remaining implications, I think. I created equational#266 to execute this.

[Zoltan A. Kocsis (Z.A.K.)]

I'd be happy to try this but I can't quite parse the definition given here.

What is (0,0) ◇ (1,0)?

The way I read what you wrote, since d=0 and c=1 is non-zero, I should use the second case, b=0 so the result should be (0,e) for some e such that 0*e=1. But 0*e=0 holds always by the first clause in the preliminary definition. Where am I going wrong?

[Terence Tao]

Oops, I had a typo, it should be x*0=0 rather than 0*x=0. Fixed now.

[Zoltan A. Kocsis (Z.A.K.)]

Thanks! Then we also need cases for 0*1 and 0*2, right? Otherwise, * is partially defined.

[Terence Tao]

I just checked Knuth's paper and there was a missing equation 0*x=x as well that I had forgotten to add. Hopefully now it is complete.

[Zoltan A. Kocsis (Z.A.K.)]

Okay, so the operation table of the preliminary operation is

 *|0 1 2
--+-----
0 |0 1 2
1 |0 2 1
2 |0 2 1

(or the other way around ;)

[Zoltan A. Kocsis (Z.A.K.)]

Is there a missing clause for diamond as well?

E.g. what would be, say ab ◇ 01? Then c=0, d=1. The second and third clause do not apply. The first case cannot apply either since then we'd have ab ◇ 01 = b0, but then we'd have

1. 01 ◇ 10 = 12 since we're in case 2, b=1, c=1 and 1*2=1.
2. 10 ◇ 10 = 01 since we're in case 2, b=0, c=1 and 0*1=1,
3. 12 ◇ 01 = 20 by the above.
4. This would contradict Eqn168: x = (y ◇ x) ◇ (x ◇ z) for x=z=10, y=01, since then (01 ◇ 10) ◇ (10 ◇ 10)=12 ◇ 01=20 is not 10.

Sorry if the missing case follows easily from the paper, but I have a bit of trouble even finding the relevant section there, and you might know it off-hand.

[Terence Tao]

The law is equation (6) in the paper (as well as the discussion of the A_2 matrix on page 386). I see I made yet another typo: the final clause should be just c=0, not c=d=0, will edit now.

[Zoltan A. Kocsis (Z.A.K.)]

Yeah, that was my assumption, just wanted to double-check. Thanks!

[Zoltan A. Kocsis (Z.A.K.)]

Some preliminary results: I generated a multiplication table for $A_2$ (it indeed satisfies 168). Adding it to All4x4Tables settles 190 additional anti-implications. I've not yet checked which ones of the form 168=>X it refutes.

[Terence Tao]

In case $A_2$ does not resolve all implications, Knuth has six central groupoids $A_1,\dots,A_6$ of order 9. They are represented on pages 385-386 as 9 x 9 matrices with entries 0, 1. The rule is that i ◇ j = k if the (i,k) and (k,j) entries of $A$ are both equal to 1 (the matrices are designed so this uniquely defines k from i, j).

[Terence Tao]

$A_1$ is a "natural central groupoid" and probably won't eliminate any further equations, if the discussion in Section 5 is any guide.

[Bhavik Mehta]

I have a formalisation of the free Central groupoid from later in that paper, which does resolve all the remaining implications from 168. It's currently all in mathlib language and notation, I'm working on converting it.

[Zoltan A. Kocsis (Z.A.K.)]

Very nice (I was a bit behind on this, due to several other tasks involving All4x4Tables)!
I have a construction of $A_2$ itself in Lean, with a proof of isomorphism to its Fin 9-based multiplication table, but I'm not quite sure what to do with it or where to put it.

[Zoltan A. Kocsis (Z.A.K.)]

(never mind, misread the comment about mathlib)

[Bhavik Mehta]

That's the plan right now, yeah

[Sebastian Luther]

Since there is interest in small magmas for equations: Some days back I brute forced small magmas and one side product was this log showing the size of the smallest magma for each equation (if one exists with N<=5): https://gist.github.com/few/f47af9e3d94c411a638f07ce1cf8727d

[Terence Tao]

Nice! I've added it to our (still very modest) data folder (and started a list in README to begin documenting this data).