Proposed new target: 63 and 1692 ("Dupont and Dupond")

Stream: Equational

[Terence Tao]

The greedy algorithm has been run on all remaining equations, leaving 19 equations (up to duality) unresolved. I propose focusing efforts on Equation 63 x = y ◇ (x ◇ (x ◇ y)) and Equation 1692 x = (y ◇ x) ◇ ((y ◇ x) ◇ y), which share some similarities with the Asterix/Obelix pair, and which @Jose Brox has proposed calling "Dupont and Dupond" after the (Francophone version of) the bumbling detectives from "Tintin". Neither equation is known to imply the other; and 1692 also has 10 other unknown implications. After duality, understanding this pair would resolve 24 implications.

It is tempting to try everything in our bag of tricks to attack these laws. Some initial observations (very analogous to the Asterix/Obelix relation):

• Any magma obeying 1692 is left-cancellative: the maps x → y ◇ x are injective. Similarly, for any magma obeying 63, the maps x → y ◇ x are surjective.
• Conversely, 1692 implies 63 if the maps x → y ◇ x are surjective, since in that case one can write x = y ◇ z in 63 and invoke 1692. Similarly, 63 implies 1692 if the maps x → y ◇ x are injective, since by substititution 63 implies y ◇ x = y ◇ ((y ◇ x) ◇ ((y ◇ x) ◇ y)).
• In particular, for finite magmas the two laws are equivalent.

[Daniel Weber]

My greedy construction rule searching found 45 rules for 63 without terminating, so I'm not sure if that approach would be effective - I'll try to give it more time to run, though

[Terence Tao]

More simple observations:

• As noted in equation explorer, 63 implies 1922 x = (y ◇ (y ◇ x)) ◇ (x ◇ y). Proof: replace y with y ◇ (y ◇ x) in 63, and then simplify using 63 again.
• 63 also implies 23, x = (x ◇ x) ◇ x. Proof: replace y with x ◇ x in 63, and simplify using 63 again.
• 63 implies nine more non-trivial laws, but they are all easily derived from the above laws by simple substitutions. Unsurprisingly, these laws are precisely the ones that 1692 is not known to imply (except for 1629 x = (x ◇ x) ◇ ((x ◇ x) ◇ x), which is a consequence of 23 and hence 63, and also the y=x case of 1692).

[Daniel Weber]

Daniel Weber said:

My greedy construction rule searching found 45 rules for 63 without terminating, so I'm not sure if that approach would be effective - I'll try to give it more time to run, though

It can't find any counterexample for these rules, but also can't prove that they're preserved

[Jose Brox]

