CENTRAL_GROUPOID: Resolve all remaining implications of the form 168 => X #266
Comments
|
claim |
|
Progress report. Knuth's A_2 resolves a whole bunch of these negatively, but not quite all of them. The following 13 remain unknown: Next step: I'll read the paper and construct the other nonnatural central magmas; if that fails for some reason, I'll try some hand-guided generation to see if I can produce more counterexamples. |
|
I guess this means that A_2 also creates some additional anti-implications beyond 168=>X then? But perhaps those were already all known. I also find fascinating to read Knuth's use of 1970-level computer technology to assist him in that paper. In some ways the current project is a scaling up of Knuth's work to 2024-level technology. |
|
Yes, it resolves a few non-168 implications as well. The reason there is no PR yet is that I plan to put |
Adds Knuth's central groupoid A2 via both an explicit construction and a direct 9x9 multiplication table. The two presentations are proved isomorphic. Progresses teorth#266, and resolves an additional 190 unknown implications.
Progresses #266 by adding the central groupoid A2 via both an explicit construction and a direct 9x9 multiplication table. The two presentations are proved isomorphic. Gives both a streamlined construction of A2 and a FinOp table presentation, and proves them isomorphic. This settles a bunch of anti-implications of the form 168=>X, and resolves 190 previously unknown anti-implications in total. Construction based on the article [D. E. Knuth, Notes on central groupoids, Journal of Combinatorial Theory, Volume 8, Issue 4, 1970](https://doi.org/10.1016/S0021-9800(70)80032-1)
|
With the latest update, it seems from https://teorth.github.io/equational_theories/implications/?168 that we have now in fact resolved all implications (from what I can tell, all the open implications were in fact true!). |
|
One can of course continue formalizing results about central groupoids, but it seems that this particular issue is in fact now resolved. |
|
Sweet, thanks! |
Only 42 implications of the form Equation 168 => Equation X remain open. Equation 168 is the equation of a central groupoid. The discussion in Section 5 of Knuth's paper https://www.sciencedirect.com/science/article/pii/S0021980070800321?ref=cra_js_challenge&fr=RR-1 appears to resolve many of these, as does his examples of "non-natural central groupoids", such as those in Section 7 of Knuth, which could be added to the current lists of interesting magmas, as discussed in https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Collecting.20interesting.20finite.20magmas.
The text was updated successfully, but these errors were encountered: