Finite witnesses for infinite groups

A presentation is a small object: some letters, some equations. The group it describes need not be small at all. Even two generators and one relation can hide an infinite family of elements.

For Kourovka problem 17.124, the question is whether a machine can eventually recognize every ordinary finite presentation whose group is metabelian. There is no promise about the input. The machine has to find its own reason to say yes.

The difficulty lives in the word “every.” To be metabelian, a group must satisfy

$[[a,b],[c,d]]=1\qquad\text{for every }a,b,c,d\in G.$

Here $[a,b]=a^{-1}b^{-1}ab$ . Individual elements may fail to commute; their commutators must commute with one another. Equivalently, the derived subgroup $G'$ is abelian, so $G''=1$ .

Checking more and more instances of that identity gives more and more evidence. It never tells us when we have checked enough. The proof needs a mechanism that makes the unchecked cases follow.

One relation, infinitely many consequences

Start with a group simple enough to see through:

$H=\langle a,t\mid t^{-1}at=a^2\rangle.$

Write $a_i=t^{-i}at^i$ for every integer $i$ . Conjugating the one defining relation gives

$a_{i+1}=a_i^2\qquad(i\in\mathbb Z).$

Now choose any two indices $i\le j$ . Iterating the relation gives $a_j=a_i^{2^{j-i}}$ . Both elements are powers of $a_i$ , so they commute. This works however far apart the indices are, including negative ones.

The subgroup $A=\langle a_i:i\in\mathbb Z\rangle$ is therefore abelian. It is normal: conjugation by $t$ shifts the indices, and conjugation by $a=a_0$ preserves it. Killing $A$ leaves a group generated by $t$ , which is also abelian. Thus $H'\subseteq A$ and $H''=1$ .

We have proved infinitely many commuting relations from a single equation. The certificate is a rule that propagates, rather than a longer list of checked cases.

This example also reveals what goes wrong with a naive search. For an abelian group with finitely many generators, finitely many generator-pair commutators suffice. For a metabelian group, the derived subgroup need not come with a finite generating set as a group. Conjugation produces new elements indefinitely. The elementary chain above has an obvious direction in which to reduce; a general presentation does not.

The paper replaces that chain by a lattice, and “take a power of an earlier element” by a finite collection of Laurent relations. Its geometric task is to ensure there is always a way back into a region already understood.

Give the search something it can check

For an ordinary presentation $P=\langle x_1,\ldots,x_n\mid R\rangle$ , write $G_P=F_n/\langle\!\langle R\rangle\!\rangle$ . The double brackets mean normal closure: the relators may be conjugated, inverted, and multiplied. They do not supply an oracle for equality in $G_P$ .

My September 2026 preprint constructs a finite witness for exactly the positive instances:

Every proposed witness can be checked in finite time. If the group is metabelian, some witness succeeds. If it is not, this search keeps going. That is recursive enumerability; the theorem does not promise a decision procedure that also returns a negative answer.

The adjective ordinary matters. A presentation within the metabelian variety already imposes the desired identity as an ambient law. Here we start in a free group, among all groups, and must prove that the given relators force it.

The strategy changes the direction of the problem. Instead of inspecting the input group directly, build a group whose metabelian structure has a finite certificate, then certify a surjection onto the input:

$\underbrace{P_{\mathcal R}}_{\text{certified metabelian cover}}\;\twoheadrightarrow\;\underbrace{G_P}_{\text{input group}}.$

Metabelianity passes to quotients. If a certificate proves that the source is metabelian and that this map really is onto, soundness follows.

Completeness needs much more: every finitely presented metabelian group must be reached by some cover in the family. Otherwise the search could miss a positive instance forever. The paper makes a classical Bieri–Strebel construction effective and proves this cofinality property.

There are three finite pieces to a certificate:

Signed Laurent data describing the cover and the relations available to propagate commutation.
A dyadic margin $2^{-r}$ certifying that those relations cover every direction.
Words and finite relation proofs certifying an epimorphism from the resulting cover to the input group.

The geometry supplies a finite presentation for the source. The last piece connects that structured source to an arbitrary presentation supplied as input.

Relations acquire a direction

Suppose $A$ is an abelian normal subgroup of a group $E$ , with $E/A\cong\mathbb Z^k$ . Choose lifts $t_1,\ldots,t_k$ of a basis of this quotient. Conjugation makes $A$ a module over the Laurent polynomial ring

$\Lambda=\mathbb Z[t_1^{\pm1},\ldots,t_k^{\pm1}].$

In the example above, the index $i$ recorded how many times we conjugated by $t$ . Here an index is a lattice vector $u\in\mathbb Z^k$ . A monomial records that displacement before conjugating. A Laurent polynomial packages finitely many such moves:

$\lambda=\sum_{u\in S_\lambda}c_{\lambda,u}t^u,\qquad S_\lambda\subset\mathbb Z^k.$

The finite set $S_\lambda$ is its support. Coefficients carry the algebra; support vectors carry the geometry. A relation $A(\lambda-1)=0$ says that each element of $A$ can be expressed through the prescribed combination of its translates. Negative Laurent exponents are allowed, so movement in both lattice directions is available.

The construction uses signed relations. A plus relation acts on $A$ ; a minus relation acts on $A^*$ , the module with inverse action. The sign changes the action, not the displayed support. Keeping that convention straight matters when converting module identities back into noncommutative words.

For every nonzero direction $v$ , the cone condition asks for a polynomial whose entire support lies strictly ahead of the hyperplane perpendicular to $v$ :

$\forall v\ne0\;\exists\lambda\;\forall u\in S_\lambda,\quad v\cdot u>0.$

The quantifier order is essential. We need one whole support on the positive side, not merely one favorable point somewhere in the collection.

The test uses ε = ½. Rotate toward 180° after removing a support to find an uncovered direction.

Each folded fan represents directions where one support clears the ½ margin. Height is illustrative; the exact test remains two-dimensional. This is a geometric model, not a group certificate.

The model above uses four singleton supports. On the square $\|v\|_\infty=1$ , at least one coordinate has absolute value one, so some support has dot product one. The uniform margin is therefore one. Removing the west support leaves the direction $(-1,0)$ uncovered: its best remaining dot product is zero.

For a real certificate, supports may contain several vectors. Replace each support’s score by the smallest dot product among its vectors, then take the largest score over the supports. That max–min expression is the margin function.

The gap between a picture and a proof

The condition quantifies over infinitely many real directions. A finite checker cannot sample angles and hope it found the narrowest gap. The paper instead turns a proposed margin into finitely many exact rational feasibility problems.

Normalize directions to the compact set

$\Sigma=\{v\in\mathbb R^k:\|v\|_\infty=1\}.$

It is the union of $2k$ faces of the cube: choose a coordinate $j$ and a sign, fix $v_j=\pm1$ , and keep every other coordinate between $-1$ and $1$ . Strict coverage and compactness give a positive uniform margin. Some dyadic number $\varepsilon=2^{-r}$ lies below it.

To disprove a proposed margin on a face, choose one bad vector from each support and ask whether all of these inequalities can hold together:

$-1\le v_i\le1,\qquad v_j=\pm1,\qquad v\cdot u_\lambda\le\varepsilon\quad\text{for every }\lambda.$

There are finitely many faces and finitely many choices of the vectors $u_\lambda$ . Each system has rational coefficients. Exact Fourier–Motzkin elimination decides its feasibility by eliminating variables and combining lower and upper bounds. No floating-point tolerance is needed.

If every candidate failure system is infeasible, the proposed margin is certified. The existential search over $r$ belongs to certificate search; checking a supplied $r$ is a bounded, primitive-recursive calculation. This separates the non-effective-looking compactness argument from the actual checker.

The step that makes infinity finite

Imagine that every commutator indexed by a lattice point inside a ball has already been proved trivial. Take the first point just outside. A Laurent relation will replace the element there by a product of translates. This helps only if every term in that product lands inside the ball.

For a numerical picture, take $v=(8,5)$ and a support with two displacements, $u_1=(-1,0)$ and $u_2=(-1,1)$ . Then

$\|v\|^2=89,\qquad\|v+u_1\|^2=74,\qquad\|v+u_2\|^2=85.$

Both terms move inward. A support with one inward term and one outward term would leave part of the proof unresolved. This is why the earlier cone condition asks for an entire support on the correct side of a hyperplane.

The example is only an illustration of the estimate. To make it work uniformly, for every distant point and every required commutator, the paper extracts a positive margin from the cone condition and chooses an explicit starting radius.

The constants in the paper are deliberately explicit. With $\varepsilon=2^{-r}$ , set

