1516 -> 255

Stream: Equational

[Terence Tao]

This is a new thread to discuss the specific question of whether 1516 $x = y^2 \diamond (x \diamond (x \diamond y))$ implies 255 $x = x^4$, where we recursively define $x^{n+1} = x^n \diamond x = R_x^n x$. This, and its dual, would resolve two open implications. It has been discussed extensively in a previous thread; I now summarize some progress here.

Immunities:

• (T) Implication is true for translation-invariant models (even noncommutative ones).
• (L) Implication is true for linear models (even noncommutative ones).
• (F) Implication is true for finite models.
• (C) Implication is true for commutative models.
• Implication is true if squaring is surjective.
• Implication is true if one has "flip-injectivity": a ◇ b = c ◇ d implies b ◇ a = d ◇ c.

Examples:

• The smallest non-trivial finite magma is of order 5. (In view of comments:) This is the law $x \diamond y = 3x + 3y$ on ${\mathbb Z}/5{\mathbb Z}$. In particular $x^2 = x$ in this case. This is also a translation-invariant, commutative model.
• (Added in view of comments below:) Another linear model is $x \diamond y = 4x + y$ on ${\mathbb Z}/7{\mathbb Z}$. In this model, $x^2 = 5x$, $x^3 = 0$, and $x^4 = x$, and then $x^n$ repeats with period 3.

Some known identities/properties for 1516 magmas:

• $x^2 = L_{x^2}^3 x = L_{x^2}^2(x^3)$
• $L_{x^2}$ is surjective
• $(x^3)^2 = (x^2)^3$
• $x^2 = (x^3)^2 \diamond x^2 = (x^2)^4$. That is to say, 255 is true for square numbers.

1516 does not seem to obviously imply

• $x = x^n$ for $n = 7, 10,  13, 16, 19, 22$.
• $x = L_x^3(x^3)$

[Pace Nielsen]

Does 1516 imply x^4 = x^7, x^4 = x^10, or x^7 = x^10?

[Daniel Weber]

Some rules from the greedy ruleset:

• If $x^2 = x$ and $x \diamond y = x$ then $y^2 = x$
• If $x \diamond y = y \diamond x = x$ then $x^2 = x$
• If $x \diamond y = y \diamond y = x$ then $x^2 = x$

[Michael Bucko]

Do we have a tptp for this one?

[Pace Nielsen]

The smallest non-trivial magma mentioned above is linear. I thought it might be useful to describe all linear maps

$$x\diamond y = ax+by+c$$

satisfying 1516.

The carrier ring must be commutative, and a reduction system is given by

$$ba\mapsto ab$$

$$ab^2\mapsto -ab+1$$

$$b^3\mapsto -ab-a^2$$

$$a^2b\mapsto -a^3-ab-b+1$$

$$a^4\mapsto 2a^3+b^2+b+2a-1$$

$$b^2c\mapsto -bc-ac-c$$

$$a^2c\mapsto -ac-c$$

Not the simplest system in the world.

The 5-element magma corresponds to the ring $\mathbb{Z}/5\mathbb{Z}$ taking $a=b=3, c=0$.

[Terence Tao]

The model $x \diamond y = 3x + 3y$ on ${\mathbb Z}/5{\mathbb Z}$ is idempotent, $x^2 = x$. Is there a slightly larger model which isn't idempotent? I don't see $a+b=1$ listed among your laws, so I suspect the answer is "yes".

[Pace Nielsen]

Running a search in $\mathbb{Z}/p\mathbb{Z}$ for small primes, there are lots of examples. The smallest where the idempotent law fails is when $p=7, a=4, b=1$.

[Terence Tao]

That law $x \diamond y= 4x + y$ on ${\mathbb Z}/7{\mathbb Z}$ might serve as a good test model as a first approximation of what rules might and might not be consequences of 1516. For instance here we have $x^2 = 5x$, $x^3 = 0$, $x^4 = x$, and $x^n$ just repeats periodically mod 3. Which is of course consistent with your request to investigate $x = x^n$ for various $n = 1 \hbox{ mod } 3$.

[Pace Nielsen]

Just checked that the relations force all linear maps to satisfy $x^4=x$.

[Terence Tao]

I think you had previously confirmed that this implication was immune to linear models (even noncommutative ones), but it doesn't hurt to double check.

[Pace Nielsen]

Oh yeah, I forgot for a moment that the target was $x^4=x$. Good to have double-checked it!

[Alex Meiburg]

For a system with many immunities, one strategy that I haven't seen mentioned could be a LORC (linear on residue classes) function. There's a couple ways to think of it, one would be operations of the form "if x is even and y is odd [foo], else if x is odd [bar], else [baz]" and so on, but generalized to arbitrary mod k. Another way to look at it is that the magma on (Fin k)×ℤ -- or some other ring, doesn't have to be ℤ -- with a sort of semidirect product structure. The map (x,y) -> x gives a homomorphism to a k-element magma, and for all i and j, the map fun x y => ((i,x) ⋄ (j,y)).2 is linear.

[Alex Meiburg]

We could try this (mostly by hand I guess) by trying successively larger k, taking a k-element magma that obeys the law, and then trying to fill in the k^2 linear functions. I think a few other infinite examples people used to solve hard nonimplications follow this form with k=2, which is why I have some hope it could work further

[Alex Meiburg]

Although, in this case, that could get very messy fast. Hmm. The smallest nontrivial example is on 5 elements, which means you need 25 linear functions, or to solve for some 75 variables.

[Alex Meiburg]

Well, I plunk out the system of equations and see if there's an obvious thing to do. Maybe there's even lots of solutions! :)

[Terence Tao]

It's worth a shot, though the immunity that this problem has to constructions in which squaring is surjective gives me some pause.

[Alex Meiburg]

Do the finite magmas satisfying 1516 always have a surjective square map? The ones listed above all do

Assuming so, that means that (since the homomorphism to Fin k will lead to a surjective square map), if we don't want a LORC construction to have a surjective square, we need at least one of the ax+by+c maps to have gcd(a,b) != 1. And that's sufficient then for having it not be a surjective squaring map

[Alex Meiburg]

Well, the k=5 case doesn't work at least (with the ring as Z). Since it's idempotent, there's a closed submagma on (1,x), and indeed for every (i,x). Since by construction that's a linear model, it has to obey the equations people discussed earlier. I derived them as a * (b^2-b) = 1 together with either 1-b+2b^2-2b^3+b^4 = 0 or (c = 0 and -1-b+b^3 = 0). Solving these over ℂ, we find that there are no integer solutions. (There are solutions over ℂ, in fact over the algebraic integers, but then the squaring map on this submagma is surjective.) Since the squaring map on these submagmas is surjective, it's also true of the whole magma, so it can't be a counterexample.

[Terence Tao]

All finite 1516 models have surjective squaring map. Proof So this is indeed a significant obstacle to LORC constructions, since they will likely have finite models thanks to the Lefschetz principle (unless one works with a noncommutative LORC).

[Terence Tao]

This massive amount of immunity is annoying!

[Alex Meiburg]

I see. Furthermore I found that it doesn't work with the p=7 case above, because just having a _single_ idempotent element actually makes the argument above fall through. In the p=7 case, 0^2 = 0, and so the submagma induced there again needs some a/b/c to work, and there are no rational solutions. So there's no LORC over Z sitting above the p=7 magma, or above any finite magma with at least one idempotent element.

And then -- I didn't quite the follow the Lefschetz part, it's not my area, but I think this is the idea? -- we could say, okay, instead of taking the ring to be Z, we could take (say) the algebraic integers, where we do have a solution for the idempotent elements. And we could then still have a map like x⋄y = 2x+4y for one of the other parts, something that isn't surjective on the algebraic integers. So in that way we could get a LORC that doesn't have a surjective squaring map. But if we had that, we could just extend it to operating on C instead of the algebraic integers, and now squaring is surjective, so it will necessarily obey 255.

[Terence Tao]

I guess I'm using the Lefschetz principle in a slightly nonstandard form, namely that any first-order statement that is true over a characteristic 0 algebraically closed field such as C, is also true in (algebraically closed) fields of sufficiently large finite characteristic p, and hence also in certain finite fields of large characteristic; this basically follows by combining the usual form of the Lefschetz principle with the compactness theorem in logic. There is a nice article of Serre describing this technique, for instance to prove the Ax-Grothendieck theorem (which is relevant here). I think this method shows that any polynomial or PORC type construction in any field will necessarily induce a similar construction in a finite field, which we know already to be impossible.

[Alex Meiburg]

Alright, that makes sense now, thanks! (It's been a while since I had occasion to think about the Ax-Grothendieck theorem, but it's a happy memory; such a fun result.) So, this also rules out PORC type constructions over any commutative ring of characteristic 0, since they could always be extended to the field of fractions. In particular, nothing over Z. Would have to look at something noncommutative, or with positive characteristic.

[Terence Tao]

I'm thinking that a NORC (nonlinear over residue classes, aka an extension of a finite model) has a chance (it's basically the same strategy @Bernhard Reinke outlined over on the 1323 thread). Taking the ${\mathbb Z}/5{\mathbb Z}$ model is problematic due to squaring being idempotent there, so let's take the ${\mathbb Z}/7{\mathbb Z}$ model instead. So our carrier is now of the form $G \times {\mathbb Z}/7{\mathbb Z}$ with a magma operation of the form
$(x, a) \diamond (y,b) = (x \diamond_{a,b} y, 4a+b)$
where we have a frightening-looking 49 separate magma operations $\diamond_{a,b}: G \times G \to G$. However, we can take advantage of dilation symmetry to make the projective ansatz $\diamond_{ka, kb} = \diamond_{a,b}$ for all invertible $k$, which cuts us down to "just" 1 + 48/6 = 9 magma operations. The law 1516 can now be computed to take the form
$(y \diamond_{b,b} y) \diamond_{5b, a+b} (x \diamond_{a,4a+b} (x \diamond_{a,b} y)) = x$
for all $a,b,x,y$. This is 49 different magma-type laws, but with the projective ansatz we cut back to 9. Firstly there is the a=b=0 case, which is just saying that $\diamond_{0,0}$ obeys 1516. Then we have the $b=0, a=1$ case, which is
$(y \diamond_{0,0} y) \diamond_{0, 1} (x \diamond_{1,4} (x \diamond_{1,1} y)) = x; \quad (1)$
the $b=1, a=0$ case, which is
$(y \diamond_{1,1} y) \diamond_{1, 3} (x \diamond_{0,1} (x \diamond_{0,1} y)) = x \quad (2)$
and then six more cases with $a=1$ and $b$ non-zero, which are
$(y \diamond_{1,1} y) \diamond_{1, (b+1)/5b} (x \diamond_{1,b+4} (x \diamond_{1,b} y)) = x. \quad (3)$
Bearing in mind that squaring shouldn't be surjective, it is tempting to make $y \diamond_{1,1} y$ equal to a constant 0 to simplify the latter two rules. (We have no examples of 1516 magmas with squaring not surjective right now, so we can't easily make $y \diamond_{0,0} y$ non-surjective.) The hope is now that the various magma operations here are sufficiently "decoupled" from each other that it becomes easier to construct counterexamples.

[Terence Tao]

Unfortunately, we can't simultaneously make squaring in $\diamond_{0,0}$ surjective while setting squaring in $\diamond_{1,1}$ equal to a constant $0$. The former hypothesis together with (1) makes all the left multiplication operators $L_y^{0,1}$ surjective, where $L_y^{a,b}$ denotes left-multiplication $x \mapsto y \diamond_{a,b} y$. On the other hand the latter hypothesis and (2) makes $L^{1,3}_0$ surjective, hence $L^{1,3}_0 (L^{0,1}_x)^2$ is surjective, but from (2) and the above hypothesis we know that this map is also constant, a contradiction.

One can still hope that a greedy construction works here, but it doesn't look appetizing; one can wait to see if the simpler situation in 1323 falls to this approach first.

[Bernhard Reinke]

A difference to the situation in 1323 is that 255 is a law in only one variable, while for 1323 we want to refute a law in two variables. Part of my assumptions in 1323 is that one-generated submagmas are as simple as possible, namely isomorphic to the finite magma that we are extending over. We of course cannot make this assumption here.

On the other hand, if there is a counterexample, there should be a one-generated counterexample. So I am curious what happens in the following case: z should be our generator and impose $z^4 \neq z$, what kind of inequalities in the terms in z can we deduce? For example we get $z^2 \neq z$. Are there any other easy ones?

[Pace Nielsen]

In semigroups and rings, elements satisfying the periodic identity $x^n=x^{n+k}$, for some integers $n,k\geq 1$ are well-studied. If we take $n$ to be the smallest such integer it is called the index, and then the smallest such $k$ is called the period. Moreover, then $x^j=x^{j+i}$ if and only if $j\geq n$ and $k\mid i$.

It seems that these types of facts carry over to the magma setting, using left-parenthesized powers, by the same arguments. Since we are trying to avoid $x=x^4$, it is interesting to ask which of its consequences might hold.

Also, it seems that tripling of multiplication is common when working with 1516. So I'm wondering whether or not 1516 implies $x^{10}=x^{19}$. (This should cover the other identities I was asking about earlier.)

[Pace Nielsen]

Checked these in Vampire, and it timed out.

[Jose Brox]

Pace Nielsen ha dicho:

Checked these in Vampire, and it timed out.

imagen.png

[Pace Nielsen]

Below, for ease of notation, I'm going to suppress the diamond operation by using concatenation and parentheses. Also, I take $x^1:=x$ and $x^{n+1}:=x^nx$ as usual.

I'm wondering if some of the techniques that helped solve 854 might apply to 1516, in the following sense. Looking at the equation explorer, we see that 1516 does not imply any other equation (below 4684) except 1426 (coming from taking y=x) and the trivial equation 1. Thus, one might a priori hope that a reduced form could be found by blindly applying the 1516 reduction rule, taking anything looking like y^2(x(xy)) to x, repeatedly in subwords.

However, after a little computation, we see that this isn't the case. For instance, taking $y=z, x=z^2$ in 1516 yields

$$z^2(z^2z^3)=z^2$$

and so (as mentioned at the very beginning of this thread) we get a new relation

$$(z^3)^2z^2 = (z^3)^2(z^2(z^2z^3))=z^2.$$

Thus, even though $z^2$ and $(z^3)^2z^2$ are both reduced under "blind" applications of 1516, they are nonetheless equivalent.

