854

Stream: Equational

[Terence Tao]

This is a new thread to discuss the law 854 x = x ◇ ((y ◇ z) ◇ (x ◇ z)), which was previously discussed here. It has five open implications Graphiti, to 413 x = x ◇ (x ◇ (x ◇ (y ◇ x))), 1045 x = x ◇ ((y ◇ (y ◇ x)) ◇ x), 1055 x = x ◇ ((y ◇ (z ◇ x)) ◇ x), 3316 x ◇ y = x ◇ (y ◇ (x ◇ y)), and 3925 x ◇ y = (x ◇ (y ◇ x)) ◇ y. So understanding this equation would resolve 10 outstanding implications. Remark: 1055 implies 1045 as a special case, but otherwise the open consequents are unrelated.

It may be worth introducing the set E of pairs (x,y) with x ◇ y = x. The 854 law then asserts that
(x, (y ◇ z) ◇ (x ◇ z)) lies in E for all x, y, z. So one expects E to be somewhat "large". Note that if (y,z), (x,z), (y,x) all lie in E, then (x,y) must also lie in E. That is to say, E is symmetric when restricted to any column {x: (x,z) ∈ E} of E.

Immunities:

• (L) Implication is true for linear models (even noncommutative ones)
• Implication is true assuming the reflexive axiom x ◇ x = x, even permitting three exceptions.

Examples:

• Left-absorptive magmas x ◇ y = x (i.e., every pair lies in E).
• A sporadic 12-element magma

Equation 10 x = x ◇ (y ◇ x) may play a role. It is not implied by 854, nor does it imply 854; but it does imply all of the open consequents of 854. The sporadic order 12 magma obeys 10 with the single exception 0 ◇ (2 ◇ 0) ≠ 0.

The sporadic magma was used to resolve three other implications from 854, so this is evidence that the finite magma approach may continue to be fruitful here.

[Daniel Weber]

Some rules for 854 from the partial greedy ruleset:

• If $x \diamond y = y$ then $y = x$
• $(x \diamond y) \diamond y = x \diamond y$
• $x \diamond x^2 = x$
• If $z \diamond (x \diamond y) = x$ then $(x \diamond y) \diamond x = x \diamond y$
• If $y \diamond (x \diamond y) = x$ then $x = y$
• $x \diamond ((x \diamond y) \diamond x) = x$

[Terence Tao]

One thought: observe that in the multiplication table for the sporadic order 12 magma, 0 only appears in the first row. What this means is that this order 12 magma is actually an order 11 magma (deleting 0) that also obeys 854, with an additional element 0 adjoined.

This suggests a possible route to constructing more finite magmas that could potentially serve as counterexamples. For instance, one could try to adjoin an additional element 13 to the order 12 magma and ask an ATP to try to fill out the new entries of the multiplication table to recover 854 but refute one of the desired claims. Or, more generally, one could search for counterexamples with one element 0 that is deletable (which means that x ◇ y ≠ 0 if x, y ≠ 0 or even two elements 0, ∞ that are sequentially deletable (thus x ◇ y ≠ ∞ if x, y ≠ ∞, and x ◇ y ≠ 0,∞ if x, y ≠ 0,∞).

[Terence Tao]

Separate thought: as mentioned in the first post here, E has a restricted symmetry property. Suppose we assume total symmetry: that is we impose the axiom that if x ◇ y = x, then y ◇ x = y. Does this imply any of the outstanding claims? If so, that is another immunity. Otherwise, it could be a useful axiom to add to find more potential counterexamples.

[Michael Bucko]

Do we have a tptp for this one?

[Douglas McNeil]

In the spirit of reporting our failures as well as our successes, here are things that didn't work:

(1) Starting with the known sporadic 12 and growing a size 13 or higher example, with or without deletability constraints. I mean, it ran, but provided no new counterexamples.

(2) Trying to randomly evolve a counterexample-providing neighbour to the one we know about by emptying cells and using randomized backtracking to fill them in. It's easy to make minor changes, but there are definite "pools" you need to jump out of: you have to raise the percentage of change per step and/or run it for a long time to even get things which start to _look_ different. But it feels more like I'm just random-walking my way around the same fundamental solution than going anywhere.

Eventually the patterns of shifting numbers become kind of hypnotic and you can almost convince yourself you can grok the inner meaning of 854, if only you could put it into words.. anyway, everything which satisfied 854 satisfied everything else . :man_shrugging:

[Terence Tao]

Interesting that you observe that the counterexample is not rigid, that it admits small local perturbations. This is very different from how, say, a group behaves - these are highly symmetric objects, and cannot be locally perturbed. This opens up a whole new type of way to generate constructions, by doing a probabilistic construction that verifies the 854 axiom most of the time, and then some secondary cleanup operation to fix the violations.

On the other hand, your other negative result seems to show that not every 854 magma can be extended by one element. So something special must be true about the order 11 magma that the sporadic order 12 magma is an extension of. Here it is in finite magma explorer. It obeys a ton of laws (Graphiti), including 10 x = x ◇ (y ◇ x), which as noted above implies all the other open laws. In fact Graphiti shows that it obeys the even stronger law 433 x = x ◇ (y ◇ (x ◇ (z ◇ y))), which implies both 10 and 854. Perhaps one could first randomly generate a finite magma obeying 433, then try to extend that by one element in a way that keeps 854 but breaks 10, and hopefully also the other open claims?

[Douglas McNeil]

To be clear, I can extend the 12 to 13 and higher -- I think I got bored around 22 or so -- it's just that they're not interesting, and not merely in the sense they don't falsify anything. The majority of extensions, even when I'm deliberately weighting things to look less like their parent and randomizing fill order and everything possible to make it more exciting, tends to still produce extensions which look more like adding the more "typical" 854s to the edges. By that I mean the ones like this:

 2  2  0  0  2  7  2  0
 2  2  1  1  2  2  2  1
 2  2  2  2  2  2  2  2
 3  3  3  4  3  3  3  3
 2  7  4  4  2  7  7  4
 7  7  5  5  2  7  7  5
 7  2  6  6  7  7  7  6
 7  7  7  7  7  7  7  7

which at this point I think I could do freehand.

[Douglas McNeil]

Incidentally, if my TPTP coding can be trusted (ehh), assuming total symmetry implies all of 413, 1045, 1055, 3316, and 3925, which may mean 854 has even more defences IIUC.

[Terence Tao]

Oh. Then what I said before might not be the smartest thing to try (one could still try it). It is however very strange that you now suggest that there is a highly non-unique way to perform extensions in general, but somehow these extensions are moving the magma away from being counterexamples, rather than towards the counterexamples.

Are you trying to force counterexample behavior into the extension? One could simply try to extend the order 12 magma (say) with two new elements 12, 13 with the 413-contradicting axiom 12 ≠ 12 ◇ (12 ◇ (12 ◇ (13 ◇ 12))) (say) together with 854 and see if it can actually build one. (It may possibly be easier to extend the order 11 magma, as it has more starting structure.)

[Terence Tao]

What do you mean by total symmetry? Symmetry of the magma operation (the commutative law), or symmetry of E?

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

Terence Tao said:

This is very different from how, say, a group behaves - these are highly symmetric objects, and cannot be locally perturbed. This opens up a whole new type of way to generate constructions, by doing a probabilistic construction that verifies the 854 axiom most of the time, and then some secondary cleanup operation to fix the violations.

You can also generate groups by using a probabilistic construction that verifies the group axioms most of the time, then clean up the local violations.

[Douglas McNeil]

Terence Tao said:

What do you mean by total symmetry? Symmetry of the magma operation (the commutative law), or symmetry of E?

I meant ((magma(X, Y) = X) => (magma(Y, X) = Y)))

[Terence Tao]

Ah, so symmetry of E. Okay, so that is indeed another "immunity" this problem has, hmm.

@Zoltan A. Kocsis (Z.A.K.) Heh, you're completely right - for instance I know of this nice work of Gowers and Long in this area. I guess the difference here is that the cleaned up object isn't unique. And yet none of the non-unique perturbations seem to be contradicting the open implications, which is very mysterious to me.

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

The only real issue is that you'll sometimes generate tables that verify all group axioms with extremely high probability, but happen not to be close to the multiplication table of any actual group. But the same thing is not ruled out by malleability observations concerning 854 either.

These "fake groups" happen to be exceedingly rare, but they do exist. Here's an example:
Start with ((Z/2Z)^k,+) with your favorite k (even k=0, I did the construction this way because I was answering a different question at the time, and now don't have time to remove it). Let 0 denote the identity of this group. Define a new structure (H,*) with underlying set H = (Z/2Z)^k U {1..n}, and the operation * defined by the following clauses:

x * y = x + y      if x,y both in (Z/2Z)^k
x * y = y          if x in (Z/2Z)^k and y in {1..n}
x * y = x          if y in (Z/2Z)^k but x in {1..n}
x * x = 0          if x in {1..n}
x * y = min{x,y}   if x,y both in {1..n} and x /= y

If you choose n large enough, then the axioms x*x=0, x*(y*z)=(x*y)*z, x*0=0*x = x will all be satisfied with a
probability arbitrarily close to 1. But you need to edit (add/delete/remove) on the order of O(|H|^2) entries to make the multiplication table of the operation * coincide with that of a group.

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

Note that this does not contradict Gowers-Long, since they need to assume injectivity to make their result work.

[Douglas McNeil]

As for the extensions, what I mean concretely is that you get something like this unless you try very hard:

      9 11  0  9  0  0 11 13  0  0 11 10 11 11 11
      2  4  1  2  1  1 11  1  1  1  9  1  8  9  4
      2  2  7  2  5  4  4  2  4  5  2  5  2  2  2
      9 11  3  9  3  3 11 10  3  3 11 13 11 11 11
      4  4  7  4  7  4  4  4  4  5  4  5  4  4  4
      5  5  7  5  5 14  7  5  4  5  5  5  5  5  5
      2  8 13  2  6 13  4  6 13  6  2  6  2  2  2
      9  7  7  8  7  7  7 10  7  7  7  5  7  7  7
      8  8  7  8  8 13  7  8  4  8  8  8  8  8  8
      9  9  7  9  7  9  9  9  9  5  9  5  9  9  9
      4  2 10  2 10 10  4 10 10 10  9 10 11  9 11
      9 11  7  9  7 11 11  9 11  7 11  5 11 11 11
      8 11 12  4 12 12 11 12 12 12  4 12  9  9  9
      2  4 13  8 13 13 11 13 13 13  9 13  2  4 11
      4  2 14  9 14 14  9 14 14 14  8 14  4  4  4

I tried building a few levels at once to give more space for differences to emerge, but it had no effect. I can try dropping to 11 and starting from there before throwing in the towel.

[Terence Tao]

You seem to have some intuition as to what 854 magmas "look boring" and which ones "look interesting" which I don't understand, but would love to learn more about. Do you mean that the new rows and columns added are nearly identical (except for incrementing 12 to 13, say)? Also, in your last example here, are oyu starting with an order 14 magma and adding one final row and column? I don't see a copy of the original 12-magma here so I'm not quite sure what you're doing here.

In any case, if you have some files of various magmas you've generated in this fashion, it could be useful to make them available, so that other collaborators could test various hypotheses and strategies on them.

[Terence Tao]

I think I'm beginning to understand what you mean by boring extensions. Consider the sporadic order 12 magma, which can be viewed as an order 11 magma with an additional element 0 adjoined, thus adding a row and column (and a new square: in the current numbering, 0 ◇ 0 = 5). The row adjoined can contain some zeroes (0 ◇ x = 0 for several x), but the column does not (x ◇ 0 ≠ 0 for all x), which is consistent with the first rule identified by @Daniel Weber here.

One can cheaply extend this further to an order 13 magma by adding another element 0', thus adding another row and column, by basically duplicating the 0 row and column except for replacing every occurrence of 0 in the output with 0'. Thus x ◇ 0' = x ◇ 0, and 0' ◇ x is 0 ◇ x with any appearance of 0 replaced by 0'. Finally, we can set 0' ◇ 0, 0 ◇ 0', 0' ◇ 0' all equal to 0 ◇ 0. It is a routine matter to check that this new order 13 magma will obey 854 if the order 12 magma did. Unfortunately it also inherits all the other laws that we want to disprove.

There is a small amount of play in perturbing this table by adjusting some insignificant entries, but it does not seem to generate any interesting new failures of law 10, which is why it is also not disproving any of the laws we want to disprove, all of which are consequences of 10. I'll explain this more in the next comment.

[Terence Tao]

Here is a heuristic argument why the law 10 seems to hold almost universally on 854-magmas, which is a significant obstacle blocking us from disproving all the remaining implications. We have this one order 12 example with a single failure of law 10, and we can artificially inflate this failure a little bit by adding dummy rows and columns as above, but that isn't really helping the situation.

First, observe from this graphiti that 854 implies a ton of other laws, even disregarding the five blue conjectural ones. This has many consequences for the left-absorbent sets $E_x := \{ y: x \diamond y = x \}$, namely that they have to be pretty big. For instance, we have

• $x^2 \in E_x$ (law 8).
• $y \in E_x$ if and only if $x$ lies in the range of $R_y$ (law 378).
• For any $y$, the elements $R_x L_x y, y \diamond (L_x y^2), (L_x y)^2, R_{x^2} R_x y, y^2 \diamond L_x y, R_x( (L_x y) \diamond y ), R_x R_{x^2} y$ all lie in $E_x$ (laws 101, 430, 823, 832, 843, 123, 1035 respectively). The open implication 412 also asserts that $L_{x^2} R_x y$ lies in $E_x$.
• The open implication 3316 implies that if $y \in E_x$, then $y \diamond L_x y$ is also in $E_x$.
• Law 10 (which is not a consequence of 854, but is "almost" true as discussed below) asserts that $R_x G \subset E_x$ for all $x$.

From 854, we see that Law 10 holds whenever $y \in G \diamond E_x$, that is to say $y = y' \diamond z$ for some $y',z$ with $x \diamond z = x$. Since $E_x$ was already pretty big, $G \diamond E_x$ is massive. It then becomes very hard to avoid falling into this set, and so there are very few counterexamples $x,y$ to Law 10. (As one subcase: Law 10 holds whenever $E_x \cap E_y \neq \emptyset$.)

Probably the easiest target to refute here is law 1055, which is the only three-variable law to refute. In the language of law 10, the task is to find a pair $x,y$ violating law 10, such that $y \in G \diamond (R_x G)$. One would think that $G \diamond (R_x G)$ is also a very large set, and it should be rare for $y$ to fall outside this set, but unfortunately for the one order 12 magma we have (and the various extensions of it we can build), the small number of exceptions to 10 fail to obey this condition. It could just be that we were unlucky with the initial "seed" magma and that some other finite magma may solve the problem here.

[Daniel Weber]

A few finite magmas ruling out some rules from the partial rule set

• https://teorth.github.io/equational_theories/fme/?magma=%5B%5B4%2C%200%2C%200%2C%207%2C%200%2C%209%2C%200%2C%209%2C%207%2C%207%2C%209%5D%2C%20%5B2%2C%203%2C%205%2C%201%2C%208%2C%201%2C%2010%2C%201%2C%2010%2C%201%2C%208%5D%2C%20%5B2%2C%203%2C%205%2C%202%2C%206%2C%202%2C%2010%2C%202%2C%2010%2C%202%2C%208%5D%2C%20%5B6%2C%203%2C%203%2C%207%2C%203%2C%203%2C%200%2C%203%2C%207%2C%206%2C%203%5D%2C%20%5B4%2C%203%2C%205%2C%204%2C%206%2C%204%2C%204%2C%204%2C%204%2C%204%2C%209%5D%2C%20%5B4%2C%205%2C%205%2C%205%2C%205%2C%209%2C%205%2C%204%2C%205%2C%205%2C%209%5D%2C%20%5B6%2C%203%2C%203%2C%202%2C%206%2C%206%2C%207%2C%206%2C%207%2C%206%2C%206%5D%2C%20%5B4%2C%207%2C%207%2C%207%2C%207%2C%209%2C%207%2C%204%2C%207%2C%207%2C%209%5D%2C%20%5B6%2C%203%2C%203%2C%202%2C%208%2C%208%2C%200%2C%208%2C%207%2C%206%2C%208%5D%2C%20%5B4%2C%209%2C%209%2C%207%2C%209%2C%209%2C%209%2C%209%2C%207%2C%206%2C%209%5D%2C%20%5B4%2C%205%2C%205%2C%2010%2C%205%2C%204%2C%2010%2C%204%2C%2010%2C%2010%2C%209%5D%5D
• https://teorth.github.io/equational_theories/fme/?magma=%5B%5B1%2C%200%2C%209%2C%200%2C%200%2C%200%2C%203%2C%200%2C%209%2C%200%2C%203%2C%200%5D%2C%20%5B1%2C%204%2C%205%2C%201%2C%201%2C%204%2C%201%2C%2010%2C%201%2C%2011%2C%2011%2C%2010%5D%2C%20%5B3%2C%202%2C%209%2C%208%2C%200%2C%202%2C%203%2C%202%2C%203%2C%202%2C%203%2C%200%5D%2C%20%5B3%2C%203%2C%207%2C%207%2C%200%2C%203%2C%203%2C%203%2C%203%2C%203%2C%203%2C%208%5D%2C%20%5B4%2C%204%2C%209%2C%207%2C%200%2C%204%2C%204%2C%204%2C%204%2C%204%2C%204%2C%208%5D%2C%20%5B5%2C%204%2C%205%2C%205%2C%205%2C%204%2C%205%2C%2010%2C%205%2C%207%2C%2011%2C%2010%5D%2C%20%5B1%2C%206%2C%209%2C%206%2C%206%2C%206%2C%203%2C%206%2C%209%2C%206%2C%203%2C%206%5D%2C%20%5B7%2C%204%2C%207%2C%207%2C%207%2C%208%2C%207%2C%206%2C%207%2C%207%2C%207%2C%208%5D%2C%20%5B9%2C%208%2C%209%2C%208%2C%208%2C%208%2C%203%2C%208%2C%209%2C%208%2C%203%2C%208%5D%2C%20%5B9%2C%204%2C%209%2C%209%2C%209%2C%204%2C%209%2C%209%2C%209%2C%207%2C%204%2C%209%5D%2C%20%5B9%2C%206%2C%209%2C%2010%2C%2010%2C%206%2C%209%2C%2010%2C%209%2C%206%2C%203%2C%2010%5D%2C%20%5B11%2C%204%2C%207%2C%207%2C%207%2C%204%2C%2011%2C%204%2C%2011%2C%2011%2C%2011%2C%208%5D%5D
• https://teorth.github.io/equational_theories/fme/?magma=%5B%5B9%2C%202%2C%200%2C%201%2C%200%2C%2010%2C%207%2C%2010%2C%200%2C%200%2C%205%5D%2C%20%5B9%2C%209%2C%201%2C%201%2C%201%2C%2010%2C%205%2C%2010%2C%201%2C%201%2C%205%5D%2C%20%5B2%2C%202%2C%204%2C%201%2C%202%2C%202%2C%202%2C%202%2C%206%2C%202%2C%204%5D%2C%20%5B3%2C%203%2C%204%2C%206%2C%208%2C%203%2C%203%2C%208%2C%204%2C%208%2C%204%5D%2C%20%5B4%2C%204%2C%204%2C%206%2C%205%2C%204%2C%204%2C%208%2C%204%2C%208%2C%204%5D%2C%20%5B9%2C%209%2C%205%2C%205%2C%205%2C%202%2C%205%2C%208%2C%205%2C%205%2C%205%5D%2C%20%5B9%2C%209%2C%206%2C%206%2C%206%2C%206%2C%205%2C%206%2C%206%2C%206%2C%204%5D%2C%20%5B9%2C%209%2C%207%2C%205%2C%205%2C%209%2C%207%2C%208%2C%207%2C%205%2C%207%5D%2C%20%5B8%2C%208%2C%204%2C%201%2C%208%2C%208%2C%208%2C%208%2C%206%2C%208%2C%204%5D%2C%20%5B9%2C%209%2C%209%2C%206%2C%205%2C%209%2C%209%2C%208%2C%209%2C%208%2C%209%5D%2C%20%5B2%2C%202%2C%206%2C%206%2C%2010%2C%2010%2C%202%2C%2010%2C%206%2C%2010%2C%204%5D%5D

[Terence Tao]

I'm a little confused, I thought all the rules in the partial ruleset had to be consequences of 854, due to the way the greedy algorithm worked?

[Daniel Weber]

Yes, but when the rules are minimized I attempt to relax the assumptions while still being a consequence, and if it fails to be a consequence I search for a counterexample to more quickly rule out other relaxations

[Daniel Weber]

It might be useful to assume something which isn't always a consequence of 854, but still doesn't immediately imply some target

[Douglas McNeil]

I wasn't thinking nearly at that level of detail, to put it mildly, but it squares up: I was mostly going from the regularity and how straightforward it was to extend to something which was pretty obviously itself extensible. I'd expected to have to work much harder on the backtracking, hence my desperate attempts to introduce more entropy to find something qualitatively different.

In the last example I guess the reference order 12 magma seems pretty hidden! :-) That one started as s12 before it mutated and grew. I can't remember the precise numbers offhand, but if you just randomly change two cells of an order 12 854 magma to other elements you'll still satisfy 854 over 1% of the time. That's what it was for the sporadic, anyway.

