Equations with full spectrum

Stream: Equational

[Jose Brox]

As a future direction, @Ibrahim Tencer asked 1) which equations have models of all finite sizes (i.e., have full spectrum), and 2) among those which have directly irreducible models of all sizes.

I did some work on 1) a while ago that I'm continuing a bit now in order to report before leaving on Christmas holidays.

As Ibrahim noted, if an equation has an operation on either side then it will allow the constant model of any size, while if it is of the form $x = f$ with $x$ as the right-most or left-most variable in $f$ then it will be implied by one of the absorption laws and also have a model of any size (where all elements of each row or column respectively are equal to its index). This we can readily identify: up to 4694 there are 2946, which can be found in the following file:
Theoretically full spectrum up to 4694.txt

[Jose Brox]

Next thing I did was to try to find countermodels for the remaining equations (note that since varieties are closed under products, only prime orders need to be checked). From computing up to 19, I got a list of equations without full spectrum since they fail for some prime, another with a list of equations that probably have full spectrum, since they have a model for each prime up to 19, and a list of inconclusive equations, for which no model was found for some prime in the allowed time without exhausting the search space.

The 1620 equations we know don't have full spectrum are in the following file:
Not full spectrum up to 4694.txt

The ones with possibly full spectrum are the following 17:

POSSIBLY FULL SPECTRUM

504: x = y * (y * (x * (y * y))).
508: x = y * (y * (x * (z * z))).
910: x = y * ((y * x) * (y * y)).
914: x = y * ((y * x) * (z * z)).
1519: x = (y * y) * (x * (y * y)).
1523: x = (y * y) * (x * (z * z)).
1722: x = (y * y) * ((x * y) * y).
1726: x = (y * y) * ((x * z) * z).

---

1925: x = (y * (y * x)) * (y * y). (Dual of 1722)
1929: x = (y * (y * x)) * (z * z). (Dual of 1726)
2125: x = ((y * y) * x) * (x * y).
2128: x = ((y * y) * x) * (y * y). (Dual of 1519)
2132: x = ((y * y) * x) * (z * z). (Dual of 1523)
2737: x = ((y * y) * (x * y)) * y. (Dual of 910)
2741: x = ((y * y) * (x * z)) * z. (Dual of 914)
3143: x = (((y * y) * x) * y) * y. (Dual of 504)
3147: x = (((y * y) * x) * z) * z. (Dual of 508)

Observe that except 2125 they come in pairs in which $p\implies q$, with
$p(x,y)=q(x,y,z=y)$; then it is enough to show that $p$ has full spectrum, since $q$ has at least the same models as $p$. Observe also that the second half of the list (except 2125) is formed by the duals of the first half, so we can ignore those. We are therefore reduced the study to 5 equations: 504, 910, 1519, 1722, and 2125.

We can actually show that 504 $x = y * (y * (x * (y * y)))$ has full spectrum:
For the multiplication table of the model, take as first row
$(0,n-1,n-2,...,1)$
and cyclically permute it to the right iteratively to get the next rows, so that
$x*x=0$ and $x*0 = x$. Then $x = y * (y * (x * (y *y)))$ is satisfied in the model iff $x = y*(y*x)$, and this is true because the permutation given by each row is a product of disjoint transpositions (and fixed points).

We should study the other 4 in a similar fashion (didn't have the time yet).

[Jose Brox]

Lastly, the list of the 111 inconclusive equations together with their failed primes is in the following file:
Inconclusive spectrum up to 4694.txt

More work needs to be done on this, for example the first two equations are pretty small and we should be able to determine them theoretically:

14: x = y * (x * y).
29: x = (y * x) * y.

[Douglas McNeil]

For 504, 910, and 1519 it looks like we can take a model with x*y = y except 0*y=y , x*0=x, and x*x=0.
Almost the same for 1722 except we flip y to x in the "standard" value: x*y = x except 0*y=y , x*0=x, and x*x=0.

[Bruno Le Floch]

Interesting question indeed!

• For equations 14, 29, 464, 477, 489, 492, 511, 522, 572, 680, 684, 692 etc (actually 80 of your 111 equations!) the same linear model $x\diamond y=-x-y\mod n$ on the carrier $\mathbb{Z}/n\mathbb{Z}$ works. More generally, I suspect that others can be eliminated by linear models.
• Equation 543 is Tarski's axiom for abelian groups with subtraction so it has full spectrum by $(\mathbb{Z}/n\mathbb{Z},-)$.

[Bruno Le Floch]

The three linear models $x\diamond y\to \pm x\pm y$ on $\mathbb{Z}/n\mathbb{Z}$ with the choices of signs $(\pm,\pm)=(-,-),(+,-),(-,+)$ show that 108 of the 111 have full spectrum. The remaining equations are

Equation 1482: x = (y ◇ x) ◇ (x ◇ (y ◇ y))
Equation 1682: x = (y ◇ x) ◇ ((x ◇ x) ◇ y)
Equation 1885: x = (y ◇ (x ◇ x)) ◇ (x ◇ y)

which are a dual pair 1682-1885, and also the dual 1482 of 2125 that was confusingly alone in the other list.

[Douglas McNeil]

2125 can be modelled by x * y = 1 except 1*1=0, 1*y=y for y !=0,1, and x*1=x for x != 0,1.

[Bruno Le Floch]

Equation 1682 (and 1885) has linear models $x\diamond y=ix-y\mod p$ whenever there exists a solution of $i^2=-1\mod p$, so that gives a model for all primes $p=1\mod 4$. The models that mace4 finds for $p=3,7$ do not have obvious structure.

[Bruno Le Floch]

Equation 1523 x = (y ◇ y) ◇ (x ◇ (z ◇ z)) and its dual equation 2132 have a family of models with x*x=0 and x*0=0*x=x, and other entries unspecified, so they have full spectrum.

[Jose Brox]

Amazing job, guys! :tada:

Douglas McNeil ha dicho:

For 504, 910, and 1519 it looks like we can take a model with x*y = y except 0*y=y , x*0=x, and x*x=x.

You mean $x*x=0$, right? (And $0*y=y$ is superseded by $x*y=y$). The same for the flipped version.

[Bruno Le Floch]

Out of the 4694 equations,

• 1620 do not have full spectrum (ATP search by Jose);
• 3072 have full spectrum, by constant or absorbing models (2946 of them), or by linear models $x\diamond y=\pm x\pm y$ (122 additional ones), or by Douglas' model (for equations 1482 and 2125), or by my last message (for equations 1523 and 2132);
• 2 are unknown: for the dual pair 1682-1885 we don't know existence of models with prime order $p=3\mod 4$.

[Bruno Le Floch]

For these last two equations, I think we can take a model of equation 29 x = (y * x) * y and add to it a unit 0 and set x*x=0 and x * 0 = x and 0 * x = x. I'm not sure which orders this works for. I have to run and be busy for the next few hours.

[Douglas McNeil]

@Jose Brox : oops, yeah, 0, I'll edit. The superseding I'm not worried about because it made a more symmetric setup in vampire. Basically to my eyes the model looks like "mostly one thing with some changes" rather than "this combination of things" even if the latter is more concise. :-)

