Finite presentations of metabelian groups: effective enumeration via Laurent relations

For an ordinary finite presentation $P=⟨x_1,\dots ,x_n\mid R⟩$, put $G(P)=F_n\mathrm{/}⟨⟨R⟩⟩$. We construct a primitive-recursive predicate $V$ with $G(P{)}^{\mathrm{\prime }\mathrm{\prime }}=1⟺\mathrm{\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.