[Terence Tao]

Each 854 magma G is associated with a "Cayley graph" that seems to control a lot of the algebra. Namely make a directed edge x → y if one can write y = z ◇ x for some z. The first observation is that we have an equivalent characterization: x → y if and only if y ◇ x = y. This is thanks to law 378.

The next observation is that law 10 is equivalent to this graph being undirected: x → y if and only if y → x. This is an easy consequence of the previous equivalence. In practice it seems that this graph is nearly undirected, with most edges being symmetric x ↔ y and only a few exceptions.

We have lots and lots of symmetric edges, due to all the various consequences of 854. Examples: $x \leftrightarrow x^2$, $x \leftrightarrow (x \diamond y) \diamond x$, $x \leftrightarrow (y \diamond x^2) \diamond x$, $x \leftrightarrow (y \diamond x) \diamond x^2$, $x \diamond y \leftrightarrow x \diamond (x \diamond y)$. If $z \to x, y$, then we have $x \leftrightarrow y \diamond x$ and $y \leftrightarrow x \diamond y$. If $z \to x \to y$ and $z \to y$, then $x \leftrightarrow y$.

The open law 1055 is the assertion that if $x \to y \to z$ then $x \leftrightarrow z \diamond x$.

It's an amazing amount of structure for such a "non-rigid" object!

[Daniel Weber]

This is the graph for the 12 element magma
Figure_1.png

[Daniel Weber]

Can one recover the magma from this graph?

[Terence Tao]

That's a good question. Certainly the relation that x → y if and only if y ◇ x = y already fills out a big chunk of the multiplication table from the graph. At that point there is this Sudoku game one has to play. I guess one could for instance ask an ATP to reconstruct the 12 element magma from that graph, i.e., from the 854 rule plus the additional rule that x → y if and only if y ◇ x = y.

[Terence Tao]

In the example above, the edge 0 → 2 is the only directed edge; not coincidentally, 0 and 2 are the only adjacent elements that have no mutual friends, i.e., no z such that 0, 2 → z. This is related to the law (an easy consequence of 854) that if z → x, y and x → y then y → x.

[Ibrahim Tencer]

I've found some models of 854. We take some function f and define x * y = f(x) if x = y, otherwise x * y = x. We also assume that x ≠ f(x) and x ≠ f(f(x)). Then a bit of case checking gives that this will satisfy 854. But this model will also satisfy 10.

I also tried modifying it: you can take some q, s, t that are all distinct (provided they aren't linked by f in some way) and redefine qs = sq = t. But if f(q) = s then 10 fails via q(qq) = qs = t, but then for any u that isn't q or s, q((qu)(qu)) = q(qq) = qs = t, so 854 fails too. I haven't checked exactly what conditions you need on q, s, and t for this to work, it requires a lot of tedious case checking, but there's an example below. Maybe there is some other way of modifying these models to get a counterexample.

Here is the unmodified model on Z/7 with f(x) = x + 1:

https://teorth.github.io/equational_theories/fme/?magma=%5B%0A%20%20%20%20%5B1%2C%200%2C%200%2C%200%2C%200%2C%200%2C%200%5D%2C%0A%20%20%20%20%5B1%2C%202%2C%201%2C%201%2C%201%2C%201%2C%201%5D%2C%0A%20%20%20%20%5B2%2C%202%2C%203%2C%202%2C%202%2C%202%2C%202%5D%2C%0A%20%20%20%20%5B3%2C%203%2C%203%2C%204%2C%203%2C%203%2C%203%5D%2C%0A%20%20%20%20%5B4%2C%204%2C%204%2C%204%2C%205%2C%204%2C%204%5D%2C%0A%20%20%20%20%5B5%2C%205%2C%205%2C%205%2C%205%2C%206%2C%205%5D%2C%0A%20%20%20%20%5B6%2C%206%2C%206%2C%206%2C%206%2C%206%2C%200%5D%0A%5D

And the same magma but with 0 * 3 = 3 * 0 = 5:

https://teorth.github.io/equational_theories/fme/?magma=%5B%0A%20%20%20%20%5B1%2C%200%2C%200%2C%205%2C%200%2C%200%2C%200%5D%2C%0A%20%20%20%20%5B1%2C%202%2C%201%2C%201%2C%201%2C%201%2C%201%5D%2C%0A%20%20%20%20%5B2%2C%202%2C%203%2C%202%2C%202%2C%202%2C%202%5D%2C%0A%20%20%20%20%5B5%2C%203%2C%203%2C%204%2C%203%2C%203%2C%203%5D%2C%0A%20%20%20%20%5B4%2C%204%2C%204%2C%204%2C%205%2C%204%2C%204%5D%2C%0A%20%20%20%20%5B5%2C%205%2C%205%2C%205%2C%205%2C%206%2C%205%5D%2C%0A%20%20%20%20%5B6%2C%206%2C%206%2C%206%2C%206%2C%206%2C%200%5D%0A%5D

[Daniel Weber]

You can use * to write * without it turning to italics

[Ibrahim Tencer]

Daniel Weber said:

You can use * to write * without it turning to italics

Thanks

[Ibrahim Tencer]

Is it known if there are any other counterexamples to the implications that are of order less than 12?

[Terence Tao]

@Ibrahim Tencer Thanks for this construction. This also answers @Daniel Weber 's question of whether the graph determines the magma; it does not, as for all of your examples the directed graph is the complete directed graph without loops, and so the directed graph does not "see" the squaring function f(x). One could take this to mean that the graph is trying to tell us that the values of this function are not extremely relevant.

If you want to create a failure in 10 (which is a necessary precondition for contradicting the laws we actually want), so that x → y but not y → x, then one thing that must happen is that x and y must have disjoint incoming neighborhoods; the set of z for which z → x must be disjoint from that with z → y. So quite a few edges have to be deleted from the complete directed graph before we even have a chance of contradicting 10.

[Terence Tao]

One small observation. Here is a reordering of the order 12 example (Finite Magma Explorer):

  4   0   5   0   0   2   2   5   5   0   2   0
  1   0   1   2   1   1   1   1   1   2   2   2
  4   2   4   2   2   2   2   5   5   2   2   2
  3   2   3   2   3   3   3   3   3   2   7   7
  4   4   4   4   1   4   4   4   5   7   4   7
  4   5   5   5   5   3   2   5   5   5   2   5
  4   6   6   6   6   3   2   6   6   6   2   6
  4   7   4   7   7   7   7   5   5   7   7   7
  4   8   4   8   7   8   8   4   5   7   8   7
  9   8   9   8   1   9   9   9   1   6   8   6
  3   6  10   6  10   3   3  10  10   6   2   6
  9   8  11   8  10  11  11  11  10   6   8   6

With this ordering, observe that the top left n x n minor only contains elements less than n for all $6 \leq n \leq 12$. What this means is that this example can actually be obtained from an order 6 example (the top left 6 x 6 minor) by adjoining one more element six more times. The lone counterexample to 10 in this case is coming from $11 \to 0$ but not $0 \to 11$: $11 \diamond (0 \diamond 11) = 9 \neq 11$. So starting with the order 6 example, one has to perform six more extensions before one violates the equation 10! On the one hand, this does show that repeated extension can eventually produce results even if initially the extensions look "boring". On the other hand, the counterexample only barely involves the initial values 0,1,2,3,4,5 of the seed magma; somehow the magma has to grow enough so that the forward image of 0 (i.e., the 0 column entries 1,3,4,9) can be made distinct from the forward image of 11 (i.e., the 11 column entries 0,2,5,6,7) which is basically a precondition for a 10 violation to take place.

A tentative conclusion is then that maybe the iterated extension idea shouldn't be abandoned just yet - it may just take more time to work than previously thought, and some intelligent way to guide the extension may be needed. (One wild idea: try reinforcement learning, with a loss function that rewards approximate compliance with 854 while forcing a specific counterexample configuration to exist?)

[Daniel Weber]

Perhaps just telling the ATP to look for extensions might let it be more efficient

[Terence Tao]

One promising target might be to disprove 1055 x = x ◇ ((y ◇ (z ◇ x)) ◇ x)as follows. With the above renumbering we already have a violation of 10: 11 ≠ 11 ◇ (0 ◇ 11) (of course we had this as well in the original model, with different renumbering). To disprove 1055, it suffices to find an extension of this model that contains two new elements y, z such that 0 = y ◇ (z ◇ 11). One would think that this is an easy task (one equation, two unknowns: looks underdetermined!) but it seems that doing the naive thing of just adding two more elements 12, 13 and trying to force 0 = 12 ◇ (13 ◇ 11)right away doesn't seem to work. One approach might be to select a good candidate element of the original magma, say 7 for sake of argument, then find an extension in which 0 can eventually appear on the 7th column, e.g. one may reach this with the element 15 with 0 = 15 ◇ 7. Then all one has to do is keep extending until 7 can appear in the 11 column, e.g. if one can extend until one has 7 = 23 ◇ 11 then one can declare victory with an order 24 magma: 11 ≠ 11 ◇ ((15 ◇ (23 ◇ 11)) ◇ 11).

[Matthew Bolan]

There is a 5 in column 3 of the first row, is this the correct reordering? The needed property still seems to be satisfied for $6 \le n \le 12$

[Terence Tao]

Gah, I made an off-by-one error. You're right. The seed magma has order 6 (and I don't think it is an extension of an order 5 magma). I've adjusted the preceding comment accordingly.

[Douglas McNeil]

I need to go touch grass, but I think I found an order 13 case with another 10 violation.

https://teorth.github.io/equational_theories/fme/?magma=%5B%5B5%2C%2011%2C%203%2C%205%2C%200%2C%200%2C%2011%2C%206%2C%200%2C%200%2C%2011%2C%206%2C%203%5D%2C%0A%20%5B4%2C%202%2C%201%2C%204%2C%201%2C%201%2C%204%2C%201%2C%201%2C%201%2C%204%2C%201%2C%201%5D%2C%0A%20%5B2%2C%202%2C%207%2C%202%2C%208%2C%204%2C%204%2C%202%2C%204%2C%208%2C%202%2C%208%2C%207%5D%2C%0A%20%5B5%2C%2011%2C%203%2C%205%2C%203%2C%203%2C%2011%2C%201%2C%203%2C%203%2C%2011%2C%201%2C%203%5D%2C%0A%20%5B4%2C%204%2C%207%2C%204%2C%207%2C%204%2C%204%2C%204%2C%204%2C%208%2C%204%2C%208%2C%207%5D%2C%0A%20%5B5%2C%205%2C%207%2C%205%2C%205%2C%204%2C%204%2C%205%2C%2010%2C%205%2C%205%2C%205%2C%207%5D%2C%0A%20%5B5%2C%205%2C%2010%2C%205%2C%206%2C%2010%2C%204%2C%206%2C%2010%2C%206%2C%205%2C%206%2C%2010%5D%2C%0A%20%5B9%2C%207%2C%207%2C%209%2C%207%2C%207%2C%207%2C%201%2C%207%2C%207%2C%207%2C%208%2C%207%5D%2C%0A%20%5B8%2C%208%2C%207%2C%208%2C%208%2C%204%2C%204%2C%208%2C%2010%2C%208%2C%208%2C%208%2C%2010%5D%2C%0A%20%5B9%2C%209%2C%207%2C%209%2C%207%2C%209%2C%209%2C%209%2C%209%2C%208%2C%209%2C%208%2C%207%5D%2C%0A%20%5B9%2C%204%2C%2010%2C%204%2C%2010%2C%2010%2C%209%2C%2010%2C%2010%2C%2010%2C%204%2C%2010%2C%2010%5D%2C%0A%20%5B9%2C%2011%2C%207%2C%209%2C%207%2C%2011%2C%2011%2C%209%2C%2011%2C%207%2C%2011%2C%208%2C%207%5D%2C%0A%20%5B12%2C%2012%2C%207%2C%2012%2C%208%2C%204%2C%204%2C%2012%2C%204%2C%208%2C%2012%2C%208%2C%207%5D%5D

I think the new violation is at (0, 12).

[Terence Tao]

My previous proposal needs revision. law 378 x ◇ y = (x ◇ y) ◇ y does present one obstruction to the above approach: if for instance one wants to write 0 = x ◇ 7 for some x, it is necessary that 0 = 0 ◇ 7, which is not actually the case in this particular construction. So if we had 0 = 15 ◇ 7 and 7 = 23 ◇ 11 then we would also have 0 = 0 ◇ 7 and 7 = 7 ◇ 11 and the 1055 counterexample would already have been seen at the seed magma. So this approach doesn't work as stated.

But a revision might work. One starts with the same seed magma as before with the same 10 violation 11 ≠ 11 ◇ (0 ◇ 11) but now extends until one gets a new element, say 15, obeying both 0 = 0 ◇ 15 and 15 = 15 ◇ 11. That would then give a 1055 violation 11 ≠ 11 ◇ ((0 ◇ (15 ◇ 11)) ◇ 11). This no longer sets off the 378 objection, but unfortunately 854 also implies a ton of other laws, and I am not sure yet whether these two requirements 0 = 0 ◇ 15 and 15 = 15 ◇ 11 force some other constraint that would have been detectable in the original magma.

[Douglas McNeil]

4 now? When I get back I'll have to figure out which change I tried had such an effect.

https://teorth.github.io/equational_theories/fme/?magma=%5B%5B5%2C%2011%2C%203%2C%205%2C%200%2C%200%2C%2011%2C%206%2C%200%2C%200%2C%2011%2C%2010%2C%203%2C%2011%2C%206%2C%205%5D%2C%20%5B4%2C%202%2C%201%2C%204%2C%201%2C%201%2C%204%2C%201%2C%201%2C%201%2C%204%2C%201%2C%201%2C%204%2C%201%2C%204%5D%2C%20%5B2%2C%202%2C%207%2C%202%2C%208%2C%204%2C%204%2C%202%2C%204%2C%208%2C%202%2C%208%2C%207%2C%202%2C%202%2C%202%5D%2C%20%5B5%2C%2011%2C%203%2C%205%2C%203%2C%203%2C%2011%2C%201%2C%203%2C%203%2C%2011%2C%201%2C%203%2C%2011%2C%2010%2C%209%5D%2C%20%5B4%2C%204%2C%207%2C%204%2C%207%2C%204%2C%204%2C%204%2C%204%2C%208%2C%204%2C%208%2C%207%2C%204%2C%204%2C%204%5D%2C%20%5B5%2C%205%2C%207%2C%205%2C%205%2C%204%2C%204%2C%205%2C%2010%2C%205%2C%205%2C%205%2C%207%2C%205%2C%205%2C%205%5D%2C%20%5B5%2C%205%2C%2010%2C%202%2C%206%2C%2010%2C%204%2C%206%2C%2010%2C%206%2C%205%2C%206%2C%2010%2C%202%2C%206%2C%205%5D%2C%20%5B8%2C%207%2C%207%2C%208%2C%207%2C%207%2C%207%2C%201%2C%207%2C%207%2C%207%2C%208%2C%207%2C%207%2C%2010%2C%205%5D%2C%20%5B8%2C%208%2C%207%2C%208%2C%208%2C%204%2C%204%2C%208%2C%2010%2C%208%2C%208%2C%208%2C%2010%2C%208%2C%208%2C%208%5D%2C%20%5B9%2C%209%2C%207%2C%209%2C%207%2C%209%2C%209%2C%209%2C%209%2C%208%2C%209%2C%208%2C%207%2C%209%2C%209%2C%209%5D%2C%20%5B9%2C%204%2C%2010%2C%204%2C%2010%2C%2010%2C%209%2C%2010%2C%2010%2C%2010%2C%204%2C%2010%2C%2010%2C%2011%2C%2010%2C%209%5D%2C%20%5B9%2C%2011%2C%207%2C%209%2C%207%2C%2011%2C%2011%2C%209%2C%2011%2C%207%2C%2011%2C%208%2C%207%2C%2011%2C%209%2C%209%5D%2C%20%5B12%2C%2012%2C%207%2C%2012%2C%208%2C%204%2C%204%2C%2012%2C%204%2C%208%2C%2012%2C%208%2C%207%2C%2012%2C%2012%2C%2012%5D%2C%20%5B4%2C%209%2C%2013%2C%205%2C%2013%2C%2013%2C%204%2C%2013%2C%2013%2C%2013%2C%204%2C%2013%2C%2013%2C%205%2C%2013%2C%205%5D%2C%20%5B9%2C%2014%2C%2014%2C%208%2C%2014%2C%2014%2C%2014%2C%201%2C%2014%2C%2014%2C%2014%2C%208%2C%2014%2C%2014%2C%208%2C%209%5D%2C%20%5B9%2C%2011%2C%203%2C%209%2C%2015%2C%2015%2C%2011%2C%206%2C%2015%2C%2015%2C%2011%2C%2010%2C%203%2C%2011%2C%206%2C%209%5D%5D

And these locations seem suggestive:

[(0, 2, 0, 3), (0, 12, 0, 3), (15, 2, 15, 3), (15, 12, 15, 3)]

[Terence Tao]

OK, here is an interesting phenomenon: in order to contradict 1055, it is not enough to have a single violation of 10; one must have at least two.

Suppose we want to contradict 1055 x = x ◇ ((y ◇ (z ◇ x)) ◇ x) using a 10 counterexample such as 11 ≠ 11 ◇ (0 ◇ 11), so we want x = 11 and y ◇ (z ◇ x) = 0. If we call z ◇ x 15 for sake of argument, then y ◇ 15 = 0 and z ◇ 11 = 15, hence by law 384 we have 0 ◇ 15 = 0 and 15 ◇ 11 = 15. But if (11,15) does not violate 10, this also forces 11 ◇ 15 = 11, and now from the original law 854 we must have 11 = 11 ◇ ((0 ◇ 15) ◇ (11 ◇ 15)) = 11 ◇ (0 ◇ 11), contradicting our original hypothesis. So 11,15 must also be a violation to 10: 11 ≠ 11 ◇ (15 ◇ 11).

So the extensions need to generate new 10 violations. I guess this dovetails very nicely with what @Douglas McNeil is trying right now. By the way, what do the quadruples such as (0,2,0,3) mean in your notation?

[Daniel Weber]

Could something like a greedy approach work, but instead of setting $a \diamond b = c$ for a fresh $c$ you set $a \diamond b = a$?

[Terence Tao]

This sounds promising. More precisely, in situations where one has to decide what to do for $a \diamond b$, one has two options: create something novel, or set it equal to $a$, and perhaps one can try an iteration that only generates additional rules if both of these options are blocked.

[Douglas McNeil]

Okay, new record of 6 violations of 10 in an 854 magma:

https://teorth.github.io/equational_theories/fme/?magma=5%2011%203%205%200%200%2011%206%200%200%2011%2010%203%2011%206%205%209%0A4%202%201%204%201%201%204%201%201%201%204%201%201%204%201%204%204%0A2%202%207%202%208%204%204%202%204%208%202%208%207%202%202%202%202%0A5%2011%203%205%203%203%2011%201%203%203%2011%201%203%2011%2010%209%205%0A4%204%207%204%207%204%204%204%204%208%204%208%207%204%204%204%204%0A5%205%207%205%205%204%204%205%2010%205%205%205%207%205%205%205%205%0A5%205%2010%202%206%2010%204%206%2010%206%205%206%2010%202%206%205%205%0A8%207%207%208%207%207%207%201%207%207%207%208%207%207%2010%205%205%0A8%208%207%208%208%204%204%208%2010%208%208%208%2010%208%208%208%208%0A9%209%207%209%207%209%209%209%209%208%209%208%207%209%209%209%209%0A9%204%2010%204%2010%2010%209%2010%2010%2010%204%2010%2010%2011%2010%209%204%0A9%2011%207%209%207%2011%2011%209%2011%207%2011%208%207%2011%209%209%209%0A12%2012%207%2012%208%204%204%2012%204%208%2012%208%207%2012%2012%2012%2012%0A4%209%2013%205%2013%2013%204%2013%2013%2013%204%2013%2013%205%2013%205%204%0A9%2014%2014%208%2014%2014%2014%201%2014%2014%2014%208%2014%2014%208%209%205%0A9%2011%203%209%2015%2015%2011%206%2015%2015%2011%2010%203%2011%206%209%205%0A9%2011%203%205%2016%2016%2011%206%2016%2016%2011%206%203%2011%206%205%205