Let me explain why the linear magmas over (non)commutative rings cannot show that 63 does not imply 1692:
Let x·y:=ax+by in some ring. Then x·y=x·y' iff b(y-y')=0, so if the product has to be non-injective, then b must be a left zero divisor (this is actually valid over any (non)associative algebra.

Now, imposing 63 to the product, in any ring we get the set of equations b^2a+ba = 1, b^3+a=0. Rearranging, (b+1)ba = 1, a=-b^3. Hence a commutes with b, so (b+1)ba=1 is (b+1)ab=1, so b has a left inverse, and therefore cannot be a left zero divisor. Hence the product is injective.

So any linear magma satisfying Dupont also satisfies Dupond, over any ring.

[Pace Nielsen]

Here is a way to approach 1692 using linear-invariance. It is a bit different than previous linear-invariant arguments, because I couldn't make a finite greedy algorithm work because of strange collisions that kept coming up. So, instead I greedily adjoined infinitely many pairs at once.

Equation1692.pdf
Equation1692.tex

[Bhavik Mehta]

A curious fact, the dual of 1692 (1895) together with 65 (Asterix) imply 63. Or more specifically, 1895+Asterix imply commutativity, in which case 63 and 65 are equivalent

[Pace Nielsen]

Finished the non-implications from 1692.
Equation1692.pdf

[Terence Tao]

Bhavik Mehta said:

A curious fact, the dual of 1692 (1895) together with 65 (Asterix) imply 63. Or more specifically, 1895+Asterix imply commutativity, in which case 63 and 65 are equivalent

Nice crossover! https://tintin.fandom.com/wiki/Thompson_and_Thomson?file=Dupondt_em_Asterix.jpg

[Terence Tao]

Opened equational#607 to formalize @Pace Nielsen 's arguments (and will add the results to Conjectures.lean shortly). So I guess it's only 63 !=> 1692 that is remaining in this cluster?

[Ibrahim Tencer]

I believe I've found a counterexample to 63 => 1692 using the translation-invariant method. The functional equation for 63 is h = f(f(f(h)) - h). So if you know h and f(f(h)) you get an element h_2 = f(f(h)) - h with f(h_2) = h. So given initial values for h, f(h), and f(f(h)) you can construct the whole sequence going backwards such that each term is in the preimage of the previous one. The sequence has a linear recurrence relation which going forwards means that each term is the sum of the two terms before the previous term. The function you get in this way is apparently linear due to the linear recurrence relation, so if you make the initial three values generators of a free abelian group you can simply define f(a) = b, f(b) = c, and f(c) = a + b for the three generators a, b, c and extend by linearity. So for an arbitrary element we have f(xa + yb + zc) = xb + yc + z(a + b). It's straightforward to check that 63 holds for this, and it turns out that the RHS of 1692 is actually equal to 2y - x.

Because f is linear the resulting operation actually satisfies x*x = x. Has this kind of thing been seen before? I saw a recent thread using a free abelian group but I can't recall which one.

[Pace Nielsen]

@Ibrahim Tencer This looks quite interesting! The functional equation I'm getting for 63 is f(f^2(h)-h) = -h, but perhaps I'm using a different translation substitution. Which one are you using?

[Terence Tao]

Unfortunately I think this sign change rules out linear counterexamples. I agree with @Pace Nielsen that under the model $x \diamond y = x + f(y-x)$, 63 becomes $f(f^2(h)-h) = -h$, while 1692 becomes $f(h)+f^2(-f(h)) = h$. Under a linear model, the two equations are now equivalent.

[Terence Tao]

It might be interesting though to pursue nonlinear models using your idea, perhaps assuming that $f$ is odd in order to get the linear recurrence going properly. EDIT: to contradict 1692, $f$ will need to be non-injective. Otherwise, 63 implies $f(f^2(-f(h))+f(h)) = f(h)$, and this implies $f(h) + f^2(-f(h)) = h$ if $f$ is injective.

[Terence Tao]

Huh. If $f$ is odd then $f(f^2(h)-h)=-h$ becomes $f(h-f^2(h))=h$, and this does imply injectivity. Indeed, suppose that $f(h)=f(h') = a$, and write $f(a)=b$, then $f(h-b)=h$ and $f(h'-b)=h'$, then $f(h-b-a) = h-b$ and $f(h'-b-a)=h'-b$, and finally $f(-b-a)=h-b-a$ and $f(-b-a)=h'-b-a$, hence $h=h'$. So one has to break the odd-ness, which makes it trickier to iterate these equations. Still playing around with it...

[Daniel Weber]

There are 45 rules the greedy approach produced here. Vampire can prove that they're not preserved, but only via saturation, it can't produce a finite model, so I can't continue them. Would it be helpful to send them?

[Ibrahim Tencer]

Pace Nielsen said:

Ibrahim Tencer This looks quite interesting! The functional equation I'm getting for 63 is f(f^2(h)-h) = -h, but perhaps I'm using a different translation substitution. Which one are you using?

Yeah, it turns out I made a sign error. The construction does seem to give a model but the f you get is bijective so 1692 will also hold there.

[Terence Tao]

@Daniel Weber Sure, it can't hurt to see this. My guess is that with this rule, every entry one adds to the multiplication table has to be accompanied by a lot of other entries to maintain compatibility, which is why the ruleset must necessarily explode, but it is still good to see an example of what "greedy algorithm failure" looks like.

