Finite Magma Explorer - better late than never

Stream: Equational

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

Hey everybody!

Responding to issue 332, and people's complaints that it's hard to add stuff to All4x4Tables, I made a new tool for exploring finite magmas.

The Finite Magma Explorer is currently hosted here. If you have ideas on how to add it to the project website (or opinions on whether to add it at all), please comment under the Github issue.

Features:

1. You can enter an operation table for a finite magma in a variety of human- and machine-readable formats.
2. It lists all the equations the given magma satisfies, and gives counterexamples to all the equations that it doesn't. You can filter the equations by their number or by their structure.
3. Double-clicking an equation takes you to corresponding page in the Equation Explorer.
4. If you find a previously unknown implication, it gives you instructions on how to add your magma to All4x4Tables. Ironically, I expect that this feature will never be used...
5. It should be blazing fast on anything up to 16x16, if it's not, that's a bug and you should report it.

feature-1.png
feature-2.png
feature-3.png

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

I've been too busy to contribute for the last couple of days, but I'm planning an update to All4x4Tables later today, both to make it easier to modify, and because there might be a couple of tables that I need to add myself. Thanks to everyone who pinged me (and those who didn't and want me to do something in All4x4Tables can still ping me of course).

[David Renshaw]

[[2, 1, 2, 2, 4, 2, 6, 4],
 [3, 5, 9, 3, 5, 5, 5, 3],
 [0, 6, 6, 3, 4, 5, 6, 7],
 [4, 1, 2, 2, 4, 2, 6, 4],
 [0, 8, 2, 3, 8, 5, 8, 5],
 [10, 1, 2, 9, 4, 9, 6, 4],
 [0, 8, 2, 3, 5, 5, 5, 5],
 [10, 8, 2, 9, 8, 2, 8, 8]]
Error

I have encountered an error while parsing your input. Invalid entry: 9.

[David Renshaw]

^ this table is the transpose of Refutation726 https://github.com/teorth/equational_theories/blob/11ab32cf92d0ce5c1516fef6f5e63251c8cd5b66/equational_theories/Generated/All4x4Tables/Refutation726.lean

[David Renshaw]

and it resolves some still-open implications

[David Renshaw]

I'd like to add it "the right way" if possible

[David Renshaw]

Ironically, I expect that this feature will never be used.

I want to use it!

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

@David Renshaw , I'm a bit confused. Isn't FEM in the right here? You seem to have a multiplication table for an 8-element magma, but the table has 11 different types of entries: [0,1,2,3,4,5,6,7,8,9,10].

[Joachim Breitner]

(deleted)

[David Renshaw]

oops, my mistake

[David Renshaw]

[[2, 1, 2, 2, 4, 2, 6, 4, 8, 2, 2],
 [3, 5, 9, 3, 5, 5, 5, 3, 9, 9, 9],
 [0, 6, 6, 3, 4, 5, 6, 7, 6, 9, 9],
 [4, 1, 2, 2, 4, 2, 6, 4, 8, 2, 2],
 [0, 8, 2, 3, 8, 5, 8, 5, 8, 9, 10],
 [10, 1, 2, 9, 4, 9, 6, 4, 8, 9, 10],
 [0, 8, 2, 3, 5, 5, 5, 5, 8, 9, 10],
 [10, 8, 2, 9, 8, 2, 8, 8, 8, 9, 10]]

[David Renshaw]

let me try the tool again...

[David Renshaw]

ugh, other dimension too..

[David Renshaw]

[[2, 1, 2, 2, 4, 2, 6, 4, 8, 2, 2],
 [3, 5, 9, 3, 5, 5, 5, 3, 9, 9, 9],
 [0, 6, 6, 3, 4, 5, 6, 7, 6, 9, 9],
 [4, 1, 2, 2, 4, 2, 6, 4, 8, 2, 2],
 [0, 8, 2, 3, 8, 5, 8, 5, 8, 9, 10],
 [10, 1, 2, 9, 4, 9, 6, 4, 8, 9, 10],
 [0, 8, 2, 3, 5, 5, 5, 5, 8, 9, 10],
 [10, 8, 2, 9, 8, 2, 8, 8, 8, 9, 10],
 [0, 6, 9, 3, 4, 5, 6, 7, 9, 9, 9],
 [7, 1, 2, 7, 4, 5, 6, 7, 8, 4, 2],
 [7, 6, 6, 7, 4, 5, 6, 7, 6, 4, 6]]

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

This is exciting!

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

Which implications should it refute?

[David Renshaw]

1647, 2240, 2459, 3068

[David Renshaw]

your tool says "All implications refuted by this magma are already known" but I think the ones list here ^ are not currently known

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

Which implications are these 1647 -> 2240 and 2459 -> 3068? Or am I reading it wrong?

[David Renshaw]

Facts G [2712] [1647, 2240, 2459, 3068]

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

Hmm, let me see unknowns.json

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

(this might be a bug)

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

Okay, they are in unknowns.
Gimme a sec, will track down this bug.

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

It's getting it right that 2712 is satisfied and 1647 isn't, it's just not displaying the "Export" message for some reason.
Not that surprising: it's not well-tested, since I had few examples to work with :D

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

Okay, think I found it. Will fix in a minute.

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

Bug fixed (it was a type error in the JavaScript worker).
Please try again @David Renshaw .
If it still doesn't work, that'll be a caching issue, try again in incognito/private-browsing mode.

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

Actually, no, don't try again yet :)

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

Okay, should be fixed.

[David Renshaw]

Then add the following to extra.txt in `All4x4Tables/data`:

[David Renshaw]

I don't see an existing extra.txt file. Should I create a new one?

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

Indeed, you should create it!

[David Renshaw]

equational#430

[David Renshaw]

another one from a known dual:

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

[Terence Tao]

A feature request: an option to generate a linear magma x ◇ y = ax + by on a ring R. There is an easy option to implement and a more challenging option. In the easy option, R is a cyclic group Z/qZ, and a, b can be specified as integers (so one needs to input q, a, b). Most likely q will be prime, but this does not need to be the case.

A more challenging option (in that the input is harder to parse) is to take R to be of the form F_p[t] / (f(t)) for some prime p and some polynomial f(t) of some degree k with coefficients in F_p, thus this is the ring of polynomials with coefficients in a finite field F_p of prime order modulo a fixed polynomial f. (If f is irreducible, this creates a finite field of order p^k, which is the main use case for this input format.) The inputs would then be a prime p and three polynomials f, a, b. E.g., p=5, f = t^2+2, a = t+2, b=2t+3 would give a linear model in F_25. The ring R can be indexed by the p^k polynomials of degree up to k-1, ordered lexicographically. This is perhaps a bit complex to implement, and so one could just implement the easy option for now.

Ideally, these options would come with a stable URL that one could link to directly to describe a linear model (rather than a URL that describes the entire multiplication table, which could get quite sizeable).

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

Thanks @Terence Tao, great ideas. My first priority is to integrate FME into the main project repo. Once that's done, I'll almost certainly crank out linear magmas over Z/nZ; I might add options for working in certain fixed finite fields as well, but the more challenging option in full generality will probably have to wait (unless somebody else volunteers to do it, of course ;) ).

[Pietro Monticone]

I have integrated the FME tool developed by @Zoltan A. Kocsis (Z.A.K.) with the "Compile Blueprint" workflow generating directly the output on our project website.

It will be online in 20 mins if everything goes well.

Screenshot 2024-10-09 at 17.58.21.png
Screenshot 2024-10-09 at 18.39.51.png

[Pietro Monticone]

The relevant PR is equational#468

[Pietro Monticone]

Merged