Papers With

← All papers
First page of Finite presentations of metabelian groups: effective enumeration via Laurent relations

Finite presentations of metabelian groups: effective enumeration via Laurent relations

Achyuth Jayadevan

math.GR Sep 9, 2026 · v1 math.LO
formalization algebra logic
Read PDF arXiv abstract Code
TL;DR
The enumeration theorem for finite presentations of metabelian groups and its algebraic ingredients are formalized in Lean 4.
Abstract
For an ordinary finite presentation $P=\langle x_1,\ldots,x_n\mid R\rangle$, put $G(P)=F_n/\langle\langle R\rangle\rangle$. We construct a primitive-recursive predicate $V$ with $G(P)''=1 \Longleftrightarrow \exists c\in\mathbb{N}: V(P,c)=1$. Thus finite presentations of metabelian groups are recursively enumerable, answering Kourovka Problem 17.124. An effective form of the Bieri-Strebel covering construction, using signed Laurent relations and rational separation, gives a family of finitely presented metabelian groups cofinal under epimorphisms. Products of conjugates of defining relators witness these epimorphisms. The construction and enumeration theorem are formalized in Lean 4.
Problem

Kourovka Problem 17.124 and related questions of Shpilrain ask whether ordinary finite presentations of metabelian groups are recursively enumerable, and whether membership can be certified by finite witnesses.

Approach

A primitive-recursive predicate V is constructed so that G(P)”=1 iff there exists a finite witness c with V(P,c)=1. An effective form of the Bieri-Strebel covering construction, using signed Laurent relations and a decidable rational separation (margin) test, yields a cofinal family of finitely presented metabelian groups P_R. Epimorphisms onto arbitrary finitely presented metabelian groups are witnessed by products of conjugates of defining relators. The construction and enumeration theorem are formalized in Lean 4 with assistance from a foundation model via a LangGraph harness.

Results

Finite presentations of metabelian groups are shown to be recursively enumerable, answering Kourovka Problem 17.124, with explicit finite Laurent data and normal-closure derivations serving as certificates.