[Jose Brox]

(deleted)

[Jose Brox]

Bruno Le Floch ha dicho:

For these last two equations, I think we can take a model of equation 29 x = (y * x) * y and add to it a unit 0 and set x*x=0 and x * 0 = x and 0 * x = x.

This has a problem: we have x*(n-2x) = x, so (x*(n-2x))*x = x*x=0 instead of n-2x; and since the model is linear, there is only one value y giving y*x = n-2x (which is y=x), making it impossible to just change x*(n-2x) to another value.

[Douglas McNeil]

Do we have any order 11 or order 17 examples? Or is this one of those 677-like cases where they exist but it takes an eternity to find them?

[Jose Brox]

Douglas McNeil ha dicho:

Do we have any order 11 or order 17 examples? Or is this one of those 677-like cases where they exist but it takes an eternity to find them?

I'm computing models of size 11 for 1682 right now. In 660s I've got 1408 models (may be isomorphic), I'm waiting to see if I can exhaust the size and get all isoclasses. This is done with selection_measure 1, skolems_last set in Mace4.

[Douglas McNeil]

Ha, I've gotten too used to -M 3 -O 2 lately! Thanks,

[Jose Brox]

It is a bore, but I always check first the best combination among (2,1/3/4,yes/no) with smaller sizes, then start the long run. I want to write a script for this to make the process automatic (and upload it to the project), but it is not as easy as it seems, because it depends on whether we want just one model or exhaust the search, and whether there are many models or very few.

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

We likely have models of 1682 + 8 + 23 in any size, and constructing them should not be difficult. I think this because Mace4 can find models of 1682 + 8 + 23 whose m x m prefix also forms a closed model of 1682 + 8 + 23 for any m. This suggests that there is probably a construction which extends a model of 1682 + 8 + 23 of size n to one of size n+1. I believe Weber-style greedy methods will probably suffice to find such a construction (in fact, one might be able to read one off from the example below).

Here's such a model of size 17 - click for FME:

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

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

(keep in mind that there are a whole lot of non-isomorphic such models, even in low sizes, and some may have a lot more legible structure than this one)

[Jose Brox]

Zoltan A. Kocsis (Z.A.K.) ha dicho:

Mace4 can find models of 1682 + 8 + 23 whose m x m prefix also forms a closed model of 1682 + 8 + 23 for any m.

Very interesting! Which clauses do you use to get this kind of search?

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

@Jose Brox You can run the following Python script to generate the formulas I used.

def generate_formulas(n):
    formulas = []
    for i in range(1, n):
        formulas.append(f"  all x all y (\n    S{i}(x) & S{i}(y) ->\n    S{i}(x * y)\n  ).")
        if i == 1:
            formulas.append(f"  all x ( -S{i}(x) <-> x = {n} ).")
        else:
            formulas.append(f"  all x ( -S{i}(x) <-> (-S{i-1}(x) | x = {n-i+1}) ).")
    return "\n\n".join(formulas)


n = 17  # Change this value to adjust the sequence length
result = generate_formulas(n-1)
print(result)

[Bruno Le Floch]

Here is Zoltan's model as a python function taking two non-negative integers and producing a non-negative integer. It is a model on $\mathbb{N}$ which obeys 2125 (and probably other equations, as he mentioned) and the property that $i\diamond j\leq\max(i,j)$ for all $i,j$, so that one can truncate the model to any size. I did not prove these facts, but the construction is "smooth" enough that testing them to some medium order guarantees that it works (probably order 5 or so would be enough).

def m(i, j):
   if j == 0:
      return i
   if j == 1:
      return (1 if i == 0 else 0)
   if ((i + j) % 2 == 0):
      if i >= 2 and j >= 2:
         return (i if i >= j else i + 1)
      if i == 1 and j >= 3:
         return j
      if i == 0 and j >= 2:
         return 1
   if ((i + j) % 2 == 1):
      if i >= 1 and j >= 3:
         return (j if j > i else j - 1)
      if i == 1 and j == 2:
         return 2
      if i == 0 and j >= 3:
         return 2
      if i >= 3 and j == 2:
         return 0
   return (i, j)

print(all(m(i,j) <= max(i,j) for i in range(100) for j in range(100))) # True
print(all(m(m(j,i),m(m(i,i),j)) == i for i in range(100) for j in range(100))) # True

[Bruno Le Floch]

Conclusion: out of the 4694 equations, 3074 equations have full spectrum, and 1620 do not. EDIT: should this discussion lead to a section, or does it have a natural home in another part of the paper?

[Jose Brox]

Zoltan A. Kocsis (Z.A.K.) ha dicho:

You can run the following Python script to generate the formulas I used.

Thank you! With this I realize that when writing formulas for ATPs I wasn't thinking about the power of predicates, just using functions, so this tip is making me aware of another tool. I'm always learning from your contributions! :big_smile:

[Jose Brox]

Bruno Le Floch ha dicho:

Conclusion

So, what about @Ibrahim Tencer 's question 2) about the varieties with full directly irreducible spectrum? I believe someone already had some written code to detect if a model was a product? Can someone share it or point to it?

[Bruno Le Floch]

Does "directly irreducible" mean that the magma is not a direct product of two magmas?

Almost all equations with full spectrum were proven to have such a spectrum by using linear models $x\diamond y=ax+by$ over $\mathbb{Z}/n\mathbb{Z}$ with $(a,b)$ among $(0,0)$ (constant law), $(1,0)$ or $(0,1)$ (projections), $(1,-1),(-1,1),(-1,-1)$ (which I used). We can start by asking when such a model is a direct product for composite $n$.