I may have found the trick. :fingers_crossed:

[Douglas McNeil]

And now 12.

https://teorth.github.io/equational_theories/fme/?magma=%5B%5B5%2C%2011%2C%203%2C%205%2C%200%2C%200%2C%2011%2C%206%2C%200%2C%200%2C%2011%2C%2010%2C%203%2C%2011%2C%206%2C%205%5D%2C%20%5B4%2C%202%2C%201%2C%204%2C%201%2C%201%2C%204%2C%201%2C%201%2C%201%2C%204%2C%201%2C%201%2C%204%2C%201%2C%204%5D%2C%20%5B2%2C%202%2C%207%2C%202%2C%208%2C%204%2C%204%2C%202%2C%204%2C%208%2C%202%2C%208%2C%207%2C%202%2C%202%2C%202%5D%2C%20%5B5%2C%2011%2C%203%2C%205%2C%203%2C%203%2C%2011%2C%201%2C%203%2C%203%2C%2011%2C%201%2C%203%2C%2011%2C%2010%2C%209%5D%2C%20%5B4%2C%204%2C%207%2C%204%2C%207%2C%204%2C%204%2C%204%2C%204%2C%208%2C%204%2C%208%2C%207%2C%204%2C%204%2C%204%5D%2C%20%5B5%2C%205%2C%207%2C%205%2C%205%2C%204%2C%204%2C%205%2C%2010%2C%205%2C%205%2C%205%2C%207%2C%205%2C%205%2C%205%5D%2C%20%5B5%2C%205%2C%2010%2C%202%2C%206%2C%2010%2C%204%2C%206%2C%2010%2C%206%2C%205%2C%206%2C%2010%2C%202%2C%206%2C%205%5D%2C%20%5B8%2C%207%2C%207%2C%208%2C%207%2C%207%2C%207%2C%201%2C%207%2C%207%2C%207%2C%208%2C%207%2C%207%2C%2010%2C%205%5D%2C%20%5B8%2C%208%2C%207%2C%208%2C%208%2C%204%2C%204%2C%208%2C%2010%2C%208%2C%208%2C%208%2C%2010%2C%208%2C%208%2C%208%5D%2C%20%5B9%2C%209%2C%207%2C%209%2C%207%2C%209%2C%209%2C%209%2C%209%2C%208%2C%209%2C%208%2C%207%2C%209%2C%209%2C%209%5D%2C%20%5B9%2C%204%2C%2010%2C%204%2C%2010%2C%2010%2C%209%2C%2010%2C%2010%2C%2010%2C%204%2C%2010%2C%2010%2C%2011%2C%2010%2C%209%5D%2C%20%5B9%2C%2011%2C%207%2C%209%2C%207%2C%2011%2C%2011%2C%209%2C%2011%2C%207%2C%2011%2C%208%2C%207%2C%2011%2C%209%2C%209%5D%2C%20%5B12%2C%2012%2C%207%2C%2012%2C%208%2C%204%2C%204%2C%2012%2C%204%2C%208%2C%2012%2C%208%2C%207%2C%2012%2C%2012%2C%2012%5D%2C%20%5B4%2C%209%2C%2013%2C%205%2C%2013%2C%2013%2C%204%2C%2013%2C%2013%2C%2013%2C%204%2C%2013%2C%2013%2C%205%2C%2013%2C%205%5D%2C%20%5B9%2C%2014%2C%2014%2C%208%2C%2014%2C%2014%2C%2014%2C%201%2C%2014%2C%2014%2C%2014%2C%208%2C%2014%2C%2014%2C%208%2C%209%5D%2C%20%5B9%2C%2011%2C%203%2C%209%2C%2015%2C%2015%2C%2011%2C%206%2C%2015%2C%2015%2C%2011%2C%2010%2C%203%2C%2011%2C%206%2C%209%5D%5D

I expect I could keep going for a bit, the exceptions have a pretty recognizable pattern (the syntax from before, Terence, was just (x,y,lhs,rhs)). This is probably cleaner:

Verifying equations:
✓ Equation 854 satisfied
✓ Found 12 violations of equation 10:
At (x,y)=(0,2): 0 ≠ 0 ◇ (2 ◇ 0) = 0 ◇ 2 = 3
At (x,y)=(0,12): 0 ≠ 0 ◇ (12 ◇ 0) = 0 ◇ 12 = 3
At (x,y)=(0,18): 0 ≠ 0 ◇ (18 ◇ 0) = 0 ◇ 18 = 3
At (x,y)=(15,2): 15 ≠ 15 ◇ (2 ◇ 15) = 15 ◇ 2 = 3
At (x,y)=(15,12): 15 ≠ 15 ◇ (12 ◇ 15) = 15 ◇ 12 = 3
At (x,y)=(15,18): 15 ≠ 15 ◇ (18 ◇ 15) = 15 ◇ 18 = 3
At (x,y)=(16,2): 16 ≠ 16 ◇ (2 ◇ 16) = 16 ◇ 2 = 3
At (x,y)=(16,12): 16 ≠ 16 ◇ (12 ◇ 16) = 16 ◇ 12 = 3
At (x,y)=(16,18): 16 ≠ 16 ◇ (18 ◇ 16) = 16 ◇ 18 = 3
At (x,y)=(17,2): 17 ≠ 17 ◇ (2 ◇ 17) = 17 ◇ 2 = 3
At (x,y)=(17,12): 17 ≠ 17 ◇ (12 ◇ 17) = 17 ◇ 12 = 3
At (x,y)=(17,18): 17 ≠ 17 ◇ (18 ◇ 17) = 17 ◇ 18 = 3

You can see what turns out to be happening. Originally we only had the (0,2), then I found (0,12) and then we added (15,12), and (15,2), and now the game is on.

[Douglas McNeil]

Yeah, it looks like in this way I can carry on (I just hit 28), because of the very dull extending pattern I've been complaining about. :-) Once we got to an "outer border" which is self-sustaining, we can carry on indefinitely. I mean, look at this thing:

 5 11  3  5  0  0 11  6  0  0 11 10  3 11  6  5  9  5  3  3  3  3  3
 4  2  1  4  1  1  4  1  1  1  4  1  1  4  1  4  4  4  1  1  1  1  1
 2  2  7  2  8  4  4  2  4  8  2  8  7  2  2  2  2  2  7  7  7  7  7
 5 11  3  5  3  3 11  1  3  3 11  1  3 11 10  9  5  5  3  3  3  3  3
 4  4  7  4  7  4  4  4  4  8  4  8  7  4  4  4  4  4  7  7  7  7  7
 5  5  7  5  5  4  4  5 10  5  5  5  7  5  5  5  5  5  7  7  7  7  7
 5  5 10  2  6 10  4  6 10  6  5  6 10  2  6  5  5  5 10 10 10 10 10
 8  7  7  8  7  7  7  1  7  7  7  8  7  7 10  5  5  5  7  7  7  7  7
 8  8  7  8  8  4  4  8 10  8  8  8 10  8  8  8  8  8  7  7  7  7  7
 9  9  7  9  7  9  9  9  9  8  9  8  7  9  9  9  9  9  7  7  7  7  7
 9  4 10  4 10 10  9 10 10 10  4 10 10 11 10  9  4  4 10 10 10 10 10
 9 11  7  9  7 11 11  9 11  7 11  8  7 11  9  9  9  9  7  7  7  7  7
12 12  7 12  8  4  4 12  4  8 12  8  7 12 12 12 12 12  7  7  7  7  7
 4  9 13  5 13 13  4 13 13 13  4 13 13  5 13  5  4  5 13 13 13 13 13
 9 14 14  8 14 14 14  1 14 14 14  8 14 14  8  9  5  5 14 14 14 14 14
 9 11  3  9 15 15 11  6 15 15 11 10  3 11  6  9  5  9  3  3  3  3  3
 9 11  3  5 16 16 11  6 16 16 11  6  3 11  6  5  5  5  3  3  3  3  3
 9 11  3  5 17 17 11  6 17 17 11  6  3 11  6  5  5  5  3  3  3  3  3
18 18  7 18  8  4  4 18  4  8 18  8  7 18 18 18 18 18  7  7  7  7  7
19 19  7 19  8  4  4 19  4  8 19  8  7 19 19 19 19 19  7  7  7  7  7
20 20  7 20  8  4  4 20  4  8 20  8  7 20 20 20 20 20  7  7  7  7  7
21 21  7 21  8  4  4 21  4  8 21  8  7 21 21 21 21 21  7  7  7  7  7
22 22  7 22  8  4  4 22  4  8 22  8  7 22 22 22 22 22  7  7  7  7  7

What we haven't seen yet is any violations of 10 which aren't of the form x * (y * x) = 3. Whether this a real thing or just an artifact of our search isn't clear, my explorations have definitely been biased towards descendants of the original. Be kind of interesting if it turned out that there can only be one "3", i.e. one violating rhs x(yx) value, in an 854 magma.

[Michael Bucko]

Douglas McNeil schrieb:

5 11 3 5 0 0 11 6 0 0 11 10 3 11 6 5 9 5 3 3 3 3 3
4 2 1 4 1 1 4 1 1 1 4 1 1 4 1 4 4 4 1 1 1 1 1
2 2 7 2 8 4 4 2 4 8 2 8 7 2 2 2 2 2 7 7 7 7 7
5 11 3 5 3 3 11 1 3 3 11 1 3 11 10 9 5 5 3 3 3 3 3
4 4 7 4 7 4 4 4 4 8 4 8 7 4 4 4 4 4 7 7 7 7 7
5 5 7 5 5 4 4 5 10 5 5 5 7 5 5 5 5 5 7 7 7 7 7
5 5 10 2 6 10 4 6 10 6 5 6 10 2 6 5 5 5 10 10 10 10 10
8 7 7 8 7 7 7 1 7 7 7 8 7 7 10 5 5 5 7 7 7 7 7
8 8 7 8 8 4 4 8 10 8 8 8 10 8 8 8 8 8 7 7 7 7 7
9 9 7 9 7 9 9 9 9 8 9 8 7 9 9 9 9 9 7 7 7 7 7
9 4 10 4 10 10 9 10 10 10 4 10 10 11 10 9 4 4 10 10 10 10 10
9 11 7 9 7 11 11 9 11 7 11 8 7 11 9 9 9 9 7 7 7 7 7
12 12 7 12 8 4 4 12 4 8 12 8 7 12 12 12 12 12 7 7 7 7 7
4 9 13 5 13 13 4 13 13 13 4 13 13 5 13 5 4 5 13 13 13 13 13
9 14 14 8 14 14 14 1 14 14 14 8 14 14 8 9 5 5 14 14 14 14 14
9 11 3 9 15 15 11 6 15 15 11 10 3 11 6 9 5 9 3 3 3 3 3
9 11 3 5 16 16 11 6 16 16 11 6 3 11 6 5 5 5 3 3 3 3 3
9 11 3 5 17 17 11 6 17 17 11 6 3 11 6 5 5 5 3 3 3 3 3
18 18 7 18 8 4 4 18 4 8 18 8 7 18 18 18 18 18 7 7 7 7 7
19 19 7 19 8 4 4 19 4 8 19 8 7 19 19 19 19 19 7 7 7 7 7
20 20 7 20 8 4 4 20 4 8 20 8 7 20 20 20 20 20 7 7 7 7 7
21 21 7 21 8 4 4 21 4 8 21 8 7 21 21 21 21 21 7 7 7 7 7
22 22 7 22 8 4 4 22 4 8 22 8 7 22 22 22 22 22 7 7 7 7 7

So beautiful!

[Douglas McNeil]

image.png

^ for us visual-minded types

[Terence Tao]

I'm pretty sure by taking the direct product of an 854 magma with a 10 violation, and some other 854 magma (which doesn't need to have 10 violations), one can create a magma with 10 violations with many different values, although this is again a "boring" way to create more 10 violations. Still, this is encouraging that there is enough "malleability" in 854 to create a few more 10 violations, as these are essential precursors to refuting the outstanding implications. More precisely, any 10 violation $x \diamond (y \diamond x) = z \neq x$ can be "promoted" to a new anti-implication if one of the following happens:

• Promotion to 413 counterexample occurs if $x \neq x \diamond (x \diamond z)$.
• Promotion to 1045 counterexample occurs if $y = (w \diamond (w \diamond x))$ for some $w$.
• Promotion to 1055 counterexample occurs if $y = (u \diamond (w \diamond x))$ for some $w, u$, or equivalently if $y \diamond v = y$, $v \diamond x = v$ for some $v$.
• Promotion to 3316 counterexample occurs if $y \diamond x \neq y \diamond z$.
• Promotion to 3925 counterexample occurs if $x \diamond y \neq z \diamond y$.

I don't have a clear idea how to force any of these to occur on top of an existing 10 violation, although 1045 or 1055 seem the most promising given that they have an existential quantifier.

[Douglas McNeil]

I've got alerts in to warn me if I hit anything which refuted any of the outstanding implications and didn't hit any of them, including an overnight perturbation run w/~1M magma, unfortunately.

Running out of ideas, although before I found more violations than I knew what to do with, I was considering starting with seeds with lots of 10 violations but worse 854 behaviour and trying to pull them towards 854, which is basically the opposite of what I was trying before with 854 and 413.

Could still be a snipe hunt, more's the pity.

[Terence Tao]

Given all the recent progress on 1485, I now propose an analogous approach to attack 854. The main idea is to introduce the notion of a "relaxed 854-magma" which is hopefully easier to construct and could (again hopefully) be used as a guide to build an actual 854-magma by a greedy construction.

A relaxed magma is a magma with multiplicity allowed in the multiplication table: a given product x ◇ y could have multiple possible values, though there must always be at least one. See here for an example, adapted for 1485 analysis. For such a relaxed magma to be consistent with 854 x = x ◇ ((y ◇ z) ◇ (x ◇ z)), we need the following rule:

• If one has already chosen values for y ◇ z, x ◇ z and (y ◇ z) ◇ (x ◇ z) consistent with the relaxed multiplication table, then x is a permissible choice of x ◇ ((y ◇ z) ◇ (x ◇ z)) in that table.

Or to put it another way, if R(x,y,z) denotes the relation that z appears as one of the options for x ◇ y in the table, we need the following axioms:

• Claim 1'. For each x, y, there is at least one z for which R(x,y,z) holds.
• Claim 854. If R(y,z,w), R(x,z,u), and R(w,u,v), then R(x,v,x).

On the other hand, if we would like to refute a law, say 413 x = x ◇ (x ◇ (x ◇ (y ◇ x))) for sake of argument, we would like to have the following:

• Claim anti-413. There exists x,y,z,w,u such R(y,x,z), R(x,z,w), R(x,w,u) are true, but R(x,u,x) is false.

Note that if we could upgrade Claim 1' to

• Claim 1. For each x, y, there is at exactly one z for which R(x,y,z) holds.

while also obeying Claims 854 and anti-413, we would get the anti-implication 854 !-> 413. So I propose looking for finite relaxed magmas that just obey Claims 1', 854, anti-413, and similarly for the other four outstanding implications. We then have to figure out how to greedily create an actual 854 magma that follows the relaxed 854 magma as a model, but perhaps our previous experience in greedy constructions will help here. (Given the huge number of laws that 854 implies, I suspect this will need to be an automated task, similar to what @Daniel Weber did with the pure greedy approach.)

Note: the definition of a "relaxed 854 magma" may be subject to revision. It may be that one has to take every single known consequence of 854 and also place relaxed version of those laws as additional axioms, though many may be redundant. Similarly for the laws identified by Daniel Weber several days ago. Maybe this can be done by an iterative process: first generate a relaxed 854 counterexample magma with the plain 854 rule, test if any of the other laws are not obeyed, and if not add one of them as an axiom and search again.

Another note: I have the vague feeling that the closer that the relaxed magma is to an actual magma, in that there are very few entries that are ambiguous, the better a guide it will be, as there will be fewer cases to check in the greedy algorithm analysis. I also have the vague sense that it would be good to avoid idempotents R(x,x,x), as this may cause particular problems in the greedy algorithm.

[Michael Bucko]

I was trying to take the relaxed magma approach and address 854-413. I guess those kinds of operation tables aren't admitted by the FMT, but perhaps I can use this kind of relaxed format in one of the solvers?

[
    [[0,1],    [0],      [1,2],    [0],      [4],      [5]],
    [[1],      [1,2],    [2],      [1,4],    [0],      [5]],
    [[2],      [2],      [2,3],    [3],      [4],      [1]],
    [[0],      [3],      [3],      [3,4],    [0,5],    [5]],
    [[4],      [4],      [4],      [5],      [4],      [5]],
    [[5],      [5],      [5],      [5],      [5],      [5]]
]

[Terence Tao]

Unfortunately it doesn't seem like this table obeys 854. Take x=y=z=0. Then one possible value w of y ◇ z is 1, one possible value u of x ◇ z is 1, and one possible value v of w ◇ u = (y ◇ z) ◇ (x ◇ z) is 2; but then x ◇ ((y ◇ z) ◇ (x ◇ z)) = 0 ◇ 2cannot equal x = 0 (it can only equal 1 or 2).

But this is the sort of solution - with very few multiple values - I would like to see. If hypothetically the table did obey 854, one could then guide a search for finite 854 magmas refuting 413 by having vertices of six Classes 0-5, being multiplied according to the above table, for instance the product of a Class 0 object and a Class 0 object should be Class 0 or 1, the product of a Class 0 object and a Class 1 object should be Class 0, and so forth. If the underlying relaxed magma obeyed 854 and refuted 413, this would greatly increase the chance that any such extended magma would also obey 854 and refuted 413, though it is not guaranteed. (After a lengthy discussion over at the 1485 thread I see now that the greedy algorithm approach is likely to be significantly more complicated for 854 than it will be for 1485, so I am hoping that a heuristic approach for 854 may be sufficient to locate a concrete finite counterexample.)

[Jose Brox]

I've been working in another approach that seemed to be promising for 854, I will see if I can finish it soon (or at least give you the details if it gets too complicated).

[Michael Bucko]

Terence Tao schrieb:

Unfortunately it doesn't seem like this table obeys 854. Take x=y=z=0. Then one possible value w of y ◇ z is 1, one possible value u of x ◇ z is 1, and one possible value v of w ◇ u = (y ◇ z) ◇ (x ◇ z) is 2; but then x ◇ ((y ◇ z) ◇ (x ◇ z)) = 0 ◇ 2cannot equal x = 0 (it can only equal 1 or 2).

Prof. Tao, you're right.

[Michael Bucko]

Wrote a simple Sage script -- trying to locate a concrete finite counterexample. It's been running for 30 minutes. I'll let it run some more, and then try to add some heuristics.
(I should probably just stick to z3 and Lean, but I wanted to try that)
854.sage.pas

UPDATE: the Sage script run for a couple of hours, and didn't find anything. I'll most likely focus on Lean+z3 and experiment with heuristics.

[Terence Tao]

Perhaps 413 was too hard of an initial target to refute. The easiest-looking target is 1055 x = x ◇ ((y ◇ (z ◇ x)) ◇ x). Writing w = z ◇ x, u = y ◇ w, and v = u ◇ x, we need to find an example with x ≠ x ◇ v. Because of Law 378, the condition u = y ◇ w for some w is equivalent to u = u ◇ w, so we may eliminate a variable. In terms of R, the axiom is now

• Anti-1055: There exists x, z, w, u, v such that R(z,x,w), R(u,w,u), R(u,x,v) are true, but R(x,v,x) is false.

Perhaps it could be slightly easier to locate counterexamples here.

[Terence Tao]