[Daniel Weber]

• $R(x, y, z) \wedge R(x, y, w) \to z = w$
• $R(x, y, z) \wedge R(x, z, w) \to R(y,w,x)$
• $R(x, y, z) \wedge R(y, y, x) \to R(z,y,x)$
• $R(x, y, z) \wedge R(y, x, x) \to R(z,y,x)$
• $R(x, x, y) \wedge R(x, y, z) \to R(z,y,x)$
• $R(x, x, y) \to R(y,x,x)$
• $R(x, y, z) \wedge R(x, w, y) \wedge R(w, x, u) \to R(z,u,w)$
• $R(x, y, z) \wedge R(x, w, y) \wedge R(w, x, w) \to R(w,w,z)$
• $R(x, x, y) \wedge R(x, z, x) \to R(x,y,z)$
• $R(x, y, z) \wedge R(y, x, w) \wedge R(w, x, w) \wedge R(w, y, w) \to R(x,z,w)$
• $R(x, y, z) \wedge R(y, x, w) \wedge R(w, x, w) \wedge R(w, y, w) \to R(y,z,w)$
• $R(x, y, x) \wedge R(x, z, x) \wedge R(z, y, x) \to R(z,x,y)$
• $R(x, y, z) \wedge R(x, z, w) \wedge R(y, x, y) \to R(x,w,y)$
• $R(x, y, x) \wedge R(y, x, z) \wedge R(z, x, w) \to y = w$
• $R(x, y, z) \wedge R(x, z, w) \wedge R(y, x, y) \to R(w,z,x)$
• $R(x, y, x) \wedge R(x, z, x) \to y = z$
• $R(x, y, z) \wedge R(y, x, y) \to R(z,y,x)$
• $R(x, y, z) \wedge R(y, x, z) \wedge R(z, x, z) \to x = y$
• $R(x, y, z) \wedge R(y, x, z) \wedge R(z, x, x) \to x = y$
• $R(x, y, z) \wedge R(x, w, y) \wedge R(y, u, x) \wedge R(w, x, v) \wedge R(u, x, w) \wedge R(u, y, u) \to R(v,u,z)$
• $R(x, y, z) \wedge R(x, w, z) \wedge R(y, x, u) \wedge R(w, x, u) \to y = w$
• $R(x, y, z) \wedge R(y, w, x) \wedge R(w, y, y) \to R(x,z,w)$
• $R(x, x, y) \wedge R(x, z, x) \wedge R(z, x, w) \to R(z,w,y)$
• $R(x, y, z) \wedge R(y, x, z) \wedge R(z, w, x) \wedge R(w, x, y) \wedge R(w, z, w) \to R(x,z,x)$
• $R(x, y, z) \wedge R(y, z, x) \wedge R(z, x, y) \wedge R(z, y, w) \wedge R(w, x, y) \to R(x,z,z)$
• $R(x, y, z) \wedge R(x, w, z) \wedge R(y, x, w) \wedge R(w, u, x) \wedge R(u, w, y) \to R(x,z,u)$
• $R(x, y, z) \wedge R(y, x, w) \wedge R(z, w, x) \wedge R(w, x, y) \wedge R(w, z, w) \to y = w$
• $R(x, y, z) \wedge R(x, w, z) \wedge R(y, x, y) \wedge R(w, x, w) \to y = w$
• $R(x, x, y) \wedge R(x, z, x) \wedge R(z, x, w) \wedge R(z, u, w) \to R(u,y,z)$
• $R(x, y, z) \wedge R(x, w, z) \wedge R(y, x, y) \wedge R(w, x, z) \to x = w$
• $R(x, y, z) \wedge R(x, z, w) \wedge R(x, u, z) \wedge R(y, x, u) \wedge R(u, x, v) \to R(v,y,w)$
• $R(x, y, z) \wedge R(y, x, w) \wedge R(y, z, w) \wedge R(z, y, x) \wedge R(w, z, z) \to R(x,z,y)$
• $R(x, y, z) \wedge R(y, x, w) \wedge R(z, x, y) \wedge R(w, x, y) \wedge R(w, z, x) \to R(x,z,y)$
• $R(x, y, z) \wedge R(x, w, z) \wedge R(y, x, u) \wedge R(w, x, y) \wedge R(u, w, v) \to R(x,z,v)$
• $R(x, y, z) \wedge R(x, z, w) \wedge R(x, u, z) \wedge R(y, x, u) \wedge R(u, x, v) \wedge R(v, u, y) \to R(x,w,z)$
• $R(x, y, z) \wedge R(y, x, w) \wedge R(y, u, w) \wedge R(u, y, x) \wedge R(u, z, z) \to u = y$
• $R(x, y, z) \wedge R(x, w, z) \wedge R(y, x, w) \wedge R(w, x, y) \to w = y$
• $R(x, y, z) \wedge R(x, w, z) \wedge R(y, x, u) \wedge R(w, x, y) \wedge R(u, y, w) \to R(z,z,x)$
• $R(x, y, z) \wedge R(y, z, w) \wedge R(y, u, w) \wedge R(z, y, u) \wedge R(u, y, x) \to R(w,x,y)$
• $R(x, y, z) \wedge R(x, z, w) \wedge R(x, u, z) \wedge R(y, x, v) \wedge R(u, x, y) \wedge R(u, v, u) \to R(w,u,z)$
• $R(x, y, z) \wedge R(y, w, u) \wedge R(w, y, v) \wedge R(w, u, v) \wedge R(u, w, x) \to R(u,z,w)$
• $R(x, y, z) \wedge R(y, x, w) \wedge R(y, z, w) \wedge R(z, y, u) \wedge R(u, x, v) \to R(v,u,z)$
• $R(x, y, z) \wedge R(x, w, u) \wedge R(x, v, z) \wedge R(y, x, x') \wedge R(v, x, y) \wedge R(v, x', v) \to R(y,w,u)$
• $R(x, y, z) \wedge R(y, w, u) \wedge R(w, y, v) \wedge R(w, u, v) \wedge R(u, w, x) \to R(y,z,w)$
• $R(x, y, z) \wedge R(y, x, w) \wedge R(y, z, w) \wedge R(z, y, u) \wedge R(u, x, v) \to R(v,z,x)$

