Equation 65 -> left cancellability

Stream: Equational

[Daniel Weber]

I attempted to think of Equation 65 -> Equation 359 (x = y ◇ (x ◇ (y ◇ x)) -> x ◇ x = (x ◇ x) ◇ x) for a couple of hours, but couldn't think of anything successful.
My first attempt was to look at sextuples of natural numbers, and define the operation as "rotate the RHS by 2, and if the XORs of the numbers in the LHS and in the RHS are different then XOR to the all numbers on the RHS the xor of all numbers on the LHS". The idea here that the XOR is an invariant - the XOR of the output is the XOR of the LHS, and using it the involution of "XOR some values depending on y to all values" can only fire for y, not for x. The problem with this, of course, is that the interesting part doesn't activate for (x ◇ x) ◇ x, so it satisfies equation 359.

Then I wanted to generalize it, by using the fact that the LHS isn't rotated---define some compatibility relation, such that compatible(y, x ◇ (y ◇ x)) ↔ compatible(y, x) and compatible(x, y ◇ x), and then define the operation differently based on whether the LHS and the RHS are compatible. The problem with this is that for it to be interesting we need ¬ compatible(x ◇ x, x), and I'm not sure how to get that.

One thing I thought of is finding a triple of functions $f,g,h$ such that $f \circ g \circ h = g \circ h \circ f = h \circ f \circ g = \text{id}$, but not the other way round $h \circ g \circ f \ne \text{id}, f \circ h \circ g \ne \text{id}, g \circ f \circ h \ne \text{id}$. I have a vague intuition that this could be helpful, as pairs of functions such that $f \circ g = \text{id}, g \circ f \ne \text{id}$ had been useful for other infinite models, but I'm not sure.

[Terence Tao]

It seems to me that the linear operation x ◇ y = ω y, where ω is a cube root of unity in the ambient field, should establish the anti-implication, no? But then it should have been picked up by the large linear magma sweep we just did, which is odd.

(Just to record my thought process on how I found this example. I postulated that there was some unary operation L on the magma so that x ◇ (y ◇ x) = L(x) and x = y ◇ L(x), in order to break up the hypothesis 65 into simpler pieces. The second law forces L to be injective. Replacing x with L(x) in the first law got me to L(x) ◇ x = L^2(x), and replacing x with L(x) again then got me to x = L^3(x). At this point I realized I should try L being multiplication by a cube root of unity, leading to the above example.)

EDIT: oh, wait, this example also obeys 359, so it isn't a counterexample. Ah, not as easy as it looks...

[Terence Tao]

OK, trying again, this time with a general linear operation x ◇ y = ax+by. If I have calculated things correctly, Equation 65 becomes the system a(1+b^2)=0, b(a+b^2)=1, and Equation 359 becomes a(a+b-1)=0. Oh, interesting, here it does seem that again the former implies the latter. If a=0 this is clear, otherwise we have 1+b^2=0 and b(a+b^2)=1, and on multiplying the latter by b and substituting b^2=-1 we get after some algebra a+b-1=0. OK, this explains why this wasn't picked up by the linear magma sweep.

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

This is the "sibling" of the 65->3862 potential implication that I proposed in this thread, right? I don't have access to my notes right now but IIRC 65 and 359 together imply 3862, so it'd resolve that too.

[Daniel Weber]

Could you explain the proof that the implication holds on finite magmas? I imagine that might guide searching for counterexamples

[Daniel Weber]

Here's another idea I had:
We define an inductive type with three constructors, t : type -> type -> type, pair : type -> type -> type and nil : type. We write (a, b) for pair a b, t_x(a) for t x a and t_x(a, b) for t_x(pair a b).
We now start with basic definition a * b = (a, b), and each time add exceptions, the latest applicable definition is the one that applies, and the idea is to eventually get a model where 65 holds. First we add b * (a, b) = t_a(b) and a * t_a(b) = b.
Now b * ((a, b) * (b * (a, b))) = b * ((a, b) * t_a(b)) != (a, b), so we add (a, b) * t_a(b) = t_b(a, b).
Now a * (t_a(b) * (a * t_a(b))) = a * (t_a(b) * b) != t_a(b), so we add t_a(b) * b = t_a(t_a(b)).
Then (a,b) * (t_a(b) * t_b(a, b)) != t_a(b), so we add t_a(b) * t_b(a,b) = t_{a,b}(t_a(b)).

This can continue manually, but is probably better done using a computer (either semi or fully automatically), until we either finish, or maybe spot a pattern and generalize it.

Does this seem likely to work? Is there a better inductive type/basic definitions? Perhaps more constructors will be better?

[Daniel Weber]

I think that's actually just equality saturation, which probably doesn't finish in a sensible number of steps, as vampire would've found that, but perhaps we could see some pattern to the equations

[Daniel Weber]

Apparently (a, b) * t_a(b) = t_b(a, b) is too strong of an assumption, it implies 359

[Terence Tao]

OK, here is yet another attempt at creating a counterexample, inspired by @Daniel Weber 's triple function idea.

Let $f_0, f_1, f_2: X \to X$ be a triple of functions to be chosen later. We extend this periodically mod 3, thus $f_{i+3} = f_i$. Now consider the magma $X \times ({\bf Z}/3{\bf Z})$ with operation

$(x,i) \diamond (y,j) := (f_{i-j}(y), j+1).$

Then we have
$(x,i) \diamond (x,i) = (f_0(x),i+1)$
and
$((x,i) \diamond (x,i)) \diamond (x,i) = (f_1 \circ f_0(x),i+2)$

so 359 is certainly false. On the other hand,
$(y,j) \diamond (x,i) = (f_{j-i}(x), i+1)$
$(x,i) \diamond ((y,j) \diamond (x,i)) = (f_{-1} \circ f_{j-i}(x), i+2)$
$(y,j) \diamond ((x,i) \diamond ((y,j) \diamond (x,i))) = (f_{j-i-2} \circ f_{-1} \circ f_{j-i}(x), i)$
so if we can solve the equations
$f_{j-i-2} \circ f_{-1} \circ f_{j-i} = \mathrm{id}$
then we get a counterexample.

Oh, but we can just take all the $f_i$ to be the identity! And $X$ to be trivial! So, um, it seems that a really simple counterexample is ${\bf Z}/3{\bf Z}$ with operation $x \diamond y = y+1$. That was embarrassingly obvious. But perhaps the more general construction above will be helpful for other problems.

The broader metatheorem seems to be: if the hypothesis is $w \simeq w'$ with both $w, w'$ ending in the same letter, and whose lengths are equal modulo $n$, then all equations implied by this hypothesis have to have the same property. Proof: use the operation $x \diamond y = y+1$ on ${\bf Z}/n{\bf Z}$. I'll add that metatheorem to the blueprint later today.

But it does raise an obvious TODO: study affine magmas $x \diamond y = ax + by + c$ and see if they can clear out a chunk of the remaining implications.

[Daniel Weber]

$x \diamond y = y+1$ doesn't work, it satisfies $x \diamond x = (x \diamond x) \diamond x$

[Daniel Weber]

The problem is that $((x,i) \diamond (x,i)) \diamond (x,i) = (f_1 \circ f_0(x),i+1) \ne (f_1 \circ f_0(x),i+2)$, but I think the functional equation could still potentially be solved to generate a counterexample

[Terence Tao]