Actually this suggests the following exercise for anyone with some spare ATP compute. We have five open implications from 854:  413 x = x ◇ (x ◇ (x ◇ (y ◇ x))), 1045 x = x ◇ ((y ◇ (y ◇ x)) ◇ x), 1055 x = x ◇ ((y ◇ (z ◇ x)) ◇ x), 3316 x ◇ y = x ◇ (y ◇ (x ◇ y)), and 3925 x ◇ y = (x ◇ (y ◇ x)) ◇ y. We know that 1055 implies 1045, but otherwise the five laws have no implications between them. However, if we assume 854, it may be that there are more equivalences here. Over on the 1485 thread, for instance, the open implications from 1485 are to 151, 3456, and 3862; they are not equivalent to each other in the absence of any other axioms, but we also know that assuming 1485, they are equivalent, so really there is just one anti-implication to resolve there. So perhaps there is a similar collapse among the five open implications here, and if so that should be able to be picked up by standard ATP queries. This may help clarify which of these laws are the easiest to attack.

[Michael Bucko]

Running one more Sage script for 854->1055 with anti-1055 (posting for the reference- hoping to not have a bug here).

# Check 854:
def check_equation_854(table):
    for x in S:
        for y in S:
            for z in S:
                yz = table[y][z]
                xz = table[x][z]
                yz_xz = table[yz][xz]
                lhs = x
                rhs = table[x][yz_xz]
                if lhs != rhs:
                    return False
    return True

# NOT 1055:
# There exists x, z, w, u, v such that:
# w = z ◇ x
# u = u ◇ w
# v = u ◇ x
# x ≠ x ◇ v
def check_not_equation_1055(table):
    for x in S:
        for z in S:
            w = table[z][x]
            for u in S:
                # Check if u = u ◇ w
                if table[u][w] != u:
                    continue
                v = table[u][x]
                # Check if x != x ◇ v
                if table[x][v] != x:
                    return True  # Yay!
    return False

[Jose Brox]

Terence Tao ha dicho:

We have five open implications from 854:  413 x = x ◇ (x ◇ (x ◇ (y ◇ x))), 1045 x = x ◇ ((y ◇ (y ◇ x)) ◇ x), 1055 x = x ◇ ((y ◇ (z ◇ x)) ◇ x), 3316 x ◇ y = x ◇ (y ◇ (x ◇ y)), and 3925 x ◇ y = (x ◇ (y ◇ x)) ◇ y. We know that 1055 implies 1045, but otherwise the five laws have no implications between them. However, if we assume 854, it may be that there are more equivalences here.

I've been running in Prover9/Mace4 for several minutes all the implications starting or ending with 413, and no proof nor countermodel has been found. Is there perhaps any set-theoretical reason impeding finite counterexamples?

[Michael Bucko]

Jose Brox schrieb:

Terence Tao ha dicho:

We have five open implications from 854:  413 x = x ◇ (x ◇ (x ◇ (y ◇ x))), 1045 x = x ◇ ((y ◇ (y ◇ x)) ◇ x), 1055 x = x ◇ ((y ◇ (z ◇ x)) ◇ x), 3316 x ◇ y = x ◇ (y ◇ (x ◇ y)), and 3925 x ◇ y = (x ◇ (y ◇ x)) ◇ y. We know that 1055 implies 1045, but otherwise the five laws have no implications between them. However, if we assume 854, it may be that there are more equivalences here.

I've been running in Prover9/Mace4 for several minutes all the implications starting or ending with 413, and no proof nor countermodel has been found. Is there perhaps any set-theoretical reason impeding finite counterexamples?

Can you please share your Prover9 script with anti-1055?

[Ibrahim Tencer]

Douglas McNeil said:

Verifying equations:
✓ Equation 854 satisfied
✓ Found 12 violations of equation 10:
At (x,y)=(0,2): 0 ≠ 0 ◇ (2 ◇ 0) = 0 ◇ 2 = 3
At (x,y)=(0,12): 0 ≠ 0 ◇ (12 ◇ 0) = 0 ◇ 12 = 3
At (x,y)=(0,18): 0 ≠ 0 ◇ (18 ◇ 0) = 0 ◇ 18 = 3
At (x,y)=(15,2): 15 ≠ 15 ◇ (2 ◇ 15) = 15 ◇ 2 = 3
At (x,y)=(15,12): 15 ≠ 15 ◇ (12 ◇ 15) = 15 ◇ 12 = 3
At (x,y)=(15,18): 15 ≠ 15 ◇ (18 ◇ 15) = 15 ◇ 18 = 3
At (x,y)=(16,2): 16 ≠ 16 ◇ (2 ◇ 16) = 16 ◇ 2 = 3
At (x,y)=(16,12): 16 ≠ 16 ◇ (12 ◇ 16) = 16 ◇ 12 = 3
At (x,y)=(16,18): 16 ≠ 16 ◇ (18 ◇ 16) = 16 ◇ 18 = 3
At (x,y)=(17,2): 17 ≠ 17 ◇ (2 ◇ 17) = 17 ◇ 2 = 3
At (x,y)=(17,12): 17 ≠ 17 ◇ (12 ◇ 17) = 17 ◇ 12 = 3
At (x,y)=(17,18): 17 ≠ 17 ◇ (18 ◇ 17) = 17 ◇ 18 = 3

You can see what turns out to be happening. Originally we only had the (0,2), then I found (0,12) and then we added (15,12), and (15,2), and now the game is on.

So in all of these examples we have yx = x and x² ≠ x. Is it known whether a counterexample to 10 must be like this?

[Terence Tao]

I think I've gotten a way to get abstract nonsense (or "syntactic" arguments) to get new anti-implication, namely that 854 x = x ◇ ((y ◇ z) ◇ (x ◇ z)) does not imply 3925 x ◇ y = (x ◇ (y ◇ x)) ◇ y, but I'm not 100% sure about this, it's sort of a weird argument, mostly taking advantage of the fact that the 854 law is of the left-absorbent form x = x ◇ f(x,y,z) for some word f(x,y,z).

Define the G to be the free magma on two generators x, y, i.e., the magma of words in x, y, and let G/~ be the quotient of G by the equivalence relation ~ defined by saying that w ~ w' if one can rewrite w to w' after finitely many applications of the law 854. Then, abstract nonsense tells us that G/~ is universal for 854, at least regarding identities involving at most two variables. In particular, to disprove 3925, it suffices to show that the words x ◇ y, (x ◇ (y ◇ x)) ◇ y are not equal in G/~.

Now, 854 is not a confluent law, nor do we know of a complete rewriting system for it, so the relation ~ is pretty mysterious, which is why we have not tried to make much use of this equivalence relation so far. But we can say a few things about it. If we can refute some proposed law w(x,y) = w'(x,y) in any magma obeying 854, then this implies that w and w' are not equivalent. For instance, because we have at least one known counterexample to the 10 law x = x ◇ (y ◇ x), we know that the words x and x ◇ (y ◇ x) are not equivalent with respect to ~. More generally, the large number of implications and anti-implications that we already have regarding 854 (collected very conveniently in Equation Explorer) tell us a lot about this equivalence relation already for short words. Also, all of the finite 854 examples we have been collecting will be very useful for establishing if two given long words are not equal to each other.

Also, 854 implies law 378, x ◇ y = (x ◇ y) ◇ y. As a consequence, if we define the left Cayley graph on an 854 magma by declaring x → y whenever y = z ◇ x for some z, we see that x → y if and only if y = y ◇ x. We can then lift this up to a graph on the free group G: in this group, x → y if and only if y ~ y ◇ x, or equivalently (by law 378) if y ~ z ◇ x for some z.

As observed previously, law 10 asserts that this graph has some one-way edges. In particular, for the two generators x, y of G, we have x → y ◇ x (because (y ◇ x) ◇ x ~ y ◇ x), but we do not have the edge y ◇ x → x (because it is not true that x ◇ (y ◇ x) ~ x.) More generally, the implications and anti-implications we already know about 854, as well as the many finite models we have, already tell us a lot about this directed graph on short and medium length words.

OK, so far this is just abstract nonsense translating things we already know into the free magma. But here is the key new fact: the free magma has a "unique factorization" type property!

Unique factorization. Suppose that a, b, c, d are elements of the free group such that a ◇ b ~ c ◇ d, with the relations b → a and d → c being false (thus, a ◇ b ~ a and c ◇ d ~ c are both false). Then a ~ c and b ~ d.

Proof. By hypothesis, it is possible to transform the word a ◇ b into the word c ◇ d by some finite number of rewrites using 854. Because of the form of 854, any rewrite either replaces a term e with an equivalent term e ◇ f for which there is an edge f → e, or else replaces e ◇ f with an equivalent term e for which there is an edge f → e. Because of this and the initial hypothesis that we do not have the edge b → a, we see from induction that the only words that can be obtained from rewriting a ◇ b take the form (((a' ◇ b') ◇ w(1)) ◇ ... ◇ w(n)) where a' ~ a, b' ~ b, n is a natural number, and w(1),...,w(n) are words such that we have edges
w(i+1) → (((a' ◇ b') ◇ w(1)) ◇ ... ◇ w(i)) for all i<n. Comparing this with c ◇ d, the words can only match if n=0, c=a', d=b', giving the claim. □

Now we can contradict 3925. It suffices to show that the words x ◇ y, (x ◇ (y ◇ x)) ◇ y are not equivalent. We already know (from the failure of 10) that x and (x ◇ (y ◇ x)) are not equivalent. From unique factorization, we are then done unless we have an edge y → x or an edge y → (x ◇ (y ◇ x)).

If we had an edge y → x, then x ◇ y ~ x. That is to say, every 854 law would obey the left absorption property x ◇ y ~ x (Equation 4). So this is clearly not the case.

If we had an edge y → (x ◇ (y ◇ x)), then (x ◇ (y ◇ x)) ◇ y ~ x ◇ (y ◇ x), and then 3295 would simplify to
x ◇ y = x ◇ (y ◇ x) (Equation 325). But this law is not implied by 854 (this is listed on Equation Explorer, presumably one of the many 854 magmas we have generated will demonstrate this). So we are done!

[Note: the way I came up with this argument was by observing that the greedy approach to building an 854 magma would always either define a ◇ b equal to a, or else to some completely new element c that one never tries to "use" again. This suggested something like a unique factorization property holding true for this greedy model, but I had trouble formalizing this intuition until I returned to the abstract nonsense world of formal words.]

[Matthew Bolan]

I suppose this doesn't apply to the other 4 implications because they are all of the form $x = x \diamond g(x,y,z)$

[Matthew Bolan]

Where is the assumption that $d\to c$ is false used?

[Terence Tao]

Well, 3316 has a decent chance I think; I haven't checked it, perhaps someone else is willing to give it a try.

As for the other three, it may be possible to prove something like the following: in the free magma, the relation w → x (i.e., x ~ x ◇ w) is only true if w ~ (y ◇ z) ◇ (x ◇ z) for some y,z. Then this converts the other three laws back into something involving products for which unique factorization might be useful again.

[Terence Tao]

One needs the falsity of $d \to c$ to exclude the $n>0$ cases, e.g., to prevent $c \diamond d$ from being equal to $(a' \diamond b') \diamond w$ for some $w$.

[Matthew Bolan]

ah, thanks

[Terence Tao]

The conditions $b \not \to a$ and $d \not \to c$ are saying somehow that the products $a \diamond b$, $c \diamond d$ are "irreducible" at the top level. It seems that unique factorization means that every word in the free group has a unique "canonical reduction" in which all products at all levels are irreducible.

[Terence Tao]

This isn't the same as confluence, I think because the edges $b \to a$ can be obtained in a rather complicated fashion; it isn't just using the 854 rule to shorten the word, sometimes you have to lengthen the word as well.

[Matthew Bolan]

So, 3316 being false boils down to showing that we don't have an edge $(y \diamond (x \diamond y)) \to x$ ?

[Terence Tao]

Well, there are two cases. If we don't have an edge, then I think we can conclude by unique factorization since we know from the failure of 10 that $y \diamond (x \diamond y))$ is not equivalent to $y$, and we also know there is no edge $y \to x$. If there is an edge, then the RHS of 3316 collapses to $x$ and I think we again win because of the failure of Equation 4. So, I guess basically the same argument used for 3925 should work for 3316.

[Terence Tao]

Probably we don't have an edge, by the way, and presumably one of the finite magmas we possess will demonstrate that.

[Terence Tao]

Or, one can use the fact (from EE) that law 53 x = x ◇ (y ◇ (x ◇ y)) is not a consequence of 854.

[Terence Tao]

(Now we're really using the full power of Equation Explorer!)

[Terence Tao]

Basically unique factorization + equation explorer seems to tell us quite a lot of information about the free magma for 854

[Michael Bucko]

Michael Bucko schrieb:

Running one more Sage script for 854->1055 with anti-1055 (posting for the reference- hoping to not have a bug here).

# Check 854:
def check_equation_854(table):
    for x in S:
        for y in S:
            for z in S:
                yz = table[y][z]
                xz = table[x][z]
                yz_xz = table[yz][xz]
                lhs = x
                rhs = table[x][yz_xz]
                if lhs != rhs:
                    return False
    return True

# NOT 1055:
# There exists x, z, w, u, v such that:
# w = z ◇ x
# u = u ◇ w
# v = u ◇ x
# x ≠ x ◇ v
def check_not_equation_1055(table):
    for x in S:
        for z in S:
            w = table[z][x]
            for u in S:
                # Check if u = u ◇ w
                if table[u][w] != u:
                    continue
                v = table[u][x]
                # Check if x != x ◇ v
                if table[x][v] != x:
                    return True  # Yay!
    return False

It was running for 3 hours. No result.

[Terence Tao]

OK here are a few more basic facts about the free magma.

Call a word "irreducible" if it is not of the form a ◇ b with b → a; that is to say, it is either one of the generators x, y, or else is of the form a ◇ b with no edge of the form b → a. Clearly if a word is reducible then it is equivalent to the shorter word a, so on iterating we see that every word is equivalent to an irreducible word. Unique factorization then says that this irreducible word is unique up to replacing its factors by equivalent words. So every word in fact has a unique "totally irreducible" equivalent, in which every term in the word is irreducible.

A modification of the syntactic analysis shows that if one performs rewrites to an irreducible word a ◇ b, then the only words one can reach are of the form ((a' ◇ b') ◇ w(1)) ... ◇ w(n) where a' ~ a, b' ~ b, and for each i<n, the word w(i+1) is equivalent to a word of the form (Y ◇ Z) ◇ (X ◇ Z) where X ~ ((a' ◇ b') ◇ w(1)) ... ◇ w(i). (I use capital letters here because I am reserving x, y for the generators of the free magma.) This completely describes all the words equivalent to a ◇ b, and so we conclude that W → a ◇ b if and only if W ~ (Y ◇ Z) ◇ ((a ◇ b) ◇ Z) for some Y, Z. Similarly if a ◇ b is replaced by one of the generators x, y. Since every word is equivalent to one of these irreducible forms, we conclude

Description of graph. Let X, W be words in the free group. Then W → X if and only if W ~ (Y ◇ Z) ◇ (W ◇ Z) for some words Y, Z.

Informally, the only way (up to equivalence) to generate edges in this graph is from the obvious way of just applying 854.

This description may help make some headway with the other open implications 413, 1045, 1055. It won't be as easy as with 3316 and 3925 in which we only had to analyze short words though, because now the new words Y, Z are not initially of any bounded size. But perhaps unique factorization can be used to bring them under control.

[Matthew Bolan]

What is U in the description of the graph?

[Terence Tao]

Oops that was a typo, it should have been W.

[Matthew Bolan]

Is there a reason why you restrict to only the open anti-implications here? Is there some automated check done to see if known anti-implications don't contradict unknown ones? Terence Tao said:

Actually this suggests the following exercise for anyone with some spare ATP compute. We have five open implications from 854:  413 x = x ◇ (x ◇ (x ◇ (y ◇ x))), 1045 x = x ◇ ((y ◇ (y ◇ x)) ◇ x), 1055 x = x ◇ ((y ◇ (z ◇ x)) ◇ x), 3316 x ◇ y = x ◇ (y ◇ (x ◇ y)), and 3925 x ◇ y = (x ◇ (y ◇ x)) ◇ y. We know that 1055 implies 1045, but otherwise the five laws have no implications between them. However, if we assume 854, it may be that there are more equivalences here. Over on the 1485 thread, for instance, the open implications from 1485 are to 151, 3456, and 3862; they are not equivalent to each other in the absence of any other axioms, but we also know that assuming 1485, they are equivalent, so really there is just one anti-implication to resolve there. So perhaps there is a similar collapse among the five open implications here, and if so that should be able to be picked up by standard ATP queries. This may help clarify which of these laws are the easiest to attack.

[Matthew Bolan]

I guess I am asking if there is any work done on understanding the implication graphs for the remaining equations -- in an 854 magma, which laws are known to imply which others?

[Matthew Bolan]

I suppose for 854 the most interesting anti-implications we know come from this 12-element magma, which we know doesn't resolve anything open.

[Amir Livne Bar-on]

I formalized 854+anti1055 and 854+anti413 as integer linear programs. It takes a few minutes to run through all 5-element multi-valued magmas and prove there are no solutions. I'm running now with 6-elements, this will probably take a few hours to complete.

But the fact it works at all means that maybe we can use ILP solvers to find interesting magmas for 854. What's an interesting property? I wasn't following the discussion too closely. We can look for counter-examples to 10 with specific properties for instance.

[Michael Bucko]

Amir Livne Bar-on schrieb:

I formalized 854+anti1055 and 854+anti413 as integer linear programs.

Could you please share those programs? (I'm always learning from those examples)

[Michael Bucko]

(deleted)

[Amir Livne Bar-on]

Sure, here's the code: scip_854.py

[Terence Tao]

Matthew Bolan said:

I guess I am asking if there is any work done on understanding the implication graphs for the remaining equations -- in an 854 magma, which laws are known to imply which others?

In principle we could look at all of the 4660 equations not implied by 854, and see what the implication graph among those equations is assuming 854, but this is basically repeating the entire project, but now for 854 magmas, and seems like quite a lot of work. It could potentially give a little bit of insight as to how the five (or maybe now just three) outstanding implications relate to each other, but it seems like quite a bit of effort for relatively little reward right now.

That said, it has been proposed multiple times that this project could be extended at some point to study things like "Do Law X and Law Y jointly imply Law Z"? Certainly many of our techniques would carry over, but the project seems to be significantly larger in scale, and likely to contain many more extremely difficult implications, than our current project.

[Mario Carneiro]

Terence Tao said:

I think I've gotten a way to get abstract nonsense (or "syntactic" arguments) to get new anti-implication, namely that 854 x = x ◇ ((y ◇ z) ◇ (x ◇ z)) does not imply 3925 x ◇ y = (x ◇ (y ◇ x)) ◇ y, but I'm not 100% sure about this, it's sort of a weird argument, mostly taking advantage of the fact that the 854 law is of the left-absorbent form x = x ◇ f(x,y,z) for some word f(x,y,z).

It seems to work! equational#745

[Terence Tao]

That was incredibly fast!

[Terence Tao]

I was still writing up the blueprint proof lol

[Mario Carneiro]

Can someone help me figure out how to prove these theorems:

theorem not_l4' : ∃ (G : Type*) (_ : Magma G), Equation854 G ∧ ¬Equation4 G := sorry
theorem not_l10' : ∃ (G : Type*) (_ : Magma G), Equation854 G ∧ ¬Equation10 G := sorry
theorem not_l325' : ∃ (G : Type*) (_ : Magma G), Equation854 G ∧ ¬Equation325 G := sorry

[Mario Carneiro]

I thought that was the blueprint :)

[Mario Carneiro]

I do find this kind of technique interesting, effectively the free magma lets us "superimpose" a bunch of counterexample magmas into one magma where all of the non-implications hold simultaneously

[Mario Carneiro]

It would be interesting to see if it's possible to prove it without free magmas

[Terence Tao]

We have 'Facts' to establish not_l4', not_l10', not_l325' that are somewhere in the Lean codebase

[Terence Tao]

In principle this script of @Amir Livne Bar-on should help find them

[Terence Tao]

For 4 and 10, one can find a counterexample by using the main result of https://github.com/teorth/equational_theories/blob/main/equational_theories/Generated/All4x4Tables/Refutation870.lean to refute for instance 1038, which is a special case of both 4 and 10.

[Terence Tao]

For 325, one can similarly use https://github.com/teorth/equational_theories/blob/main/equational_theories/Generated/All4x4Tables/Refutation82.lean to refute the special case 307

[Mario Carneiro]

But Refutation82 doesn't prove 854?

[Terence Tao]

This is what I see:

/-! The facts -/
@[equational_result]
theorem «Facts from FinitePoly x² + x * y % 2» :
  ∃ (G : Type) (_ : Magma G) (_: Finite G), Facts G [10, 11, 106, 109, 111, 371, 378, 433, 434, 442, 443, 854, 1043, 1053, 1247, 1257, 1265, 1271, 1855, 1863, 3285, 3306, 3321, 3726, 3727, 3895, 3931, 4087, 4293, 4318, 4673] [47, 102, 115, 117, 118, 124, 125, 127, 151, 203, 255, 307, 412, 416, 417, 419, 420, 463, 464, 466, 467, 473, 474, 476, 477, 500, 501, 503, 504, 510, 511, 513, 614, 822, 825, 826, 869, 870, 872, 873, 879, 880, 882, 883, 906, 907, 909, 910, 916, 917, 919, 1021, 1026, 1029, 1072, 1073, 1075, 1076, 1082, 1083, 1085, 1086, 1109, 1110, 1112, 1113, 1119, 1120, 1122, 1232, 1275, 1276, 1278, 1279, 1285, 1286, 1288, 1289, 1312, 1313, 1315, 1316, 1322, 1323, 1325, 1426, 1629, 1833, 1837, 1838, 1840, 1841, 1848, 1858, 1884, 1885, 1887, 1888, 1894, 1895, 1897, 1898, 1921, 1922, 1924, 1925, 1931, 1932, 1934, 2035, 2238, 2441, 2644, 2847, 3050, 3254, 3258, 3259, 3261, 3262, 3268, 3269, 3271, 3272, 3281, 3308, 3309, 3342, 3343, 3345, 3346, 3352, 3353, 3456, 3664, 3667, 3668, 3674, 3675, 3678, 3712, 3714, 3722, 3748, 3749, 3751, 3752, 3759, 3761, 3863, 3868, 3871, 3877, 3880, 3890, 3917, 3918, 3924, 3927, 3951, 3952, 3954, 3955, 3961, 3962, 3964, 4074, 4080, 4118, 4120, 4121, 4127, 4128, 4130, 4155, 4157, 4158, 4164, 4165, 4167, 4268, 4272, 4273, 4275, 4276, 4283, 4284, 4290, 4291, 4320, 4321, 4343, 4380, 4585, 4587, 4599, 4605, 4629, 4635, 4658] :=
    ⟨Fin 2, «FinitePoly x² + x * y % 2», Finite.of_fintype _, by decideFin!⟩

854 is listed there as something that is obeyed I think

[Mario Carneiro]

oh there are multiple Refutation82's, you meant https://github.com/teorth/equational_theories/blob/main/equational_theories/Generated/FinitePoly/Refutation82.lean

[Terence Tao]

Oh sorry oops I was doing all this manually. (I couldn't get Amir's script to build the big json file, something to do with Windows maximum path length or some such nonsense)

[Mario Carneiro]

all fixed now

[Douglas McNeil]

@Amir Livne Bar-on : FWIW I got the dreaded "unsatisfiable" via sat on 854 + at least one 413 violation up to order ~8 I think, maybe 9. Can't remember offhand how high I got for 10, but it wasn't enough to rule out a smaller example than 11. That might be as much a measure of how well I was coding before bed that day as anything, of course. ;-)

