math.GR — Group Theory

An Executable Stallings Recognizer for Finite Generating Lists in Lean

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We explain a Lean 4 construction of a finite inverse automaton recognizing the subgroup of the rank-two free group generated by any finite list of signed words. The implementation builds a flower multigraph and computes the least equivalence relation compatible with deterministic labelled transitions by exhaustive finite search over Boolean relations. Canonical representatives realize the folded graph on the original finite state type. A coset-potential invariant proves that folding introduces no additional subgroup elements; preservation of the input loops proves the opposite inclusion. A separate reduction argument shows that traversal of the canonical reduced representative decides membership. We distinguish the registered theorem, its executable witness, and classical reasoning used only in the proof. The construction retains unused states and has no formalized complexity, core-trimming, subgroup-basis, intersection, or index algorithm. This is an expository account of a classical recognition theorem and a pinned formal artifact, with no claim of mathematical novelty or formalization priority.