Add code to brute force all 4x4 tables, and a minimal covering set

[carlini]

This branch makes partial progress towards refuting anything that can be done with a 4x4 magma. There are 4^(4*4) = 2^32 of them, and each needs to be checked on all 4696 equations. This C code can brute force this in a few hundred CPU hours. It could be made much more efficient if needed (likely at least 10-100x) by keeping everything in memory and not using the disk so much. Also, it is not thread safe and has race conditions. But I've run it several times and got the same output each time so I'm confident in these results being complete.

[euprunin]

Nice work!

I'm trying to parse the refutations.txt file. Is this the correct interpretation?

Table [[3, 1, 0, 0], [2, 1, 0, 0], [0, 3, 1, 1], [1, 0, 1, 3]]
Proves [1, 8, 411, 430, 436, 1020, 1832, 3253, 3306, 3319, 3862, 3915]

This corresponds to the rendered table:

	0	1	2	3
0	3	1	0	0
1	2	1	0	0
2	0	3	1	1
3	1	0	1	3

… with, for example, 0 ∘ 0 = 3, 0 ∘ 1 = 1, 1 ∘ 0 = 2, etc.?

I understand that the numbers in the "Proves" line correspond to the equations below, but could you clarify how to parse the line: Proves [1, 8, 411, 430, 436, 1020, 1832, 3253, 3306, 3319, 3862, 3915]?

equation 1 := x = x
equation 8 := x = x ∘ (x ∘ x)
equation 411 := x = x ∘ (x ∘ (x ∘ (x ∘ x)))
equation 430 := x = x ∘ (y ∘ (x ∘ (y ∘ y)))
equation 436 := x = x ∘ (y ∘ (y ∘ (x ∘ x)))
equation 1020 := x = x ∘ ((x ∘ (x ∘ x)) ∘ x)
equation 1832 := x = (x ∘ (x ∘ x)) ∘ (x ∘ x)
equation 3253 := x ∘ x = x ∘ (x ∘ (x ∘ x))
equation 3306 := x ∘ y = x ∘ (x ∘ (x ∘ y))
equation 3319 := x ∘ y = x ∘ (y ∘ (y ∘ y))
equation 3862 := x ∘ x = (x ∘ (x ∘ x)) ∘ x
equation 3915 := x ∘ y = (x ∘ (x ∘ x)) ∘ y

[carlini]

Err, I think I might have messed something up in converting these tables to something human readable.

IN THEORY, each of these equations should be true under this table, if you let the \circ operator be a lookup into the table.

For example, let's consider the first equation x = x ∘ (x ∘ x).

If x = 0, then we're evaluation 0 ∘ (0 ∘ 0) = 0 ∘ 3 = 0
If x = 1, then we're evaluation 1 ∘ (1 ∘ 1) = 1 ∘ 1 = 1
If x = 2, then we're evaluation 2 ∘ (2 ∘ 2) = 2 ∘ 1 = 3 ?????
If x = 3, then we're evaluation 3 ∘ (3 ∘ 3) = 3 ∘ 3 = 3

I'll look into this to see what I did wrong in a bit.

[euprunin]

Yeah, it was exactly that equation (number 8) that made me a bit confused when checking against the table:

0 = 0 ∘ (0 ∘ 0) = 0 ∘ (3) = 0
1 = 1 ∘ (1 ∘ 1) = 1 ∘ (1) = 1
2 ≠ 2 ∘ (2 ∘ 2) = 2 ∘ (1) = 3
3 = 3 ∘ (3 ∘ 3) = 3 ∘ (3) = 3