[Terence Tao]

It's possible that a noncommutative model $x \diamond y = x f(x^{-1} y)$ may fare better than a commutative one for this particular equation, but I haven't explored this properly.

[Terence Tao]

I've managed to make the translation-invariant greedy construction work and finish off the final anti-implicatin 63 != 1692. However, the proof is a bit messy and there may be a simpler option.

As discussed above, the issue is to construct solutions to the equation $f(f^2(h)-h) = -h$. The fact that the right-hand side is $-h$ rather than $h$ is what is causing all the difficulty. The greedy algorithm consists of iteratively building two sets in the carrier which I found convenient to take to be a four-dimensional lattice ${\mathbb Z}^3 \times {\mathbb Z}$: a smaller set $E_1$, which is symmetric around the origin and contains ${\mathbb Z}^3$ together with some finite number of elements, where the Dupont equation 63 is verified; and an additional finite set $E_2 \backslash E_1$ of elements $h$ on which the function $f(h)$ is defined, but $f(-h)$ is not, and the Dupont equation has not yet been verified here. The general strategy is then (as with the Asterix equation) to remote "promote" elements of $E_2 \backslash E_1$ to $E_1$ by extending the function $f$ to obey the Dupont equation, and also to "promote" elements outside of $E_2$ to lie inside $E_2$. However, the number of side rules needed to maintain consistency is moderately large, and I was forced to take a rather complex construction to maintain these side rules (the biggest problem was ensuring that $f^2(h) - h$ did not accidentally fall into the set where $f$ was already defined).