Argh! Can't believe I made the same mistake three times in a row. I should have computed
$((x,i) \diamond (x,i)) \diamond (x,i) = (f_1(x), i+1)$
so actually one needs to solve the system
$f_0 \circ f_2 \circ f_2 = \mathrm{id}$
$f_1 \circ f_2 \circ f_0 = \mathrm{id}$
$f_2 \circ f_2 \circ f_1 = \mathrm{id}$
$f_0 \neq f_1$
which looks doable (but I haven't checked details, maybe I made another mistake).

[Daniel Weber]

Sadly this is impossible, $f_1 = \text{id} \circ f_1 = f_0 \circ f_2 \circ f_2 \circ f_1 = f_0 \circ \text{id} = f_0$

[Daniel Weber]

A potential approach using Vampire is to try and add some equations (and maybe some pairs of equations) in hopes that they might not imply Equation 359 but still limit the search space enough for Vampire to find a saturation

[Daniel Weber]

Is it theoretically possible that there's a false implication which we can't disprove in ZFC?

[Pace Nielsen]

Using a map of the form x⋄y=ax+by+c, leads to the set of equations ba+b^3=1, a+b^2a=0, and a^2+ab\neq a. It turns out these are inconsistent over noncommutative rings. So no affine map with work over coefficients from a ring.

[Pace Nielsen]

Daniel Weber said:

Is it theoretically possible that there's a false implication which we can't disprove in ZFC?

Yes, it was shown in the literature that whether or not an equation implies x=y is algorithmically undecidable.

[Terence Tao]

Daniel Weber said:

Is it theoretically possible that there's a false implication which we can't disprove in ZFC?

That's a good question. I believe there finite systems of equations, for which it is undecidable in ZFC whether they imply some other equation, but I don't know the literature well. Actually it will be good to sort this out, this needs to be mentioned in the paper.

Shame that the functional and the ring-theoretic approaches now seem fairly conclusively ruled out. On the other hand, perhaps this should be viewed as evidence that the implication is in fact true? We've now constructed a reasonably diverse set of models to 65 and they all "accidentally" happen to satisfy 359 as well. This is beginning to look like it's not a coincidence... perhaps the above arguments can somehow be deconstructed for clues on how to get from 65 to 359, e.g., by identifying some intermediate assertion that also seems to be true for all the models?

EDIT: we should also test the above models on the other unresolved potential consequences 614, 817, 1426, 1491, 3862, 4065 of 65. And maybe try to work out the logical relations between these statements assuming 65 as an ambient hypothesis. We might be trying to work on the hardest implication, despite it being the shortest unresolved one.

[Terence Tao]

@Vlad Tsyrklevich Is it easy to get Graphiti to do a Hasse diagram of all the statements that are either implied by, or potentially implied by, a given statement such as 65?

EDIT: Oh, it is!

graph.png

[Terence Tao]

From the diagram it seems we should test both the ring-theoretic and the function-theoretic constructions against 1491 first.

[Terence Tao]

(But it would be nice to have the ability to generate this graph in one click from the Equation Explorer page for 65. I did it manually by entering in all the potential consequences of 65.)

[Daniel Weber]

Terence Tao said:

Daniel Weber said:

Is it theoretically possible that there's a false implication which we can't disprove in ZFC?

That's a good question. I believe there finite systems of equations, for which it is undecidable in ZFC whether they imply some other equation, but I don't know the literature well. Actually it will be good to sort this out, this needs to be mentioned in the paper.

Shame that the functional and the ring-theoretic approaches now seem fairly conclusively ruled out. On the other hand, perhaps this should be viewed as evidence that the implication is in fact true? We've now constructed a reasonably diverse set of models to 65 and they all "accidentally" happen to satisfy 359 as well. This is beginning to look like it's not a coincidence... perhaps the above arguments can somehow be deconstructed for clues on how to get from 65 to 359, e.g., by identifying some intermediate assertion that also seems to be true for all the models?

EDIT: we should also test the above models on the other unresolved potential consequences 614, 817, 1426, 1491, 3862, 4065 of 65. And maybe try to work out the logical relations between these statements assuming 65 as an ambient hypothesis. We might be trying to work on the hardest implication, despite it being the shortest unresolved one.

I still think that this is false, but all the models we managed to think of are too nice for it to fail. In particular, the magma being left cancellative implies 359, as does f_y(x) = x * (y * x) being surjective for all y

[Terence Tao]

Do you have proofs of these assertions written up somewhere? They might provide further clues.

The function model at least doesn't have surjectivity of f_y, and could potentially be not left-cancellative if the functions involved are not injective. So I hold out some hope that some more sophisticated version of the model (e.g., $(x,i) \diamond (y,j) := (f_{i-j,x}(y), j+1)$ where $f_{i-j,x}$ depends in some relatively mild way on $x$) might still work.

EDIT: the new system seems to be
$f_{0,y} \circ f_{2,x} \circ f_{2,y}(x) = x$
$f_{1,y} \circ f_{2,x} \circ f_{0,y}(x) = x$
$f_{2,y} \circ f_{2,x} \circ f_{1,y}(x) = x$
$f_{1, f_{0,x}(x)}(x) \not \equiv f_{0,x}(x)$

[Daniel Weber]

Terence Tao said:

Do you have proofs of these assertions written up somewhere? They might provide further clues.

[...]

Vampire proved them and I'm not at home right now, I'll send them in a couple of hours

[Vlad Tsyrklevich]

Terence Tao said:

(But it would be nice to have the ability to generate this graph in one click from the Equation Explorer page for 65. I did it manually by entering in all the potential consequences of 65.)

So just to verify: a link to chart of implies for the target equation and all it's unknowns. I can put a PR up later tonight for that. What's a good name for that graph? https://teorth.github.io/equational_theories/graphiti/?render=true&implies=65,359,614,817,1426,1491,3862&highlight_red=65&highlight_blue=359,614,817,1426,1491,3862

I suppose what may also be nice is to have dashed edges between unknowns in the chart to also show what unknown relationships there are between the vertices, though maybe the unknown set is small enough now that that feature is no longer as useful.

[Terence Tao]

"Potential forward implications of EquationX"?
Similarly one can have
"Potential backward implications of EquationX" (proven + conjectured + open)
"Conjectured forward implications of EquationX" (proven + conjectured)
"Conjectured backwards implications of EquationX" (proven + conjectured)

similar to the current functionality of
"Proven forward implications of EquationX" (proven only)
"Proven backwards implications of EquationX" (proven only)

so maybe one just needs to add a dropdown feature next to the current "Equation implies" and "Equation implied by" text boxes to indicated whether implies/implied by means "proven only", "proven or conjectured", or "proven, conjectured, or open" (with the former being the default).

[Terence Tao]

One can also have options to include conjectural implications and open implications (dashed arrows and dotted arrows, perhaps?) within the visualization as you suggest, though turned off by default.

[Terence Tao]

Terence Tao said:

EDIT: the new system seems to be
$f_{0,y} \circ f_{2,x} \circ f_{2,y}(x) = x$
$f_{1,y} \circ f_{2,x} \circ f_{0,y}(x) = x$
$f_{2,y} \circ f_{2,x} \circ f_{1,y}(x) = x$
$f_{1, f_{0,x}(x)}(x) \not \equiv f_{0,x}(x)$

If one takes a piecewise linear model
$f_{2,x}(y) = ax+by; f_{1,x}(y) = cx+dy; f_{0,x}(y) = ex+fy$
then (if my hand calculations are correct) the system becomes
$e+fba = 0; f(a+b^2)=1$
$c+dbe = 0; d(a+bf)=1$
$a+b^2 c = 0; b(a+bd)=1$
$c(e+f)+d \neq e+f$
and it should be possible to use a standard algebra package to see if this is solvable. (But it should be double checked, as one can see from past history I am making a lot of mistakes with this hand calculation.)

[Daniel Weber]

One thing to note is that the implication holds over finite models (as the magna is then left cancellative), so examples like this (which from what I understand imply that it has a counterexample in fields with large enough characteristic) can't work

[Terence Tao]

Ok... well one may have to go to noncommutative models then, where it should become possible to exclude finite models. The algebra should still be the same, but now one needs a noncommutative algebra package rather than a commutative algebra package to analyze it...

[Terence Tao]

This equation 65 is beginning to remind me of the village of Asterix and Obelix ("One small village of indomitable Gauls still holds out against the invaders...")

[Daniel Weber]

Daniel Weber said:

Terence Tao said:

Do you have proofs of these assertions written up somewhere? They might provide further clues.

[...]

Vampire proved them and I'm not at home right now, I'll send them in a couple of hours

The proof is via Equation 1491 x = (y ◇ x) ◇ (y ◇ (y ◇ x)), which is immediate to deduce from left cancellativity and 65 by applying y to the left

[Daniel Weber]

Terence Tao said:

From the diagram it seems we should test both the ring-theoretic and the function-theoretic constructions against 1491 first.

I see you mentioned 1491 earlier here, perhaps we should focus on 65 -> 1491

[Terence Tao]

Tellingly, 1491 is also the only equation whose implication into 65 remains open.

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

Daniel Weber said:

Could you explain the proof that the implication holds on finite magmas? I imagine that might guide searching for counterexamples

Sorry, I was traveling and mostly offline yesterday, just catching up with this thread. I see you've got the left-cancellability proof (it's the one I had, I've been a one-trick pony with my cancellative monoids in this project).

I picked 65 for good reason after your question about all remaining implications being false -
I've tried quite hard to construct infinte counterexamples after that, and bounced back hard. Glad to see in this thread that it wasn't just a "me" problem :sweat_smile:

[Daniel Weber]

Does equation 65 appear somewhere in the literature, by any chance?

[Terence Tao]

If it's not known, I (half-seriously) propose calling 65 "Asterix", and 1491 "Obelix".

[Terence Tao]

A simple observation: assuming 65, 1461 is in fact equivalent to left cancellability (since 1461 recovers x from y and yx). So the key question is whether models of 65 have to be left cancellative, ie left multiplication by y is injective. (Certainly it is surjective.)

[Daniel Weber]

Setting $0 \diamond 1 = 0 \diamond 2$ and quotienting by equation 65 it may be interesting to see what equivalence classes Vampire can prove, perhaps that could give some insight to how they look

[Daniel Weber]

Here are the (conjectured) non-trivial equivalence classes (where non-trivial means using equation 65). There's nothing interesting yet, but I'm doing a larger run now (which will likely take a few hours)

• $0$: $0 \diamond (0 \diamond (0 \diamond 0))$, $1 \diamond (0 \diamond (1 \diamond 0))$, $2 \diamond (0 \diamond (2 \diamond 0))$
• $1$: $0 \diamond (1 \diamond (0 \diamond 1))$, $0 \diamond (1 \diamond (0 \diamond 2))$, $1 \diamond (1 \diamond (1 \diamond 1))$, $2 \diamond (1 \diamond (2 \diamond 1))$
• $2$: $0 \diamond (2 \diamond (0 \diamond 1))$, $0 \diamond (2 \diamond (0 \diamond 2))$, $1 \diamond (2 \diamond (1 \diamond 2))$, $2 \diamond (2 \diamond (2 \diamond 2))$

[Hernan Ibarra]

I think free semigroup on x,y modulo the equation (y x)^2 = x satisfies 65 but not 359

[Hernan Ibarra]

I don't have a proof of this yet (confluence might help; otherwise induction on the proof tree). Does it seem like it would work?

[Daniel Weber]

Sadly associativity + 65 implies 359, according to Vampire

[Hernan Ibarra]

Darn

[Hernan Ibarra]

Good to know though

[Daniel Weber]

In fact it even implies $x \diamond y = y$

[Joachim Breitner]

Is the rule (yx)(yx) -> x confluent, by a similar argument as 477? Probably not exactly the same argument, as it can apply on its own lhs's subterms, can it? But only if y = x, so maybe that helps with a (more complicated) confluence proof.

[Daniel Weber]

Daniel Weber said:

Here are the (conjectured) non-trivial equivalence classes (where non-trivial means using equation 65). There's nothing interesting yet, but I'm doing a larger run now (which will likely take a few hours)
[...]

This finished. Any patterns you can see here? (I don't include values which contain $0 \diamond 2$, as that's immediately reducible)

• $0$: $0 \diamond (0 \diamond (0 \diamond 0))$, $1 \diamond (0 \diamond (1 \diamond 0))$, $2 \diamond (0 \diamond (2 \diamond 0))$
• $1$: $0 \diamond (1 \diamond (0 \diamond 1))$, $1 \diamond (1 \diamond (1 \diamond 1))$, $2 \diamond (1 \diamond (2 \diamond 1))$
• $2$: $0 \diamond (2 \diamond (0 \diamond 1))$, $1 \diamond (2 \diamond (1 \diamond 2))$, $2 \diamond (2 \diamond (2 \diamond 2))$
• $0 \diamond 0$: $0 \diamond (0 \diamond (0 \diamond (0 \diamond 0)))$, $0 \diamond (1 \diamond (0 \diamond (1 \diamond 0)))$, $0 \diamond (2 \diamond (0 \diamond (2 \diamond 0)))$, $(0 \diamond (0 \diamond (0 \diamond 0))) \diamond 0$, $(1 \diamond (0 \diamond (1 \diamond 0))) \diamond 0$, $(2 \diamond (0 \diamond (2 \diamond 0))) \diamond 0$
• $0 \diamond 1$: $0 \diamond (0 \diamond (1 \diamond (0 \diamond 1)))$, $0 \diamond (0 \diamond (2 \diamond (0 \diamond 1)))$, $0 \diamond (1 \diamond (1 \diamond (1 \diamond 1)))$, $0 \diamond (1 \diamond (2 \diamond (1 \diamond 2)))$, $0 \diamond (2 \diamond (1 \diamond (2 \diamond 1)))$, $0 \diamond (2 \diamond (2 \diamond (2 \diamond 2)))$, $(0 \diamond (0 \diamond (0 \diamond 0))) \diamond 1$, $(0 \diamond (0 \diamond (0 \diamond 0))) \diamond 2$, $(1 \diamond (0 \diamond (1 \diamond 0))) \diamond 1$, $(1 \diamond (0 \diamond (1 \diamond 0))) \diamond 2$, $(2 \diamond (0 \diamond (2 \diamond 0))) \diamond 1$, $(2 \diamond (0 \diamond (2 \diamond 0))) \diamond 2$
• $1 \diamond 0$: $1 \diamond (0 \diamond (0 \diamond (0 \diamond 0)))$, $1 \diamond (1 \diamond (0 \diamond (1 \diamond 0)))$, $1 \diamond (2 \diamond (0 \diamond (2 \diamond 0)))$, $(0 \diamond (1 \diamond (0 \diamond 1))) \diamond 0$, $(1 \diamond (1 \diamond (1 \diamond 1))) \diamond 0$, $(2 \diamond (1 \diamond (2 \diamond 1))) \diamond 0$
• $1 \diamond 1$: $1 \diamond (0 \diamond (1 \diamond (0 \diamond 1)))$, $1 \diamond (1 \diamond (1 \diamond (1 \diamond 1)))$, $1 \diamond (2 \diamond (1 \diamond (2 \diamond 1)))$, $(0 \diamond (1 \diamond (0 \diamond 1))) \diamond 1$, $(1 \diamond (1 \diamond (1 \diamond 1))) \diamond 1$, $(2 \diamond (1 \diamond (2 \diamond 1))) \diamond 1$
• $1 \diamond 2$: $1 \diamond (0 \diamond (2 \diamond (0 \diamond 1)))$, $1 \diamond (1 \diamond (2 \diamond (1 \diamond 2)))$, $1 \diamond (2 \diamond (2 \diamond (2 \diamond 2)))$, $(0 \diamond (1 \diamond (0 \diamond 1))) \diamond 2$, $(1 \diamond (1 \diamond (1 \diamond 1))) \diamond 2$, $(2 \diamond (1 \diamond (2 \diamond 1))) \diamond 2$
• $2 \diamond 0$: $2 \diamond (0 \diamond (0 \diamond (0 \diamond 0)))$, $2 \diamond (1 \diamond (0 \diamond (1 \diamond 0)))$, $2 \diamond (2 \diamond (0 \diamond (2 \diamond 0)))$, $(0 \diamond (2 \diamond (0 \diamond 1))) \diamond 0$, $(1 \diamond (2 \diamond (1 \diamond 2))) \diamond 0$, $(2 \diamond (2 \diamond (2 \diamond 2))) \diamond 0$
• $2 \diamond 1$: $2 \diamond (0 \diamond (1 \diamond (0 \diamond 1)))$, $2 \diamond (1 \diamond (1 \diamond (1 \diamond 1)))$, $2 \diamond (2 \diamond (1 \diamond (2 \diamond 1)))$, $(0 \diamond (2 \diamond (0 \diamond 1))) \diamond 1$, $(1 \diamond (2 \diamond (1 \diamond 2))) \diamond 1$, $(2 \diamond (2 \diamond (2 \diamond 2))) \diamond 1$
• $2 \diamond 2$: $2 \diamond (0 \diamond (2 \diamond (0 \diamond 1)))$, $2 \diamond (1 \diamond (2 \diamond (1 \diamond 2)))$, $2 \diamond (2 \diamond (2 \diamond (2 \diamond 2)))$, $(0 \diamond (2 \diamond (0 \diamond 1))) \diamond 2$, $(1 \diamond (2 \diamond (1 \diamond 2))) \diamond 2$, $(2 \diamond (2 \diamond (2 \diamond 2))) \diamond 2$
• $0 \diamond (0 \diamond 0)$: $0 \diamond ((0 \diamond (0 \diamond 0)) \diamond 0)$
• $0 \diamond (1 \diamond 0)$: $1 \diamond ((0 \diamond (1 \diamond 0)) \diamond 0)$
• $0 \diamond (2 \diamond 0)$: $2 \diamond ((0 \diamond (2 \diamond 0)) \diamond 0)$
• $1 \diamond (0 \diamond 1)$: $0 \diamond ((1 \diamond (0 \diamond 1)) \diamond 1)$
• $1 \diamond (1 \diamond 1)$: $1 \diamond ((1 \diamond (1 \diamond 1)) \diamond 1)$
• $1 \diamond (2 \diamond 1)$: $2 \diamond ((1 \diamond (2 \diamond 1)) \diamond 1)$
• $2 \diamond (0 \diamond 1)$: $0 \diamond ((2 \diamond (0 \diamond 1)) \diamond 2)$
• $2 \diamond (1 \diamond 2)$: $1 \diamond ((2 \diamond (1 \diamond 2)) \diamond 2)$
• $2 \diamond (2 \diamond 2)$: $2 \diamond ((2 \diamond (2 \diamond 2)) \diamond 2)$

[Hernan Ibarra]

Daniel Weber said:

In fact it even implies $x \diamond y = y$

Do you mind sharing the proof? I don't see it

[Hernan Ibarra]

Joachim Breitner said:

Is the rule (yx)(yx) -> x confluent, by a similar argument as 477? Probably not exactly the same argument, as it can apply on its own lhs's subterms, can it? But only if y = x, so maybe that helps with a (more complicated) confluence proof.

Yeah I thought it might be confluent for a similar reason but I haven't worked out the details yet

[Joachim Breitner]

Let's see. A term that can be rewritten in two (not independent) places has to be ((yx)(yx))((yx)(yx)). So the critical pair consists of (xx) if I apply the nested occurrences, and (yx) if I rewrite on the outside. Doesn't look confluent to me, I fear.

[Kevin Buzzard]

Terence Tao said:

OK, trying again, this time with a general linear operation x ◇ y = ax+by. If I have calculated things correctly, Equation 65 becomes the system a(1+b^2)=0, b(a+b^2)=1, and Equation 359 becomes a(a+b-1)=0. Oh, interesting, here it does seem that again the former implies the latter. If a=0 this is clear, otherwise we have 1+b^2=0 and b(a+b^2)=1, and on multiplying the latter by b and substituting b^2=-1 we get after some algebra a+b-1=0. OK, this explains why this wasn't picked up by the linear magma sweep.

This argument assumes that the base ring has no zero divisors ("if a=0...otherwise we have 1+b^2=0...") so it occurred to me that there was a little leeway here, but annoyingly even without this assumption the implication still holds:

import Mathlib.Tactic

example (R : Type) [CommRing R] (a b : R) (h1 : a * (1 + b * b) = 0)
    (h2 : b * (a + b * b) = 1) : a * a + a * b = a := by
  polyrith -- Try this: linear_combination (b ^ 2 + a - 1) * h1 - 1 * a * b * h2

[Daniel Weber]

Hernan Ibarra said:

Daniel Weber said:

In fact it even implies $x \diamond y = y$

Do you mind sharing the proof? I don't see it

Vampire found it:
By using equation 65 with $x := b \diamond a \diamond b, y := a$, $b \diamond a \diamond b = a \diamond (b \diamond a \diamond b) \diamond a \diamond (b \diamond a \diamond b) = (a \diamond b \diamond a \diamond b) \diamond (a \diamond b \diamond a \diamond b)= b \diamond b$.
Now by equation 65 $(a \diamond b) \diamond c \diamond (a \diamond b) \diamond c = c$, so $c = a \diamond b \diamond (c \diamond a) \diamond b \diamond c = a \diamond b \diamond b \diamond c = a \diamond (b \diamond a \diamond b) \diamond c = b \diamond c$

[Kevin Buzzard]

Pace Nielsen said:

Using a map of the form x⋄y=ax+by+c, leads to the set of equations ba+b^3=1, a+b^2a=0, and a^2+ab\neq a. It turns out these are inconsistent over noncommutative rings. So no affine map with work over coefficients from a ring.

Oh in fact Pace was one step ahead of me :-) (although I only checked commutative rings)