[Amir Livne Bar-on]

Kind of odd that we can't get at the file names, but anyway here's the file, generated 2 days ago on commit a1d9acd6:
full_entries.json

[Amir Livne Bar-on]

Douglas McNeil said:

Amir Livne Bar-on : FWIW I got the dreaded "unsatisfiable" via sat on 854 + at least one 413 violation up to order ~8 I think, maybe 9. Can't remember offhand how high I got for 10, but it wasn't enough to rule out a smaller example than 11. That might be as much a measure of how well I was coding before bed that day as anything, of course. ;-)

Was this for magmas or for multi-magmas? In any case, sounds like SAT is a better fit for this problem than integer programming.

[Douglas McNeil]

Only magmas (assuming multimagmas are the multivalued magmas of the relaxation conversation?) but I don't trust negative results I produce anyway.. too easy for me to accidentally overconstrain and not realize it because I'm still getting enough of what I expect to see.

That said, I'd be happy if someone proved there were no finite counterexamples!

[Terence Tao]

Moot now, but I got the script to work with the json provided.

PS C:\Users\teort\Dropbox\Lean\equational_theories> py scripts/explain_implication.py Equation854 Equation10
Equation10 => Equation3935
    RewriteHypothesis.Equation10_implies_Equation3935  in  Generated/TrivialBruteforce/theorems/RewriteHypothesis.lean
Equation854  has a model that does not satisfy  Equation3935
    «Facts from FinitePoly [[2,3,0,4,0,10,0,10,0,7,7],[1,5,6,1,8,1,8,8,6,1,6],[2,9,6,2,2,2,2,2,9,2,6],[2,3,3,2,3,9,3,9,3,7,7],[4,5,4,4,8,4,5,8,4,4,4],[2,5,5,2,5,9,5,2,5,5,5],[6,5,6,6,8,6,5,8,6,6,6],[4,3,7,4,5,4,5,8,7,7,7],[8,9,6,8,8,8,8,8,9,8,6],[2,9,9,2,9,9,9,9,9,4,4],[2,9,9,2,10,10,10,10,9,2,6]]»  in  Generated/All4x4Tables/Refutation870.lean
PS C:\Users\teort\Dropbox\Lean\equational_theories> py scripts/explain_implication.py Equation854 Equation4
Equation4 => Equation3722
    Subgraph.Equation4_implies_Equation3722  in  Subgraph.lean
Equation854  has a model that does not satisfy  Equation3722
    «Facts from FinitePoly x² + x * y % 2»  in  Generated/FinitePoly/Refutation82.lean
PS C:\Users\teort\Dropbox\Lean\equational_theories> py scripts/explain_implication.py Equation854 Equation325
Equation325 => Equation307
    SimpleRewrites.Equation325_implies_Equation307  in  Generated/SimpleRewrites/theorems/Rewrite_yx.lean
Equation854  has a model that does not satisfy  Equation307
    «Facts from FinitePoly x² + x * y % 2»  in  Generated/FinitePoly/Refutation82.lean

[Terence Tao]

@Mario Carneiro It's not super urgent, but if at some point you are able to update your proof of 854 !=> 3925 to also refute 3316 that would be great (it's almost the same argument, re-using the same facts not_l4', not_l10, not_l325'; see https://teorth.github.io/equational_theories/blueprint/854-chapter.html). I could try to modify the code myself but I would probably make it much clunkier as a result.

[Mario Carneiro]

equational#749

[Mario Carneiro]

one fun fact here is that X ≠ X ◇ (Y ◇ X) and Y ≠ Y ◇ (X ◇ Y) are actually different theorems, you have to prove them separately, making use of the fact that X and Y are generators of the free group. So now there are two versions of not_l10 in the proof

[Amir Livne Bar-on]

Amir Livne Bar-on said:

I'm running now with 6-elements.

The order 6 run took a bit more than an hour (and failed for both anti-axioms), and order 7 has been running since and is going to take a while

[Michael Bucko]

Terence Tao schrieb:

This script is very useful working on their learning Lean skills and exploring the graph.

(equational_theories) riccitensor@insight equational_theories % python3 scripts/explain_implication.py --entries-file ./full_entries.json Equation854 Equation1054
Equation1054 => Equation1047
    SimpleRewrites.Equation1054_implies_Equation1047  in  Generated/SimpleRewrites/theorems/Rewrite_wz_zx.lean
Equation1047 => Equation650
    Equation1047_implies_Equation650  in  Generated/VampireProven/Proofs1.lean
Equation650 => Equation448
    Equation650_implies_Equation448  in  Generated/VampireProven/Proofs11.lean
Equation448 => Equation441
    Equation448_implies_Equation441  in  Generated/VampireProven/Proofs10.lean
Equation441 => Equation4
    Equation441_implies_Equation4  in  Generated/VampireProven/Proofs10.lean
Equation4 => Equation3
    Subgraph.Equation4_implies_Equation3  in  Subgraph.lean
Equation854  has a model that does not satisfy  Equation3
    Magma2c.Facts  in  SmallMagmas.lean

[Eric Taucher]

Terence Tao said:

build the big json file, something to do with Windows maximum path length or some such nonsense

Had same/similar problem

@Richard Copley noted a work around.

I was able to get an exe by writing the arguments to a file args.txt then invoking leanc as leanc.exe @args.txt.

It is noted in this topic with the specific problem being solved with the help of @Richard Copley starting with this reply.

[Eric Taucher]

If you want just the exact steps that worked in my case for the Windows command line length problem, they are in this reply.

[Michael Bucko]

Mario Carneiro schrieb:

equational#749

Inspiring proof! (and thank you for your suggestions)
Asking questions related to the proof and the techniques here (while playing with not_1055)- https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/not_1055.20for.20beginners/near/479252733

[Michael Bucko]

Re 854 not 1055: could we use a similar line to the other proofs from @Mario Carneiro ?

Something like this:

• refine (find witnesses to existential qualifier) the core theorem (needs to be found) using unique factorization (another 1-3 theorems need to be found?), and a custom relation (to be found) to optimize for contradiction potential (in rather few steps)

What's the blocker here?

Also, given that we can (very efficiently) write software / train models / do atp and so on, is there any way to "bootstrap" those proofs with lines (like the one above)?

For the reference, the three theorems from Mario:

theorem not_l4 : X ≠ X ◇ Y := by
  refine fun h => let ⟨G, _, h1, h2⟩ := not_l1038'; h2 fun x y => ?_
  let φ := FreeMagmaWithLaws.evalHom (fun | 0 => x | _ => (y ◇ (x ◇ y)) ◇ x) <|
    Law.satisfiesSet_singleton.2 <| (Law854.models_iff _).2 h1
  simpa [MagmaHom.map_op, X, Y, φ] using congrArg φ h

theorem not_l10_2 : Y ≠ Y ◇ (X ◇ Y) := by
  refine fun h => let ⟨G, _, h1, h2⟩ := not_l1038'; h2 fun x y => ?_
  let φ := FreeMagmaWithLaws.evalHom (fun | 1 => x | _ => y ◇ (x ◇ y)) <|
    Law.satisfiesSet_singleton.2 <| (Law854.models_iff _).2 h1
  simpa [MagmaHom.map_op, X, Y, φ] using congrArg φ h

theorem not_l325 : X ◇ Y ≠ X ◇ (Y ◇ X) := by
  refine fun h => let ⟨G, _, h1, h2⟩ := not_l307'; h2 fun x => ?_
  let φ := FreeMagmaWithLaws.evalHom (fun _:ℕ => x) <|
    Law.satisfiesSet_singleton.2 <| (Law854.models_iff _).2 h1
  simpa [MagmaHom.map_op, X, Y, φ] using congrArg φ h

And the custom relation:

def Rel (x y : G) := ∃ z, y = z ◇ x
local infix:50 " ⇝ " => Rel

theorem rel_iff {x y} : x ⇝ y ↔ y = y ◇ x := ⟨fun ⟨_, H⟩ => H ▸ l378 .., fun H => ⟨_, H⟩⟩

[Mario Carneiro]

It would be a good benchmark to try to get an ATP to at least reproduce the disproof of 3925 if you give it all the facts we used (the non-theorems, the unique factorization theorem and the main law and possibly the derived laws too)

[Ibrahim Tencer]

Mario Carneiro said:

one fun fact here is that X ≠ X ◇ (Y ◇ X) and Y ≠ Y ◇ (X ◇ Y) are actually different theorems, you have to prove them separately, making use of the fact that X and Y are generators of the free group. So now there are two versions of not_l10 in the proof

I know nothing about Lean but is there not some way to combine the proofs? At the very least by using an automorphism of the free group or something.

[Mario Carneiro]

yes, but that is literally what those lines are already doing

[Mario Carneiro]

if it came up more than a few times we could process it a bit more to get the line count down

[Mario Carneiro]

in particular, at the very least you need to prove that i != j in order to instantiate that for arbitrary generators Leaf i and Leaf j instead of X := Leaf 0 and Y := Leaf 1

[Terence Tao]

Here is a different way to view the recent proofs of the anti-implications. Let $M$ be the free magma on some generators, say $X,Y$. To avoid some confusion I will denote the free magma operation on $M$ by $*$ rather than $\diamond$. Define a relaxed magma $M_R$ with the same carrier as $M$ but with the multi-valued magma operation

$w \diamond w' = \{ w * w', w \}$
thus the product of $w$ and $w'$ is either the usual product $w * w'$, or just the left entry $w$. Intuitively, this models a "sometimes left-absorptive" magma operation.

Finally, let $M_{854}$ be the free magma on the same generators $X,Y$ modulo the law 854. Then unique factorization tells us that there is an injective homomorphism from $M_{854}$ to $M_R$, that maps each word to its unique totally irreducible representation, where totally irreducible means that it is either a generating variable, or of the form $w \diamond w'$ where $w,w'$ are totally irreducible and $w' \not \to w$. The existence of this injective homomorphism is coming from the (sometimes) left-absorptive nature of the law 854; we would not expect this behavior for say 1485 for instance.

Now consider for instance the law 3925 $x \diamond y = (x \diamond (y \diamond x)) \diamond y$. In order for this to hold in the relaxed magma $M_R$ for a given choice of $x,y$, a case check shows that one of the following must hold for the various interpretations used for $\diamond$ in order for this identity to hold:

1. $x = x \diamond (y \diamond x)$. (Equation 10)
2. $x \diamond y = x$. (Equation 4)
3. $x \diamond y = x \diamond (y \diamond x)$ (Equation 325).

Hence if 3925 is to hold in the injective copy of $M_{854}$, one of these three laws must hold in $M_{854}$ itself for the generating variables $X,Y$, and hence be true in every 854-obeying magma for all choices of variables by universality; but we have counterexamples to refute all three possibilities. A similar argument refutes 3316.

This doesn't help us with the other three open anti-implications, but I think it clarifies a little bit what is going on. We're still using custom designed magmas to refute implications; it's just that now we found one which is a relaxed magma rather than a genuine magma.

[Michael Bucko]

So the path for 3925 to hold in M854 was (at least) through 10, 4 or 325, but we can find counterexamples that deny those paths, so 854 can't imply 3925.

We might need to find more aggressive ways of finding those paths / counterexamples (compute seems to be a major limitation). We're currently considering relaxed magmas - could relaxed implication chains be a thing?

So far, my transformer check didn't work (DeepSeek). Tactic generation based on the existing proofs based on the DeepSeek model didn't work.

I'm switching to LeanDojo & will be experimenting (code + llm + lean combined).

[Amir Livne Bar-on]

There are two reasons why this proof search might fail: either the prover is not good enough to generate proofs, or the other ones are more difficult/ very different from the training data.aybe we can check whether it can prove one of the non-implications after seeing the other two?

[Michael Bucko]

Amir Livne Bar-on schrieb:

There are two reasons why this proof search might fail: either the prover is not good enough to generate proofs, or the other ones are more difficult/ very different from the training data.aybe we can check whether it can prove one of the non-implications after seeing the other two?

I always provide them with more information. But even that didn't help the current Lean tactic generators. I shared one notebook that uses DeepSeek for generating tactics in a different thread. Check it out, esp. using a longer context.

On the ATP side, I still need more time, but I guess we simply need to give them all the facts we know (Mario mentioned that too). This also means that we need to generate those facts efficiently.

@Adam Topaz will soon put his pretrained transformer on HF, and we might be able to use Spaces and Autotrain to experiment.

EDIT: What I am using now is Cursor with LLMs. And soon, hopefully today, LeanDojo.

[Matthew Bolan]

I'd like to think aloud about what unique factorization tells us about whether 854 implies 413 (x = x ◇ (x ◇ (x ◇ (y ◇ x)))). IIUC, by unique factorization, $x \sim x ◇ (x ◇ (x ◇ (y ◇ x))))$ iff $(x ◇ (x ◇ (y ◇ x)))) \sim (a ◇ b) ◇ (x ◇ b)$ for some words $a,b$. Now, as $(x ◇ (y ◇ x)) \not \to x$ by equation 49, $(y ◇ x) \not \to x$ by equation 10, and $x \not \to y$ by equation 4, (x ◇ (x ◇ (y ◇ x)))) is "totally irreducible", so I think unique factorization gives us strong constraints on what a and b can be. Is this kind of analysis correct and worth pursuing further?

[Terence Tao]

Yes, I think so far so good. The next logical step is to divide into two cases, depending on whether $x \diamond b \to a \diamond b$ or not. As you point out, the key issue is to constrain $a$ and $b$, which currently can be words of unbounded length. In some cases we can "eliminate quantifiers" and remove an unbounded variable by using Law 378, which converts a statement such as "There exists $a$ such that $a \diamond b = c$" to just "$c \diamond b = c$", but this trick doesn't cover all use cases.

[Matthew Bolan]

Can we even say $x\diamond(x\diamond (y\diamond x)) \not \sim (x\diamond(x\diamond(y\diamond x)))\diamond (x\diamond(x\diamond(y\diamond x)))$ ?

[Terence Tao]

I think the free 854 magma contains no idempotents, because we have models of 854 with no idempotents (e.g., the original sporadic order 12 example). So in particular we do know that $x \diamond (x \diamond (y \diamond x))$ is not equivalent to its square. That's a useful additional technique, by the way: if law fails for every choice of variable in some model, then it also fails in the universal magma for every choice of variable.

Here's maybe some more notation to fix conventions. As before, $M$ is the free magma on say two generators $X, Y$ (we can add more generators as needed, e.g., to study 1055), with operation $*$. In this magma, no two words are equal; for instance, $(X*Y)*Y$ is not equal to $X*Y$, despite this equality holding for all 854 magmas. In particular $M$ does not obey 854. We can view the free magma $M_{854}$ for 854 as a modified submagma of $M$, where the carrier consists of all the completely irreducible words in $M$, and the operation $\diamond$ is given by $x \diamond y = x \hbox{ or } x * y$, depending on whether $y \to x$ is true or not (or equivalently, whether $x*y$ is reducible or irreducible). One can think of $x \diamond y$ as a "reduced" version of $x*y$, in which one uses the law 854 to try to reduce the product if possible. We don't have full understanding of the relation $y \to x$, and as such we don't fully know how to compute $x \diamond y$ for all $x, y$, but thanks to EE and existing finite models, we understand a very large fraction of this relation. For instance, we know enough to say that $X * (X * (Y * X))$ is completely irreducible (because none of the laws $x = x \diamond (x \diamond (y \diamond x))$ (equation 49), $x = (x \diamond (y \diamond x))$ (equation 10), or $y = y \diamond x$ (equation 4) are consequences of 854), so in particular $X \diamond (X \diamond (Y \diamond X)) = X * (X * (Y * X))$, but it is currently open whether $X * (X * (X * (Y * X)))$ is completely irreducible: $X \diamond (X \diamond (X \diamond (Y \diamond X)))$ could be equal to either $X$ or $X * (X * (X * (Y * X)))$, depending on whether 413 is a consequence of 854 or not. Roughly speaking, we can fill out all small entries of the $M_{854}$ multiplication table except for those involving 413, 1045, or 1055.

One thing we do know is that for $x,w \in M_{854}$, that $x \diamond w = x$ (i.e., $w \to x$) if and only if $w = (y \diamond z) \diamond (x \diamond z)$ for some $y,z \in M_{854}$. Unfortunately we do not have any bounds of the length of $y,z$ in terms of $x,w$, so this does not reduce the verification of the $\to$ relation to any finite search yet. But it is something.

[Matthew Bolan]

That's great if we know models with no idempotents, I ran into the above case at least once.

[Matthew Bolan]

Where can I find such models, is it the 12 element one again? Oh I missed the part of your message where you said this

[Douglas McNeil]

Order 12 is overkill for non-idempotency, even [[2, 0, 0],[1, 0, 1],[2, 2, 1]] is 854. :-)

[Terence Tao]

That could be a useful little model to keep in mind to quickly establish some non-implications $y \not \to x$. In particular, since in this order 3 model the $\to$ relation is just the $\neq$ relation, we see that we will have $y \not \to x$ whenever $x$, $y$ are words that can map to the same element of this order 3 model. (This generalizes the previous observation that $x \not \to x$, i.e., no idempotents.)

[Terence Tao]

Algebraically, this model is ${\mathbb Z}/3{\mathbb Z}$ with $x \diamond y$ equal to $x$ if $x \neq y$, and $x-1$ if $x=y$, or more compactly $x \diamond y = x - 1_{x=y}$. Even more algebraically, $x \diamond y= x + (x-y)^2 - 1$.

[Terence Tao]