I have a suspicion that the argument could be simplified if one took a more nonabelian approach, but I couldn't find it. The proof, while complicated, is still amenable to formalization, so I will mark it as a conjecture and set up equational#643 to formalize this. But I am somewhat hoping that a simpler approach is found.

[Pace Nielsen]

Ah, you beat me to it. My solution looks a bit more complicated than yours, but here it is.
Equation63.pdf
Equation63.tex

[Terence Tao]

Nice! Actually I'd say yours is slightly simpler (I start with an infinite "seed" which is basically ${\mathbb Z}^3$ and this complicates things a bit. It's a remarkably fiddly law to work with, the naive greedy constructions need all sorts of tweaks until they finally start working...

[Jose Brox]

(Edited to write the correct identities)
I was working with a different approach: imposing some other equation in addition to 63 so that together they still don't imply 1692 (measured by running Prover9 a sensible time without a positive answer), trying to get as few models as possible, in order for the decision tree to be as determined as possible when trying to construct the infinite model.

One can for example add xx=x or xx=yy. I decided to add x(xx) = y(yy), which imposes more restrictions. It for example implies that there is a such that a^2 = a, and no other x has x^2 = a or x (neither can we have x^2 = y and y^2 = x for any two x,y). It also implies xa = x and a(xx) = x, which in addition to(xx)x = x, x(xx) = a and a = x(a(ax)) seem to almost determine a single model. I was planning to write a program to write the sudoku with human guiding (I will try to write it anyway).

Note that this variety does not have any nontrivial translation-invariant model, even noncommutative!

[Jose Brox]

Also, the resulting variety of 63+x(xx) = y(yy) happens to be congruence-permutable, as it possess the Malcev term p(x,y,z) = y(x(x,z)) satisfying p(x,y,y) = x, p(x,y,x) = y. I suspect this could help with a more algebraic proof, but didn't have the time to think about it.

[Ibrahim Tencer]

It turns out that 63 along with associativity implies x = y although this is a bit tricky to prove. 63 then becomes x = yxxy which implies x = x⁴ in particular. But then also x² = yx²x²y = yx⁴y = yxy, so x² = x³ in particular. But then we can multiply both sides by x² to get x⁴ = x⁴x so in fact x = x². Then the original equation becomes x = yxy, which we can multiply on both sides by x to get x² = yxyx = (yx)² so x = yx. But we also get x = xy by multiplying on the other side so x = xy = y.

Not sure if commutativity or idempotence or even both would imply triviality but they also don't seem very helpful without associativity. Edit: actually the linear model I constructed earlier is idempotent.

[Jose Brox]

Ibrahim Tencer ha dicho:

Not sure if commutativity or idempotence or even both would imply triviality but they also don't seem very helpful without associativity. Edit: actually the linear model I constructed earlier is idempotent.

This kind of question can be resolved quickly with the aid of Prover9: 63+commutativity don't seem to imply x=y (Prover9 runs for a while without finding a proof), but they do imply 1692 (Prover9 finds a proof in a split second). In fact I checked 63 + any other equation up to 200 or so, to find those seemingly not implying 1692.

[Terence Tao]

I added @Pace Nielsen 's proof to the blueprint (phrased over the integers to simplify the notation a little), see equational#656. I think axiom (8) is not actually needed, so I removed it to very slightly simplify the proof. I think this one will be a little bit easier to formalize than my first proof.

[Terence Tao]

By the way, the main reason my proof was so complicated is that I had made the initial design choice to make the partial function closed under forward iteration: if $h \in E$, then $f(h) \in E$. This required first setting up an infinite seed (basically a copy of ${\mathbb Z}^3$) which was already a global solution to the Dupont equation, and then adding more elements to $E$ by basically connecting them to this seed after some finite number of iterates. But I now see that there was no need to enforce this forward closure, and Pace's construction, in which the partial solutions are not closed under either forward or backward iteration (or negation), is simpler for iterative purposes.