$D=1+\sum_{\lambda}\sum_{u\in S_\lambda}\|u\|_1,\qquad C=\frac{2^{-r}}k,$

$R=1+2k\bigl(1+D+D^2k2^r\bigr),\qquad \delta=\min\left(\frac C4,\frac1{4k}\right).$

The radius is conservative. Its job is to make the proof and the finite construction effective, rather than to promise a small presentation.

The key estimate is a familiar expansion:

$\|v+u\|^2=\|v\|^2+2v\cdot u+\|u\|^2.$

Choose support vectors pointing sufficiently against $v$ . Their negative dot products beat the quadratic error from their bounded lengths. If $\rho\ge R$ and $\rho\le\|v\|<\rho+\delta$ , the signed relation lets us replace the current conjugate by translates satisfying $\|v+u\|<\rho$ . Those translates are already inside the region where commutation has been proved.

The size of the displacement $u$ stays bounded. As $v$ moves farther out, the inward term $2v\cdot u$ grows in magnitude while $\|u\|^2$ does not. Eventually inward motion wins uniformly. The chosen radius makes “eventually” a concrete integer.

This is an induction over shells. At the start, finitely many commutation relations are imposed. Each shell reduces to the preceding one, and every lattice vector eventually lies in some shell. No finite sample is being mistaken for a universal statement: the reduction proves the missing cases.

The presentation uses generators $t_i$ and a finite set of module letters, including designated letters $a_{ij}$ . Its four families of relations encode:

$[t_i,t_j]=a_{ij}$ , so the quotient by the module letters is abelian.
$[a,b^{q(v)}]=1$ for lattice vectors inside the finite ball.
The plus Laurent relations, written as ordered products of conjugates.
The minus Laurent relations, using literal inverse words for their action.

Here $q(v)=t_1^{v_1}\cdots t_k^{v_k}$ . Its inverse is the reversed word $t_k^{-v_k}\cdots t_1^{-v_1}$ ; it is not generally the same word as $q(-v)$ . Treating the lifts as if they already commute would assume part of what the construction must prove. This is where the Bieri–Strebel collection argument earns its place: it justifies rearranging the words using only commutation already available inside the smaller region.

After propagation, the normal closure of the module letters is abelian. The quotient by that closure is also abelian. Consequently the derived subgroup lies in an abelian subgroup: the cover is metabelian.

Why the search reaches every yes

A family of certified examples is not yet an enumeration theorem. It could consist entirely of easy cases. The remaining structural argument shows that every finitely presented metabelian group is a quotient of a group in this family.

Begin with an arbitrary finitely presented metabelian group $G$ . Put $A=G'$ and $Q=G/A$ . Choose a surjection $\mathbb Z^k\twoheadrightarrow Q$ and form the pullback

$E=G\times_Q\mathbb Z^k.$

The construction fits into two useful exact sequences:

$1\longrightarrow A\longrightarrow E\longrightarrow\mathbb Z^k\longrightarrow1,$

$1\longrightarrow\ker(\mathbb Z^k\to Q)\longrightarrow E\longrightarrow G\longrightarrow1.$

The second kernel is central and free abelian of finite rank. In this setting, $E$ is again finitely presented and metabelian. The first sequence gives precisely the free abelian quotient needed for the Laurent-module construction.

The classical Bieri–Strebel necessity result supplies suitable finite signed Laurent relations. The effective cover construction then produces a map $P_{\mathcal R}\twoheadrightarrow E$ , and composition gives the required surjection onto $G$ .

This is the completeness bridge. It connects an arbitrary positive input to the highly structured certificate family, even though the search was not initially given $A$ , $Q$ , the pullback, or the correct Laurent data.

No word-problem oracle

There is one remaining obstacle. How do we check a homomorphism between finitely presented groups without a general solution to their word problems?

Let the source be $H=\langle y_1,\ldots,y_m\mid S\rangle$ and the target be $G=\langle x_1,\ldots,x_n\mid R\rangle$ . Supply an image word $u_i(x)$ for each source generator. For every source relator, supply a finite proof that substituting these images makes it trivial in the target.

To certify surjectivity, also supply a source word $v_j(y)$ for every target generator, together with a proof that $v_j(u)x_j^{-1}$ is trivial. Every generator of the target is then in the image.

A proof of triviality is an explicit finite product of conjugates of defining relators or their inverses:

$w=\prod_{\ell=1}^{N}h_\ell^{-1}r_{j_\ell}^{\sigma_\ell}h_\ell,\qquad\sigma_\ell\in\{-1,1\}.$

The checker verifies indices, performs substitutions, and freely reduces finite words. It does not need to discover these proofs; they arrive inside the certificate. This is the recurring move: turn an unbounded search problem into a finite witness-verification problem.

What the checker actually promises

The arXiv v1 ancillary files contain the Lean development. These are actual declarations from Kourovka/Paper.lean, with the surrounding comments omitted:

abbrev certificateCheck : ℕ → ℕ → Bool :=
  EpimorphismEnumeration.check

theorem certificateCheck_primrec : Primrec₂ certificateCheck :=
  EpimorphismEnumeration.check_primrec

theorem metabelian_iff_certificate (p : ℕ) :
    DefinesMetabelian p ↔ ∃ c : ℕ, certificateCheck p c = true :=
  EpimorphismEnumeration.check_correct p

theorem metabelian_presentations_re : REPred DefinesMetabelian :=
  EpimorphismEnumeration.kourovka_17_124_via_epimorphisms

The natural numbers encode presentations and certificates. DefinesMetabelian carries the input semantics; it is not a Boolean oracle for metabelianity. The first theorem establishes the complexity class of verification. The second states soundness and completeness together. The last packages the enumeration conclusion.

At the structured-data level, the checker combines a well-formedness guard with the zero-generator case, or with a cone certificate and an epimorphism certificate. Making malformed encodings and degenerate presentations explicit is part of turning the mathematical argument into a total function.

Read the complete pinned excerpt, download the arXiv v1 source, or explore the repository. The ancillary README pins Lean 4.24 and documents ./scripts/check.sh, including its transitive axiom audit. These excerpts were checked against the submitted source for this article; this website build does not rerun the Lean development.

A search that cannot neglect a witness

For a fixed presentation, enumerate possible certificates and run the finite checker on each. For an enumeration of all positive presentations, visit presentation–certificate pairs diagonally:

$(0,0);\quad(0,1),(1,0);\quad(0,2),(1,1),(2,0);\quad\ldots$

Every pair occurs after finitely many visits. Whenever the checker accepts, output that presentation. Repetitions are harmless: the theorem enumerates presentations, not unique isomorphism classes of groups.

No witness found yet does not mean the property is false.

Each ring holds pairs with the same diagonal index. The moving thread visits all 64 displayed pairs; three toy witnesses leave bright beads. This illustrates enumeration, not execution of the Lean checker.

A presentation with no witness found yet stays unresolved. Giving it more time may find a certificate, but elapsed time alone cannot justify a negative conclusion. The formal result guarantees eventual success on positive inputs; it supplies no useful universal waiting time for this search.

What is inherited, what becomes effective

The construction sits at the intersection of established structural group theory and effective witness checking. These sources explain the division of work:

Bieri–Strebel, 1980. Valuations and finitely presented metabelian groups supplies the geometric structure and finite-presentation machinery used by the cover argument. The present paper makes the required finite choices and checks explicit.
Baumslag–Cannonito–Robinson, 1994. The algorithmic theory of finitely generated metabelian groups develops algorithms with metabelian input conventions. The preprint explains why that setting does not directly settle recognition from an ordinary finite presentation.
Groves–Manning–Wilton, 2012. Recognizing geometric 3-manifold groups using the word problem, Lemma 11.4, already gives recursive enumerability for the abelian-by-cyclic case. The current target is the full class of finitely presented metabelian groups.
Shpilrain, 2010. Search and witness problems in group theory places the gap between deciding a property and finding a positive witness in a broader algorithmic context.
Bartholdi–Pernak–Rauzy. Groups with presentations in EDT0L, also available as arXiv:2402.01601, discusses the recognition question among related presentation problems.

The geometric construction is classical. The contribution claimed here is to turn its choices into a certificate family with a primitive-recursive verifier, connect that family to ordinary finite presentations, and formalize the enumeration argument in Lean. This remains a research preprint.

The useful change in viewpoint is small enough to keep in mind: we do not explore an infinite group until we feel convinced. We find a finite reason that the unexplored part must behave the same way.

The full definitions, radius estimates, collection argument, and theorem dependencies are in Finite presentations of metabelian groups: effective enumeration via Laurent relations. The problem itself appears in the Kourovka Notebook. This essay follows v1, submitted 9 September 2026.