Open teorth opened 1 month ago
One can also explore the statistics of the implication graph stratified by k. For instance, the above heuristic predicts that the k=1 laws should have many laws implying them, but few consequences, whereas the k>2 laws should have the opposite. It should in particular be quite rare for a low k law to imply a high k law, though this is not an absolute prediction (e.g. one can artificially introduce more variables via substitutions).
Discussed in https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/visualization.20of.20graph.20closure . Let k denote the number of variables in a law. As discussed above, the k=1 laws should be underdetermined and obeyed by a large number of finite magmas; k=2 laws should be determined and obeyed by a few number of finite magmas; and k>2 laws should be overdetermined and obeyed by mostly just the trivial magma. Now that we have data sets of what laws are obeyed by which finite magmas of order up to 4, plus some selected larger magmas, some data analysis should be able to see whether this heuristic holds up, and whether there are anomalous laws that exhibit a different number of solutions than the heuristic predicts.
When done, report on the outcome of the experiment in a new chapter of the blueprint.