Questions for equation commentaries

Stream: Equational

[Bruno Le Floch]

I'm preparing a pull request on commentaries on the equations (e.g., see first commit), and have a few questions.

• Are there other equations meriting commentary?

• What do we mean by "local consequences" for equation 118 and 511: «surprisingly large (but finite) number of "local" consequences»

• Is equation 713 still a particular outlier in terms of complexity of proof using SAT? «This is one of the laws where greedy completion has been shown (via extensive SAT-solver calculations) to work, but only barely. As such, the proof of anti-implications from these laws is extremely lengthy, to the extent that Lean struggles to verify them. See this discussion.»

• About Terry's massive 522-element magma obeying equation 1518, reduced to size 232, was it used in the Lean formalization?

• We have commentary on equation 345169 (Sheffer stroke). Do we want commentary on all equations in the Tour of selected equations?

• About Dupond/Dupont (1692/63) and Asterix/Obelix (65/1491), earlier commentary only talked about one implication being true in the finite but not infinite case, but according to the equation explorer, the equations are equivalent in the finite case and have no implications in the infinite case. Am I reading this right?

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

We have commentary on equation 345169 (Sheffer stroke). Do we want commentary on all equations in the Tour of selected equations?

I for one think it's worth having as much commentary as possible: it improves the usability of the Equation Explorer as an (admittedly niche) research tool, and as far as I can tell the costs are negligible.

[Vlad Tsyrklevich]

Bruno Le Floch said:

• About Terry's massive 522-element magma obeying equation 1518, reduced to size 232, was it used in the Lean formalization?

Yes, this is equational_theories/Generated/All4x4Tables/Refutation939.lean

[Bruno Le Floch]

Thanks Vlad. Is this file auto-generated from somewhere else in the codebase?

[Vlad Tsyrklevich]

Yes, equational_theories/Generated/All4x4Tables/data/plan.txt and extra.txt, I forget which one does exactly what

[Terence Tao]

Bruno Le Floch said:

• What do we mean by "local consequences" for equation 118 and 511: «surprisingly large (but finite) number of "local" consequences»
  

Thanks for doing this! From what I can reconstruct from the past discussion, when trying to set up a greedy algorithm to build interesting 118 magmas, one was forced to add about ten more rules to the greedy ruleset to maintain consistency. These are "local" consequences of 118, which can be deduced by some finite number of applications of 118 that wouldn't have been picked up by a naive greedy implementation of 118 due to some "cancelling" going on in the applications. (I guess by the Birkhoff completeness theorem, all consequences are local, but some are more local than others; for instance E2 is eventually a local consequence of E1689 but one would have had to perform a massive iteration of the greedy algorithm before one would have discovered that.) Anyway, the wording of the commentary can definitely be changed.

[Terence Tao]

Bruno Le Floch said:

• About Dupond/Dupont (1692/63) and Asterix/Obelix (65/1491), earlier commentary only talked about one implication being true in the finite but not infinite case, but according to the equation explorer, the equations are equivalent in the finite case and have no implications in the infinite case. Am I reading this right?

That looks right to me. I think at the time of the commentary we had not systematically worked out all the finite implications.

[Terence Tao]

Bruno Le Floch said:

• We have commentary on equation 345169 (Sheffer stroke). Do we want commentary on all equations in the Tour of selected equations?