So we add this new reduction rule to our list of rules, and try again. If I understand correctly (someone please correct me if I'm wrong), someone performed this sort of computation and the process of finding a normal form does not appear to converge to a simple finite set of rules. However, the hope is that by studying enough of the forced new rules, we might be able to glean a new (non-forced) principle that would let us find a reduced form for magmas "close" to 1516.

If someone has access to the program that searched for a normal form, could it be modified to spit out the first 10 (say) new reduction rules that are forced in 1516 magmas? I'm hopeful that we can notice a pattern. [Really, we only need to consider 1-generated 1516 magmas, since we are trying to refute a 1-variable law.]

[Pace Nielsen]

Here are the first few new reduction relations I found in addition to the ones above.

$$x^2 = (y(yx))^2(x^2y)$$

$$y^2=((x(xy))((x(xy))y))^2x$$

[Pace Nielsen]

Okay, I found something that is puzzling to me, but Vampire seems to confirm (if I entered it correctly).

Assuming 1516, if $x=y\diamond z$, then $y=(z\diamond z)\diamond (y\diamond x)$.

[Terence Tao]

I think this is just a relabeling of 1516.

[Pace Nielsen]

You are right.

[Pace Nielsen]

Does this give us an infinite sequence of reductions? Starting from $a=b^2(a(ab))$, we then get (taking $x=a,y=b^2,z=a(ab)$ ) the new reduction $b^2=(a(ab))^2(b^2a)$, which in turn gives us the new rule $(a(ab))^2 =(b^2a)^2[(a(ab))^2b^2]$, etc... Not sure if this stabilizes, or gives lots of independent reductions.

[Pace Nielsen]

We have $x=yz \Rightarrow y=(z^2)(yx)$. Vampire times out on the converse, so it seems a safe bet that it just doesn't hold. OTOH, if we impose the converse implication anyway, Vampire continues to time out on Eq255. So, to avoid an explosion of new reduction rules, it might be helpful to add the assumption

$$y=(z^2)(yx) \Rightarrow x=yz.$$

[Terence Tao]

This comes close to imposing the requirement that squaring is injective. If we impose that as well, does that trivialize the problem?

[Terence Tao]

Related to this, one could explore whether left or right cancellability has any impact on the problem. For instance, left cancellability implies injective squaring: if $y^2=z^2$ then $L_{y^2} L_x^2 y = L_{y^2} L_x^2 z$, hence $y=z$ if left multiplication is injective.

[Pace Nielsen]

Vampire times out when trying to prove Eq255 (after 999s), assuming Eq1516 + left-cancellativity + the converse implication I mentioned above. So probably we can assume left-cancellativity as well. (Eq1516 + right-cancellativity does give Eq255.)

[Terence Tao]

By the way, left cancellability also implies the converse implication you stated anyway, since if $y = (z^2)(yx)$ then $(z^2)(yx) = (z^2)(y(yz))$ and hence $x = yz$ by left cancellability.

We already knew that $L_{x^2}$ was surjective, so now with left cancellability these maps are now invertible. So for instance $x^3 = L_{x^2}^{-2}(x^2)$ and $x = L_{x^2}^{-3}( x^2)$. From 1516 the inverse is in fact explicitly given as $L_{x^2}^{-1} y = y(yx)$.

[Terence Tao]

It is possible that left-cancellability is in fact true in the free group $M_{1516}$, which could lead to further useful properties on that group. Do we know of any consequence of 1516 of the form $w \diamond w' \equiv w \diamond w''$ for some words $w,w',w''$ with $w' \not\equiv w''$?

One possible consequence of left-cancellability, in addition to injectivity of the squaring map, is a unique factorization claim $w_1 \diamond w_2 \equiv w_3 \diamond w_4 \implies w_1 \equiv w_3 \wedge w_2 \equiv w_4$ when $w_1,w_3$ are not equivalent to squares.

[Matthew Bolan]

There are at least left-cancellative models of some fairly large finite sizes, for example This 9x9 one

[Matthew Bolan]

I suppose that's not too surprising given the known finite linear models.

[Terence Tao]

Most of the linear models seem to be left-cancellative as well.

Under the working hypothesis that the free group is left-cancellative, this should imply that squaring is injective, and then I think the only way to rewrite a non-square $x$ into an equivalent form $x'$ is either by showing their components agree, $x_L = x'_L$, $x_R = x'_R$ (i.e., one is in the "unique factorization scenario"), or else if one can first show that $x(xy)$ is rewritable into $x'(x'y)$ for some $y$. If one can safely conjecture that $x(xy)$ is never a square when $x$ is not a square then there is a chance of iterating this and actually establishing some of these conjectures by some sort of induction argument.

[EDIT: actually this probably doesn't work unless one assumes that both $x$ and its left component $x_L$ are non-squares, but then in the absence of unique factorization, "left component" might not be well defined. Ugh, maybe the free magma here is actually quite gross...]

[Terence Tao]

My experience with the 854 free group suggests that once has a near-complete list of properties (such as unique factorization or left cancellability) that you (correctly) conjecture the free magma to satisfy, you can prove them all in a giant induction, but if you only have a partial list of these properties, you can't prove anything (sort of like how if you only have a portion of a working greedy ruleset, one cannot draw any useful conclusions, other than perhaps a clue as to what the next addition to the ruleset needs to be).

[Terence Tao]

(deleted)

[Terence Tao]

OK, I think here is what one can correctly say about the free magma by tracing through all possible rewrite options: if $x = x_L \diamond x_R$ and $x' = x'_L \diamond x'_R$ are words with $x_L$ not equivalent to a square, and $x'_L$ not equivalent to a square, then in order to prove $x \equiv x'$, one must either first prove $x_L \equiv x'_L$ and $x_R \equiv x'_R$, or else one must first prove $x \diamond (x \diamond y) \equiv x' \diamond (x' \diamond y')$ for some $y,y'$ with $y \diamond y \equiv y' \diamond y'$.

Basically, there are three different type of rewrites one can apply to a word $w = w_L \diamond w_R$. Firstly, one can rewrite $w_L$ into something equivalent, or $w_R$ into something equivalent; let me call these "low level rewrites". Or one can do a "top level expansion", replacing $w$ with $y^2 \diamond (w \diamond (w \diamond y))$ for some $y$. Or, one can do a "top level reduction", if $w$ happens to be of the form $y^2 \diamond (w' \diamond (w' \diamond y))$ in which case it can be reduced to $w'$. With the hypotheses on $x$ or $x'$, any rewriting route from $x$ to $x'$ either has to avoid all top level expansions or reductions (which is the first case, as only low level rewrites are involved), or at some point involves at some point a top level expansion followed (after some low level rewrites) by a top level reduction (which gives the second case), since the first top level operation applied to $x$ cannot be a top level reduction, and the last top level operation applied to reach $x'$ cannot be a top level expansion.

[Terence Tao]

Here is a random thought: we know that the implication holds when squaring is surjective. What about the opposite case where squaring is constant, i.e., $x^2 = 0$ for all $x$, and the equation is now $x = L_0(x(xy))$ for all $x,y$. Does Vampire give a proof of 255 in this case? If not then this might be a significantly simpler model to analyze.

[Terence Tao]

OK, constant squaring implies triviality: if $x^2=0$, then $L_0 R_0 x = (x^2) \diamond (x(xx)) = x$, and also $L_0^3 x = (x^2) (0(0x)) = 0$, hence $x = L_0 R_0 x = L_0^3 R_0^3 x = 0$.

I might try a two-valued model $x^2 = \pm 1$ later tonight.

[Matthew Bolan]

I think prover9 is telling me the only models with $x^2 = \pm 1$ are trivial.

[Terence Tao]

Ah, that's a shame.

[Pace Nielsen]

Vampire is telling me that Eq1516 + left cancellativity implies the following two special forms of right cancellativity:

$$x^2z=y^2z \Rightarrow x^2=y^2$$

$$x(xz) = y(yz) \Rightarrow x=y.$$

The second one may simplify the case analysis above.

When I was trying to work through the possible rewrite options, subject to left cancellativity, another case to handle arises from the identity

$$(y^2x)((y^2x)y)=x.$$

This is a bit different because of the (possible) lack of a square in the left factor.

When looking at other possible rewrite rules, the following all imply Eq255 (when put in conjunction with Eq1516): $x^2z=yz \Rightarrow x^2=y$, and $x(xy)=\square \Rightarrow x=xy$, and $x(xy)=\square \Rightarrow x=\square$.

However, it appears safe to add the following (independent) rewrite to to Eq1516 + left cancellativity: $x\neq x^2$!

[Andy Jiang]

Inspired by Kevin M's ideas at 1485, and some of the above discussion, I asked Vampire to prepare a list of conditions which are both not obviously implied by 1516 and does not obviously imply 255 together with 1516
tally.txt
Hope it can be helpful for inspiration if you are looking for conditions you can impose to models
? means exist and ! means for all by the way
(Note: checked by Vampire at very low time limit so could be obvious non-examples so if you are going to assume one of them please check with Vampire for longer or ask me and I can do it)

As a sample of the file above here are two conditions vampire found with above criterion which seems to only overlap on the trivial model

1) X^3 is constant
2) for some element B, (B * X)^2 is constant

The second condition together with left-cancelation implies 255. So if you are assuming left-cancellation. 1) is a possible additional assumption which you may wish to take

[Andy Jiang]

X^3 being constant even has a finite model with left-cancellation being
[[0,1,2,3,4,5,6],
[5,2,3,6,0,1,4],
[6,0,5,1,3,4,2],
[1,3,6,4,5,2,0],
[2,6,4,0,1,3,5],
[3,4,0,5,2,6,1],
[4,5,1,2,6,0,3]]
This is like almost literally a sodoku. Does anyone know an interpretation of this magma? (like in some ansatz)

[Bernhard Reinke]

Terence Tao said:

• (Added in view of comments below:) Another linear model is $x \diamond y = 4x + y$ on ${\mathbb Z}/7{\mathbb Z}$. In this model, $x^2 = 5x$, $x^3 = 0$, and $x^4 = x$, and then $x^n$ repeats with period 3.

maybe it is this one?

[Andy Jiang]

