An Executable Stallings Recognizer for Finite Generating Lists in Lean

The recognition theorem and its scope

A finite labelled graph can encode an infinite subgroup of a free group. The based loops supply group elements, while deterministic transitions make the reduced-word membership question a finite traversal. This is the recognition aspect of Stallings’ finite-graph method [4]. Kapovich and Myasnikov give a later combinatorial and computational treatment [1]. The present article explains a deliberately limited formal implementation of that recognition result. It does not formalize the full range of applications of subgroup graphs developed in those works.

All implementation claims below refer to the repository stallings-folding at commit 117dde0a8415d3da1787e15ad22a6223a744432d [3]. This is the commit recorded by PALOMAR-2026-09-23-000004, version 1 [2]. The public record selects Stallings.folded_recognizer_exists and the closed statement definition Stallings.completeStatement. The construction and intermediate correctness results are in the implementation modules; the final interface is in Solution.lean.

Words and the generated subgroup

Write $A=\{a,a^{-1},b,b^{-1}\}$ and let $x\mapsto\bar{x}$ exchange a letter with its inverse. A word is a finite list of letters. Its evaluation in $F_{2}=F(a,b)$ is denoted by $[w]$. If $w=x_{1}\cdots x_{k}$, its inverse word is $\bar{x}_{k}\cdots\bar{x}_{1}$. In Lean these data are Fin 2 × Bool, lists of these pairs, and FreeGroup (Fin 2); the Boolean value true denotes the positive orientation. The definitions letterInv, wordInv, and wordEval implement inversion and evaluation.

For a finite list $S=(s_{0},\ldots,s_{m-1})$ of words, set

Copyright 2026 the authors. Licensed under Creative Commons Attribution 4.0 International (CC BY 4.0).

The source defines generatorSubgroup S using Subgroup.closure of the range of evaluation on Fin S.length. There is no requirement that the input words be reduced, nonempty, distinct, or a free basis. The empty list and lists containing empty words are allowed.

Theorem 1.1 (Registered finite-recognizer statement). For every finite list $S$ of signed words, there exist a finite type $V$, a basepoint $o \in V$, and a partial transition map $\delta: V \times\mathcal{A} \to V \cup\{\bot\}$ such that

and, for every $g \in F_{2}$,

Here $\operatorname{red}(g)$ is the canonical reduced word for $g$ and traversal fails if a required transition is absent.

In the registered definition, $V$ has a Fintype instance, $\delta$ returns Option V, and traversal is written directly with List.foldl and Option.bind. The canonical word is FreeGroup.toWord g. A successful return is some base; none represents failure. Thus the statement uses Mathlib’s free group and list operations without importing the candidate’s automaton semantics. It specifies recognition existentially; the implementation supplies the witness through foldWords S.

Inverse automata and canonical-word traversal

The subgroup represented by an automaton

The structure InverseAutomaton V consists of a basepoint, a partial transition map, and the inverse-edge law (2). Determinism is built into the type of the transition map: an input pair $(v,x)$ has at most one target. The structure itself does not require $V$ to be finite; this allows its semantic lemmas to be used independently of the later finite construction.

The function InverseAutomaton.run recurses over a word, propagating failure through Option.bind. The inductive predicate InverseAutomaton.Walk records the corresponding path. The theorem run_eq_some_iff_walk equates successful execution with a walk having the stated endpoint. Walks concatenate, and reversing a walk while inverting its labels gives a walk in the reverse direction.

For an inverse automaton $G$ with basepoint $o$, define

Empty walks, concatenation, and reversal prove that $L(G)$ is a subgroup. This is the carrier of InverseAutomaton.loopSubgroup; no additional subgroup closure is needed in this definition.

Why reduction is part of the specification

A partial automaton need not read every word representing an accepted group element. If a required edge is missing, inserting an inverse pair can turn a successful traversal into a failure. The usable direction is that deleting an inverse pair from a successful traversal preserves its endpoint.

