quadratula

How much of the implication structure of Schröder's 990 quasigroup laws can already be seen in small quasigroups?

Bruno Le Floch (arXiv:2603.29909, CC BY 4.0) settled every implication between these laws with Prover9 and Mace4. He reports that each non-implication is disproven by some finite quasigroup. This repository takes every quasigroup of order 1 to 6 up to isomorphism, computes which laws each one satisfies, and measures against Le Floch's data how many non-implications, classes and varieties this exhaustive floor accounts for. It also finds the smallest set of quasigroups that does the same work.

Results are in REPORT.md. Verification gates are in CONTROLS.md. Both files are generated by analysis/report.py, and they contain no hand-typed numbers.

Claims and their trust level

Claim	Trust level
Counts of quasigroups and Latin squares of order ≤ 6	exhaustive computation, checked against OEIS and by an orbit-stabiliser identity
Which of the 990 laws each quasigroup of order ≤ 6 satisfies	exhaustive computation; law evaluator checked by six classical OEIS counts and by S3 equivariance on every Latin square of order ≤ 5
Saturation, class separation, varieties realised, marginal value per order	exact computation from the above and Le Floch's data
Size of the minimum cover	ILP solved to optimality by HiGHS, with the LP bound reported
Separation curves, least witness orders and least realising orders beyond order 6	exhaustive search over the models of every still-open variety (src/search.rs), checked against the enumerator through order 5, against OEIS A076017 at orders 7–9, and against Mace4
Least witness orders from Mace4 alone	Mace4 search, every model re-checked by the Rust engine; superseded by the exhaustive search where that completed
Both covers, residual witnesses, nonexistence of witnesses below the least orders	re-checked independently by make independent-checks: own parser and evaluator, Le Floch's raw files, SAT (kissat)
Optimality of the full cover among quasigroups of any order	ILP lower bound over Le Floch's 114 closed sets; assumes his list of closed sets is complete
OEIS matches for model-count sequences	lookup pinned with its date; a lead, not a proof
Implications, equivalence classes and varieties used as ground truth	cited from Le Floch (Prover9/Mace4); not re-proved here

Nothing is certified in Lean yet.

Layout

• src/: Rust (law.rs parser, qg.rs operations and evaluator, enumerate.rs isomorphism classes, search.rs models of given laws, parastrophe.rs S3 action, bin/qg.rs CLI)
• analysis/: Python (lefloch.py ground truth, compute.py all measurements up to order 6, residual.py Mace4, beyond.py exact results past order 6, gates.py, report.py; oeis_fingerprints.py needs network and is run by hand)
• data/beyond/: at each order k = 7..9, every model up to isomorphism of each variety still unrealised at order k−1, with the run log
• data/signatures/model_counts.tsv: model counts by order for every class and variety
• data/lefloch/: Le Floch's ancillary files, unmodified, with provenance
• data/floor/order{n}.tsv.gz: every quasigroup of order n up to isomorphism: order, lexicographically least table (row-major digits), automorphism count, satisfied Schröder law numbers (- if none)
• data/signatures/distinct_signatures.tsv, data/cover/min_cover.tsv: plain-text results
• data/derived/: run logs and results.json
• tests/: Rust gate tests and pytest gates over the full runs

Reproduce

make reproduce

Requires rustup (the toolchain is pinned in rust-toolchain.toml) and uv (Python and packages are pinned in .python-version and uv.lock). make residual also needs mace4 on the PATH and skips cleanly without it.

Run time: about 2 hours on an Apple M3 Pro (11 threads). Almost all of it is the exhaustive order-9 search in make beyond; everything up to order 8 takes a few minutes. Per-run timings are in data/beyond/runs.tsv. To rebuild everything except the order 7-9 search, run make build rust-test runs analysis residual report.

The paper PDF needs TeX: make paper.

License and credit

Apache-2.0, see LICENSE and NOTICE. Parts of the enumeration and signature code are adapted from parsimagma. All ground-truth implication data comes from Le Floch and is used under CC BY 4.0.

AI use: code, analysis and documents were written with Claude (Anthropic) under the author's direction. All numbers come from the scripts in this repository.