• For constant law and projections the product of two magmas is a magma with the same (constant or projection) law, so these constructions will only produce directly irreducible magmas of prime orders. So all of these equations would have to be revisited (e.g., all equations with the operation on both sides).

• For subtraction and backwards subtraction ($a=-b=\pm 1$) we are talking about a structure that captures all about the group $\mathbb{Z}/n\mathbb{Z}$, so direct irreducibility is the same as for the group. I think this means the magma is directly irreducible precisely when $n$ is a prime power.

• For $a=b=-1$ the magmas whose order is not a prime power are directly reducible for the same reason, but I am not totally sure whether all prime powers give directly irreducible magmas.

It seems we would need to go through the equations one by one to answer the question. Seems hard.

[Jose Brox]

Bruno Le Floch ha dicho:

It seems we would need to go through the equations one by one to answer the question. Seems hard.

Yep, that's why I think we need the product-detecting code :big_smile: Nevertheless, making a sweep to sieve most but a small fraction should be easily doable if we can integrate the code into the ATP formulas (for me this is what this project is all about: try to do as little abstract or algebraic reasoning as possible, and making the automatic tools do the work, so more programming and conditions reasoning).

[Bruno Le Floch]

Even if we don't have product-detecting code, you could exhaustively search for models of size $p$ and $q$ up to isomorphism, then build the direct products of order $pq$, and when seeking models of size $pq$, eliminate those that are isomorphic to any of the products.

[Ben Gunby-Mann]

This reminds me of something I was wondering about (though likely outside the purview of the current project) which is whether there exist any "nontrivial Wilf-equivalences"--pairs of equations that have the same number of models of size n for each integer n (labelled, i.e. isomorphic models are different though the question is still interesting if this is changed), but are neither equivalent to each other or each other's dual. Possibly there's a very easy positive answer to this that I'm missing, but I don't think there's any among two-operation or fewer equations except possibly the Putnam law, which I couldn't find a terse way of enumerating.

(For those who are curious, closed-form-or-at-least-somewhat-terse descriptions of enumerations for these with explanations for the nontrivial ones, leaving out duals or equivalences:
Equation 1: $n^{n^2}$

Equation 2: $1$ if $n=1$, $0$ otherwise

Equation 3: $n^{n^2-n}$

Equation 4: $1$

Equation 8: $(2n-1)^n n^{n^2-2n}$. Can construct each row separately; if $x\cdot x=x$ there are $n^{n-1}$ choices for the row and if $x\cdot x\neq x$ there are $n-1$ choices for $y:=x\cdot x$, whereupon $x\cdot y=x$ is forced and all other choices are free for $(n-1)n^{n-2}$ choices, so the total number of choices is $(n^{n-1}+(n-1)n^{n-2})^n$.

Equation 9: $\left(\displaystyle\sum_{k=1}^{n-1}\binom{n-1}{k}k^{n-k-1}\right)^n$. Again, rows can be constructed independently; the condition is that $L_x^2$ is the constant function $x$. Letting $y=x\cdot x$ we can confirm that $x\cdot x=x$. First choose the set $S:=\{y\neq x: x\cdot y=x\}$. If $|S|=k$, there are $\binom{n-1}{k}$ choices for $x$, and it is necessary and sufficient that $x\cdot y=x$ if $y\in S$ and $x\cdot y\in S$ otherwise.

Equation 10 (the most interesting one among these): $\displaystyle\sum_{G}\displaystyle\prod_{x\in V(G)} d_G(x)^{n-d_G(x)}$, where $G$ is taken over all graphs on $n$ vertices with potential self-loops.
Connect $x,y$ by an edge if $x\cdot y=x$. Note that by the given condition, if $y\cdot x=y$, then $x\cdot y=x$, so this is indeed a symmetric relation, and it is fully determined by the magma. The given condition $x\cdot (y\cdot x)=x$ says that $y\cdot x$ is adjacent to $x$ for all $y$. So there is only $1$ choice for $y\cdot x$ if $xy$ is an edge (namely $y$), and $d_G(x)$ choices all other times (note that as $xy$ is not an edge in this case, none of these choices will make $y\cdot x=y$, which would have contradicted our choice of $G$). This gives the formula above. It would be interesting if this could be simplified but I would be surprised.

Equation 11: $\displaystyle\sum_{k=1}^n\binom{n}{k}k^{n-k}n^{(n-1)(n-k)}$. Choose a set $S$ of squares, and suppose it has size $k$. Then for all $x$, $x\cdot x\in S$, and if $y\in S$, $x\cdot y=x$ (note that the first of these is redundant if $x\in S$). So the columns of all $k$ elements in $S$ are fully determined, the remaining $n-k$ diagonal elements must be one of the $k$ elements in $x$, and the remaining $(n-1)(n-k)$ elements may be freely chosen.

Equation 13: # of involutions on $n$ elements. Equivalent to $19$, which says that $L_yL_z=Id$ for all $y,z$. From this we can see that all $L_y$ must be involutions, and indeed must all be equal. This fully determines the multiplication table.

Equation 14 (Putnam equation): ???

Equation 16: (# of involutions on $n$ elements)^n. Again we may go row-by-row, and the equation says that $L_y^2=Id$. So each $L_y$ can be chosen to be an independent involution.

23-37: Dual to 8-22.

38: $n^n$.

40: $n^{n^2-n+1}$

41: $n$ (constant law)

43: $n^{\frac{n^2+n}{2}}$.)

[Terence Tao]

Wow, it's great that this problem got completely solved within 24 hours. The frustrations we are having right now with 677->255 are perhaps disguising the fact that we actually have developed a lot of powerful ways to create models of equational laws, and to use ATPs effectively. This can certainly go as a section of the paper or blueprint; I opened equational#1029 for this.

I'm on vacation right now so will not be particularly active on this project for the next week or two.

[Bruno Le Floch]

I think we should dig some more into Zoltan's model as it hints to a new construction method. There is an underlying magma on $\mathbb{Z}$ where the result of the operation is piecewise linear with the pieces depending both on the parity of operands and their ordering:

$$i\diamond j = \begin{cases} i + 1 & \text{if } i < j \text{ and } i + j = 0 \mod 2 , \\ i & \text{if } i \geq j \text{ and } i + j = 0 \mod 2 , \\ j & \text{if } i < j \text{ and } i + j = 1 \mod 2 , \\ j - 1 & \text{if } i \geq j \text{ and } i + j = 1 \mod 2 . \end{cases}$$

Then the model is tweaked to truncate it to non-negative values. I wonder how to abstract both of these constructions to general abelian groups, in hope to apply it to 677→255 (or other stubborn equations such as those in the "Some results from order 5" topic, or the Higman-Neumann one.)

[Vlad Tsyrklevich]

I've been formalizing some bits of this to practice Lean. I just got to the point where I looked at transitively reducing the proofs and I was surprised that there are fewer necessary proofs that what I would have expected. For proving full spectrum equations, I believe you only need 7 proofs (up to transitive closure and duality). For the negative proofs, there are slightly more, 32 I believe.

[Vlad Tsyrklevich]

Assuming I have not made an error, I have all the positive cases proved. (Including a proof that Bruno's 1682 python code above is indeed a model at all cardinalities >2.)

[Bruno Le Floch]

Do you formalize the fact that all 4-variable equations fit in one of your formalized results, or do you check it with other tools? I've been wondering whether we should have formalize a Lean analogue of the find_equation_id.py script that maps equation ids to equations and vice-versa. But then we would want to define some kind of infinite stream of equations, with tools to access the n-th item, but also ways to get all equations with a given order, or a given number of different variables, a given shape, etc.

[Vlad Tsyrklevich]

Do you mean 4 operation or 4 variable?

[Vlad Tsyrklevich]

I have only formalized individual results, I am interested in a completeness result as well just to experiment, but first I need to formalize the negative cases.

[Bruno Le Floch]

Sorry, indeed I meant the 4694 operations that this project has mostly been about. How come there are so few negative proofs needed? Is it that most of the equations to rule out imply one of a list of 32 basic equations? Do these basic equations have any particular recognizable structure?

[Vlad Tsyrklevich]

Full spectrum equations represent a cut in the graph: if an equation is full spectrum, then every equation it implies is also full spectrum. Conversely, if an equation is not full spectrum, then clearly every one which implies it is also not. So one way to think about it is that a couple of (pretty general) equations have the full spectrum property, and the 32 (modulo duality) equations are the leftovers on the other side of the cut of the full spectrum equations transitive closure. I don't know that that is really a satisfying answer to "why", but it helped me understand why the number could be so much fewer than what I had expected. I haven't looked too much at the negative equations specifically.

The minimal set of equations that I've calculated is:
Have full spectrum: [4, 41, 492, 1090, 1482, 1523, 1682]
Do not have full spectrum: [66, 73, 118, 167, 467, 474, 481, 501, 667, 670, 677, 704, 873, 883, 907, 1076, 1083, 1098, 1110, 1279, 1286, 1313, 1480, 1483, 1485, 1486, 1489, 1516, 1526, 1685, 1692, 1719]

[Vlad Tsyrklevich]

An interesting little side question I just thought of is: What's the minimal set of those 7 equations whose conjunction generates that set? What I'm really thinking about is: in the infinite graph, are full spectrum equations generated by the conjunction of an infinite set of equations, or is it possible that the generating set is finite, perhaps even enumerated within our order 4 world?

[Douglas McNeil]

Sorry, but could you spell out the "clearly every one implied by it is also not" argument? Why couldn't there be an equation which isn't full spectrum (e.g. 677) but implies something (say by setting all variables to x, e.g. 614) which is much easier to satisfy because now you only have to worry about the diagonal terms and idempotence will often get you there?

Or was that just a typo for "every one which implies it"?

[Bruno Le Floch]

Interestingly we don't have to go far at all to see that the equations do not have full spectrum: [66, 73, 118, 167, 467, 474, 501, 670, 677, 704, 873, 907, 1076, 1083, 1110, 1279, 1286, 1313, 1480, 1486, 1489, 1516, 1685, 1692, 1719] have no model of size 2, and [481, 667, 883, 1098, 1483, 1485, 1526] have no model of size 3. So the formalization can probably just be: try every magma of these sizes, perhaps with an optimization of only trying one of each isomorphism class, but then one has to formalize the proof that one hits all isomorphism classes.

It might even be easy to deal with most or all order-5 equations, or at least have a pretty good conjecture if most failures of full spectrum continue to happen at such low domain sizes.

[Bruno Le Floch]

Here are my results for orders up to 5.

• 38984 equations have constant models or linear models $ax+by$ with $a,b\in\{-1,0,1\}$, hence have a full spectrum.
• 23478 equations have no magmas of size 2.
• 74 equations have magmas of size 2 but none of size 3.
• 40 equations are not determined by these techniques: [1482, 1523, 1682, 1885, 2125, 2132, 17187, 17190, 17191, 17194, 17198, 17206, 18054, 18055, 18057, 18061, 18064, 18067, 18074, 18075, 18078, 18082, 18083, 27701, 27702, 27738, 27739, 27775, 27852, 27853, 27889, 27890, 27926, 28157, 28615, 28616, 28766, 28767, 28804, 29035]. Well the first six are of order 4 so we already understood them, they all have full spectrum. Keeping only the order 5 equations and removing duals we go down to 17 equations to study, all of them of the form x=(y ◇ x) ◇ (x ◇ cubic).

Equations for which the full spectrum property remains unknown

Equation 17187: x = (y ◇ x) ◇ (x ◇ (y ◇ (x ◇ y)))
Equation 17190: x = (y ◇ x) ◇ (x ◇ (y ◇ (y ◇ y)))
Equation 17191: x = (y ◇ x) ◇ (x ◇ (y ◇ (y ◇ z)))
Equation 17194: x = (y ◇ x) ◇ (x ◇ (y ◇ (z ◇ z)))
Equation 17198: x = (y ◇ x) ◇ (x ◇ (z ◇ (x ◇ z)))
Equation 17206: x = (y ◇ x) ◇ (x ◇ (z ◇ (z ◇ z)))
Equation 18054: x = (y ◇ x) ◇ (x ◇ ((x ◇ x) ◇ y))
Equation 18055: x = (y ◇ x) ◇ (x ◇ ((x ◇ x) ◇ z))
Equation 18057: x = (y ◇ x) ◇ (x ◇ ((x ◇ y) ◇ y))
Equation 18061: x = (y ◇ x) ◇ (x ◇ ((x ◇ z) ◇ z))
Equation 18064: x = (y ◇ x) ◇ (x ◇ ((y ◇ x) ◇ y))
Equation 18067: x = (y ◇ x) ◇ (x ◇ ((y ◇ y) ◇ y))
Equation 18074: x = (y ◇ x) ◇ (x ◇ ((z ◇ x) ◇ y))
Equation 18075: x = (y ◇ x) ◇ (x ◇ ((z ◇ x) ◇ z))
Equation 18078: x = (y ◇ x) ◇ (x ◇ ((z ◇ y) ◇ y))
Equation 18082: x = (y ◇ x) ◇ (x ◇ ((z ◇ z) ◇ y))
Equation 18083: x = (y ◇ x) ◇ (x ◇ ((z ◇ z) ◇ z))

Python script: fullspectrum5.py
Lists of equations of the various kinds mentioned above: fullspectrum5-out.txt

[Bruno Le Floch]

For the 950941 equations of orders up to 6 my code is too slow to search for order 3 magmas, but I found that

• 596121 equations (62.7%) have full spectrum (by constant or simple linear models)
• 338758 equations (35.6%) have no magmas of size 2
• 16062 equations (1.7%) are not determined yet.

[Vlad Tsyrklevich]

Douglas McNeil said:

Or was that just a typo for "every one which implies it"?

Yes, indeed.

[Vlad Tsyrklevich]

Bruno Le Floch said:

Interestingly we don't have to go far at all to see that the equations do not have full spectrum

Yes I've already got proofs for the equations that have no models of order 2 by brute force enumeration. Perhaps due to my ignorance of how to optimize proofs, those proofs are actually still pretty slow, so enumerating $3^{3^2}\approx20k$ cases seems out of the question, so I'm writing some custom code to figure out how to rule out the order 3 equations with minimal case splits per-equation at the moment.

[Vlad Tsyrklevich]

To answer my own question above, of the 13 order 4 equations (not modulo duality) that generate full spectrum equations, they are all generated by just the conjunction of equations 4 and 5, but this is because 4+5 just imply everything. My original thought was that equations implied by the conjunction of full spectrum equations must also be full spectrum, but that is not true.

[Vlad Tsyrklevich]

(deleted)

[Bruno Le Floch]

Unsurprisingly your list of 13 parallels the list of models we used in our human proof of the full spectrum: equation 4 is x*y=x and it implies all equations with the first variable on the lhs and rhs being the same, equation 41 is the constant law, equation 492 corresponds (only?) to the x*y=-x-y model, equation 1090 to backwards subtraction (the dual 2552 is equivalent to Tarski's 543), and then we have the equations 1482, 1523, 1682 (and duals) that we had to deal with by hand.

[Vlad Tsyrklevich]

I've finished proving the negative cases, the PR is here if anyone cares to look. Most of the files ends up being the large'ish (but fairly fast) proofs for equations that have models of cardinality 2 but not 3.

I think it'd be interesting to try to write a completeness proof since it should be easier than the overall completeness proof: we are only proving something for 4694 equations instead of a theoretical max of $~4694^2$ implications. For now I'm not going to pursue that.

[Bruno Le Floch]

All 34 order 5 equations (dual pairs) that remain unknown have (many) models of sizes 2,3,5,7 so I conjecture they all have full spectrum. Since some of them are consequences of others, it would be enough to show that the 11 equations [17191, 17194, 17198, 17206, 18055, 18061, 18074, 18075, 18078, 18082, 18083] have full spectrum to conclude.

[Bruno Le Floch]

Most magmas of size 2 are such that direct powers of them have submagmas of all cardinalities. For instance if $0*x=0$ in the size-2 magma $M$ then the subset of $0$ and basis vectors in $M^k$ forms a magma of size $1+k$. The only size-2 magmas that are exceptions to that are $(\mathbb{Z}/2\mathbb{Z},+)$ and booleans equipped with NAND.

This means that either an equation has no model of size 2 (then it is not full spectrum), or it has one of the most common models of that size (then it is full spectrum), or its only models of size 2 are addition modulo 2 or NAND. Out of the 114 equations of order up to 5 that are not outright dealt with by this observation, 62 have addition mod 2, and 52 have NAND. The first of equations only exists for equations of even order (by a parity argument). The second set of equations has a nice form, all of the equations (or their duals) have the form $x = (y*x)*(x*\text{expr})$ where expr is quadratic or cubic in the variables.

EDIT: The same phenomenon can happen at size 3. Consider equation 1482 (respectively 1523). Its only size-2 model is NAND (respectively addition mod 2), whose powers do not have interesting submagmas, but the magmas of arbitrary order given by Douglas McNeil, 0*0=1 (respectively 0*0=0), 0*x=x*0=x for x!=0, and other x*y=0, are actually submagmas of powers of his size-3 magma.

Something similar happens for equation 18055 where powers of the size-3 magma with multiplication table [[0,0,1],[0,2,1],[1,1,1]] contain submagmas of all odd sizes, consisting of the elements (x,0,0,0,...), (x,x,0,0,...), (x,x,x,0,...) etc of the product. Then the direct products of these odd-size magmas with powers of the NAND magma of size 2 show that 18055 (and its consequence 18054) have full spectrum. The same technique fails for 1682, for which we needed a complicated magma construction, and for the 15 remaining unknowns at order 5, [17187, 17190, 17191, 17194, 17198, 17206, 18057, 18061, 18064, 18067, 18074, 18075, 18078, 18082, 18083] (and of course duals thereof).

[Bruno Le Floch]

By the way, this suggests that a better notion than directly irreducible is as follows: a magma M is simple if every magma morphism M→N is injective or maps all of M to the same element of N. Equivalently, any equivalence relation on M that respects the magma operation is either nothing-equal or everything-equal. Simplicity is more efficient to check algorithmically than direct irreducibility: for any pair {x,y} of elements of M, complete the equivalence relation x~y into one that respects the magma operation, and check if it identifies all elements. This can be posed as a graph theory problem on the set of pairs in M, with edges given by {x,y}→{z,w} if there exists v with x*v=z and y*v=w, etc.

With this definition, direct products cannot contain new simple submagmas in the following sense. If M is a simple A-magma contained in a direct product N₁×N₂, then the induced magma morphism M→N₁ is (by simplicity) either injective or has a singleton image. If injective, then M is already a submagma of N₁ without taking the direct product with N₂. If singleton then M is contained in a singleton times N₂, hence injects in N₂ already without taking a direct product with N₁.

If a magma is not simple, then there exists a non-trivial non-injective morphism M→N, whose image is automatically a magma satisfying the same laws as M (and more laws), so that M can be seen as a magma extension of this image. This is why the word simple seems apt.

[Bruno Le Floch]

On the integer interval $\{-k,-k+1,\dots,k-1,k\}$ consider the operation defined by

$$x \diamond y = \begin{cases} -y & \text{if } y>0 , \\ -x & \text{if } x,y\leq 0 , \\ 0 & \text{if } y\leq 0 \leq x . \end{cases}$$

It obeys a bunch of properties, for instance $x=(y\diamond x)\diamond(x\diamond z)$ unless $x<0<z$, and one can check it obeys equations [17187, 17190, 17198, 17206, 18054, 18055, 18057, 18061, 18064, 18067, 18074, 18075, 18078, 18083]. This gives models of all odd sizes for these equations. Since they also have a model of size 2 they are full spectrum.

At order 5, we are thus left with three equations (and their duals) for which we don't know whether they have full spectrum. All three have a unique model of size 3,

• Equation 17191 x = (y * x) * (x * (y * (y * z))), model [ [0,0,1],[2,0,2],[2,0,2] ].
• Equation 17194 x = (y * x) * (x * (y * (z * z))), model $\mathbb{Z}/3\mathbb{Z}$ with $x\diamond y=y-x$.
• Equation 18082 x = (y * x) * (x * ((z * z) * y)), model $\mathbb{Z}/3\mathbb{Z}$ with $x\diamond y=x-y$.

Equation 17194 and equation 28157 (dual of 18082) have models of all odd sizes (checked up to 13) with additionally x*x=0 and 0*x=x. Note that this does not reduce the equation to x=(y*x)*(x*y) because 0 is not a right-identity. I wasn't able to identify the structure of these models to generalize to all odd sizes.

[Bruno Le Floch]

Equation 17191 has full spectrum. Models of sizes 2 and 5 are easy to find. Any other size belongs to some interval $[k(k+1)/2,k^2]$, for some $k\geq 1$, and here is a family of models that have all theses sizes.

Let $E\subset[0,k-1]^2$ be a collection of edges such that there does not exist $x,y$ with $(x,y),(y,x)\in E$, namely there are no self-loops $(x,x)$ nor cycle of length 2. Then define a magma operation on $M = [0,k-1]^2\setminus E$ by $(x,y)\diamond(z,w)=(y,z)$ whenever this is possible, and otherwise $(y,y)$ or $(z,z)$ as needed to make certain properties hold.
Specifically, let

$$(x,y) \diamond (z,w) = \begin{cases} (y,y) & \text{if } (y,z)\in E , z=w , \\ (z,z) & \text{if } (y,z)\in E , z\neq w , \\ (y,z) & \text{if } (y,z)\not\in E . \end{cases}$$

In particular $(x,y)\diamond(y,z)=(y,y)$. In the case $E=\emptyset$ this is just a normal central groupoid. More generally, we can evaluate

$$(x,y) \diamond \bigl( (x,y) \diamond (z,w) \bigr) = \begin{cases} (x,y) \diamond (y,y) = (y,y) & \text{if } (y,z)\in E , z=w , \\ (x,y) \diamond (z,z) = (y,y) & \text{if } (y,z)\in E , z\neq w , \\ (x,y) \diamond (y,z) = (y,y) & \text{if } (y,z)\not\in E . \end{cases}$$

The middle case is interesting because the condition $(y,z)\in E$ that caused $z$ to stick around after the first operation is responsible for eliminating it now. Altogether we have $(x,y)\diamond((x,y)\diamond(z,w))=(y,y)$, which simplifies equation 17191 to $(x,y) = ((z,w)\diamond(x,y)) \diamond ((x,y)\diamond(w,w))$. We compute, for $(x,y),(z,w)\in M$,

$$((z,w)\diamond(x,y)) \diamond ((x,y)\diamond(w,w)) = \Bigl( (w,x) \text{ or } (x,x) \text{ or } (w,w) \Bigr) \diamond \Bigl( (y,w) \text{ or } (y,y) \Bigr) .$$

When the first operand is one of the first two cases $(\dots,x)$, this correctly results in $(x,y)$ since $(x,y)\not\in E$. The only danger is the last case $(w,w)$, which occurs only if $(w,x)\in E$ and $x=y$. In that case, $(x,w)\not\in E$ (by the assumption on cycles) so the second operand is $(x,w)$. Then we compute $(w,w)\diamond(x,w)=(x,x)$ because $(w,x)\in E$ and $x\neq w$.

[Bruno Le Floch]

Equations 17194 x=(y*x)*(x*(y*(z*z))) and 28157 x=((y*(z*z))*x)*(x*y) (dual to 18082) have full spectrum too. We have the size-2 model NAND so only odd sizes are needed. On the integer interval $\{-k,\dots,k\}$, define the operation

$$x\diamond y = \begin{cases} -|x-y| & \text{if } x,y<0 , \\ |x-y| & \text{if } x,y>0 , \\ y & \text{if } x=0 , \\ -x & \text{if } 0\leq y<-x \text{ or } -x<y\leq 0 , \\ -y & \text{if } 0<-x\leq y \text{ or } y\leq -x<0 . \end{cases}$$

For all $x$ one has $x\diamond x=0$ and $x=0\diamond x=(-x)\diamond 0=x\diamond(-x)$ and sign flip is an automorphism, namely $(-x)*(-y)=-(x*y)$. Equations 17194 x=(y*x)*(x*(y*(z*z))) and 28157 x=((y*(z*z))*x)*(x*y) both reduce to x=((-y)*x)*(x*y) up to flipping the sign of y. Because sign flip is an automorphism, we only need to check the equation for $x\leq 0$:

$$((-y)\diamond x)\diamond (x\diamond y) = \begin{cases} y\diamond y = 0 & \text{if } x=0 , \\ x\diamond(-x) = x & \text{if } y=0 , \\ y\diamond (y-x) = - |x| & \text{if } y<x<0 , \\ (-x)\diamond (x-y) = x & \text{if } x\leq y<0 , \\ (x+y)\diamond (-x) = x & \text{if } 0<y<-x , \\ (-x-y)\diamond (-y) = - |x| & \text{if } 0<-x\leq y . \end{cases}$$

I will not pursue order 6 equations, because there are too many equations that remain unknown (having models of size 2 and 3 but no linear models of all sizes). Those whose size-2 model is addition modulo 2 seem quite diverse, in contrast to order 5 where only the NAND model was possible (due to parity of the number of operands) and all the unknown equations were restrictions of the central groupoid law.

[Bruno Le Floch]

This completely resolves the question of which equations of order up to 5 have full spectrum. It is exactly those which have models of sizes 2 and 3. Namely, 39024 equations have full spectrum and 23552 do not.

[Bruno Le Floch]

A crucial simplification in the above story is that all equations of order ≤ 5 are in one of the following cases:

• 38984 have full spectrum thanks to linear models (including constants and projections).
• 23478 have no magma of size 2.
• 74 have a magma of size 2 but none of size 3.
• 36 are obeyed by a size 2 magma (in fact, NAND or addition mod 2), and by a piecewise linear magma on $\mathbb{Z}$ with $x\diamond y$ among $x,y,0,-x,-y$ depending on the signs of $x,y,|x|-|y|$. The intervals $[-k,k]$ are submagmas of all odd sizes.
• 2 are Equation 1682 and its dual, which have a similar piecewise linear model but with special values for $x=\pm 1$ or $y=\pm 1$. (This is not written up.)
• 2 are Equation 17191 and its dual, which have a graph-theory based model.

Except for these equations 1682 and 17191, the search can be automated, so I've done that for the 950941 equations of order up to 6:

• 596121 equations (62.7%) have full spectrum by linear models
• 338758 equations (35.6%) have no magmas of size 2
• 14734 equations (1.5%) have magmas of size 2 but none of size 3
• 1015 equations (0.1%) have full spectrum by a piecewise linear model
• 313 equations (0.03%) are not determined by these techniques:

List of equation ids

[1682, 1885, 17191, 29035, 71936, 72573, 76713, 80887, 85027, 89160, 93273, 97299, 97413, 109196, 109719, 109833, 109860, 109867, 113859, 118140, 121616, 125555, 125716, 125756, 126420, 126427, 129896, 138136, 138176, 138813, 138840, 138847, 142316, 163016, 163539, 163653, 163687, 171296, 171933, 175436, 175959, 176073, 176107, 179576, 180213, 184387, 191996, 200947, 205080, 209193, 213219, 217359, 217507, 221640, 224915, 225116, 225639, 225753, 225780, 225787, 229927, 234033, 234067, 237373, 237386, 237388, 237389, 237390, 237392, 237396, 237496, 238207, 241513, 241516, 241523, 241526, 241532, 241536, 241575, 241663, 242340, 245769, 245776, 245816, 246453, 246487, 249829, 249833, 249846, 249850, 249868, 250627, 253901, 253911, 253938, 253948, 254733, 254760, 258048, 258060, 262188, 262363, 267187, 274595, 274635, 275460, 278735, 279573, 282875, 282922, 283076, 283747, 287015, 287203, 287351, 287880, 291155, 291168, 291993, 292027, 295295, 295308, 295342, 295496, 299448, 299460, 300260, 300261, 307715, 307728, 307762, 307869, 307876, 307916, 311855, 312539, 312727, 316196, 316716, 320172, 320336, 320849, 320960, 320961, 324300, 324429, 324436, 324463, 324476, 325147, 325628, 328452, 328569, 329129, 329935, 332558, 332716, 332756, 333941, 336856, 337369, 337567, 337679, 340835, 340989, 341036, 345012, 345359, 345659, 345689, 349115, 349276, 349303, 349799, 349940, 349987, 353302, 353416, 353456, 353939, 354127, 354608, 354976, 361548, 361564, 361572, 362249, 362407, 365688, 365704, 366500, 367396, 370006, 370687, 373955, 374143, 374780, 374827, 378095, 378296, 378920, 378933, 382235, 382282, 382571, 382959, 386375, 386563, 386576, 387247, 390515, 391353, 394655, 395366, 395379, 403136, 407122, 407900, 412040, 412936, 416079, 416193, 416703, 416780, 417075, 417152, 419569, 419696, 419720, 420243, 420394, 421293, 423796, 423836, 424319, 424473, 424507, 427822, 427850, 428154, 428232, 428499, 428828, 428829, 429278, 430022, 431990, 432076, 432116, 432294, 432968, 433712, 434162, 434804, 436256, 436893, 440396, 444335, 444536, 445059, 445173, 445200, 445207, 449199, 452816, 453480, 457620, 461733, 465759, 469376, 478327, 485936, 490713, 490747, 494216, 494853, 494880, 494887, 498993, 499027, 506636, 507273, 507300, 507307, 528007, 531436, 531476, 531999, 532113, 532147, 540427, 543695, 543856, 543896, 544419, 544567, 548707, 552699, 556980, 560456, 560979, 561093, 561120, 561127, 573513, 573540, 577653, 581679, 585296, 589436, 594213, 598353, 598387]

At least equations 237386, 237388, 237389, 237390 and their duals are consequences of lower-order full-spectrum equations, so they have full-spectrum. We should be down to only 301 unknown equations if I counted right.

[Bruno Le Floch]

Here are the results at order 7, with a total of 852 unknown equations out of 16071046.

order	full spectrum	nonfull spectrum	unknown
0	1=1+0+0	1=1+0+0	0
1	3=3+0+0	2=2+0+0	0
2	27=27+0+0	12=12+0	0
3	229=229+0+0	135=135+0	0
4	2814=2808+4+2	1470=1408+62	0
5	35950=35916+32+2	21932=21920+12	0
6	558125=557137+978+10	329940=315280+14660	300
7	9227082=9223929+3153+0	5892466=5889143+3323	557
8	172221522=172064190+157332+0	109694882=105709286+3985596+0	25086
9	3424959441=3424347706+611735+0	2273518895=2272623385+895510+0	152524

Equations with known full spectrum split into those known thanks to linear models, piecewise models, or ad-hoc models. The number of equations known to have gaps is split between a first gap at sizes 2 or 3. The reason laws of odd orders are comparatively better resolved is that they cannot be obeyed by addition modulo 2, so more have a gap at size 2. EDIT: added order 8. At order 6, the equations 237386, 237388, 237389, 237390, 325628 and their duals are consequences of lower-order full-spectrum equations.

[Alex Meiburg]

I've been away from the project for a bit - but I would like to note that this "has full spectrum" isn't just a cut in the implication graph, it's a cut in the definability graph, which has considerably denser in its arrows. That is, if a magma obeying G can be first-order defined from a magma obeying H, and H has full spectrum, then G does too. (And the contrapositive.) There's formalization regarding this already at https://github.com/teorth/equational_theories/tree/main/equational_theories/Definability

This can considerably cut down the minimal examples/counterexamples. The 4694 equations collapse to (at most - haven't proved it's tight) 138 equivalence classes under this. See #Equational > Tarski's axiom 543 @ 💬

[Alex Meiburg]

^^ that message linked, where I said 138, was just the definability implications I've proved - I've not proved many non-definability relations (but you shouldn't need those for this). I say "term definability", which is actually a bit stronger, but so far haven't any definable equations that aren't also term-definable.

[Bruno Le Floch]

Interesting. Maybe conversely showing that laws have different low-lying spectra could be used to show some non-definability relations? Looking at the magmas in more detail could be interesting to show non-definability: if a law is obeyed by [[0,1],[1,0]] (mod 2 addition) and another by [[1,1],[1,0]] (NAND) then the first cannot first-order define the second because any expression in x,y using addition mod 2 reduces to either addition mod 2 or projection or constant.

Have you used already that if a law is obeyed by a projection then it cannot first-order define any law that is not obeyed by projections? Similar statements hold for constant laws.

[Jose Brox]

Bruno Le Floch ha dicho:

By the way, this suggests that a better notion than directly irreducible is as follows: a magma M is simple if every magma morphism M→N is injective or maps all of M to the same element of N. Equivalently, any equivalence relation on M that respects the magma operation is either nothing-equal or everything-equal.

This is precisely the notion of simplicity in universal algebra. I believe that what @Ibrahim Tencer wanted originally to capture are those equations giving "new information" for each element of their spectra, so that for each $n$ there is a magma of size $n$ which cannot be built from magmas of smaller sizes. In this sense, the direct irreducibility notion seems good, as any finite algebra (of any signature) is isomorphic to a direct product of directly irreducible algebras. The ultimate weapon though would be subdirect irreducibility, which gives also a decomposition theorem for arbitrary algebras: any algebra is isomorphic to a subdirect product of subdirectly irreducible algebras (Birkhoff's theorem). Note that [EDITED] simple implies sudirectly irreducible implies directly irreducible, with reciprocals false in general.

The definition: $A$ is a subdirect product of $\{A_i\}_i$ if $A$ is a subalgebra of $\prod_i A_i$ and $\pi_i(A)=A_i$ for all projections $\pi_i$.

[Alex Meiburg]

Bruno Le Floch said:

Interesting. Maybe conversely showing that laws have different low-lying spectra could be used to show some non-definability relations? Looking at the magmas in more detail could be interesting to show non-definability: if a law is obeyed by [[0,1],[1,0]] (mod 2 addition) and another by [[1,1],[1,0]] (NAND) then the first cannot first-order define the second because any expression in x,y using addition mod 2 reduces to either addition mod 2 or projection or constant.

Have you used already that if a law is obeyed by a projection then it cannot first-order define any law that is not obeyed by projections? Similar statements hold for constant laws.

For sure, in fact looking at some low-level spectra is pretty much the only way I can think of to show non-definability:

If A has a model of size n and B doesn't, then B can't be definable from A. Every automorphism of the A model must be respected by the corresponding B model, so if the only A model of size 5 has a Z2 symmetry, and the only B model has a Z3 symmetry, then B can't be definable.

If B is "structural" for A (definable in a way that lets the A operation be recovered), then B must have at least as many distinct models of size n as A. The automorphism groups must be isomorphic.

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

@Jose Brox said:

In this sense, the direct irreducibility notion seems good, as any finite algebra (of any signature) is isomorphic to a direct product of directly irreducible algebras.

Even in the finite case, subdirect irreducibility has important advantages over direct irreducibiility.

1. Subdirect irreducibility is a stronger condition than direct irreducibility. Many algebras are directly irreducible, often for not very "algebraic" reasons (e.g. having prime cardinality). We usually have a lot fewer subdirectly irreducible algebras, a strong property to work with, and few structures to classify.
2. However, unlike simplicity, subdirect irreducibility still tells us everything there is to know about the equational theory of our structures. This is true in the finite domain just as much as in the infinite domain.

Let me demonstrate what I mean through some Heyting algebra examples. The distributive lattice depicted below is subdirectly reducible as a Heyting algebra, but not directly reducible (since it has 5 elements).

h5-sred.png

Subdirectly irreducible Heyting algebras are in fact easy to characterize: these are the algebras in which $\exists! y. \forall x. x \rightarrow y = \top \text{ or } x = \top$ holds. And knowing all the subdirectly irreducible algebras would allow us to understand the equational theory of Heyting algebras completely. The simple Heyting algebras also admit a straightforward characterization: the two-element Boolean algebra is the only one. As expected, simplicity is a much stronger condition, yet knowing everything about the sole simple algebra tells us next to nothing about what the equational theory of an arbitrary Heyting algebra may look like.

[Bruno Le Floch]

I finished my run of the python script fullspectrum.py at sizes 8 and 9 and updated my table above. To remain fast, the code only seeks piecewise linear models for equations whose simplification has at most 6 variables, so it may miss some equations which "easily" have full spectrum. In total, 178467 equations remain unknown, out of 5996643396 (six billion).

[Bruno Le Floch]

Thanks @Zoltan A. Kocsis (Z.A.K.) for pointing out subdirect irreducibility. As you can see at #Equational > Simple and (sub)directly irreducible spectrum , I've analyzed that for equations up to order 2 only, because it's pretty tough.