Lemma 2.1 (Successful traversal survives reduction). If $\operatorname{run}_{G}(v,w)=z$ and $w'$ is obtained from $w$ by free reduction, then $\operatorname{run}_{G}(v,w')=z$.

Proof. For one cancellation write $w=px\bar{x}q$. Successful traversal of $p$ ends at some vertex $u$, and the next letter $x$ takes $u$ to a vertex $t$. The inverse-edge law forces the following $\bar{x}$ transition to return to $u$. Removing these two steps leaves traversal of $q$ unchanged. Induction over a sequence of cancellations proves the claim. $\square$

The source develops this argument in run_success_cancel, run_success_of_red_step, run_success_of_red, and run_success_of_reduction. The concatenation identity run_append isolates the cancelled pair inside the traversal.

Proposition 2.2 (Canonical-word recognition). For every inverse automaton $G$ and $g \in F_{2}$, traversal of $\operatorname{red}(g)$ returns to the basepoint if and only if $g \in L(G)$.

Proof. A successful canonical-word traversal is itself a based loop, and its word evaluates to $g$. Conversely, choose a based-loop word $w$ evaluating to $g$. Lemma 2.1 preserves its successful endpoint while reducing $w$. Mathlib’s reduced-word soundness identifies this reduction with the canonical reduced representative of $g$. The result follows. □

This is InverseAutomaton.accepts_iff_mem_loopSubgroup. The Boolean function InverseAutomaton.membershipTest, available when vertices have decidable equality, tests whether the canonical traversal returns some base. Its correctness theorem is InverseAutomaton.membershipTest_eq_true_iff. The proof uses Mathlib’s FreeGroup.mk_toWord and FreeGroup.reduce.sound [5]. It does not assert equality of traversal outcomes for all freely equivalent, unreduced words.

A finite least-congruence folding construction

The input multigraph and admissible relations

Before folding, the labelled graph can have several targets for a fixed source and label. The structure InverseMultigraph V represents these targets by finite sets $E(v,x)$. Its inverse law is

Throughout the folding module, $V$ has finite enumeration, decidable equality, and a linear order. The order is used to choose representatives.

Definition 3.1 (Fold congruence). A relation $R$ on $V$ is a fold congruence if it is an equivalence relation and satisfies

The condition includes $v=w$, so all targets of the same label from one vertex must be identified. It also enforces consistency after source vertices have been identified. The source predicate IsFoldCongruence uses a Boolean table $r : V \to V \to\mathrm{Bool}$ and expresses reflexivity, symmetry, transitivity, and (4) with finite quantifiers. Its explicit decidability instance follows from the finite types involved.

Define the relation $R_{*}$ by

This is foldRel. The universal Boolean relation is a fold congruence, so the family is nonempty. The lemmas foldRel.refl, foldRel.symm, foldRel.trans, and foldRel.edge_congr prove that its intersection is itself a fold congruence. By its definition, $R_{*}$ is contained in every fold congruence. These facts justify describing it as the least deterministic fold congruence.

Representatives and partial transitions

Let $\operatorname{rep}(v)$ be the least vertex in the $R_{*}$ class of $v$. Reflexivity ensures that this class is nonempty. The function foldRep takes the minimum of a filtered Finset.univ. Its main properties are

They are proved by foldRep_rel, foldRep_eq_of_rel, and foldRep_idem.

For a class and a label, collect the original targets

This finite set is foldTargets G v x. Any two of its elements are $R_{*}$ equivalent, by (4); this is foldTargets_pair. Hence every target in $T(v,x)$ has the same representative. The transition chooses the least target and then its representative, or fails if the target set is empty.

The actual state type remains $V$. The function foldedNext permits outgoing transitions only when $v=\operatorname{rep}(v)$; other vertices have no outgoing transitions. The basepoint becomes $\operatorname{rep}(o)$, and every successful target is canonical. Thus traversals from the basepoint stay in the canonical part of $V$, although the returned type still includes noncanonical vertices. The definition foldAutomaton proves the inverse law for these transitions using the original inverse edges and equality of target representatives.

Executability and termination

The computation uses decidable predicates on finite types, finite filtering, and finite minima. In particular, deciding (5) enumerates the finite type of Boolean relations and checks the fold congruence conditions. This is exhaustive reference computation; there is no implemented union-find fold sequence. Traversal is structural recursion on the input word. These definitions do not depend on a search for an unbounded sequence of folds or on an external termination oracle.

The executable functions should be distinguished from a classical predicate used only in their correctness proof. The private definition cosetBool in Folding.lean is noncomputable: it converts membership in a generally undecidable subgroup coset relation into a Boolean relation under classical reasoning. It supplies a candidate relation to the proof of (5); the folding code never computes cosetBool or queries subgroup membership. No complexity bound or performance benchmark is proved or reported here.

The coset invariant and preservation of subgroup labels

Identifying vertices can create new combinatorial walks, so preservation of old paths alone proves only one inclusion of subgroups. The reverse inclusion uses a potential valued in the free group. This avoids an assertion that every folded walk lifts to a walk with the same word in the unfolded graph.

The orientation of the coset relation

For a subgroup $H\leq F_{2}$, write

Equivalently $Hg=Hh$. Formula (6), rather than terminology about left or right cosets, fixes the convention. The relation is an equivalence relation and is invariant under common multiplication on the right:

Indeed $(gx)(hx)^{-1}=gh^{-1}$. The source names this relation CosetEquivalent and proves the corresponding reflexivity, symmetry, transitivity, and right_mul lemmas.

Definition 4.1 (Compatible potential). A potential $p:V\to F_{2}$ is compatible with a labelled multigraph modulo $H$ if each edge $v\xrightarrow{x}w$ satisfies

This is HasCosetPotential. Induction on walks gives

The same expression holds for successful folded traversal, as shown below.

Lemma 4.2 (A fold respects compatible potentials). If $p$ is compatible modulo $H$, then $v\,R_{*}\,w$ implies $p(v)\sim_{H}p(w)$.

Proof. Consider the relation $v\,R_{p}\,w$ defined by $p(v)\sim_{H}p(w)$. It is an equivalence relation. If $v\,R_{p}\,w$ and there are $x$ edges from $v,w$ to $u,t$, compatibility and (7) give

Thus $R_{p}$ is a fold congruence. Represent it as a Boolean relation using classical decidability. Definition (5) places $R_{*}$ inside this relation, proving the assertion. □

The lemma is foldRel_cosetPotential. Using it to move between a vertex and its representative, foldedNext_cosetPotential proves that each folded transition satisfies (8). Induction on words then gives run_cosetPotential:

Equality of the represented subgroups

For an inverse multigraph $G$, the source defines its based-loop subgroup as the subgroup closure of evaluated labels of walks based at $o$. Denote this subgroup by $H_G$. This differs definitionally from the automaton’s direct loop carrier, although both have the intended group semantics.

Proposition 4.3 (Folding preserves the loop subgroup). Suppose that $G$ has a potential compatible modulo $H_G$ and $p(o)=1$. Then $L(\operatorname{fold}(G))=H_G$.

Proof. Each original edge induces a folded transition between representatives, by foldedNext_of_edge. Induction gives foldWalk, which maps an original walk’s endpoints to their representatives without changing its word. Every original based loop therefore belongs to the folded loop subgroup. Closure proves $H_G\subseteq L(\operatorname{fold}(G))$.

For the opposite inclusion, let a folded loop at $\operatorname{rep}(o)$ have label $w$. Lemma 4.2 and $p(o)=1$ imply $p(\operatorname{rep}(o))\in H_G$. (9) gives