I wonder if the other finite magma models we have are extensions of this model, for instance can the order 12 model have their 12 elements be grouped into three classes so that the multiplication table looks like a block version of the order 3 model? (Class 0 ◇ Class 0 = Class 2, Class 0 ◇ Class 1 = Class 0, etc.) If so, this may be a good way to try to focus the search for finite models.

[Ibrahim Tencer]

Douglas McNeil said:

Order 12 is overkill for non-idempotency, even [[2, 0, 0],[1, 0, 1],[2, 2, 1]] is 854. :-)

Yes and this is one example of the class of models that are left-absorptive except on the diagonal, all of which have no idempotents.

[Terence Tao]

I guess one should plot the complementary graph of non-edges $y \not \to x$ for say the order 12 model. If this complementary graph breaks up into three or more connected components, then there is a chance for this graph to be an extension of the order 3 model, or more generally one of Ibrahim's models. It looks like there may be a few too many non-edges for this to be the case, though.

[Matthew Bolan]

Continuing my above thoughts, we know that x=x◇(x◇(x◇(y◇x)))) iff (x◇(x◇(y◇x))))=(a◇b)◇(x◇b) for some elements a,b. I think we cannot have $(x \diamond b) \not \to (a \diamond b)$. If this were the case, then $x\diamond(x\diamond(y\diamond x)) = (a \diamond b) \diamond (x \diamond b)$ together with unique factorization imply $(a \diamond b) = x$, and thus $(a \diamond b) = (a \diamond b) \diamond b = x \diamond b$. Now $x\diamond(x\diamond(y\diamond x)) = (a \diamond b) \diamond (a \diamond b),$ and the fact about idempotents means we don't have an arrow $(a \diamond b) \to (a \diamond b)$, so $x = (a \diamond b) = x\diamond(y\diamond x)$, violating the fact 854 does not imply equation 10.

In the case $(x \diamond b) \to (a \diamond b)$, I also think we cannot have $a \not \to b$. Suppose otherwise. Then $x\diamond(x\diamond(y\diamond x)) = (a \diamond b) \diamond (x \diamond b) = a \diamond b$ together with unique factorization tells me $a = x$ and $b = x\diamond(y\diamond x))$, so $x\diamond(x\diamond(y\diamond x)) = (a \diamond b) \diamond (x \diamond b) = (x \diamond(x\diamond(y\diamond x)))) \diamond (x \diamond(x\diamond(y\diamond x))))$, which we found impossible above.

In the final case, $(x \diamond b) \to (a \diamond b)$ and $a \to b$ tells me $x\diamond(x\diamond(y\diamond x)) = (a \diamond b) \diamond (x \diamond b) = (a \diamond b) = a$, but I haven't found a contradiction coming from this yet.

[Matthew Bolan]

Checked this last chain of equalities against the 12 element magma and 3 element one mentioned here, no dice. To falsify it we want to find a magma such that there exist $x,y$ such that for all $a,b$ the equalities x⋄(x⋄(y⋄x))=(a⋄b)⋄(x⋄b)=(a⋄b)=a do not hold. I think there is actual content in the first two cases I did (For example, it looks like the 12 element magma doesn't rule them out either), so this last case has a chance of being dealt with by something we know about?

[Matthew Bolan]

Maybe I'll break out the SAT solver on that after dinner, though I should probably stop obsessing over this and do the math my advisor actually wants me to do soon

[Michael Bucko]

(deleted)

[Terence Tao]

Obviously your "day job" comes first :). But this may well be an actual reduction of the problem. It feels like one is now adding a lot more axioms to constrain the magma and so we may be able to find counterexamples faster and for larger magmas than we did before. And it can't be harder than the original problem, since if your chain of equalities always hold for some a,b then by 854 we conclude that 413 holds as well.

[Terence Tao]

Pushing your final case analysis a bit further. You've already pinned down $a$ completely as $a = x \diamond (x \diamond (y \diamond x))$, which is great. The remaining conditions in the scenario are that $b, x \diamond b \to a$ (you wrote $a \to b$ but I think you meant $b \to a$). The second condition $x \diamond b \to a$ can be unfolded as $x \diamond b = (c \diamond d) \diamond (a \diamond d)$ for some $c,d$. Now we can split into cases:

1. $(a \diamond d) \not \to (c \diamond d)$. Then by unique factorization (and because $x$ was already irreducible) we must have $b \not \to x$, $x = c \diamond d$, and $b = a \diamond d$. The scenario here is thus that there exists $d$ such that $a \diamond d \to a$, $a \diamond d \not \to x$, and $d \to x$. Conversely, if this scenario holds, then $b := a\diamond d$ is such that $(a \diamond b) \diamond (x \diamond b) = a \diamond ((x \diamond d) \diamond (a \diamond d)) = a$, so that $x \diamond (x \diamond (x \diamond (y \diamond x))) = x \diamond a = x$ giving 413, so this is a scenario that we actually have to rule out.
2. $(a \diamond d) \to (c \diamond d)$. So now $x \diamond b = c \diamond d$, so the conditions are $b \to a$, $d \to x \diamond b$, and $a \diamond d \to x \diamond b$. Conversely, if $b,d$ obey these conditions, then $x \diamond b = c \diamond d$ for some $c$, and $x \diamond b = (c \diamond d) \diamond (a \diamond d)$, hence $(a \diamond b) \diamond (x \diamond b) = a \diamond ((c \diamond d) \diamond (a \diamond d)) = a$ and we again get 413. So again we need to rule out this scenario.

It's possible that we can find one finite magma that rules out scenario 1, and a separate finite magma that rules out scenario 2, and then by the magic of free magmas, we get to rule out 413 holding universally. We could keep splitting these scenarios into further and further subscenarios - if some of them start getting ruled out by finite examples then this approach has some potential, as long as somehow our ability to find finite counterexamples "outruns" the branching of the scenarios.

[Terence Tao]

If we can somehow nudge the case analysis towards scenarios where there are many more constraints than free variables then it raises the chance that e.g., the order 3 magma can be used to rule those scenarios apart. For instance, from the pigeonhole principle and the order 3 magma we can't have four words $w_1,w_2,w_3,w_4$ such that $w_i \to w_j$ for all $1 \leq i < j \leq 4$. In fact, the undirected version of the graph on $M_{854}$ must be 3-colorable!

[Matthew Bolan]

Perhaps I've done something wrong but it looks like the 12 element magma falsifies your condition 1 (x=1, y=0). I see you've just edited though.

[Terence Tao]

I'll check with my own Python code. This may take a while.

[Terence Tao]

One thing is that homomorphisms preserve the $\to$ relation but not necessarily the $\not \to$ relation.

[Douglas McNeil]

[ehh, foolishness!]

[Terence Tao]

OK, according to my python code, in the 12 element magma if one sets x=1, y=0, then a=2, and the only d that obeys $d \to a$, $d \to x$ is d=2. Now, it is true that we have $a \diamond d \to x$ in the 12-element magma in this case, but unfortunately this doesn't guarantee that this happens back in the free magma $M_{854}$; the homomorphism doesn't work in both directions. Nevertheless, this magma is putting a little bit of a constraint on the possible values of $d$ in $M_{854}$; it has to map to $2$ under the homomorphism that sends $x$ to $1$ and $y$ to $2$. This could possibly be useful later under some more case analysis. Also, the fact that 11 out of the 12 options of $d$ were ruled out by this one randomly selected magma gives some hope; maybe a tweaked version of this magma rules out all options.

[Matthew Bolan]

Ah, i definitely missed this fact about $\not \to$ not being preserved by homomorphism in my original claim about the 12 element magma.

[Terence Tao]

Yeah, I didn't notice it either until we had this discussion. So it seems that we would greatly prefer to start seeing a lot of $\to$ constraints in our scenarios than a lot of $\not \to$ constraints, as we can use finite magma models (or any other model we happen to get our hands on) to then create contradictions. On the other hand, $\not \to$ constraints are good for other reasons - they guarantee irreducibility of certain products, allowing one to use unique factorization.

[Douglas McNeil]

Let me try again (my previous mistake was that I only looked at violating the adjacent equalities in x⋄(x⋄(y⋄x))=(a⋄b)⋄(x⋄b)=(a⋄b)=a, which was a lot easier than ensuring all the pairs were distinct). What properties should magmas have (in a ⋄ sense, not a → sense) which would help at this point?

[Terence Tao]

I guess that, given that directly finding a 413 counterexample is hard, we can assume that 413 holds (and similarly for 1055/1045) to try to speed up the ATP. Possibly we could even assume that 10 holds, though one might first want to ask an ATP if 10+854 is strong enough to rule out any of the scenarios we are proposing.

[Terence Tao]

To be a bit more precise, consider the following two properties that an 854 magma may or may not satisfy.

1. Scenario_1: For every $x, y$ there exists $d$ such that $a \diamond d \to a$ and $d \to x$, where $a = x \diamond (x \diamond (y \diamond x))$.
2. Scenario_2: For every $x,y$ there exists $b,d$ such that $b \to a$, $d \to x \diamond b$, and $a \diamond d \to x \diamond b$, where $a = x \diamond (x \diamond (y \diamond x))$.

(So I'm explicitly dropping the $a \diamond d \not \to x$ condition from Scenario_1, as we don't have it for anything except the free magma $M_{854}$.) By the previous discussion, either of these properties implies 413, and if we show that each of these properties fail for at least one magma, then we are done. So we have split the original problem into two easier (or at least not harder) problems.

Unfortunately the 12-element magma doesn't obey Scenario_1 (the best choices for a counterexample are when x=1, but even then there is always one choice of d that blocks you), and the situation is similarly blocked for Scenario_2 (again x=1 is the best option, but I always get 7 options for b,d). Maybe other magmas fare better, though.

[Terence Tao]

I guess we want to try magmas where the relation $\to$ is relatively sparse?

[Matthew Bolan]

I tried all magmas with <= 4 elements in both my original condition and both your scenarios. No luck.

I notice that the 12 element magma satisfies a few laws that 854 is known not to imply - are there more interesting finite magmas falsifying these laws I should try?

[Pace Nielsen]

Continuing the case analysis of @Matthew Bolan it seems like we would take $b=a^2$. Note that 413 is equivalent to saying that $x\diamond a=x$. Thus, with that choice,

$$(a\diamond b)\diamond (x\diamond b)=(a\diamond a^2)\diamond ((x\diamond a)\diamond(a^2)) = a\diamond((x\diamond a)\diamond(a\diamond a))=a.$$

[Pace Nielsen]

Or, at least, that is a major case we would need to rule out.

[Matthew Bolan]

So you're using 413 in the first equality to replace $x$ with $x \diamond a$?

[Matthew Bolan]

That probably destroys any hope of this condition being progress then.

[Terence Tao]

Hmm, the same analysis shows that "Scenario 1" is also implied by 413 (take $c=x$, $d=a$). So, yes, unfortunately we have not actually gained any ground with this approach yet :sad:

[Pace Nielsen]

I believe the same analysis also applies to the other two open implications from 854.

[Matthew Bolan]

Yeah, even though I did nothing, the remaining laws still come down to understanding whatever is going on with the equivalence class of $x$, and we at least know all short words in this class, so it still seems promising to try analysis of this type. I think the reason why I did nothing is that it is somehow not very interesting to do rewrites only in subwords of your equation you already know to be irreducible. A proof of 413 ( x=x◇(x◇(x◇(y◇x))))) from 854 eventually needs to do a rewrite that gets rid of the leftmost multiplication on the righthand side, before then all you have done is replace the irreducible word x and the irreducible word (x◇(x◇(y◇x)))) by things equivalent to them.

[Terence Tao]

Here is a small observation that lets us create some more 854 magmas. Given an 854 magma $G$ with some marked elements $x,y$, one has a relation $\to$ on it by declaring $b \to a$ if $a \diamond b = a$. This then lifts back to a relation $\to_G$ on the free magma $M$ generated by $X$ and $Y$, using the homomorphism that maps $X,Y$ to $x,y$ respectively. One can then say that a word in $M$ is $G$-reduced if it is a single variable or of the form $w_1 * w_2$ where $w_2 \not \to_G w_1$, and completely $G$-reduced if every subword of $w$ is $G$-reduced. Then the set $M_G$ of completely $G$-reduced words is again an 854 magma, where the operation $w \diamond_G w'$ is defined to equal $w * w'$ if $w' \not \to_G w$, and $w$ otherwise. Informally, $M_G$ is the freest 854 magma one can make that has the "same" graph as $G$.

This magma $M_G$ is intermediate between the free magma $M_{854}$ and the original 854 magma $G$, as there are canonical homomorphisms from $M_{854}$ to $M_G$, and from $M_G$ to $G$. It is typically infinite even when $G$ is finite, and has a slightly better chance of disproving laws than the original magma $G$. On the one hand, it has a more explicit description than $M_{854}$ (because we can compute $\to_G$, whereas the corresponding relation $\to$ on $M_{854}$ is only partly understood), so one can check various identities to be true here (in particular, I think this gives a more explicit counterexample for the two anti-implications we recently proved, taking $G$ to be the product of all the finite magmas used as ingredients in the proof). On the other hand, I don't think it will disprove say 413 if the original magma $G$ did not disprove 413. But maybe one can tweak the relation $\to_G$ to get more play here.

Example: take $G$ to be the order 3 magma and mark $x=0$. Then $x \not \to x$, hence $X \not \to_G X$, and so $X \diamond_G X = X * X$. On the other hand $x \diamond x \to x$, hence $X \diamond_G X \to_G X$, so $X \diamond_G (X \diamond_G X) = X$. But $x \diamond x \not \to x \diamond x$, so $(X \diamond_G X) \diamond_G (X \diamond_G X) = (X*X) * (X*X)$. In particular, as one repeatedly squares $X$, one just gets longer and longer words, so in particular $M_G$ is infinite even though $G$ is finite. (Squaring $0$ three times will get you back to $0$ in $G$, but squaring $X$ three times instead gives a rather long word.)

[Terence Tao]

Perhaps a toy problem is to find a new proof of 854 !=> 10 that doesn't go through a large explicit magma like the order 12 example (or the polynomial example that we actually use in the Lean codebase to disprove 10).

[Terence Tao]

Just abstracting an observation implicitly made by @Pace Nielsen : In any 854 magma,and any x, a, the following are equivalent:

1. $a \to x$
2. $x = x \diamond a$
3. $x = c \diamond a$ for some $c$
4. $b, x \diamond b \to a$ for some $b$
5. $x \diamond a^2 \to a$
6. $a \diamond (x \diamond a^2) = a$
7. $a = (c \diamond b) \diamond (x \diamond b)$ for some $b,c$.
8. $a \to x \diamond a^2$.

Proof: Equivalence of 1 and 2, or 5 and 6, is by definition. 3 trivially implies 2, and the converse comes from Law 378. Since $a^2 \to a$, 5 implies 4. If 4 is true, then $a = (a \diamond b) \diamond (x \diamond b)$, giving 7. Law 854 shows that 7 implies 2. If 2 is true, then $a \diamond (x \diamond a^2) = a \diamond ((x \diamond a) \diamond (a \diamond a)) = a$, giving 6. Finally, to show the equivalence of 1 and 8, use the already established equivalence of 1 and 5, together with law 378 which gives $(x \diamond a^2) \diamond a^2 = x \diamond a^2$.

[Matthew Bolan]

I notice that we can say a little bit about how many rewrites two equivalent words are away from eachother. My earlier argument was saying something about the form some of the rewrites in a proof of 413 need to take, and Pace's obstruction to my argument was a direct application of the rewrite I am already trying to do, so maybe there's some sort of descent argument here? If the shortest possible sequence of rewrites actually needs to turn a proper subword $X * A$ into $A$ then we're done.

[Terence Tao]

Right, if we had some way to measure the "complexity" of an edge, and could show that any proof of a target edge $a \to x$ required first locating an edge of equal or "higher" complexity, and similarly for any edge of higher complexity than the target edge, then we are done.

[Matthew Bolan]

Is it possible to prove equation 8 ($x = x \diamond (x \diamond x)$ ) in just 2 rewrites? Toying around with things it feels like (I have not proven anything formal yet, so please take this with a grain of salt!) to prove $X*W\sim X$ for $W$ a totally irreducible word, I always pass through a proof that there exists some auxiliary word $Z$ such that $X*Z\sim X$ and $W*(W*Z) \sim W$, which would mean proving these latter two edges takes fewer rewrites than proving the edge we initially cared about, so in particular $Z \not = W$. In law $8$, the role of $Z$ can be played by $(X*X) *(X *X)$, which allows both of my auxilliary edges to be resolved in a single rewrite. Ah, this last statement was false for $W*(W*Z) \sim W$, this still takes two rewrites

[Matthew Bolan]

Hmm, something is wrong, maybe I've forgotten a condition on Z. Fixed the thing that concerned me, though now there's more questions about whether such a statement holds for law 8.

[Terence Tao]

Hmm, perhaps out of all the words $W$ with $X * W \sim X$, we can try to order them by the number of previous results of the form $X * Z \sim X$ are needed to prove them? In particular, what words $W$ can we prove such a thing without using previous results? Clearly a word of the form $W = (Y * Z) * (X * Z)$ would work; what else is there?

[Matthew Bolan]

Nothing right? If you forbid yourself such rewrites, you forbid yourself to change the righthand side to anything. To turn the lefthand side into just $X$ will then take such a rewrite. Or did you mean rewrites which shorten the word or something?

[Terence Tao]

I guess I was thinking of rewrites that specifically involve the original term $X$. Maybe that isn't the right metric though. Consider the 413 task of trying to see if we can prove $X * (X * (X * (Y * X))) \sim X$. We know that the equivalence $X * (X * (X * Z)) \sim X$ is false for two generators $X,Z$. So if $X * (X * (X * (Y * X))) \sim X$ is to be provable by rewrites, at least one of the rewrites at some point must be able to look inside the term $Y*X$ and use its specific structure somehow. But if we can show that every rewrite applied to $X * (X * (X * (Y * X)))$ either leaves the $Y*X$ term untouched, or else replaces $Y*X$ with an equivalent term, then we know that it can't ever reach $X$ because the same argument would then also give the false statement $X * (X * (X * Z)) \sim X$. If there was some metric on "rewrite distance" that could detect this sort of thing then we could be in business; I had thought "number of uses of a $X * Z \sim X$ type law" might be one such metric, but on further reflection this probably isn't the right one to use.

[Matthew Bolan]

Does vampire think anything of the form $x = x \diamond ( x \diamond ( ...(x \diamond (y \diamond x))...))$ is true?

[Matthew Bolan]

Also, what are the known proofs law 10 fails? Is it only the 12 element magma?

[Matthew Bolan]

Probably I should be trying to do this descent stuff for 10 before attempting 413.

[Michael Bucko]

This operation table satisfies 854, and satisfies 413. Changing (7,7) to 6 does not satisfy not 413 anymore (unfortunately, 845 gets refuted too).

1 0 0 0 0 0 0 0
1 1 1 1 1 1 1 1
2 2 1 2 2 2 2 2
3 3 3 3 3 3 3 3
4 4 4 4 3 4 4 4
5 5 5 5 5 1 5 5
6 6 6 6 6 6 6 6
7 7 7 7 7 7 7 3

[Matthew Bolan]

I get that this satisfies quite a few laws, including law 10. Am I misunderstanding? I notice that both laws you list begin with 413, so perhaps you have an active filter on finite magma explorer.

[Michael Bucko]

Matthew Bolan schrieb:

I get that this satisfies quite a few laws, including law 10. Am I misunderstanding? I notice that both laws you list begin with 413, so perhaps you have an active filter on finite magma explorer.

You're right. I was filtering for 413. Removing "only" in the prev post.

[Michael Bucko]

Also, reframed to "Changing (7,7) to 6 does not satisfy not 413 anymore (unfortunately, 845 gets refuted too)."

Btw. we should be able to filter using multiple equations. That'd enable us to see the implication status in one go, without the need for double filtering.

[Matthew Bolan]

Terence Tao said:

Perhaps a toy problem is to find a new proof of 854 !=> 10 that doesn't go through a large explicit magma like the order 12 example (or the polynomial example that we actually use in the Lean codebase to disprove 10).

By the way, I did wind up programming something which can do computations in this sort of magma (at least for when the seed magma is finite). No idea what to do with it though.

[Michael Bucko]

The diagonal of the operation table can be quite freely modified to keep 845 satisfied. Are there any configs of the diagonal that give us higher chances of refuting 413?

[Michael Bucko]

(deleted)

[Matthew Bolan]

The law is 854, not 845

[Terence Tao]

The three laws we want to disprove can be expressed in $\to$ notation as follows:

• 413: $x \diamond (x \diamond (y \diamond x)) \to x$
• 1045: $((y \diamond (y \diamond x)) \diamond x \to x$
• 1055: $((y \diamond (z \diamond x)) \diamond x \to x$.

On the other hand, law 10 asserts that the relation $\to$ is symmetric: $x \to y$ iff $y \to x$.

With this in mind, it is also natural to consider the reversals of the above laws:

• 413*: $x \to x \diamond (x \diamond (y \diamond x))$, i.e., $(x \diamond (x \diamond (y \diamond x))) \diamond x = x \diamond (x \diamond (y \diamond x))$.
• 1045*: $x \to ((y \diamond (y \diamond x)) \diamond x$, i.e. $(((y \diamond (y \diamond x)) \diamond x) \diamond x = ((y \diamond (y \diamond x)) \diamond x$.
• 1055*: $x \to ((y \diamond (z \diamond x)) \diamond x$, i.e. $(((y \diamond (z \diamond x)) \diamond x) \diamond x = ((y \diamond (z \diamond x)) \diamond x$.

Do we know the status of these laws? For instance, does Vampire determine if they are consequences of 854? What about the various finite magmas that we have? Unfortunately these laws have just a few too many operations to be directly visible in our implication graph, but presumably the methods we have already could be used here.

EDIT: I see that 1045* and 1055* are special cases of 378. The situation is less clear for 413* though.

[Matthew Bolan]

413* is true for all 3 and 4 element 854 magmas, according to my code

[Terence Tao]

I believe I've managed to make a breakthrough on 854. The standard greedy algorithm does not seem to work: picking two elements $a,b$ for which $a \diamond b$ is currently undefined and setting it equal to some new value $c$ can lead to an explosion of other relations being forced. However, I think that if one also imposes the new unique factorization axiom, then the explosion does not occur and one can in fact make the greedy algorithm work, and thus presumably close off all three remaining implications by a suitable choice of seed. I will write up the details now and report back soon.

[Terence Tao]

OK, it turns out that the greedy algorithm didn't close after all, even with the unique factorization property (and some additional axioms I had to add on). I now see a specific obstruction to greedy arguments, which is the following consequence of 854:

Lemma. If $x \diamond y \to x$ and $y \to z$, then $x \to z$.

Proof. By hypothesis, $x = u \diamond (x \diamond y)$ and $z = v \diamond y$ for some $u,v$, then
$z \diamond x = z \diamond (x \diamond ((v \diamond y) \diamond (x \diamond y))) = z \diamond ((u \diamond (x \diamond y)) \diamond (z \diamond (x \diamond y))) = z$
giving the claim. $\Box$

Now suppose that we try to greedily adjoin $a \diamond b = c$ to a partially defined magma, then $b \to c$. The problem is that if one then has a chain $x_1, x_2, \dots, x_n$ in the existing multiplication table such that $x_i \diamond x_{i+1} \to x_i$ for $i=1,\dots,n-1$ and $x_n = b$, the above lemma then forces $x_i \to c$ for all $i=1,\dots,n$. Then for any $y$ with $y \diamond b = x_i$ for some $i$, one has $y \diamond c =y \diamond (c \diamond x_i) = y \diamond ((a \diamond b) \diamond (y \diamond b)) = y$ so now $c \to y$ for all such $y$. And then for any $y,y'$ of that form we have
$y = y \diamond ((y' \diamond c) \diamond (y \diamond c)) = y \diamond (y' \diamond y),$
thus equation 10 has to hold for a large number of existing elements. This is a quite "global" constraint that makes it very difficult to run a greedy argument, and unique factorization does not seem to be effective at ruling out this type of global condition.

The only way out of this I see is if one can prevent the hypothesis $x \diamond y \to x$ from occurring for anything other than $x \diamond x \to x$ which is forced by Equation 8, so as not to make the above Lemma cause a combinatorial explosion. The implication 413 that we are trying to disprove is already of this form, though, so ruling out this scenario is at least as hard as the original problem.

[Matthew Bolan]

I recognize that lemma, it showed up for me when I was trying to get some "rewrite metric" to work.

[Terence Tao]

Curiously, for the order 12 magma this is in fact an if and only if: the assertion "For all $z$, $y \to z$ implies $x \to z$" holds if and only if $x \diamond y \to x$. Not sure if this is true in general.

[Matthew Bolan]

I think I have a proof that is true in general, let me check my notes

[Terence Tao]

That would mean the relation $x \diamond y \to x$ is transitive, which is a little weird

[Matthew Bolan]

very weird, so I'd bet on me having misremembered...

[Terence Tao]

It's also an if and only if for the order 3 magma

[Matthew Bolan]

I can't find the statement in that form in my notes. I was mostly working with the specific question of showing $A \to X$ a proof of 413 would require. The statements I did write down seem to rest heavily on it being that particular case, so I cannot translate them easily, not that I found an analog of this one anyway. I was probably just remembering the direction you already showed. I'll check the other order 3 and 4 magmas (By the way I tabulated a list of them a while ago, IDK if others have larger lists or if people want me to share my list)

[Matthew Bolan]

Ok I had a stupid bug in there for a while, but It seems to be true for all 3 and 4 element magmas

[Matthew Bolan]

854magmas.txt
Here's the python I have been using to check against these small magmas.

[Terence Tao]

I now have a proof of the converse.

Converse Lemma. Suppose that $x,y$ are such that $y \to z$ implies $x \to z$ for all $z$. Then $x \diamond y \to x$.

Proof. Since $y \to x \diamond y$ (by 378), we have $x \to x \diamond y$, thus $(x \diamond y) \diamond x = x \diamond y$. On the other hand, from Equation 101 one has $x \diamond ((x \diamond y) \diamond x) = x$. Thus $x \diamond (x \diamond y) = x$, giving the claim.

So now we have the following odd consequences:

Corollary. The relation $y \leq x$ defined by $x \diamond y \to x$ (or equivalently, $\{ z: y \to z \} \subseteq \{ z: x \to z \}$) is a pre-order.

Corollary. For any $z$, the set $\{ y: y \to z \}$ is upwardly closed with respect to this pre-order.

Corollary. $x \diamond y \to x$ if and only if $x \to x \diamond y$.

So perhaps we need to study this pre-order. One obvious thing to do is to first try to understand the equivalence relation $x \equiv y$ defined by $x \leq y \leq x$, i.e. $x \diamond y \to x$ and $y \diamond x \to y$, or equivalently $\{ z: y \to z \} = \{ z: x \to z\}$. Possibly we may be able to "quotient out" by this equivalence and assume that this equivalence relation is equality (a similar quotienting did help us with identifying finite magmas for an unrelated equation).

[Matthew Bolan]

413 says $(x(yx)) \le x$, which seems strange to me, but I don't have a good grasp on this pre-order yet. In particular, are there elements not equal to $X$ in the same class as $X$ in $M_{854}$?

[Michael Bucko]

Wrote a script for 854N413.

Script

It's modifying the 854 as long as 854 is satisfied or 413 is refuted until it reaches (854 satisfied, 413 refuted). I'd be happy to add more exploration paths / strategies to it.

I'm running it now (if you see any bugs, please let me know).

(@Shreyas Srinivas tagged -- because of the PR related question)

Step 21148:

Current Operation Table:

7 0 0 0 0 0 0 0

0 1 1 1 1 1 1 1

2 2 1 2 2 2 2 2

3 3 3 3 3 3 3 3

4 4 4 4 3 4 4 4

5 5 5 5 5 3 5 5

6 6 6 6 6 6 6 6

7 7 7 7 7 7 7 7

Equation 854 is not satisfied.

Equation 413 is refuted.
--------------------------------------------------

Step 21149:

Current Operation Table:

0 0 0 0 0 0 0 0

0 1 1 1 1 1 1 1

2 2 1 2 2 2 2 2

3 3 3 3 3 3 3 3

4 4 4 4 3 4 4 4

5 5 5 5 5 3 5 5

6 6 6 6 6 6 6 6

7 7 7 7 7 7 7 7

Equation 854 is not satisfied.

Equation 413 is refuted.

[Douglas McNeil]

I suppose I can mention what I've been up to. Lots of "they'd have been very clever if they worked" ideas failed. So I fell back on something which should give me something, basically by relying on the explosion of relations instead of trying to avoid them.

I loop over all the possible "types" of 413 violation (depending on how many elements they involve and in what pattern). For each one, I then exhaustively try to grow the magma in all consistent ways and find a contradiction. Sometimes for a good choice of direction this ends pretty quickly and would work for any order magma with that pattern, and we could formalize it without much difficulty I think to show any 413-violating 854 magma can't have a violation like that.

OTOH sometimes the most efficient end actually depends upon the size as you take advantage of the magma closing in on itself and fill in the x=y line. By the time a magma's >80% full or so the paths are pretty likely to tail off.

So the hope was that this would either (1) show that every initial point terminates, which I can actually do for what I already knew, small magmas <= 7, or (2) find a counterexample (no luck yet, naturally), or as a fallback (3) find a high-density almost consistent magma which would have minimal need for relaxation.

I think I'm going to implement some kind of adaptive strategy: there are magmas which close almost instantly if you pick the right cell and take hours if you take the wrong one, and I spend almost all of my time trying to resolve a relatively few patterns.

[Michael Bucko]

Douglas McNeil schrieb:

I loop over all the possible "types" of 413 violation (depending on how many elements they involve and in what pattern). For each one, I then exhaustively try to grow the magma in all consistent ways and find a contradiction. Sometimes for a good choice of direction this ends pretty quickly and would work for any order magma with that pattern, and we could formalize it without much difficulty I think to show any 413-violating 854 magma can't have a violation like that.

Do you maybe have a script for that? I'd love to have a look.

[Terence Tao]

Matthew Bolan said:

413 says $(x(yx)) \le x$, which seems strange to me, but I don't have a good grasp on this pre-order yet. In particular, are there elements not equal to $X$ in the same class as $X$ in $M_{854}$?

It may be a good idea to try to work out what this pre-order looks like for small words in $M_{854}$, assuming conjecturally that any implication that cannot be proven quickly in Vampire is false. Given your observation about 413, the pre-order may somehow be tied to violations of the 10 axiom $x(yx) = x$ (though the order relation is different, we have $y \leq x$ if $x (xy) = x$). Perhaps if one temporarily assumes 10 as a working axiom, the pre-order simplifies somehow? (Certainly the directed graph becomes symmetric under 10: $x \to y$ iff $y \to x$.)

[Matthew Bolan]

We have some other laws in equation explorer that can be interpreted as saying things about this pre-order by the way

[Matthew Bolan]

Mostly in the "does not imply" column

[Matthew Bolan]

I notice that if $y \le x$, we have $x \to x \diamond y$ and $x \diamond y \to x$ even without assuming law 10.

[Terence Tao]

Law 10, while false in general, seems to be true in many special cases.

[Terence Tao]

I guess it comes down to law 101, which is the special case of law 10 x = x(yx) when y = xz for some z. I.e. we have $x \to x \diamond y$ iff $x \diamond y \to x$. [Edit: 101 gives only one direction of this implication, but the proof of the lemma and converse lemma gives the other.]

[Terence Tao]

Using the order 3 model I see the relation $y \leq x$ is actually quite rare on the free magma $M_{854}$; the words $y, x$ have to be identical on every interpretation of the generators on the order 3 model in order for this relation to have a chance of being true. In particular the 413 law $x(yx) \leq x$ is one of the first non-trivial possibilities (the other is $x \leq x(yx)$, which I guess we could also investigate. Incidentally I think the modification 413* I proposed earlier is actually equivalent to 413 by the above discussion.)

[Matthew Bolan]

Here's an easy observation about this pre-order that I didn't spot until just now for some reason: If $A \le B$ in the free magma, then $A \not \to B$. Indeed, otherwise $A \to B \implies B \to B$, which is false since we have models with no idempotents.

[Matthew Bolan]

Maybe that's a good way to try and avoid $x(yx) \le x$ holding? Is there some reason $x(yx) \to x$ is hard/impossible to cook up?

[Pace Nielsen]

There may also be some potential to the translation-invariant approach to 854. The functional equation we get is

$$f[f(f(x)x^{-1}yf(y)^{-1})f(y)y^{-1} x] = 1.$$

The sort of "quotient" quantity $f(x)x^{-1}$ is playing a major role here. The equation we want to avoid from 413 is $f^3(f(x)x^{-1})=1$.

Using Vampire, we find that the carrier group has to be noncommutative, but we can assume $x^3=1$ if we want to simplify powers. We also find some quick consequences, such as the following (where I set $p:=f(1)\neq 1$)

$$f(p)=f(p^2)=f(p^{-1})=1,$$

$$f(pf(x))=1,$$

$$f(xf(x)^{-1})=1.$$

So, lots of things must map to 1. That last equality is very close to what we want to avoid (up to inverses).

Using Vampire some more, we see that we should be able to take $a,b$ with $f(a)=b, f(b^{-1}a)=b$. So it seems like we may be able to greatly restrict the output of f, mostly to $1,b$ (except for $f(1)$).

[Matthew Bolan]

We have a model $G$ with no idempotents, and a model $H$ where $x(yx) \to x$ always, (for example any left absorbing magma), so maybe some "quotient" of Terry's construction $M_{G \times H}$ is worth trying?

[Terence Tao]

@Pace Nielsen huh, so in contrast to the other equations, 854 is not known to be immune to a pure translation invariant approach? That's worth looking into. In particular the preorder on a translation invariant model should give the group the structure of a (pre)-ordered group, which is interesting. Also the relation $\to$ is now a Cayley graph and determined by a single subset of $G$.

[Terence Tao]

OK, this definitely needs checking (and formalization), but I think I managed to repair the greedy argument, equational#760 . To avoid the problem coming from the partial order, I simply imposed as an additional rule that the partial order is always trivial: $x \leq y \implies x=y$. Amazingly, and after a lot of case analysis, it appears that the greedy algorithm barely closes with this additional axiom (as well as the unique factorization axiom, and some further axioms along for the ride including known consequences 8, 101, 46155, 378 of 854, a no idempotence axiom, and a "monotonicity" axiom that basically prevents a word from being a strict subword for itself (but without using the language of words)). Among other things, the triviality of the order immediately rules out 413, which is $x \diamond (y \diamond x) \leq x$, simply by starting with a seed that fails the 10 law $x \diamond (y \diamond x) = x$, which as one can imagine from all of our previous attempts to build 10-violating 854 magmas is quite feasible.

It is an extremely delicate analysis, with almost all hypotheses just barely closing with no "slack", and I suspect that the greedy magma being constructed here is in fact very close to the universal magma $M_{854}$.

In principle 1045 and 1055 should now also fall by constructing a suitable seed for each, but I have not attempted this.

[Matthew Bolan]

Wow! I hope it checks out. I guess my job is to look for seeds for 1045 now.

[Mario Carneiro]

Does monotonicity refer to the ordering relation $\le$ defined on 854 or the ordering relation on $\mathbb{N}$?

[Terence Tao]

The ordering relation on Nat. Which is admittedly artificial but it worked (i needed to ensure that words like (xy)z could not equal x unless (xy)z=xy=x

[Terence Tao]

IMG_1223.jpeg in case anyone is interested, this is the blackboard i needed to stare at for fifteen minutes before i realized the argument could close if the partial order was trivial

[Mario Carneiro]

looks like fun, I will try my hand at formalizing it tomorrow

[Matthew Bolan]

Ok I think I have a search for seeds running. Is there an obvious obstruction to 3 element seeds?

[Matthew Bolan]

Is there perhaps a typo in the seed in the proof of 12.10? For $x=0, y=2$ my program says 46155 fails due to $(x \diamond y) \diamond (x\diamond (x \diamond y))$ not being well defined, and eyeballing it I think I agree.

[Matthew Bolan]

The needed 413 violation also seems to simplify to $0 \diamond 0 = 0$ to me, which violates no idempotents, so I'm guessing there's a typo in the table. EDIT: I see, you are claiming the equality fails here by the no idempotents requirement. I'll modify my check to assume this.

[Matthew Bolan]

It's also complaining about the auxiliary law with $x=0$ and $y=2$

[Terence Tao]

I think the $0 \diamond 3 = 0$ entry should be deleted. (I mistakenly added it as I thought it was a consequence of the other entries and Equation 101, but I confused $(x \diamond y) \diamond x$ and $x \diamond (y \diamond x)$.)

The derivation here is: to get $x \diamond (y \diamond x) \neq x$, I chose $x = 0$, $y=1$, then set $y \diamond x$ equal to $2$, and $x \diamond (y \diamond x)$ equal to $3$. Law 378 then forces $3 \diamond 2 = 3$ and $2 \diamond 0 = 2$, but then I think one can stop.

[Matthew Bolan]

Ok, and that explains why my program didn't find any similar examples, I was checking the naive condition for 413 rather than the condition you are, and that was destroying it since the needed products weren't defined.

[Matthew Bolan]

My program agrees then, and finds seeds for at least 1055, assuming no bugs.

[Matthew Bolan]

[[1, 0, None], [1, None, None], [None, None, None]] is supposed to be a seed for 1055.

[Terence Tao]

It should also be possible to directly find a slightly larger seed that violates 413 directly. I just didn't have the patience to Sudoku enough of the multiplication table to find it.

[Terence Tao]

Huh, that is smaller than I expected. Let me check it by hand.

[Matthew Bolan]

well, definite bug, so one second.

[Terence Tao]

Yeah it has to be at least as big as my seed magma as a 1055 example has to contain a 10 violation

[Matthew Bolan]

yeah, forgot to check something was well defined when I rewrote 1045 to 1055.

[Matthew Bolan]

well, more accurately, I was still checking the thing from 1045 was well defined.

[Matthew Bolan]

ugh, back to it not finding small examples. Time to rewrite to be less naive about it, or alternately someone plays sudoku.

[Matthew Bolan]

Wait!
[[None, 0, 0, None], [3, None, None, None], [None, 2, None, None], [3, None, None, None]]

[Terence Tao]

It seems to obey the axioms, but I don't see the 1055 violation

[Matthew Bolan]

let me get it to print it, maybe another bug. My track record is not good tonight.

[Terence Tao]

Incidentally the greedy algorithm is itself pretty amenable to programming on a computer, and should start happily generating an infinite 854 magma a couple entries at a time, from a given seed

[Matthew Bolan]

Ok It thinks the violation is with (x,y,z) = (1,0,2)

[Terence Tao]

Huh, it checks out I think. I get x ◇ ((y ◇ (z ◇ x)) ◇ x) = 3 distinct from x=1.

[Matthew Bolan]

On to 1045

[Matthew Bolan]

I agree with your computation by the way

[Terence Tao]

Your seed would also work for the 413 anti-implication. Basically anything that contains a 10 violation will work for that one.

[Matthew Bolan]

oh then the 1045 seed will be a 3-for-1 special then

[Matthew Bolan]

1 0 0 _ _
1 _ 1 _ 1
_ 4 3 2 _
_ _ 3 _ _
_ 4 _ _ _

[Matthew Bolan]

Should be anti 1045

[Matthew Bolan]

But I have been very sloppy tonight, and am quite tired. In fact, I no longer trust that the previous 1055 example was correct for law 854 itself, I was checking that the whole term was well defined instead of just the righthand factor.

[Matthew Bolan]

On the bright side, to find that thing I had to implement the greedy algorithm itself, and it seems to work. It is very fun to tell it to grow a seed to size 100.

[Matthew Bolan]

The table
2 0 0 _
_ _ 3 _
2 2 _ 2
_ _ 3 _
also supposedly works for 1045, with the counterexample at 1 0, and it is smaller. This example is actually very annoying to see, as 3 hours ago I had a computer crash right before the search for tables with 8 entries was to begin. I could have saved myself a lot of time.

[Matthew Bolan]

Matthew Bolan said:

On the bright side, to find that thing I had to implement the greedy algorithm itself, and it seems to work. It is very fun to tell it to grow a seed to size 100.

Just for fun, here is a 10x10 anti-1045 seed:

 1 0 0 0 _ _ _ _ _ _
 1 3 1 1 _ 6 _ 1 _ _
 _ 7 5 4 _ 2 2 8 _ _
 3 3 _ _ 3 _ _ _ _ 3
 _ _ _ 4 _ _ _ _ _ _
 _ _ 5 9 _ _ 5 _ _ _
 _ _ 6 _ _ 6 _ _ _ _
 _ 7 _ _ _ _ _ _ 7 _
 _ _ _ _ _ _ _ 8 _ _
 _ _ _ 9 _ _ _ _ _ _

[Jose Brox]

Terence Tao ha dicho:

It is an extremely delicate analysis, with almost all hypotheses just barely closing with no "slack", and I suspect that the greedy magma being constructed here is in fact very close to the universal magma M854​.

Hi again! I've been quite ill the last few days and had to disconnect. The idea I was working on had several points in common, as unique factorization and monoticity: I was trying to get a model over Nat by using exponentials in the product, e.g.
$x*y = 2^x3^y,$
and imposing 101, 378, etc. (so e.g. $2^x3^y*y = 2^x3^y$) and some other experimental tweaks and more complicated versions. I didn't get to prove the model closed. Do you think it could be valid/useful?

[Mario Carneiro]

@Terence Tao Not a bug in the proof exactly, but the case seems misleadingly presented:

• Equation 8: As this equation is of a left-absorbent form, the only addition to the table that could cause a violation is $a \diamond b = c$, that is to say the only case that needs to be ruled out is $(x, x \diamond x) = (a,b)$. But then $a \diamond b$ would already have been defined by Equation 8, contradiction.

The proof is going by cases on $x\diamond x$, so the new case is not $(x, x \diamond x) = (a,b)$ but rather $(x, x) = (a,b)$. In this case it is not a contradiction, but rather the goal holds because of the clause $b\diamond c=b$.

[Terence Tao]

@Mario Carneiro Thanks for the catch! I have updated the blueprint accordingly (and also added @Michael Bucko 's 1045 seed; I have to travel today, but I will check it by computer on the plane).

@Jose Brox This is a very nice idea to revive the Kisielewicz type construction! Basically you have selected an ansatz in which $x * y = x$ if $y \to x$ and $x * y = 2^x 3^y$ otherwise, and the only difficulty is to figure out how to select the relatino $\to$. This finally resolves an issue someone (I think @Daniel Weber asked some time ago, which is whether the directed graph $\to$ contained enough information to determine the magma. This wasn't literally true, but with your ansatz it becomes true, and the problem is now "just" a graph theory problem of designing a directed graph obeying a certain complicated set of axioms. My construction is highly recursive but with this perspective you might be able to find a simpler and more explicit rule. It's nice that the unique factorization and monotonicity axioms already come "for free" in this approach. More generally, I like the idea of using this type of ansatz to attack the other open implications like 1323.

[Matthew Bolan]

Matthew Bolan said:

The table
2 0 0 _
_ _ 3 _
2 2 _ 2
_ _ 3 _
also supposedly works for 1045, with the counterexample at 1 0, and it is smaller. This example is actually very annoying to see, as 3 hours ago I had a computer crash right before the search for tables with 8 entries was to begin. I could have saved myself a lot of time.

If it helps to verify, this table was grown in 1 step from the table

2 0 0
_ _ _
2 2 _

[Terence Tao]

Reminds me of the many hours I lost to Minesweeper as a student...

It's possible that by starting with the empty seed, one will by chance generate a 10 counterexample, and then with a few more iterations, get a 413 and 1045 counterexample as well, though it may depend on the order in which one takes the greedy construction. Though if @Jose Brox 's construction works out, that may be the more elegant construction in the end.

[Matthew Bolan]

I generated quite a few starting from the empty seed and got nothing. I had to start with 3x3 seeds to get results.

[Matthew Bolan]

but once you do that and grow for a few steps, counterexamples seem common.

[Terence Tao]

OK. There could be an "abiogenesis" problem; we've seen in practice that it's hard to generate 10 counterexamples (which, in the abiogenesis analogy, would be like "amino acids") from scratch, but once one has them, they seem to be useful for generating more complex counterexamples as well.

[Douglas McNeil]

In the case of 413, there are about ~160 distinct minimal seeds. About 1/2 of those can be ruled out as generating 854 compatible magmas almost immediately. Another 1/4 can with a fair chunk of work and correct choice of next coordinate to inspect can be shown to fail if you exhaust every possibility. The remaining ones.. are a pain, and while I was hoping they'd all close, I guess one of them must not if the greedy algorithm works! :sweat_smile:

[Terence Tao]

In retrospect, the reason why the strategy of finite model extension was not working so well was that the initial finite magmas already had a non-trivial partial order relation, which was creating a lot of constraints to extending the magma consistently (and I think, over time, the partial order became so "dense" that the extension became "boring", with no real choices in how to place the new element in relation to previous rows). Plus, when extending element at a time, there were pigeonhole principle issues that forced one to abandon unique factorization and reuse some numbers as products, which also created additional unwanted constraints.

[Terence Tao]

It might be nice to generate an explicit 413 seed, just for reassurance (even if we get the Lean guarantee, it would be nice to have a human-confirmable verification as well). I think all one has to do is extend a 10-violating seed a couple times and it will automatically generate a 413 violation due to the auxiliary law, but I don't have an explicit partial multiplication table exhibiting this.

[Matthew Bolan]

Do I misunderstand something? I thought we already had one of those

[Matthew Bolan]

Or do you want a full table

[Terence Tao]

We have a small table with a 10 violation, and a theoretical argument that any 10-violating seed can be extended to a 413-violating seed, but I don't know if any of the seeds already listed above already violate 413 (it's possible that some of the larger ones already do this, I haven't checked).

[Matthew Bolan]

Oh, I can easily give you one, just a moment.

[Terence Tao]

This is mostly just a sanity check to make sure theory and numerics are aligned. Of course once we have Lean formalization we have all the reassurance we need.

[Matthew Bolan]

Yeah, that makes sense. It is quite promising to me though that my program still thinks the tables your algorithm grows obey the needed requirements.

It says
3 2 4 0 5 _
1 _ 1 _ _ _
_ 2 _ _ 2 _
3 _ _ _ _ _
_ _ 4 _ _ 4
_ _ _ _ 5 _
works, with the counterexample at (x,y)=(0,1).

[Matthew Bolan]

let me have it also say how it grew that

[Matthew Bolan]

It started from
_ 2 _
1 _ 1
_ 2 _
for that one, then added 3,4,5 in that order.

[Terence Tao]

Wow, that is a bit bigger than I thought. Glad I didn't attempt the human Sudoku problem and just stopped when I reached a 10 violation.

Given how several new relations are generated at each step, it is something close to a miracle that the construction doesn't ever create any collisions (once one imposes the unique factorization, monotonicity, non-idempotence and auxiliary laws, each of which was not "forced" by the greedy construction, but became a tactical choice because the argument was simply not closing at all without them). It is still somewhat mysterious to me exactly what this beast of an 854 law is - it clearly has a lot of structure on one hand, but also seems very "free" on the other. Certainly this is the sort of "mathematics from Mars" I was hoping this project would uncover!

[Matthew Bolan]

Yeah! I'm honestly sad you resolved it so quickly, I've become quite interested by 854 magmas.

[Terence Tao]

Well, the outstanding implications are likely resolved, and we have a lot of ways to generate 854 models now, but we still don't fully understand the law. For instance we don't quite have a description of $M_{854}$, though I think we are pretty close to doing so now.

[Mario Carneiro]

I think I found a hole in the proof. It's in case 5 of the proof of 854. The scenario is that $(x, z) = (a, b)$, $y \ne c$, $x\diamond z=c$, $y\diamond z=y=b_1$ and $b_1$ is relevant.

[Mario Carneiro]

actually nevermind, I'm back on track, I just got thrown off by an early sentence

[Terence Tao]

Feel free to update the blueprint if you spot any poor wording

[Mario Carneiro]

I did have to use monotonicity though in a way that wasn't obvious from the text

[Mario Carneiro]

on the whole the case split is structured quite differently for me so I have to do a lot of translation

[Terence Tao]

I'm sure my splitting is not the optimal one, it was the first one that worked and I didn't try to polish it

[Mario Carneiro]

np, that's my job :)

[Terence Tao]

It's probably just outside of the range of aesop to resolve each individual case, I assume?

[Mario Carneiro]

eh, maybe? Each case is actually tiny, but there are more of them than the text implies

[Mario Carneiro]

I'm feeling pretty good about the proof structure so far

[Terence Tao]

OK. I'm looking forward to seeing the final proof. The proof of your previous 854 argument was quite elegant, in particular the proof of unique factorization for the free magma was a lot less painful than I expected.

[Terence Tao]

I imagine this one will be... less elegant, though.

[Mario Carneiro]

I think it's still pretty slick, but it is definitely larger

[Mario Carneiro]

In case 6, where did b1 and b2 come from?

[Mario Carneiro]

I don't think the context gives us anything to tell us that b factors

[Terence Tao]

x * z = b and b = b1 * b2

[Terence Tao]

oh. let me see

[Terence Tao]

we are given that $x \diamond z = b$ and $z \not \to x$, so $b$ factors

[Mario Carneiro]

but why?

[Mario Carneiro]

Is this one of our IH's?

[Terence Tao]

Yeah $(y \diamond z, x \diamond z) = (a,b)$, so $x \diamond z = b$

[Mario Carneiro]

I mean what prevents the situation from being such that $b$ has no factorization, even though $z\not\to x$

[Terence Tao]

$b$ is equal to $x \diamond z$ and $x \diamond z$ manifestly factors into $x$ and $z$

[Mario Carneiro]

although in that case it's not clear what unique factorization is asserting here since we just define b1 := x and b2 := z

[Terence Tao]

well ok it could be a notational quirk but I am implicitly using the notation $b_1$, $b_2$ under the assumption that they are uniquely defined which is what unique factorization guarantees. One could arrange the proof differently, e.g., to define $b_1 \diamond c= b_1$ for _all_ relevant $b_1$, and only use unique factorization later when it becomes important to know that $b_1$ is unique (not sure actually where that is used but I think it shows up somewhere).

[Mario Carneiro]

I gathered that, I was just confused because we only have uniqueness and not existence in this setting

[Mario Carneiro]

One could arrange the proof differently, e.g., to define b1​⋄c=b1​ for _all_ relevant b1​, and only use unique factorization later when it becomes important to know that b1​ is unique (not sure actually where that is used but I think it shows up somewhere).

Oh, I actually guess I did that

[Terence Tao]

Usually yes but in this particular case we happen to possess an explicit factorization of $b$ so we can guarantee existence in this case only.

[Terence Tao]

Then I guess you don't actually need unique factorization in Case 6. But I suspect it may show up elsewhere. Or perhaps as with your 1485 formalization, maybe it never shows up at all and then we can simplify the proof.

[Mario Carneiro]

oh yes, it definitely has

[Michael Bucko]

Since 854 is really reluctant when it comes to collapsing to simpler forms, and always dreams up those non-colliding features / data points, perhaps we should have a deeper look into 1043 (and 433) too.

2,4  →  1043 → 433  →  854
2,4  →  1043 →  854
2,4  →  854

[Terence Tao]

The family tree of inequivalent laws implied by 1043 (which includes 854 and all of its descendants, as well as the important law 10) is really quite impressive.

[Mario Carneiro]

It's done!

[Mario Carneiro]

equational#768

[Matthew Bolan]

Are the seeds confirmed?

[Michael Bucko]

The fact that 1043[x = x ◇ ((y ◇ (x ◇ z)) ◇ z)] can imply 433 [x = x ◇ (y ◇ (x ◇ (z ◇ y)))] which can then imply 854 [x = x ◇ ((y ◇ z) ◇ (x ◇ z))] feels more intuitive (which feels wrong) at first than 1043 [x = x ◇ ((y ◇ (x ◇ z)) ◇ z)] being able to directly reach 854 [x = x ◇ ((y ◇ z) ◇ (x ◇ z))].

Perhaps we should look into property mapping, i.e. there could be a list of properties within the equations (in the implication chain) that allow for certain (aggressive, immediate, direct) simplifications.

Perhaps we could use property mapping in order to learn simplifications . (I hope to touch some math from Mars!!) One thing that comes to mind is to outsource simplification learning to diffusion models.

[Mario Carneiro]

Matthew Bolan said:

Are the seeds confirmed?

not yet

[Mario Carneiro]

Which are the seeds we want to verify, and what laws do they counter?

[Matthew Bolan]

They are both in the blueprint already. One counters 413, the other 1045.

[Matthew Bolan]

And then the 1045 will also counter 1055 implicitly

[Matthew Bolan]

Corollaries 12.10 and 12.11.

[Terence Tao]

The seed for 1045 can also be used to refute 413 if you want to economize on seeds

[Terence Tao]

I like how inductive types make the case analysis somewhat more manageable

[Mario Carneiro]

yeah when I first saw you added 5 elements in the inductive step I knew the case splits would be legendary

[Mario Carneiro]

luckily they break up into logical groups and this is reflected in the proof (a lot of the time things simplify for left-absorbent laws)

[Terence Tao]

This is certainly one case where formalization is essential. I don’t think even I would fully trust my own argument otherwise, it is so fragile

[Mario Carneiro]

I'm failing to validate the seed for 1045. Properties eq854, eq101, eq46155, eq378, uniq_fac, mono fail

[Matthew Bolan]

That's surprising

[Matthew Bolan]

2 0 0 _
_ _ 3 _
2 2 _ 2
_ _ 3 _

[Matthew Bolan]

This was the intended table, can you confirm that's what you have?

[Mario Carneiro]

oh mono is obviously broken for $3\diamond 2=2$

[Mario Carneiro]

my list is

    [((0,0),2), ((0,1),0), ((0,2),0), ((1,2),3), ((2,0),2), ((2,1),2), ((2,3),2), ((3,2),2)]

[Matthew Bolan]

Looks like a typo. Try ((3,2),3)

[Mario Carneiro]

yep that did it

[Mario Carneiro]

I'll fix the blueprint

[Mario Carneiro]

where does it violate 413?

[Matthew Bolan]

Let me check.

[Matthew Bolan]

(deleted, bug)

[Matthew Bolan]

Yeah it's at $(x,y) = (1,2)$. Law 413 is the same as saying $x \diamond (y \diamond x) \le x$, which should fail for $(x,y) = (1,2)$

[Matthew Bolan]

Something still seems not quite right. Fixed.

[Matthew Bolan]

(x,y) = (1,2), sorry. I was looking at the wrong table.

[Matthew Bolan]

now $1 \diamond (2 \diamond 1) = 1 \diamond 2 = 3$, and by the auxilliary law we cannot have $1 \diamond (1 \diamond 3) = 1$

[Mario Carneiro]

@[equational_result]
theorem not_413_1045 : ∃ (G : Type) (_ : Magma G), Facts G [854] [413, 1045] := ...

equational#768

[Terence Tao]

I was just going to say that I had verified the seed in Python, but this is clearly moot now :grinning_face_with_smiling_eyes:

[Terence Tao]

Glad to see you could verify the seed by decide, it would have been tedious otherwise

[Mario Carneiro]

yes, this is the next step up the industrial strength proof scale past the one for 1485

[Mario Carneiro]

There are more steps past this; I'm glad you didn't give me a 12x12 seed to check

[Michael Bucko]

(deleted)

[Terence Tao]

It is perhaps of less interest now that 854 is fully resolved, but I did actually manage to get a fully explicit description of the free magma $M_{854}$. It is the set of words (on some fixed set of generators) generated by an operation $x \diamond y$ which is equal to the free operation $x * y$ unless a certain relation $y \to x$ holds, in which case it is equal to $x$. The relation can be defined recursively as follows, where we use $x_L, x_R$ to denote the left and right components of a word $x$ (so $x = x_L * x_R$), $x_{RL}, x_{RR}$ to denote the left and right components of $x_R$, etc..

Definition of directed graph: $x \to y$ holds iff one of the following statements is true:

1. $x = y_R$.
2. $y = x_{RL}$ and $x_{RR} \to x_L$.
3. $x = y_{RL}$, $y_{RR} \to y_L$, and $y_R \to y_{RL}$.
4. $y = x_R$, and there exists $z \in \{ x_{LR}, x_{LRL}, x_{RR}, x_{RRL} \}$ such that $z \to x_L$ and $z \to x_R$.
5. $y = x_R$, and one of the claims $x_L = x_R$, $x_L = x_{RL}$, or $x_R = x_{LL}$ holds.

Here we adopt the convention that a statement can only hold if all the terms needed to verify it are well-defined. For instance for part 2 to hold, $x_{RL}, x_{RR}, x_L$ must be well-defined. In part 4, $x_{RRL}$ will need to be defined if one is selecting $z$ to equal $x_{RRL}$, though if one selected $z$ to equal say $x_{LR}$ instead then there is no such requirement.

One interesting feature of this relation is that it forces $x,y$ to be somewhat "close" to each other, in that one is a depth one or depth two subword of the other. Specifically, $x \to y$ can only hold if one of $x = y_R, x = y_{RL}, y = x_R, y = x_{RL}$ holds. (This property is also preserved by the 854 greedy construction, and is what led me eventually to the above characterization.)

The verification that this actually obeys 854 and is universal is a lengthy case check, comparable to that for the 854 greedy construction. I put it in the blueprint at equational#779, but I don't consider it a priority for formalization given that 854 is now fully resolved by other means.

[Amir Livne Bar-on]

A thought about the "math from Mars" angle: equation 543 has an operation definable from the magma operation that obeys a very symmetrical set of laws, which are together equivalent to that one equation.
Did anyone try to search for something similar for 854? That is, whether there's a definable operation (or multi-valued operation? or several operations?) that is equivalent to law 854 when symmetrical or otherwise pretty equations hold for the new operation?

[Terence Tao]

Well, we have identified the directed graph relation $\to$ and the pre-ordering $\leq$ on 854 magmas which, when combined with the original magma operation $\diamond$, do obey a large number of interesting relations. I haven't looked into the extent to which one can try to reduce the axioms to hide the original law 854 from view and instead have a number of simpler looking laws. Given the complex nature of the free 854 group, I'd say there is a limit to how much one can clean up the algebra, but I can certainly believe one can replace one weird-looking law 854 by a small number of nicer looking laws (in particular, the fact that $\leq$ obeys the standard pre-ordering axioms may beautify the axioms a little bit, or at least make them slightly less Martian in nature. On the other hand, this pre-order is trivial on the free group $M_{854}$, so there's a limit to how much it can help on its own.).

[Alex Meiburg]

Terence Tao said:

It is perhaps of less interest now that 854 is fully resolved, but I did actually manage to get a fully explicit description of the free magma $M_{854}$.

I can't be alone in thinking that finding explicit descriptions of free magmas for different equations is of independent interest. ("Explicit" in the sense of "a computable algorithm for testing equality of words".) Both because I think they provide another good perspective on what the equation is really doing, but also they make proving any future non-implications pretty much maximally easy.

[Alex Meiburg]

Actually, personally I think that this project (for each law L, write down a def for a Magma that is provably isomorphic to the FreeMagmaWithLaws L, such that this def is computable) would be a great Future direction

[Kevin Buzzard]

There are a lot of laws though!

[Eric Taucher]

Alex Meiburg said:

for each law L, write down a def for a Magma that is provably isomorphic to the FreeMagmaWithLaws L, such that this def is computable

Could you provide an example of this? It sounds like one of the side tasks I'm working on while learning the math involved. Additionally, since I'm not a mathematician and am working on creating source code for this, could you explain it more as an algorithm?

[Alex Meiburg]

Kevin Buzzard said:

There are a lot of laws though!

Haha yes! It would definitely be a slow project, with probably close to zero help from automation - except maybe to show certain operations close from a SAT solver for the really hard ones

[Amir Livne Bar-on]

There are dozens of confluent laws so these are already solved automatically

[Alex Meiburg]

Oh that's true! I hadn't thought about that

[Alex Meiburg]

Eric Taucher said:

Could you provide an example of this? It sounds like one of the side tasks I'm working on while learning the math involved.

So Eq4512, the associative law, can be described as List x, where x is the generators. This is the free associative magma on x. There is an existing definition in the repository of the free associative magma, but it's noncomputable: two expressions are equal _if there exists some series of expressions related by the associative law_ that lets you turn one into the other. There isn't an algorithm immediately to check if such a series exists, so this is a non-constructive version of the free associative magma.

But, by showing that this is isomorphic to List x, we can make a constructive and computable version of it.

The FreeMagmaWithLaws gives this non-constructive definition for each law. It would be nice to find a constructive definition of as many laws as possible. List is a particularly easy one. Terence Tao's message from Nov 2 gives a constructive definition of the free Eq854 magma, which is obviously quite a bit more complicated.

As one other example: Eq543 defines an abelian group structure, and the free abelian group is DFinsupp x Int. The magma operation is then subtraction of these DFinsupp's.

[Eric Taucher]

@Alex Meiburg

Thanks. Still a bit over my head, the magma parts, but enough meat on the bone to chew on. :smile: