发表机构
Manipal Institute of Technology MAHE（马尼帕尔理工大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文构造原始递归谓词判定亚贝尔群有限表示的可解性，实现有效枚举，回答Kourovka问题17.124，并在Lean 4中形式化验证。
AI 中文摘要
对于普通有限表示 $P=\langle x_1,\ldots,x_n\mid R\rangle$，令 $G(P)=F_n/\langle\langle R\rangle\rangle$。我们构造一个原始递归谓词 $V$，使得 $G(P)''=1 \Longleftrightarrow \exists c\in\mathbb{N}: V(P,c)=1$。因此，亚贝尔群的有限表示是可递归枚举的，这回答了Kourovka问题17.124。Bieri-Strebel覆盖构造的一种有效形式，使用带符号的Laurent关系和有理分离，给出了在满同态下共尾的有限表示亚贝尔群族。定义关系的共轭乘积见证了这些满同态。该构造和枚举定理已在Lean 4中形式化。
英文摘要
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.
Comments9 pages, 1 figure. Lean 4 formalization included as ancillary files
