Zulip Chat Archive
Stream: Equational
Topic: FINITE: 677 -> 255
Terence Tao (Dec 05 2024 at 18:53):
Creating a thread here for the last remaining unknown implication for the finite graph, whether 677 x = y ◇ (x ◇ ((y ◇ x) ◇ y))
implies 255 x = ((x ◇ x) ◇ x) ◇ x
.
We know remarkably little about this equation. @Pace Nielsen worked out that the solutions over a generic field to a linear model come in two flavors. Type 1: is negative a primitive 5th root of unity (i.e. a root of and (so it is a translation-invariant model). Type 2: is a root of and , which (as observed by @Ben Gunby-Mann) also implies (i.e., is a primitive root of unity). Unfortunately, for such models 255 factors as
The smallest non-trivial model is of order 5; this particular example is on .
Empirically, the magma cohomology approach seems to fail for this equation, but we do not have a satisfactory explanation as to why.
Douglas McNeil (Dec 05 2024 at 19:02):
I only know of four nontrivial examples in total for 677 and would love some more if anyone has any!
The minimal 5, 7a and 7b, and 11 .
All Latin squares, and some quick checks made it seem like the only diagonals which will satisfy 614 but violate 255 are also permutations of [0..n-1], but that was a little rushed the other day.
Ibrahim Tencer (Dec 05 2024 at 20:08):
Douglas McNeil said:
I only know of four nontrivial examples in total for 677 and would love some more if anyone has any!
The minimal 5, 7a and 7b, and 11 .
All Latin squares, and some quick checks made it seem like the only diagonals which will satisfy 614 but violate 255 are also permutations of [0..n-1], but that was a little rushed the other day.
What do you mean by nontrivial? It's easy to generate linear models, so are these all known to be non-linear? It seems difficult to characterize the linear models only using the magma operation.
Ibrahim Tencer (Dec 05 2024 at 20:28):
So at least in the Type 1 models we'll have . So if I understand correctly that means that the implication is immune to linear models.
Ibrahim Tencer (Dec 05 2024 at 21:19):
Here are all the linear models up to order 500 in ℤ/pℤ, p prime:
models
I'm searching with Vampire for an order 17 model but it hasn't found one yet.
Douglas McNeil (Dec 05 2024 at 22:14):
Ha, no, I was crossing streams in my mind. I was associating the linear models, which even include small ones like the ones I hit, with the enormous ones in the other thread! :upside_down: Neither vampire nor mace4 seems to like finding these guys for me for very much.. thanks for the list!
Bruno Le Floch (Dec 06 2024 at 01:55):
This 677->255 implication is immune to all linear models based on a (not necessarily commutative) ring where left-invertible ⇔ right-invertible (this includes finite rings and finite matrices over a field for instance).
The required equations to obey 677 are and . We want to show the condition for 255, which is . To proceed, we work with and . Note that the first assumption makes invertible. The two assumptions are
The first equation tells us how commutes through : intuitively it is mapped as . This is an involution, so we can get useful mileage from commuting through . Namely, we write and compute the LHS using the formula for and the RHS using the formula for . After reordering using the first identity, we get a formula of the form . Right-multiplying by and reducing we get . If I didn't mess up my calculations, we have enough to deduce , which is 255.
Matthew Bolan (Dec 06 2024 at 02:14):
I think I have also used Magma to rule out all non-commutative linear models modelled on a vector space with scalar field of characteristic 0 or positive characteristic less than 10000. In this online calculator one can run
for p in PrimesUpTo(10000) do
F<a, b, c> := FreeAlgebra(FiniteField(p),3);
B := [(-1)+(b*a)+(b*b*a*b),(a)+(b*b*a*a)+(b*b*b),(b*b*a*c)+(b*b*c)+(b*c)+(c)];
I := ideal<F | B>;
if not ((-1)+(a*a*a)+(a*a*b)+(a*b)+(b) in I and (a*a*c)+(a*c)+(c) in I) then
print(p);
end if;
end for;
print("Done");
to test small characteristics. (And testing the rationals is similar).
Pace Nielsen (Dec 06 2024 at 03:01):
Sorry I didn't make this clearer on the previous thread. When I worked out the two solutions over a generic field, I actually worked out the full reduction system over (potentially noncommutative) rings. For a map of the form , a reduction system is given by
(255 does indeed follow for such linear maps over rings.)
Matthew Bolan (Dec 06 2024 at 03:30):
Did you do that by hand or do you have software which can do that automatically? I'd like to compute the graph for linear implications.
Terence Tao (Dec 06 2024 at 03:43):
I can't believe it took 70 days into the project before we finally were able to make use of Magma...
Matthew Bolan (Dec 06 2024 at 03:51):
And it still isn't very useful (I was able to rediscover something close to your 1117 -> 2441 example with it though).
Matthew Bolan (Dec 06 2024 at 03:54):
(with this code in case you are curious. The ideal is the needed equations to be a linear model of 1117, the final two inclusions come from 2441)
F<a, b, c> := FreeAlgebra(Rationals(),3);
B := [(-1)+(b*a*b*a),(a)+(b*a*a),(b*a*b*b)+(b*b),(b*a*b*c)+(b*a*c)+(b*c)+(c)];
I := ideal<F | B>;
GroebnerBasis(I);
(-1)+(a*a)+(a*b*a*a)+(a*b*a*b)+(a*b*b)+(b) in I;
(a*b*a*c)+(a*b*c)+(a*c)+(c) in I;
Pace Nielsen (Dec 06 2024 at 03:55):
Matthew Bolan said:
Did you do that by hand or do you have software which can do that automatically? I'd like to compute the graph for linear implications.
I used code I wrote (and have updated over the years) in Mathematica. I'm happy to share it if you are interested---just shoot me an email.
Matthew Bolan (Dec 06 2024 at 03:58):
That's some useful stuff, I really could not find a standard package to do it for me and was dreading writing it myself.
Bruno Le Floch (Dec 06 2024 at 06:48):
(deleted)
Ibrahim Tencer (Dec 06 2024 at 06:51):
So do we really not have a single model that is known not to be linear?
Bruno Le Floch (Dec 06 2024 at 20:52):
A diagnosis of linear models is that all (finite) linear models are Latin squares (the condition makes invertible, then the condition makes invertible). It's clear that 677 implies that left multiplication is invertible, since is the whole magma and surjective implies injective. Both prover9 and mace4 are inconclusive on whether right multiplication has to be invertible in a general 677 magma (I am not very good with these tools though). This could influence the type of counterexamples we seek.
Terry used as a fall-back rule for his gigantic 1518 example because this was an easy way to fulfill the equation for most of the table. Here one option is to use a linear fallback, but the linear models are somewhat complicated. Another option is to use as a fallback a magma satisfying equation 14 (), but modifying the squares (or the products involving squares). Then for most the equation would reduce to . I didn't push this yet, in part because I wasn't sure if I had to make the magma right-cancellative.
Terence Tao (Dec 06 2024 at 22:41):
Hmm, the latter option looks problematic because it's going to be hard to have and both hold for most (if one replaces by then the first equation suggests that should equal , not ). One could perhaps ask an ATP whether the constant-squaring case is at all permissible, if so that might be a possible model to pursue.
Douglas McNeil (Dec 06 2024 at 22:51):
FWIW, there are definitely x*x=0 cases which satisfy 14/614, e.g. 5 or 13.
Ah, but you want eq 13 too, at least mostly, hmm.
Bruno Le Floch (Dec 06 2024 at 23:36):
Sorry, you're right, imposing equations 14 and 13 at the same time makes no sense. I had started an attempt by partitioning the magma in two subsets, but I don't have anything concrete at this stage.
The question of right-cancellation remains. In some sense, we need multiplication to preserve all the information in the right operand (due to left-cancellation) and at least "half" of the information in the left operand: indeed, the equation can be written as where and , and we want the pair of and to uniquely determine (for a given ). So maybe a better starting point would be to try a carrier and to find an example of 677 magma that is not right-cancellative. Then hopefully it helps with making a 255 counterexample.
Jose Brox (Dec 07 2024 at 08:47):
Bruno Le Floch ha dicho:
Both prover9 and mace4 are inconclusive on whether right multiplication has to be invertible in a general 677 magma (I am not very good with these tools though).
If we impose bijectivity of left and right multiplications, then 677 implies 255. Here is a Prover9 proof (it only uses left injectivity and right surjectivity):
PROVER9 677 plus left and right mult bijective implies 255 PROOF.txt
Jose Brox (Dec 07 2024 at 08:57):
Terence Tao ha dicho:
One could perhaps ask an ATP whether the constant-squaring case x⋄x=0
677 plus left multiplication bijective plus x^2 = y^2 implies 255.
I'm running a search of 677+left mult bijective + equation against 255, where equation ranges in [2,4694]. For now there are only 225 candidates left; I'll update soon.
Bruno Le Floch (Dec 07 2024 at 10:50):
The specific idea of dropping uniformly the "same half" of the left operand fails. In the equation written (in the finite case) as x = (y ◇ x) ◇ ((y ◇ (y ◇ x)) ◇ y)
, that would mean that the only dependence on y1 is from the last variable, and this dependence never disappears because this y
is acted on by bijective L_{y ◇ x}
and L_{y ◇ (y ◇ x)}
. So we need more mixing.
Douglas McNeil (Dec 07 2024 at 14:29):
So, that was a complete failure: mutation didn't work at all here, despite a fresh run.
I had one last faint hope that I simply had too few samples, but even after I had the dozens of linear models to play with thanks to Ibrahim, no luck. They're too tightly coupled together to use as good seeds. If you remove too few cells you wind up completing back to the original, and if you don't, you get an enormous number of linked failures which don't seem repairable. Reducing to a partial solution using fewer elements and trying to grow that, which helped before, also didn't work. Frankly, both vampire and mace4 have trouble finding the known solutions for me without a lot of prompting at larger N, although that might not apply to less coupled solutions, to be fair.
Efforts to use 614 as a base and then migrate back towards 677 didn't work either, and I can't even use the trick of driving toward a solution gradually by imposing some of an equation's implications because 677 doesn't have any in our set.
For evolutionary approaches to work, you need at least to be able to jump from one useful state (target or not) to another efficiently. This fails when useful states are too rare or it takes too long to get a new state, both of which seem to be true here.
Terence Tao (Dec 07 2024 at 15:55):
Jose Brox said:
Bruno Le Floch ha dicho:
Both prover9 and mace4 are inconclusive on whether right multiplication has to be invertible in a general 677 magma (I am not very good with these tools though).
If we impose bijectivity of left and right multiplications, then 677 implies 255. Here is a Prover9 proof (it only uses left injectivity and right surjectivity):
PROVER9 677 plus left and right mult bijective implies 255 PROOF.txt
This feels like an important clue to me. For finite magmas we get left injectivity for free. If we can get a human proof of why right surjectivity implies 255 that should make it clearer what a counterexample might look like (or what a proof might look like - this implication could well be true for finite magmas!).
Terence Tao (Dec 07 2024 at 16:16):
One possible thought is to try to adapt a technique that worked for weak central groupoids (see blueprint), which is to find a small (e.g., order 2) "relaxed" solution to 677 (where the magma operation is slightly multivalued), and try to build an extension of that by some pseudo-greedy algorithm. This amounts to imposing a coloring on the magma and imposing some rules about how the color of relates to the color of and (e.g., if is red and is blue, then must be blue, but if and are both red, then could be either red or blue, etc.). It may be possible to "decouple" the magma structure this way, for instance one could try to make the equation 13 hold for red elements and 14 hold for blue elements, thus dodging the issue that 13 and 14 are not compatible with each other. However I don't know if there is a practical relaxed magma that can be used as a base (of course one can always use the trivial relaxation in which every color output is permitted, but this doesn't gain anything).
Jose Brox (Dec 07 2024 at 16:18):
Terence Tao ha dicho:
f we can get a human proof of why right surjectivity implies 255 that should make it clearer what a counterexample might look like
Ok! I will have a look at it later and translate it from "telegraphic superposition calculus" to something more human-readable.
Jose Brox (Dec 07 2024 at 16:19):
Jose Brox ha dicho:
I'm running a search of 677+left mult bijective + equation against 255, where equation ranges in [2,4694]. For now there are only 225 candidates left; I'll update soon.
24 candidates have survived a 10min Prover9 search. So, together with 677 (and left multiplication bijective) it is probably also safely to assume any of
[411, 513, 623, 642, 817, 1020, 1035, 1048, 1223, 1238, 1251, 1426, 3659, 4065, 4073, 4131, 4276, 4293, 4321, 4343, 4380, 4591, 4599, 4695]
against 255.
Later I will look at combinations of these additional equations.
Ibrahim Tencer (Dec 07 2024 at 16:27):
There are no 677 models of size 2, 3, 4, and 6. I've been running a Vampire search for a model of order 8 for 26 hours but it still hasn't found one.
Terence Tao (Dec 07 2024 at 16:39):
It's relatively rare for a two-variable equation such as 677 to have so few models, and so much restriction on the order. Weak central groupoids (1485) also had a lot of restrictions on the order, but that's a three-variable equation, so less surprising (it imposes constraints rather than constraints).
On the other hand, in contrast to say 854, 677 does not seem to be implying a lot of other laws (Equation Explorer only lists the trivial consequence 614, even if one assumes finiteness). So this equation is imposing some "rigidity", but the rigidity is coming from an unknown source.
Matthew Bolan (Dec 07 2024 at 16:47):
The key point of the prover9 proof seems to be that 677 says that so and thus by left injectivity.
From here, the point is that 677 + left injectivity tell us , so , and so Right multiplying this by gives 255.
Terence Tao (Dec 07 2024 at 16:53):
To rephrase the argument: if we have , then by 677 , hence by left-cancellativity . Meanwhile from 677 with replaced by we also have , so by left-cancellativity again and hence which is 255 for .
So we don't even need full right surjectivity; just being able to solve for each would give 255. Conversely, 255 clearly implies that is solvable, so this is an equivalent form of 255.
Terence Tao (Dec 07 2024 at 17:06):
This now reminds me of the ruleset of the (automatically generated) greedy algorithm refuting 677->255 for infinite magmas (which is conveniently accessible from the 677 Equation Explorer page). The 677 ruleset (ignoring Rule 0, which says that is a partial function) is
- If , , , then (this is just 677)
- If then
- If , , and then
- If , , and , then .
Rule 2 can be strengthened with the above analysis: if then so if we also have then is idempotent, and by left-cancellativity we have . Not sure yet where Rule 3 and Rule 4 are coming from though.
Terence Tao (Dec 07 2024 at 17:21):
A proof of Rule 3 (for finite magmas at least): by hypothesis, . From 677 we have hence by left-cancellability as required.
Matthew Bolan (Dec 07 2024 at 17:33):
Rule 4 holds since , so
Terence Tao (Dec 07 2024 at 17:48):
Given that one needs to avoid solving the equation to obtain a counterexample, a possible relaxed base magma to choose is the carrier with and permitted to be either or , thus cannot equal when . An extension of this relaxed base would thus be a magma colored in two colors, 0 and 1, such that the product of anything with a 1-colored object must be 0-colored. As far as I can tell, this is compatible with 677 (but perhaps having an ATP confirm this would be great). So if we can create such a 2-colored finite 677 magma with at least one element 1-colored, we have refuted 677 -> 255 for finite magmas!
One natural place to start is to see if it is possible to start with some base 677 magma, such as a linear model, declare it to be 0-colored, and see if one can add a single 1-colored element to it and preserve 677. Given how rigid the 677 magmas seem to be, this seems unlikely, but perhaps discovering the obstruction to this working would be instructive.
Terence Tao (Dec 07 2024 at 17:57):
OK, adjoining 1-colored objects to an existing 0-colored magma would not work, as it would violate left-surjectivity (the product of a 0-colored object with anything would not be 1-colored).
Jose Brox (Dec 07 2024 at 19:00):
Terence Tao ha dicho:
So we don't even need full right surjectivity; just being able to solve y⋄x=x for each x would give 255. Conversely, 255 clearly implies that y⋄x=x is solvable, so this is an equivalent form of 255.
Jose Brox ha dicho:
24 candidates have survived a 10min Prover9 search. So, together with 677 (and left multiplication bijective) it is probably also safely to assume any of
[411, 513, 623, 642, 817, 1020, 1035, 1048, 1223, 1238, 1251, 1426, 3659, 4065, 4073, 4131, 4276, 4293, 4321, 4343, 4380, 4591, 4599, 4695]
against 255.
I'm now running 10min searches for models with 677+one of the 24 candidates+left multiplication bijective + (exists x such that doesn't exist y such that yx = x). Already without adding any candidate, size 8 is exhausted in seconds.
Terence Tao (Dec 07 2024 at 19:29):
One possible stronger axiom than (exists x such that doesn't exist y such that yx = x) is (exists distinct 1,0 such that y1=0 for all y). If we can find a finite 677 magma that obeys this axiom then we are done, but perhaps there is a simple reason why such axioms are incompatible with 677.
Terence Tao (Dec 07 2024 at 19:32):
OK, the strong axiom is not compatible. 677 implies , so by left invertibility is independent of . In particular , hence by left cancellability for all , which is absurd.
Terence Tao (Dec 07 2024 at 19:39):
This still allows for the possibility that one has for all (and for some ), though.
Ibrahim Tencer (Dec 07 2024 at 21:54):
One observation: 255 says where we define powers with right-multiplication. The model is finite so two powers of x must coincide, giving with . If right-cancellation holds then we can repeatedly take x's off of both sides to get it in the form , but otherwise we can repeat @Terence Tao 's argument to instead get . So for a counterexample we should think about what m and n can be.
Terence Tao (Dec 07 2024 at 22:38):
Sorry, could you clarify how you get that final equation ? I can see that and we also have , but then I get stuck.
Ibrahim Tencer (Dec 07 2024 at 22:44):
Ah never mind, I was getting x^n and x mixed up there.
Terence Tao (Dec 07 2024 at 22:46):
I assume that a law such as (equation 359) would already have been ruled out by @Jose Brox 's sweep, though perhaps it is worth figuring out why such a law would immediately give 255.
Jose Brox (Dec 07 2024 at 22:51):
Ibrahim Tencer ha dicho:
There are no 677 models of size 2, 3, 4, and 6. I've been running a Vampire search for a model of order 8 for 26 hours but it still hasn't found one.
Making trials with sizes 6 and 7, it seems that the best Mace4 configuration for 677 is selection_order 2, selection_measure 3, skolems_last set. With it, Mace4 has been able to check in 41min that 677 has NO models of size 8.
Size 9 has been running for almost 4h already, no models yet.
Btw, in sizes 5 and 7 there is only one model (up to isomorphism).
Douglas McNeil (Dec 07 2024 at 23:32):
@Jose Brox : you mean only one model under the additional props of your search, right? There are definitely two non-iso order 7 677s (with and without constant squares).
Jose Brox (Dec 07 2024 at 23:44):
Douglas McNeil ha dicho:
you mean only one model under the additional props of your search, right? There are definitely two non-iso order 7 677s (with and without constant squares).
Oh, this seems like another bug in Windows' isofilter :melting_face:
I meant without any other properties, because that is what isofilter says! It only returns the model with non-constant squares (see the pictures below), but it does find the constant squares one, so it seems to be isofilter and not Mace4 what fails.
Thank you for this observation!
Isofilter serious bug 1.JPG
Isofilter serious bug 2.JPG
EDITED: This bug only appears in the Windows GUI, isofilter in the Ubuntu command line gives the right answer, with two isoclasses.
Jose Brox (Dec 08 2024 at 14:36):
(deleted)
Jose Brox (Dec 08 2024 at 14:39):
Terence Tao ha dicho:
this implication could well be true for finite magmas!
And if I have everything right, indeed it is!
677 + left multiplication injective + (right multiplication injective iff right multiplication surjective) implies 255:
**Prover9 assumptions**
x = y * (x * ((y * x) * y)) #label(677).
x*y = x*z -> y = z.
(y*x = z*x -> y = z) <-> (all u all v exists w (w*u = v)).
**Prover9 goal**
x = ((x * x) * x) * x #label(255).
PROVER9 677 implies 255 in finite setting PROOF2.txt
The proof is simpler if we also impose that is not always solvable, as we know we can do:
PROVER9 677 implies 255 in finite setting PROOF.txt
Is everything right?
Matthew Bolan (Dec 08 2024 at 14:54):
I think the "for all" quantifiers have the wrong scope in the third assumption, they should be inside the parentheses. I'd expect
(all y all z (y*x = z*x -> y = z)) <-> (all v exists w (w*x = v)).
or
(all x all y all z (y*x = z*x -> y = z)) <-> (all u all v exists w (w*u = v)).
Bruno Le Floch (Dec 08 2024 at 15:10):
EDIT: I had previous claimed here that prover9 finds a proof with the corrected version given by Matthew, but actually I missed parentheses. Now it doesn't work.
Terence Tao (Dec 08 2024 at 17:34):
No problem, we all make mistakes here (I've certainly made my own fair share)!
Bruno Le Floch (Dec 08 2024 at 21:50):
(incorrect) 25-element refutation of 677->255
Douglas McNeil (Dec 08 2024 at 21:51):
Uh, doesn't that refute 255->677 instead? :upside_down:
Bruno Le Floch (Dec 08 2024 at 21:52):
Ouch. Yes! Perfect smiley, by the way.
Jose Brox (Dec 08 2024 at 23:05):
Matthew Bolan ha dicho:
I think the "for all" quantifiers have the wrong scope in the third assumption, they should be inside the parentheses.
Thank you, this is indeed the case! This one is subtle: according to its manual, when parsing free variables in clauses and formulas Prover9 assumes they are universally quantified at the outermost level. I had understood this fact to be relative, i.e., to mean "at the outermost level of each subformula given by parentheses", but it is in fact absolute, meaning "at the outermost level of the global formula". Hence
x*y = x*z -> y = z
works as intended, but
(x*y = x*z -> y = z)<->(all u all v exists w (w*u = v))
actually means
all x all y all z ((y*x = z*x -> y = z) <-> (all u all v exists w (w*u = v)))
instead of
(all x all y all z (y*x = z*x -> y = z)) <-> (all u all v exists w (w*u = v))
. The variant
all x all y all z (y*x = z*x -> y = z) <-> all u all v exists w (w*u = v)
also works as intended.
Terence Tao ha dicho:
No problem, we all make mistakes here (I've certainly made my own fair share)!
I've made quite a few! Mine tend to be misunderstanding errors (worse in weekends :upside_down:) ...
Zoltan A. Kocsis (Z.A.K.) (Dec 09 2024 at 00:00):
@Jose Brox :
meaning "at the outermost level of the global formula"
In first-order model theory, writing down the simplest possible definition of the satisfaction relation naturally leads to interpreting "free variables as universally quantified", in the sense that a formula with free variables counts as satisfied in a model precisely if its universal closure is satisfied in that model.
The treatment of free variables in Prover9/Mace4 attempts to follow the same convention. This explains why the manual's explanation is so unnuanced. The authors failed to anticipate that the users would not necessarily be logicians familiar with this convention.
Bruno Le Floch (Dec 09 2024 at 01:53):
Consider 677-cohomology. We consider an abelian coefficient group with a linear operation with . The extension is equipped with . The cocycle equation (stating that the extension obeys 677) is
On the other hand, has to obey 677, so and , which reduce in the abelian case to and .
Claim: if a 677 model has (which holds for type 1 linear models over fields), then for any 677-coefficients the 677-cohomology is a subgroup of the 255-cohomology. In other words, any of its extensions by linear models obeys 255.
For the cocyle equation reduces to . To establish 255 we want to show . The bookkeeping, working modulo , works out.
This suggests looking at type 2 linear models over fields, such as the two 7-element magmas. Unfortunately both of them have trivial cohomology over (hence with arbitrary coefficients?). It would be good to understand why.
Another option for the base is a magma that has already been linearly extended once.
Matthew Bolan (Dec 09 2024 at 02:05):
I've already checked all extensions with , linear (including a constant term) and order <= 25 with no luck. I can try taking the base to be magmas which have been extended once though.
Terence Tao (Dec 09 2024 at 02:41):
It's good to get some theoretical explanation as to why the cohomological approach wasn't being successful here! We already knew that to disprove a one-variable equation like 255 one can assume without loss of generality that the base model is generated by a single element, which explains why it isn't productive to use base magmas in which every element is idempotent.
My cohomological algebra is extremely rusty (definitely not my favorite class in grad school) but I guess these magma cohomology groups should obey some sort of "universal coefficient theorem" that relates the complex coefficient groups to the others [EDIT: but then I guess we also have to define some "magma homology" that is dual to "magma cohomology"?]. I had some vague hope that even if the characteristic zero cohomology is trivial, there is some "ramification" at some prime caused by some determinant in the linear algebra having a prime or prime power factor which could then lead to a finite counterexample. I think it would also be interesting to find infinite counterexamples to 677->255 defined over the complex numbers; currently our only construction of this counterexample proceeds by the greedy method and does not give a very tractable description of the resulting magma.
Matthew Bolan (Dec 09 2024 at 02:58):
I think we actually already have an example of some kind of "ramification" for the linear models. Bruno's degree 307 counterexample in the HN law project is very interesting, over the polynomial is in the relevant ideal, and if is invertible, then and no linear counterexample can exist, but modulo 307 we have a linear counterexample.
Matthew Bolan (Dec 09 2024 at 03:01):
the degree 103 example has a similar property, though I think it also has counterexamples in characteristic 5.
Matthew Bolan (Dec 09 2024 at 03:10):
There are examples of similar phenomena in the main project by the way, for example law 895 (Which is a law for abelian groups of exponent 2) only has linear models in characteristic 2.
Terence Tao (Dec 09 2024 at 03:13):
I have a vague intuition that such exceptional primes may be the best bet for finding counterexamples from the cohomological approach, because often the relevant matrices in the linear algebra calculations are going to have full rank (after quotienting out the coboundaries) and so in general characteristic will not have an interesting kernel that we can use to produce non-trivial extensions. But if there is ramification then we can hope to sneak in an interesting counterexample at specific primes. Except that for this particular equation, we only get magmas at relatively large primes like 5, 7, or 11, so the probability of getting ramification is sadly somewhat low. Though your examples at 307 and 103 do indicate that maybe all hope is not lost...
Terence Tao (Dec 09 2024 at 03:33):
Actually, at every prime it should be possible to construct a linear magma in characteristic by using an appropriate finite field that holds all the relevant coefficients , so maybe one will be fine as soon as there is ramification at any prime...
Terence Tao (Dec 09 2024 at 03:37):
Would it be possible to make your cohomology code give the Smith normal form of the cocycle equation for a given base magma (presumably a Type 2 base model, given that Type 1 models are useless)? The prime factors of the elementary divisors of that form would be the natural choices for the characteristic for the coefficient magma as the cohomology groups should be unusually large over those characteristics. (One may have to work first in some abstract coefficient ring over generated by the defining equations for the coefficients before specializing to a finite characteristic .)
Matthew Bolan (Dec 09 2024 at 03:44):
I think that should be possible provided sage supports the Smith Normal Form computation over the relevant ring, which it hopefully does.
Matthew Bolan (Dec 09 2024 at 04:27):
Hmm, I'm running into some trouble. The needed abstract coefficient ring is not a PID, and so I don't think Smith Normal Form makes sense for it (at least, not in a way sage supports or I can easily implement).
Terence Tao (Dec 09 2024 at 04:35):
OK so apparently there is something called the Hermite normal form that can work for Dedekind domains that aren't PIDs and may be sufficient here as a substitute for the Smith normal form. It's implemented in SAGE at https://doc.sagemath.org/html/en/reference/matrices/sage/matrix/matrix_integer_dense.html#sage.matrix.matrix_integer_dense.Matrix_integer_dense.hermite_form
Terence Tao (Dec 09 2024 at 04:37):
Hmm but the sage implementation is only over the integers
Terence Tao (Dec 09 2024 at 04:42):
Following links from ChatGPT, I find that this specific functionality was listed as "Extreme difficulty" to implement in SAGE in https://wiki.sagemath.org/GSoC/2015?utm_source=chatgpt.com#Hermite_Normal_Forms_for_modules_over_the_ring_of_integers_of_number_fields. , and presumably never implemented. :sad:
Terence Tao (Dec 09 2024 at 04:43):
Though it suggests that Magma or PARI can do it.
Terence Tao (Dec 09 2024 at 04:54):
Apparently the relevant documentation page for the Magma implementation is https://magma.maths.usyd.edu.au/magma/handbook/text/276 , but I've never actually used Magma so I don't know how easy it would be to use these methods for our specific application.
Matthew Bolan (Dec 09 2024 at 04:54):
I think it is definitely worth pursuing, it didn't occur to me to check Magma but if is has this functionality then it should have enough to just let me compute directly.
Matthew Bolan (Dec 09 2024 at 04:58):
In the meantime I'm going to go back to trying base models which are already extensions, so that I can do an overnight run of that check.
Terence Tao (Dec 09 2024 at 04:59):
Do you know by the way if any of the extensions were non-trivial (i.e., not by coboundaries)? That is to say that was actually non-trivial for some choices of ?
Matthew Bolan (Dec 09 2024 at 05:00):
Yes, that seems to occur. In fact for some choices of I was surprised by how large was - makes me worry I've done something wrong in my computation of I've just written.
Terence Tao (Dec 09 2024 at 05:02):
It might be worth sharing some examples of such non-trivial extensions here for others to play with. As I understand it right now the only explicit finite models we have for this equation are the linear ones (and direct products thereof).
Matthew Bolan (Dec 09 2024 at 05:07):
I was planning to, just trying to make sure I don't share any nonsense (Is there any easy way to prove a model is non-linear?).
Terence Tao (Dec 09 2024 at 05:34):
Hmm. In a linear model all the left and right multiplication operators lie in the affine group, which is solvable (and even metabelian), so for instance . Most likely any nonlinear model would fail this identity.
Matthew Bolan (Dec 09 2024 at 06:06):
Alright, implementing that test currently seems like more trouble than it is worth. I'm just going to print out for each the magmas corresponding to some basis of and send a giant text file.
Matthew Bolan (Dec 09 2024 at 06:07):
They should work out anyway
Matthew Bolan (Dec 09 2024 at 06:14):
Matthew Bolan (Dec 09 2024 at 06:15):
Using linear models of size <= 15
Jose Brox (Dec 09 2024 at 08:47):
A model of 677 of size 9, found in 32.5h by Mace4 (it also satisfies 255):
[[ 0, 2, 3, 5, 1, 7, 4, 8, 6],
[ 1, 3, 4, 6, 7, 0, 2, 5, 8],
[ 2, 8, 5, 1, 3, 4, 6, 0, 7],
[ 3, 5, 6, 7, 4, 2, 8, 1, 0],
[ 4, 6, 8, 0, 2, 3, 5, 7, 1],
[ 5, 1, 7, 4, 6, 8, 0, 3, 2],
[ 6, 7, 0, 2, 8, 5, 1, 4, 3],
[ 7, 4, 2, 8, 0, 1, 3, 6, 5],
[ 8, 0, 1, 3, 5, 6, 7, 2, 4]]
Zoltan A. Kocsis (Z.A.K.) (Dec 09 2024 at 12:49):
@Jose Brox : The structure your long search found appears to be a "twisted copy" of the elementary Abelian group .
edit: There was a miscalculation here - the model is linear however, see below.
We can find functions and so that . Or, more legibly, if you change the base set of your magma to coincide with that of , then you in fact have , where is the group operation.
Let's use a compact notation for elements of , with e.g. denoting the pair .
Then the permutation is given by the cycles , while is given by . And is just the obvious map sending into , and its inverse.
NB I found by fixing first, so mayhap for some other the two permutations admit a more readable form. But in the end is a -twisted version of a group operation.
Zoltan A. Kocsis (Z.A.K.) (Dec 09 2024 at 12:51):
(Please note that I'm still mostly out-of-the-loop after my long hiatus, maybe it's already obvious from the study of the linear case that these examples will always have this form. If so, apologies. Just thought it was a fact that should be documented.)
Terence Tao (Dec 10 2024 at 16:29):
Interesting! It's not obvious to me why an operation of the form should have any particular likelihood to solve 677 if are nonlinear. Perhaps if we figure this out, we would have a new ansatz for searching for finite models (right now we basically only have three viable ansatzes: the linear model, the translation-invariant model, and cohomological models. Of the three, we haven't really explored translation-invariant models much, but the functional equation for 677 is rather unappetizing there...)
Terence Tao (Dec 10 2024 at 18:39):
@Zoltan A. Kocsis (Z.A.K.) I'm having trouble matching your model with @Jose Brox 's model. For instance, Jose's model is right-unital, , but the model is not going to be right-unital unless is a shift of the identity map. Perhaps there is a typo somewhere?
Matthew Bolan (Dec 10 2024 at 19:06):
Just to make sure, we know that Jose's model is not one of the two linear ones over ? Those are both right unital
Terence Tao (Dec 10 2024 at 19:07):
According to my calculations, the magma is instead equivalent to a linear model with carrier and operation where . I think this is also a linear model over .
Matthew Bolan (Dec 10 2024 at 19:11):
The linear models over are and , where .
Terence Tao (Dec 10 2024 at 19:11):
Yeah that matches. So unfortunately this isn't a new model
Jose Brox (Dec 10 2024 at 21:57):
Terence Tao ha dicho:
Yeah that matches. So unfortunately this isn't a new model
I should have made a search for more than one model, as Mace4 tends to find them in batches, with small perturbations of the first one encountered. I'm running two new searches, one of them forcing the model not to have a right unit.
Douglas McNeil (Dec 10 2024 at 21:59):
@Jose Brox : is it just me or are 677 magmas noticeably slower to find than others? It was easier for me to find models in the ~15 range for some three-variable equations than it is to find models with only a third as many cells here. I don't know if it's the fact every substep has a new element so there's lots of coupling or what.
Terence Tao (Dec 10 2024 at 22:41):
There's something very "mixing" about 677. It doesn't have easy models like left-absorptive or right-absorptive models that one can hope to modify, nor does it involve the squaring map which seems to simplify the structure (in that a law involving three magma operations and a square seems easier to satisfy than four magma operations and no square). Also it can't be easily expressed purely in terms of left multiplication or purely in terms of right multiplication, but instead mixes together both. So, other than using a linear ansatz, there don't seem to be cheap ways to try to make it more likely to create a 677 magma. Also the fact that half of the linear models are idempotent is also weakening the power of the cohomological method to construct interesting magmas.
Jose Brox (Dec 10 2024 at 23:38):
There are no countermodels of 255 satisfying 677 in size 9, computation done in 29.6h by Mace4 (order 2, measure 3, skolems_last) with the formulas
**ASSUMPTIONS**
x = y * (x * ((y * x) * y)) #label(677).
x*y = x*z -> y = z.
all x all y exists z (x*z = y).
exists x -(exists y (y*x = x)).
(all x all y all z (y*x = z*x -> y = z)) <-> (all u all v exists w (w*u = v)).
**GOAL**
x = ((x * x) * x) * x #label(255).
Zoltan A. Kocsis (Z.A.K.) (Dec 11 2024 at 00:51):
Terence Tao said:
Zoltan A. Kocsis (Z.A.K.) I'm having trouble matching your model with Jose Brox 's model. For instance, Jose's model is right-unital, , but the model is not going to be right-unital unless is a shift of the identity map. Perhaps there is a typo somewhere?
Yes, I revisited my notes and found the miscalculation :/ Apologies for sending you on a wild goose chase. Further reviewing the notes, I think I do show that one can at least write for a nontrivial over $\mathbb{Z}/3\mathbb{Z}^2$$ but since this happens to be a linear model anyway, I won't pursue it any further.
Jose Brox (Dec 11 2024 at 07:54):
Jose Brox ha dicho:
I'm running two new searches, one of them forcing the model not to have a right unit.
Two negative results:
1) There are no other size 9 models of 677 satisfying , , besides the linear one (1.2h in Mace4).
2) There are no size 9 models of 677 that are not right unital (5.8h in Mace4).
There seem to be few models of size 9...
Bruno Le Floch (Dec 11 2024 at 10:27):
The cohomological approach cannot yield counterexamples to 255. The set of (right-)cancellative 677 models is stable under cohomological extensions (see proof below), so for each we have a solution of , which we know implies 255. Copying Terry Tao's version of the argument here: so by left-cancellativity so by left-cancellativity hence , equation 255.
Why is right-cancellativity stable? Consider with a linear model. We know (finite) linear models are right-cancellative (in other words is invertible). If then and . The first equation gives by right-cancellativity of the base. The second equation then gives by invertibility of .
That said, the cohomological approach could still possibly provide nonlinear examples of 677, which may be of independent interest.
Bernhard Reinke (Dec 11 2024 at 12:47):
Were finite non-commutative translation invariant models already considered?
Bernhard Reinke (Dec 11 2024 at 13:23):
I think in that setting, one could try to consider something like so that , left cancellative implies that is a injective (so a bijection for finite models), and what we want to avoid is , so should be fixed-point free (hence a derangement).
Bernhard Reinke (Dec 11 2024 at 14:05):
if I am not mistaken, then 677 translates to .
Bernhard Reinke (Dec 11 2024 at 14:10):
Or in straight-line notation: if we denote the graph of by , then we have
Bruno Le Floch (Dec 11 2024 at 14:17):
Is it clear that we need non-commutativity to get interesting 677 models? It seems easier to explore if the carrier is simply a finite abelian group.
Bernhard Reinke (Dec 11 2024 at 14:47):
For me it is not clear, but maybe it can help. Here is a naive exploration idea that doesn't really see the commutativity: we fix a finite group G
(represented by its multiplication table and inverse function). We can try to construct a SAT problem with variables and clauses: basically, for each subterm of the equation that we consider, we have a |G|^2 many variables corresponding to the graph of the subterm (so for each subterm and , we have a variable corresponding to . For each multiplication in the equation, we have |G|^3 3-term clauses that correspond to . Similar, for function application we have |G|^3 3-term clauses corresponding to (for inversion we only need |G|^2 2-term clauses). The equation itself gives us also 2|G|^2 clauses. Then we add that each subterm should be a function and should be a derangement, and then we ask a SAT solver whether this has a solution.
Pace Nielsen (Dec 11 2024 at 15:35):
Unless I made a mistake, Vampire says that 677 does imply 255 subject to (1) left cancellativity and (2) right cancellativity => surjectivity of right multiplication. I believe both conditions hold for finite models. Here is the code I ran:
fof(eq677, axiom, X = mul(Y, mul(X, mul(mul(Y, X), Y)))).
fof(leftcanc, axiom, mul(X, Y) = mul(X, Z) => Y = Z).
fof(rtcanctosurj, axiom, (! [U, V, W] : mul(V, U) = mul(W, U) => V = W) => (! [Y, Z] : ? [X] : mul(X, Y) = Z)).
fof(eq255, conjecture, X = mul(mul(mul(X, X), X), X)).
Edited to add: Jose found the error below.
Matthew Bolan (Dec 11 2024 at 15:38):
Why does right surjectivity hold for finite models?
Pace Nielsen (Dec 11 2024 at 15:40):
Matthew Bolan said:
Why does right surjectivity hold for finite models?
I'm not assuming surjectivity of right multiplication. I'm assuming that such surjectivity follows from injecitivty of right multiplication (which is true for finite models).
Matthew Bolan (Dec 11 2024 at 15:41):
Ah, understood.
Pace Nielsen (Dec 11 2024 at 15:45):
Just ran a sanity check, by simply assuming that right multiplication is not cancellative, and Vampire couldn't prove 255 in that case. So, I'm thinking that something is wrong with that 3rd line (but I'm not sure what, since I've looked it over a few times now).
Jose Brox (Dec 11 2024 at 15:46):
Pace Nielsen ha dicho:
fof(rtcanctosurj, axiom, (! [U, V, W] : mul(V, U) = mul(W, U) => V = W) => (! [Y, Z] : ? [X] : mul(X, Y) = Z)).
I think here there is the same mistake that I made with Prover9: in TPTP language, quantification has higher precedence than binary connectives, so you need to move the parentheses to the inside of the formula.
Jose Brox (Dec 11 2024 at 15:47):
fof(rtcanctosurj, axiom, ! [U, V, W] : (mul(V, U) = mul(W, U) => V = W) => ! [Y, Z] : ? [X] : (mul(X, Y) = Z)).
Pace Nielsen (Dec 11 2024 at 15:49):
That fixed it. Thanks Jose!
Pace Nielsen (Dec 11 2024 at 15:58):
By the way (after that fix) Vampire is finding no problems with a (commutative or noncommutative) translation-invariant approach.
Pace Nielsen (Dec 11 2024 at 16:03):
This might be a silly question, but what was the method used to disprove the implication 677 => 255 for infinite magmas?
Matthew Bolan (Dec 11 2024 at 16:04):
It was among those resolved by the automated greedy algorithm.
Matthew Bolan (Dec 11 2024 at 16:04):
There's some discussion about the nature of its greedy algorithm here: #Equational > FINITE: 677 -> 255 @ 💬
Jose Brox (Dec 11 2024 at 16:09):
Terence Tao ha dicho:
I assume that a law such as x2=x3 (equation 359) would already have been ruled out by @Jose Brox 's sweep, though perhaps it is worth figuring out why such a law would immediately give 255.
Sorry, this message went under my radar until now! Yes, 677 with 359 implies 255 in the finite case. I attach the shortest proof I've been able to extract from Prover9 (it has 39 steps):
PROVER9 677 with 359 finite implies 255 PROOF.txt
Terence Tao (Dec 11 2024 at 16:14):
@Bruno Le Floch Thanks for explaining why the implication is immune to the cohomological method! Disappointing of course - this looked like our best shot to finishing off the last implication - but at least we now have a satisfactory explanation for why the numerical implementation of the cohomological method was not working.
So now we need a new method. Bernard is already proposing the translation invariant model, which seems to be the best option we currently have. Regarding other constructions, I only have some largely negative results to report here.
-
One variant of the cohomological construction is a piecewise linear model . Let's say the base is the order 5 model, then we have 50 unknowns here . For idempotent , have to be coefficients of a linear model (and in particular will exhibit right cancellativity) but a priori there is no such requirement for off-diagonal coefficients . On the other hand, 677 will force 50 separate quartic equations on these 50 unknowns, which is quite unappealing (with a translation invariant ansatz one can cut this down to 10 equations in 10 unknowns, which is still bad) but also would suggest there are only finitely many solutions in any given field, with no particular reason for any one of the to vanish. So the chance of getting a non-right-cancellative example here is slim. [EDIT: one can combine this model with the cohomological model to consider the more complex operation , but this doesn't add any capabilities - if we had such a model that was not right-cancellative, then we could set and already get a model that was not right-cancellative.]
-
Another option is the extension method: start with an existing model, e.g., a linear model , and add a few elements to it with the hope of making a new model. One cannot just add one element: if one adds a new element to an existing 677 magma , then by left-invertibility we must have for all , which is not actually possible since by previous analysis for each the only possible solution to is . So the first available option is to add two elements to and impose the laws , for . If one can also assure that , say, then one is done, as now there is no solution to . So perhaps one could explore if an ATP thinks this is a viable approach?
Jose Brox (Dec 11 2024 at 16:25):
Recall that together with 677 plus finiteness conditions it seems safe to assume one of the following list of
Additional properties
At first glance,
513: x = y * (y * (y * (y * x)))
, 4591: (x * x) * x = (y * y) * y
, and 4599: (x * x) * y = (x * y) * y
seem particularly interesting to me. With the last two there are no countermodels up to size 13 (I'm running size 14 now). Also 4276, 4293, 4321, 4343 look similarly promising.
With 513, note that we can write the inverse of any left multiplication , and from we get and other interesting identities like
,
, and
,
which may suggest an approach focused on the functions
Pace Nielsen (Dec 11 2024 at 17:03):
(deleted)
Bernhard Reinke (Dec 11 2024 at 17:09):
Oh well, that is too bad. Do you mind sharing the final tptp file you used for this?
Pace Nielsen (Dec 11 2024 at 17:11):
Oh, I realized I made an error. After the fix, Vampire is finding no problem with a carrier group for a translation-invariant model to be commutative of exponent 3.
Pace Nielsen (Dec 11 2024 at 17:35):
(deleted)
Terence Tao (Dec 11 2024 at 17:53):
More negative progress: my proposal to have two elements with for won't work. If a 677 magma has more than 5 elements we can find such that . On the other hand, 677 gives which simplifies using the given hypotheses to , contradiction.
More generally this suggests that taking an existing 677 magma and adding a small number of elements to it is unlikely to be possible once the base magma is moderately large.
Terence Tao (Dec 11 2024 at 18:22):
Recording another failed approach as a negative result. If one defines , then 677 can be written as . So, using left cancellativity, one can describe the relation between and by two axioms:
- If , then .
- If , then .
So I tried first choosing the function , and seeing if one could build a magma operation that obeyed Axiom 1 and Axiom 2 for that choice of . The point is that the axioms are rather simple: both axioms assert that one entry in the multiplication table propagates to another. The problem is that these axioms don't commute, and in principle after N applications of these axioms, a single entry on the table can propagate into 2^N other entries, leading almost certainly to collisions. One somehow wants to choose an with a special property that the propagation rules of Axiom 1 and Axiom 2 (i.e., the functions and ) obey a lot of algebraic relations that cuts down on this complexity, but setting to be too simple (e.g., constant) quickly leads one to violate the requirement that each entry of the multiplication table has a unique answer. Of course, because we have linear models, we know that it is possible to satisfy both of these axioms with a linear choice of ; I tried a little bit with the scenario in which stays linear but we allow for nonlinear , but didn't make much headway there. (Also, if is right-cancellative then will be also, since we already have left-invertibility, so even if I did make a non-linear model out of this, it still wouldn't refute 255.)
Ben Gunby-Mann (Dec 11 2024 at 21:43):
Jose Brox said:
Recall that together with 677 plus finiteness conditions it seems safe to assume one of the following list of
Additional properties
At first glance,
513: x = y * (y * (y * (y * x)))
,4591: (x * x) * x = (y * y) * y
, and4599: (x * x) * y = (x * y) * y
seem particularly interesting to me. With the last two there are no countermodels up to size 13 (I'm running size 14 now). Also 4276, 4293, 4321, 4343 look similarly promising.With 513, note that we can write the inverse of any left multiplication , and from we get and other interesting identities like
,
, and
,
which may suggest an approach focused on the functions
Possibly interesting to note (not hard to show but on my phone now) is that 677+513 has no nontrivial commutative linear models. So any nontrivial model of both of these simultaneously will be something new!
EDIT: Not true; this has the solution in any commutative ring of characteristic 5; however, these are the only linear solutions in commutative integral domains; see correction below.
Jose Brox (Dec 11 2024 at 22:08):
Ben Gunby-Mann ha dicho:
So any nontrivial model of both of these simultaneously will be something new!
EDITED: Already running in sizes 13 and 14 :fingers_crossed:
Giovanni Paolini (Dec 11 2024 at 23:06):
Bruno Le Floch said:
Is it clear that we need non-commutativity to get interesting 677 models? It seems easier to explore if the carrier is simply a finite abelian group.
I used Gurobi to look for translation-invariant 677 models of the form on for (not sure if these are ruled out by previous considerations).
For an arbitrary (bijective) , such models exist only for and ; and the known linear models have this form, with on and on .
By additionally imposing that has no fixed point, there is no such model at all for .
Zoltan A. Kocsis (Z.A.K.) (Dec 12 2024 at 00:37):
Ben Gunby-Mann said:
Possibly interesting to note (not hard to show but on my phone now) is that 677+513 has no nontrivial commutative linear models. So any nontrivial model of both of these simultaneously will be something new!
The unique 5x5 model of 677 already satisfy 513, Said model is also linear over , with . So the "nontrivial" clause says that this is the only linear model of 677+513, right?
Ben Gunby-Mann (Dec 12 2024 at 02:09):
Zoltan A. Kocsis (Z.A.K.) said:
Ben Gunby-Mann said:
Possibly interesting to note (not hard to show but on my phone now) is that 677+513 has no nontrivial commutative linear models. So any nontrivial model of both of these simultaneously will be something new!
The unique 5x5 model of 677 already satisfy 513, Said model is also linear over , with . So the "nontrivial" clause says that this is the only linear model of 677+513, right?
Ack, you’re right of course. I accidentally did it as if beta is a primitive 5th root of unity in case 1, instead of the negative of that.
I think the correct statement you get from taking linear combinations of the polynomials is that the only nontrivial commutative linear models are Type 1 models in characteristic 5 (which must be of the form 2x-y, as you said).
Terence Tao (Dec 12 2024 at 02:33):
More negative results: the implication is immune not only to the cohomological extensions , but even to the more general piecewise affine extensions , at least when extending by a field. Given , we know that to solve 255, we need to find such that . Assuming the base already obeys 255, we can find such that , and then we are done unless vanishes, so that is independent of . But in that case, we apply 677 to see that for any one has
and use the aforementioned invariance (and the fact that when , by left cancelling ) to conclude that
but this contradicts left-invertibility.
Ben Gunby-Mann (Dec 12 2024 at 04:54):
Ben Gunby-Mann said:
Zoltan A. Kocsis (Z.A.K.) said:
Ben Gunby-Mann said:
Possibly interesting to note (not hard to show but on my phone now) is that 677+513 has no nontrivial commutative linear models. So any nontrivial model of both of these simultaneously will be something new!
The unique 5x5 model of 677 already satisfy 513, Said model is also linear over , with . So the "nontrivial" clause says that this is the only linear model of 677+513, right?
Ack, you’re right of course. I accidentally did it as if beta is a primitive 5th root of unity in case 1, instead of the negative of that.
I think the correct statement you get from taking linear combinations of the polynomials is that the only nontrivial commutative linear models are Type 1 models in characteristic 5 (which must be of the form 2x-y, as you said).
To be explicit about this, 513 implies that for commutative linear models and , so as long as we're in an integral domain, either we have the model (which doesn't satisfy 677) or . In case 2, b is both a root of and , and since the model must be trivial. However, in case 1 we have and , which has solutions only over characteristic 5 (similarly, ). In characteristic 5, , so again if we are in an integral domain the only root is , and we are left with the solution , as mentioned. So this is the only linear solution in a commutative integral domain. Not sure what happens if we drop either the commutativity or the integral domain condition, though.
Possibly also interesting here is 4599, which @Jose Brox mentioned. It has no nontrivial models which are both left- and right-cancellative (as then would imply ), so this actually does have the property that any nontrivial model of both 677 and 4599 together would be something notably new.
Jose Brox (Dec 12 2024 at 12:40):
Reporting some "fieldwork":
1) The only other equations (up to 4694) that can be added to 677+513 without provably implying 255 are:
- 411
x = x * (x * (x * (x * x)))
, which is just 513 with . - 4380
(x * x) * x = x * (x * x)
, which is implied by 677+513 (put and cancel on the left twice). - 3659
x * x = (x * x) * (x * x)
, which doesn't seem to be implied by 677+513 (plus left bijectivity and not always solvable), survives 30min in Prover9.
I have checked 677+513+3659 (plus left bijectivity) against 255 with Prover9, Vampire, and Vampire in CASC mode, for 30min each without getting a proof, so it seems a safe combination to take.
2) We also know that a model of 677+513 against 255 must have size at least 14 [UPDATED].
3) Other idea I have tried: I have looked at models of 513 against 255, and it turns out that they allow "complete failure" of right injectivity, i.e., there are models satisfying . As we already know this doesn't work with 677, and neither does it if all rows of the multiplication table are equal but one; but if it is all rows but two,
all x all y all z ((x!=0 & x!=1 & z!=0) -> x*y = z*y),
then the problem 677+513+3659+most rows equal (with left bijectivity) survives 30min in Prover9 (I'm looking for models of size 13 now).
(Deleted, silly comment)
4) On the other hand, 577+4599 against 255 (plus the extra clauses) progresses faster: any model must have size at least 17. This is somewhat suspicious, as problems that exhaust sizes quick tend to don't actually have models (i.e., the implication can be proven in those cases), but the progress is not that fast. In any case, I have tried to prove the implication without success for 30min with Vampire and Vampire-CASC (but Vampire in normal mode exits quickly, only saying "killed" :melting_face: ), and for 3h in Prover9 (still running, just in case).
Terence Tao (Dec 12 2024 at 21:09):
I managed to convert the greedy construction of a 677 magma into a Kisielewicz type model (which I believe to in fact be a free 677 magma (or at least contain such a free magma as a submagma), though I have not proved this). Unfortunately, it is infinite and I see no way to convert it to a finite model, but I report it here in case it somehow is helpful.
The carrier is the positive integers . We will build the multiplication table recursively, one row at a time: thus to define for a given we assume that has already been defined for all . The multiplication rule is then
Rule. If for some , then . Otherwise, .
Note that there is only one possible choice of that can be assigned to in the former case (namely, the number of times divides ). Also, by construction in that case and are both less than , so to evaluate the rule one only needs to compute products with . So the rule is recursively well defined. Intuitively, for "most" , will be larger than and "remember" all the information about and (this is a capability that only seems possible in infinite models), but for some exceptional , will be smaller than , and return the number of times divides instead. Because of this, can become for certain (and specifically of the form , which is where 677 will come from.
From definition we have the following property:
Lemma 1: For any , we either have , or with . In particular, in both cases we have .
From this and a somewhat involved case analysis we have
Lemma 2: For any , we have .
Proof: Write , , and , then we wish to show . Suppose for contradiction this were not the case, then by Lemma 1 we have . From Lemma 1 again we have and , hence . Since , we conclude from Lemma 1 that ; comparing with our previous formula for , we conclude and . From Lemma 1 we have , , and . Thus only can be the largest of , so and hence by Lemma 1. Since we then have by Lemma 1, hence , contradicting Lemma 1.
Remark: the ability to prove this lemma roughly corresponds to the ability to close the greedy argument when constructing 677 magmas, where in both cases the point is that no "unexpected collisions" show up to derail things.
Now we can verify 677:
Lemma 3: For any we have .
Proof: By Lemma 2 and the multiplication rule, it suffices to show that . From Lemma 1 we have and , hence , as required.
From Lemma 1 we have for all , so in particular 255 fails in this model.
Giovanni Paolini (Dec 12 2024 at 22:35):
I continued the search for translation-invariant 677 models of the form , as suggested by @Bernhard Reinke, across all groups of order up to 17. Aside from the previously identified cases, namely and , only supports such models. In addition, for all such models, has a fixed point (so 255 holds).
This is an example of a translation-invariant 677 model over :
[0, 4, 14, 10, 2, 6, 12, 8, 5, 1, 11, 15, 7, 3, 9, 13]
[5, 1, 11, 15, 7, 3, 9, 13, 0, 4, 14, 10, 2, 6, 12, 8]
[12, 8, 2, 6, 14, 10, 0, 4, 9, 13, 7, 3, 11, 15, 5, 1]
[9, 13, 7, 3, 11, 15, 5, 1, 12, 8, 2, 6, 14, 10, 0, 4]
[6, 2, 8, 12, 4, 0, 10, 14, 3, 7, 13, 9, 1, 5, 15, 11]
[3, 7, 13, 9, 1, 5, 15, 11, 6, 2, 8, 12, 4, 0, 10, 14]
[10, 14, 4, 0, 8, 12, 6, 2, 15, 11, 1, 5, 13, 9, 3, 7]
[15, 11, 1, 5, 13, 9, 3, 7, 10, 14, 4, 0, 8, 12, 6, 2]
[13, 9, 3, 7, 15, 11, 1, 5, 8, 12, 6, 2, 10, 14, 4, 0]
[8, 12, 6, 2, 10, 14, 4, 0, 13, 9, 3, 7, 15, 11, 1, 5]
[1, 5, 15, 11, 3, 7, 13, 9, 4, 0, 10, 14, 6, 2, 8, 12]
[4, 0, 10, 14, 6, 2, 8, 12, 1, 5, 15, 11, 3, 7, 13, 9]
[11, 15, 5, 1, 9, 13, 7, 3, 14, 10, 0, 4, 12, 8, 2, 6]
[14, 10, 0, 4, 12, 8, 2, 6, 11, 15, 5, 1, 9, 13, 7, 3]
[7, 3, 9, 13, 5, 1, 11, 15, 2, 6, 12, 8, 0, 4, 14, 10]
[2, 6, 12, 8, 0, 4, 14, 10, 7, 3, 9, 13, 5, 1, 11, 15]
In this example, the permutation is a product of three 5-cycles:
= (0)(1 4 2 14 9)(3 10 11 15 13)(5 6 12 7 8).
The elements of are indexed in such a way that the group operation is the bit-wise sum mod 2. In particular, the five elements in each cycle have sum 0. All of this strongly suggests that we are in fact looking at a linear model over , with acting as multiplication by a 5-th root of unity, though I have not checked it.
Interestingly, the time taken by Gurobi to prove non-existence of models differs significantly across the remaining groups of order 16: 7 groups are "hard" (~1 hour), 5 are "easy" (< 2 minutes), and 1 is "intermediate" (~10 minutes).
Jose Brox (Dec 12 2024 at 23:35):
Jose Brox ha dicho:
3) Other idea I have tried: I have looked at models of 513 against 255, and it turns out that they allow "complete failure" of right injectivity, i.e., there are models satisfying xy=zy. As we already know this doesn't work with 677, and neither does it if all rows of the multiplication table are equal but one; but if it is all rows but two,
all x all y all z ((x!=0 & x!=1 & z!=0) -> x*y = z*y),
then the problem 677+513+3659+most rows equal (with left bijectivity) survives 30min in Prover9 (I'm looking for models of size 13 now).
This doesn't work: already with 2 rows equal, there seems to be no finite models (we can go up to size 100 quickly). The fact that a proof is not found probably means that there are infinite models satisfying the property.
5) A similar, interesting thing happens with 4343 x(yy) = y(xx)
:
There are no models of 4343, left bijectivity and not always solvable up to size at least 237 :scream: ... (this is true even without 677!) ...
...but Vampire-CASC says that the problem is satisfiable (even when a bunch of finiteness conditions are thrown in), what points to the existence of infinite models.
Is there some clear reason why this is the case, why imposing together with left bijectivity forces a solution to for all in the finite case?
(NOTE: The model search is so fast thanks to choosing selection_measure 1 in Mace4, so it could be interesting to replicate the Mace4 process in this case and see why the multiplication table is so easily seen to be impossible to fill with these conditions. Vampire's finite model builder is also fast, but slower than Mace4 with this configuration).
Jose Brox (Dec 12 2024 at 23:47):
Terence Tao ha dicho:
One somehow wants to choose an f with a special property that the propagation rules of Axiom 1 and Axiom 2 (i.e., the functions (y,x,z)↦(z,y,f(x,y)) and (y,z,x)↦(x,f(x,y),z)) obey a lot of algebraic relations that cuts down on this complexity
Not sure if this is interesting, but I've looked for in the form of another magma expression. The only one in 2 variables up to degree 4 that doesn't seem to get the implication to 255 is . I have checked that there are no models of 677+ against 255 up to size 13 (included).
In degree 5 we have 64 candidates that stand against 255 for 1min in Prover9:
candidates
I haven't run the search for degree 6 or higher, but if we impose 513, since then , from equating 513 to 677 through we get
.
Douglas McNeil (Dec 13 2024 at 00:07):
Given the size of counterexamples lately it's hard to put too much weight on the resistance this one's putting up, but am I the only one wondering if this one's actually true?
Are there properties of finite magmas we haven't invoked yet, or consequences of them that ATPs would have trouble detecting?
Zoltan A. Kocsis (Z.A.K.) (Dec 13 2024 at 00:07):
Okay, I have some questions at this point.
The possibility that 677 has very few models in general seems like a major obstacle to me, especially when trying search based approaches. If 677 has only, say, 6 models of order , then the fact that our searches fail to find models of certain combinations if equations really doesn't tell us much.
I wish I could confirm my hunches myself, but the thread has grown too long to search efficiently given my current time constraints, and I suspect that many of you have tacit knowledge not written up here, so I think I'll ask a series of questions instead. Hopefully, the answers will help refine the main axis of effort instead of just satisfying my personal curiosity.
- Do we know any finite models of 677 that are not outright cancellative? If not, do we have proof (or at least some heuristic) telling us not to expect such models? NB if we cannot expect such models, then imposing 4599 and similar equations whose models tend to be very noncancellative is perhaps not that promising.
- Do we know any finite models of 677 that have even order? If not, do we have reason not to expect such models?
- Do we know two non-isomorphic finite models of 677 that have the same order? If not...
- How many different models do we know? How many models of order less than 15?
Matthew Bolan (Dec 13 2024 at 00:11):
For question 2, there are linear models of even order, for example over . The answer to question 3 is yes, for example there are two non-isomorphic linear models of order 7. For question 4, AFAIK we only know linear models and cohomological extensions of linear models, and I think there are only linear models known below order 15. I'd have to check which linear models are isomorphic in order to give an exact count.
Zoltan A. Kocsis (Z.A.K.) (Dec 13 2024 at 00:28):
Douglas McNeil said:
Are there properties of finite magmas we haven't invoked yet, or consequences of them that ATPs would have trouble detecting?
Technically, proofs that some implication always holds in a finite magma can be arbitrarily difficult (which doesn't mean that we should expect this particular problem to be difficult; indeed, I don't think this one's true). One could look up famous such proofs (starting with Artin-Zorn perhaps?) to see what sorts of properties they invoke, and whether we're missing any of them.
Bruno Le Floch (Dec 13 2024 at 01:00):
Summary of what we know.
- All known finite models are linear or cohomological extensions thereof, typically nonlinear.
- List of linear models on Z/pZ for primes p up to 500. More general (e.g., non-commutative) linear models are mostly understood.
- 677 implies left-cancellative. Finite linear 677 implies right-cancellative too. Cohomological extensions keep cancellativity. 677 and cancellativity implies 255.
- Assuming 677, equation 255 is equivalent to
∀x ∃y y*x=x
. Piecewise affine extensions by a field preserve that property so cannot produce counterexamples. - 677 is incompatible with
0!=1∧∀y,y*1=0
—also incompatible with0!=1∧∀y,(y=1 or y*1=0)
by a quick prover9 run I just did and also with∀x(x=0 or x=1 or (x*0=1 and x*1=0))
. - 677 together with any of {411,513,623,...} does not imply 255. —particular interest for 513 combined with translation-invariance (no new model for n≤16) or with 3659.
- Some hope to use translation-invariant models.
- Some inconclusive usage of rule sets and a concrete Kisielewicz type infinite counterexample.
- An idea of using a relaxed base magma..
Bruno Le Floch (Dec 13 2024 at 01:10):
Some other equations with very few finite models seem to have a good reason for that. The cardinal of finite central groupoids must be a square because the square of the adjacency matrix is an all-1 matrix. For weak central groupoids we have a conjecture that the cardinal is a square or twice a square. Is there anything special about the cardinal of 677 models, or the size of cosets, etc?
For , namely , we have hence , which is -independent. For any , we get by left-cancellativity, so the map is injective. In particular, has at least as many elements as for any . This generalizes the incompatibility with 0!=1∧∀y,y*1=0
because so all have to be surjective, which is wrong for . But it does not capture the other related incompatibilities listed in my previous post. There is probably something more conceptual tracking the whole set of and .
Matthew Bolan (Dec 13 2024 at 01:20):
It is very likely that the cohomological extensions are not linear I think. If they are it's probably good to know, as it means that something about 677 really is forcing linearity. I'd be very surprised if even the first example in my file, this order 25 magma , were linear.
Matthew Bolan (Dec 13 2024 at 01:24):
I'll also comment that 1076 has very few finite models, but I am not aware of a good reason for this.
Terence Tao (Dec 13 2024 at 01:26):
One consequence of linearity is that the operators , being translations, commute with each other and with the (assuming right invertibility in the latter case). So this may be one test to verify if a given magma is linear or not.
Matthew Bolan (Dec 13 2024 at 02:00):
Hmm, the order 25 one can't be proven non-linear by that test, so perhaps it is some linear model over after all is only one dimensional in that case. Other models in the file are able to be proven non-linear via that method though.
Matthew Bolan (Dec 13 2024 at 02:05):
Bruno Le Floch (Dec 13 2024 at 09:16):
I was a bit quick concerning the piecewise affine models: Terry Tao's argument only proves immunity to piecewise affine extensions by a field. I don't see how to rule out a case where would be non-invertible but non-zero. I've edited my summary above to reflect that information. This is one of our best hopes. In particular the proof that finite linear 677 implies cancellative clearly does not go through when you have multiple and .
Terence Tao (Dec 13 2024 at 18:54):
I guess I should share some inconclusive attempts to study these sorts of extension models then. We know that the base should contain non-idempotents, so the order 5 magma isn't a useful base; it's the two order 7 models that offer the first shot at some non-trivial constructions. I'll arbitrarily choose the model on (the other model has broadly similar behavior). One could consider general extension models on carrier for some binary operations to be chosen later. The rule 677 then becomes
for all and . This is 49 equations involving 49 different binary operations - not appetizing! However, the case doesn't interact with any other case, and is just saying that is a submagma of . As for the other 48 cases, one can impose a projective symmetry where takes place in the projective line with the convention that for any non-zero . Then we get to divide by six, and end up with eight equations in eight unknowns , of the form
for . More explicitly, one has
(if I did not make any mistakes). Note that the most important case here for the purposes of testing 255 is when , so that and so one is interested in seeing whether the equation admits solutions for every . The equation
together with the left-cancellability of and will tell us that one cannot have depend only on ; there has to be some -dependence, which in the case of piecewise linear models over a field implies solvability and hence 255. (This is what led me to my previous result about how the implication is immune to piecewise linear models extending by a field.) In fact this argument tells us for linear models that the kernel of can at most be the cardinality of the square root of the cardinality of .
One could just write down the linear ansatz (ignoring for now any lower order term ) and try to solve the resulting system of sixteen quartic equations in sixteen non-commutative unknowns, but I don't know if this is even computationally feasible. We do have the known solutions where , is independent of and solves the original system of equations, but this is presumably only a small subset of all possible solutions here.
One amusing thing about the above system is that only appears in two equations:
This raises the possibility that this particular operation is more "mutable" than the others, and one could create models in which all the other , are standard operations (e.g., a standard linear model ) and is modified from the linear model. On the other hand, since 255 concerns rather than , such modifications don't actually bring us any closer to refuting 255.
I wish we had a simpler model to play with than the above system of eight equations. If the base magma was translation-invariant then we could play with a translation-invariant model instead of a projection-invariant one, but the translation-invariant models that I know of are all idempotent and therefore not useful to us.
Bruno Le Floch (Dec 13 2024 at 21:46):
A curious ramification. Linear models over Z/pZ (p prime) are nicely classified between type 1 with and a primitive 10th root of unity and , and type 2 with and and and arbitrary . The parameter can be set to zero by shifting magma elements in all models except one which is both of type 1 and 2, namely . This number comes from . That might be a hint to this case being slightly more flexible than usual linear models. In particular it is a non-idempotent translation-invariant model. That said, it is big, so I'm not sure it is an improvement over the 7-element magmas as a base.
Terence Tao (Dec 13 2024 at 22:48):
Thanks for this. Taking for instance (I think all other non-constant choices of can be rescaled to this one and taking the translation-invariant ansatz , I get a system of 31 equations in 31 unknown operations :
for . To solve requires on the base, so one is interested in seeing whether is solvable for each . For this choice of we have so the previous argument blocking from being independent of still applies.
I don't see an obvious further structure here to reduce the complexity of a system of 31 equations in 31 unknowns while still having a decent chance at solvability. One could maybe consider an ansatz where the vary linearly in (in some field of characteristic 31), but I think this creates 8 equations in 4 unknowns, so very unlikely to be solvable.
Bruno Le Floch (Dec 14 2024 at 00:43):
Your projective model is more promising than the 31 equation one. I've checked that your set of 8 equations for the projective model is correct. A commutative linear version of that () is not ruled out I think?
It might be barely tractable. The equations are of the form and with various indices. The first type of equations give invertibility of and can be solved for assuming that differs from and from . (If we decide to violate that, then we get two free but two constraints on from this set of equations.) The second set of eight equations becomes 25th-degree polynomials in with a total of 210 terms, but at least we only have variables left.
Surprisingly, the equations are invariant under scaling by some factor and by the inverse factor, so we can normalize . There are also some discrete scalings of other by fourth roots of unity.
Bruno Le Floch (Dec 14 2024 at 01:10):
Ah, nooo!! :sad: Yet another immunity, this time to all (finite) piecewise affine extensions of the kind we consider here, so . Namely, if the base magma obeys 255 the extension also does.
Pick some . By 255 on the base we have some with , so hence as we already observed. Then equation 677 implies
where dots denote unimportant indices. Crucially, the same left-multiplication map appears twice. If is not injective, then two different (say, ) will have equal left-multiplications, but then we can cancel all these by left cancellativity so eventually . Thus is injective. By finiteness, it is surjective, so there exists such that . Namely 255 holds.
I think this kills any hope based on anything linear. Are there some extra twists that I forgot to account for?
I'm starting to think that the implication might hold. Maybe we should try to track how much information has. It must not be too invertible nor too forgetful.
Terence Tao (Dec 14 2024 at 04:02):
Wow, that's a pretty strong immunity. Well, I'm glad you found it before we decided to set up a massive calculation that was doomed to fail...
For the more general extension models , what this shows is that whenever , the left multiplication maps have to depend injectively on : . In piecewise affine models, these left multiplication maps are translations (composed with a fixed invertible map), so injectivity and finiteness forces all translations to be attained, and then we can solve . So if we want to keep an extension model, these left multiplication maps have to be genuinely more complicated than translations, but then it's much less likely that the required equations are going to hold.
Another way of thinking about it: one feature of linear models is that if agree at one location, they in fact agree at all locations: . [Geometrically: two lines of the same slope are either parallel or identical.] So injectivity of implies injectivity of for any fixed , i.e., the are injective, hence invertible by finiteness, and we get 255. So we need operations for which left-multiplication by different elements can agree in some locations but not in others.
Forgetting about extensions for the moment, maybe this suggests semilinear models such as that are linear in the second variable but not the first. Ugh, but this particular model just leads to a total mess when one computes 677.
There's something very special about linear (or affine) binary operations - the composition of linear operations is again linear, and this is essential in keeping the number of equations and the number of unknowns matching when considering an equation like 677. If one starts looking at quadratic maps, for instance, suddenly one gets way more equations than unknowns when one matches coefficients. If there was some other class of binary operations than linear or affine for which operations such as had the "same" complexity as the original map (in that they are described by exactly the same number of parameters), then we might have a shot, but I can't think of any other candidates... [EDIT: Okay, translation invariant models are one other candidate of this type. And I guess, trivially, the entire class of arbitrary binary operations are also of this type.]
Terence Tao (Dec 14 2024 at 06:14):
Reporting a very silly thing I tried, just to take it off the table: instead of trying to extend or enlarge a base magma, I tried for an embarrassingly long amount of time to experiment with the reverse operations of quotienting a magma by an equivalence relation, or restricting to a submagma. For instance I was poking around to see if the linear magma model had any quotients that were not linear. But then I realized that any law such as 255 would be automatically preserved by passing to quotients or submagmas, so there is probably no point in trying to use such constructions (unless perhaps as a base magma for some construction for which we don't currently have an immunity result). [EDIT: there is perhaps a possibility that one could start with a magma that doesn't obey either 677 or 255, then perform a quotienting to enable 677 but not 255, which might work if we had some useful way of constructing a magma that "nearly" obeys 677, but I have no proposal in this direction.]
Bernhard Reinke (Dec 14 2024 at 07:43):
Bruno Le Floch said:
Ah, nooo!! :sad: Yet another immunity, this time to all (finite) piecewise affine extensions of the kind we consider here, so . Namely, if the base magma obeys 255 the extension also does.
Pick some . By 255 on the base we have some with , so hence as we already observed. Then equation 677 implies
where dots denote unimportant indices. Crucially, the same left-multiplication map appears twice. If is not injective, then two different (say, ) will have equal left-multiplications, but then we can cancel all these by left cancellativity so eventually . Thus is injective.
Maybe I am confused, but shouldn't left cancellativity give you that is always injective, not ?
Bruno Le Floch (Dec 14 2024 at 09:45):
Bernhard Reinke said:
Maybe I am confused, but shouldn't left cancellativity give you that is always injective, not ?
What you say is correct, but the argument I meant is that if for , and if the two coincide, then we have that are equal for . This takes the form
and we can cancel any from this equation to get that the two agree. We deduce from that that .
Bernhard Reinke (Dec 14 2024 at 09:53):
Oh I see, thanks for the explanation!
Zoltan A. Kocsis (Z.A.K.) (Dec 14 2024 at 11:28):
Terence Tao said:
But then I realized that any law such as 255 would be automatically preserved by passing to quotients or submagmas, so there is probably no point in trying to use such constructions [...] if we had some useful way of constructing a magma that "nearly" obeys 677
Random thought: we know at least one infinite model where 677 holds but 255 fails. IIRC it's obtained by a greedy construction, so I guess it'd be hard to tell whether it admits finite factors of the relevant kind.
Terence Tao (Dec 14 2024 at 15:46):
That's a good point. It's possible that if we understand the infinite model better then we could figure out how to place a cofinite equivalence relation on it that one can quotient by to create a useful finite 677 model. Though this hasn't been super successful in group theory - we completely understand what the free group on a fixed set of generators looks like, but this doesn't exactly make it easy to generate finite groups.
In group theory we have this extremely useful family of groups coming from permutations on an arbitrary set, with Cayley's theorem guaranteeing that all the other groups are basically subgroups of this model. (Similarly for monoids and functions on an arbitrary set.) There's also the group of general linear transformations of vector spaces, leading to the extremely rich and useful field of representation theory. I guess there's no reason to expect a similarly useful family for 677 though. For some other laws, we had the left-absorptive or right-absorptive models which were also useful (though more as base models to modify than models to take submagmas of), but again these are not available here. Instead we just have a twp strange families of linear models,some extensions of them, and a handful of infinite models...
Pace Nielsen (Dec 14 2024 at 19:32):
I've been playing with the translation-invariant models, but no real progress. Setting in some group, we have injectivity of left multiplication
Setting , this translates to
Thus, is injective, and so bijective. Hence, the functional equation for can be rewritten as
Eq513 is equivalent to , which would mean that under eq513 takes the carrier set and decomposes it into cycles of lengths 1, 2, 4. Vampire says that no cycle of length 1 is allowed if 255 fails. So the carrier set must have even cardinality, and it seems reasonable to just suppose that is a bunch of 4-cycles. I'm not sure if this would speed up searches using Mace4.
Terence Tao (Dec 14 2024 at 21:44):
I have a tentative approach based on my previous suggestion to split up 677 into two equations
and
The vague idea I had is to somehow propose a candidate for first, and then use (1) and (2) to solve for . So we would like to understand the properties we want to have.
We can rewrite (1) in the form
and by left cancellativity we can similarly write (2) in the form
Thus both equations relate one entry of the multiplication table to another. But there is a difference in behavior between the two equations, as we shall now see.
Observe that the transformation in (1') is injective: given , one can recover by left cancellativity.
By finiteness, the transformation (1') must therefore be a bijection on the multiplication table. Among other things this means that is "equidistributed" in the sense that each element of is attained exactly times by .
If 255 fails at some , then is not surjective, hence not injective, thus for some . From (2') we then have , so , thus is not injective on columns. Intuitively, is "forgetting" some information about .
Furthermore, if 255 fails at , then for all , so from (1) we see that for all . Thus is not surjective on rows either, and must "forget" some information about as well as .
Now that is forgetting information about both and , we see that the transformation in (2') is non-injective: there are entries of the multiplication table, but this needs to somehow transform to fewer than entries .
So I started searching for candidate functions that were equidistributed, but which forgot some information on both inputs. My first candidate was the natural central groupoid law, where for some finite set and ; note that this is equidistributed while still forgetting information from both inputs. The equation (1) can be solved in this case as follows. Suppose one has located some subset of which is invariant under shifts , and is a bijection when projected to any four of the five components. (For instance, if was an abelian group, one could take to be the hyperplane obeying , but many other choices were possible). If one then defines by the law
for all , one can check that this operation is well-defined and obeys (1') and hence (1). [Conversely, one can show that all solutions to (1') for this choice of are of this form; this is a fun little exercise, coming from iterating (1') five times.] Unfortunately, one cannot make it obey (2'). Inserting the above law into (2') one obtains
This law is not directly consistent with the previous one since in general, but I don't see this as a fatal obstacle because one could perhaps modify the law (and ) on a small set to get around this. The more serious problem is that the left-hand side only constrains three coordinates out of the tuple , leaving unconstrained, so this equation is necessarily inconsistent, in a way that I don't see easy to fix with small modifications.
One can try more complicated constructions of this type, but so far I have run into similar obstructions. Suppose for instance that now and one has a subset of which is shift-invariant and a bijection when projected to any six coordinates. We can similarly define
for , and this will obey (1') with
If we insert the above law into (2'), we obtain
Again, this is not directly consistent with the previous law, but only covers a small minority of the multiplication table ( of the entries) so I don't see this as fatal. Again, we have the more serious issue that upon fixing , remains unconstrained.
I'm still experimenting with this paradigm, so I don't know yet whether these difficulties can be overcome, or conversely whether they are hinting at a way to establish the positive implication, but I thought I would report this work in progress.
Giovanni Paolini (Dec 14 2024 at 22:22):
Pace Nielsen said:
I've been playing with the translation-invariant models, but no real progress. Setting in some group, we have injectivity of left multiplication
[...]
Eq513 is equivalent to , which would mean that under eq513 takes the carrier set and decomposes it into cycles of lengths 1, 2, 4. Vampire says that no cycle of length 1 is allowed. So the carrier set must have even cardinality, and it seems reasonable to just suppose that is a bunch of 4-cycles. I'm not sure if this would speed up searches using Mace4.
If I am not mistaken, then a translation-invariant model satisfying 677 + 513 would not satisfy 255? (Because we know that 677 + 255 require to have a fixed point.)
The size-5 model over is translation-invariant (with ) and satisfies 677, 513, and 255, though.
Bruno Le Floch (Dec 14 2024 at 22:28):
Giovanni Paolini said:
The size-5 model over is translation-invariant (with ) and satisfies 677, 513, and 255, though.
What you write is correct. What Pace Nielsen meant is that if has a fixed point then 255 is satisfied. A putative translation-invariant counterexample to 677+513⇒255 must thus be such that cycles are of lengths 2 and 4, only.
Terence Tao (Dec 15 2024 at 16:05):
Not much positive progress on my previous approach, but I at least have a model problem to propose:
- Can one build a finite left-cancellative magma that obeys 677 at least 99% of the time (thus, the 677 equation holds for at least 99% of pairs ) but for which right surjectivity only holds 1% of the time (i.e., the equation is solvable for at most 1% of pairs )?
(The reason why I ask for failure of right surjectivity rather than failure of 255 is that it is easy to make the one-variable equation 255 fail 100% of the time just by modifying the multiplication table on the diagonal, so I need a two-variable condition instead.)
The hope is that if such a counterexample can be found, then one can modify the example on a small portion fo the multiplication table to exactly solve 677 but fail to solve 255. (This may be related to a discussion @Zoltan A. Kocsis (Z.A.K.) and I had back in October on magmas that nearly obey a given law.)
Anyway, to construct such a counterexample, it suffices to find a left-cancellative operation on a finite carrier that does two things:
- The expression "forgets" information about , in the sense that at most 1% of pairs in can be of the form .
- The expression forgets the same information about , that is to say for a given , one has if and only if . (One could maybe tolerate a a failure of this if-and-only-if 1% of the time for the purposes of this model problem.)
Then if one modifies the operation on the small number of pairs so that (maybe doing a few more modifications to preserve left cancellativity), one obtains 677 basically 99% (or maybe 98%) of the time while (probably) violating right surjectivity quite a bit (because of all the collisions .
So far I can get constructions where and both lose a comparable amount of information about , but I can't get them to lose the same information, which is the main remaining obstacle. Consider for instance a linear model where are not commutative and possibly non-invertible linear transformations on . We already have ruled this model out for the original problem, but it also runs into problems here. In this model, has to be invertible for left-cancellability, and we have . If is non-invertible then there will be some loss of information about , coming from the kernel of . We also have , so information is lost here if is non-invertible, coming from the kernel of . But, unfortunately, the two kernels cannot coincide: if lies in the kernel of both and then it lies in the kernel of , contradicting the invertibility of .
Another model I played with was a model where was a non-abelian group and the operation was conjugation, , which is left-cancellative but not right-cancellative when is non-abelian. Here can lose some information in but it is hard to discern exactly what information is lost; meanwhile loses information in relating to the centralizer of . It doesn't look like one can create a group where the information lost is the same. One can play with other words here than the conjugation word but there doesn't seem to be an obvious way to make the two information losses resemble each other.
I'm not throwing in the towel yet, but I think there is a possibility that we may eventually have to "declare victory" on the ETP without necessarily closing off this final implication, and pose it in the paper as an open problem. Still, a success rate of 100.00% on the original graph and 99.99999% on the finite graph isn't exactly a terrible record...
Terence Tao (Dec 15 2024 at 16:15):
By the way, here is a linear model that I found somewhat instructive. Let be a field of large prime order , let be a finite subset of with and its translate by one disjoint, but and , having non-trivial intersection, e.g., one can take . Take the carrier to be , i.e. the space of tuples taking values in . Then take the following (linear) magma operation: given any polynomial of degree at most , set
This is a well-defined map due to the disjointness of and and the Lagrange interpolation formula; it is left-cancellative but will not be right-cancellative since and overlap, so loses information about . It is easy to see that the function defined previously can be given by
Because overlaps with , will lose information about : knowing and only specified on the set which has cardinality strictly smaller than the degrees of freedom of , whereas knowing and specifies all degrees of freedom. I tried for a while to make the information losses in and line up until finally realizing that all linear models are obstructed by the argument given previously.
Terence Tao (Dec 15 2024 at 23:02):
Here is an amusing reformulation of 677. Given a left-cancellative magma , define a good sequence to be a sequence obeying the recursion . By left-cancellativity, every pair extends uniquely to a good sequence, which looks like
(with the bar being notation for indicating the element of this sequence indexed by zero). We call this the good sequence generated by .
Let be the set of good sequences. Given any integers , let be the function that takes a good sequence to the good sequence generated by . Thus for instance is just the shifted sequence
and is an invertible transformation on . The maps can also be seen to be invertible.
However, the other can be non-invertible. (For instance, the invertibility of is equivalent to right cancellability.)
The law 677 can now be rewritten as . Indeed, if one starts with the good sequence generated by , i.e.,
then is the sequence
so is the sequence
and hence is the sequence
which matches precisely when , i.e., when 677 holds for .
In the equation , the maps and are invertible, so the equation implies that and are "equally non-invertible" in some sense. This is another way of stating the previous assertion that and "lose the same information in ).
Specifying a left-cancellative operation is equivalent to specifying a class of good sequences that is shift-invariant, and such that any pair uniquely generates a good sequence. Such a class then generate the operators. But I don't see a good candidate for a class for which we have a hope of matching with (other than ones coming from 677 magmas that we already know how to construct, of course).
Bruno Le Floch (Dec 16 2024 at 11:36):
I want to focus on some other parts of the project for a bit (especially Higman-Neumann), but am hoping to return here in two weeks or so, near the very end of the project. There is still a bit of time as the formalization work is not done yet.
I like your model problem, but so far did not have any success. On the other hand I think your reformulation in terms of complicates things.
Central groupoids, which are subject to a three-variable equation (hence expected to be more restrictive), can often be modified by a "switching" operation that acts very simply on the graph. In an n-element magma it affects sqrt(n) entries in the multiplication table if I remember correctly. So it wouldn't be crazy to hope that for our two-variable equation 677 we could also modify a large linear magma "by hand" in a reasonable number of places to get a new magma that violates 255. I don't think we've explored this enough. The problem is that 677 is very mixing somehow.
Maybe we could learn something about sizes of cosets, and the flow of information, from having a model that is not right-cancellative. However, the only current hope to produce them is piecewise affine models which involve solving huge systems of nonlinear equations.
I don't think we've ruled out models of the form that are linear in one of the two arguments only. We could even try something like with or a similar tiny set.
Amir Livne Bar-on (Dec 16 2024 at 11:43):
I ran some searches with mace4. Assuming I got the syntax right, there are likely no translation-invariant models with . Mace4 searches up to order 120 in under 30 seconds, then it reaches its memory limit and gives up. I don't know an argument why it's impossible to have such models with a non-trivial group.
Searching with does do some work, I'll let it run for a few hours.
Attaching here my file: eq677.in
Amir Livne Bar-on (Dec 16 2024 at 11:52):
Mace4 is magical, with the right selection order it also eliminated up to order 120
Jose Brox (Dec 16 2024 at 12:35):
Amir Livne Bar-on ha dicho:
Mace4 searches up to order 120 in under 30 seconds, then it reaches its memory limit and gives up.
I've extended the computation (allocating more memory with
assign(max_megs, 2000).
) to confirm that there are no models up to size 216 (in 300s).
Amir Livne Bar-on ha dicho:
Mace4 is magical, with the right selection order it also eliminated f4=1 up to order 120
Do you mean selection measure, or did you actually find a selection order which is better than 2 for this problem? (I've never encountered such a problem before!). Can you share the input file for this one too? Thank you!
Amir Livne Bar-on (Dec 16 2024 at 12:41):
Selection measure 3, and using selection order 2 (which might be the default).
I edited the file and I didn't save a version to reproduce, but it's the same as the file except for these changes. The run took 6 or 7 minutes.
Jose Brox (Dec 16 2024 at 12:48):
Amir Livne Bar-on ha dicho:
I ran some searches with mace4. Assuming I got the syntax right, there are likely no translation-invariant models with f2=1.
In fact, from the premises Prover9 derives FALSE (it arrives at f(inv(f(0)) = inv(f(0))
), so we have proof that there are no translation-invariant models with and for all .
Bruno Le Floch (Dec 16 2024 at 13:03):
If I understand correctly, means . We know that this assumption (or even the weaker ) together with 677 and finiteness implies 255, even without assuming translation invariance.
Indeed, (attempting to translate a prover9 proof) 677 with x,y
replaced by xx,x
and applying x(xx)=x
gives xx=x((xx)(xx))
hence (xx)(xx)=x
, then 677 with x,y
replaced by x,x
gives x(x((xx)x))=x=x(xx)
then left-cancellativity gives (xx)x=x
. This equals (xx)(xx)
so left-cancellativity gives x=xx
and we are done showing 255.
Bruno Le Floch (Dec 16 2024 at 13:04):
On the other hand Jose Brox didn't find a contradiction with 513 which in the present context is . So that's a worthwhile class of models to study.
Amir Livne Bar-on (Dec 16 2024 at 13:14):
My run with showed that it implies not only 255 but 2, i.e. no models (up to order 120, which Jose extended up to order 216)
Zoltan A. Kocsis (Z.A.K.) (Dec 16 2024 at 13:31):
I think at this stage it's worth considering the possibility that the implication might hold in the finite case (e.g. something like right-cancellativity holds over all finite models).
Perhaps the tools of classical universal algebra could help in such investigations? I mean things like subdirect representation, congruence lattices, characterizations of direct irreducibility.
Here's a concrete idea: If finite directly irreducible 677-magmas satisfy 255, then of course all finite 677-magmas do. Over certain algebraic structures, one can determine direct reducibility by counting solutions to equations. For example, a finite Heyting algebra is directly reducible precisely if the equation has more than 2 solutions (btw this is why all finite Boolean algebras have elements).
I wonder if 677-magmas admit any similar solution-counting characterization for direct reducibility. If so, these could be added as assumptions to Prover9 to see if they allow us to conclude e.g. right-cancellativity or 255.
Terence Tao (Dec 16 2024 at 16:28):
@Bruno Le Floch Yeah, the formulation was less useful than I had hoped. It does show that the maps and are "equally non-invertible" for 677 magmas in the sense that one can transform one to the other by separate invertible transformations of the domain and range. Indeed, using left cancellativity one can transform to , which by 677 is . Substituting we get the map , which after some rearranging gives .
In the specific case of on , the good sequences are the linear ones , and maps a linear sequence to the linear sequence . One can manually verify the identity in this case.
Somehow the problem is that this equation 677 is only barely solvable with finite non-trivial models; it seems very hard to find a construction in which there are more variables than unknowns (the cohomological approach comes the closest), but unfortunately all known constructions preserve 255. In particular, imposing more conditions on the magma seems to make it almost impossible to find any non-trivial model at all.
Terence Tao (Dec 16 2024 at 16:29):
By the way, not that it helps directly, but I was able to modify the previous Kisielewicz construction to describe the free 677 magma; details are in the blueprint.
Terence Tao (Dec 16 2024 at 16:50):
The final formalization of the outstanding implications for the infinite graph seems like a natural milestone to assess whether to "declare victory" on the project, regardless of whether 677->255 is resolved by then, but I suppose we can debate that (and/or hold a vote) when that day comes.
Bruno Le Floch (Dec 16 2024 at 17:15):
Terence Tao said:
The final formalization of the outstanding implications for the infinite graph seems like a natural milestone to assess whether to "declare victory" on the project, regardless of whether 677->255 is resolved by then, but I suppose we can debate that (and/or hold a vote) when that day comes.
It sounds reasonable indeed to declare victory at that point, since all the finite implications (except that one of course) have been formalized.
Bruno Le Floch (Dec 16 2024 at 21:14):
Equation 677 x = y ◇ (x ◇ ((y ◇ x) ◇ y))
is equivalent (in the finite setting) to equation 19855 x = (y ◇ x) ◇ ((y ◇ (y ◇ x)) ◇ y)
. There is a reformulation of 677 in terms of which looks somewhat similar, Equation 9321: x = y ⊙ ((x ⊙ y) ⊙ (x ⊙ (x ⊙ y)))
. However, I don't have much hope that it would be useful: linearity is preserved by passing from ◇
to ⊙
, right-invertibility as well ((∀y,z,∃x,x⊙y=z) ⇔ (∀y,z,∃x,y=x◇z)
), and the condition for 255 too ((∀y,∃x,x⊙y=y) ⇔ (∀y,∃x,y=x◇y)
). But maybe it inspires someone something.
Terence Tao (Dec 17 2024 at 02:52):
I can solve the model problem: given any , one can find a left-cancellative finite magma which obeys 677 for of pairs , but is highly non-right-invertible in the sense that only occupies of pairs.
We take a translation-invariant model for some invertible , with an abelian group. As previously computed, 677 becomes the equation
which we can rearrange as
or equivalently
To simplify the algebra we assume that is of exponent 2, to eliminate all the minus signs:
One should think of this as saying (among other things) that the functions and are "equally non-invertible".
We would like this equation (1) to hold of the time, while only takes values.
Note that (1) and the invertibility of implies that collisions in are equivalent to collisions in :
Conversely, suppose that (2) holds for all outside of an exceptional set of cardinality , and that only takes on values. This implies that also takes on only values. Then one can upgrade (2) to (1) (outside of an exceptional set of size ) by modifying on values (mostly on the values of , making some additional swaps as needed to maintain the invertibility of ). So we just need to construct a function that obeys (2) most of the time, while takes few values.
There are lots of ways to proceed here, I will take a piecewise linear model. Let be a large finite field of characteristic 2 (of size much larger than ) and let be a generator of the multiplicative group, thus the non-zero elements of are . I will take the carrier to be and the function to take the form
for all and some invertible linear transformations to be defined later. I don't bother defining on as this is only of the elements. The relation (2) then reduces the following: for of the , and all , we have
or equivalently
If we require each of the have exactly one eigenvector (up to scaling) with eigenvalue one, then will only take on about of the possible values, which is as desired, and the constraint (3) simplifies to asking that
and that there is no other solution to up to scalar multiples. So, one just needs to construct a sequence of invertible linear transformations on , with each having an eigenvector of eigenvalue one, that obeys the recursive condition (3'). But this can be done recursively. Choose to be invertible transformations with linearly independent eigenvectors of eigenvalue one. One can then select a vector independent of both and (which are themselves independent of each other) and it is not difficult to then locate an invertible linear transformation that maps to itself, maps to , and has no other solution to (3') other than scalar multiples. We keep iterating this procedure to construct . One may have some failure near the final step but that's OK since we are allowing things to break down of the time anyway.
Pace Nielsen (Dec 17 2024 at 04:04):
I had thought that a carrier group with exponent 2 was disallowed, but checking again I see that's only when we assume 513 in conjunction with 677.
Pace Nielsen (Dec 17 2024 at 04:43):
Actually, exponent 2 forces 255 when assuming 677 + injectivity of . I'm guessing that the issue is being shoved into into the failure set, somehow.
Terence Tao (Dec 17 2024 at 04:49):
Hmm, interesting. Are you able to extract a human readable proof of 255 in this case?
Pace Nielsen (Dec 17 2024 at 04:54):
I'll see what I can do. It doesn't look too bad.
Pace Nielsen (Dec 17 2024 at 05:56):
Throughout, assume translation-invariance in an exponent 2 group (which is thus commutative, so we write the operation additivitely). Also throughout, assume 677+injectivity of .
Write and . Equation 677 at yields
Next, equation 677 at yields
Since , using injectivity we get . Moving to the other side and using injectivity again, . In other words .
Next, equation 677 at yields
Recalling that and , then using injectivity of we have . Simplifying and using injectivity again, , or in other words .
We now have that takes . This means , and hence 255 holds.
Terence Tao (Dec 17 2024 at 06:35):
Thanks for this! I don't think the exponent 2 hypothesis is extremely essential to the sort of construction in my post to be possible, but it certainly makes things a little cleaner and simpler. But your argument shows that while it may end up leading to constructing a non-right-injective 677 finite magma (which I think we haven't yet been able to accomplish), it won't quite refute 677->255 on its own, unless we move away from exponent 2.
I might keep playing with the exponent 2 model a bit more as a toy problem. In particular if there is some way to take a model that solves 677 of the time and make some modification to it so that it now solves 677 say of the time then one could iterate all the way to an exact 677 model, which would give a new way of constructing these models that might hopefully adapt beyond the exponent 2 case and refute 677->255. Still more of a hope than a strategy, though.
Jose Brox (Dec 17 2024 at 08:45):
Amir Livne Bar-on ha dicho:
My run with f2=1 showed that it implies not only 255 but 2, i.e. no models (up to order 120, which Jose extended up to order 216)
The results are slightly different: @Bruno Le Floch only imposes and this implies equation 16, which together with 677 already implies 255. On the other hand, if we also impose for all , then we know that the axioms are inconsistent, i.e., even the trivial model is invalid.
Amir Livne Bar-on (Dec 17 2024 at 11:01):
The proof is rather simple too. It even suffices to have . If and , then we get from the functional equation and hence . Then by putting in the equation, we get .
Terence Tao (Dec 17 2024 at 16:12):
I'm beginning to understand now that the task of establishing 677 on of pairs (or of shifts , in the translation-invariant model) is rather different than that of establishing 677 everywhere. The problem with the latter is that it is exactly determined: equations on unknowns, or equations on unknowns in the translation-invariant case. But once one allows a failure rate, one now has an underdetermined problem, basically equations on unknowns in the translation-invariant case, so it is much easier to build examples. On the other hand, obstructions such as the exponent 2 construction only require a small number of equations and unknowns and so are invisible to the variant of the problem.
For three-variable equations such as the associative law, there can be ways to relate a specific operation on the multiplication table with quite "generic" entries of the multiplication table, with the upshot being that if such a table obeys the law 99% of the time then it is possible to modify it on a small number of entries to be obeyed 100% of the time. A classic example of this is the Blum-Luby-Rubinfeld linearity testing result: if a function obeys the linearity property 99% of the time, then one can modify a ilttle bit to be perfectly linear. The point, roughly speaking, is that one can work out what should be at by looking at for a "typical" and use this to perform "error correction". Here it is essential that the functional equation has at least two variables, in contrast to the one-variable situation we have with translation-invariant 677. This is also related to the fact that three-variable equational laws are highly overdetermined, in contrast to two-variable laws that are perfectly determined.
In the construction I gave with carrier , each of the vertical slices are self-contained submagmas which are completely arbitrary. It could be that an improved version of the construction leads to a method where one can place an arbitrary 677 structure on each such slice and then fill in the multiplication table for off-diagonal products with so that there is significant failure of right cancellativity "off the diagonal", but this wouldn't affect 255 which can be verified entirely within a single slice at a time. (This is related to the previous observation that we can assume without loss of generality that the magma is generated by a single element, so there is no point playing with models in which the magma splits into disjoint submagmas.)
Anyway, I think I'm already to abandon my tentative "99% construction" method here, as the hoped for "rigidity", "stability", or "error-correcting" phenomenon (in which a 99%-perfect 677 magma could be corrected into a 100%-perfect 677 magma) looks unlikely to be the case. (A model situation is when 677 fails for a single pair . As far as I know we have no way of ruling out this scenario, but also there is no obvious way to "repair" such a near-miss magma to obey 677 without exception.)
Zoltan A. Kocsis (Z.A.K.) (Dec 17 2024 at 16:51):
Terence Tao said:
Anyway, I think I'm already to abandon my tentative "99% construction" method here, as the hoped for "rigidity", "stability", or "error-correcting" phenomenon (in which a 99%-perfect 677 magma could be corrected into a 100%-perfect 677 magma) looks unlikely to be the case.
In my experience, similar "reconstruction" tends to be quite difficult in the absence of rigid structure. For example, if you start with the axioms x*x=0
, x*(y*z)=(x*y)*z
, x*0=0*x = x
, then you get only as your finite models.
But if you allow for these axioms to hold only up to epsilon, you immediately get many models where you have to change a fixed proportion of the operation table on before you get a group, much less . IIRC the operation given below, defined on a large , constitutes such an example:
0 * y = y
x * 0 = x
x * x = 0
x * y = min{x,y} if x,y both in {1..n} and x /= y
If you do have some rigid structure, e.g. cancellativity/injectivity, such examples do not arise (like in the theorem of Gowers and Long), but cancellativity/injectivity is precisely what we do not want in this case.
Here's a question: what if we could construct an operation table on which not just 677, but all algebraic consequences of 677 are also satisfied with high probability. Is the operation table epsilon-close to an actual model then? The analogous question for the consequences of the axioms above has a positive answer.
Jose Brox (Dec 17 2024 at 18:10):
Terence Tao ha dicho:
I'm beginning to understand now that the task of establishing 677 on 1−ε of pairs x,y (or 1−ε of shifts h, in the translation-invariant model) is rather different than that of establishing 677 everywhere.
Before abandoning this line of thought, let me comment that I've been trying to automatically find specific models where your conditions:
Terence Tao ha dicho:
- The expression f(x,y):=(y⋄x)⋄y "forgets" information about y, in the sense that at most 1% of pairs in M×M can be of the form (x,f(x,y)).
- The expression Ly−1x forgets the same information about y, that is to say for a given x,y,y′, one has f(x,y)=f(x,y′) if and only if Ly−1x=Ly′−1x.
are satisfied. The problem is that if we use first-order logic, imposing a condition like the 1% is tricky (we can do it if we impose a specific model size and throw in a bunch of variables, one for each element, etc.). So before resorting to higher-order logic I thought that perhaps I could compute all models satisfying condition 2 for many sizes, then choose the optimal models and try to approach condition 1 as the size grew, or else see if the limit was bounded from below for some reason. If things went well, one could perhaps study the optimal models and try to find some iterative construction. Hence I've used this Mace4 code:
x*y = x*z -> y=z.
all x all y exists z (x*z = y).
f(x,y) = (y*x)*y.
g(x,y) = z <-> y*z = x.
f(x,y) = f(x,z) <-> g(x,y) = g(x,z).
Up to size 6, things went well, I got a fast computation. But then Mace4 completely stalled at size 7: it has been there for more than 20h, finding only 306 models in the meantime.
Anyway, the smallest proportion of elements of the form (x,f(x,y)) (i.e., the sum of the cardinals of the sets given by the rows of the table of f(x,y) if I understood correctly) to the size of the model is 100% for size 3, 81.2% for size 4, 60% for size 5, and 58.3% for size 6. Since the naive lower bound for this proportion is 1/size, this results struck me as perhaps too high, and I thought that maybe there were some combinatorial reason (related to injectivity etc.) for this, hence to get 1% by this method we might need a size quite higher than 100.
In case they may result interesting, the optimal models for each size in [3,6] have the following functions:
OPTIMAL MODELS
If someone thinks of some smart sentence to automatically approach condition 1 (maybe with higher-order logic), we could speed up the search significantly.
A simple thing I've tried (but with no expectations at all) is just try to get unless . The search is in size 76 after 35h, so not many hopes there.
Pace Nielsen (Dec 17 2024 at 19:57):
How hard would it be to find (or rule out) a translation-invariant model of 677on , where , but 255 fails? Is size 256 just too big to effectively look for examples, even if we have constrained things a lot by fixing the carrier group?
Jose Brox (Dec 18 2024 at 00:45):
Jose Brox ha dicho:
or else see if the limit was bounded from below for some reason
@Terence Tao It is late for me in the night, but I think here we have an sketch showing that we can't go below 50%:
Suppose for ; then . Therefore
, thus if then , a contradiction with the injectivity of . Hence for each pair such that
in the -th row, we get the same pair such that in the -th row for (this extends to an arbitrary finite number of elements), and since is injective, if give different rows having repeated element with some , then and produce different rows having different elements .
Based on the examples, I'd bet that in addition we cannot have more than repeated elements per row, where is the size of the model, but no time to think about that now.
Terence Tao (Dec 18 2024 at 01:01):
Hmm, I think this shows something like that the number of possible values of for a given has to be at least , rather than at least . (It's not quite this, but if takes values, then the proportion of times one expects to have should be heuristically , which is the quantity that I think you've shown cannot exceed 50%.)
Terence Tao (Dec 18 2024 at 01:15):
The following argument can show that at least one of the right multiplication operators must have a range of size at least : If all take on less than values, then for fixed there are less than values for ,and hence less than values for thanks to 677, but this contradicts left-invertibility.
Bruno Le Floch (Dec 18 2024 at 02:15):
Three disorganized thoughts, sorry.
- Earlier, @Terence Tao considered M₇×S with M₇ one of the two 7-element 677-magmas, took an operation , noted that decouples, and used a projective Ansatz to reduce from 48 operations to only 8. We could take small S in an ATP. EDIT: I've ruled out .
The equations, for reference.
-
We could combine magma extensions with twisting, so take a carrier with both and being 677-magmas (and typically being itself a power a 677-magma), and set where every and is a magma morphism of (with bijective to get left-cancellability). If we did not have dependence on x,y then we know there is no non-trivial twisting, but using the dependence could help make the relations more redundant, hence have a solution. EDIT: for the 8-operation projective model the twists are given by and all other are the identity; in particular so the model obeys 255. This may hint to a general immunity.
-
Maybe the following graph is an interesting bookkeeping device:
y→z
if and only if∃x,z = (y ◇ x) ◇ y
if and only if∃x,x = y ◇ (x ◇ z)
. The direct implicationz = (y ◇ x) ◇ y ⇒ x = y ◇ (x ◇ z)
is 677. The reversez = (y ◇ x) ◇ y ⇐ x = y ◇ (x ◇ z)
is 677 together with left-invertibility iny ◇ (x ◇ ((y ◇ x) ◇ y)) = x = y ◇ (x ◇ z)
.
Terence Tao (Dec 18 2024 at 03:52):
The twisting extension construction is interesting! (or ) will have to be nonlinear for it to have a chance at evading 255 since otherwise it will be a linear extension model which we already know 677->255 is immune to. That is slightly worrying because the twisting semi-group doesn't seem to be aware of whether the magma one is working with is linear or not, though perhaps the nonlinearity will become important when trying to refute 255 rather than when trying to establish 677.
Bruno Le Floch (Dec 18 2024 at 08:41):
Sadly, twisting-extension doesn't work for finite 677->255. Left-invertibility (in the finite setting) requires all to be invertible. One of the equation (which states that the first and last variables receive the same action of the morphisms) has the schematic form , so is invertible. This implies right-invertibility, which implies 255.
Bruno Le Floch (Dec 18 2024 at 08:56):
Ah, I was too quick. If M is not right-invertible to begin with (which we might achieve with other constructions?), then the result is not right-invertible. And maybe ∀x,∃y,yx=x
is not preserved by this construction: even invertible twists might "move" the failures of right-invertibility from some that contains to one that does not.
Jose Brox (Dec 18 2024 at 22:34):
Pace Nielsen ha dicho:
How hard would it be to find (or rule out) a translation-invariant model of 677on (Z/4Z)4, where f4=1, but 255 fails? Is size 256 just too big to effectively look for examples, even if we have constrained things a lot by fixing the carrier group?
I'm not sure, I don't have the experience to tell: on the one hand, size 256 is quite big (tends to really slow things down), but on the other the product and inverse functions are completely specified, and (with ) is quite specific, so some search parameters combination may make the "magic" as Amir put it the other day.
In any case, I have started the experiment with two different selection measures in parallel (here I cannot tune the search parameters looking at lower sizes as easily, I'd have to generate other problems with , etc. and time the experiments to decide) and Mace4 has been holding up for a while (for comparison I have run another experiment, same carrier but arbitrary , and it has exited saying "killed" in seconds).
Apart from the lines with the multiplication (addition) table and the inverse (opposite) map, the code for this is
MACE4 ASSUMPTIONS
all x x = f(x * f((inv(x) * f(x)) * f(inv(f(x))))).
all x x != f(x).
all x x = f(f(f(f(x)))).
all x all y x@y = x*f(inv(x)*y).
all x all y all z x@y = x@z -> y = z.
MACE4 GOAL
all x x = ((x @ x) @ x) @ x.
(Please, check that I got everything right!).
I attach the complete file (close to 1MB):
MACE4 677 anti 255 linear over product of 4 copies of Z4 f order 4 measure 4.in
The Sage code I've used to generate the multiplication and inverse maps is
rings=[Zmod(4) for i in range(4)]
R=cartesian_product(rings)
#Multiplication table of R, in Mace4 format with sum written as *
s=""
for i,x in enumerate(R):
for j,y in enumerate(R):
s=s+f"""{i}*{j}={R.list().index(x+y)}.
"""
print(s)
#Inverse function of R, in Mace4 format with inverse as inv(x)
ss=""
for i,x in enumerate(R):
ss=ss+f"""inv({i}) = {R.list().index(-x)}.
"""
print(ss)
I attach a Jupyter notebook with the maps already computed and printed out:
MAGMAS PROJECT - Cartesian product of Z4, translation to Mace4.ipynb
Jose Brox (Dec 18 2024 at 23:33):
A brief summary of the experiments I'm conducting right now with Mace4, the running sizes (no models for smaller sizes) and the time they have already spent in the current size:
- 677+513+3659 anti 255: In size 14 for 109.5h
- 677+4073 anti 255: In size 14 for 107.5h
- 677+4131 anti 255: In size 14 for 107.5h
- 677+4276 anti 255: In size 13 for 116h
- 677+4293 anti 255: In size 16 for 43h
- 677+4321 anti 255: In size 15 for 107.5h
- 677+4591 anti 255: In size 14 for 106.5h
- 677+4599 anti 255: In size 18 for 96h
- 677 with translation-invariant model over noncommutative ring, any f: In size 15 for a few hours
- 677 with linear product in semirring without annihilation nor distributivity anti 255: In size 10 for 105h
- 677 with linear product in semirring without distributivity anti 255: In size 19 for 93h
The rationale for the last two is the following: over noncommutative rings the linear models cannot work. But we can keep removing axioms from the base ring until perhaps the two varieties (for 677 and 255) start differing. Even if we don't ask for distributivity or opposite elements for addition, the mere presence of and produces the same sets of polynomials (when written as sums of monomials) as the ring case, but this doesn't necessarily mean that their solutions are still the same. I have checked with Vampire that if we ask for annihilation () and left distributivity, then (with 677 anti 255) there must be opposite elements even if there is no right distributivity; and Mace4 is interestingly faster without any distributivity law, so I'm conduncting two experiments: one with annihilation, one without, both without distributivity nor opposite elements.
Giovanni Paolini (Dec 19 2024 at 14:30):
Jose Brox said:
A brief summary of the experiments I'm conducting right now with Mace4, the running sizes (no models for smaller sizes) and the time they have already spent in the current size:
[...]
In the meantime, I've kept searching for 677 translation-invariant models over groups of order >17 where has no fixed points. No model was found of order 18 and 19. I am currently checking (Gurobi has been running for 27h, with no sign of being close to finish).
To answer @Pace Nielsen, I don't think my current approach with Gurobi has any hope to handle , even if we add and no fixed points.
Jose Brox (Dec 20 2024 at 00:50):
Terence Tao ha dicho:
Hmm, I think this shows something like that the number of possible values of f(x,y) for a given x has to be at least 2, rather than at least n/2.
Apologies for being stubbornly fixated with a problem that is probably unproductive for the project, but I'm captivated by its beauty :big_smile: My "toothbrushing" sketch proof wasn't directed to find the bound for each row of (fixed ), but for the sum of the rows (that I believe is what you were asking with your condition 1 upstream). The combinatorial problem would be as follows, denoting :
Let be two functions with bijective for all (fixed) and such that
1) iff .
2) implies .
For each , let denote the cardinal of the range of . Then
where is to be determined and sharp.
My idea wasn't having into account some kind of collisions, but there is some subtlety in the iterative process: Let denote the -th row of the table of , and write for the equivalence relation in given by iff . Let for be the equivalence classes of and be their respective cardinals. Then the partition structure of affects other rows, saying that if then the -th row has at least elements (partitions). In particular, if has exactly two elements, then it has with cardinals , and hence there are two other rows with at least and elements respectively (so having at least elements per row is not the end of the story when accounting for the sum).
Also of potential interest is that forces to have at least different elements in its range (which may be quite more than ).
At the moment I don't see how to integrate the global conditions arising from the partitions of all rows in order to find the minimal sum (because a "descendant" row can have its "parent" as "descendant"). Do you have any ideas? :star_struck:
But we can show that cannot be : the following optimal model for size shows .
MODEL
Nevertheless, this combinatorial problem doesn't fully capture all the restrictions of your original 677-inspired problem, for which I still believe may be bounded from below by , and for which a check of all isoclasses for sizes suggest more: that even for each fixed row, the cardinal of the range cannot be smaller than (may be a small-numbers mirage). Here the fact that are related through the product is relevant, and not fully captured by condition 2) in my problem above (e.g. we have ).
Ibrahim Tencer (Dec 20 2024 at 08:47):
Some assorted observations:
- Notice that the argument translated by @Terence Tao above shows that there is a unique such that fixes . In a linear model is invertible iff every fixes some , in which case there is a bijection between fixers and fixpoints. (Notice that in Type 1 models , so we know it's invertible. Not sure about Type 2 -- is always invertible if nonzero?) We might try to find a counterexample where all of the have no fixpoints, or show that it can't exist.
- In a linear model implies and that the characteristic is 7. And in fact these models all work.
- In all cyclic linear models other than the characteristic 7 ones above (and the order 9 and 16 models), all of the 's appear to be conjugate as permutations, and always have orbits of equal size other than the unique fixpoint - not sure why this is. But it is not true in the order 25 model, and this is also a model where some is neither the identity nor has <= 1 fixpoints: fixes through .
I also tried to manually prove that there is no model (or countermodel) of various orders in order to gain some insight, here are a couple small results:
- cannot have a 2-cycle containing .
- If and then , i.e. there are no mutual fixpoints.
It wasn't too hard to show that there's no model of order 2 or 3, but even at order 4 the cases start to become unmanageable, there seems to be no clear pattern. So then I wrote a finite model builder in Ruby specialized to finding a counterexample for 677 => 255, it's much slower than Vampire (got up to size 7 in runs, and non-exhaustively -- it assumes the model consists only of left powers of the counterexample) but also easier to change and can give intermediate output. Code is here along with some general code about linear models and 1518 and 677 in particular.
Note that all models found so far, including the extension models, are cancellative. If a magma is linear then
So if it's cancellative and finite, and must be invertible, and
so we can recover the addition operation via
So more generally, if a magma is cancellative and has an idempotent then this construction will work and give an auxiliary cancellative magma with the same carrier in which we have for some invertible functions that fix . Then is a 2-sided identity for , but need not be either associative or commutative, nor do and need to be homomorphisms (distributive). This is similar to the twisting construction.
I tested this on the extension models found by @Matthew Bolan here. All of them have idempotents (and sometimes every element is an idempotent). Some of them don't give a commutative auxiliary magma for any choice of idempotent, some give a commutative one for only a single choice of idempotent. But only three give an associative auxiliary magma: the first (index 0) magma (of order 25), and two magmas of order 121 (at indices 98 and 240). All three are idempotent, and any element works as the 0.
Note that a finite cancellative unital magma will have both left and right inverses because and are surjective. If the magma is commutative then they are equal by cancellativity, and if the magma is associative these inverses will be equal by the usual argument. So in fact all of the commutative auxiliary magmas have inverses including the three associative ones, so they are in fact abelian groups. And according to my calculations the functions are also homomorphisms, so these could be linear. I am not sure how to determine whether they admit a ring structure that makes the homomorphisms into left-multiplication operations.
All code is here, along with the three pseudolinear magmas and their associated abelian groups (in magma_tables.rb) for anyone who wants to see or check for themselves.
Bernhard Reinke (Dec 20 2024 at 14:35):
Here is a question that hopefully can give a new line of attack: Is there a finite group with subgroup , such that there is a word , such that for , so that defines a magma structure on H that satisfies 677 (but not 255)? I tried to do this with words of the form or . Note both words actually define something translation invariant. I can recover the "flexible" translation invariant affine model on . Unfortunately it seems that they always satisfy 255.
For left cancellation, I think it is a good idea if appears exactly once (as or ) in w. I think in order to avoid the issues of right cancellation as in here, we should consider words where x appears to the left and the right of y.
Bruno Le Floch (Dec 20 2024 at 16:47):
Nice, so it's a nonabelian generalization of linear models. If we only use a single then the expression can maybe be abstracted as . Given a group's multiplication table we could use ATPs to seek solutions f,g to the resulting equation
It looks complicated in general, so I considered the case , so that the equation is and thought about groups with an exponent (large enough, for now). Then multiplying the equation with on the left and right gives , which after swapping becomes . Applying the original equation to simplify the middle gives , which has a in the middle hence simplifies further to etc:
If then , and inserting this (twice) in the original equation gives for all so the magma has a single element. If then and the same happens. If then we directly get . If then , which inserted in the equation gives and we conclude as in the first case. On the other hand, if the exponent is a multiple of there is no inconsistency, the equation with eventually gives or gives back the original equation.
So I would say that working in a non-abelian group of exponent 5 is promising.
EDIT: I forgot that for a 255 counterexample we can restrict to a magma with a single generator. If the operation is then our magma will be a subset of , so it's equivalent to working in an abelian group, and hence with a linear model , which is why I got an exponent/period of . We really need the more complicated Ansatz of Bernhard.
Bruno Le Floch (Dec 20 2024 at 17:09):
@Ibrahim Tencer I think it is good to try to see if by any chance all of the linear and cohomological models share some properties that can be abstracted and perhaps proven for general models.
-
Terry's argument tells us that implies actually, so indeed we have uniqueness. It's interesting that the map from fixpoint to fixer is bijective in all linear models (except one). Is it also the case in cohomological extensions? The one exception that you mentioned is the unique characteristic model with (the constant terms is irrelevant so there is a unique such model up to isomorphism); otherwise is always invertible.
-
An explanation for why of linear models are conjugate by a bijection : we have , which can typically reach all , unless is non-invertible. I didn't track down why there are two other exceptions of order 9 and 16, it might be interesting. It's really interesting that the cohomological models are richer in this respect. It might be possible to get some intuition about the "flow of information" by looking at these models.
-
One thing to investigate by hand/script maybe would be whether we can make a model of size with some undetermined entries (that will be later set to values larger than ) that obeys the magma rule whenever all the relevant entries are determined, then slowly add more elements (increase ) as needed, and try to make multiplication tables that are as full as possible. One has to impose left-cancellability properly to avoid creating permanent obstructions that will never disappear as we increase .
[...] abelian groups. And according to my calculations the functions are also homomorphisms, so these could be linear. I am not sure how to determine whether they admit a ring structure that makes the homomorphisms into left-multiplication operations.
You don't need anything to get a ring: the homomorphisms of an abelian group are such a ring if I understand correctly.
Ibrahim Tencer (Dec 20 2024 at 22:34):
Bruno Le Floch said:
Ibrahim Tencer I think it is good to try to see if by any chance all of the linear and cohomological models share some properties that can be abstracted and perhaps proven for general models.
Yeah I had a similar thought. I ran a few of the auxiliary magmas through the Finite Model Explorer but the results aren't too promising. The (first) auxiliary magmas for #2, #3, #10 satisfy no nontrivial laws. #47 only satisfies commutativity and its implications.
So, not much of a pattern just looking at equational laws at least. I can try to run all of them through it with a script later (hopefully it won't hit the site too hard - is there a local version?). Looking at how the two functions act might give more of an explanation.
"Is it also the case in cohomological extensions?"
I checked the first few magmas in the file and no they didn't have that property. Probably just a cyclic linear phenomenon.
Bruno Le Floch said:
[...] abelian groups. And according to my calculations the functions are also homomorphisms, so these could be linear. I am not sure how to determine whether they admit a ring structure that makes the homomorphisms into left-multiplication operations.
You don't need anything to get a ring: the homomorphisms of an abelian group are such a ring if I understand correctly.
Can you spell that out more? The endomorphisms of an abelian group do form a ring but I don't think there's a natural way to embed the group inside the ring (which is how we've basically been thinking of linear models, as defined using only ring operations). Anyways it's probably not too important to know whether it's a "real" linear magma, it's more of a side question.
Vlad Tsyrklevich (Dec 20 2024 at 22:54):
Ibrahim Tencer said:
is there a local version?
scripts/explore_magma.py
Bruno Le Floch (Dec 20 2024 at 23:10):
Ibrahim Tencer said:
You don't need anything to get a ring: the homomorphisms of an abelian group are such a ring if I understand correctly.
Can you spell that out more? The endomorphisms of an abelian group do form a ring but I don't think there's a natural way to embed the group inside the ring (which is how we've basically been thinking of linear models, as defined using only ring operations). Anyways it's probably not too important to know whether it's a "real" linear magma, it's more of a side question.
The point is that we don't actually have to embed the group inside the ring to define a linear model: you only need the ring to act on the abelian group to define (with the dot denoting the action of ring elements on group elements ) and compute expressions such as with all the usual distributive rules because by definition of an action we have .
So if you have a magma on with an idempotent such that and are invertible, and if defines an abelian group structure on , and if and are homomorphisms of , then the magma is linear in the sense that with . It's a lot of conditions, and unfortunately they are not fulfilled as you found in your investigations of the auxiliary magma.
Zoltan A. Kocsis (Z.A.K.) (Dec 21 2024 at 00:25):
Interesting. I tried a group-words approach to refute 1112->8
with infinite groups back in October. Nothing came of it, but perhaps I should revisit the code I wrote back then to see if it contains anything that'd be useful for this question (though unlikely).
Zoltan A. Kocsis (Z.A.K.) (Dec 21 2024 at 00:49):
Ibrahim Tencer said:
(hopefully it won't hit the site too hard - is there a local version?)
The Finite Magma Explorer runs its magma computations locally on your computer. The only load it places on the server is serving up the website, but the website is hosted on Github, so it won't really matter. Having long ?magma=
query strings does place a bit of a unnecessary load on Microsoft's servers, but not anything they can't cope with.
If you have Elm, you can do everything locally by saving https://teorth.github.io/equational_theories/fme/unknowns.json
in equational_theories/tools/fme/dist/
, then running elm reactor
in equational_theories/tools/fme/
and calling http://localhost:8000/dist/index.html?magma=...
.
Zoltan A. Kocsis (Z.A.K.) (Dec 21 2024 at 04:22):
Okay, I repurposed some of the old Python and GAP code I had, and can now make the following partial observations:
There is no group G
of order less than 256 and word w(x,y)
of length less than 5 for which satisfies Equation677 but not Equation255.
I am now running a search for words w(x,y)
of length less than 7 with two parameters z,w
each occurring once from the group G
. So far up to order 18, no hits (needless to say, I won't run this up to 256 :smiley:, will probably stop once I hit a few nonabelian grouos of odd order).
Zoltan A. Kocsis (Z.A.K.) (Dec 21 2024 at 07:17):
Okay, using GAP I have managed to exhaustively check that:
- For all groups of order less than 256 and all words of length less than 7, the operation defined on all of is not a counterexample to
Equation667 => Equation255
. - For all groups of order less than 48, all elements and all words of length less than 8 in which the letters occur exactly once, the operation defined on is not a counterexample to
Equation677 => Equation255
.
(edit: rewritten using fewer double negatives)
Zoltan A. Kocsis (Z.A.K.) (Dec 21 2024 at 07:31):
The smallest word operation on a non-Abelian group that satisfies 677 at all seems to be
Group ID: [ 125, 3 ]
Structure: (C5 x C5) : C5
Word: xxY
You can present [125,3]
as follows:
polycyclic group with 3 pc-generators and relations:
g1^5 = id
g2^5 = id
g3^5 = id
g2^g1 = g2*g3
all other pairs of generators commute
Zoltan A. Kocsis (Z.A.K.) (Dec 21 2024 at 07:42):
The URL is too long for Zulip, but you can copy-paste the file below into FME to see the resulting 125-element magma.
Judging by the large number of equations it satisfies, I'd not be surprised if one could show it isomorphic to a linear model.
magma125.in
Ibrahim Tencer (Dec 21 2024 at 07:54):
Bruno Le Floch said:
It's interesting that the map from fixpoint to fixer is bijective in all linear models (except one). Is it also the case in cohomological extensions?
Wait a sec, I was answering a different question (about the cycle types being all the same). In the extensions L_x always has a unique fixpoint in 287 out of 346 cases. Here are the cases where it does or doesn't and their orders:
unique fixpoints?
Ibrahim Tencer (Dec 21 2024 at 08:09):
and 65 of those cases are idempotent (in which case L_x must have a unique fixpoint)
idempotent?
Zoltan A. Kocsis (Z.A.K.) (Dec 21 2024 at 15:37):
One more cheap exhaustive check, just to make sure we're not missing any low-hanging fruit. Call a magma operation boring if it has the form for some over a finite group . The only non-Abelian group of order < 256 which admits a boring operation satisfying 677 is [125,3]
given above.
Bruno Le Floch (Dec 21 2024 at 22:20):
Part of your search space @Zoltan A. Kocsis (Z.A.K.) is already ruled out by some immunities. Consider a finite counterexample of 677->255 that is a subset of some group (possibly infinite), equipped with with a word in the letters and some constants in .
-
cannot consist only of and ; otherwise the submagma of generated by a counterexample of 255 is simply contained in the subgroup which is abelian, so the magma is linear, but we already ruled out such counterexamples.
-
cannot take the form nor . First we show that is injective: if then then for any (irrelevant) we have , and the only difference between is the last , so left-cancellativity implies . Then injectivity of implies that the operation is right-cancellative and it cannot be a counterexample.
-
We need to be injective on from to . If we take (which I think you are doing) then the easiest way to satisfy that is to take with an integer coprime with (or equivalently with the group's exponent, or the order of every group element).
-
If and the word only involves a single constant (in addition to ) then the equation has to hold for and , so that the overall powers of in have to be the coefficients in a linear model on with the order of in . This restricts the words quite a lot, especially if we think the form should be . Then we could go through the low-order linear models, for instance the 5-element one with so for instance or with . The first example here is ruled out by noting that idempotent models are solutions of 255, but the second is not.
Zoltan A. Kocsis (Z.A.K.) (Dec 21 2024 at 22:47):
@Bruno Le Floch Thanks, a nice collection of observations. I was aware that this hits some known immunities, calling the models above boring was no accident. My goal with the search was not finding potential counterexamples, I just wanted to see whether it's cheap-and-cheerful to construct yet-unseen 677-models by considering words over small non-Abelian groups, and after trying some templates, I'm satisfied that it isn't.
Ibrahim Tencer (Dec 21 2024 at 23:59):
Here's something interesting. I noticed that there were never any distinct elements a, b in a finite 677 model such that for all x. And in fact there can't be: if there is, then and so then by canceling three times. But notice that all we need here is for and to agree on two points: and (or , or put another way ). So a finite 677 model is "almost" right-cancellative. If we could say that implies then it would show right cancellation because is a positive power of due to finiteness.
Bruno Le Floch (Dec 22 2024 at 00:45):
How far was an exhaustive search of 677->255 counterexamples pushed? With the following code I ruled out sizes up to 9 in ten seconds, but I killed the size 10 run after half an hour. Maybe @Jose Brox already pushed this farther (without assumptions beyond 677)?
mace4 code
Jose Brox (Dec 22 2024 at 01:26):
Bruno Le Floch ha dicho:
How far was an exhaustive search of 677->255 counterexamples pushed?
That's a good question that I posed to myself two days ago. I believe that I exhausted size 12, but couldn't find the proof for it (and I've lost some files due to a blackout), so I simply restarted the search again. Size 10 is ruled out, I have 11-13 in parallel now. With your script you have remembered me that the consequence of 677 in fact speeds up the search, so I have changed the script. Thanks!
Jose Brox (Dec 22 2024 at 01:40):
Ibrahim Tencer ha dicho:
Here's something interesting.
I think this is a particular case of my small exploration of @Terence Tao's two conditions idea: Since we have , and by left cancellation if and only if , i.e., iff in Tao's terminology. I showed that by injectivity of , if and then , what implies that . In other words, if (as would happen when in the finite case) then we must have .
Jose Brox (Dec 22 2024 at 02:09):
I'm leaving on vacation in a few hours! I will try to reappear around January 5th. Here I report about another idea I've worked with last week, I hope you can get some juice from it.
One clear problem we have is the rigidity of 677: it doesn't imply many other identities, so it is satisfied by fewer models, hence the finite search against 255 is costly. Given an equation , call a relaxation to any equation such that (call a constriction of ). Obvious facts: A relaxation of has more models than has, and is a necessary condition for a model to satisfy . If then necessarily . To show that , it may be easier to start with a model of and then modify such model to get the desired one.
Most relaxations may be trivial, at least to the human eye (i.e., substitutions), but perhaps we can find some interesting ones, or some easier for the ATPs to establish proofs with. With this in mind, I have tried to determine the relaxations of 677 up to 13*10^6. The (mostly raw) results follow:
IMPLIED BY 677
Of these, equivalent to 677 when left multiplication is bijective (some obviously so):
EQUIVALENT TO 677 WITH LEFT BIJECTIVITY
While not equivalent to 677 with left multiplication bijective are:
NOT EQUIVALENT TO 677 WITH LEFT BIJECTIVITY
Interestingly, of these some don't imply 255 even with left multiplication bijective, so are good candidates to try to find countermodels by modification:
DON'T IMPLY 255 WITH LEFT BIJECTIVITY
The most promising seem to be
1466035: x = y * (y * ((x * ((y * x) * y)) * (x * y))).
3919117: x = (y * y) * (x * (((y * y) * x) * (y * y))).
10383419: x * x = y * ((x * x) * ((y * (x * x)) * y)).
On the other hand, there are identities with inconclusive computation for being relaxations of 677 (some obviously so), when given 30s each in Prover9/Mace4:
INCONCLUSIVE RELAXATIONS
Of these, some are relaxations when bijectivity of left multiplication is added (the rest are all still inconclusive, with 130s for Prover9/Mace4):
INCONCLUSIVE WITH LEFT BIJECTIVITY
Interestingly, of the inconclusive ones there are some that imply 255 when left multiplication is bijective, so if we can show that 677 indeed implies any of these, then 677 implies 255 in the finite case:
INCONCLUSIVE IMPLYING 255
And that's all, folks! I also did some work with constrictions of 677, but I don't have the time to upload the results. See you soon, Merry Christmas, and have fun!
Ibrahim Tencer (Dec 22 2024 at 18:06):
FYI, only a few of the extension models have f or g as a homomorphism:
[0, 3, 98, 240, 281, 283, 284, 292, 294, 295]
The pseudolinear ones 0, 98, 240 have f and g as a homomorphism for any choice of idempotent.
For #3, only f is a homomorphism in one case (#3)
And for the rest, only g is a homomorphism and only in case 0.
Terence Tao (Dec 22 2024 at 19:17):
Recording a negative result that I found somewhat instructive. I considered the general extension method of trying to build a finite 677 magma on a carrier where already obeys 677. Ostensibly, this gives us equations on operations , namely
So one could naively hope to just randomly assign the , so that there are possibilities, and hope from random heuristics that each choice has a of working, so we might get a solution out of this.
Besides being computationally prohibitive, this approach ignores the fact that the have to be left-invertible for this method to have a chance of working. So one could try to modify the approach so that the arbitrary magma operations are replaced with left-cancellative ones, of which there are some number . But this cuts down the number of possibilities without a necessarily matching increase in the success probability. This can be seen by solving for in the above equation: setting , we can rearrange it using left-invertibility as
The right-hand side defines some magma operation , and so one can view this equation as definining in terms of , , . If was left-cancellative and was chosen randomly, this equation would then have a chance of being obeyed. But there is no obvious reason why should be left-cancellative, hence the probability that this equation is satisfied should be less than and now this probabilistic approach is unlikely to produce solutions.
One can hope to get around this by restricting to some subclass of operations in which the right-hand side of (1) stays in the same subclass. For instance, we have affine models which basically have this property (if is large then most models will be left-cancellative), and are a promising approach for building 677 solutions (but unfortunately not 255 counterexamples, due to affine extension immunity). Linear models and cohomological models are subclasses of the affine model that also enjoy basically this property (and cohomological models obey it completely, as left-cancellativity is enforced). Partially translation invariant models , with required to be injective, unfortunately do not: the right-hand side of (1) will still have the translation-invariant form, which is good, but has no reason to be injective.
So, the only extension approaches I know of that still have a good chance of randomly generating finite models are the affine ones, but we know that 677->255 is immune to all such approaches (the problem being that implies in all such models) . If we had a separate class of extensions that was basically "closed" under (1) and did not have this immunity, then we would be back in business...
Bruno Le Floch (Dec 22 2024 at 21:23):
Ibrahim Tencer said:
FYI, only a few of the extension models have f or g as a homomorphism:
Sorry, what are f and g here? I lost track.
Ibrahim Tencer (Dec 22 2024 at 21:59):
Bruno Le Floch said:
Ibrahim Tencer said:
FYI, only a few of the extension models have f or g as a homomorphism:
Sorry, what are f and g here? I lost track.
I mean when we define the 677 magma operation in the generalized-linear way as where is recovered using an idempotent.
Ibrahim Tencer (Dec 22 2024 at 22:02):
Jose Brox said:
Ibrahim Tencer ha dicho:
Here's something interesting.
I think this is a particular case of my small exploration of Terence Tao's two conditions idea: Since we have , and by left cancellation if and only if , i.e., iff in Tao's terminology. I showed that by injectivity of , if and then , what implies that . In other words, if (as would happen when in the finite case) then we must have .
ok I will have to think more about this. The reason it came up, by the way, is that I was trying to do the generalized linear construction on an existing 677 magma. But this can't work because f has to be non-injective, but then we will have such a pair of distinct x, x' such that for all y. So the construction will preserve right-cancellativity.
Terence Tao (Dec 23 2024 at 06:26):
Here is a way to construct some more finite 677 magmas, including theoretically some non-right-cancellative ones (but unfortunately doesn't get us closer to disproving 255). One can write this law as , which by left cancellativity is equivalent to . Now suppose we have a finite magma with a 677 operation , as well as a left-cancellative operation obeying the relaxed version
of this equation, for some permutation . Clearly this is a more general law (677 being the special case ) and so one should be able to find more operations obeying this relaxed law, in particular it should be possible to find here that are not right cancellative.
Since is a permutation, it must have some finite order, . Now, locate a finite field with divisible by , so that there is a fifth root of unity , with the property that the is a primitive element of . Such a field should exist by a version of Artin's primitive root conjecture, and should be locatable by brute force numerical search.
Now construct an operation on as follows: we have
and for any integer we have
We claim that this obeys 677 for any . For this follows from the first law. Now suppose that for some . From the second law, we write
for ; and observe that this is periodic in of period ; in particular, multiplying by any tenth root of unity will not affect this law. Equation 677 can then be written after some calculation as
which by the above invariances simplifies to
and by left-invertibility and writing this can rearrange to
which one can obtain from (1).
Unfortunately, this construction uses a Type I linear base model in which every element is idempotent, and so for the purpose of testing 255 we never get to use the second law for and only the first law. So this doesn't directly get us any closer to refuting 677=>255, but it may give some broader intuition as to what 677 finite magmas can look like.
Ibrahim Tencer (Dec 23 2024 at 11:29):
Consider generalized-linear models of the form , with being the source operation (what was called auxiliary above).
If is left-cancellative and is invertible then is also left-cancellative because implies , so by left-cancellativity of and then by injectivity of .
But also, if is left-cancellative, then is injective: if then for any arbitrary x so so .
And if and are surjective then being left-cancellative implies that is left-cancellative too: if , let , , and . Then i.e. , so by left-cancellativity of , so .
We showed above that f has to be a bijection in a finite generalized-linear 677 model, so must also be left-cancellative, and in a countermodel it can't be right-cancellative because is a bijection so then would be right-cancellative too. (This also implies that can't be commutative or have two-sided inverses, which immediately rules out anything like linear countermodels.)
So to summarize: in a generalized-linear countermodel and are both bijections and the source magma is left-cancellative but not right-cancellative (and therefore neither commutative nor having right inverses).
Terence Tao said:
Here is a way to construct some more finite 677 magmas, including theoretically some non-right-cancellative ones (but unfortunately doesn't get us closer to disproving 255).
This may help! Maybe I'm missing something but without right-cancellativity I don't see any reason why this won't work as a source magma for a generalized-linear countermodel (even if which as I understand it does in this construction). We know 255 is equivalent to every x having some with , so can't be the identity, but it may still be possible in general.
Matthew Bolan (Dec 23 2024 at 17:06):
I'm having trouble finding any solutions to which are not right cancellative. Currently searching order 9.
I am on vacation and so have not been following so closely lately, however I am intrigued by Zoltan's order 125 example. It is not linear as , so it might be something new.
Bruno Le Floch (Dec 23 2024 at 18:29):
I had missed Zoltan's example. Is it in a group of exponent 5? Could it simply be a cohomological extension of the 5-element 677-magma? If so, it should partition into submagmas of order 25.
Pace Nielsen (Dec 23 2024 at 18:47):
The following re-expresses some obvious consequences of finiteness, which might have some potential. Given any finite set and any self-map , there must exist some nonnegative integer and positive integers such that . In particular, we could take taking to be a finite magma satisfying 677, and take to be left multiplication by some . Since is invertible, we may as well take , and so is just (a multiple of) the order of the left multiplication by map. We can make independent of , by replacing it with the lcm of all such 's (as varies). Thus, we should expect an equation like 513 [which corresponds to taking ] to hold in such a magma.
We can repeat this argument, but now with taken to be right multiplication by . Here, we don't want , on pain of getting 255. Taking , then Vampire tells us that small values of are not allowed. I wonder if this might help search for examples. For example, we could assume 677+513+(n=5 and k=1 for right mult.), and look for examples in size 20. Or instead take n=6, and look for examples in size 24. Or perhaps modify 513 a bit to allow other possibilities.
Another thought I had was to consider taking above to be , and doing a similar analysis.
Bruno Le Floch (Dec 23 2024 at 23:23):
Throughout this discussion, we've had quite a few constructions, and ruled them out in different senses: some of them preserve right-cancellativity, some of them preserve ∀x∃y,y*x=x
, and some preserve idempotence or some other properties when restricted to the submagma generated by any given element. I don't have time now but we should be very careful about which construction preserves what: maybe we can put together several constructions that would successively break right-cancellativity and then ∀x∃y,y*x=x
(or vice-versa).
Bruno Le Floch (Dec 23 2024 at 23:31):
Just like twisting can be done with two different automorphisms, I suspect Terry's last construction could involve a pair of permutations instead of powers of a single one.
Terry's last construction is a magma extension of a type 1 linear model , with a useful Ansatz for the operations that expresses all of them in terms of a single one (actually special-casing to all be equal to another operation) in such a consistent way that the equations reduce to a single equation. Maybe the general Ansatz could be
where f_{x,y},g_{x,y},h_{x,y}
are chosen such that the resulting equations on coincide.
I suspect the order-31 model that is in some sense the only one of type 1 and 2 could serve as a useful basis for a similar construction, but one has to find a variant of the idea of keeping all the same, and treating the other separately.
Zoltan A. Kocsis (Z.A.K.) (Dec 24 2024 at 10:06):
Matthew Bolan said:
I am on vacation and so have not been following so closely lately, however I am intrigued by Zoltan's order 125 example. It is not linear as L0L1−1L0L2−1(0)=L0L2−1L0L1−1(0), so it might be something new.
Thanks for checking this! Alas, I think @Bruno Le Floch 's suspicion about it being cryptomorphic to a cohomological construction is probably correct; indeed, one can partition the magma into disjoint submagmas of order 25 as follows:
Part 1: [1, 2, 6, 8, 15, 18, 29, 33, 48, 52, 53, 56, 60, 73, 77, 81, 92, 96, 99, 107, 110, 112, 117, 119, 120]
Part 2: [4, 5, 7, 12, 14, 17, 25, 28, 32, 43, 47, 51, 64, 68, 71, 72, 76, 91, 95, 106, 109, 116, 118, 122, 123]
Part 3: [10, 11, 13, 16, 22, 24, 27, 31, 39, 42, 46, 50, 59, 63, 67, 70, 80, 84, 87, 89, 90, 105, 115, 121, 124]
Part 4: [20, 21, 23, 26, 30, 36, 38, 41, 45, 49, 55, 58, 62, 66, 69, 75, 79, 83, 86, 88, 94, 98, 101, 103, 104]
Part 5: [0, 3, 9, 19, 34, 35, 37, 40, 44, 54, 57, 61, 65, 74, 78, 82, 85, 93, 97, 100, 102, 108, 111, 113, 114]
In the meantime, I checked that similar examples can be obtained in orders 7^3=343
and 5^4=625
; but we don't have them in orders 3^3 = 27
, 4^4=64
, 3^4=81
, and 6^3=216
. I think this leads further credence to the hypothesis that these non-Abelian group models arise from smaller linear models (Abelian group models) which exist in orders 5 and 7, but not 3,4,6. Of course, it still might be worth analyzing what actually happens in the other orders, but to me it didn't look that promising for constructing counterexamples.
Ibrahim Tencer (Dec 24 2024 at 15:39):
The order-125 model is idempotent, and oddly enough for any choice of idempotent produces an associative source model (for the generalized-linear construction) which is however not commutative. This is the only example of that we have so far, all the other extensions have sources that are both associative and commutative, only commutative, or neither.
But, none of the f's and g's used in the generalized-linear construction are homomorphisms, and associativity (with its consequences) is the only equation it satisfies up to order 4.
Ibrahim Tencer (Dec 24 2024 at 15:47):
I guess that is not so odd given how it was constructed :) but at least it is unique compared to the other models known.
Terence Tao (Dec 25 2024 at 11:51):
I managed to construct a translation-invariant finite 677 model which is not right-cancellative, though unfortunately it still obeys 255. The carrier is , where is a finite field that supports both a cube root of unity and a fifth root of unity . To solve 677 with a translation-invariant model , has to be invertible and one has to solve the equation
We use the ansatz for various functions , and now we need to solve the system
for all . To handle the case we set , and one can verify the equation here (this is just the standard linear Type I solution on ). For the non-zero , we use the ansatz when is a quadratic residue and otherwise. Since is a quadratic residue mod , but and are not, we have the system
and
Pen and paper revealed that the choice , solves this system. The function is not injective because of the choice of , so we get a loss of right cancellativity. On the other hand we have idempotence , so 255 holds.
In less translation-invariant terms, if one defines the operations and on , one can compute that
and hence one has the 677-pair
and
The above constructions are basically a way to convert such a 677-pair to an actual 677 magma.
Matthew Bolan (Dec 25 2024 at 17:29):
677_non_right_cancellative.txt
Here is an order example of Terry's construction. Right cancellativity fails quite often, for example
Matthew Bolan (Dec 25 2024 at 17:35):
The argument for immunity to cohomological constructions used that such constructions preserved right cancelativity - perhaps extensions of this have a shot? Unfortunately the relevant linear algebra will be in dimensions, but at least it's pretty sparse...
Bruno Le Floch (Dec 25 2024 at 20:34):
Cohomological extensions are a special case ( and constant) of piecewise affine extensions . The implication 677->255 is immune to those in the sense that if the base magma obeys 677 and 255 and the resulting magma obeys 677 then it obeys 255.
I proposed "twisting-extension" earlier, namely . If the base 677 magma is right-cancellative then the resulting magma is right-cancellative, but there was no direct immunity to 677->255, so there is still a bit of hope there.
Terence Tao (Dec 25 2024 at 21:23):
Unfortunately my model is idempotent and so useless as a base (for the purpose of testing 255 one can restrict attention to magmas generated by a single element, hence we can restrict to base magmas that are generated by a single element. But in the idempotent case that only leaves the trivial magma). In the notation of my construction, all the 255 action is taking place in the portion of the construction, while the right-cancellativity is living in the portion.
Another way of thinking about it is as follows. We know that in order for an extension model on to obey 677, the base model must already obey 677, and we also need the system of equations
Suppose we have some collection of left-cancellative magma operations on , and call a four-tuple of such operations "compatible" if one has the identity
Solving (1) then amounts to coloring the table by elements of such that, for any , the colors of , , , are compatible. We now know that can admit some non-right-cancellative operations, though they are not in the right "places" to contradict 255 unfortunately.
In my construction, I have three colors , , on , with , , . There are three compatible tuples: , , . So I can get a valid coloring by selecting as a base with and coloring by if , if is a non-zero quadratic residue, and if is a non-zero quadratic non-residue. Because is not right-cancellative and this color is used at least once, the entire magma is not right-cancellative.
On the other hand, if the base obeys 255, then for any we can solve , and then must be a colored by a compatible tuple. So the compatible tuples we care about the most are the ones in which the first and third colors are the same, and these cases we unfortunately know that linear (or affine) operations will necessarily be right-cancellative. So the tuples , I used are not directly useful for attacking 255. However, the broader strategy of locating pairs (or maybe larger numbers) of magma operations that generate several compatible tuples, combined with a suitable coloring of a base magma, may be potentially promising. Unfortunately, even if such magma operations can be located, the coloring problem could be difficult: for the Type I models with a fifth root of unity, there is an affine structure to the tuples , , , that makes them relatively easy to color, but these models are idempotent and so not useful. For the other models I know of, the tuples are much more "mixing" or "expanding" and thus unlikely to be colored with a small number of colors and compatible tuples (except with the degenerate case of constant colorings).
Terence Tao (Dec 28 2024 at 21:51):
Reporting a negative attempt. I was playing around with the extension model, where the task is to solve the system of equations
In order to break 255, i.e., to not be able to solve for all we need to be non-right-cancellative for at least one with . With my previous construction, we have non-right-cancellative behavior for some , but unfortunately not with . And we know that in order to break non-right-cancellativity in this case, we need to use a nonlinear operation; linear or affine operations will allow one to solve .
I was trying a mostly linear model, where is linear if and non-linear if , with the hope of simplifying the large system (1) to a much more manageable system involving only one nonlinear operation. When we have in (1), then things look reasonably good for (1), as we will have two nonlinear operations while the other two operations can be checked to be linear (unless we are in the idempotent case , which we want to avoid). However, problems arise because , could also be non-linear. If only one of them is non-linear then it is very unlikely that (1) is solvable (for instance, as observed earlier, one can solve for in terms of the other three operations, so if the latter three are linear, this one is linear too). So what one would like is that these operations are nonlinear at the same time, i.e., if and only if . But if both equations are true then (hence , while from 677 . Hence , and so we are back in the idempotent case which is no good for extensions.
In general, any attempt to use an extension involving a mixture of linear and nonlinear operations, with non-linear for at least one with , seems to either lead to (a) a single nonlinear operation obeying 677 (which brings us back to the original problem), (b) at least one equation involving three linear and one nonlinear operation, or (c) at least one equation involving multiple nonlinear operations (so no essential simplification to the system (1)).
Terence Tao (Jan 02 2025 at 08:46):
This is perhaps my last-ditch attempt to resolve this implication before throwing in the towel. Here are two conjectures which, if both true, would refute 677 -> 255 for finite magmas:
Conjecture 1. There exists a finite set with two operations obeying the three 677-like laws
for all , and such that the equation is not solvable for at least one choice of .
Note: if 677->255 is false for a finite magma , then Conjecture 1 is true, since we can set in this case. So this is a weaker conjecture than the original problem, and thus hopefully easier to establish. The point here is that only two of the four magma operations need to come from the non-right-cancellative operation , the others can come from the "base" operation , which can be a standard choice such as a Type 1 or Type 2 operation.
Conjecture 2: There exists a finite 677 magma and a set of pairs in obeying the following axioms:
- contains at least one pair with .
- For any , we have iff .
- For any , we have iff .
- For any we do not have and both in .
If we join two pairs in by a blue edge if they arise in axiom 2 or axiom 3, and a red edge if they arise in axiom 4, Conjecture 2 asserts that one of the components of the blue graph has no red edges, and also contains a vertex with (or equivalently ). So basically it's a hope that Axioms 2 and 3 do not propagate to cover so much of the pairs in that they start violating Axiom 4.
If Conjecture 1 and Conjecture 2 are both true, we can build a 677 magma on by declaring to equal if and otherwise. The various conclusions of the two conjectures imply that this is indeed a 677 magma, and that the equation is not solvable for at least one choice of , giving the desired refutation. So this factors the original problem into two independent sub-problems that are hopefully simpler to establish.
I have some hope that we can resolve Conjecture 2 with one of our existing magmas that is not completely idempotent, e.g., the Type 2 linear magmas, or the special translation-invariant magma on (or maybe ). For Conjecture 1, my plan was to take to be a translation-invariant linear magma with a finite field and a primitive fifth root of unity, and to be a non-linear translation-invariant operation . Then (1) is obeyed, and axioms (2) and (3) become
and
if I computed correctly. This can be written as
and
(I think). There is already a standard solution to this system (arising from setting ), and I am hoping that for some choices of field there is a non-standard solution for which has no fixed points (so basically one should modify the standard solution at and at some other points); this amounts to understanding the group generated by the linear transformations and , and hoping that this group is relatively small for at least some choices of field. It seems vaguely advantageous to work in a field that is large enough that it is not completely generated by , so that one can set to equal something that is independent of , e.g., may be the first place to look.
It's sort of a long shot at present, but if we somehow manage to verify one of the two conjectures, then I think we have a viable strategy.
Terence Tao (Jan 02 2025 at 09:52):
Grr, Conjecture 1 is immune to idempotent , which rules out my proposal to resolve it using the Type 1 linear models for . Indeed, suppose that , then by (3) , hence by left-cancellativity of where . Now from (2) we have , hence by left-cancellativity , hence by the 677 nature of , , so is idempotent whenever is. In particular the equation will be solvable for all if is idempotent.
There is still a chance that one can attack Conjecture 1 using the Type 2 models for , butincluding the special models in characteristic 31, but this is beyond the abilities of my pen-and-paper calculations, and would likely require some computer search.
Jihoon Hyun (Jan 05 2025 at 17:13):
I made a c++ program which outputs a DIMACS CNF format with variables and clauses. This CNF will be satisfied if there is a magma which satisfies 677 but not 255 (If I haven't messed up).
#include <iostream>
#include <vector>
int main(int argc, char *argv[]) {
using ssize_t = long long;
if(argc != 2) {
std::cerr << "Usage: " << argv[0] << " [Number of elements]" << std::endl;
return 1;
}
ssize_t n;
try {
n = std::stoll(argv[1]);
if(n < 0) { throw std::invalid_argument("Number of elements must be non-negative."); }
if(n > 1'000'000) { throw std::invalid_argument("Number of elements is too large."); }
} catch(std::exception const &e) {
std::cerr << e.what() << std::endl;
return 1;
}
std::vector<std::vector<ssize_t>> clauses;
/** `var1(x, y, i)` is $X_{yx, i}$. */
auto const var1 = [n](ssize_t const x, ssize_t const y, ssize_t const i) noexcept {
return 1 + (x * n + y) * n + i;
};
/** `var2(x, y, i)` is $X_{(yx)y, i}$. */
auto const var2 = [n](ssize_t const x, ssize_t const y, ssize_t const i) noexcept {
return 1 + n * n * n + (x * n + y) * n + i;
};
/** `var3(x, y, i)` is $X_{x((yx)y), i}$. */
auto const var3 = [n](ssize_t const x, ssize_t const y, ssize_t const i) noexcept {
return 1 + 2 * n * n * n + (x * n + y) * n + i;
};
/** `var4(x, i)` is $X_{((xx)x)x, i}$. */
auto const var4 = [n](ssize_t const x, ssize_t const i) noexcept {
return 1 + 3 * n * n * n + x * n + i;
};
/** For every $x$ and $y$, exactly one of $X_{yx, i}$ for $0 \leq i < N$ is true. */
for(ssize_t x = 0; x < n; x++) {
for(ssize_t y = 0; y < n; y++) {
/**
* For each distinct pair $X_{yx, i}$ and $X_{yx, j}$ of variables,
* there is at least one false variable. */
for(ssize_t i = 0; i < n; i++) {
for(ssize_t j = i + 1; j < n; j++) {
clauses.push_back({-var1(x, y, i), -var1(x, y, j)});
}
}
/** There is at least one true $X_{yx, i}$. */
std::vector<ssize_t> clause;
clause.reserve(n);
for(ssize_t i = 0; i < n; i++) { clause.push_back(var1(x, y, i)); }
clauses.push_back(std::move(clause));
}
}
/** For every $x$ and $y$, exactly one of $X_{(yx)y, i}$ for $0 \leq i < n$ is true. */
for(ssize_t x = 0; x < n; x++) {
for(ssize_t y = 0; y < n; y++) {
/**
* For each distinct pair $X_{(yx)y, i}$ and $X_{(yx)y, j}$ of variables,
* there is at least one false variable. */
for(ssize_t i = 0; i < n; i++) {
for(ssize_t j = i + 1; j < n; j++) {
clauses.push_back({-var2(x, y, i), -var2(x, y, j)});
}
}
/** There is at least one true $X_{(yx)y, i}$. */
std::vector<ssize_t> clause;
clause.reserve(n);
for(ssize_t i = 0; i < n; i++) { clause.push_back(var2(x, y, i)); }
clauses.push_back(std::move(clause));
}
}
/**
* For every $x$, $y$, and $i$, $X_{(yx)y, i}$ is true if and only if there is some $j$ which
* $X_{yx, j}$ and $X_{jy, i}$ are true.
*
* As we assumed there exists a unique $i$ which makes $X_{yx, j}$ true, we may simplify the
* proposition as follows.
*
* For every $x$, $y$, and $i$, $X_{(yx)y, i}$ is true if and only if for every $j$ which
* $X_{yx, j}$ is true, $X_{jy, i}$ is also true. */
for(ssize_t x = 0; x < n; x++) {
for(ssize_t y = 0; y < n; y++) {
for(ssize_t i = 0; i < n; i++) {
for(ssize_t j = 0; j < n; j++) {
clauses.push_back({var1(y, j, i), -var1(x, y, j), -var2(x, y, i)});
clauses.push_back({var2(x, y, i), -var1(x, y, j), -var1(y, j, i)});
}
}
}
}
/** For every $x$ and $y$, exactly one of $X_{x((yx)y), i}$ for $0 \leq i < n$ is true. */
for(ssize_t x = 0; x < n; x++) {
for(ssize_t y = 0; y < n; y++) {
/**
* For each distinct pair $X_{x((yx)y), i}$ and $X_{x((yx)y), j}$ of variables,
* there is at least one false variable. */
for(ssize_t i = 0; i < n; i++) {
for(ssize_t j = i + 1; j < n; j++) {
clauses.push_back({-var3(x, y, i), -var3(x, y, j)});
}
}
/** There is at least one true $X_{x((yx)y), i}$. */
std::vector<ssize_t> clause;
clause.reserve(n);
for(ssize_t i = 0; i < n; i++) { clause.push_back(var3(x, y, i)); }
clauses.push_back(std::move(clause));
}
}
/**
* For every $x$, $y$, and $i$, $X_{x((yx)y), i}$ is true if and only if there is some $j$ which
* $X_{(yx)y, j}$ and $X_{xj, i}$ are true.
*
* As we assumed there exists a unique $i$ which makes $X_{(yx)y, i}$ true, we may simplify the
* proposition as follows.
*
* For every $x$, $y$, and $i$, $X_{x((yx)y), i}$ is true if and only if for every $j$ which
* $X_{(yx)y, j}$ is true, $X_{xj, i}$ is also true. */
for(ssize_t x = 0; x < n; x++) {
for(ssize_t y = 0; y < n; y++) {
for(ssize_t i = 0; i < n; i++) {
for(ssize_t j = 0; j < n; j++) {
clauses.push_back({var1(j, x, i), -var2(x, y, j), -var3(x, y, i)});
clauses.push_back({var3(x, y, i), -var2(x, y, j), -var1(j, x, i)});
}
}
}
}
/** For every $x$, $y$, and $i$, if $X_{x((yx)y), i}$ is true, then $X_{yi, x}$ is also true. */
for(ssize_t x = 0; x < n; x++) {
for(ssize_t y = 0; y < n; y++) {
for(ssize_t i = 0; i < n; i++) { clauses.push_back({var1(i, y, x), -var3(x, y, i)}); }
}
}
/** For every $x$, exactly one of $X_{((xx)x)x, i}$ for $0 \leq i < n$ is true. */
for(ssize_t x = 0; x < n; x++) {
/**
* For each distinct pair $X_{((xx)x)x, i}$ and $X_{((xx)x)x, j}$ of variables,
* there is at least one false variable. */
for(ssize_t i = 0; i < n; i++) {
for(ssize_t j = i + 1; j < n; j++) { clauses.push_back({-var4(x, i), -var4(x, j)}); }
}
/** There is at least one true $X_{((xx)x)x, i}$. */
std::vector<ssize_t> clause;
clause.reserve(n);
for(ssize_t i = 0; i < n; i++) { clause.push_back(var4(x, i)); }
clauses.push_back(std::move(clause));
}
/**
* For every $x$ and $i$, $X_{((xx)x)x, i}$ is true if and only if there is some $j$ which
* $X_{(xx)x, j}$ and $X_{jx, i}$ are true.
*
* As we assumed there exists a unique $i$ which makes $X_{(xx)x, i}$ true, we may simplify the
* proposition as follows.
*
* For every $x$ and $i$, $X_{((xx)x)x, i}$ is true if and only if for every $j$ which
* $X_{(xx)x, j}$ is true, $X_{jx, i}$ is also true. */
for(ssize_t x = 0; x < n; x++) {
for(ssize_t i = 0; i < n; i++) {
for(ssize_t j = 0; j < n; j++) {
clauses.push_back({var1(x, j, i), -var2(x, x, j), -var4(x, i)});
clauses.push_back({var4(x, i), -var2(x, x, j), -var1(x, j, i)});
}
}
}
/**
* We want to find a case when the equation 677 (x = y(x((yx)y))) is satisfied but the equation
* 255 (x = ((xx)x)x) is not.
*
* If there is some $x$ which $X_{((xx)x)x, x}$ is false, then we are done. */
{
std::vector<ssize_t> clause;
clause.reserve(n);
for(ssize_t x = 0; x < n; x++) { clause.push_back(-var4(x, x)); }
clauses.push_back(std::move(clause));
}
// DIMACS CNF Generation start
std::cout << "p cnf " << 3 * n * n * n + n * n << ' ' << clauses.size() << '\n';
for(auto const &clause: clauses) {
for(auto const lit: clause) { std::cout << lit << ' '; }
std::cout << "0\n";
}
}
You can get an executable with g++ code.cpp -o generator
on any reasonable linux machine supporting c++11.
I'm not sure if this will help as there are more applicable tools in use already. However the sat attack for this problem was stuck in my head for quite a long time, and I couldn't help writing the generator.
Pace Nielsen (Jan 08 2025 at 19:32):
@Jihoon Hyun Can you give a low-level explanation of how you translated this question into an SAT problem? (And any report on runs with small values of n?)
Jihoon Hyun (Jan 09 2025 at 02:04):
Pace Nielsen 말함:
Jihoon Hyun Can you give a low-level explanation of how you translated this question into an SAT problem? (And any report on runs with small values of n?)
Let be the number of elements of the magma.
I declared four types of variables: , , , and . Each variables are true if and only if for given and , the expression results in . They are named as var1
to var4
in the program.
For each type of variables, the first thing to note is that given and , there exists a unique which makes true. This condition can be expressed by first denoting that no two distinct pair of variables are both true, and there is at least one variable which is true.
The second type of restriction comes from the expression. For example, is true if and only if there is some which and are both true. We can tweak the existing condition by using the uniqueness condition above. Also, by replacing with another value like , we can restrict the CNF to satisfy the equation 677.
The last restriction lets us find the magma which satisfies the equation 677 but not 255. For this we simply check the clause of all , to see if there is any false variable.
With CaDiCaL, the cases when turned out to be unsatisfiable after a few seconds, meaning that there is no magma with 5, 6, or 7 elements which satisfies eqn 677 but not 255.
- 10.1k seconds of CaDiCaL with showed that there is no magma satisfying 677 but not 255. However this was expected as there is no magma satisfying 677 with order 8.
Matthew Bolan (Jan 09 2025 at 06:23):
Terence Tao said:
Conjecture 2: There exists a finite 677 magma and a set of pairs in obeying the following axioms:
- contains at least one pair with .
- For any , we have iff .
- For any , we have iff .
- For any we do not have and both in .
I'm back from my holiday, so I decided to try tackling this conjecture. However, Prover9 suggests it is false, with input
Input
and this output
Output
The point seems to be that if , then by axiom 2, but this conflicts with axiom 4. Axioms 1 and 3 then provide such an pretty easily (this is in lines 16, 43, 51 of the Prover9 proof), namely , where and .
Terence Tao (Jan 09 2025 at 07:57):
Ah, good to know. (I had also tested quite a few linear magmas and showed they could not be used to verify conjecture 1, so i think I’m ready to abandon this attack strategy.)
Jose Brox (Jan 10 2025 at 13:18):
Hi again! Reporting on experiments and negative results after my holidays!
- 6 experiments have been running in some size for 25 days now (e.g. 677 with 4073 anti 255 in size 14); I now know how to make them faster, but I hesitate to kill them and start again with some unknown speed up factor, since some of the others have finished in the last few days... I will eventually do it though.
- 677 anti 255 is still in size 11 after 19 days, so there is no way I had exhausted up to size 12 before. We only know there are no models up to size 10 (included).
- There is only one model of 677 in size 9 (the linear one). With speed ups, this was found in 6min. I'm searching for all models of sizes 10,11 now (more than 1 day of computation already).
- There are no models of 677+513 in size 13, now looking in sizes 14-16. Size 13 needed 8h.
- There are no models of 677+4131 in size 14 (size 15 for 5 days already).
- There are no models of 677+4276 in size 12 (size 13 for 6 days already).
- There are no models of 677+4591 in size 14 (size 15 for 6 days already).
- There are no translation-invariant models (with any f) up to size 17 included (size 18 for 5 days already). Size 17 needed 25h.
- I have several other experiments with variations of linear products (without distributivity, identity, annihilation, with weaker axioms than associativity of the product...). For the moment being, no new models of 677 have been found, although I have found some weaker underlying products giving rise to the same magma product; e.g. in size 16 there are both a nonassociative flexible product, and a nonflexible product satisfying but not , that give rise to the unique linear model. Some of those I think we may theoretically show to give no new magma models through an endomorphism ring argument.
- The previous experiments show that size 16 may be qualitatively different, since there appear many more possibilities (for underlying products for example) and runs tend to take much more time in this size relatively speaking (also happens with other square numbers). Accordingly, I am also trying 677 anti 255 in size 16, just in case; apart from the Mace4 run, I also tried Vampire for 10h, without success; I will give it unlimited time next time.
Jose Brox (Jan 10 2025 at 15:17):
- Also, @Pace Nielsen's idea of trying a translation-invariant model of 677 anti 255 with over is still running after 23 days.
Daniel Weber (Jan 12 2025 at 07:39):
(deleted)
Daniel Weber (Jan 12 2025 at 08:06):
What techniques were attempted to resolve this positively? I mostly see discussion about constructing counterexamples
Zoltan A. Kocsis (Z.A.K.) (Jan 12 2025 at 15:57):
@Daniel Weber I don't know what others did, as we didn't discuss much, but I made attempts using both the usual injective/surjective arguments, and trying to use the fact that iterating a function on a finite set eventually repeats a value, using various term functions , both by hand and by ATP. Didn't get anything.
After @Terence Tao constructed his large non-right-cancellative model, I kinda gave up: it convinced me that one can probably build a large model where this implication fails too. But before I gave up, I was planning to try the following approaches:
- Look up proofs of the most impressive implications I know about finite structures (e.g. Artin-Zorn) to see if any general algebraic techniques used in them are missing from our ATP toolbox.
- Try to find a first-order property characterizing the directly irreducible models of 677, and see using ATP whether , along with the finiteness assumptions above, implies 255. If so, we're done, since every finite model is a product of directly irreducible finite models, and each product satisfies the equations that hold in all its factors.
Since I mostly converted to the "there is a counterexample" side, there is one more thing I would like to try in an attempt to construct one. Take the largest set of equations such that our ATPs fail to prove . Try to brute-force the free -algebra on one generator. If we get lucky (and our is big enough), this free algebra should be finite of manageable size, and thus a counterexample of the sort we're looking for.
Matthew Bolan (Jan 12 2025 at 16:02):
I think @Vlad Tsyrklevich also ran a number of such experiments.
Vlad Tsyrklevich (Jan 12 2025 at 18:22):
Mostly I just tested the injective<=>surjective hypotheses and coping the arguments of the eventually-periodic finite implications in as much as I was able to express them to the ATP--so nothing new.
Terence Tao (Jan 12 2025 at 20:00):
Zoltan A. Kocsis (Z.A.K.) said:
Since I mostly converted to the "there is a counterexample" side, there is one more thing I would like to try in an attempt to construct one. Take the largest set of equations such that our ATPs fail to prove . Try to brute-force the free -algebra on one generator. If we get lucky (and our is big enough), this free algebra should be finite of manageable size, and thus a counterexample of the sort we're looking for.
This may be our best remaining hope. One thought is to work both with the original operation and its reflection , so one has the relation . The reflected operation obeys a nice law . Perhaps if we use both and to fill out our additional system , we may be able to get enough equations to constrain the magma.
Jose Brox (Jan 12 2025 at 22:55):
More negative results in small sizes:
- There are no models whatsoever of 677 in size 10 (39h in Mace4).
- I have written a better Mace4 script for translation-invariant models of 677 anti 255. There are no such models with any up to size 19 included (73min for this last size), and no models with up to size 29 included (size 28 in 65min). I have also started a new @Pace Nielsen's size-256 experiment with a faster script.
Jose Brox (Jan 12 2025 at 23:01):
About using SAT solvers: Vampire already implements SAT solvers inside its finite model builder (it uses Minisat and Z3).
As a matter of fact, my Vampire search for a 677 anti 255 model in size 16 with unlimited time was killed after 15h because Minisat needed more than the 2GB of RAM I had allocated for it (it's running again with 10GB of RAM).
Henrik Böving (Jan 12 2025 at 23:10):
If you want to do some work with SAT solving and are concerned about speed I would still recommend giving more modern solvers like CaDiCal or Kissat a try though, I would expect both of them to always outperform minisat and Z3 when you just give them a query directly.
Daniel Weber (Jan 13 2025 at 03:42):
Is there an infinite counterexample where is bijective? Maybe we can try to construct such an example with the greedy method
Jose Brox (Jan 13 2025 at 08:00):
Yet more negative results:
- 677+4599 anti 255 has finally ended in size 18 after 26.5 days (without models). I can make the script faster, so I will try with 19+ (EDITED: with the new script, size 18 was completed in 25min :sweat_smile: ).
- No translation-invariant models with any in size 20 (4h).
- No translation-invariant models with in size 30 (28h). Given the progression of time with size in this case (24: 3min, 26: 9min, 28: 1h, 30: 28h) I don't expect to be able to exhaust size 32, but it still is worth a shot, since it is a power of 2 (like 16).
Bernhard Reinke (Jan 13 2025 at 14:55):
Has there already been a search for a 677 anti 255 model that is explicitly one-generated? If there is finite counterexample, then there must be a finite counterexample that is only generated by an element . For this counterexample there must be a constant n
such that every element of can be written via at most n
multiplications of .
If we are given such an n
, we could try to do the following: we consider , the Dyck words with at most n
pairs of brackets. We can search for a pair of an equivalence relation and such that
- R descends to a magma on satisfiying 677
- We have whenever
- 255 fails for x
I think up to n=4 we know it is not possible (as there are only 9 Dyck words with at most 4 pairs of brackets), n=5 might be feasible to check and is not yet covered by our computations.
Jose Brox (Jan 13 2025 at 17:34):
Bernhard Reinke ha dicho:
Has there already been a search for a 677 anti 255 model that is explicitly one-generated?
I have tried more or less what you suggest using Prover9, but the search (at least with my code) is slower than just checking 677 against 255. For example, for my code is:
PROVER9 ASSUMPTIONS
x = 0 | x = (0*0) | x = (0*(0*0)) | x = ((0*0)*0) |
x = (0*(0*(0*0))) | x = (0*((0*0)*0)) | x = ((0*0)*(0*0)) | x = ((0*(0*0))*0) | x = (((0*0)*0)*0).
x=y*(x*((y*x)*y)) #label(677).
x=(y*x)*((y*(y*x))*y) #label(consequence677).
x*y = x*z -> y = z.
exists x -(exists y (y*x = x)).
PROVER9 GOAL
x=((x*x)*x)*x #label(255).
With usual 677 anti 255, size 9 is exhausted in 12s (with selection_measure 1 and without the last clause included in the code above), while with the one-generator code, times are 36s, 42s, 65s for (with selection_measure 4 and skolems_last checked).
Terence Tao (Jan 13 2025 at 17:45):
Daniel Weber said:
Is there an infinite counterexample where is bijective? Maybe we can try to construct such an example with the greedy method
This is an interesting idea! I think abstractly one exists: one considers the theory with two operations , with obeying 677 and with the additional laws and , so that the left multiplication operators invert each other. I think the Type II linear models contain arbitrarily large submodels that are generated by a single generator, so the free magma for this theory from one generator is necessarily infinite.
With pen and paper it does not seem that the greedy algorithm converges for this system, but there were a lot of cases and I am not 100% sure about this.
Terence Tao (Jan 13 2025 at 20:28):
By the way, one simple infinite example with one generator: take a Type II linear model over the complex numbers and restrict to the submagma generated by, say, the complex number 1.
Jose Brox (Jan 13 2025 at 21:50):
No models of 677+4599 anti 255 in size 19 (7.5h).
No translation-invariant models with any in size 21 (10h).
Still some room to explore with these.
Jose Brox (Jan 13 2025 at 22:04):
Daniel Weber ha dicho:
What techniques were attempted to resolve this positively? I mostly see discussion about constructing counterexamples
Something I'm starting to explore is semantic guidance: when we have a theory T that does not imply a fact F, but T together with some extra hypothesis H does, then a model of T anti F can be used to speed up a proof of T+H -> F, by evaluating the candidate clauses in the model to see if they are false or not for it.
Semantic guidance is implemented in Prover9, we just need to find some model(s) of T+neg(F) with Mace4 and include them as guidance. What I'm doing is using, from my lists of relaxations, those equations that are implied by 677 but are not equivalent to it (even when left multiplication is bijective) and do not imply 255; I take such an equation T as a theory (weaker than H=677) and use its countermodels for F=255 as semantic guidance. For the moment I have only explored
1466035: x = y * (y * ((x * ((y * x) * y)) * (x * y)))
with Prover9 (different configurations with more or less max_weight and sos_limit, and more or less finiteness bijectivity conditions, for 10h each), without success.
Something I also tried was simply adding to the 677 anti 255 Prover9 search the (higher-order-logic) clause
all f ( (all x all y f(x) = f(y) -> x = y) <-> (all x exists y f(y) = x) )
but it didn't produce a proof.
Jose Brox (Jan 13 2025 at 22:09):
I also thought that using typed higher-order logic, a priori it should be possible to write a Vampire script in which the finiteness of the model is imposed, and not just some weaker consequences, but I haven't deepened into this. With Prover9 perhaps it could be done with an order relation and a successor function.
Jose Brox (Jan 13 2025 at 22:11):
Henrik Böving ha dicho:
If you want to do some work with SAT solving and are concerned about speed I would still recommend giving more modern solvers like CaDiCal or Kissat a try though
What speed up factor do you guess we may get? Would it be worth the effort?
Jose Brox (Jan 13 2025 at 22:14):
The dimacs format that @Jihoon Hyun's script gives as output is the standard one for CaDiCaL? (Btw, I checked that the program compiles and runs correctly giving some array of numbers).
Jihoon Hyun (Jan 13 2025 at 23:04):
Jose Brox said:
The dimacs format that Jihoon Hyun's script gives as output is the standard one for CaDiCaL? (Btw, I checked that the program compiles and runs correctly giving some array of numbers).
Yes, it is. The first line with p cnf
is the header with the number of variables and clauses. The rest are clauses, each ending with 0.
Douglas McNeil (Jan 13 2025 at 23:29):
I've done a fair bit of SAT work now, mostly using glucose which knocked off two implications early and after that kissat which helped springboard 854. I don't think there are a lot of performance gains lurking there left for us, TBH. mace4 and vampire in solver mode both seemed to work better for me at larger sizes.
Jihoon Hyun (Jan 13 2025 at 23:32):
If you're using my generator, there are many places for improvement. I'll share a repo for updates within a couple of hours.
Daniel Weber (Jan 14 2025 at 03:28):
@Jose Brox said:
Daniel Weber ha dicho:
What techniques were attempted to resolve this positively? I mostly see discussion about constructing counterexamples
Something I'm starting to explore is semantic guidance: when we have a theory T that does not imply a fact F, but T together with some extra hypothesis H does, then a model of T anti F can be used to speed up a proof of T+H -> F, by evaluating the candidate clauses in the model to see if they are false or not for it.
Semantic guidance is implemented in Prover9, we just need to find some model(s) of T+neg(F) with Mace4 and include them as guidance. What I'm doing is using, from my lists of relaxations, those equations that are implied by 677 but are not equivalent to it (even when left multiplication is bijective) and do not imply 255; I take such an equation T as a theory (weaker than H=677) and use its countermodels for F=255 as semantic guidance. For the moment I have only explored
1466035: x = y * (y * ((x * ((y * x) * y)) * (x * y)))
with Prover9 (different configurations with more or less max_weight and sos_limit, and more or less finiteness bijectivity conditions, for 10h each), without success.Something I also tried was simply adding to the 677 anti 255 Prover9 search the (higher-order-logic) clause
all f ( (all x all y f(x) = f(y) -> x = y) <-> (all x exists y f(y) = x) )
but it didn't produce a proof.
Could you take H = the magma is finite
here? The greedy ruleset lets us decide the free theory modulo 677 efficiently
Jihoon Hyun (Jan 14 2025 at 04:24):
I got a result that if, for given , there is some which , then such is unique and .
So proving the existence of such for all , especially for all , is equivalent to proving 255.
Is there any known result for this?
I know there is a non-right cancellative model, but that won't imply there is some which for every , holds.
Zoltan A. Kocsis (Z.A.K.) (Jan 14 2025 at 06:41):
Jihoon Hyun said:
I got a result that if, for given , there is some which , then such is unique and .
So proving the existence of such for all , especially for all , is equivalent to proving 255.
Is there any known result for this?
I know there is a non-right cancellative model, but that won't imply there is some which for every , holds.
Iirc it's been known that this condition is equivalent to 255 given 677, but the non-right-cancellative model is idempotent so not very useful for constructing 255-counterexamples.
Since many linear models were enumerated: On a related note, @Bruno Le Floch do you know if we have a nowhere-idempotent model with even cardinality?
Henrik Böving (Jan 14 2025 at 08:05):
Jose Brox said:
The dimacs format that Jihoon Hyun's script gives as output is the standard one for CaDiCaL? (Btw, I checked that the program compiles and runs correctly giving some array of numbers).
Dimacs is the standard for all serious SAT solvers basically since the dawn of time :tm:.
Jose Brox said:
Henrik Böving ha dicho:
If you want to do some work with SAT solving and are concerned about speed I would still recommend giving more modern solvers like CaDiCal or Kissat a try though
What speed up factor do you guess we may get? Would it be worth the effort?
Well what is the effort? You should just need to swap the binary that you run? Also note that you can gear the heuristics of some solvers to optimize looking for a certain outcome. E.g. cadical has a --unsat flag to make trying to find UNSAT instances faster etc.
Henrik Böving (Jan 14 2025 at 08:08):
And regarding the performance expectations, as j mentioned above I would expect them to be notably faster when you let e.g. minisat run straight at a problem, this is not to say that a tool like vampire that can do additional preprocessing etc isn't going to be faster vs a custom but not well optimized encoding
Bernhard Reinke (Jan 14 2025 at 09:39):
Jose Brox said:
I have tried more or less what you suggest using Prover9, but the search (at least with my code) is slower than just checking 677 against 255.
With usual 677 anti 255, size 9 is exhausted in 12s (with selection_measure 1 and without the last clause included in the code above), while with the one-generator code, times are 36s, 42s, 65s for (with selection_measure 4 and skolems_last checked).
Thanks for doing this! Just to make sure, for the list of times with the one-generator code, do you still impose the overall size bound of 9 or is it without any size bound?
Jihoon Hyun (Jan 14 2025 at 14:25):
Jihoon Hyun 말함:
If you're using my generator, there are many places for improvement. I'll share a repo for updates within a couple of hours.
I just made a repository to update the code. I believe there are still more places for improvements, and will update when found.
Also, if you have any experiments in mind, I might craft a generator for it.
Bruno Le Floch (Jan 14 2025 at 19:32):
Zoltan A. Kocsis (Z.A.K.) said:
On a related note, Bruno Le Floch do you know if we have a nowhere-idempotent model with even cardinality?
I didn't track all the models. I know of the order-31 linear model that is nowhere idempotent, and I think the type II linear model over with and is almost nowhere idempotent, with the exception of .
Operation table for the F16 model
same In the finite magma explorer.
It obeys 677, 255 of course and all are equal, and and and and are each symmetric in for some reason.
Matthew Bolan (Jan 14 2025 at 19:38):
The direct product of the order 31 nowhere independent model with a model of even order should work
Giovanni Paolini (Jan 14 2025 at 22:32):
Jose Brox said:
Yet more negative results:
- 677+4599 anti 255 has finally ended in size 18 after 26.5 days (without models). I can make the script faster, so I will try with 19+ (EDITED: with the new script, size 18 was completed in 25min :sweat_smile: ).
- No translation-invariant models with any in size 20 (4h).
- No translation-invariant models with in size 30 (28h). Given the progression of time with size in this case (24: 3min, 26: 9min, 28: 1h, 30: 28h) I don't expect to be able to exhaust size 32, but it still is worth a shot, since it is a power of 2 (like 16).
You are clearly faster than me at checking translation-invariant models! :smiley: I had size 20 running for several days and I have now stopped it. (My computer was longing for a restart, so this is for the best.)
Zoltan A. Kocsis (Z.A.K.) (Jan 15 2025 at 04:11):
Bruno Le Floch said:
I didn't track all the models.
Sorry, I assumed you had, based on how quickly you could answer my previous question! And this is not the first time this particular 16-element linear model almost-satisfies a query I have, so I've now saved it on my "things to try before asking a question" list :)
Jose Brox (Jan 15 2025 at 09:48):
Bernhard Reinke ha dicho:
Thanks for doing this! Just to make sure, for the list of times with the one-generator code, do you still impose the overall size bound of 9 or is it without any size bound?
These times are for size 9 only. I didn't compare times in size 10 because for usual 677 anti 255 it needs 1h, but now I've started size 10 with n=6, just in case [EDITED: killed after 1h without exhausting]. We should also try Vampire, could do things differently and be faster with one generator.
Jose Brox (Jan 15 2025 at 10:00):
Giovanni Paolini ha dicho:
You are clearly faster than me at checking translation-invariant models! :smiley: I had size 20 running for several days and I have now stopped it. (My computer was longing for a restart, so this is for the best.)
:big_smile: I recently changed the script to make it faster (you now, I didn't care that much about speed at first because I started running small experiments thinking we wouldn't explore many sizes and the problem would be solved sooner, etc.).
In fact now size 22 has also been exhausted (in 27h) and size 23 is running. The running time progression with size in this case is
17: 12min, 18: 44min, 19: 73min, 20: 234min, 21: 603min, 22: 1633min.
As you see, the time increases by a factor of around 3, so I expect to be able to exhaust size 23 in around 3 days, size 24 in around 9 days, and size 25 in around 1 month if things come to this. This is the horizon for this experiment (with Mace4).
In case you are interested, the Mace4 script for this is
%677 anti 255, translation-invariant product. Exists any f?
%with 2,3,no
%size 23
%size 14: 2,3,no: 44.7s; 2,3,yes: 45.2s; 2,4,no/yes: more than 120s; 2,1,no/yes: more than 45s. 0,3/,no,yes: more than 45s
if(Mace4). % Options for Mace4
assign(max_seconds, -1).
assign(max_megs, 2000).
assign(selection_measure, 3).
end_if.
formulas(assumptions).
all x all y all z (((x * y) * z) = (x * (y * z))).
all x (0 * x = x).
all x (x * 0 = x).
all x (x * inv(x) = 0).
all x (inv(x) * x = 0).
all x (x = f(x * f((inv(x) * f(x)) * f(inv(f(x)))))) #label(677).
all x (x = f(x)*f((inv(f(x))*f(f(x)))*f(inv(f(f(x)))))) #label(677consequence).
end_of_list.
formulas(goals).
0 = f(0)*(f(inv(f(0)))*f(inv(f(inv(f(0))))*inv(f(0)))) #label(255).
end_of_list.
Zoltan A. Kocsis (Z.A.K.) (Jan 15 2025 at 11:51):
@Jose Brox : There are as many groups of order 24 as there are groups between orders 18 and 23 altogether. I'm not sure how that will affect the computation time, but I wouldn't be surprised if it took longer than what one would expect by continuing the exponential.
Do you have data on the jump from order 15 to order 16? That's similar to the 23-24 jump: there's only one group of order 15, but 14 groups of order 16.
I tried what happens if I give a group operation table explicitly to Mace4, instead of constructing it. I.e. instead of having
all x all y all z (((x * y) * z) = (x * (y * z))).
all x (0 * x = x).
all x (x * 0 = x).
all x (x * inv(x) = 0).
all x (inv(x) * x = 0).
in your assumptions list, you explicitly supply
formulas(operations).
0 * 0 = 0.
0 * 1 = 1.
0 * 2 = 2.
% ...
inv(0) = 0.
inv(1) = 10.
inv(2) = 9.
end_of_list.
When I force Mace4 to construct the group of order 11 by itself using the assumptions,time mace4 -n 11 -f ...
gives the following:
real 0m3.677s
user 0m3.667s
sys 0m0.003s
However, when I supply the operation tables in advance explicitly and ask it only to produce a suitable f
, I get
real 0m0.287s
user 0m0.276s
sys 0m0.012s
This looks like a significant potential speedup to me.
Giovanni Paolini (Jan 15 2025 at 21:03):
I agree, fixing the group would probably make things faster! That's what I did in my script (https://github.com/giove91/equational/blob/main/translation_invariant.sage). I got each group's multiplication table from Gap's atlas of small groups (through Sage).
Jose Brox (Jan 16 2025 at 00:48):
Zoltan A. Kocsis (Z.A.K.) ha dicho:
Do you have data on the jump from order 15 to order 16?
Sure! Size 14 in 45s, size 15 in 103s, size 16 in 324s, size 17 in 12min.
My code didn't seem particularly affected by the fact of having "many" more groups. I guess this is due to the fact that when computing groups, Mace4 has a redundancy factor (finds many isomorphic models) that can be orders of magnitude higher than the actual number of isoclasses.
Zoltan A. Kocsis (Z.A.K.) ha dicho:
This looks like a significant potential speedup to me.
Yes, this is a nice idea! I've written a Sage script to generate the code (I've seen @Giovanni Paolini's answer later :melting_face:) also using GAP's database.
There is indeed a significant speedup, although at the cost of quite more RAM (if we want to check all groups of a given order in one batch), since Mace4 evaluates all possibilities of all given clauses at the start. This also needs a significant amount of time, although much less than exhausting the size with the other method, if there are few groups. For example, for order 25 where we have two nonisomorphic groups, Mace4 has needed 18min to start the actual computation.
Here we find a wall I've been hitting a few times with Prover9/Mace4: no matter what memory limit you set up (even unlimited), it seems that it allows an absolute maximum of 1GB, and ignores any quantity above that. Do you know any way of shortcircuiting this? (Perhaps we could look at the code and modify it). I know there is (at least) a non-official newer version of Prover9/Mace4, available in Github, do you know if it is trustworthy?
Otherwise to avoid this artificial limit, we'll need to check groups in small batches.
Times with the explicit-groups method:
size 14 (2 models) in 18s, size 15 (1 model) in 1s, size 16 too much RAM (14 models), size 17 (1 model) in 7s, size 18 too much RAM (5 models), size 19 (1 model) in 46s, size 20 too much RAM (5 models), size 21 (2 models) starting up for a good while, size 23 (1 model) running for 20min…
Jose Brox (Jan 16 2025 at 00:55):
I attach my Sage code:
MAGMAS PROJECT - Translate group Cayley table into MACE4 format.ipynb
MAGMAS PROJECT - Translate group Cayley table into MACE4 format.py
At present it only generates the groups clauses, which I copy-paste to a pregenerated Mace4 script. Tomorrow I will update the code to run Mace4 directly from the file and partition the groups in smaller batches.
Bruno Le Floch (Jan 16 2025 at 08:35):
To me it seems much better to do one mace4 run for each group, rather than messing with the RAM. The calculations for different groups are completely independent anyway. Besides, it would give you more comparable timings, as a function of the group size and perhaps other aspects of its structure.
Notification Bot (Jan 16 2025 at 12:22):
2 messages were moved from this topic to #Equational > Mace4 malloc issues by Zoltan A. Kocsis (Z.A.K.).
Jose Brox (Jan 16 2025 at 12:32):
Bruno Le Floch ha dicho:
To me it seems much better to do one mace4 run for each group, rather than messing with the RAM
I agree (once I write the code), but the RAM problem is important anyway, because eventually it will also affect computations with single groups when they are big enough, so we need to get rid of this artificial bottleneck (also for Prover9 computations with bijectivity conditions).
Terence Tao (Jan 16 2025 at 16:35):
= Daniel Weber said:
Is there an infinite counterexample where is bijective? Maybe we can try to construct such an example with the greedy method
I played around with this idea more and came to the conclusion that a greedy construction will be quite difficult once one has left invertibility. 677 plus left invertibility implies the laws
and also (substituting and cancelling a )
and hence
so on substituting ,
The upshot of this is that if one is performing a greedy algorithm and wants to assign for some novel , then (if one wants to retain on left invertibility) one may also have to assign if all the sub-expressions in the left-hand side are already defined by the partially defined operation. The problem is that this rule may propagate indefinitely, and when combined with the other rules forced by 677 could eventually lead to collisions that seem quite hard to rule out. It also suggests that the free magma generated by 677 and left invertibiilty may be rather complicated.
In comparison, the greedy rule for 677 without left-invertibility is simpler: when imposing for a novel , also impose for any for which . But no further relations of the form are generated.
Jose Brox (Jan 16 2025 at 17:25):
The new Sage script for translation-invariant models for all f with explicit groups, checked group by group, is already running. The previous summary is that there are no models for groups of orders 2-23,25 (included). I'm currently running orders 24 and 26.
I attach the Sage Jupyter notebook:
MAGMAS PROJECT - 677 anti 255 translation-invariant all f explicit groups.ipynb
@Bruno Le Floch with the script you can collect the running time for each group. In this doc file you can find the times for all groups in orders 16-20:
677 anti 255 translation-invariant all f explicit groups timings.docx
I've also modified the script to run the case, currently in size 32:
MAGMAS PROJECT - 677 anti 255 translation-invariant f^4=1 explicit groups.ipynb
Jose Brox (Jan 21 2025 at 22:37):
Quick update of negative results:
No models of 677+4293 anti 255 in size 16 (2.1 days).
No models of 677+4599 anti 255 in size 20 (7.5 days).
No translation-invariant models with any in sizes 24-26 (2.6d, 8h, 10.5h respectively).
No translation-invariant models with in size 34 (3.8h, size 32 still running).
Running time for each group in translation-invariant models with any , in minutes:
TIME PER GROUP
Jihoon Hyun (Jan 23 2025 at 17:00):
I was searching for magma of size 15, with 677 anti 255. After 526k seconds(6 days) I got a segfault for some reason, and the solver spiited out an unknown result. Magmas of size 13 and 14 with same condition are still running. Still, I wanted to state that it is unlikely to find magma of size 15 with 677 anti 255. I used cadical with this code as a generator.
Terence Tao (Jan 30 2025 at 17:44):
I have decided to bow to reality and rewrite the portion of the draft paper that tentatively claimed that both the infinite and finite magma implication graph was completed by the ETP, and instead posing 677->255 as an open problem: equational#1071 . Of course, if there is a new breakthrough on this implication before the paper is finalized, we can update the paper accordingly, but at our current trajectory it appears that the three remaining known anti-implications for the infinite graph will be formalized first, which I think would be a natural time to "declare victory" and then focus on finishing the paper.
Matthew Bolan (Jan 31 2025 at 16:13):
Do we have a single finite 677 magma which is not linear and generated by only 1 element?
Terence Tao (Jan 31 2025 at 16:26):
Not that I know of, though in principle the cohomological construction might be able to provide one (of course the linear base magma would have to be of the "Type II" kind without idempotents).
Matthew Bolan (Jan 31 2025 at 16:36):
Ah, I thought I had checked those, but further inspection revealed a bug. Here is a non-linear order 49 magma which is generated by a single element (Any element works as a generator, and it is non-linear as )
677_nonlinear_1_generated.txt
Bruno Le Floch (Feb 02 2025 at 22:45):
Claim: in a 677 magma, for a given , (iv) implies (iii) implies (ii) implies (i) implies that obeys 255. We already knew this last implication, which was quite useful in finding immunities. I think these observations are useless, but who knows, maybe someone will get inspired.
Proof of the implications
It might be interesting to look for a magma such that equation 255 is obeyed by none of the elements. This would mean that (i)-(iv) above are always violated, so and and and have no fixed point (where is the squaring map).
Terence Tao (Feb 02 2025 at 23:10):
Nice observations! I just added them to the 677 chapter in the blueprint, just in case they are useful in the future. I suspect that many of these implications are in fact reversible, so that this leads to several new equivalent conditions for 255.
Matthew Bolan (Feb 03 2025 at 00:03):
Prover 9 suggests that obeying 255 implies (iv) for in a 677 magma, so they should all be equivalent conditions to 255.
Proof
Viliam Vadocz (Feb 03 2025 at 01:35):
Hello, I would like to try finding a counterexample (via automated search). I skimmed the paper (accessed from the dashboard) looking for what has been tried. I did not see much mentioned about this particular implication.
- Am I looking at the most recent version of the paper? If not, where can I see the latest version?
- Is there a better way to get caught up on this particular problem?
- I would also like to know how the implication for the infinite magmas was shown to be false. Where could I see that?
Terence Tao (Feb 03 2025 at 01:41):
Welcome! This particular Zulip thread is probably the main location to record all the different things that have been tried for this specific implication, with some of what we have done also recorded on the blueprint at https://teorth.github.io/equational_theories/blueprint/677-chapter.html , which contains details of the infinite magma construction as well.
Matthew Bolan (Feb 03 2025 at 06:04):
Somewhat unimportant, but I was thinking a bit about other ways to detect if a magma is linear, and I noticed that in commutative linear magmas, any linear map is a homomorphism as . In particular, checking whether squaring (or more general maps like is a homomorphism seems to be a fast test for linearity which works well for 677 magmas.
Bruno Le Floch (Feb 04 2025 at 10:42):
A human-understandable proof that my implications above are equivalences, loosely based on Matthew's prover9 output above. I'll follow his lead denoting by the element whose properties we are looking at.
- 255 obeyed by implies (i) by taking so ;
- (i) implies (ii) by taking so so so ;
- (ii) implies (iii) by taking so ;
- (iii) implies (iv) by writing .
So all around quite trivial equivalences.
Terence Tao (Feb 04 2025 at 17:26):
I've updated the blueprint to state these equivalences more explicitly.
I was playing around with a graphical interpretation of (left-invertible) 677 and came up with the following, though I wasn't able to get further with it. We replace the magma operation with a labeled directed graph by writing if . Then left cancellability means that the edges labeled by form a permutation. The law 677 then concerns paths of the form
Namely, any incomplete path that contains all of the above four edges except for one of the first three, can be completed by adding in the missing edge. For instance,
can be completed to
Indeed, if one replaces by and performs all the obvious substitutions, then the incomplete path is
and completing the path precisely corresponds to 677 holding for this choice of . Completing the first or second edge corresponds to other equivalent forms of 677 (assuming left cancellativity) that we have worked out in the past (and are also recorded in the blueprint). (Completing the final edge is more problematic, this seems to require right cancellativity which we know can fail.)
Shreyas Srinivas (Feb 04 2025 at 17:27):
I noticed an issue in the blueprint and wasn't sure if it was worth creating a separate thread for. We speak about duals of equations in chapter 2 of the blueprint without defining duality first.
Shreyas Srinivas (Feb 04 2025 at 17:28):
This could potentially be fixed in any PR that updates the blueprint
Shreyas Srinivas (Feb 04 2025 at 17:31):
The first occurrence of duality appears to be Chapter 4
Terence Tao (Feb 04 2025 at 17:44):
I've added a forward reference to Chapter 4 in Chapter 2 to reflect this.
The blueprint is something of an organic mess right now; the paper has supplanted it as the main "official" record of the general theory, so it's main remaining purpose is to guide the formalization of the last few outstanding implications, though we did not really follow the paradigm of other formalization projects in strictly following the blueprint to decompose large formalization tasks into modular small components.
Shreyas Srinivas (Feb 04 2025 at 17:46):
I think we should try to keep the blueprint consistent with the paper since we need a way to cross check things we say in the paper
Shreyas Srinivas (Feb 04 2025 at 17:47):
Not only now, but whenever the reviewers get back (presumably a few weeks or months) and we have forgotten stuff
Shreyas Srinivas (Feb 04 2025 at 17:47):
It's our equivalent of a lab notebook (without all the bureaucratic requirements associated with one).
Terence Tao (Feb 04 2025 at 17:51):
I agree that we should maintain notational consistency between the blueprint and the paper. But I am much more relaxed about having inconsistent emphasis of material between the two. For instance the set of equations singled out in Chapter 2 of the blueprint is now somewhat different from the set of equations listed in the appendix of the paper (or from the "selected equations" page of the Github wiki, or the "commentary" pages in Equation Explorer), for a number of reasons, and similarly some proofs in the paper are arranged a little differently from their counterparts in the blueprint. But I think as long as everything is technically correct and the notation is consistent, this should not be a major issue.
Matthew Bolan (Feb 04 2025 at 18:00):
To return to 677, an outside idea for why the implication might hold in the finite setting that I've been playing with is to try and find in any magma violating 255 a proper submagma violating 255, in which case we would be done by infinite descent. I have no real reason to believe this is possible, besides that I think it is true of the free 677 magma. ATP seems to find no issue with a magma having only a single 255 counterexample, so probably the idea would need to be tweaked to find infinitely many distinct elements some other way. Still, in my personal list of reasons why an implication could imaginably hold for finite magmas and not infinite ones, this is up there and has a slightly different flavor to the methods we've tried so far. I personally believe the implication to be false though.
Bruno Le Floch (Feb 05 2025 at 00:01):
Relatedly, ATP seem to find no immediate problem with having a single counterexample 2*0=1*0
to right-cancellativity (but I have no idea if my Prover9 settings are useful values).
assign(sos_limit, 2000).
assign(max_weight, 1000).
assign(max_seconds, 200).
formulas(sos).
y*(x*((y*x)*y))=x. % eq 677
(y*x)*((y*(y*x))*y)=x. % consequence
(x*y = x*z) -> (y = z). % left-cancellativity
2*0 = 1*0. 1 != 0. 2 != 1. 2 != 0. % failure of right-cancellativity
(x*z = y*z) -> (x = y | (x = 1 & y = 2 & z = 0) | (x = 2 & y = 1 & z = 0)). % no other failure
end_of_list.
Matthew Bolan (Feb 05 2025 at 00:10):
Hmm, for finite magmas we know that there must be more than one counterexample to right-cancellativity, as in a magma of order left cancellativity implies each element is a product of two elements in exactly ways, but then if is the unique failure of right cancellativity, is a product of two elements in exactly ways, by right cancellativity away from .
Bruno Le Floch (Feb 05 2025 at 00:48):
Great! What you just pointed out hints to an effect of finiteness that is not yet captured in any of the ATP runs as far as I know. Maybe there is a way to state it without involving the cardinal explicitly?
Matthew Bolan (Feb 05 2025 at 00:54):
One consequence that actually seems to be speeding up Mace4 quite a bit for me (Edit: I misremembered the old timings, a new control run suggests it isn't such a great speed-up) is that given some element , we can solve , if and only if there is an element such that for all .
Matthew Bolan (Feb 05 2025 at 01:03):
That's interesting for 255, since if , then for all , so we must have b,c,d with and .
Bruno Le Floch (Feb 05 2025 at 12:09):
@Jose Brox If you are still running prover9/vampire on 677 + other equations + left-cancellativity, it might be interesting to also include Matthew's observation. I think it is all a ((exists b exists c exists d (b!=c & b*d=a & c*d=a)) <-> (exists e all f a!=f*e)).
Kevin M (Feb 26 2025 at 02:22):
Jihoon Hyun said:
Let be the number of elements of the magma.
I declared four types of variables: , , , and . Each variables are true if and only if for given and , the expression results in . They are named asvar1
tovar4
in the program.
...
The last restriction lets us find the magma which satisfies the equation 677 but not 255. For this we simply check the clause of all , to see if there is any false variable.
I think it is probably better to break symmetry here.
Instead of having a clause that is essentially "there exists an element for which eqn 255 does not hold", just require some specific element (for example: element 0) violates eqn 255. Which if I'm understanding, could be done by forcing true.
Kevin M (Feb 26 2025 at 02:24):
For what sizes has the SAT instance been run on?
I only have a little experimental experience with SAT solvers, but proving UNSAT seems to take exponentially longer than finding a SAT instance if it exists. So maybe it would be worth just running the SAT problem for different sizes, but just for 10 hours each size or something.
Does anyone have a fair amount of experimental experience with SAT such that they could give a (very rough) estimate of what sizes are even worth running here?
Maybe we could try this type of encoding on some other equation where the allowed sizes are known -- just to get a rough experimental idea of what sizes are feasible to explore with this SAT encoding.
Jihoon Hyun (Feb 26 2025 at 02:32):
Kevin M 말함:
For what sizes has the SAT instance been run on?
I only have a little experimental experience with SAT solvers, but proving UNSAT seems to take exponentially longer than finding a SAT instance if it exists. So maybe it would be worth just running the SAT problem for different sizes, but just for 10 hours each size or something.
Does anyone have a fair amount of experimental experience with SAT such that they could give a (very rough) estimate of what sizes are even worth running here?
Maybe we could try this type of encoding on some other equation where the allowed sizes are known -- just to get a rough experimental idea of what sizes are feasible to explore with this SAT encoding.
Currently it's running with size 12 to 17. To generate the cnf I'm currently using please check the git repository. I'll update the compilation part of the README in a few minutes. I updated the compilation part of the README. Please tell me if there are any issues when compiling.
You suggested some symmetry breaking, and I did implement it. It doesn't seem to give significant impact on large instances, though. (I mean, these are currently running for 3*10^6 seconds or so, and I can't tell if this was better with larger magmas. Still, breaking symmetries did reduce time for smaller instances, like n <= 10.)
Finally, please contact me any time if you have any questions about the source code.
zirconium.n (Mar 04 2025 at 08:25):
Hello, new here. Just read through the topic. I still have this naive problem, what's the rationale behind assuming 677 does not imply 255?
Vlad Tsyrklevich (Mar 04 2025 at 08:59):
People have also tried exploring that it may be an implication, but didn't make headway there, and it doesn't happen to fit the pattern of the other implications we have proved in the project. If it is an implication, it requires a new idea to prove it. I think most people do believe it is a non-implication though, because of the failed attempts to find proof that it is an implication.
Zoltan A. Kocsis (Z.A.K.) (Mar 04 2025 at 10:20):
@zirconium.n
As Vlad Tsyrklevich points out, one reason comes by an argument from ignorance: assuming something fails because we tried hard but failed to prove that it holds. Indeed, we tried all our tricks to prove the 677->255
implication but made no progress. If it holds, its proof has to be quite unlike any other proof we've done over the course of the project.
But that's not all. As things stand, it looks quite plausible to me that most non-right-cancellative models of 677 would refute 677->255
, and we're just not very good at constructing such models. Let me elaborate.
We know that a countermodel to 677 -> 255
cannot be right-cancellative. Constructing a non-right-cancellative model of 677 is therefore no harder than constructing a countermodel to 677->255
. But when we actually try to construct non-right-cancellative finite models of 677, the very same difficulties appear as when we try to prove the 677->255
implication:
- Typical finiteness assumptions, such as function periodicity, injections coinciding with bijections, do not help our ATP tools prove the statement.
- Mace4 and similar tools fail to construct a countermodel, possibly because even the smallest ones exceed feasible size limits.
- The methods that we devised to extend existing models to larger models while refuting some property provably break down (i.e. we can prove that they would only work if the existing model was already a counterexample, and then there'd be no reason to use them).
Yet non-right-cancellative models of 677 turn out to exist! No small examples are known, of course: computer searches found none, and the smallest known case (whose table was computed by Matthew Bolan) has order 496. Worse, the only method we currently know to construct such models (due to Tao) always yields idempotent magmas, and such magmas cannot serve as counterexamples to 677->255
.
The overall pattern, and the fact that we could eventually construct non-right-cancellative models of 677, strongly suggest to me that we will eventually be able to construct countermodels to 677->255
as well: all known difficulties appear quite similar. Indeed, it looks plausible to me that most non-right-cancellative models of 677 would refute 677->255
as well, and we just got unlucky in that the first working attempt to produce non-right-cancellative models yielded idempotent ones.
Matthew Bolan (Mar 04 2025 at 14:27):
Terry's construction yields infinitely many non-right-cancellative models, one for each field supporting a 15th root of unity. The model corresponding to will be of order . All I did was produce the table corresponding to to confirm it worked.
Zoltan A. Kocsis (Z.A.K.) (Mar 04 2025 at 14:46):
@Matthew Bolan I know that this results in infinitely many models: the point is that even the smallest one among them (the one whose operation table you computed) is large. And as I stated above, the models resulting from this construction are all idempotent, so satisfy 255.
Matthew Bolan (Mar 04 2025 at 15:06):
Right, I don't doubt that you know this, and I agree with your message. I was mostly reacting to the phrase "and the only case we could work out" which could mislead someone new to the project into thinking it was unique, or that the other models in the family are hard to compute (actually before I remembered I computed an order model, which I can dig up or recompute if anyone wants it).
Zoltan A. Kocsis (Z.A.K.) (Mar 04 2025 at 16:07):
@Matthew Bolan Thanks, that makes sense! I've now edited the comment and changed that phrase to clarify this.
zirconium.n (Mar 07 2025 at 09:22):
Thank you for the explanations! These are very insightful. I will read through the topic again to gain further understandings. I think I will try to prove the positive result anyway (after reading all failed attempts ofc), since I get the feeling we get way more exploration on the anti-implication side. But surely it seems requires some creative thinking...
Jose Brox (Mar 12 2025 at 10:18):
Jihoon Hyun ha dicho:
Magmas of size 13 and 14 with same condition are still running. Still, I wanted to state that it is unlikely to find magma of size 15 with 677 anti 255.
Did your computations for 13 and 14 finished eventually? And have you been able to exhaust sizes 11 and 12 with cadical? If this is the case, how much time did the size 11 computation need?
Jose Brox (Mar 12 2025 at 10:20):
Matthew Bolan ha dicho:
Here is a non-linear order 49 magma
How did you find this magma, was it in the course of some more general search?
Jose Brox (Mar 12 2025 at 10:54):
Bruno Le Floch ha dicho:
@Jose Brox If you are still running prover9/vampire on 677 + other equations + left-cancellativity, it might be interesting to also include Matthew's observation. I think it is
all a ((exists b exists c exists d (b!=c & b*d=a & c*d=a)) <-> (exists e all f a!=f*e)).
In my experience this kind of formula, with existence quantifiers or inequalities of elements, often does not improve MACE4 computing time, and this is consistent with the inner workings of the program: at the start it generates all combinations of elements of each formula, then applies its "sudoku" algorithm.
Nevertheless I have tried it for small sizes, and the computation is quite slower. But perhaps we can give another formulation which is better suited to MACE4.
I have also tried adding it as a finiteness condition to PROVER9, but it hasn't provided a proof. I will try with Vampire later, as it seems to be better for finding proofs when formulas have implications.
Jose Brox (Mar 12 2025 at 11:30):
While I was in bureaucratic hell (from which I'm starting to return!), some more negative results have been found by my MACE4 experiments farm. We have exhausted:
- 677 anti 255: size 11 (57 days).
- 677+513+3659 anti 255: size 14 (34d).
- 677+4073 anti 255: size 14 (17h).
- 677+4131 anti 255: size 15 (57d).
- 677+4321 anti 255: size 15 (2d).
Moreover, since there seems neither PROVER9 nor Vampire find any problems with a 677 model having just one failure of 255, I have also experimented with adding that condition to the 677 anti 255 search, giving a speedup of 3 for size 9, 5 for size 10, and 13 for size 11 (for which it needed 4.5 days). It is currently running in size 12.
I have also played with the idea of the magma operation * being the product of a nonassociative "semirring" (R,+,*): we of course remove 0 and opposites for +, but even then, if both distributive laws are satisfied, then PROVER9 can show that 677 implies 255 (under left cancellativity and the equation consequence of 677). Neither PROVER9 nor Vampire have been able to show the same when one of the two distributive laws is removed, so I'm running these "one-legged 677 semirring" experiments.
Having left distributivity is much better for computations, so we may guess that in this case 677 actually implies 255; with left distributivity I have already exhausted size 24 (16h), while with right distributivity is still running in size 12.
Lastly, the translation-invariant experiments run group-by-group had a big crash and I have yet to resume them (I'm waiting for a SAGE update in my department's computer).
Jihoon Hyun (Mar 12 2025 at 12:45):
Jose Brox said:
Jihoon Hyun ha dicho:
Magmas of size 13 and 14 with same condition are still running. Still, I wanted to state that it is unlikely to find magma of size 15 with 677 anti 255.
Did your computations for 13 and 14 finished eventually? And have you have been able to exhaust sizes 11 and 12 with cadical? If this is the case, how much time did the size 11 computation need?
I didn't run it for size 11 as I thought you were exploring that space. Also there was a blackout once, so currently all experiments from size 12 to 17 are running for 4*10^6 seconds.
Matthew Bolan (Mar 12 2025 at 17:25):
Jose Brox said:
How did you find this magma, was it in the course of some more general search?
It was among the cohomological extension models I had already computed. It is an extension of an order 7 example by another.
Jihoon Hyun (Mar 13 2025 at 02:12):
I leave a small lemma before I forget: If , then holds, and satisfies Equation 255.
Jihoon Hyun (Mar 25 2025 at 07:16):
I asked gpt to generate a visualizer of a magma. The result was satisfying, so I share the script here. All you have to do is to prepare a text file which contains a single integer representing the size of the magma, and the next n lines containing n integers each which is the magma multiplication table.
Python script
Example input:
After importing the file, you should choose a number from 0 to n - 1. Red and blue arrows will appear in the graph, which represents the left and right multiplication of the selected number, respectively.
Jihoon Hyun (Mar 26 2025 at 05:39):
- Is there a non-right-cancellative finite 677 magma which is not idempotent? The non-right-cancellative model with elements uploaded here is idempotent.
- Do all finite magmas satisfying 677 have a unique idempotent element, unless all elements are idempotent?
- Is there an explicit example of non-isomorphic finite 677 magmas with equal order?
Terence Tao (Mar 26 2025 at 05:41):
I think one can answer these questions with the direct product construction. For instance, by taking the direct product of the idempotent non-right-cancellative finite model and a non-idempotent finite model one should get a finite model that is both non-right-cancellative and non-idempotent. Similarly for the second question. For the third one should be able to take the product of two linear models on which could be distinguished from a linear model on .
Jose Brox (Mar 26 2025 at 11:19):
Jihoon Hyun ha dicho:
- Is there an explicit example of non-isomorphic finite 677 magmas with equal order?
The first size in which this happens is 7, in which there are two isoclasses of 677 models. Here you have two representatives:
NON-ISOMORPHIC MODELS OF SIZE 7
Jihoon Hyun (Apr 02 2025 at 09:40):
After looking into several 677 magmas, I now have a conjecture that when . This will give at least two fixed points for a map unless or not 255.
Jihoon Hyun (Apr 16 2025 at 03:51):
17.zip
I had to interrupt cadical running for magma (satisfying 677 but not 255) of size 17. Here are cnf and its corresponding log.
Jose Brox (Apr 29 2025 at 10:40):
Perhaps you know that yesterday there was a national electrical blackout in Spain (where I'm located) for several hours. Luckily, the computer where my experiments farm is running is sited inside a tier 2 data center, what has allowed the computations to survive the blackout. So the 23 experiments I'm running for 677 are still going on (although they may not matter much now with the initial project being officially completed, modulo the paper).
Bruno Le Floch (May 01 2025 at 22:53):
Can someone with more computing power check that ATPs fail to prove 255 from ((x*y)*z)*x=((x*z)*(y*z))*x
and 677 and left-cancellability and existence of an idempotent? Same question for ((x*y)*z)*y=((x*z)*(y*z))*y
instead. Among 3-variable equations obeyed by linear 677-magmas of type 1 (a+b=1
and b^4-b^3+b^2-b+1=0
) they are the simplest that might not imply 255.
Then, I would seek Lie magmas obeying 677 and that equation, constructed order by order around an idempotent element. With a 3-variable equation, the lowest-order terms in the expansion typically fix the higher-order terms, just like a Lie algebra exponentiates to a Lie group by Lie's third theorem —with possible non-perturbative obstructions.
Last updated: May 02 2025 at 03:31 UTC