Sure, if this isn't too much trouble on your end. Though currently Equation Explorer doesn't have a way of accessing any equation of order greater than 4, so these commentaries would only be visible through the github repository at present. (But perhaps a future tool, or a tweak to EE as per equational#378, could make use of them.)

[Bruno Le Floch]

I plan to also add commentary when the equation implies any of {idempotence, commutativity, associativity, left or right cancellativity, left or right surjectivity}.

Is there a plan to show the commentary of the canonical equivalent equation? E.g., when I look at the Equation Explorer for equation 6 the fact that it is trivial is hidden at the bottom of the page.

[Terence Tao]

Fair enough; I've opened equational#1218 if anyone has the time (and familiarity with the EE code) to implement this.

[Bruno Le Floch]

Thanks for all the comments! I'm slowly going through things and preparing corresponding commits. In the literature there are single-axiom descriptions of various structures (groups, groups with various exponents, Sheffer stroke, natural central groupoid, inverse loop, commutative Moufang loop of exponent 3, etc.), which often come in large families of dozens of equivalent equations, plus large families of equations that are only known to be equivalent for finite magmas. Currently I'm writing one commentary for the lowest number in these families, but it is not so clear what the best plan is. Any thoughts?

[Terence Tao]

One could make very short commentaries for the other equations in the family (particularly any below 4684) that basically consist of a hyperlink ("See Equation X") to the lowest number Equation Explorer page (if below 4684) or just directly to the relevant .md file in commentary. (Retroactively one could also clean up some of the duplicated existing commentaries this way - there are a couple equations that are linked together and the same commentary is placed for both, but actually the more sustainable approach (with regards to future edits) is to only have the commentary for the lowest-numbered equation and everybody else gets a hyperlink redirect only.)

[Bruno Le Floch]

To avoid duplication I will answer Terry's last comment on the Equation Explorer in the 'extra equations thread.

---

Here is a pull request with commentary updates:

Commentary on many equations:

• Merging commentary of dual equations together; I sometimes left it duplicated when the higher-numbered one was much better known (e.g., Littlewood). This should be revisited depending on what we do in FRONTEND: Get equation explorer to mention canonically equivalent form #1218.
• Corrections to commentary that mentioned unknown implications, now all known.
• Those that imply equation 38 or its dual 39, equivalent to sets equipped with some structure.
• Those that imply associativity, whose free group is describable.
• Those that imply commutativity.
• Those that imply idempotence.
• Higher-order ones that were in the tour of selected equations, and some from the literature characterizing groups with a certain exponent, Moufang loops with exponent 3.

[Fox Room]

While you're here though, you should note that 4380 is "cube-associativity", or "power-3-associativity", of note in algebra that fail to even be flexible.

[Fox Room]

And a few more notes:

• 16 is the "Steiner property", as in, a "Steiner magma" is commutative and 16
• 26 is the "right involutory" property characterizing keis (a type of quandle)
• 28 is an axiom of a certain kind of differential structure... ugh, it's in my notes, but I can't find a source elaborating on this. maybe you can figure out wtf I'm talking about
• 40 is sometimes called "unipotence", although there may be another concept with the same name
• 333 is the "graphic property" satisfied by graphic monoids
• 378 is the other property, along with the graphic property, that must be satisfied by a shelf in order for it to be "proto-unital"
• 4396 and its dual are "alternativity"
• x * (y * (z * x)) = ((x * y) * z) * x is the "extra" property, which I believe is of interest in loop theory
• (x * z) * (y * w) = (x * y) * (z * w) is the "medial" property
• (x * y) * (x * z) = (y * x) * (y * z) is the axiom satisfied by "cycle sets" which are structures encoding set-theoretic solutions to the Yang-Baxter equation
• (x * x) * (y * z) = (x * y) * (x * z) and its dual are "semimedial" properties
• (z * x) * (y * w) = (w * x) * (y * z) is the "paramedial" property

[Notification Bot]

A message was moved here from #Equational > Laws with finite free magmata by Bruno Le Floch.

[Notification Bot]

A message was moved here from #Equational > Laws with finite free magmata by Bruno Le Floch.

[Bruno Le Floch]

In my upcoming PR I'm taking into account most of these suggestions (but moved to the lower-numbered dual).

• I ignored the "Steiner property" as commutative-law-16 is the same as commutative-law-14, which is equivalent to 492.
• About law 9 (law 28) «a certain kind of differential structure» I don't understand much. Linear magmas are x◇y=x+b(y-x) with b squaring to zero, which resembles something differential. In general $L_x$ maps the magma to a subset and that subset to $\{x\}$. It's too vague to include in the commentary.
• About 4396, https://en.wikipedia.org/wiki/Alternativity calls 4396+dual «alternative (flexible)», but a quick mace4 run finds that neither implication from/to the flexible identity 4435 holds. Are you sure of the correct terminology here?
• The "graphic property" of monoids is xy=yxy, but it is not clear whether the magma analogue should be 333 x*y=y*(x*y) or 385 x*y=(y*x)*y. Do you have a reference? Is one of the two more interesting?
• Do you have a ref for the fact that 378 (dual of 323) is «the other property, along with the graphic property, that must be satisfied by a shelf in order for it to be "proto-unital"?
• Do you have a ref for the fact that Law 933170 (x * y) * (x * z) = (y * x) * (y * z) is the «axiom satisfied by "cycle sets" which are structures encoding set-theoretic solutions to the Yang-Baxter equation»?

[Fox Room]

Bruno Le Floch said:

• I ignored the "Steiner property" as commutative-law-16 is the same as commutative-law-14, which is equivalent to 492.

Interesting, TIL!
Bruno Le Floch said:

About law 9 (law 28) «a certain kind of differential structure» I don't understand much. Linear magmas are x◇y=x+b(y-x) with b squaring to zero, which resembles something differential. In general $L_x$ maps the magma to a subset and that subset to $\{x\}$. It's too vague to include in the commentary.

I'm confident I didn't invent this, but I don't remember what the source is. I'll look to see if I can find it again.
Bruno Le Floch said:

About 4396, https://en.wikipedia.org/wiki/Alternativity calls 4396+dual «alternative (flexible)», but a quick mace4 run finds that neither implication from/to the flexible identity 4435 holds. Are you sure of the correct terminology here?

Yes, I've noted before that for some reason wikipedia has "alternative (flexible)" but they are indeed two completely separate laws. FWIW, if something is alternative on either side AND flexible, it's guaranteed alternative, but otherwise I have no idea why wikipedia has that qualifier. In any case, wikipedia has a page on the actual flexible property as well that clarifies the relation, so I'm really not sure what's up with this.
Bruno Le Floch said:

• The "graphic property" of monoids is xy=yxy, but it is not clear whether the magma analogue should be 333 x*y=y*(x*y) or 385 x*y=(y*x)*y. Do you have a reference? Is one of the two more interesting?
• Do you have a ref for the fact that 378 (dual of 323) is «the other property, along with the graphic property, that must be satisfied by a shelf in order for it to be "proto-unital"?

I was going to confidently say yes, but it turns out that the answer is only sort of. They're apparently only ever used in associative contexts, so the grouping is inferred... sorry about that.

As for which is more interesting, well, there's 34 of the former among magmata of order 3 versus 44 of the latter? And then in order 4 there's 4055 of the latter, but 4556 of the former. Huh. I was assuming it'd be unambiguous that one was more common than the other, but I guess not. I have no idea.
Bruno Le Floch said:

Do you have a ref for the fact that Law 933170 (x * y) * (x * z) = (y * x) * (y * z) is the «axiom satisfied by "cycle sets" which are structures encoding set-theoretic solutions to the Yang-Baxter equation»?

Yes.

[Fox Room]

Aha, I found the "differential" structure. It's mentioned in this paper, with a reference to a paper I can't access, and also called "2-reductivity". You can derive a few more properties to comment on using this nomenclature, actually.

[Fox Room]

Here's another paper mentioning the structure.

[Fox Room]

This is also relevant!

[Fox Room]

Fox Room said:

Bruno Le Floch said:

About 4396, https://en.wikipedia.org/wiki/Alternativity calls 4396+dual «alternative (flexible)», but a quick mace4 run finds that neither implication from/to the flexible identity 4435 holds. Are you sure of the correct terminology here?

Yes, I've noted before that for some reason wikipedia has "alternative (flexible)" but they are indeed two completely separate laws. FWIW, if something is alternative on either side AND flexible, it's guaranteed alternative, but otherwise I have no idea why wikipedia has that qualifier. In any case, wikipedia has a page on the actual flexible property as well that clarifies the relation, so I'm really not sure what's up with this.

Wait, this is apparently only true for algebra over a field, and not general magmata. In fact, a magma can be flexible AND alternative on both sides and still not be associative!

[Fox Room]

I totally forgot about this paper which names 3737 the "Ward quasigroup" property

[Fox Room]

Also, 3918 is the equation a central groupoid must satisfy to be a natural cental groupoid

[Fox Room]

Hm, actually it's given as an implication... wikipedia must be wrong

[Bruno Le Floch]

Ward quasigroups are in one-to-one correspondence with groups equipped with division. It's very surprising that 3737 is a much shorter (order 4) characterization than the Higman-Neumann axiom of order 8. The crucial point is that 3737 only works among quasigroups while Higman-Neumann works among all magmas.

Erratum for your comment: wikipedia correctly states that 3915 (or its dual 3522) characterizes natural central groupoids among central groupoids. In fact, it also characterizes it among weak central groupoids too. I'm adding that to an upcoming commentary PR.

[Fox Room]

image.png

This is 3918, not 3915, no? Which would be false, as centrality implies 3918.

[Bruno Le Floch]

No, the equation explorer for law 3915, and my find_equation_id.py script, both show that 3915 is the same as wikipedia, x ◇ y = (x ◇ (x ◇ x)) ◇ y, whereas in 3918 the next-to-last letter is replaced by y, so x ◇ y = (x ◇ (x ◇ y)) ◇ y.

[Fox Room]

oh, you're right. somehow i'd gotten it in my head that this was the other way around

[Pace Nielsen]

Equation #4, xy=x, is called a "left projection" on the equation explorer. Magmas satisfying the equation are also called "left zero semigroups" because every element acts like a zero from the left (while "right zero semigroups" are defined symmetrically).

[Fox Room]

Decided to look at the literature on quasigroups to find some more named equations.
167 is the "bookend" property or the "Stein third identity"
159 is the Schroder identity (ibid.)
The Dupont equation 63 is listed but not named in (ibid.), and is called "T2" here
1587 is the Schroder identity of generalized associativity (ibid.)
3113 defines a pentagonal quasigroup alongside mediality and idempotence
weirdly, (ibid.) calls 14 "hexagonal"
2538 defines a GS-quasigroup (ibid.)
4658 defines an ARO-quasigroup (ibid.)
335 defines a Stein quasigroup (ibid.)
4684 is called the right modular property (ibid.) (and as confirmed here that makes 4369 left modular)
264 defines a C3-quasigroup (ibid.) (and its dual is also called the C3 law)
952 is called the Neumann identity
3810 is called the Schweizer identity (ibid.)
3740 is called transitivity
4399 is called Schroder's first property
4364 is called cyclic associativity
4673 and its dual are permutability (ibid.)
4515 is the commuting product law (ibid.)

[Bruno Le Floch]

Thanks, I've done these changes, together with some others that I had accumulated. See the pull request.

FYI the names quadratical, pentagonal, hexagonal, affine-regular-octagon, golden section, are related to what the linear models of these laws (over complex numbers) look like geometrically.

The reference https://arxiv.org/pdf/1809.07095 that you cite is strange, they present their Theorem 15 as new, but it states that 952 characterizes abelian group subtraction, which was known by Higman and Neumann since 1952. Do you understand what's going on?

[Fox Room]

Hm, you're right. (I hadn't noticed, I was just skimming these papers for definitions.) Perhaps it's just putting some related theorems together that hadn't appeared together elsewhere? It doesn't explicitly say that the results are novel...
Interestingly enough, the only other place I can find where "Schweizer quasigroup" or "Schweizer identity" appears is the thesis of one of the authors, though as I'm not in academia my only tools for searching are arXiv and Google (I am under the impression that anything better requires at the very least a subscription.)