[Daniel Weber]

$(y \diamond x) \diamond (y \diamond x) = x$ together with 65 also implies 1491 :cry:

[Daniel Weber]

The equations that 65 doesn't imply, and together with it they still don't seem to imply 1491, are:

['Equation3076', 'Equation2053', 'Equation2054', 'Equation3078', 'Equation2567', 'Equation2060', 'Equation2063', 'Equation4629', 'Equation2584', 'Equation4121', 'Equation4636', 'Equation3105', 'Equation2088', 'Equation3115', 'Equation49', 'Equation2097', 'Equation2098', 'Equation4146', 'Equation4658', 'Equation4157', 'Equation4158', 'Equation4165', 'Equation3142', 'Equation73', 'Equation2125', 'Equation3667', 'Equation1109', 'Equation1112', 'Equation3675', 'Equation2660', 'Equation2670', 'Equation1648', 'Equation2672', 'Equation1654', 'Equation1655', 'Equation632', 'Equation1657', 'Equation124', 'Equation639', 'Equation2699', 'Equation2700', 'Equation1682', 'Equation1684', 'Equation1685', 'Equation2709', 'Equation669', 'Equation670', 'Equation159', 'Equation676', 'Equation677', 'Equation3749', 'Equation167', 'Equation679', 'Equation3752', 'Equation704', 'Equation1728', 'Equation706', 'Equation2243', 'Equation707', 'Equation4293', 'Equation3271', 'Equation713', 'Equation1229', 'Equation1231', 'Equation3279', 'Equation2263', 'Equation1241', 'Equation4321', 'Equation3308', 'Equation2804', 'Equation2293', 'Equation3318', 'Equation2300', 'Equation261', 'Equation1285', 'Equation263', 'Equation1288', 'Equation273', 'Equation3353', 'Equation2330', 'Equation1312', 'Equation2337', 'Equation1315', 'Equation2853', 'Equation2855', 'Equation1322', 'Equation1840', 'Equation2865', 'Equation2866', 'Equation819', 'Equation4405', 'Equation4406', 'Equation1848', 'Equation825', 'Equation1850', 'Equation2875', 'Equation2873', 'Equation833', 'Equation1860', 'Equation3925', 'Equation2902', 'Equation4442', 'Equation1885', 'Equation2910', 'Equation872', 'Equation1897', 'Equation879', 'Equation3952', 'Equation882', 'Equation2939', 'Equation4480', 'Equation385', 'Equation1922', 'Equation906', 'Equation907', 'Equation2447', 'Equation2449', 'Equation2450', 'Equation1428', 'Equation917', 'Equation3481', 'Equation1434', 'Equation2460', 'Equation1444', 'Equation1451', 'Equation429', 'Equation1454', 'Equation437', 'Equation3519', 'Equation1479', 'Equation1482', 'Equation2506', 'Equation1488', 'Equation1489', 'Equation466', 'Equation473', 'Equation476', 'Equation3548', 'Equation2531', 'Equation3555', 'Equation2533', 'Equation4071', 'Equation1518', 'Equation3056', 'Equation3058', 'Equation4083', 'Equation1526', 'Equation4599', 'Equation504', 'Equation3066', 'Equation2043', 'Equation3068', 'Equation3069', 'Equation4606', 'Equation511']

[Will Sawin]

Kevin Buzzard said:

Oh in fact Pace was one step ahead of me :-) (although I only checked commutative rings)
````
A tricky thing about commutative rings is any relation of the form "this equation holds but this one doesn't" that holds in a commutative rings with finitely many generators holds already in a happens for finite commutative rings (since these rings inject into the product of their finite quotients). So already knowing there are no finite counterexamples tells you you won't be able to make a counterexample with commutative algebra.

[Terence Tao]

Inspired by @Daniel Weber Vampire-driven exploration of the "Asterix" law 65 under the hypothesis    0 ◇ 1 = 0 ◇ 2, I conducted by hand an exploration of the variant hypothesis 0 ◇ 0 = 0 ◇ 1 = 0 (with 0,1 distinct) and managed slightly more than half of an infinite multiplication table filled out. Not sure what to make of this, so I thought I'd record what I had here.

I'm going to write $L_y x = y \diamond x$ for the left-multiplication operators, so 65 becomes $x = L_y L_x L_y x$, and our hypothesis is that $L_0 0 = L_0 1 = 0$. If we define $2 := L_1 0$, then we have $1 = L_0 L_1 L_0 1 = L_0 2$, thus $L_0 2 = 1$ (so in particular 2 is distinct from 0,1). If we then define $3 := L_2 1$, then $2 = L_0 L_2 L_0 2 = L_0 3$, so $L_0 3 = 2$ (so in particular 3 is distinct from 0,1,2). Continuing in this fashion, we obtain distinct elements $0,1,2,\dots$ in the magma with
$L_0 (n+1) = n$ and $L_{n+1} n = n+2$ for $n=0,1,\dots$.

Next, we have $0 = L_1 L_0 L_1 0 = L_1 L_0 2 = L_1 1$, thus $L_1 1 = 0$. Then $1 = L_1 L_1 L_1 1 = L_1 2$, so $L_1 2 = 1$. $2 = L_1 L_2 L_1 2 = L_1 L_2 1 = L_1 3$, so $L_1 3 = 2$. By induction we see that $L_1 n = n-1$ whenever $n \geq 1$.

In a similar vein, $1 = L_2 L_1 L_2 1 = L_2 L_1 3 = L_2 2$, so $L_2 2 = 1$; $2 = L_2 L_2 L_2 2 = L_2 L_2 1 = L_2 3$, so $L_2 3 = 2$; and by induction $L_2 n = n-1$ whenever $n \geq 2$.

A further induction now tells us that $L_m n = n-1$ when $m \geq 0$ and $n \geq m, 1$, and we had also previously established $L_m (m-1) = m+1$ when $m \geq 1$. That's about half of the multiplication table on $0,1,2,\dots$ (the upper-triangular region and one lower diagonal). I have had trouble filling in the rest of the table, though, which may be a good sign since perhaps these hypotheses are in fact contradictory.

[Daniel Weber]

Vampire can't find a contradiction to this

[Daniel Weber]

Looking at the quotient of the free magma by the rules you describe, Vampire found the following equivalence classes which aren't found by the multiplication table:

• $0$: $2 \diamond (0 \diamond (2 \diamond 0))$, $0 \diamond (2 \diamond (0 \diamond (2 \diamond 0)))$, $(2 \diamond (0 \diamond (2 \diamond 0))) \diamond 0$, $(2 \diamond (0 \diamond (2 \diamond 0))) \diamond 1$
• $2$: $1 \diamond (2 \diamond (0 \diamond (2 \diamond 0)))$
• $0 \diamond (2 \diamond 0)$: $2 \diamond ((0 \diamond (2 \diamond 0)) \diamond 0)$

[Daniel Weber]

What happens if you set all values not described by $L_m n = n-1, L_{m}(m-1) = m+1$ to 0? It seems to work here

[Daniel Weber]

No, $L_4 L_1 L_4 1 \ne 1$ then

[Daniel Weber]

I can try to fill values for the multiplication table with Vampire, each time setting it to the smallest value which doesn't let it derive a contradiction, and maybe it'd get stuck (which would mean we have to use values outside of $\mathbb{N}$) or we'd spot a pattern

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

For the record, I tried a similar approach a couple of days ago without spotting a pattern. My issue was that I could go really quite far before reaching a contradiction even when I filled in the table in a commutative way. But we know that commutativity together with 65 implies left-cancellativity, so eventually continuing that particular table should become impossible. It just takes longer than my patience and computational capability extended.

[Daniel Weber]

It makes this
| * | 0 | 1 | 2 | 3 |
|---|---|---|---|---|
| 0 | 0 | 0 | 1 | 2 |
| 1 | 2 | 0 | 1 | 2 |
| 2 | 0 | 3 | 1 | 2 |
| 3 | 0 | stuck | none | none |

[Terence Tao]

Hmm, perhaps one has to extend the domain beyond the natural numbers then. Here is a possible "translation-invariant" ansatz. Let G be an abelian AddGroup, and consider a magma operation on G of the form y ◇ x = x + f(x-y) for some function f : G → G. If I have computed correctly, Equation 65 then simplifies to the functional equation

f(h) + f(f(h)) + f(h + f(h) + f(f(h))) = 0 (*)

for all h : G. Left-cancellability corresponds to the injectivity of h ↦ h + f(h). (This function is necessarily surjective, since it will map h + f(h) + f(f(h)) to h thanks to (*).)

The partially filled multiplication table above corresponds to trying to work out f on the integers, and getting as far as f(h) = -1 for h ≥ 0 and f(-1) = 2. This verifies (*) for all h ≥ -1. Not sure how to fill out the rest of f though.

[EDIT: This so looks like an Olympiad problem. Time to ping Deepmind?]

[Kevin Buzzard]

I must confess that I spent some time two days ago pinging some ATP experts about this particular problem, but warned them that smart people had already been throwing some of their favourite toys at it. Clearly desperation is setting in! That comment above about "I wonder if it's independent of ZFC" is more evidence of this :-)

[Thomas Browning]