yup! thanks (sorry I didn't see it before)

[Kevin M]

If x^3 = constant, then all squares satisfying x^4 = x means there is an element 1*x = x for squares?
Can we deduce what this element does to non-squares?

[Kevin M]

Since the goal is to contradict eqn255, then if we try for x^3 = constant, that is like postulating an element that "detects" squares. 1◇x=x for squares, 1◇x!=x for non-squares.

[Kevin M]

Sorry, that is too strong (collapses to trivial). Just 1◇x!=x for at least one non-square.

[Andy Jiang]

Kevin M said:

Sorry, that is too strong (collapses to trivial). Just 1◇x!=x for at least one non-square.

ah it's interesting that collapses to trivial--could be interesting to understand the proof there

[Andy Jiang]

btw easy observation by vampire: such a universal cube must be idempotent b/c
(0 * 0)
=(0 * 0) * ((0 * 0) * ((0 * 0) * 0)) (substitute y=0 and x=(0 * 0) in 1516)
= (0* 0) * ((0 * 0) * 0) (by 0 is 0^3)
= (0 * 0) * 0 (by 0 is 0^3)
= 0 (by 0 is 0^3)

[Andy Jiang]

I guess the mechanism is really if y^3 = y then y^2 = y with no assumptions because you just substitute x= (y * y) in the equation and it collapses in a funny way

[Kevin M]

Maybe its worth trying to fill out a table again.
First an element to violate eqn255
0 != ((0◇0)◇0)◇0
which forces (0◇0) to be distinct so
1 = 0◇0
Then our "simplification guess" (x◇x)◇x = constant, which as you noted needs to be idempotent, so it is a distinct element.
2 = (x◇x)◇x
This forces:
2◇2 = 2
1◇0 = 2
2◇1 = 1
The element (0◇1) must be distinct, as well as the square of that. Vampire cannot decide if this is another violation of eqn255 or not. Knowing that we need an infinite magma to get a counter-example, and the square is a new element as well, maybe we can put that in here.

So yet another guess, with infinity in mind this time,
f(n+1) = f(n) ◇ (f(n) ◇ f(n))
with f(0) = 0,
could these all be considered non-squares, and violators of eqn255?

Unlike 1485 "shifts", this is more like "successor".
Since ideally all elements would be 'generated' from f(0) with multiplications, I wonder if there is some way the table is "symmetric" to only keeping the elements that can be generated by f(1). Basically, if we can somehow fill out the table such that each element has a "successor" count (or counts), like the f(n), then we can drop 0, reduce all the counts by 1, and get an equivalent table. This should be quite restrictive, so we can probably find a way to rule it out quickly if this cannot work.

[Terence Tao]

I spent some time trying to figure out what the free 1516 magma $M_{1516}$ looked like. In the case of $M_{854}$, the free 854 magma ended up having a carrier that was a subset of the free magma $M$ generated by a single binary operation $*$, with the actual operation $x \diamond y$ defined to equal $x*y$ when the pair $(x,y)$ is "irreducible", and $x$ if the pair is "reducible", with the former being the dominant case.

For 1516, because of the commutativity relation $CS = SC$ between the squaring map $Sx = x \diamond x$ and the cubing map $Cx = Sx \diamond x$, I think the base free magma $M$ has to be take this into account, and will therefore be the free magma generated by a binary operation $*$ and two commuting unary operations $S, C$. So every element $w$ of $M$ is either a generator, or is uniquely factorable into the form $S^s C^c (w_L * w_R)$ for some natural numbers $s,c$ and some smaller words $w_L, w_R \in M$. One can think of elements of $M$ as decorated trees in which the leaf nodes are generators and the branching nodes are decorated by pairs $(s,c)$ of natural numbers. For instance if $x,y$ are generators then $SC( (Sx * Cy) * (y * S^2x))$ would be a typical word in $M$. So $M$ is a magma with two commuting operations $S,C$, but I stress that these operations are not homomorphisms: $S(w_1 * w_2) \neq Sw_1 * Sw_2$ for instance.

My starting point the observation is that 1516 can be viewed as the law $Sy \diamond ( x \diamond (x\diamond y)) = x$, so the product of $Sy$ and $x \diamond (x \diamond y)$ is the "left factor" $x$ of $x \diamond (x \diamond y)$. Accordingly I am trying to work with an ansatz in which $M_{1516}$ has a carrier that is a subset of $M$, with the operation $x \diamond y$ defined to equal $x*y$ for "irreducible" pairs $(x,y)$, and defined to equal $y_L$ when $y = y_L * y_R$ and $(x,y_L,y_R)$ is a "reducible triple", and is equal to $z$ if $(x,y,z)$ is a "sporadic triple". Intuitively, reducible triples encode all the identities of the form $x \diamond (y_L \diamond y_R) = y_L$ with $y_L \diamond y_R$ irreducible that are forced by 854, and the sporadic triples encode all the other identities. My hope is that most pairs are irreducible, a few triples are reducible, and a very small number of triples are sporadic.

The hard part is to figure out all the definitions of the terms in quotes. The definition of irreducibility is clear: $(x,y)$ is irreducible if $y$ is not of the form $y = y_L * y_R$ for some reducible triple $(x,y_L,y_R)$, and there is no sporadic triple of the form $(x,y,z)$. To keep the operation well-defined, sporadicity also has to be a partial function (if $(x,y,z), (x,y,z')$ are sporadic, then $z=z'$) and disjoint from reducibility in the sense that if $(x,y_L,y_R)$ is reducible then $(x,y_L*y_R,z)$ cannot be sporadic. Then on splitting the 1516 law into various cases, one gets the following additional rules:

1. If $(x, x \diamond y)$ is irreducible, then $(Sy, x, x \diamond y)$ is reducible (or one could instead classify $(Sy, x * (x \diamond y), y)$ as sporadic, if this is more convenient).
2. If $(x, x \diamond y)$ is coming from a reducible or sporadic triple, then one has to classify $(Sy, x \diamond (x \diamond y), x)$ as sporadic. So for instance if $(x, x \diamond y, z)$ is sporadic then so is $(Sy, z, x)$.

Also, the definition of squares and cubes gives some initial sporadic triples $(x,x,Sx)$ and $(Sx,x,Cx)$. This generates a few more sporadic triples: $(S(a*Sa), Ca, Sa)$, $(S(Sa*Ca), S^2 a, Sa)$, $(SCa, Sa, Sa)$. The reducible triples include $(Sy, x, x * y)$ for irreducible pairs $(x,y)$ (plus a few coming from the sporadic triples), and propagate by the rule that if $(x,y,z)$ is reducible then so is $(S(y * z), x, y)$.

At one point I thought I had the whole system under control with a complete description of both the reducible and sporadic triples, but there are some annoying famillies of sporadic triples that show up, such as
$(S((y \diamond (y \diamond x)) \diamond ((y \diamond (y \diamond x)) \diamond x)), y, Sx)$
that reflects the identities
$Sx \diamond (((y \diamond (y \diamond x)) \diamond ((y \diamond (y \diamond x)) \diamond x)) = (y \diamond (y \diamond x)$
and
$Sx \diamond (y \diamond (y \diamond x) = y.$
There is some hope that the families of sporadic triples are still sufficiently under control that they can be described explicitly, and shown to not collide with each other or the reducible triples, but this is becoming quite a mess of an approach - in principle still formalizable, but worse than the task of formalizing the description of $M_{854}$ which was already somewhat complex. This approach might still be possible, but I am hoping that there are some other simpler approaches to rule out 255 specifically (which, in this language, corresponds to ensuring that $(Cx, x, x)$ does not emerge as a sporadic triple, which I think will be automatic if this scheme at all closes).

[Kevin M]

I made a little progress investigating the following idea

• $0 \neq ((0◇0)◇0)◇0$
• $x^3 := (x◇x)◇x = 2$
• infinite sequence:
  • $f(0)=0$
  • $f(n+1)=f(n) ◇ (f(n) ◇ f(n))$
  • $2◇f(n) \neq f(n)$

I'm not sure how this relates to Tao's idea as now CS=SC is trivialized to a constant map. (does this simplify things there, or break that approach?)

[Kevin M]

Anyway, I haven't found a contradiction yet, but here are some initial relations.
Square elements obey:

• $2◇x = x$ (since square elements satisfy eqn255)
• $x◇(x◇2) = x$

And all elements follow a combination of those two square relations

• $2 ◇ (x ◇ (x ◇ 2)) = x$

[Kevin M]

Then something interesting popped up with "left cubes".

• $x = (( (x◇(x◇x)) ◇ (x◇(x◇x)) )◇2) ◇ (x◇(x◇x))$
  or if we define the "left cube" $x_L^3 := x◇(x◇x)$

• $x = (( x_L^3 ◇ x_L^3 )◇2) ◇ x_L^3$

That gives a way to go "backward" along the sequence as well:
$f(n-1) = ((f(n) ◇ f(n))◇2)◇f(n)$

So a bi-directional "shift" operation seems to have shown up!

[Kevin M]

Andy Jiang said:

Kevin M said:

Sorry, that is too strong (collapses to trivial). Just 1◇x!=x for at least one non-square.

ah it's interesting that collapses to trivial--could be interesting to understand the proof there

I went back to look at this, and I had made a mistake writing the statement in the prover.
Vampire does not find a contradiction when I include axioms for the following:

! [A, B] : A=mul(mul(B,B),mul(A,mul(A,B)))  % eqn1516
0 != mul(mul(mul(0,0),0),0)  % an element refuting eqn255
! [A] : mul(mul(A,A),A) = 2  % "right" cube is a constant
! [A] : ( (? [B] : A = mul(B,B)) | (mul(2,A) != A) )  % (non-square  implies  2*x != x)

[Andy Jiang]

ok had some time this morning to play around with vampire and got
assuming 2=(x◇x)◇x for all x and left-cancellation
2◇(2◇x) = x (vampire seems to use left-cancellation to prove this)
(2◇(x◇x))◇x =2 (this follows from Kevin's above observation that 2 ◇ (x ◇ x) = (x ◇ x))
but did not find any simple + nontrivial homomorphisms of this magma
Edit:
((x ◇ x)◇x) = 2 = (x ◇ x) ◇(2◇(2◇x))
directly implies x=(2◇(2◇x)) by left-cancel

[Andy Jiang]

does suggest x -> 2◇x is some involution that fixes the squares (again assuming left-cancel + universal cube=2)

[Kevin M]

Generalizing the f(n) shifting, we can define:

• cube from left multiplying $x^3_L = x ◇ (x◇x)$
• $\text{shift}(x) := x^3_L$
• $\text{unshift}(x) := ((x ◇ x)◇2)◇x$

From the result forced by $((x ◇ x)◇x)=2$.
$x = (( x_L^3 ◇ x_L^3 )◇2) ◇ x_L^3$
This gives $\text{unshift}(\text{shift}(x))=x$.

However, with everything I assumed so far, even adding left-cancelation, it does not imply shift(unshift(x))=x.
Throwing that in as yet another axiom, still no contradictions.
Maybe that is the missing piece to simplify everything?

[Terence Tao]

Just wanted to say that I hope this approach of imposing simplifying axioms such as constant cubes and left-cancellability will work like it did for 1485; it is almost the opposite approach of the free approach in which one wants to keep everything as distinct as possible, but this leads one to the edge of a combinatorial explosion in relations. I think it might barely close for 1516 and leave us with an in-principle describable free magma, but it is extremely complex.

One small comment is that the linear model $x \diamond y = 4x+y = {\mathbb Z}/7{\mathbb Z}$ has constant cubes. Of course we know that translation-invariant or finite models are not good for this problem, but perhaps it might still supply some intuition.

[Michael Bucko]

Kevin M schrieb:

Andy Jiang said:

Kevin M said:

Sorry, that is too strong (collapses to trivial). Just 1◇x!=x for at least one non-square.

ah it's interesting that collapses to trivial--could be interesting to understand the proof there

I went back to look at this, and I had made a mistake writing the statement in the prover.
Vampire does not find a contradiction when I include axioms for the following:

! [A, B] : A=mul(mul(B,B),mul(A,mul(A,B)))  % eqn1516
0 != mul(mul(mul(0,0),0),0)  % an element refuting eqn255
! [A] : mul(mul(A,A),A) = 2  % "right" cube is a constant
! [A] : ( (? [B] : A = mul(B,B)) | (mul(2,A) != A) )  % (non-square  implies  2*x != x)

I'm quite new to Vampire. I turned this script into this format. Is that how you are also using it?

fof(eq1516, axiom, ! [A, B] : (A = mul(mul(B, B), mul(A, mul(A, B))))).

fof(refute_eq255, axiom, 0 != mul(mul(mul(0, 0), 0), 0)).

fof(right_cube_constant, axiom, ! [A] : (mul(mul(A, A), A) = 2)).

fof(non_square_implication, axiom,
    ! [A] : ((? [B] : (A = mul(B, B))) | (mul(2, A) != A))).

(it ran for 60s and also didn't find a contradiction)

[Michael Bucko]

Tried to solve Equation1516_implies_Equation255 using Duper (1,000,000 hearbeats), but it asked for more heartbeats. I'll try with 10,000,000.

[Michael Bucko]

Ran it with 10,000,000 heartbeats - no results.

[Andy Jiang]

random observation there's a size 8 model of form
(a,b,c) * (d,e,f) = (a+b+e,d+e+f+a+c,e+f+b) everything mod 2
idk if this is linear in a finite field or something
I would guess no? But I guess generalizations of these are ruled out by linear

[Amir Livne Bar-on]

Noting here the three linear models of order 7, they have quite different properties. One of them might turn out to be useful.

(a) $x \diamond y = 4x + y$ has constant cubes (where cube is $(x \diamond x) \diamond x$)
(b) $x \diamond y = 4x + 5y$ has constant left-cubes (expressions of the form $x \diamond (x \diamond x)$
(c) $x \diamond y = 6x + 2y$ has $x \diamond x = x$

These operations can be derived from one another, for example $x \diamond_b y = x \diamond_a (y \diamond_a y)$.

[Kevin M]

Apologies, but I have a really basic question.
I'm having a bit of trouble understanding what needs to be proven to show that we have a well-defined infinite algebra when we only have one relation to enforce.

Let's consider this toy model:

I'll represent elements as a generator A, or 2-tuples of other elements.
-- define:
head(element) = head of tuple if element is a 2-tuple
                or (A,A) if element is A
tail(element) = tail of tuple if element is a 2-tuple
                or (A,(A,A)) if element is A
x * y = head(y) if head(x) = tail(x) and head(y) = head(tail(y)) and head(x) = tail(tail(y))
           else (x,y)

Note:
x*A != A, because head(A) != head(tail(A)).
So ((A*A)*A)*A != A, violating eqn255.

Basically, each element is defined as the history of how it was generated (with A treated as a special "self-referential" object). Then the multiplication can access this history to enforce the one relation.

If there were multiple relations to enforce, I could see a potential issue where inconsistencies could arise due to the order these are applied or something. But here we only have a single relation. So any other relation derivable from it would have to just be multiple applications of that same relation. So isn't that already encoded in above? I realize this is very hand-wavey, but I'm not sure how to make it more precise to see what I'm missing. And I'm having trouble working on an infinite model without resolving this misunderstanding.

[Andy Jiang]

don't you just have to show that your magma obeys 1516? then it's enough I think

[Terence Tao]

Note that not all expressions of the form $Y = x*(x*y)$ will have the form $head(Y) = head(tail(Y))$ because $x*y$ need not be $(x,y)$ and $x*(x*y)$ need not be $(x,(x,y))$. Similarly for the other two conditions you propose. One can try to make the definition of the multiplication operation more complicated to handle the other cases, but it's a recursive process, every new change one makes to the magma operation generates a new edge case that potentially needs to be handled. This is basically what I tried to do a few days ago; I do think the process will eventually converge, but the rule is not going to be anywhere near as simple as what you propose.

[Andy Jiang]

If I calculated correctly (which is unlikely tbh) I think this particular one fails 1516 for X=(A,A) and Y=((A,A),A)
Edit: I take it back
Edit2: I think actually it does fail at those inputs...

[Andy Jiang]

btw what's simplest model we know of 1516 with non-square elements?

[Terence Tao]

I'm not sure we have one yet

[Andy Jiang]

I think vampire can't refute the existence of a model with left-cancel and ((X * X) * X) always = 2 with only 2 non-squares elements which are swapped by the involution x -> 2 * x. Although these conditions are not the simplest so I'm not sure how much weight to put on that

[Andy Jiang]

Personally feel like it might be possible to fill in the multiplication greedily row by row b/c the conditions can be written with left multiplication. Like posit two non-squares 0 and 1 which are swapped by left-multiplication by 2 and assume 2 is universal right cube and left-cancellation--I still think these conditions +1516 is not extremely strong on the table. But I haven't seriously tried so could be missing something obvious.

[Andy Jiang]

OK upon further thought I think it's probably not so simple...

[Amir Livne Bar-on]

Some more finite models for 1516:

I asked Mace4 for non-idemponent models of order 9, and got this one. I did a bit or renaming, guided by the existence of an element $e$ that satisfied $x \diamond e = x$ and $(e \diamond x)^2 = e \diamond x^2 = x$. It has the further property that $x^3 = e \diamond (e \diamond x)$, which I don't know if follows from these (it's equivalent to $((x^3)^2)^2=x$). Can anyone identify this as some known algebraic structure?

  | e 0 1 2 3 4 5 6 7
--+------------------
e | e 7 0 1 2 3 4 5 6
0 | 0 1 4 2 7 6 e 3 5
1 | 1 6 2 5 3 0 7 e 4
2 | 2 5 7 3 6 4 1 0 e
3 | 3 e 6 0 4 7 5 2 1
4 | 4 2 e 7 1 5 0 6 3
5 | 5 4 3 e 0 2 6 1 7
6 | 6 0 5 4 e 1 3 7 2
7 | 7 3 1 6 5 e 2 4 0

Order 8 had only idempotent models, here's an example after slight renaming (which might confuse more than help). Again I can't identify this operation.

  | 0 1 2 3 4 5 6 7
--+----------------
0 | 0 2 3 4 5 6 7 1
1 | 4 1 6 0 7 3 5 2
2 | 5 3 2 7 0 1 4 6
3 | 6 7 4 3 1 0 2 5
4 | 7 6 1 5 4 2 0 3
5 | 1 4 7 2 6 5 3 0
6 | 2 0 5 1 3 7 6 4
7 | 3 5 0 6 2 4 1 7

There were no 1516 magmas of order 10 (this is a merge of results of 2 long runs and I might have had a bug). Order 11 has a single linear model $7x+5y$ which is idempotent, and Mace4 is having a lot of trouble finding a non-idempotent model, but hadn't ruled it out yet.

[Amir Livne Bar-on]

Checked with an ATP, 1516 and $((x^3)^2)^2=x$ together imply 255

[Andy Jiang]

Matthew Bolan said:

I think prover9 is telling me the only models with $x^2 = \pm 1$ are trivial.

just for kicks I asked vampire the case where there are three squares and so far on my machine it hasn't proved 255 from it yet.
Edit: Nevermind

[Kevin M]

Hmm... it's not the most constructive, but here is an attempt at a finite algorithm defining an eqn1516 magma that violates eqn255.

Represent elements as a generator 0, or 2-tuples of other elements.
As before we define L * R = (L,R) unless a simplification using eqn1516 is possible.

A "simplification" will happen in L * R when there are x,y such that L=(y ◇ y) and R=(x ◇ (x ◇ y)),
in which case L * R = x.

Squaring will never trigger a simplification, so for all x, x * x = (x, x).
This means we can determine if L is a square, and get y from L unambiguously.

The simplification rule is enforcing eqn1516, x = (y ◇ y) ◇ (x ◇ (x ◇ y))
and therefore ( (x ◇ (x ◇ z)) = (y ◇ (y ◇ z)) ) <-> (x=y).
So given elements R,y if we find an x such that R=(x ◇ (x ◇ y)), it is unique.

The depth of the tuple L * R (if viewed as defining a tree), will be less than the max depth of L or R if a simplification occurred. So given R and y, we can just search for an x with depth < max(depth(R), depth(L)) such that R=(x ◇ (x ◇ y)). If we find one, it is unique. If none is found, there is no smaller depth element to reduce to, and the result is just the tuple (L,R).

[Daniel Weber]

Isn't it possible that a simplification occurred in the definition of R?

[Kevin M]

yes, that is what the search is intended to handle.

[Daniel Weber]

But then can't the depth of R be less than the depth of x?

[Kevin M]

Yes, but if L * R can result in a simplification, we must be able to write R in the form x * (x * y) where y comes from L = y * y = (y, y). And we'll search for x up to max(depth(L), depth(R)). So in some cases we will search beyond the depth of R.

[Daniel Weber]

But isn't it possible that y is very small, x is very large, but some sequence of simplifications caused R to simplify to something smaller than x?

[Terence Tao]

I think you are going down a similar path to the one I took in trying to construct something close to the free 1516 magma. I think the approach has a chance of eventually working, but is quite complex and as such I was reluctant to push for it. But since it seems to be emerging organically, perhaps I will share more of the computations that I have.

Say that $(x,y,z)$ is a "simplification triple" if one has $x \diamond (y \diamond z) = y$. Then 1516 asserts that $(Sy, x, x \diamond y)$ is a simplification triple for any $x,y$, where $Sy = y \diamond y$ is the squaring operator. One can hope that most of the time one can write $x \diamond y = (x,y)$ (and also $x \diamond (x \diamond y) = (x,(x, y))$), and that the simplification rules given by this case (i.e., $Sy \diamond (x,(x,y)) = x$) are close to a complete set of simplifications. This was where I was a few days ago, and I'm guessing that this is the hope right now.

But there are some complications. Firstly, there is a propagation property of simplification triples:

Lemma 1. If $(x,y,z)$ is a simplification triple, then so is $(S(y \diamond z), x, y)$.

Proof: By hypothesis, $y = x \diamond (y \diamond z)$, thus $S(y \diamond z) \diamond (x \diamond y) = S(y \diamond z) \diamond (x \diamond (x \diamond (y \diamond z))) = x.$ $\Box$

So in addition to the original simplification triples $(Sy,x, x \diamond y)$, one also has

$(S(x \diamond (x \diamond y)), Sy, x)$

$(S(Sy \diamond x), S(x \diamond (x \diamond y)), Sy)$

$(S(S(x \diamond (x \diamond y)) \diamond Sy), S(Sy \diamond x), S(x \diamond (x \diamond y)))$

and so forth.

This still isn't so bad, one could just add all of these to the list of simplification rules, show that they don't conflict with each other, and hope that now we have a near-complete list of simplifying rules. I tried this, but another problem emerged. There are some "sporadic" simplifying rules $a \diamond b = c$ that are not of the standard form $x \diamond (y \diamond z) = y$ (in the sense that $b$ is not expected to be of the form $b = (c,d)$ for some $d$). An example is the rule $SCx \diamond Sx = Sx$, where $Cx$ is the cubing map $Cx = Sx \diamond x$ (this is related to the previously observed fact that $S$ and $C$ commute, as well as the fact that in the constant cubing case $Cx = 2$ one has $2 \diamond Sx = Sx$). At first I thought there were only a small number of sporadic rules (a finite number of rules parameterized by one variable $x$), but then I found more due to this lemma:

Lemma 2. If $(x,y,z)$ and $(x, y \diamond z, w)$ are simplifying triples, then we have the sporadic identity $S((y \diamond z) \diamond w) \diamond y = x$.

Proof: By hypothesis, $x \diamond (y \diamond z) = y$ and $x \diamond ((y \diamond z) \diamond w) = y \diamond z$, thus $S((y \diamond z) \diamond w) \diamond y = S((y \diamond z) \diamond w) \diamond (x \diamond (x \diamond ((y \diamond z) \diamond w)) = x$. $\Box$

For instance, since we know $(Sy,x,x \diamond y)$ and $(Sy, x \diamond (x \diamond y), (x \diamond (x \diamond y)) \diamond y))$ are simplifying triples, we have the sporadic identity $S F(x,y) \diamond x = Sy$, where $F(x,y)$ is the word

$F(x,y) = (x \diamond (x \diamond y)) \diamond ((x \diamond (x \diamond y)) \diamond y).$

Okay, so we have to add a few sporadic identities in addition to the previous families of simplifying triple identities. Now do we have something close to a complete set of simplifying rules? Well, unfortunately sporadic identities beget further sporadic identities:

Lemma 3. If we have a sporadic identity of the form $Sx \diamond y = z$, then we get another sporadic identity of the form $S(y \diamond (y \diamond x)) \diamond z = Sx$.

Proof. $S(y \diamond (y \diamond x)) \diamond z = S(y \diamond (y \diamond x)) \diamond (Sx \diamond Sx \diamond (y \diamond (y \diamond x)) = Sx.$ $\Box$

So for instance starting from $SF(x,y) \diamond y = Sx$ we have

$S(F(x,y) \diamond (F(x,y) \diamond x)) \diamond Sx = SF(x,y)$

and this can be iterated further to obtain an increasingly complex sequence of sporadic identities.

So, now are we done? Regrettably, there is another propagation vector: sporadic identities also generate new simplifying triples!

Lemma 4. If we have a sporadic identity $x \diamond y = z$, then we have a simplifying triple $(Sy, x, z)$.

Proof. This is just a specialization of the previous observation that $(Sy, x, x \diamond y)$ is always a simplifying triple. $\Box$

So now we have a potential feedback loop in which simplifying triples and sporadic identities beget each other in a combinatorial explosion. However, with my computations it seems that this explosion is barely averted: the "simplifying triple -> sporadic identity" vector in Lemma 2 requires two simplifying triples to create a sporadic identity, and it appears that all of the additional simplifying triples beyond the standard ones $(Sy, x, x * y)$ do not actually generate any further sporadic identities, and so the process stops with a finite (but rather complex) collection of families of both simplifying triples and sporadic identities.

I believe that if one then writes down all these identities (as well as the commutativity law $SC x = CSx$), one can use this to build a version of Kevin's magma that actually does obey 1516 in all cases, and is in fact the free 1516 magma (because every rule one imposed is actually forced on us by 1516), but the verification of this is extremely lengthy and tedious - longer for instance than the verification of the free 854 magma in the blueprint. If it seems like this is the only way to resolve this equation I can try to get all the details into the blueprint, but I was really hoping that there was another way to proceed here.

[Terence Tao]

It's possible that the theory of terminating rewriting systems can be deployed to automatically check that the final set of rewriting rules is actually complete. The main issue is that this is not a finite set of rules, but has some infinite families (and even a doubly infinite family, obtained by the many applications of Lemma 3 applied a standard sporadic triple, then one application of Lemma 4, then many applications of Lemma 1). However, I think it may be possible to truncate the family and create a slightly overcomplete, but now finite, set of rewriting rules. This would no longer generate the free 1516 magma but could still be enough to resolve the implication to 255. Is there an automated way to verify completeness of a finite set of rewriting rules? In that case I can relatively easily generate a candidate set of such rules.

[Kevin M]

I remember a blog post of Scott Aaronson about using some automated tooling for verifying termination of rewriting rules. Let me see if I can find that.

[Kevin M]

Oh, it was his Collatz paper.

maybe these would be useful:
https://github.com/jwaldmann/matchbox
https://aprove.informatik.rwth-aachen.de/

[Matthew Bolan]

When you say "verify completeness", you mean verifying that all rules in the original rewriting system belong to the new one?

[Terence Tao]

Perhaps I am using the wrong terminology - I am not sufficiently familiar with the language of rewriting systems to be sure - but basically one has a magma operation $\diamond$ on the free magma generated by a single pairing operation $(,)$ and two commuting unary operators $C,S$, which is usually just the pairing operation $x \diamond y = (x,y),$ but with a finite number of exceptional rules, the most common of which is
$Sy \diamond (x,(x,y)) = x$
and also the defining rules for $S,C$
$x \diamond x = Sx$
$Sx \diamond x = Cx$
but there are others such as
$S((x,(x,y)) \diamond (Sy,x) = x$
$SCx \diamond Sx = x$
$SF(x,y) \diamond x = Sy$
(where $F(x,y) = ((x,(x,y)), ((x,(x,y)),y))$), and so forth (I think I have about 20 such rules overall). I would like to show that the magma with this ruleset (a) is well-defined (in that there are no conflicting rules of the form $x \diamond y = z$ and $x \diamond y = z'$ with $z \neq z'$), (b) obeys 1516, and (c) does not obey 255 (this one I expect to be easy). It is (b) which is tricky because 1516 involves three magma operations and naively one has 21^3 cases to check if there are 20 different exceptions to the rule $x \diamond y = (x,y)$, but perhaps this can be done automatically.

If I wanted the free magma, I think I would need to specify an infinite family of such rules, but for the purposes of ruling out 255 it would be enough to have a finite set of rules that include all the rules forced by 1516, but a few unnecessary ones that simplify the ruleset. For instance, any rule obtained using two or more applications of Lemma 1 above from a simplification triple $(x,y,z)$ will be of the form
$S(x,y) \diamond (S(y,z), x) = S(y,z)$
so I was thinking of simply adding _all_ such rules of this form to the ruleset, regardless of whether $(x,y,z)$ was already known to be a simplification triple, with the intuition that the inputs $S(x,y)$ and $(S(y,z),x)$ here are highly related to each other and this rule is unlikely to cause significant problems as it is so rarely invoked. This way I can truncate all applications of Lemma 1 beyond the second one.

EDIT: I considered also adding a rule such as $Cx = 2$ but actually this does not seem to simplify the ruleset much, as most of the rules do not actually involve $C$. This may help explain why this alternate approach to the problem was only yielding limited progress.

[Pace Nielsen]

I have been experimenting with the Kisielewicz ansatz for 1516, trying to come up with (hopefully) an easier description on the free 1516 magma, or something close to it, as follows.

Think of our carrier set as the positive integers, and take as our first "rule" the equality

$$(0)\qquad a\diamond a = p_1(x)$$

where $p_1$ is some (injective) function on the positive integers, mapping to a nice, easily recognizable image. (For instance, we might take $p_1(a)=2^a$, in which case that nice subset would be "powers of 2".) Using the 1516 identity $x=S(y)\diamond(x\diamond(x\diamond y))$, we can now iterate and define new rules as follows.

Taking $x=a,y=a$, we get the identity $a=p_1(a)\diamond (a\diamond p_1(a))$. So we can take

$$(1)\qquad a\diamond p_1(a)=p_2(a)$$

$$(2) \qquad p_1(a)\diamond p_2(a)=a$$

Again, we would like to think of $p_2$ as a nice function, mapping to somewhere "new", something like $p_2(a)=3^a$, although we'll keep things arbitrary for now.

We can use (2), taking $x=p_1(a),y=p_2(a)$ to get the identity $p_1(a)=p_1p_2(a)\diamond (p_1(a)\diamond a)$. So we can take

$$(3) \qquad p_1(a)\diamond a=p_3(a)$$

$$(4) \qquad p_1p_2(a)\diamond p_3(a)=p_1(a)$$

We can use (3), taking $x=p_1(a),y=a$ to get $p_1(a)=p_1(a)\diamond(p_1(a)\diamond p_3(a))$. So we can take

$$(5) \qquad p_1(a)\diamond p_3(a)=p_4(a)$$

$$(6)\qquad p_1(a)\diamond p_4(a)=p_1(a)$$

Using (5), taking $x=p_1(a),y=p_3(a)$ we get $p_1(a)=p_1p_3(a)\diamond (p_1(a)\diamond p_4(a)) = p_1p_3(a)\diamond p_1(a)$. So we just get

$$(7) \qquad p_1p_3(a)\diamond p_1(a)=p_1(a)$$

Now using (7), taking $x=p_1p_3(a),y=p_1(a)$ we get $p_1p_3(a)=p_1^2(a)\diamond (p_1p_3(a)\diamond p_1(a)) = p_1^2(a)\diamond p_1(a)=p_3p_1(a)$. This means that $p_1,p_3$ commute. Of course, we already knew this because squaring and cubing commute. (But it is nice to see it arise again.) If we think of $p_1$ as a somewhat "generic" exponentiation map on the positive integers, then the only other nice maps that commute with it are powers of it.

I tried experimenting with taking $p_3=p_1^0,p_1^1,p_1^2$, but in those three cases eventually problems arose. I'm starting to think that this method is unfortunately unworkable when taking cubing to be a simple integer power of squaring. [Maybe someone can see an easy reason for this.]

[Pace Nielsen]

Maybe a better carrier set would be something like $(\mathbb{Z}_{>0}\times \mathbb{Z}/2\mathbb{Z}) \cup \{\infty\}$, where we treat infinity as the constant value of cubing, and right multiplication by it is the obvious "shift the second coordinate" involution?

[Terence Tao]

Ugh, it turns out there is a fifth vector, again from sporadic pairs to simplifying triples:

Lemma 5. If $Sy \diamond x = z$, then $(Sz, S(x \diamond (x \diamond y)), Sy)$ is a simplifying triple.

Proof. From 1516, $(Sy, x, x \diamond y)$ is a simplifying triple, hence by Lemma 1 so is $(S(x \diamond (x \diamond y)), Sy, x)$, and hence by Lemma 1 again so is $(S(Sy \diamond x), S(x \diamond (x \diamond y)), Sy)$. Substituting $Sy \diamond x = z$, we obtain the claim. $\Box$

Assuming no more vectors show up, I can truncate to a ruleset of size about 60 rules, but now the generation of the rules as well as its verification both need to be computer generated, as there are just too many opportunities for mistakes here.

[UPDATE: Actually, things are not as bad as I feared. Lemma 5 is actually just Lemma 3 followed by Lemma 4, so doesn't actually generate new rules.]

My explorations did produce one unusual sporadic rule, namely
$(Sx \diamond Cx) \diamond ((Sx \diamond Cx) \diamond x) = Cx$
which I believe is actually forced from 1516 (perhaps this can be checked with an ATP: UPDATE, see below, this is not quite implied by 1516 unless one assumes injective squares) and which may possibly be useful in advancing the "assume $Cx=2$" strategy. (This is an unusual rule in that it is a rule of the form $x \diamond y = z$ where the first argument $x$ is not obviously a square. The only other rule of this type I have discovered is the rule $x \diamond x = Sx$ defining $S$.)

[Terence Tao]

IMG_1224.jpeg in case anyone is interested, here are the rewriting rules I found so far, which may be complete enough to verify 1516 in all cases (but now there are like 60^3 cases to check)

[Terence Tao]

@Pace Nielsen I think I have generated a similar list of sporadic laws involving squares and cubes. My list is

1. $x \diamond x = Sx$
2. $Sx \diamond (x \diamond Sx) = x$
3. $Sx \diamond x = Cx$
4. $Sx \diamond (Sx \diamond Cx) = Sx$
5. $S(x \diamond Sx) \diamond Cx = Sx$
6. $S(Sx\diamond Cx) \diamond S^2 x = Sx$
7. $SC x \diamond Sx = Sx$
8. $S((x \diamond Sx) \diamond ((x\diamond Sx) \diamond x)) \diamond x = Sx$
9. $S((Sx \diamond Cx) \diamond ((Sx \diamond Cx) \diamond x)) = SCx$ (correcting a previous version)
10. $S( (Cx \diamond (Cx \diamond (x \diamond Sx))) \diamond Sx = S(x \diamond Sx)$
11. $S((S^2 x \diamond (S^2 x \diamond (Sx \diamond Cx))) \diamond Sx = S(Sx \diamond Cx)$

and then there are about two dozen more of an irregular "simplifying triple" form (basically applying Lemma 4 or Lemma 5 to the above list, followed optionally by one application of Lemma 1), and the rest lie in about three infinite families (formed by two applications of Lemma 1, or two applications of Lemma 4). (Somehow the exercise reminds me of learning about irregular verbs and obscure tenses in French.) I can imagine that setting $C = S$ or $C=S^2$ causes clashes here, though I'm a little surprised that $C = S^0$ caused an issue given all the previous analysis of the $Cx=2$ case.

But actually the most frequent rules that show up don't involve any unary operator beyond squaring, so I now think that trying to fix the other unary operators in terms of squaring may not yield decisive simplifications (one may get from say 60 rules down to 40 or so, but still computer assistance would be required). For instance, the rule $S F(x,y) \diamond x = Sy$, where $F(x,y) := B(B(x,y),y)$ and $B(x,y) := (x \diamond (x \diamond y))$, doesn't involve anything other than squaring, but is a relatively frequent rule that one encounters when trying to verify the (many) cases of 1516, largely because one of the inputs $x$ and the output $Sy$ are almost completely unconstrained. (Most of the rules have so many constraints between their inputs and outputs that their case analysis is quite easy to resolve, but the ones in which two out of the three of the inputs and outputs are relatively unconstrained cause difficulties in that they keep generating new identities out of old, as captured by Lemmas 1-5.)

[Kevin M]

I'm having trouble verifying number 9 and 11 with vampire.

[Terence Tao]

For 11, the proof should start with equation 6, $S(Sx\diamond Cx)\diamond S^2x=Sx$, which should imply
$Sx = S(Sx \diamond Cx) \diamond (S(Sx\diamond Cx) \diamond (S^2 x \diamond (S^2 x \diamond (Sx \diamond Cx))),$
and on multiplying both sides on the left by $S(S^2 x \diamond (S^2 x \diamond (Sx \diamond Cx)))$ one should get the claim. If some of these previous claims are not proven by Vampire, that would pinpoint where the error lies.

For 9, I think I removed a square incorrectly. Is the weaker claim
$S( (Sx \diamond Cx) \diamond ((Sx \diamond Cx) \diamond x)) = SCx$
proven by Vampire?

[Amir Livne Bar-on]

Trying to understand the finite models above, the order 8 model is isomorphic to a linear model on $(F_2)^3$, with the matrix

1 1 0 0 1 0
1 1 1 1 0 1
1 0 1 1 0 0

where the convention is that the first operand is concatenated to the second to create a vector in $(F_2)^6$, which is multiplied with this matrix.

[Kevin M]

prover9 found 11 (so I probably wrote something a bit off for vampire), but no luck with 9 still

[Kevin M]

okay, found a missing parens for 11 in vampire, that is all okay now.
adding S to both sides of 9, it now proves that as well.

[Terence Tao]

OK then I will correct my text, thanks for confirming.

[Jose Brox]

Pace Nielsen ha dicho:

I have been experimenting with the Kisielewicz ansatz for 1516

I also tried the Kisielewicz sword against the 1516 boss for a while, in the end I move to other things because I run into problems with all the options I tried... Basically, when confronting an ambiguity there are two possibilities: either allow the iteration of the existing functions and add a new rule for the new case, or add new functions to resolve the ambiguity. If I recall correctly, in the 1516 case there were a lot of these choices (I also tried with 854, etc.).

[Jose Brox]

(where Terry has a set of blackboards, I have a Kisielewicz paper's ocean :sweat_smile: :grinning_face_with_smiling_eyes:)
20241105_225837.jpg

[Pace Nielsen]

@Jose Brox Yeah, unless I see some simplifying principle, the Kisielwicz ansatz seems to be just reproducing some of (with less generality) Terry's computations.

[Jose Brox]

Jose Brox ha dicho:

I also tried the Kisielewicz sword against the 1516 boss

Although provisional and abandoned, I share here
Kisielewicz model for equation 1516.pdf
my try at the Kisielewicz model, just in case it may be useful. I changed it multiple times, so there will be mistakes.

[Terence Tao]

Pace Nielsen said:

Jose Brox Yeah, unless I see some simplifying principle, the Kisielwicz ansatz seems to be just reproducing some of (with less generality) Terry's computations.

Yeah, if you replace the free magma with the natural numbers, the pairing operation $(x,y)$ with say $2^x 3^y$, and the squaring and cubing operations with say $Sx = 5x$ and $Cx = 7x$ then I think one can convert the model I am proposing into a (very complicated) Kisielewicz type model.

While the model is horrible to describe in human-readable terms, I think I can describe in (barely) human-readable form what properties the model has to satisfy, and propose an initial candidate for the model (as I said, it will have about 60 or so rules, but they can be "procedurally generated" from a smaller seed to a certain extent). It may therefore be possible to get to the point where the model can be first computer verified, and then formally verified. Will send an update on this later today.

[Andy Jiang]

Sorry naive question: why is the carrier set the free magma with no relations (i assume single generator so it's like binary trees)? I would've thought you would define it in reduced trees (relative to your rules) and show that the reduction rules are confluent (Diamond lemma sort of thing like no reduction choice should make a difference in the end). What does completeness of rewriting mean in this setting(sorry if it's a standard term I'm happy to read a reference)? Sorry if you already explained above but I didn't quite understand. Like if you do it this way with all the rules not a modified set, why do you generate the free 1516? I don't understand because your carrier contains unreduced expressions--I think I'm missing something simple

[Terence Tao]

This may be a better approach (restricting only to words that are reduced, and demonstrating confluence of the set of reduction laws). You are right that what I am trying to prove here is slightly stronger than is needed, which is that the magma operation on even the non-reduced words still satisfies 1516. To get to the free 1516 magma, one then has to restrict to the subset of words which can actually be generated from the magma operation, which is probably the same thing as the set of reduced words.

So perhaps the ruleset can be written in terms of just $\diamond$ (and also $S$ and $C$, which I still believe should be kept separate operations otherwise the commutativity property $SC=CS$ is going to cause real headaches) abandoning explicit use of the pairing map $(,)$, and one might be able to check confluence of the system which would be a slightly different, but certainly viable, way to proceed.

[Andy Jiang]

Oh I didn't mean it as a suggestion of improvement haha I was only trying to understand! Also does theory guarantee that confluence/rewriting system completeness is decidable by some algorithm? Is the idea that two reductions can only overlap in finitely many ways and you just enumerate all the ways and each way have a common reduction?

[Andy Jiang]

Oh sorry is it correct to say for the rewriting system you only do a single reduction step at multiplication time with one of your rules, and the only thing you need to check is 1516 is satisfied in the constructed magma? Where you take binary trees as carrier and multiplication is check against all rules and if not matching then join into a larger tree?

[Terence Tao]

Here is part I of the complex proposal to build a nearly free 1516 magma. It requires one to guess a good ruleset of "sporadic rules" and "simplifying rules" that need to obey 12 axioms, but I am still working on a viable proposal for what that good ruleset might be. Most likely the first few iterations of the proposal won't quite close and so one will need to keep tweaking it. This is a very tedious and error-prone process to do by hand, so we may have to look into more automated options.

--

We work in the free algebra generated by a pairing operation $(,)$ and two commuting unary operators $S,C$, and some set of generators (one could also work with the natural numbers with pairing $(x,y)=2^x 3^y$, $Sx = 5x$, and $Cx=7x$, but I don't think this actually simplifies anything). We assume that we have a collection of "sporadic rules" $x \diamond y = z$, as well as "simplifying rules" of the form $x \diamond (y,z) = y$ for some collection of "simplifying triples" $(x,y,z)$. This lets us define an operation $\diamond$ on the free algebra by the following rules:

• (Sporadic case) If $x \diamond y = z$ is a sporadic rule, then we define $x \diamond y$ equal to $z$.
• (Simplifying case) If $(x,y,z)$ is a simplifying triple, we define $x \diamond (y,z)$ equal to $y$.
• (Generic case) In all other cases, we define $x \diamond y$ to equal $(x,y)$.

In order for this to give a magma, we need to verify two axioms:

Axiom 1. If $x \diamond y = z$ and $x \diamond y = z'$ are both sporadic rules, then $z=z'$.
Axiom 2. If $(x,y,z)$ is a simplifying triple, then there are no sporadic rules of the form $x \diamond (y,z) = w$.

We would like to have $x \diamond x = Sx$ for all $x$, so we impose

Axiom 3. For any $x$, $x \diamond x = Sx$ is a sporadic rule.

Now we need to verify 1516, which is $Sx \diamond (y \diamond (y \diamond x)) = y$. Note that $y \diamond x$ can be sporadic, simplifying, or generic; and $y \diamond (y \diamond x)$ can also be sporadic, simplifying, or generic. So there are nine cases to consider.

Case 1: $y \diamond x$ is generic; $y \diamond (y \diamond x)$ is generic. Then we need to show $Sx \diamond (y, (y,x)) = x$ and so it will suffice to have

Axiom 4. If $y \diamond x$ and $y \diamond (y,x)$ are generic, then $(Sx, y, (y,x))$ is a simplifying triple.

Remark: This axiom should somehow contribute the "most frequently encountered" simplifying triples (otherwise this method is unlikely to work).

Case 2: $y \diamond x$ is simplifying; $y \diamond (y \diamond x)$ is generic. Then we have $x = (z, w)$, $y \diamond x = z$, and $y \diamond z$ generic. So we need to have

Axiom 5. If $(y,z,w)$ is a simplifying triple and $y \diamond z$ is generic, then $(S(z,w), y, z)$ is a simplifying triple.

Remark: Iterating this axiom twice, we expect to see simplifying triples of the form $(S(y,z), S(z,w), y)$. I am hoping we can truncate the ruleset by declaring all such triples to be simplifying triples.

Case 3: $y \diamond x$ is sporadic; $y \diamond (y \diamond x)$ is generic. Then we have some sporadic rule $y \diamond x = z$ and $y \diamond z$ is generic. So it suffices to have

Axiom 6. If $y \diamond x = z$ is a sporadic rule and $y \diamond z$ is generic, then $(Sx, y, z)$ is a simplifying triple.

Remark: This axiom basically means that every sporadic rule also generates a simplifying triple.

Case 4: $y \diamond x$ is generic; $y \diamond (y \diamond x)$ is simplifying.

In this case $y \diamond (y \diamond x) = y$. So we need

Axiom 7. If $y \diamond x$ is generic and $(y,y,x)$ is a simplifying triple, then $Sx \diamond y = y$ is a sporadic rule.

Remark: I am hoping that this axiom only activates very rarely.

Case 5: $y \diamond x$ is simplifying; $y \diamond (y \diamond x)$ is simplifying.

We now have $x = ((z,w),u)$ for some simplifying triples $(y,(z,w),u)$ and $(y,z,w)$. So we need

Axiom 8. If $(y,(z,w),u)$ and $(y,z,w)$ are simplifying triples, then $S((z,w),u) \diamond z = y$ is a sporadic rule.

Remark: I am hoping that this axiom mainly only activates when both simplifying triples arose from Axiom 4. This gives rise to the sporadic rules $SF(x,y) \diamond x = Sy$ where $F(x,y) = B(B(x,y),y)$ and $B(x,y) = (x,(x,y))$. Another consequence of this axiom is that if $x \diamond y = z$ is sporadic, then almost certainly we will have to have the sporadic rule $S B((x,z),y) \diamond x = Sy$.

Case 6: $y \diamond x$ is sporadic; $y \diamond (y \diamond x)$ is simplifying.

So now $y \diamond x = (z,w)$ is a sporadic rule and $(y,z,w)$ is a simplifying triple. The axiom we need then is

Axiom 9. If $y \diamond x = (z,w)$ is a sporadic rule and $(y,z,w)$ is a simplifying triple, then $Sx \diamond z = y$ is a sporadic rule.

Remark: I am hoping that this axiom activates very rarely.

Case 7: $y \diamond x$ is generic; $y \diamond (y \diamond x)$ is sporadic.

Here we have $y \diamond (y,x) = z$ as a sporadic rule. So the axiom needed here is

Axiom 10. If $y \diamond x$ is generic and $y \diamond (y,x) = z$ is a sporadic rule, then $Sx \diamond z = y$ is a sporadic rule.

Remark: I am hoping that this axiom only activates very rarely.

Case 8: $y \diamond x$ is simplifying; $y \diamond (y \diamond x)$ is sporadic.

So now $x = (z,w)$ for some simplifying triple $(y,z,w)$ and there is a sporadic rule $y \diamond z = u$. So the axiom needed is

Axiom 11. If $(y,z,w)$ is a simplifying triple and $y \diamond z = u$ is a sporadic rule, then $S(z,w) \diamond u = y$ is a sporadic rule.

Remark: I am hoping this axiom is activated primarily when the simplifying triple arose from Axiom 4, in which case it asserts that the sporadic rule $Sy \diamond z = u$ creates the sporadic rule $SB(z,y) \diamond u = Sy$, which in turn creates the sporadic rule $SB(u,B(z,y)) \diamond Sy = SB(z,y)$, where $B(z,y) = (z,(z,y))$.

Case 9: $y \diamond x$ is sporadic; $y \diamond (y \diamond x)$ is sporadic.

So now we have two sporadic rules $y \diamond x = z$ and $y \diamond z = w$, and the axiom needed is

Axiom 12. If $y \diamond x = z$ and $y \diamond z = w$ are sporadic rules, then $Sx \diamond w = y$ is a sporadic rule.

Remark: I am hoping that this axiom activates only rarely.

One could imagine setting up an automated scheme in which one starts with a good "seed" of sporadic rules and simplifying triples, and then runs the above axioms to generate more, hoping that the process terminates without creating a contradiction (a violation of Axiom 1 or Axiom 2). I have some ideas for what the seed should be, but I am still working on it.

[Andy Jiang]

I wonder if after you have a list of rules (maybe machine-help-generated) and you write it into Lean as like an operation on the type freely generated by S, and the magma operation (the carrier you have) and write down the multiplication--is it possible that Lean itself can with enough time verify that 1516 is satisfied by repeated uses of cases and simp tactics or something? but I'm not very familiar with the capabilities of Lean so I don't know

[Terence Tao]

Yes, Lean would be able to do so, but it could be extremely tedious unless we find a way to automate it.

Here is a simplification of the approach in which we abandon the concept of a "simplifying triple" by absorbing it into the "sporadic rules", which are now a larger family of rules $x \diamond y = z$. The magma operation is now given by just two rules:

• (Sporadic case) If $x \diamond y = z$ is a sporadic rule, then we define $x \diamond y$ equal to $z$.
• (Generic case) In all other cases, we define $x \diamond y$ to equal $(x,y)$.

Naively, one could try to suspend all genericity hypotheses and work with the following slightly too-strong axioms:
Axiom 1 If $x \diamond y = z$ and $x \diamond y = z'$ are both sporadic rules, then $z=z'$.
Axiom 2 We have the sporadic rule $x \diamond x = Sx$.
Axiom 3 For every $x,y$, we have the sporadic rule $Sx \diamond (y, (y,x)) = x$.
Axiom 4 If we have the sporadic rule $y \diamond x = z$, then we have the sporadic rule $Sx \diamond (y,z) = y$.
Axiom 5 If we have the sporadic rule $y \diamond (y,x) = z$, then we have the sporadic rule $Sx \diamond z = y$.
Axiom 6 If we have the sporadic rules $y \diamond x = z$ and $y \diamond z = w$, then we have the sporadic rule $Sx \diamond w = y$.

Unfortunately, the commutativity of squaring and cubing shows that these axioms are inconsistent. More precisely:

1. From Axiom 1 and Axiom 4 we have $Sx \diamond (x,Sx) = x$.
2. From 1. and Axiom 4 we have $S(x,Sx) \diamond (Sx,x) = Sx$.
3. From Axiom 3 we have $Sx \diamond (Sx, (Sx,x)) = Sx$.
4. From 3. and Axiom 5 we have $S(Sx,x) \diamond Sx = Sx$.
5. From 4. (twice) and Axiom 6 we have $S^2 x \diamond Sx = S(Sx,x)$.
6. From 1., 5., and Axiom 6 we have $S(Sx, S^2 x) \diamond S(Sx,x) = S^2 x$.
7. From 5. and Axiom 4 we have $S^2 x \diamond (S^2 x, S(Sx,x)) = S^2 x$.
8. From 7. and Axiom 5 we have $S^2(Sx,x) \diamond S^2 x = S^2 x$.
9. From 8. (twice) and Axiom 6 we have $S^3 x \diamond S^2 x = S^2(Sx,x).$
10. On the other hand, from 5. we have $S^3 x \diamond S^2 x = S(S^2 x, Sx).$ This and 9. now violate Axiom 1, since $S^2(Sx,x) \neq S(S^2 x, Sx)$ in the free magma.

To fix this we have to implement the cubing operator $C$, and replace any occurrence of $(Sx,x)$ by $Cx$. This requires adding the additional sporadic axiom
Axiom 2' $Sx \diamond x = Cx$
and then also reinstating as much of the genericity hypotheses to the axioms as we can. So, at a given state of the ruleset, we replace Axioms 3-5 with
Axiom 3' For every $x,y$, if we do not currently have any rule for $y \diamond x$ or for $y \diamond (y,x)$, then we have the sporadic rule $Sx \diamond (y, (y,x)) = x$.
Axiom 4' If we have the sporadic rule $y \diamond x = z$, but we do not currently have any rule for $y \diamond z$, then we have the sporadic rule $Sx \diamond (y,z) = y$.
Axiom 5' If we have the sporadic rule $y \diamond (y,x) = z$, but we currently do not have any rule for $y \diamond x$, then we have the sporadic rule $Sx \diamond z = y$.

We can then try to dynamically grow the ruleset starting from just Axiom 2 and Axiom 2' by greedily trying to verify Axioms 3', 4', 5'; the previous contradiction is now blocked from occuring. I suspect that to block a collision later on, we will also need to impose
Axiom 2'' $(Sx, Cx) \diamond ((Sx,Cx),x) = Cx$.
(This law does not appear to be forced by 1516, but its square is, so we have to include it in this ansatz, as squaring is necessarily injective here. By the way this seems to indicate that squaring is not injective in the free magma, which means that this approach will not be able to capture that free magma precisely, but it may still get close enough to it that we can still refute 255.)

It may be possible to just run a greedy algorithm on this initial ruleset and see numerically if any collisions occur. This will not terminate currently, but it might give some hope that the strategy could work, and one can then try to add a few more seed axioms (motivated by, but not forced by, 1516) to force termination in finite time.

[Jose Brox]

Terence Tao ha dicho:

Pace Nielsen said:

Jose Brox Yeah, unless I see some simplifying principle, the Kisielwicz ansatz seems to be just reproducing some of (with less generality) Terry's computations.

Yeah, if you replace the free magma with the natural numbers, the pairing operation $(x,y)$ with say $2^x 3^y$, and the squaring and cubing operations with say $Sx = 5x$ and $Cx = 7x$ then I think one can convert the model I am proposing into a (very complicated) Kisielewicz type model.

The thing with Kisielewicz is that you can reduce freeness at the cost of introducing more functions when a new ambiguity appears; but for this you have to make educated guesses which may prove to be incompatible with the operation several steps in the future... It is kind of similar to be building a finite-state automaton and creating a new state instead of just creating new transitions between existing states.

[Pace Nielsen]

Today I need to teach classes and write a letter of recommendation, but I do have some ideas about how to implement an automation to find/check if the list of sporadic rules is complete. I'll try to get to that as soon as possible, probably tomorrow though.

[Andy Jiang]

Do we have any toy examples of a system of rules like this for another equation we can try to implement in the meantime? Like maybe free 854 magma? Just to test any general frameworks we might be able to build

[Terence Tao]

I looked at the Kiseleiwicz constructions, but those are mostly modifications of the constant law $x \diamond y = 1$ rather than modifications of a free law $x \diamond y = (x,y)$, and also they have so many operations that the number of axioms needed is rather large. I guess one could use this procedure to discover a large number of rules of the form $x \diamond y = x$, which would slowly fill out the infinite family of relations in https://teorth.github.io/equational_theories/blueprint/854-chapter.html#free-relate .

[Terence Tao]

I guess one could try building this type of model with 1323, $x = y \diamond ( ((y \diamond y) \diamond x) \diamond y)$. Here, we work on a free magma generated by one generator $\emptyset$ and a pairing operation $(,)$ (i.e., trees), and the magma operation $x \diamond y$ is equal to $(x,y)$ unless there is a sporadic rule $x \diamond y = z$. To simplify things we also assume that there are no sporadic rules for $x \diamond x$, so $x\diamond x = (x,x)$. If one can impose the axioms

Axiom 1 If there are sporadic rules $x \diamond y = z$ and $x \diamond y = z'$, then $z=z'$.
Axiom 2 There is no sporadic rule of the form $x \diamond x = z$.
Axiom 3 One has the sporadic rule $y \diamond (((y,y),x),y) = x$.
Axiom 4 If one has the sporadic rule $(y,y) \diamond x = z$, then one has the sporadic rule $y \diamond (z,y) = x$.
Axiom 5 If one has the sporadic rule $((y,y),x) \diamond y = z$, then one has the sporadic rule $y \diamond z = x$.
Axiom 6 If one has the sporadic rules $(y,y) \diamond x = z$ and $z \diamond y = w$, then one has the sporadic rule $y \diamond w = x$.

Such a system will automatically obey 1323, and if so has a good chance of not obeying 2744. So one could hope to just generate rules using Axioms 3,4,5,6. If one is super optimistic then this process terminates with a finite number of sporadic rules (in terms of arbitrary trees $x,y$) that still do not violate Axioms 1,2, in that any new sporadic rule generated is a special case of an existing rule. But there may be self-sustaining chains of rules, for instance one may discover that every sporadic rule of the form $x \diamond y = z$ creates another rule of the form $x' \diamond y' = z'$ where $(x',y',z') = T(x,y,z)$ for some transformation $T$. If this is the case, this creates an infinite sequence of families of rules, but one can truncate it by declaring for instance that $x'' \diamond y'' = z''$ is a rule whenever $(x'',y'',z'' ) = T^2(x,y,z)$ for some $x,y,z$, even if no rule of the form $x \diamond y = z$ exists. This makes the ruleset slightly too large to be the free magma, but could help make the task of finding a complete ruleset terminate in finite time.

So maybe this is a good model problem to work on first before tackling 1516, which seems to generate many more rules and has the additional complication of squaring and cubing having to commute.

[Terence Tao]

OK, this one may be harder to truncate than I thought. Axiom 4 iterates itself if we keep squaring $y$. For instance two applications of Axiom 4 tell us that if we have the sporadic rule $((y,y),(y,y)) \diamond x = z$, then we have the sporadic rule $y \diamond (x, (y,y)) = (z,y)$. I had thought to truncate this iteration by just adding all rules of the form $y \diamond (x, (y,y)) = (z,y)$ as sporadic rules for any $x,y,z$, but this violates Axiom 1 because the right-hand side involves $z$ and the left-hand side doesn't. So perhaps one just has to add the infinite family of all rules generated by Axiom 4 (starting from Axiom 3) and hope that this doesn't trigger any invocations of Axiom 5 and Axiom 6, then we get to close the system. One thing that gives me hope is that in the sporadic rules $x \diamond y = z$ generated by Axiom 4, $y$ is longer than $x$; but for at least one of the sporadic rules $x \diamond y = z$ needed for Axiom 5 or Axiom 6, $x$ is longer than $y$. So maybe all the extra rules generated by Axiom 4 don't cause uncontrollable combinatorial explosion (and/or violation of Axiom 1 or Axiom 2).

[Terence Tao]

Actually, I think this just works for 1323. Setting $L_y x := (y,x)$, $R_y := (x,y)$, and $S y := (y,y)$, then Axiom 3 says $y \diamond R_y L_{Sy} x=x$ and Axiom 4 says that $Sy \diamond x = z \implies y \diamond R_y z = x$, which iterates to give an alternating infinite family of sporadic rules
$y \diamond R_y L_{Sy} x = x$
$y \diamond R_y x = R_{Sy} L_{S^2 y} x$
$y \diamond R_y R_{S^2 y} L_{S^3 y} x = R_{Sy} x$
$y \diamond R_y R_{S^2 y} x = R_{Sy} R_{S^3 y} L_{S^4 y} x$
$y \diamond R_y R_{S^2 y} R_{S^4 y} L_{S^5 y} x = R_{Sy} R_{S^3 y} x$
etc. and I think this ruleset obeys Axioms 1, 2, 5, 6 (hence 1323) and not 2744?

Wait, Axiom 6 might not be obeyed. Checking...

[Terence Tao]

OK, Axiom 5 is fine (because in the hypothesis $R_x Sy \diamond y = z$, $R_x Sy$ is longer than $y$, which is not the case for any of the axioms in the above list), and Axiom 6 is fine unless the rule $Sy \diamond x = z$ is of the $y \diamond R_y L_{Sy} x = x$ form (i.e., $x = R_{Sy} L_{S^2 y} z$), in which case Axiom 6 now reads

Axiom 6'. If $z \diamond y = w$ is a sporadic rule, then $y \diamond w = R_{Sy} L_{S^2 y} z$ is a sporadic rule.

So this unfortunately generates further infinite families of rules (now generated a free semigroup on two generators, Axiom 4 and Axiom 6') but it still might be possible to get enough control on the rules generated that no further triggering of Axiom 6 or Axiom 5 occurs, or any violation of Axiom 1 or Axiom 2, in which case we are still in business.

[Terence Tao]

OK, I think the process can terminate, though it's not super clean. Setting $T_y := R_{Sy} L_{S^2 y}$ for brevity, then Axiom 6' says that $z \diamond y = w$ implies $y \diamond w = T_y z$, which iterates to $w \diamond T_y z = T_w T_y y$. To stop proliferation, I will simply add all rules of this type as a new axiom:

Axiom 7. $w \diamond T_y z = T_w T_y y.$

Note that this does not violate Axiom 1 since $w$ and $T_y z$ determine $w,y$ and hence $T_w T_y y$. (In contrast, one could not truncate earlier at $y \diamond w = T_y z$.)

The complete rule set is then, I conjecture, all the rules coming by starting with either Axiom 3 or Axiom 7, applying 0 or more applications of Axiom 4, and then applying 0 or 1 applications of Axiom 6'. The point is that after applying 1 application of Axiom 6', the term to the left of $\diamond$ should no longer be a square, and so Axiom 4 can't trigger, and after 2 applications of Axiom 6', one is back in Axiom 7. One also has to check that Axiom 5 can't trigger, nor can any other case of Axiom 6 other than the one leading to 6', but I think this is just a finite case check (hopefully).

[Bernhard Reinke]

I am not sure I understand Axiom 7, what relations should hold between $y, z, w$ such that the conclusion holds? $z$ doesn't appear on the RHS, so I guess there are some assumptions.

[Terence Tao]

No, there are no assumptions on $y, z, w$; it is a relatively sweeping law. It is not forced by 1323, but I am hoping that we can insert it in order to close the iteration and obtain a superset of all the laws forced by 1323 that are stil self-consistent and still refute 2744. Am writing notes on this for the blueprint right now.

[Bernhard Reinke]

Hm, I think it we add to 1323 the law that corresponds to axiom 7 (in the sense of using the magma operation $\diamond$ in $T_y$ instead of the tree building operation, this already implies 2744

[Terence Tao]

Oof that is a blow to the strategy. Um what if instead we add the third iterate instead, $T_y z \diamond T_w T_y z = T_{T_y z} w$?

[Terence Tao]

This makes the propagation tree slightly more complicated, because if one starts from Axiom 3 and applies Axiom 6' twice, then one can then apply Axiom 4 indefinitely, but I have some hope that that is the only other infinite family produced and so the argument may still close.

[Bernhard Reinke]

Terence Tao said:

Oof that is a blow to the strategy. Um what if instead we add the third iterate instead, $T_y z \diamond T_w T_y z = T_{T_y z} w$?

Same issue unfortunately

[Terence Tao]

That surprises me a little to be honest. That complex rule implies 2744 in all cases? Is this an ATP check?

[Terence Tao]

oh by the way I think I misspelled the law. checking... no, it's correct

[Bernhard Reinke]

yes, this is the tptp snippet, vampire shows 2744 immediately

fof(eq1323,axiom,
X = m(Y,m(m(m(Y,Y),X),Y))
).

fof(def_T, axiom,
t(Y,X) = m(m(m(m(Y,Y),m(Y,Y)),X),m(Y,Y))
).

fof(axiom_7, axiom,
m(t(Y,Z),t(W,t(Y,Z)))=t(t(Y,Z),W)
).

fof(eq2744,conjecture,
X = m(m(m(Y,Y),m(Y,X)),Y)
).

[Bernhard Reinke]

I hope this corresponds to what you had in mind (this is version for the iterated law)

[Terence Tao]

It looks all right but just as a sanity check - if you restrict Axiom 7 to only those Y,Z,W for which m(Z,Y)=W, is it a consequence of 1323?

[Terence Tao]

Anyway this makes me realize that it is far better to use ATPs to test whether various relaxations of laws are possible in order to truncate the iteration, than to simply propose them and then do a very tedious human verification

[Terence Tao]

One could also try the next iteration out, $T_w T_y z \diamond T_{T_y z} w = T_{T_w T_y z} T_y z$. If that still implies 2744 then there's something fundamental that this approach is missing. Perhaps it is that we are not forcing $L_y$ to be non-injective for some $y$.

[Bernhard Reinke]

Terence Tao said:

It looks all right but just as a sanity check - if you restrict Axiom 7 to only those Y,Z,W for which m(Z,Y)=W, is it a consequence of 1323?

It doesn't seem to be a consequence, at least vampire runs quickly out of memory

[Terence Tao]

OK, then there is a typo somewhere. Can you verify that 1323 implies Axiom 6', namely that $m(Z,Y)=W$ implies $m(Y,W) = t(Y,Z)$?

[Bernhard Reinke]

yes, that is ok

[Terence Tao]

ok... does $m(Z,Y)=W$ imply $m(W, t(Y,Z)) = t(W,t(Y,Z))$?

[Terence Tao]

Ah I see my mistake

[Terence Tao]

$m(Z,Y) = W$ should imply $m(W,t(Y,Z)) = t(W,Y)$ instead

[Terence Tao]

if it does, I propose $m(W,t(Y,Z)) = t(W,Y)$ as the new Axiom 7 (with no prior restriction that $m(Z,Y)=W$) and see if this does not imply 2744

[Bernhard Reinke]

it is now a consequence of 1323 with the assumption $m(Z,Y) = W$, but the new Axiom 7 still implies 2744.

[Terence Tao]

OK... um can you try the same exercise with $m(W,t(Y,Z)) = t(W,Y)$ replaced by $m(t(Y,Z), t(W,Y)) = t(t(Y,Z),W)$?

[Terence Tao]

i.e. it should be a consequence of 1323 with $m(Z,Y)=W$, and (fingers crossed) does not imply 2744.

[Terence Tao]

My intuition here is that once all three components of a law $m(A,B)=C$ become complex, then the law becomes dramatically less influential for proving other laws

[Bernhard Reinke]

Same as before, it is a consequence of 1323 with $m(Z,Y) = W$, but without it implies 2744

[Bernhard Reinke]

fof(eq1323,axiom,
X = m(Y,m(m(m(Y,Y),X),Y))
).

fof(def_T, axiom,
t(Y,X) = m(m(m(m(Y,Y),m(Y,Y)),X),m(Y,Y))
).

fof(axiom_7_second_iterate, axiom,
m(t(Y,Z),t(W,Y)) = t(t(Y,Z),W)
).

fof(eq2744,conjecture,
X = m(m(m(Y,Y),m(Y,X)),Y)
).

this is the tptp snippet for the last claim. I have to run now, but maybe other people can help with ATP questions if you have them

[Michael Bucko]

Terence Tao schrieb:

My intuition here is that once all three components of a law $m(A,B)=C$ become complex, then the law becomes dramatically less influential for proving other laws

Interesting idea! Much less influential in terms of predictive power, or reusability for proofs? If reusability, is it reusability for humans, or any computer?

[Michael Bucko]

Terence Tao schrieb:

Anyway this makes me realize that it is far better to use ATPs to test whether various relaxations of laws are possible in order to truncate the iteration, than to simply propose them and then do a very tedious human verification

That could enable more gradual, smaller, and very well defined ATP tests. Such smaller tests could also be (to some extent) (co-)coordinated by LLMs. I'll open a GitHub issue - I could make a script for this. One would only have to add their LLM API key and the path to Vampire.

EDIT: https://github.com/teorth/equational_theories/issues/803

[Terence Tao]

@Bernhard Reinke Thanks so much! I have to attend to other things now, but will come back to this, probably on the 1323 thread rather than the 1516 thread. Anyway this seems to be a simpler model for this type of approach than 1516, so thank you @Andy Jiang for the suggestion!

[Pace Nielsen]

@Terence Tao I started the work of automating the search for new rules for 1516. Below I'll ignore the sporadic rules of the form $Sy\diamond (x,(x,y))=x$

It immediately found the primary relation $SC=CS$, which we already knew. After incorporating that identity into the search, it then found the next (again well-known) identity $QS=S$, where $Qx:=Cx\diamond x=x^4$. (This is your sporadic rule 7 in the list you posted on Nov. 5 at 12:48 PM). The next few identities are of the same form---things like $SQS=S^2$ or slightly more complicated things like $SQSx\diamond CSx=S^2x\diamond SCx$. I'm still thinking about the best way to incorporate these types of relations into the framework before pushing further. (The trouble is that we want to treat $SQx\diamond Cx$ as different than $Sx\diamond Cx$, even though they become the same after replacing $x$ with a square.) I'll update everyone when I get further.

[Terence Tao]

Can you run the same exercise for 1323 along the lines of what I indicated above? It might be somewhat simpler. I'll make a comment over at the 1323 thread about this.

[Pace Nielsen]

I may be able to run the same exercise for 1323, once I've figured out 1516 fully. I did figure out a nice way to handle the identity $QS=S$, and am now double-checking things, and then will run a final search over generic pairs.

[Pace Nielsen]

Here is the full report from the automated search on law 1516.

My paradigm for running the search was that instead of thinking of $x\diamond y$ as (when possible) the expression $x\ast y$ in the free magma, and instead of writing it as $(x,y)$, I instead treated it as a new "function" following the Kisielewicz ansatz. [This is really just a renaming procedure, but it was helpful for my own understanding.]

So, for example, $x\diamond x=Sx$ is a new function, and $Sx\diamond x=Cx$ is a new function, and $Cx\diamond x=Qx$ is a new function, and so forth. After this point I just started calling the new functions $p_1,p_2,\ldots$. Some of the other important functions that showed up are $p_1x:=x\diamond Sx$, $p_2x=Sx\diamond Cx$, $p_3x=Cx\diamond Qx$, and finally $p_{15}x=S^2x\diamond(S^2x\diamond x)$.

Now, the 1516 law is $x=(y\diamond y)\diamond (x\diamond (x\diamond y))$. I thought about it in the following way. Once we know that $x\diamond y=p(x,y)$ is defined (either as a new function or a composition of previously defined functions), then we generally want to define $x\diamond p(x,y)$ as a brand-new function $p'(x,y)$, and then we must take $Sy\diamond p'(x,y)=x$, which is not a new function. So each defined product generally gives rise to two new defined products, both involving the new function in some way.

Let me show how this worked in practice. Suppose we have derived the equality $x\diamond Sx=p_1x$. From this, we want to take $x\diamond p_1x=p_4x$ (a brand-new function), and then we must also take $Sx\diamond p_2x=x$.

There were two dangers in this. First, when $x\diamond y$ is defined, it might also be the case that $x\diamond (x\diamond y)$ is also already (previously) defined, so we cannot adjoin a new function (i.e. we have to use the previously defined answer). This happened exactly five times (involving those five special functions above). For example, we had the equality $Sx\diamond p_1x=x$. We can't define then $Sx\diamond x$ as a new function, because we already had it equals $Cx$.

The second danger was that when defining $Sy\diamond (x\diamond (x\diamond y))$ as $x$, it might also already have a different definition; so there could be collisions, where the expressions don't match.

The first collision it found was $CS=SC$. To accommodate this issue, I had to modify the composition of functions to always concentrate sequential powers of $S$ and $C$ together. The next collision it found was that $QS=S$. This causes problems with some new functions like $p_3$, because then $p_3S=CS\diamond QS=CS\diamond S=QS=S$. After adding the rules for these new types of collisions (essentially adding a new, third infinite family of reduction rules) there were no other collisions that the program found.

There is one other issue I want to think about, but this appears to capture the full reduction system.

[Pace Nielsen]

Actually, there might be more to the reduction system---I'll try to finish it off tomorrow.

[Terence Tao]

This looks provisionally promising, and perhaps simpler than what I was proposing. Look forward to seeing the final analysis!

[Terence Tao]

Are the problems involving $C$ and $Q$ significant enough that it is worth adding additional rules such as requiring $C$ to be constant, or do you think this does not make the anaysis substantially simpler?

[Pace Nielsen]

The previous runs of the automated searcher checked for closure under the obvious adjoining process: starting from $x\diamond y=z$, adjoin the new products $x\diamond z$ and $Sy\diamond (x\diamond z)$ in the greediest manner possible. Beginning with just the seed $x\diamond x$, it closed up.

So, next I extended the search to guarantee that if $Sx\diamond y=z$ was going to be handled, I had already handled the simpler product $y\diamond x$. The automated process then found a third collision, which was number 9 on Terry's list:

$$S((Sx\diamond Cx)\diamond ((Sx\diamond Cx)\diamond x)) = SCx.$$

So, this rule is not automatic assuming $CS=SC$ and $QS=S$ under greedy extension. I'll start thinking about how to implement this new relation, as well as whether taking $C$ constant would help.

[Terence Tao]

My thought was to impose $(Sx \diamond Cx) \diamond ((Sx \diamond Cx) \diamond x) = Cx$ as a new axiom.

[Pace Nielsen]

Let me see if Vampire says that allows 255 to fail. It would certainly be VERY easy to implement in the searcher.

[Pace Nielsen]

Of course Vampire says it is fine, because we already knew that it says left-cancellation is fine.

[Terence Tao]

I'm thinking to explore more the possibility, floated by @Bruno Le Floch over at the 1323 thread, to adapt the recent success over 1323 here, by trying to work out what's going on on the square numbers first and by imposing ATP-approved simplifying axioms, particularly on the square numbers, to make the algebraic constraints easy to solve. As Bruno pointed out, there is a new difficulty here because the target law 255 also involves square numbers, but nevertheless I think we should probe the strategy.

Perhaps we can start by imposing our previous axiom of constant cubes on our hypothetical counterexample $M$; I will write this axiom here as $C=0$ (instead of $C=2$). I'd also like to assume that the set $SM$ of squares is closed under the magma operation, hopefully an ATP can confirm that this is a likely safe assumption in that it doesn't accidentally imply 255? Then we have a submagma $SM$ of $M$ that obeys a lot of laws, including 255, $C=0$, and perhaps some others. Are there more simplifying axioms we can put on either $SM$ or $M$ that don't accidentally prove 255 for $M$? (For instance, perhaps we could make $0$ a unit for $SM$, since it is already a left-unit by 255. Another possible simplifying assumption is to have $S^n = 0$ for some small $n$ which was also a situation we enjoyed in 1323 where we could impose $S^2=0$.) This may suggest a good choice for what multiplication table to put on $SM$. Based on the 1323 experience I suspect an infinite carrier for $SM$ may be prudent.

Is it consistent to make $L_{Sy}$ invertible? Then the 1516 law becomes $x \diamond (x \diamond y) = L_{Sy}^{-1} x$, which would be similar to the simplified form we had for 1323. It hints that we don't need to think about what the multiplication table $x \diamond y$ should be when $x$ is not a square, we should be able to fill it out greedily with an infinite carrier. (In fact, we might even be able to fill it out just assuming $L_{Sy}$ surjective.) We just have to work out the portion when $x$ is a square and $y$ is not a square, in such a way that we don't accidentally make $0 \diamond y = y$ for all non-squares $y$. What constraints on this multiplication table do we have?

[Andy Jiang]

At some point I think i checked that vampire says squares being closed under the operation implies 255 (at least assuming C=0 and left cancellation) let me check again without those assumptions and report back (also to make sure I'm not misremembering)

[Matthew Bolan]

Without left cancellation I think my vampire is telling me that is fine.

[Matthew Bolan]

My vampire is fine with most of Terry's assumptions, but when I add $L_{Sy}$ being invertible it tends to find a proof of 255 (not sure what subset is doing it here), and when I try and add $S^n=0$ for small n it also tends to find a proof of 255

[Terence Tao]

How about if $S^n$ is two-valued? (One may then also need $C$ to be two-valued).

[Terence Tao]

Or if $L_{Sy}$ is injective just on the squares (i.e. $SM$ is left-cancellative even if $M$ isn't)

[Matthew Bolan]

The latter seems fine. Not yet checked the former. Here's my TPTP

fof(def_S, axiom,
s(X)=m(X,X)
).

fof(def_C, axiom,
c(X)=m(s(X),X)
).

fof(eq1516,axiom,
X = m(s(Y),m(X,m(X,Y)))
).

fof(cconst, axiom,
c(X) = c(Y)
).

fof(smclosed, axiom,
?[Z] : m(s(X),s(Y)) = s(Z)
).

fof(leftcancelonsq, axiom,
(Z=Y) | (m(s(X),s(Z)) != m(s(X),s(Y)))
).

fof(eq255, conjecture,
X = m(c(X),X)
).

[Matthew Bolan]

Adding $S^n$ being two valued to the above TPTP (so in particular still assuming SM is left-cancellative), vampire can prove 255 for $n \le 6$. The amount of time it takes gets longer as I increase $n$.

[Terence Tao]

Hmm, interesting. Ok, getting a bit desperate here... what if we require that $S^n$ is three-valued for some small $n$ and no other assumptions?

(I'm really hoping we can make the image of $S^n$ somewhat small, as this suggests a way to build a magma by first working the multiplication table on the image of $S^n$, then the image of $S^{n-1}$, and so forth back to the full magma.)

[Matthew Bolan]

So just 1516 and S^n being three valued ?

[Terence Tao]

yeah. It could be that this problem is in fact immune not just to finite magmas, but to any magma that eventually squares to a finite set, and maybe this three-element experiment will support that.

[Matthew Bolan]

With no other assumptions it's not finding a proof of 255, even with $S^2$ being 2-valued.

[Terence Tao]

Oh okay! Now we're getting somewhere. OK... what about $S^2$ 2-valued, and squares closed under multiplication? If that works, then we should start studying magmas with 2-valued squares as possible candidates for $SM$ that we can later extend to $M$.

[Matthew Bolan]

No proof of 255 from that in a minute long run.

[Terence Tao]

I guess what I am concluding from this is that left cancellability is perhaps not a good thing to want to impose. 1516 is the assertion that $L_{Sx} (y \diamond (y \diamond x)) = y$. This will be less constraining on $y \diamond (y \diamond x)$ if we allow $L_{Sx}$ to be multi-valued.

I think I'm done with ATP requests for now, thanks so much for your help!

[Matthew Bolan]

Actually, I have one more ATP observation, which is that if I ask for $S$ itself to be 2-valued it doesn't seem to be finding a proof.

[Terence Tao]

Wow, I thought we had ruled that out already

[Matthew Bolan]

Yeah, makes me suspicious, but perhaps that was under some standing assumption.

[Matthew Bolan]

I'll post the TPTP once this latest run finishes

[Terence Tao]

Yeah you had previously ruled that out at https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/1516.20-.3E.20255/near/480260405

[Matthew Bolan]

Hmm, bug hunting time then.

[Terence Tao]

Things would be quite simple if we could have $SM = \{-1,+1\}$. There are now just three rules:

0. $y \diamond y = Sy \in \{-1,+1\}$.
1. If $y \diamond x = z$ and $Sx = +1$, then $y \diamond z \in L_{+1}^{-1} y$.
2. If $y \diamond x = z$ and $Sx = -1$, then $y \diamond z \in L_{-1}^{-1} y$.

This looks relatively easy to fill out greedily if we choose $L_{+1}$ and $L_{-1}$ reasonably well (not too injective - having infinite preimages, in particular, would give us a lot of useful flexibility). If there is a chance that we can get a 255 counterexample this way then we should pursue it.

[Terence Tao]

If anyone else has the ability to do an independent ATP run of the same question "does $Sy \in \{-1,+1\}$ plus 1516 imply 255?" that would be great.

[Pace Nielsen]

When I ran the following check for a 2-valued S in Vampire, it implied 255 (by a fairly long proof).

fof(eq1516, axiom, X = mul(mul(Y, Y), mul(X, mul(X, Y)))).
fof(sdef, axiom, s(X) = mul(X, X)).
fof(twosquares, axiom, s(X) != e => s(X) = f).
fof(255, conjecture, X = mul(mul(mul(X, X), X), X)).

[Matthew Bolan]

Huh, I didn't find a proof with mine running that file, perhaps I just am not running these long enough.

[Matthew Bolan]

Wow, looks like my minute cutoff was just barely too short on my machine. I now can replicate.

[Matthew Bolan]

I guess we should run these for quite a while before we commit a lot of effort to some ansatz :sweat_smile:

[Terence Tao]

I'm going to try to figure out a pen and paper proof

[Matthew Bolan]

Prover 9's proof that all such things are trivial seems possible to understand:
proof.txt

[Terence Tao]

Hmm. I think it's related to the fact that there are no order 2 magmas solving 1516. The smallest we have is of order 5. Probably ATPs are not going to give us guidance as to whether 5-valued squares are possible, but one could imagine postulating that SM is one of the order 5 models (or the order 7 model) and going from there.

[Matthew Bolan]

Matthew Bolan said:

Actually, I have one more ATP observation, which is that if I ask for $S$ itself to be 2-valued it doesn't seem to be finding a proof.

rerunning the TPTP from here for longer and it finds a counterexample after a few minutes, so it looks like I never had a bug, I just didn't run it for long enough. Replacing 255 with just the singleton law X=Y it finds a proof in just 7 seconds.

[Matthew Bolan]

Sorry about all that :sweat_smile:

[Terence Tao]

Well, it's good for the project to get practical tips on how to use ATPs accurately!

[Matthew Bolan]

Definitely one thing I've just learned is to also check if vampire can prove the singleton law from your axioms.

[Matthew Bolan]

I'm pretty shocked the difference was so severe (especially compared with how fast prover9 solves both versions).

[Terence Tao]

I think I now understand what is going on from a theory point of view. Specifically,

Theorem. Let $M$ be a 1516 magma. If $SM$ is finite (i.e., only finitely many squares), then squaring is surjective $SM = M$. In particular, $M$ is finite and obeys 255.

Proof. Let $b = Sx$ be a square, then we know $L_b$ is surjective from the 1516 equation $L_b L_y^2 x = y$. Hence, for any $y \in M$, we can write $y = L_b^2 z$ for some $z$, then from 1516 we have $R_y Sz = L_{Sz} y = b$. Hence $R_y(SM) \supset SM$, hence $R_y$ maps $SM$ bijectively to $SM$ by finiteness. Thus for any $a \in SM$, we have $L_a y = R_y a \in SM$, i.e., $L_a$ takes values in the squares; but $L_a$ is surjective, hence $SM = M$. $\Box$

So now I am going to try taking $SM$ to be an infinite model (e.g. the product of infinitely many copies of the order 5 model) and see if I can then greedily construct a 255 counterexample from that ansatz.

[Matthew Bolan]

Vampire has just informed me after a nearly 8 minute run that $S^2$ being two valued implies 255 (and a second run reveals it implies the singleton law), so we can throw away that earlier claim too.

TPTP for that (stealing from Pace)

fof(eq1516, axiom, X = mul(mul(Y, Y), mul(X, mul(X, Y)))).
fof(sdef, axiom, s(X) = mul(X, X)).
fof(twosquares, axiom, s(s(X)) != e => s(s(X)) = f).
fof(255, conjecture, X = mul(mul(mul(X, X), X), X)).

[Terence Tao]

Yeah, I'm pretty much migrating to models with infinitely many squares (or iterated squares) now.

[Matthew Bolan]

Matthew Bolan said:

The latter seems fine. Not yet checked the former. Here's my TPTP

fof(def_S, axiom,
s(X)=m(X,X)
).

fof(def_C, axiom,
c(X)=m(s(X),X)
).

fof(eq1516,axiom,
X = m(s(Y),m(X,m(X,Y)))
).

fof(cconst, axiom,
c(X) = c(Y)
).

fof(smclosed, axiom,
?[Z] : m(s(X),s(Y)) = s(Z)
).

fof(leftcancelonsq, axiom,
(Z=Y) | (m(s(X),s(Z)) != m(s(X),s(Y)))
).

fof(eq255, conjecture,
X = m(c(X),X)
).

A 10 minute run from vampire did not prove 255 starting from this. Prover9 also seems to be unable to prove 255 from it, and Mace4 finds that the order 7 model meets the axioms (but of course does not refute 255).

[Terence Tao]

I ended up not being able to build a non-trivial model in which $SM$ was say the infinite product of the order 5 magma due to a modification of the argument when $SM$ was finite. Part of the problem was that this infinite product was right cancellative. Do we know if any 1516 model which is not right cancellative?

[Terence Tao]

Oh wait, we have a translation invariant model! This could be promising.

[Terence Tao]

OK, I think I have a plan to create a 1516 magma $M$ that contradicts 255; it's a fairly tricky construction, will try to write a more detailed blueprint soon. It will contain a submagma $SM$, the set of squares, on which simplicity I will take $S$ to be the identity (so I am assuming $S^2=S$ in the overall magma). I will use $a,b,c$ to refer to elements of $SM$ (squares), and $x,y,z$ for elements of $M \backslash SM$ (non-squares). Both sets will be infinite, but the latter is somewhat "larger" than the former in some sense. The multiplication table is built in three steps: first on $SM$ (square times square), then between $SM$ and $M \backslash SM$ (square times non-square), and finally between $M \backslash SM$ and $M$ (non-square times arbitrary).

Step 1: Construct a 1516 magma $SM$ with which $Sa = a$ for all $a \in SM$, and with the additional property that for all $a,b \in SM$ there are at least two $c,c' \in SM$ such that $R_a c = R_a c' = b$ (thus the right multiplication operations are doubly surjective).

Construction (sketch): I think one can do this with the integers as carrier and a translation-invariant model $a \diamond b = a + f(b-a)$ with $f(0)=0$ to get the $Sa=a$ law, by modifying the existing greedy construction. I'll detail this in the blueprint version. $\Box$

With this step, the left multiplication operators $L_a, a \in SM$ are defined as functions from $SM$ to $SM$. By construction, we have $L_{Sa} L_b L_b a = b$ for all $a,b \in SM$. Also, as all elements of $SM$ are squares, the $L_a: SM \to SM$ are surjective for all $a \in SM$.

Step 2: Construct a set $M \backslash SM$ of non-squares (disjoint from $SM$), a squaring map $S: M \backslash SM \to SM$, and extensions $L_a: M \to M$ of the left multiplication operators $L_a: SM \to SM$ for each $a \in SM$, such that $L_{Sy} L_b L_b y = b$ for all $b \in SM$ and $y \in M \backslash SM$. Furthermore: for each $a \in SM$ and $x \in M \backslash SM$, the set $\{ y \in M \backslash SM: L_a y = x \}$ is infinite. (Thus, all the $L_a$ are "infinitely surjective" on the non-squares.)

Construction: The non-squares will be tuples of the form $y = (a,c,n)$ where $a,c \in SM$ and $n$ is a natural number. The squaring map will be $S(a,c,n) = a$. For each $y = (a,c,n)$ and each $b \in SM$, we can use step 1 to find $c_{y,b} \in SM$ distinct from $c$ such that $R_a c_{y,b} = b$; clearly the $c_{y,b}$ are distinct as $b$ varies. We now have $L_a L_{c_{y,b}} b = L_{Sa} L_{c_{y,b}} L_{c_{y,b}} a = c_{y,b}$. So if we define $L_{c_{y,b}} y := b$, then we have $L_{Sy} L_{c'} L_{c'} y = c'$ whenever $c'$ is of the form $c' = c_{y,b}$ for some $b \in SM$. But we still have $L_{c'} y$ undefined if $c'$ is not of this form, in particular, $L_c y$ is currently not defined.

Now we greedily fill in the rest of the $L_{c'}$ functions. If $y = (a,c,n)$ is some element of $M \backslash SM$ (so that $Sy=a$) and $L_{c'} y$ is not yet defined, we can use the surjectivity of the $L_a: SM \to SM$ to write $c' = L_a b$ for some $b \in SM$, then set $L_{c'} y = b$; then we have $L_{Sy} L_{c'} L_{c'} y = c'$ as required. Also, if we want to write $y$ as $L_{c'} z$ for some $z$ where $L_{c'}$ is not defined, we can perform the previous construction if necessary to have $L_{c'} y = b$ for some $b \in SM$, then find $a'$ such that $R_b a' = c'$, and set $z = (a', c', n')$ where $n'$ is large enough that $L_{c'} z$ has not yet been assigned. Then set $L_{c'} z = y$, then $L_{Sz} L_{c'} L_{c'} z = c'$, and we have created a preimage in $\{ z \in M \backslash SM: L_{c'} z = y\}$. Iterating these procedures in a suitable order, we can obtain the claim. $\Box$

Step 3: Construct $L_x$ for non-squares $x \in M \backslash SM$, such that $L_x x = Sx$ and $L_{Sy} L_x L_x y = x$ for all $y \in M$, but such that the 255 identity $L_{L_{Sx} x} x = x$ fails at least once.

Construction (Sketch): The main constraint here is $L_{Sy} L_x L_x y = x$, or equivalently that if $$L_x y $ equals $z$, then $L_x z$ must lie in the preimage $L_{Sy}^{-1} x$. Because these preimages are infinite, we can starting with the requirement $L_x x = Sx$, we can then greedily fill out $L_x$ (ensuring that $L_x y \neq y$ for all $y$ to avoid collisions), and there is more than enough freedom to ensure that
$L_{L_{Sx} x} x = x$ fails at least once. $\Box$

[Jose Brox]

In my experience, 1 minute is sometimes not enough. I now run Prover9 for 20 minutes when the implication is relevant, just to be sure (I have been surprised once!).

[Jose Brox]

Terence Tao ha dicho:

Well, it's good for the project to get practical tips on how to use ATPs accurately!

From the collective experience here, one thing I think that we can say is that using both Prover9 and Vampire is proving useful: while Prover9 may be sometimes faster for equational proving (and perhaps finds simpler proofs), for more complicated first-order formulas Vampire can have a big advantage. In the 1323 case, Prover9 couldn't rule out the possibility of having only two squares after 30 minutes (at least in my machine and with high resources), while Vampire did it in 30s (in other computers). Apparently this was related to Vampire resorting to a SAT solver.

[Jose Brox]

Terence Tao ha dicho:

OK, I think I have a plan to create a 1516 magma M that contradicts 255

Is there anything in this strategy that prevents using it for showing that 1729 doesn't imply 817? We'd just need to swap from
$L_{Sy}L_xL_x y$ to $L_{Sy}R_yR_x y$.

[Terence Tao]

I've added a note in the plan of the paper to discuss the topic on the practical use of ATPs including the point you made above about taking advantage of the complementary strengths of different ATPs. It occurs to me that actually we have constructed a pretty good data set for benchmarking ATP performance.

I am focusing in writing up the 1516 strategy for the blueprint. Given that the strategy was derived from a similar successful strategy for 1323 that already handled 1729 -> 917, I wouldn't be surprised if there was some way to tweak it to handle the last remaining implication. But we should coordinate with @Shreyas Srinivas on this. (That is nominally the last implication outstanding, but actually there is a cluster of implications from 713, 1289, 1447 that we might want to visit because the only proofs we have right now are large greedy algorithms that involve a SAT-solver calculation that we have not figured out how to replicate within Lean in a civilized fashion.)

[Terence Tao]

I wrote up the previous arguments in the blueprint. I've also opened up equational#820 to formalize it. However it may be worth trying to see if some simplifications are possible: right now the argument involves no less than three separate greedy algorithms, first to construct the squares x squares portion of the multiplication table, then squares x nonsquares, then finally nonsquares x everything. The previous ATP-powered discussions seemed to indicate however that some complexity of this sort may be inevitable, but perhaps there are some other simplifications.

[Andy Jiang]

Could I ask how you came up with the form that the non-squares should take? Like ZxZxN? Is there a particular constraint which this form helps on? Just want to understand your solving process thanks!

[Terence Tao]

Sure! My starting point was to view the equation 1516 as a constraint $L_{Sy} L_x^2 y = x$ between the various left shift maps $L_x$, and to first see what conditions they impose on the left shift maps $L_a: M \to M$ for $a$ in the squares $SM$. Here I assume that the magma operation on $SM$ has already been defined, so the question is what $L_a$ does on the non-squares, which at present are a completely unknown set. In order to fill out the multiplication table on the non-squares later, also know that I will need these $L_a$ to be surjective, and for the greedy algorithm to work I would in fact like them to really surjective, with every element having infinitely many preimages, not just at least one.

From the analysis of the case when $SM$ was finite, I extracted the following argument. Let $y$ be some non-square, and let $b$ be a square. We know that $L_b$ is surjective, hence $y = L_b^2 z$ for some $z = z_{b,y}$. Writing $c_{b,y} = Sz_{b,y}$, we obtain $L_{c_{b,y}} y = L_{Sz} L_b^2 z = b$. Thus, each non-square $y$ comes with a function $b \mapsto c_{b,y}$ from squares to squares with the property that $L_{c_{b,y}} y = b$. This function is clearly injective. When the squares are finite, this forces the function to be surjective, and now this is a problem because this has completely determined all of the left shift maps $L_a$ on squares, and forced them to also take values in the squares, which by surjectivity means that there are no non-squares! So we need infinitely many squares, and we also need the function $c_{b,y}$ to omit at least one element $c$ in its range.

So, every non-square $y$ now should come with two important square numbers - its own square $Sy$, which I denoted $a$, and an auxiliary square $c$, for which $L_c y$ is not automatically defined by the $L_{c_{b,y}} y$ rule and can be free to assign to help fulfill requirements such as the (infinite) surjectivity of $L_c$. For greedy algorithm purposes it would be nice to have a lot of $y$ s for each possible choice of pair $(a,c)$. This is what led me to choose the space of triples $(a,c,n)$ as the carrier for the non-squares, with $a$ representing the square and thus defining the squaring map: $S(a,c,n) = a$.

The map $y \mapsto c_{b,y}$, which partially defines the left multiplication maps via the formula $L_{c_{b,y}} y = b$, will be required to avoid $c$. It also has to solve the equation $L_a L_{c_{b,y}} b = L_{Sy} L_{c_{b,y}} L_{c_{b,y}} y = c_{b,y}$. On comparing this equation with $L_a L_{c'} L_{c'} a = c'$ for all squares $c'$ (here taking advantage of the property $Sa=a$ for squares), it becomes natural to choose $c_{b,y}$ so that $L_{c_{b,y}} a = b$, or equivalently $R_a c_{b,y} = b$. But it also has to avoid $c$, so it would be nice if map $R_a$ was at least doubly surjective so that we can always pick a point in its preimage that is not $c$. This was when I asked if there were non-right-cancellative models for 1516 known, and discovered that @Pace Nielsen had basically already built one using the translation-invariant method.

After verifying that this model could produce doubly surjective right multiplication maps, I now had a construction for $c_{b,y}$ for each $y = (a,c,n)$. So now I still had some entries of the multiplication table to fill in: each $y$ had $L_c y$ undefined, together with perhaps some other $L_{c'} y$ values as well. The main constraint to fulfill here to select a value of $L_{c'} y$ was to ensure that (a) $L_{c'}$ was infinitely surjective, and (b) the equation $L_a L_{c'} L_{c'} y = c'$ (from 1516) was obeyed.

For (b) I originally had a somewhat complicated greedy algorithm approach in which $L_{c'} y$ would be set to some previously unused non-square $z$ for which $L_{c'}$ was undefined, but I realized that it would be easier to set it to a suitable square in $SM$ that obeyed a compatibility condition. This initial technique was however very suited for attaching a pre-image of $L_{c'}$ to $y$; again one has to verify a compatibility condition, but it was straightforward to figure out the constraints and see that they could be solved.

[Pace Nielsen]

I was very happy to see Terry's recent solution to 1516->255!! :tada:

Although it is now moot, I figured I might as well finish my automated search for other relations. Although there is still the strong possibility that my program has some bugs in it, I've run it for a day, and after imposing the equalities $CS=SC$, $QS=S$, and

$$(Sx\diamond Cx)\diamond ((Sx\diamond Cx)\diamond x)=Cx$$

(as well as the obvious rule coming from 1516 itself) it didn't find any new needed rules. I'll let it run for one more day, just in case something pops up.

My feeling after writing the program is that $QS=S$ acts somewhat like a "zero-divisor" in a ring; I think of it as behaving something like $(Q-1)S=0$ (but without the subtraction). [Note: The displayed rule is not strictly necessary in the free 1516 magma on one symbol, and so without imposing it, then there could be some other zero-divisor-like behavior, coming from $S$ annihilating things on the left.]

[Jose Brox]

Pace Nielsen ha dicho:

I'll let it run for one more day, just in case something pops up.

How did this go? Did you finish the run?

[Pace Nielsen]

I made a sort of "kludge" to get around some weird behaviors, and it broke the program eventually. So, nothing new popped up before the program crashed.

[Bernhard Reinke]

I am trying to extend my (noncommutative) translation invariant 1516 !=> 1489 construction (see equational#831) to a "base" for the construction as outlined in the blueprint. I haven't fully digested the proof, but I think in Lemma 14.3 one has to exclude the case h = 0 and following that the case a=bin 14.4. Is this a problem down the line?

[Terence Tao]

Oof, this is indeed necessary since if $R_a c = a$ then from 1515 $c = Sa \diamond a$ so one can't have two solutions. I think I can fix this by removing the diagonal $a=c$ from the non-squares. Will work on this now.

[Terence Tao]

Grr, this is a non-trivial issue.

[Terence Tao]

Okay, I think I fixed it in equational#837, but it was harder than I expected, in particular I need to strengthen the base construction properties (and rework the "squares x non-squares" constructions) to make the argument work. In particular the base magma now needs some non-trivial solutions to the equation $a \diamond (b \diamond a) = b$, but fortunately this is easily achieved by adding such solutions to the starting seed.

[Bernhard Reinke]

Bernhard Reinke said:

I am trying to extend my (noncommutative) translation invariant 1516 !=> 1489 construction (see equational#831) to a "base" for the construction as outlined in the blueprint. I haven't fully digested the proof, but I think in Lemma 14.3 one has to exclude the case h = 0 and following that the case a=bin 14.4. Is this a problem down the line?

I finished the "base" construction. I want to have a look at another translation invariant proof instead of doing the rest of the 1516 -> 255, but it should be OK to black box the base construction