Finiteness of simple paramedial quasigroups

A Lean 4 formalization proving that every c-simple paramedial quasigroup is finite. Consequently, every ordinary simple paramedial quasigroup is finite.

The project uses Lean 4.32.0 and Mathlib 4.32.0. It contains no sorry, admit, or custom axioms.

Read the typeset proof (PDF)

Origin of the problem

The question appears in Wikipedia's list of problems in loop theory and quasigroup theory:

Are there infinite simple paramedial quasigroups?

It was proposed by Jaroslav Ježek and Tomáš Kepka at the Loops '03 conference in Prague in 2003. This repository gives a negative answer.

Main results

theorem finite_of_isCSimple_isParamedial
    {Q : Type*} [Quasigroup Q]
    (hpm : IsParamedial Q) (h_simple : IsCSimple Q) : Finite Q

theorem finite_of_simple_isParamedial
    {Q : Type*} [Quasigroup Q] [Nontrivial Q]
    (hpm : IsParamedial Q)
    (h_simple : ∀ c : Con Q, c = ⊥ ∨ c = ⊤) : Finite Q

Both are in Paramedial/Finiteness.lean.

Here a quasigroup is a magma whose left and right translations are bijections. It is paramedial when

(x * y) * (u * v) = (v * y) * (u * x).

A multiplicative congruence is cancellative when its quotient has injective left and right translations. Quotient translations are automatically surjective, so such a quotient is again a quasigroup. A nontrivial quasigroup is c-simple when equality and the universal congruence are its only cancellative congruences. Ordinary simplicity refers to congruences of the multiplication groupoid, matching the convention in the cited papers.

Proof outline

1. The principal isotope of a paramedial quasigroup is proved paramedial and therefore carries an abelian group structure.
2. Its original multiplication is represented as x * y = f x + g y + e, where f and g are additive automorphisms with equal squares.
3. This gives a module over the integral group ring Z[<a,b | a^2=b^2>].
4. Every submodule induces a cancellative congruence. C-simplicity therefore makes the representing module simple.
5. Writing s = a^-1 b, u = a^2, and t = s+s^-1, the group ring is shown to be generated by {1,s,a,sa} over the central subring generated by u, u^-1, and t.
6. That central subring is a finitely generated Z-algebra. A general ring-theoretic lemma then shows every simple module over the group ring is finite.

What was constructed directly in Lean

Mathlib did not contain a quasigroup hierarchy or the specialized Cho--Ježek--Kepka representation needed here. The formalization explicitly constructs and kernel-checks:

• quasigroups, cancellative quotient congruences, and c-simplicity;
• the principal isotope and the full paramedial cancellation calculation;
• its abelian group structure and the two affine automorphisms;
• the presented coefficient group and its integral group-ring action;
• the coefficient-group normal form s^n a^e u^k;
• centrality, the quadratic reduction, and the four-generator module span;
• finite generation of the central subring and the finite-simple-module lemma;
• the final c-simple and ordinary-simple finiteness results.

Mathlib supplies the general algebraic infrastructure and tactics. Tactics are used for routine normalization and additive rearrangement, but they produce proof terms that are independently checked by Lean's kernel. No representation or finiteness result specific to this problem is assumed as an axiom.

Source layout

File	Contents
Quasigroup.lean	Quasigroups, paramediality, cancellative congruences, c-simplicity
Isotope.lean	Principal isotope and its abelian group structure
AffineConstruction.lean	Additive automorphisms and affine representation
Affine.lean	Affine quasigroups and submodule congruences
Coefficients.lean	Presented coefficient group, group ring, and module action
GroupRing.lean	Normal form, central subring, and four-generator module span
CentralFiniteType.lean	Finite generation of the central subring over Z
Basic.lean	General finite-simple-module theorem
Representation.lean	C-simplicity implies simplicity of the coefficient module
Finiteness.lean	Final finiteness theorems

Build

Install elan, then run:

lake exe cache get
lake build

lean-toolchain, lakefile.toml, and the committed lake-manifest.json pin the Lean and dependency revisions. lake exe cache get is an optional, network-dependent optimization; lake build can compile dependencies locally when no compatible cache is available.

Trust and axioms

Lean's kernel checks the complete proof terms. Run the checked-in audit with:

lake env lean AxiomAudit.lean

On the pinned Lean and Mathlib revisions, both final theorems report only the standard Mathlib foundations:

[propext, Classical.choice, Quot.sound]

In particular, there is no sorryAx, custom representation axiom, or assumed finiteness theorem.

References

• Wikipedia, "List of problems in loop theory and quasigroup theory," section "Existence of infinite simple paramedial quasigroups".
• J. Cho, J. Ježek, and T. Kepka, "Paramedial groupoids," Czechoslovak Mathematical Journal 49 (1999), 277-290. doi:10.1023/A:1022448218116
• J. Cho, J. Ježek, and T. Kepka, "Simple paramedial groupoids," Czechoslovak Mathematical Journal 49 (1999), 391-399. doi:10.1023/A:1022464621750

The affine representation follows the principal-isotope construction in the first paper and the simple-module reduction in the second. The formalization then proves the group-ring finiteness argument described above.

License

Copyright 2026 adrunkhuman. Licensed under the Apache License 2.0.