Setting aside this potential calculation error (which I'm sure can be resolved), the table is meant as a proof of existence that the set of equations on the Proves line can be simultaneously true?

So, the hypothetical case …

Table [[…, …, …, …], […, …, …, …], […, …, …, …], […, …, …, …]]
Proves [A, B, C]

… proves that A, B, and C can be true simultaneously by presenting a table in which A, B, and C hold true? Is that the correct interpretation?

[carlini]

Okay thanks for catching this. 39 of the tables here are incorrect because of an integer overflow in my parallelized version of the algorithm. Pushing a correction now. Should have the corrected results in an hour or so.

[carlini]

The correct interpretation is that, if you use this table, then every equation that is "proven" is true on this magma, and and every equation not mentioned is false for at least one input on this magma.

Here's a few corrected rows if you want to look at some data

Table [[2, 2, 3, 1], [1, 2, 3, 1], [3, 2, 3, 1], [0, 2, 3, 1]]
[1, 47, 359, 614, 817, 1426, 3862, 3918, 3955, 4065, 4121, 4158, 4291, 4606]

Table [[0, 0, 2, 3], [2, 2, 0, 3], [2, 2, 0, 3], [0, 0, 2, 3]]
[1, 3253, 3261, 3271, 3278, 3306, 3319, 3334, 3346, 3353, 3388, 3414, 4065, 4118, 4131, 4275, 4307, 4320, 4362]

Table [[2, 1, 0, 0], [0, 1, 2, 3], [3, 2, 3, 2], [0, 1, 2, 1]]
[1, 203, 3050, 3115, 3253, 3306, 3659, 3684, 3712]

Table [[2, 2, 3, 3], [0, 0, 1, 0], [2, 2, 3, 3], [0, 0, 1, 1]]
[1, 151, 2035, 2036, 2087, 2088, 2089, 3862, 3864, 4268, 4282]

Table [[3, 3, 2, 1], [3, 3, 2, 0], [3, 3, 0, 0], [1, 2, 2, 1]]
[1, 1629, 1634, 1644, 1654, 1664]

Table [[3, 0, 2, 3], [0, 3, 2, 2], [3, 0, 0, 2], [0, 2, 0, 3]]
[1, 3456, 3549, 3555, 3659, 3722, 3862, 3955, 4636, 4658]

[carlini]

I've also pushed a script that will validate every generated refutation, which fails currently but should pass once the generations wrap up.

[carlini]

Okay this new code fully checks out.

[teorth]

Would it be possible to add an entry to README.md describing your contribution (under the "automatically generated progress" list), and maybe also add a chapter to the blueprint (similar to e.g., https://teorth.github.io/equational_theories/blueprint/sect0005.html )? Alternatively, I can try to create a stub for that chapter once I see a summary of your results on README.md.

[carlini]

Yeah. I was going to hold off on this until someone had a chance to make Lean proofs using these tables, but I can add it now.

[carlini]

Ah I've royally messed something up in git and added way too many files in a rush to get this done before I sleep. Do not merge this PR; I'll rebase and remove the files I added incorrectly tomorrow morning.

[euprunin]

Here's a few corrected rows if you want to look at some data

Table [[2, 2, 3, 1], [1, 2, 3, 1], [3, 2, 3, 1], [0, 2, 3, 1]]
[1, 47, 359, 614, 817, 1426, 3862, 3918, 3955, 4065, 4121, 4158, 4291, 4606]

Am I parsing the table correctly in the context of equation 47 (x = x ∘ (x ∘ (x ∘ x)))?

Table: [[2, 2, 3, 1], [1, 2, 3, 1], [3, 2, 3, 1], [0, 2, 3, 1]]

	0	1	2	3
0	2	2	3	1
1	1	2	3	1
2	3	2	3	1
3	0	2	3	1

0 ∘ 0 = 2     0 ∘ 1 = 2     0 ∘ 2 = 3     0 ∘ 3 = 1
1 ∘ 0 = 1     1 ∘ 1 = 2     1 ∘ 2 = 3     1 ∘ 3 = 1
2 ∘ 0 = 3     2 ∘ 1 = 2     2 ∘ 2 = 3     2 ∘ 3 = 1
3 ∘ 0 = 0     3 ∘ 1 = 2     3 ∘ 2 = 3     3 ∘ 3 = 1

Testing equation x = x ∘ (x ∘ (x ∘ x)) with x = 0:

  x = x ∘ (x ∘ (x ∘ x))
  0 = 0 ∘ (0 ∘ (0 ∘ 0))
  0 = 0 ∘ (0 ∘ 2)
  0 = 0 ∘ 3
  0 = 1

[nomeata]

#19 is soon to be merged. I implemented pruning based on known implications and covering by earlier examples there.

Once your raw data is merged, I plan to use a single script to process both of your data sets (exhaustive search and random polynoials) and produce the lean files from those in one go, as they differ only in how the op is implemented. This should allow for even more pruning.