[Bruno Le Floch]

Schweizer and Sklar appear to have written quite a lot of papers together around 1960–1970 on various partial functions, which are cited by some papers talking about Boolean algebras, but it seems difficult to disentangle the literature (and notation) there. It is possible that Didurik and Shcherbacov simply managed to unearth the Schweizer identity from one of these old papers, hence giving it the name.

[Terence Tao]

I think it's great that we can repurpose the ETP to help organize this literature!

[Bruno Le Floch]

Thanks. However, it is only a small slice of the literature, as there are many properties of magmas that cannot be captured by equational laws with universal quantifiers. Even the notion of quasigroup (existence of left and right division) cannot be expressed as one of our laws.

(The other thing is that we are trying to be thorough in finding as many equation names as possible, but not finding all papers about them, so it's quite different from a literature review.)

[Fox Room]

Searched the literature on non-associative algebra, as although, just as I imagined, most identities involve more than one operation or are higher than order 4, there were a few applicable ones. Unfortunately, what I uncovered was more confusing than enlightening, as I've just discovered how inconsistent terminology can be across fields.
4673, which I already noted is (right) permutability, is also one of the conditions defining a Novikov algebra, and in (2 below) is called right commutativity
4684, which again I already noted above to be the right modular property, is confusingly also called left invertive
4525 and 4362 are also mentioned in (ibid.) but are not really named, per se.
4362 also appears here, defining a metAbelian Novikov algebra
4510 is the extra condition imposed other than the Jordan identity (order 6) on a non-commutative algebra in order for it to be a non-commutative Jordan algebra
(ibid.) also calls 4679 cyclic associativity, whereas its dual is called that in my previous report
4541 defines nearly-associative algebra or shift-associative algebra

[Fox Room]

I find searching through these obscure papers for definitions very entertaining, but unfortunately I'm reaching the end of what I can dig up with the limited tools for trawling the literature that I have available. I am currently poring over the search results for "groupoid" in the arXiv and picking out any stragglers that are referring to magmata as opposed to partial groups, and hope to get a couple more references from this, but once I've done that I'm out of ideas. Which is unfortunate, because although I imagine this endeavor cannot actually be of use to anyone, I have been having a lot of fun with it.

[Fox Room]

Correction: apparently a groupoid (category-theoretic) isn't the same thing as a partial group?

[Kevin Buzzard]

Yeah I think mathematicians now use groupoid to mean something else but I think it used to be synonymous with magma

[Bruno Le Floch]

As Kevin says, groupoid (old) = magma. But @Fox Room's question was about modern usage of groupoid: it covers two notions: partial group, and category in which all morphisms have inverses. These two notions are equivalent, see https://en.wikipedia.org/wiki/Groupoid#Comparing_the_definitions

[Bruno Le Floch]

Regarding your other messages, I've noted to add these to a pull request in a week or two. For more literature, you could very usefully look through the volumes of http://www.quasigroups.eu which seem to be freely available.

In particular, as described in a 2015 paper you already mentioned, Belousov's paper singled out seven laws [63, 75, 159, 167, 335, 4399, 4443] (that imply a quasigroup is orthogonal to one of its parastrophes) up to parastrophic equivalence, and I'd be very interested if you manage to decode enough of Belousov's paper to determine a list of all laws that are parastrophically equivalent to these, such as law 73.

I failed so far to locate Sade's seemingly seminal 1957 paper A. Sade: Quasigroupes obéissant à certaines lois, Rev. Fac. Sci. Univ. Istambul. Sér. 22 (1957), 151 − 184. (Alternative names of the journal: İstanbul Üniversitesi Fen Fakültesi mecmuasi. A serisi, Sırfî ve tatbikî matematik = Revue de la Faculté des sciences de l'Université d'Istanbul.)

[Fox Room]

Bruno Le Floch said:

As Kevin says, groupoid (old) = magma. But Fox Room's question was about modern usage of groupoid: it covers two notions: partial group, and category in which all morphisms have inverses. These two notions are equivalent, see https://en.wikipedia.org/wiki/Groupoid#Comparing_the_definitions

While you're correct, I'd like to contest the notion that groupoid for magma is "outdated". It's a claim I see a lot, and it's borne from the fact that most instances of the word groupoid are referring to the category-theoretic notion (completely accurate), but it implies the opposite, that most instances in which magmata come up are not called groupoids, and this seems to be totally false to me. Groupoid is still quite common among instances of referring to the concept of a magma, at least in my estimation.

[Fox Room]

In summary: my experience is that, if you hear someone say 'groupoid', they almost certainly mean a category in which all morphisms are invertible, but if you hear someone talking about sets with a closed binary operation, they are not much less likely to use the word groupoid than magma.

[Fox Room]

Bruno Le Floch said:

For more literature, you could very usefully look through the volumes of http://www.quasigroups.eu which seem to be freely available.

Awesome. I will certainly do so.

Bruno Le Floch said:

I'd be very interested if you manage to decode enough of Belousov's paper to determine a list of all laws that are parastrophically equivalent to these, such as law 73.

I will give it a good look. I was actually thinking a bit about this from that 2015 paper and it's for sure a question I'm interested in.

[Fox Room]

Fox Room said:

I am currently poring over the search results for "groupoid" in the arXiv and picking out any stragglers that are referring to magmata as opposed to partial groups, and hope to get a couple more references from this

156 and 166 are the identities characterizing a Sheffer (magma)
25 is the equational identity that holds in a travel (magma), but also the equation that characterizes De Morgan algebra among "implication zroupoids" (a "zroupoid" is just a pointed magma)
4515 is also called the Hossuzu-Tarski identity
4369 is also called Grassmann's associative law, and (ibid.) calls the above "Tarki's" associative law (I don't know if that's a typo, it's consistently spelled that way throughout the paper)

[Bruno Le Floch]

When writing some of the commentary, I'm confused about which of x◇(x◇x) and (x◇x)◇x should be called left or right cube (then more generally left/right powers are easy). If you come across a reference for that I'm interested.

[Fox Room]

I have not found a source that directly answers this question, but in non-associative algebra the convention seems to be to define powers as bracketing on the right side (that is, x(xx), see e.g. Schafer's Introduction to Non-Associative Algebra). This isn't incredibly satisfying to me, but the problem is that even in the non-associative realm, power-associativity is strongly desired as a nice property, and many, perhaps even most, classes of non-associative structures are power-associative or at least cube-associative. After all, non-associative disciplines often focus on structures with weaker forms of associativity, and cube-associativity is implied by nearly all of these. Note that even commutativity implies the flexible identity, which implies cube-associativity, and even idempotence implies cube-associativity. I'm somewhat doubtful that there is even enough literature to establish any kind of convention, in this light.

However, lacking an authoritative reference, I instead decided to see if there's a pattern among the nomenclature for identities with only one term of the form x(yz) or (xy)z, or two terms both of the same form...
equations supporting x(yz) having left affinity: 8, 16, 47, 75, 308, 316, 323, 327, 411, 513, 562, 3254, 3306
equations supporting x(yz) having right affinity: 10, 13, 62, 336, 463, 508, 3349
equations supporting both affinities: 9, 14, 48, 412, 4362, 4369, 4673

This is not by any means conclusive, and I am not satisfied with the results of my search, but I do think the indirect precedent leans towards calling x * (x * x) the left cube, and mutatis mutandis for right cubes and higher powers, etc., despite the absence of any explicit reference I can find.

[Bruno Le Floch]

Digging some more into one of your references I came across a 1957 paper by Stein which seems relevant (and points to papers by Hosszu) https://www.ams.org/journals/tran/1957-085-01/S0002-9947-1957-0094404-6/

[Bruno Le Floch]

John Halleck had a list of many logic systems, now only available on the wayback machine. It is conceivable that there could be some described by equational laws, but I wasn't able to usefully navigate the wealth of information there.

[Fox Room]

I'll look through that after the quasigroups journal, which I really meant to have done way before now but my mental health has quite deprived me of the requisite motivation over the past week or two unfortunately

[Fox Room]

4658 is called the "Tanaka equation" here

[Bruno Le Floch]

Thanks! I submitted my pull request a minute before seeing your message, and didn't have the energy to go back and modify it. This will have to wait for my next pull request, probably in early September as I'm off for a one-month vacation.

We now have around 750 commentary files at https://github.com/teorth/equational_theories/tree/main/commentary with thorough commentary on

• all Austin implications;
• laws that imply existence of a left or right zero, or left or right unit, or injectivity/surjectivity of left/right multiplications or squaring or cubing maps, or the fact that squares or cubes form a submagma, of are constant, or whether the law is incompatible with being a quasigroup or being idempotent or commutative or associative or a group;
• laws whose free magma (or free magma with one generator) I could determine;
• laws that are parastrophically equivalent to others;
• laws that were singled out by the spectrum study;
• laws with nice descriptions such as fibrations over Cartesian products or Boolean groups or abelian groups;
• laws whose submagma P={x◇y|x,y∈M} obeys interesting laws;
• laws that imply linearity, or whose models are submagmas of linear models.

[Fox Room]

Haha, I was mostly just posting it because I came across it randomly and would probably forget about it if I didn't put it in here, so that doesn't bother me

[Fox Room]

I'd like to ideally have a lot more before then though

[Fox Room]

This paper calls 25 "contraction", 4658 "quasicommutativity", and gives yet another name for 4362: "exchange". They are given as the axioms defining a Boolean implication algebra.

[Fox Room]

This paper, although it is in an associative context, has some identities which are equivalent to a single identity even in a nonassociative context. In particular, 4515 is given the name weak commutativity, 4544 pseudocommutativity, and 4525 quasiweak commutativity.

(It's rather odd to me that a dual law is named as if it were a weaker property, but my journey for these named equations has taught me that the conventions don't always make sense.)

[Fox Room]

I think there is enough commentary that it makes sense to implement a tags system into equation explorer. Several equations have the exact same datum in their commentaries, and if this was reworked into a system of tags then some additional properties (that are too trivial to note in the comments but may be of interest to see in a list) may be included. I am just thinking about easy to derive information such as order, number of variables, number of cancelled variables, height in the lattice of implications, etc...

I mention this because I specifically wished for a "pre-filtered" list of equations with the same variables on either side, and imagined there might be need for other such things.

[Bruno Le Floch]

I agree. Can you open an issue on Github, or perhaps adjoin your comment to a relevant issue on Github about the Equation Explorer? This is more about the code than the comments themselves. In principle I could find my way through that code, but I've already claimed another issue (writing about the full spectrum problem), for which I am overdue due to ongoing vacation.

[Fox Room]

I have done so now

[Fox Room]

image.png

[Fox Room]

reinforcement for the "graphic" terminology and an introduction of "paragraphic" for this related identity, which is introduced by the source

[Fox Room]

https://arxiv.org/pdf/2504.09368

[Bruno Le Floch]

Thanks, I will include this in my next PR with other equation commentary. Do you have any other one incoming shortly that I should wait for?

[Fox Room]

no, I haven't been actively searching recently, I just happened to come across this incidentally when reading about various kinds of diagram algebra. I will have more at _some_ point, as I have a large number of papers to look through, but not shortly.