Perhaps I'm missing something, but if x ◇ y = x + f(x - y), then equation 65 seems to become
x = y ◇ (x ◇ (y ◇ x))
= y + f(y - (x ◇ (y ◇ x)))
= y + f(y - (x + f(x - (y ◇ x))))
= y + f(y - (x + f(x - (y + f(y - x))))
so
y - x + f(y - x - f(x - y - f(y - x))) = 0
or equivalently,
h + f(h - f(-h - f(h))) = 0
but I don't see how this relates to (*).

[Terence Tao]

So sorry! I had written x ◇ y where I should have written y ◇ x (it's the same ansatz, but represented differently; I've edited my previous post). The calculation is as follows: if x = y + h, then
y ◇ x = x + f(h)
x ◇ (y ◇ x) = x + f(h) + f(f(h))
y ◇ (x ◇ (y ◇ x)) = x + f(h) + f(f(h)) + f(h+f(h)+f(f(h)))
and so equation 65 becomes
f(h) + f(f(h)) + f(h+f(h)+f(f(h))) = 0.

Also we have y ◇ (y+h) = y + h + f(h) so left-cancellability is equivalent to injectivity of h + f(h).

I experimented with some other ways to represent the ansatz, but this one leads to the simplest-looking equations as far as I can tell. Your version is equivalent; I think what you call f(h), I would call f(-h)-h.

[Joseph Myers]

Terence Tao said:

Hmm, perhaps one has to extend the domain beyond the natural numbers then. Here is a possible "translation-invariant" ansatz. Let G be an abelian AddGroup, and consider a magma operation on G of the form y ◇ x = x + f(x-y) for some function f : G → G. If I have computed correctly, Equation 65 then simplifies to the functional equation

f(h) + f(f(h)) + f(h + f(h) + f(f(h))) = 0 (*)

for all h : G. Left-cancellability corresponds to the injectivity of h ↦ h + f(h). (This function is necessarily surjective, since it will map h + f(h) + f(f(h)) to h thanks to (*).)

The partially filled multiplication table above corresponds to trying to work out f on the integers, and getting as far as f(h) = -1 for h ≥ 0 and f(-1) = 2. This verifies (*) for all h ≥ -1. Not sure how to fill out the rest of f though.

[EDIT: This so looks like an Olympiad problem. Time to ping Deepmind?]

I don't think these values of f can extend to the rest of the integers, though I haven't formalized my argument or spent very long checking it, so it shouldn't entirely be trusted to be correct (and there might be unnecessary pieces in it as well).

Say h < -1. If f(h) = 1 then (*) reduces to f(h) = 0, contradiction. If f(h) = 0 then (*) reduces to f(h-1) = 1, contradiction. If f(h) = -1 then f(h+1) = -1 and repeating you end up with f(-1) = -1, contradiction. And if f(h) = 2 then f(h+1) = -1, contradiction. So f(h) is not in the interval from -1 to 2 for any h < -1. So either f(h) <= -2 or f(h) >= 3; in the latter case, f(h + f(h) - 1) = 1 - f(h) <= -2, so h + f(h) - 1 <= -2, so h + f(h) <= -1, which is also trivial when f(h) <= -2. So f(h) + h <= -1 for all h < -1. In particular, f(-2) <= 1 so f(-2) <= -2.

Now consider the function t(x) = x + f(x) discussed above, for which it was noted that t(h + f(h) + f(f(h))) = h; replacing f(h) + f(f(h)) by t(f(h)) = t(t(h)-h), we have t(h + t(t(h) - h)) = h for all h. We had above that t(h) <= -1 for all h < -1.

In this equation t(h + t(t(h) - h)) = h, substitute h = x + t(t(x) - x) so that t(h) = x; we get t(x + t(t(x)-x) + t(-t(t(x)-x))) = x + t(t(x)-x). Take some x such that f(x) = t(x)-x < -1 (we know that x = -2 has this property). Then t(t(x)-x) <= -1, so -t(t(x)-x) >= 1, so t(-t(t(x)-x)) = -t(t(x)-x) - 1, so t(x - 1) = x + t(t(x)-x) <= x - 1, so t(x - 1) - (x - 1) <= 0. As t(x - 1) - (x - 1) = f(x - 1), it cannot be 0 or -1, so f(x - 1) < -1. Inductively, f(x) < -1 for all x < -1. But then the LHS of (*) is negative for all such x, a contradiction.

[Terence Tao]

Huh, that's quite an intricate argument! The problem here is an immediate specialization of the "65 -> left cancellability" problem, so if this is the simplest proof available for this special case, then it strongly suggests that the general problem is also at least this complicated to prove. So perhaps it is worth trying to find a more streamlined proof. And the argument may be specific to one dimension (certainly the proof uses the total ordering of the integers quite a bit!); if one works with larger groups, e.g., Z^2, then maybe the equation becomes solvable again.

Will have to think about this more...

[Daniel Weber]

In the other direction (1491 -> 65), the question is whether $L_y$ has to be surjective (and because it has to be injective, that implication also holds in finite models)

[Daniel Weber]

This means that there's a function $f$ such that $L_y f(y, x) = x$. Does completeness imply that if such an $f$ always exists then it's just an evaluation of some fixed term in the free magma over $x, y$?

[Daniel Weber]

Ah, never mind, $f(y,x) = L_x L_y x$ works iff 1491 implies 65, so that's not interesting

[Terence Tao]

I don't think the completeness theorem can handle existential statements very well, it's just something special about 65 and 1491 that they relate to the surjectivity and injectivity of left-multipication somehow.

This is a very minor comment, but the original law 359 in this thread corresponds in the above model to $f(-f(0))=0$. 1491 corresponds to something messier (if I computed correctly, it is $f(h) + f(h+f(h)) + f(f(h+f(h)))=0$ but I am not 100% sure of this). This pair of equations (65 and 1491) are such weird equations: tantalisingly close to being understandable, but not connected as far as I can tell to any more standard mathematical structure...

[Terence Tao]

I think I was able to show that there are functions $f: {\mathbf Z} \to {\mathbf Z}$ obeying the Asterix functional equation $f(h) + f(f(h)) + f(h+f(h)+f(f(h)))=0$ for which $h \mapsto h+f(h)$ is not injective; this shows that indeed 65 does not imply 1491. The basic idea is to build the function greedily: every time one needs to decide what value $f(h)$ has to be, select some number much larger than all previous numbers so that no collisions occur. It gets more technical than this because when one selects the value of $f$ at $h$, one also has to select the value of $f$ at some related locations such as $f(h)$ and $h+f(h)+f(f(h))$, but this can be done by a somewhat technical induction. I wrote up the details at equational#453 and it should appear in the blueprint shortly.

The same method should also resolve the other anti-implications involving 65 or 1491. I'm going to sleep now, but tomorrow I can try to set out specific Lean formalization tasks to make this (somewhat complicated) proof completely verified (in this particular case this is important because there are a lot of fiddly details with the induction, even though the idea is broadly clear).

[Daniel Weber]

I'll start working on formalizing it

[Daniel Weber]

In Lemma 7.2, when you choose an element $h_2 \in \mathbb{Z}$ such that $h_2, h_0 + h_1 + h_2$, and $- h_1 - h_2$ are all distinct and lie outside of $E_2$, the finiteness of $E_2$ isn't enough, you also need $h_0 + h_1 \ne 0$. In the first case I understand how to get that, as you choose $h_1$, but I'm not certain how to obtain that in the second and third cases.

[Daniel Weber]

I think adding the requirement that $f(x) \ne -x$ to the definition of a partial solution and requiring $0 \in E_0$ in Lemma 7.2 fixes it?
EDIT:
ah, but you can't get that in Corollary 7.4, in fact, $f(f(0) + f^2(0)) = -(f(0) + f^2(0))$ necessarily.
What about setting $f(0) = 0$ and requiring $f(x) \ne -x$ for other values of $x$? I think that works, I'll try to continue with the formalization

[Daniel Weber]

Here's a slight simplification of Lemma 7.2:
The core operation is moving an element from $E_1 \setminus E_0$ to $E_0$. This is the second part of the existing lemma, unchanged.
For an element $h \in \mathbb{Z} \setminus E_2$ we first add it to $E_1$, by choosing some arbitrary $h' \notin E_2 \cup \{h, -h\}$ and adding it to $E_2$ and setting $f(h) = h'$. Then we move $h$ from $E_1$ to $E_0$.
For an element $h \in E_2 \setminus E_1$ it must be $f(h')$ for some $h' \in E_1 \setminus E_0$. We first move $h'$ to $E_0$ and observe that this moved $h$ to $E_1 \setminus E_0$, so we can now move it to $E_0$.

[Terence Tao]

You're right, one should modify the notion of a partial solution by requiring $0 \in E_0$ and $h + f(h) \neq 0$ for all $h \in E_1 \backslash E_0$. Then one should modify the iteration a little bit to ensure the latter property propagates with the iteration.

As you note, one can seed the iteration with a situation in which $0 \in E_0$ and $f(0) = 0$ to get the iteration going, but one downside of that is that one only contradicts the Obelix equation and not the various single-variable equations downstream of that equation. However, I think one can seed the iteration also with a more complicated initial solution in which $f(0) \neq 0$ and things should still work (haven't checked this though).

I like your proposal to simplify the third case of Lemma 7.2 by first introducing a one-step version of the lemma.

I was initially thinking of breaking up the task of formalizing Section 7 into small pieces and distributing the proof out to different volunteers, but it sounds like you feel like you could do the entire thing, so I created a large task equational#463 to formalize the entirety of 65 !=> 1491 and also update the blueprint accordingly to implement the corrections and improvements you indicated above. If you would prefer to only perform a portion of the formalization / blueprint maintainance task, let me know and I will split the task into smaller pieces instead.

[Terence Tao]

I am optimistic that this method can also rule out the other unknown implications involving 65. I could set an explicit task for that as well, but perhaps the ongoing discussion here will resolve these organically? If you would like to informally claim one of these other tasks, you can "claim" it here and then I will set up a more official task in Github later.

[Terence Tao]

By the way, in case it helps, my conceptual model of the proof is that we are filling in the entries of f(h) for various h a few entries at a time, similar to solving a Sudoku puzzle; we are relying on the infinite nature of the puzzle to avoid getting "stuck". At any given point in the process, we will have a partially solved puzzle, with different type of numbers. The elements h of $E_0$ are the "completely analyzed numbers": enough of the function has been determined that one can verify the Asterix functional equation for this choice of input h. The elements h of $E_1 \backslash E_0$ are the "partially analyzed numbers": we have f(h) determined, but not enough of the rest of the function to resolve the Asterix equation here (but we have the capability to do so, by filling out a few more entries of the f function table). The elements h of $E_2 \backslash E_1$ are the "numbers of interest"; they have not yet had a value of f(h) assigned to them, but have been selected as the output f(h') of some other partially analyzed number h', and so are already slightly (but not excessively) constrained as to what values they can take. Everybody else in ${\mathbf Z} \backslash E_2$ is an "uncontacted number" - this is an infinite pool of numbers that we can draw from to keep filling out our function.

The whole procedure reminds me of the technique of forcing in model theory, from what I have gathered about that technique over the years. I have had it on my "to do" list for some time to actually learn this technique; now I have some impetus to do so.

[Pace Nielsen]

This idea may be half-baked, but I thought I'd share it anyway.

Instead of restricting $f$ to be defined on $\mathbb{Z}$, let's just define it on a general ring, and further assume it is linear $f(x)=ax+b$. Then the Asterix functional equation becomes

$$(a^3+2a^2+2a)x+(a^2b+3ab+3b)=0.$$

Working in characteristic 3, this system works out to just say $a^3=a^2+a$ and $ab=0$. The map $x\mapsto x+f(x)$ is not injective: both $0$ and $-b$ map to zero.

By taking $b^2=0$, and $ba=ab$, we have a finite commutative ring. So this should give a finite counterexample (of size 81). (Hopefully I didn't make a silly mistake.)

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

We know that finite models of 65 are left-cancellative. Or am I misunderstanding what you're saying when you write that there should be a finite counterexample of size 81?

[Will Sawin]

The problem is that a^3 =a^2+a forces a to be invertible (the inverse is a^2-a-1) and so ab=0 implies b=0.

[Will Sawin]

I had a different idea related to defining f on a general abelian group. It seems the argument works without modification for an arbitrary countable abelian group. This suggests the following modification: Work on the free abelian group on infinitely many generators. Any time the argument asks us to pick an element outside some finite set, pick a new generator. Then we can label each generator by a label that expresses which step it was constructed on and which elements were used to construct it. Now it seems like the argument is producing some kind of free algebra with operations f, - and proving that various elements of the algebra are distinct. Then maybe it's possible to rephrase the argument in terms of the structure of the free algebra, without making choices, and maybe as proving some kind of confluence-like property?

[Pace Nielsen]

Will Sawin said:

The problem is that a^3 =a^2+a forces a to be invertible (the inverse is a^2-a-1) and so ab=0 implies b=0.

Not in a general ring. For instance, these equations are consistent with taking $a=0$ and $b=1$.

Perhaps the issue with my argument is it doesn't force $f$ to be surjective. (And cannot, on pain of the problem you mention.)

[Will Sawin]

Pace Nielsen said:

Not in a general ring. For instance, these equations are consistent with taking $a=0$ and $b=1$.

Oh sorry, that was silly of me. The problem is with the claim that both $0$ and $-b$ map to $0$, since $0$ maps to $0 + a0+b = b$.

[Daniel Weber]

Will Sawin said:

I had a different idea related to defining f on a general abelian group. It seems the argument works without modification for an arbitrary countable abelian group.

You need $x + x = a$ to have coinfinitely many solutions for any $a$, if you don't modify the argument (to find $h_2$ with $h_2 + h_2 \ne -h_0 -2h_1$)

[Terence Tao]

I certainly think we will need to figure out how to abstract this approach if we are to scale it to the hopefully dozens of other equations out there for which a similar method can apply. I agree with @Will Sawin that it does feel like some sort of "additive confluence" type of property, and that the free abelian group with countably many generators is actually the most natural domain to work in (in fact I had an early draft of the argument using exactly this group, but decided halfway to switch to the integers to make the proof look less scary from a notational perspective. [Actually I had an intermediate stage where I was working with a torsion-free infinite abelian group, with the torsion-free hypothesis needed to avoid the characteristic 2 issue @Daniel Weber just pointed out, but at that point I just decided that the integers were good enough.]

By the way if we do end up having a lengthy human-written proof of all the anti-implications involving Asterix and Oberlix, this would be a good test case for the duality metatheorems that we are making progress on formalizing in Lean, because I can imagine it would be a pain to manually dualize all of those human written proofs to settle the anti-implications involving dual-Asterix and dual-Oberlix.

[Terence Tao]

By the way, I wanted to note that the final (hopefully) working proof of the anti-implication 65->1491 was either directly or indirectly inspired by a lot of the previous discussion; definitely a collaborative effort, in the spirit of past Polymath projects!

For instance, @Daniel Weber 's Vampire explorations suggested that a collision in left-cancellability was only generating a very sparse set of additional relations, not enough to create a contradiction, so this hinted that one could "outrun" these relations on an infinite magma (and we knew early on that the magma had to be infinite). On the other hand, we had this partial solution on the integers which had the translation invariant structure that suggested the useful translation-invariant ansatz reducing things to a univariate functional equation; but as @Joseph Myers worked out, the infinite number of values that this partial solution already fixed made it impossible to complete the rest of the function. This helped give me the insight that one should only fix a finite number of values of the function at a time, so as not to run into these sorts of obstructions. Last, but not least, the negative results (by @Will Sawin, @Pace Nielsen , and others) showing that the ring-theoretic constructions were not working were important in order to allow me to finally let go of these ideas and pursue the more combinatorial approach that ended up being more fruitful.

So, a rather chaotic narrative with many twists and turns, but actually this is how many actual solutions of research-level problems happen - our published papers largely only describe (in a very polished fashion) the one approach that ended up working, but there are usually a half-dozen or more failed (or partially failing) approaches which preceded that approach, and in fact were essential to identifying and then implementing the one approach that could actuallywork.

[Pace Nielsen]

Thanks go to Will Sawin for finding my previous error.

Fortunately, I think the main idea can be salvaged and extended into a possibly workable automation scheme, as follows.

Instead of using a linear $f$, make it quadratic, say (for simplicity) of the form $f(x)=ax^2+bx$. (The intuitive idea here is that it should be easier to make quadratics non-injective.) After some experimentation, it seems that working over a ring of characteristic $3$ makes things more workable. (Also, we may force $a$ and $b$ to commute, for convenience.) Then, if I didn't make any mistakes, we get a reduction system $ba\mapsto ab$, $a^2\mapsto 0$, $ab^2\mapsto ab+a$, and $b^3\mapsto b^2+b$. To ruin injectivity we adjoin two more symbols $u,v$ where $u+f(u)=v+f(v)$. Working out a reduction system, we get another five reductions $av\mapsto au$, $abv\mapsto abu$, $auv\mapsto u-v+bu-bv+au^2$, $abuv\mapsto bu-bv+b^2u-b^2v+abu^2$, and $b^2v\mapsto v-u+bv-bu+b^2u$.

Since $u$ and $v$ are unaffected by these reductions, they are distinct. (Interestingly, if we make $vu=uv$ we are forced to get $u=v$, so noncommutativity is quite important here.)

[Terence Tao]

I see. So basically you are using a quadratic ansatz to convert an intractable word problem to a ring reduction problem that might conceivably be proven to have good properties by existing methods from noncommutative ring theory (this is not my field (ha!), but it looks vaguely like you are implementing some noncommutative version of a Grobner basis?). It sounds like such counterexamples are going to be necessarily infinite, which is good as it gets around the objection that no counterexamples are possible in the finite setting.

[Pace Nielsen]

Terence Tao said:

I see. So basically you are using a quadratic ansatz to convert an intractable word problem to a ring reduction problem that might conceivably be proven to have good properties by existing methods from noncommutative ring theory (this is not my field (ha!), but it looks vaguely like you are implementing some noncommutative version of a Grobner basis?). It sounds like such counterexamples are going to be necessarily infinite, which is good as it gets around the objection that no counterexamples are possible in the finite setting.

Yes, that is exactly right. I'm using a noncommutative version of a Grobner basis computation (called the diamond lemma).

[Will Sawin]

Pace Nielsen said:

Thanks go to Will Sawin for finding my previous error.

Fortunately, I think the main idea can be salvaged and extended into a possibly workable automation scheme, as follows.

Instead of using a linear $f$, make it quadratic, say (for simplicity) of the form $f(x)=ax^2+bx$. (The intuitive idea here is that it should be easier to make quadratics non-injective.) After some experimentation, it seems that working over a ring of characteristic $3$ makes things more workable. (Also, we may force $a$ and $b$ to commute, for convenience.) Then, if I didn't make any mistakes, we get a reduction system $ba\mapsto ab$, $a^2\mapsto 0$, $ab^2\mapsto ab+a$, and $b^3\mapsto b^2+b$. To ruin injectivity we adjoin two more symbols $u,v$ where $u+f(u)=v+f(v)$. Working out a reduction system, we get another five reductions $av\mapsto au$, $abv\mapsto abu$, $auv\mapsto u-v+bu-bv+au^2$, $abuv\mapsto bu-bv+b^2u-b^2v+abu^2$, and $b^2v\mapsto v-u+bv-bu+b^2u$.

Since $u$ and $v$ are unaffected by these reductions, they are distinct. (Interestingly, if we make $vu=uv$ we are forced to get $u=v$, so noncommutativity is quite important here.)

This is a great way to understand what is going on mathematically with this example. Since the equation 65 without left cancellability cannot hold in any magma that embeds into a product of finite magmas, this must be a noncommutative ring that fails to embed into a product of finite rings. Understanding what this ring is and why it fails to embed into finite rings in ring-theoretic terms could be a way to understand the theorem and why it's hard in more traditional mathematical terms.

[Terence Tao]

This may indeed scale better than my combinatorial approach, especially if one can leverage any existing software packages for noncommutative Grobner basis computations. Is there some source you can recommend to learn more about this topic? (Or would it be faster to simply write a new chapter of the blueprint with a very abridged introduction to the diamond lemma etc.).

[Terence Tao]

Presumably the moment one has a noncommutative polynomial map which is injective but not surjective, or vice versa, it stops being able to be embeddable into a product of finite rings.

[Will Sawin]

Are you assuming a and b commute with u and v here? It looks like all the expressions have a and b on the left and u and v on the right. In that case we can make use of the fact that the ring F_3[b]/(b^3-b^2-b) splits into a product of F_3[b]/b and F_3[b]/(b^2-b-1) to reduce to assume b satisfies one of these two equations. The first one implies a=0 so probably the second one is the interesting one.

[Will Sawin]

Terence Tao said:

Presumably the moment one has a noncommutative polynomial map which is injective but not surjective, or vice versa, it stops being able to be embeddable into a product of finite rings.

Not for injective but not surjective. For example the ring F_2[x] has the squaring map which is injective but not surjective but embeds fine into a product of finite rings. Surjective but not injective, this works.

[Will Sawin]

Maybe it's clearer to say that I'm hoping for an answer that relates this ring to known infinite-dimensional rings, e.g. to Heisenberg algebras or universal enveloping algebras of infinite-dimensional Lie algebras or something like that.

[Terence Tao]

One of my hopes for this project was to uncover "Mathematics from Mars": exotic objects that have comparable levels of rich structure as the textbook mathematical objects, but were overlooked by anything that did not resemble a systematic search, because they were largely disconnected from the tree of known mathematics. I don't know whether Asterix and Obelix are genuinely Martian mathematical objects, or are actually highly disguised versions of mathematical objects that are actually already known to terrestrial mathematics, but I am looking forward to finding out either way!

[Pace Nielsen]

Terence Tao said:

This may indeed scale better than my combinatorial approach, especially if one can leverage any existing software packages for noncommutative Grobner basis computations. Is there some source you can recommend to learn more about this topic? (Or would it be faster to simply write a new chapter of the blueprint with a very abridged introduction to the diamond lemma etc.).

George Bergman's paper here is the standard reference to the diamond lemma. Rather than have you wade through the details, here is the quick gist. To tell whether or not a sequence of reductions resolves to a normal form, you essentially just need two things. First, you need a well-ordering where all reductions result in linear combinations of smaller monomials in the ordering. (In practice, just use the length-lexicographical order.) Second, you need to check that overlaps resolve to a common expression. By an overlap, I mean that if we have two reductions like $a^2b\mapsto a+b$ and $bc\mapsto 0$, then the expression $a^2bc$ could be reduced in two different ways (according to where you place parentheses), and we get $(a^2b)c=(a+b)c$ while $a^2(bc)=0$. So we get a new relation $ac+bc=0$. If all overlaps resolve, we have a system of reductions that yields a normal form.

I believe there are packages implementing this in Magma (and maybe others too).

[Terence Tao]

It's ironic that we haven't yet deployed Magma for this project

[Terence Tao]

I'm actually quite pleased to find out that there are two viable, but quite different, ways to analyze equation 65. We will hopefully be able to empirically start testing how well these two methods perform on the remaining unsolved implications. Will they have a comparable range of influence? Will one be better for one type of implication, and another better for a different type? This sort of experimental mathematics was another type of outcome I was hoping for with this project.

[Will Sawin]

Still assuming $a$ and $b$ commute with everything, saying the map $x \mapsto x+f(x)= x+bx+ax^2 = (1+b) x + a x^2$ fails to be injective is equivalent to the map $x \mapsto x + a x^2/(1+b)$ so after changing the definition of $x$ it seems that it suffices to demonstrate the existence of an $\mathbb F_9[a]/a^2$-algebra such that the map $x \mapsto x + ax^2$ is not injective.

[Will Sawin]

Although I'm a little worried because doesn't that map have an inverse $x \mapsto x - ax^2$?

[Pace Nielsen]

Will Sawin said:

Still assuming $a$ and $b$ commute with everything, saying the map $x \mapsto x+f(x)= x+bx+ax^2 = (1+b) x + a x^2$ fails to be injective is equivalent to the map $x \mapsto x + a x^2/(1+b)$ so after changing the definition of $x$ it seems that it suffices to demonstrate the existence of an $\mathbb F_9[a]/a^2$-algebra such that the map $x \mapsto x + ax^2$ is not injective.

It turns out that if one makes u and v commute with a and b, then again the reduction system forces u=v.

[Pace Nielsen]

(deleted)

[Will Sawin]

Pace Nielsen said:

Will Sawin said:

Still assuming $a$ and $b$ commute with everything, saying the map $x \mapsto x+f(x)= x+bx+ax^2 = (1+b) x + a x^2$ fails to be injective is equivalent to the map $x \mapsto x + a x^2/(1+b)$ so after changing the definition of $x$ it seems that it suffices to demonstrate the existence of an $\mathbb F_9[a]/a^2$-algebra such that the map $x \mapsto x + ax^2$ is not injective.

It turns out that if one makes u and v commute with a and b, then again the reduction system forces u=v.

So your calculations don't assume x commutes with a and b? Then why do all the formulas have a and b on the left?

[Pace Nielsen]

Arg, another error. Good point.

[Will Sawin]

One thing I observed is that if $f$ and $g$ are polynomials in a variable $x$ whose coefficients commute with $x$ and $f\circ g = \textrm{id}$ then $g\circ f = \textrm{id}$ since power series in $x$ with invertible constant term form a group under composition and hence left inverses are right inverses for them. So we can't use such polynomials for examples. But we don't assume the coefficients commute with $x$, it's hard to check any identity between the polynomials since we'll have lots of terms with different variables inserted between copies of $x$.

[Pace Nielsen]

Working over a commutative ring (so that evaluation of polynomials is a well-defined homomorphism!), I checked that if we take $f$ to be a quadratic polynomial solving the functional equation for Eqn65, then it also satisfies the functional equation for Eqn1491 (and vice versa). So no go here.

[Terence Tao]

Even if the noncommutative ring approach doesn't work for this particular equation, it's a good thing to keep in mind going forward. We still have 300 or so independent implications to resolve, and perhaps some of them will be amenable to this approach.

[Daniel Weber]

I finished formalizing Equation65_not_implies_Equation1491 successfully, now it just needs a bit of cleaning up

[Daniel Weber]

Should I try to make the resulting magma computable? That should be possible, but I'm not sure if it offers any benefits

[Daniel Weber]

I'll try to search for initial conditions to disprove all potential implications

[Daniel Weber]

I'm having trouble constructing partial solutions with $f(0) \ne 0$:
Let's say we have $f(0) = h_1, f(h_1) = h_2$. Then we must have $f(h_1 + h_2) = -(h_1 + h_2)$.
Due to $\forall x \in E_1 \setminus E_0, f(x) \ne -x$, this requires $h_1 + h_2 \in E_0$. Let $f(-(h_1 + h_2)) = h_3$.
Now we need $f(h_1 + h_2) + f^2(h_1 + h_2) + f(h_1 + h_2 + f(h_1 + h_2) + f^2(h_1 + h_2)) = 0$, that is $h_3 \in E_1$ and $f(h_3) = h_1 + h_2 - h_3$. Because $f(-(h_1 + h_2)) \in E_1$ we must have $-(h_1 + h_2) \in E_0$, which requires
$0 = f(-(h_1 + h_2)) + f^2(-(h_1 + h_2)) + f(-(h_1 + h_2) + f(-(h_1 + h_2)) + f^2(-(h_1 + h_2))) = h_1 + h_2 + f(0) = 2h_1 + h_2$, so $h_2 = -2h_1$. Because then $-(h_1 + h_2) = h_1$, this also implies $h_3 = h_2$, and we get
$f(0) = h_1, f(h_1) = -2h_1, f(-h_1) = h_1, f(-2h_1) = h_1$, which doesn't work because then $E_0 = \{-h_1, 0, h_1\}, E_1 = \{-2h_1, -h_1, 0, h_1\}, E_2 = \{-2h_1, -h_1, 0, h_1\}$, and $f$ isn't a bijection between $E_1 \setminus E_0$ and $E_2 \setminus E_1$

[Daniel Weber]

Can the conditions be weakened to allow for $f(0) \ne 0$?

[Pace Nielsen]

Daniel Weber said:

Can the conditions be weakened to allow for $f(0) \ne 0$?

If I understand what you are asking for, then yes, the following should work. Take the direct product of Terry's combinatorial example $f_1$ that you formalized with the function $f_2(h)=1$ in $\mathbb{F}_3$.

[Daniel Weber]

That works, but it isn't helpful for counterexamples as the $\mathbb{F}_3$ part is always ok

[Daniel Weber]

Daniel Weber said:

Can the conditions be weakened to allow for $f(0) \ne 0$?

You need to add $-2h_1$ to $E_0$, and then add $-3h_1$ to $E_1, E_2$ and you get $f(-3h_1) = h_1$, and then it has to be added to $E_0$, and so on and so forth, so $E_0$ has to be infinite. This is a generalization of the earlier $f(n) = \begin{cases} -1 & n \ge 0 \\ 2 & n = -1 \end{cases}$, which is stuck here, but perhaps in e.g. $\mathbb{Z} \times \mathbb{Z}$ it can continue, by generalizing the finiteness of $E_0, E_1, E_2$ to some kind of thinness condition. I'll try that

[Daniel Weber]

I got that working, but that doesn't actually refute 359, for instance. It needs $f(0) \ne f(-f(0))$, which $\begin{cases} -1 & n \ge 0 \\ 2 & n = -1 \end{cases}$ doesn't satisfy. Are there other such partial values of $f$?

[Daniel Weber]

Daniel Weber said:

I'm having trouble constructing partial solutions with $f(0) \ne 0$:
Let's say we have $f(0) = h_1, f(h_1) = h_2$. Then we must have $f(h_1 + h_2) = -(h_1 + h_2)$.
Due to $\forall x \in E_1 \setminus E_0, f(x) \ne -x$, this requires $h_1 + h_2 \in E_0$. Let $f(-(h_1 + h_2)) = h_3$.
Now we need $f(h_1 + h_2) + f^2(h_1 + h_2) + f(h_1 + h_2 + f(h_1 + h_2) + f^2(h_1 + h_2)) = 0$, that is $h_3 \in E_1$ and $f(h_3) = h_1 + h_2 - h_3$. Because $f(-(h_1 + h_2)) \in E_1$ we must have $-(h_1 + h_2) \in E_0$, which requires
$0 = f(-(h_1 + h_2)) + f^2(-(h_1 + h_2)) + f(-(h_1 + h_2) + f(-(h_1 + h_2)) + f^2(-(h_1 + h_2))) = h_1 + h_2 + f(0) = 2h_1 + h_2$, so $h_2 = -2h_1$. Because then $-(h_1 + h_2) = h_1$, this also implies $h_3 = h_2$, and we get
$f(0) = h_1, f(h_1) = -2h_1, f(-h_1) = h_1, f(-2h_1) = h_1$, which doesn't work because then $E_0 = \{-h_1, 0, h_1\}, E_1 = \{-2h_1, -h_1, 0, h_1\}, E_2 = \{-2h_1, -h_1, 0, h_1\}$, and $f$ isn't a bijection between $E_1 \setminus E_0$ and $E_2 \setminus E_1$

In fact, this shows that Equation 65 implies Equation 359 in translation-invariant magmas, and I suspect all of the relevant one variable equations

lemma Equation65_implies_Equation359_ti (f : G → G) (h : @Equation65 G (translationInvariant f)) :
    @Equation359 G (translationInvariant f) := by
  rw [Equation65_translationInvariant_iff] at h
  rw [Equation359_translationInvariant_iff]
  have v1 := h 0
  let h1 := f 0
  let h2 := f h1
  rw [zero_add, add_eq_zero_iff_eq_neg'] at v1
  change f (h1 + h2) = -(h1 + h2) at v1
  let h3 := f (-(h1 + h2))
  have v2 := h (h1 + h2)
  simp only [v1] at v2
  convert_to -(h1 + h2) + h3 + f h3 = 0 at v2
  · congr
    abel
  replace v2 : f h3 = h1 + h2 - h3 := by
    rw [← sub_eq_zero]
    convert v2 using 1
    abel
  have v3 : h3 + f h3 + f (_ + h3 + f h3) = 0 := h (-(h1 + h2))
  rw[ v2] at v3
  convert_to h1 + h2 + h1 = 0 at v3
  · congr 1
    abel
    congr 1
    abel
  change h1 = f (- h1)
  have v4 : -h1 = h1 + h2 := by
    rw [eq_comm, ← sub_eq_zero]
    trans h1 + h2 + h1
    abel
    exact v3
  rw [v4, v1, ← v4]
  abel

[Daniel Weber]

(deleted)

[Terence Tao]

Very interesting! So there is a limitation to the translation-invariant method. (Or, perhaps the 65 -> 359 implication is actually true!)

This is beginning to interact with the [recent disproof of 1661 -> 1657[(https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/1661.20-.3E.201657.20-.20another.20one.20bites.20the.20dust). In that construction, a "plain" translation-invariant magma did not work, but a finite modification of a (truncation of) the translation-invariant magma did work. I wonder to what extent the translation-invariant magma we constructed has the ability to be finitely modified, this could potentially be a way to resolve implications like 65->359 since 359 only has to fail at a single point.

Incidentally, upon reading up on the technique of forcing in model theory, I think the greedy algorithm used to construct the translation-invariant model is sort of a very simple version of forcing, which is about repeatedly adding "sufficiently generic" elements to one's model (in this case, a universe modeling ZFC) to achieve some specific law (one designed to have interesting consequences, e.g., the negation of the continuum hypothesis).

[Daniel Weber]

Could this induction be used directly to give values to the magma operation, without passing through translation-invariance?

[Daniel Weber]

For instance, say there are four right universes, $E_0 \subseteq E_1 \subseteq E_2 \subseteq E_3$. The operation is defined $f : E_0 \to E_2 \to E_3$, we want $f(x, e_0) \in E_1, f(x, e_1) \in E_2, f(x, e_2) \in E_3$ and $f(y, f(x, f(y, x))) = x$ for $x, y \in E_0$. I don't know what additional conditions are needed or how to add/move values

[Terence Tao]

Wish I had time to think about this today, this sounds like an interesting approach! The one observation I had is that this type of construction will not contain the previous translation invariant construction as a special case, but will be a different (though analogous) construction. But perhaps that's what's needed here. On the other hand, the fact that the equation is now bivariate instead of univariate suggests to me that there will be a lot more "coupling" between different equations, and one cannot independently tweak the values of f in some places without causing breakages in others, unless somehow one is very clever with how one sets up the induction (in particular, I wonder if one can even hope to make f as "injective as possible", subject of course to the non-injectivity caused by 65, and the minimal amount of non-injectivity required to break other laws )

[Daniel Weber]

Perhaps the pairs can be categorized based on how much of y * (x * (y * x)) is defined?

[Terence Tao]

That sound promising (it looks compatible with the translation-invariant construction).

One might also try this approach with the specialization
$f_{0,y} \circ f_{2,x} \circ f_{2,y}(x) = x$
$f_{1,y} \circ f_{2,x} \circ f_{0,y}(x) = x$
$f_{2,y} \circ f_{2,x} \circ f_{1,y}(x) = x$
$f_{1, f_{0,x}(x)}(x) \not \equiv f_{0,x}(x)$
of the problem introduced some days ago. The point here is that $f_{0,y}, f_{1,y}$ appear in these constraints relatively lightly, and so might be easily "forceable"; $f_{2,y}$ still appears a lot, but never three times in the same equation, and so maybe there is a bit more flexibility here.

Finally, it seems that your construction on ${\mathbb Z} \times {\mathbb Z}$, while it does obey 359, 1426, 4065, 614 actually contradicts 3862 and 817, if I computed correctly. So it does squeeze out two more anti-implications (and we get another two by duality).

[Daniel Weber]

Using $f_{i,y}(x) = x + f_i(x - y)$ could work there, perhaps? It gives $f_2(h) + f_2(f_2(h)) + f_0(h + f_2(h) + f_2(f_2(h))) = 0$, $f_0(h) + f_2(f_0(h)) + f_1(h + f_0(h) + f_2(f_0(h))) = 0$, and $f_1(h) + f_2(f_1(h)) + f_2(h + f_1(h) + f_2(f_1(h))) = 0$, and requires $f_1(-f_0(0)) \ne f_0(0)$

[Terence Tao]

I'll play with this later this evening. Certainly it can't be worse (from a logical strength perspective) than the vanilla Asterix functional equation, since it contains that one as a special case when $f_0=f_1=f_2=f$. On the other hand the previous obstruction that prevented $f(-f(0))=f(0)$ looks like it might no longer apply here, so it looks promising.

[Daniel Weber]

I think I managed to get it to work directly on the magma:

We define a partial solution using two finite sets $E_0 \subseteq E_1 \subseteq \mathbb{N} \times \mathbb{N}$, and a magma operation $f : E_1 \to \mathbb{N}$. For any $(y, x) \in E_0$ we want $(x, f(y, x)) \in E_1$, $(y, f(x, f(y, x))) \in E_1$, and $f(y, f(x, f(y, x))) = x$. For any $(y, x) \in E_1 \setminus E_0$ we want $(x, f(y, x)) \notin E_1$. Additionally, we want that for any $(y, x) \in E_1$ such that $f(y, x) = y$, we also have $(x, x) \in E_1$ and $f(x, x) = y$.

The main operation is adding a value to $E_1$. We add a pair $(y, x)$, setting $f(y, x)$ to some $z$ which is different from all values mentioned in the partial solution (and $x, y$). We'll also add $(z, z)$ and set $f(z, z) = y$.
$(z, z)$ can't violate any condition, and the only way $(x, y)$ violates a condition is some $(y', x') \in E_1 \setminus E_0$ having $x' = y, f(y', x') = x$.
We will push all of these values to $E_0$. That requires adding $(y', z)$ to $E_1$ and setting $f(y', z) = x' = y$. Adding $(y', z)$ isn't problematic because $(z, y) \notin E_1$, and $z$ isn't in the range of $f$. The third condition is only relevant if $y' = x' = y$, and then $f(z, z) = y$ takes care of it.

The only potential problem remaining is if $x = y'$, which causes the pair $(y, x)$ to break $(x, f(y, x)) \notin E_1$. That means $(x, y) \in E_1, f(x, y) = x$, and we have pushed it by setting $f(x, z) = y$. This lets us move $(y, x)$ to $E_0$, as then $f(y, f(x, f(y, x))) = f(y, f(x, z)) = f(y, y) = x$

[Terence Tao]

Nice! In order to understand your argument, I rewrote it as follows. Define a shift map to be a function from ${\mathbb N} \times {\mathbb N}$ to itself, such that the first coordinate of the output equals the second coordinate of the input. It is clear that such shift maps must take the form $(y,x) \mapsto (x, y \diamond x)$ for some magma operation $\diamond$, giving a one-to-one correspondence between shift maps and magmas. We say that a shift map has the Asterix property if, whenever one has a chain $(y,x) \mapsto (x,z) \mapsto (z,w)$ of shifts (i.e., $(y,x)$ shifts to $(x,z)$ and $(x,z)$ shifts to $(z,w)$), then we also have $(y,w) \mapsto (w,x)$. By unpacking the definitions, we see that a shift map has the Asterix property if and only if the corresponding magma operation obeys the Asterix law 65.

We make the following remark: if a shift map has the Asterix property, and $(x,y)$ shifts to $(y,x)$, then $(y,y)$ must also shift to $(y,x)$. Indeed, $(y,x)$ must shift to some $(x,z)$, then by the Asterix property applied to $(x,y) \mapsto (y,x) \mapsto (x,z)$, $(x,z)$ must shift to $(z,y)$; but then by the Asterix property applied to $(y,x) \mapsto (x,z) \mapsto (z,y)$ we obtain the claim. This remark helps motivate one of the conditions below.

To build shift maps, we define the notion of a partial shift map. This consists of two nested finite sets $E_0 \subseteq E_1 \subset {\mathbb N} \times {\mathbb N}$, and a shift map defined on $E_1$. Let's call pairs $(y,x)$ in $E_0$, $E_1 \backslash E_0$, and ${\mathbb N} \times {\mathbb N} \backslash E_1$ "green", "yellow", and "red" respectively (this is to invoke the standard traffic light colors). We require the following axioms:

• If $(x,y)$ is yellow, then its shift $(y,z)$ must be red.
• If $(y,x)$ is green, then its shift $(x,z)$ is green or yellow, leading to a chain $(y,x) \mapsto (x,z) \mapsto (z,w)$; furthermore, $(y,w)$ is green or yellow, and shifts to $(w,x)$.
• If $(x,y)$ is yellow and shifts to $(y,x)$, then $(y,y)$ must also be yellow and shift to $(y,x)$.

Now let $(y,x)$ be red. We would like to promote it to be either yellow or green. There are two cases.

CASE 1: It is not the case that $(x,y)$ is yellow and shifts to $(y,x)$. Let $(w_1,y),\dots,(w_n,y)$ be all the yellow pairs that shift to $(y,x)$ ($n$ can be zero). We pick a new natural number $z$ not previously encountered, promote the $(w_i,y)$ to green, promote $(y,x)$ to yellow (with shift $(x,z)$), and promote the $(w_i,z)$ to yellow (with shift $(z,y)$). One checks that this preserves all the axioms.

CASE 2: $(x,y)$ is yellow and shifts to $(y,x)$. This forces $x \neq y$ (since $(y,x)$ is red), and also that $(y,y)$ shifts to $(y,x)$. Let $(w_1,y),\dots,(w_n,y)$ the yellow pairs other than $(x,y)$ that shift to $(y,x)$. We pick a new natural number $z$, promote $(w_i,y), (y,x), (x,y), (y,y)$ to green, $(x,z), (y,z), (z,z)$ to yellow (with shift $(z,y)$), and the $(w_i,z)$ to yellow (with shift $(z,y)$). One checks that this preserves all the axioms.

One can now promote any yellow pair $(y,x)$ to green, by promoting its (necessarily red) shift $(x,z)$ to either yellow or green by the above procedure, which will turn $(y,x)$ as a byproduct.

To contradict 359, start with a partial shift map in which $(0,0)$ is yellow and shifts to $(0,1)$, $(1,0)$ is yellow and shifts to $(0,2)$, and all other pairs are red. This can be checked to be a partial shift map, and corresponds to a magma where $0 \diamond 0 = 1$ and $1 \diamond 0 = 2$, violating 359.

[Daniel Weber]

Should I add this proof to the blueprint? I finished the Lean formalization, equational#513

[Daniel Weber]

I wonder if this technique can be used to construct a model for equation 5105, perhaps just with translation invariance

[Daniel Weber]

I'll try to teach aesop to do the relevant case analysis, that should let us apply this method to other problems without too much pain

[Daniel Weber]

Here's a general framework of these kinds of forcing arguments:

• We have a partial definition of the magma operation.
• We consider the set of all instantiation of variables in the law. At the start, these will all be unevaluated, and as we define values for the magma operation we will evaluate these in the equations. Whenever we get $a \diamond b = c$ or $a = b \diamond c$ in this set we will take it from this set and move it to the magma definition.
• Whenever we add a value to the definition, we set it to a fresh value $z$, and we resolve this application to $z$ in all definitions.
• Now this is the tricky part: there might be definitions which now resolve to $a \diamond b = c$ or $a = b \diamond c$, and we need to add them to the magma definition, resolve them in other places, and show it doesn't lead to contradictions.
  • For equation 65, for example, this argument is: "suppose we're defining $x \diamond y = z$. If there was $a \diamond (x \diamond y) = x$ in the set of equations (i.e. $y = a \diamond x$) we get $a \diamond z = x$, so we add all of these. If there was $x \diamond (y \diamond (x \diamond y)) = y$ in the set of equations it will resolve to $x \diamond (y \diamond z) = y$, which is reduced unless $y = y \diamond x$, as then we've added $y \diamond z = x$, and to fix this we add the requirement $y \diamond x = y \to x \diamond x = y$ and define $z \diamond z = x$"

[Daniel Weber]

(deleted)

[Terence Tao]

Thanks for this explanation. Again, for my own understanding, I'm going to rephrase what you said in my own words.

We're basically trying to fill out a multiplication table on ℕ × ℕ like solving a Sudoku puzzle. A partially defined magma is like a partially solved Sudoku puzzle. For any partial state there are some obvious "moves" one can do to fill in more entries, by substituting in the already solved values into the laws of the game. For instance, if the Sudoku rules consist only of the Asterix law x = y ◇ (x ◇ (y ◇ x)), and one has already filled in 1 ◇ 2 = 3 and 2 ◇ 3 = 4, then one must also fill in 1 ◇ 4 = 2 from the x=2, y=1 specialization of the Asterix law. Of course, if you have already filled in 1 ◇ 4 to equal some other value, then you have lost the game. But let us say that a partial magma is "locally complete" if all the obvious moves one could accomplish in this fashion were already in your partial solution. So, for instance, in a locally complete partial solution to the Asterix law, if the partial solution already asserts that 1 ◇ 2 = 3 and 2 ◇ 3 = 4, then it must also assert that 1 ◇ 4 = 2. (More generally, local completeness for the Asterix law is equivalent to the assertion that whenever y ◇ x = z and x ◇ z = w, then y ◇ w = x.)

Let us say that a Sudoku ruleset (i.e., a set of laws, otherwise known as a "theory" in mathematical logic) is "greedily solvable" if, given any finite locally complete partial solution, and any relation a ◇ b not yet defined by that partial solution, there is a way to extend that solution to a larger finite locally complete partial solution, in such a way that a ◇ b is now defined. If we have this greedy solvability property, then a routine iteration (using some countable enumeration of ℕ × ℕ) shows that any finite locally complete partial solution can be extended to a global solution of the given ruleset.

There is an obvious way to try to establish greedy solvability: set a ◇ b equal to some natural number c that is novel (not equal to a or b, or any number already appearing in the finite partial solution), and attempt to complete it under obvious moves. If one can always avoid a contradiction when doing so, one has greedy solvability, hence the extension property, and one can then use this to build many useful models of one's ruleset to create anti-implications.

So, let's try to see if the Asterix law x = y ◇ (x ◇ (y ◇ x)) is greedily solvable. Suppose we have some partial solution, and we now want to extend it by imposing a ◇ b = c where c is novel. There can now be some obvious moves: if the partial solution already has y ◇ a = b for some y, then the x=a, y=y case of the Asterix law then forces y ◇ c = a. That does not directly create any contradictions because c is novel. However, if the partial solution has b ◇ a = b, then this argument forces b ◇ c = a, and then the x=b, y=a case of the Asterix law forces a ◇ a = b. This could lead to a contradiction if the partial solution already specified a ◇ a to equal some other value. So unfortunately the Asterix law, by itself, is not greedily solvable.

However, we can fix this by adding a new law to prevent this scenario. So now our Sudoku rule set consists of two rules: the first is the Asterix law x = y ◇ (x ◇ (y ◇ x)) for all x,y, and the second is the requirement that x ◇ x = y whenever y ◇ x = y. @Daniel Weber 's previous construction is then basically verifying that this rule set is greedily solvable: one can always add a new entry a ◇ b = c to a finite locally complete partial solution with a novel c. If one does not have b ◇ a = b, one has to add y ◇ c = a whenever y ◇ a = b; if one does have b ◇ a = b (and hence a ◇ a = b, by hypothesis), one also has to add a ◇ c = a and b ◇ c = a (by the first rule) and hence c ◇ c = a (by the second rule), and then a somewhat tedious check then verifies that one is now locally complete again.

I'll try later today to see if the laws 1076 and 73 that @Pace Nielsen resolved are also amenable to this technique. Another natural candidate is the Oberlix law 1491, since we still haven't resolved whether this implies the Asterix law. Hopefully this will shed some light on whether this process is automatable.

[Daniel Weber]

Here's a proof for 1491:
We will add two rules:
(1) if (y ◇ x) ◇ c = x then y ◇ (y ◇ x) is defined and equal to c
(2) x ↦ y ◇ x is injective for any y

Suppose we're setting a ◇ b = c, where c is a new value. The equation b = (a ◇ b) ◇ (a ◇ (a ◇ b)) will reduce to (*) b = c ◇ (a ◇ c) which is fine. If b = a ◇ x (there is a unique such x by (2)), there is also another equation x = (a ◇ x) ◇ (a ◇ (a ◇ x)) = b ◇ c and we need to set (a ◇ x) ◇ c = b ◇ c = x. This is OK with (1) by definition, and it's ok with (2) because if there was any (a ◇ x) ◇ d = x then by (1) a ◇ (a ◇ x) = a ◇ b would've been equal to d, but we assumed it was undefined.
If a = b = a ◇ x then (*) will further reduce to c ◇ x, so we need to add c ◇ x = b, which is ok with (2), and is ok with (1) because (a ◇ b) ◇ x = b and a ◇ (a ◇ b) = a ◇ c = b ◇ c = x

[Terence Tao]

One might need a bit more analysis here. If for instance we already have b = a ◇ x (so that we are forced to have x = b ◇ c) and we also already have b ◇ x = y for some y, then 1491 forces c = (b ◇ c) ◇ (b ◇ (b ◇ c)) = x ◇ y, so we have to add x ◇ y = c into the mix as well. In particular there would be a problem if x ◇ y were already set to some other value.

[Daniel Weber]

This represents the rule "if (a ◇ x) ◇ x = y then x ◇ y is equal to a ◇ (a ◇ x) (and if one isn't defined so is the other)", right?

[Terence Tao]

Ah, okay, I see now, thanks.

So now I guess we just need to find a partial solution to the above ruleset that violates the Asterix law...

[Daniel Weber]

Terence Tao said:

Ah, okay, I see now, thanks.

So now I guess we just need to find a partial solution to the above ruleset that violates the Asterix law...

Adding this rule might not be enough, as setting x * y will change more values, and it's possible that y = x * z, and it can continue like this, so one has to check that this can't generate contradictions

[Terence Tao]

Well, we don't need to actually add the Asterix law to the ruleset. We could start with say 1 ◇ 0 = 2, 0 ◇ 2 = 3, and 1 ◇ 3 = 4, which already violates Asterix (since 0 != 1 ◇ (0 ◇ (1 ◇ 0))), and see if anything is forced from this and your ruleset (1), (2) (and perhaps one also needs to add Oberlix itself to the ruleset, as it isn't quite implied by (1), (2) as far as I can tell, being sort of a converse to (1)). From a cursory glance it seems that nothing is forced from this, and so it should be possible to extend this three-entry partial multiplication table to a complete solution to Oberlix that also violates Asterix.

[Side note: the most natural name for a model that obeys Oberlix, but does not obey Asterix, would be "Dogmatix".]

[Daniel Weber]

I meant that the rule "if (a ◇ x) ◇ x = y then x ◇ y is equal to a ◇ (a ◇ x)" doesn't suffice to show that the multiplication table can be completed, as when using it you need to define x ◇ y = c, which implies more stuff just like setting a ◇ b = c previously did, and it's not obvious that this won't generate contradictions

[Terence Tao]

Ah, right, we need to revisit the analysis of your previous ruleset (1)+(2) to acccomodate the new rule, let's call it (3). (I had thought that (3) was just (1) in disguise but on closer inspection I see that it is a genuinely different rule.) If it doesn't close and it generates a lot more consistency conditions that then need to be added to the ruleset then this would indicate that this greedy approach is unlikely to be a good approach to construct Oberlix solutions.