If $g\in H_G$ and $g\sim_{H_G}h$, subgroup closure under products and inverses implies $h\in H_G$. Applying this fact shows $p(\operatorname{rep}(o))[w]\in H_G$. Multiplication by $p(\operatorname{rep}(o))^{-1}$ gives $[w]\in H_G$, as required. $\square$

The proposition is foldAutomaton_loopSubgroup_eq. It is stated with a compatible potential as a hypothesis. The end-to-end construction supplies that potential explicitly for its flower graph; it does not assume that an arbitrary finite inverse multigraph comes equipped with one.

The flower construction and end-to-end correctness

A finite state type with unused positions

Let $m$ be the number of input words and $M$ their maximum length, with $M=0$ when $S$ is empty. The state type is

implemented by FlowerVertex S, whose definition is the option of that finite product. The basepoint is none. Positions $0$ and $|s_i|$ on the $i$th word both map to the basepoint; positions strictly between them use their own state $(i,k)$. Each letter of $s_i$ gives a forward edge between successive positions and an inverse edge in the reverse direction.

The full product in (10) includes positions unused by these loops. In particular the pair states with $k=0$ and $k\ge|s_i|$ have no incident flower edges. The construction keeps these positions for a simple uniform finite type. It is not a core-trimming procedure. The function flowerPos treats the endpoints, flowerEdge specifies the two orientations, and flowerGraph filters the finite vertex set to obtain each target set. A lexicographic order with none first provides the linear order required for representatives.

The prefix potential

The potential at an internal position $(i,k)$ is the evaluated prefix $[s_i[0:k]]$. The basepoint and unused positions receive value $1$. For an internal forward edge, evaluation of a prefix extended by one letter is exactly its earlier value times that letter. For the final edge back to the basepoint, the full-word evaluation lies in $H_S$, so the equality is replaced by coset equivalence modulo $H_S$. Inverse edges inherit the same compatibility from inversion and common right multiplication.

These steps prove flower_hasCosetPotential for flowerPotential. The theorem flowerWalk establishes a based walk spelling each input word. It is proved by induction on the remaining suffix as the position advances, so it covers empty words as well.

Proposition 5.1 (The flower represents the input subgroup). The subgroup closure of the flower’s based-loop labels is $H_S$.

Proof. Every input word labels a based loop, giving the inclusion of its generated subgroup in the flower’s loop subgroup. For the converse, the prefix potential begins and ends at $1$ on a based loop. Compatibility along its walk implies $1 \sim_{H_S} [w]$, or $[w]^{-1} \in H_S$. Taking inverses proves that its label is in $H_S$. Subgroup closure yields the desired inclusion. $\square$

This is flowerGraph_loopSubgroup_eq_generatorSubgroup. Combining it with Proposition 4.3 gives

proved as foldWords_loopSubgroup_eq_generatorSubgroup. Proposition 2.2 then establishes the executable theorem

namely foldedMembershipTest_eq_true_iff.

Finally, Solution.lean witnesses Theorem 1.1 with $V_S$, its finite enumeration, the basepoint of foldWords S, and its transition map. The private lemma foldl_run_eq connects the registered statement’s list fold with the implementation’s recursive traversal. The inverse law and (11) then discharge the two specification clauses.

A small explanatory example

Consider $S=(aa,ab)$, with both letters positive. The active flower vertices are the basepoint $o$ and two intermediate vertices $u,v$. Both generator loops begin with an $a$ edge from $o$, so every fold congruence identifies $u$ with $v$. There is a fold congruence that keeps $o$ distinct from them and leaves each unused position separate; hence no further active vertex identification is forced. Write $q$ for the representative of $u,v$. The basepoint component of the output has transitions

and basepoint $o$. The full returned state type still has the unused positions from (10).

Reading $aa$ or $ab$ returns to $o$, while reading $a$ ends at $q$ and reading $b$ fails. The word $bb^{-1}$ also fails as a raw traversal, even though it evaluates to the identity. Its canonical reduced word is empty and is accepted. This illustrates why (3) specifies canonical-word traversal. The example is a direct mathematical reading of the definitions, rather than a reported Lean evaluation or performance measurement.

The registered artifact and verification boundaries

The statement and proof modules

The Mathlib-only Challenge.lean contains the selected closed specification and a deliberate theorem placeholder. The actual proof is in Solution.lean, which imports the implementation. The project configures separate Challenge and Solution modules for comparison. The placeholder in the challenge is not a proof of the result and is not used by the solution.

The four implementation files separate inverse-automaton semantics, finite folding, arbitrary word flowers, and a supplementary one-vertex rose for subsets of the original basis. The rose module proves a basic special case; it does not implement extraction of a free basis for an arbitrary input subgroup. The main proof follows the arbitrary-word flower path described above.

The pinned script scripts/StatementAudit.lean inspects the compiled statement’s constant dependencies and prints the theorem’s axioms. Its purpose is to ensure that the selected closed mathematical statement does not reach unselected candidate-defined data. The present source audit checked that the Challenge and Solution definitions agree and that the solution supplies the advertised witness. A text scan found the deliberate Challenge placeholder and the proof-only noncomputable cosetBool; no sorry, admit, custom axiom declaration, or unsafe declaration was found in the solution or implementation. Such a scan is a limited source check, not a kernel replay.

Historical mechanical verification

The record pins Lean 4.33.0 and Mathlib commit db584cd6d46c92f209a44c0f1c829460d327499d. It reports verification on September 23, 2026, through the recorded Palomar workflow run [2]. The comparator configuration selects the theorem and closed statement definition, enables NanoDa, and permits propext, Quot.sound, and Classical.choice. The record reports a neutral review outcome with no listed warnings and preservation of the exact source commit. These are historical registry facts; they are not a claim of human peer review.

For this article, the immutable source was checked out, the public registry record was re-read, the definitions and proof dependencies were inspected, and the manuscript was compiled and visually checked. No fresh Lean build, compiled statement audit, comparator run, or NanoDa replay was performed for this manuscript. The historical verification record supports the formal checking claim. The present inspection supports the correspondence between the prose and the pinned source, within that explicit boundary.

Attribution and assistance disclosure

Stallings’ finite-graph method is the mathematical source; the implementation adapts it to an exhaustive least-congruence computation. Mathlib supplies the free-group quotient and reduced-word API. The repository’s provenance states that its implementation was written for the project and does not vendor a prior formalization. This article makes no priority claim about other formalizations and reports no new group-theoretic theorem.

Historical repository metadata identifies Arthur Freitas Ramos as its author and responsible maintainer, and records AI-assisted proof development with GPT-6 Codex. That historical statement is separate from the present manuscript’s preparation. This manuscript was drafted primarily with GPT-6.1 assistance, including source cross-checking and typesetting. The submitting author, Arthur Freitas Ramos, reports understanding some parts of the work; this disclosure does not assert full understanding by him or any level of understanding by the other named manuscript authors. Automated source and mathematical review are not independent human peer review. The Lean source is licensed Apache-2.0; this manuscript and its TeX source are licensed CC BY 4.0.

Conclusion

The artifact gives a finite, executable witness to subgroup recognition for every finite list of words in $F_{2}$. Its correctness separates into three reusable arguments: canonical reduction preserves successful inverse-automaton traversal, least-congruence folding preserves loop labels through a coset potential, and the flower’s prefix potential identifies its loop subgroup with the input-generated subgroup. The final Mathlib-only specification packages exactly these recognition semantics.

The implementation does not trim the graph, compute subgroup bases or rank, compute intersections or index, or certify a complexity bound. Replacing the exhaustive congruence search with an optimized algorithm would require its own implementation and a proof relating its output to the existing correctness interface. The present result supplies that interface without claiming those additional algorithms.

References