% Copyright 2026 Arthur Freitas Ramos, David Barros Hulak,
% and Ruy J. G. B. de Queiroz. Licensed CC BY 4.0.
% https://creativecommons.org/licenses/by/4.0/
\documentclass[11pt]{amsart}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage[a4paper,margin=29mm]{geometry}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{microtype}
\usepackage{booktabs}
\usepackage{needspace}
\PassOptionsToPackage{obeyspaces,spaces}{url}
\usepackage{xurl}
\usepackage[hidelinks]{hyperref}
\hypersetup{pdftitle={An Executable Stallings Recognizer for Finite Generating Lists in Lean},
 pdfauthor={Arthur Freitas Ramos; David Barros Hulak; Ruy J. G. B. de Queiroz},
 pdfsubject={Finite inverse automata and subgroup membership in the rank two free group},
 pdfkeywords={Stallings folding, free groups, inverse automata, Lean 4, Mathlib}}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\newcommand{\F}{F_2}
\newcommand{\A}{\mathcal A}
\newcommand{\ev}[1]{\lbrack #1\rbrack}
\newcommand{\rep}{\operatorname{rep}}
\newcommand{\run}{\operatorname{run}}
\newcommand{\decl}[1]{{\small\nolinkurl{#1}}}
\newcommand{\source}[2]{\href{https://github.com/Arthur742Ramos/stallings-folding/blob/117dde0a8415d3da1787e15ad22a6223a744432d/#1}{#2}}
\title[An executable Stallings recognizer in Lean]{An Executable Stallings Recognizer for Finite Generating Lists in Lean}
\author{Arthur Freitas Ramos}
\author{David Barros Hulak}
\author{Ruy J. G. B. de Queiroz}
\thanks{Author ORCID identifiers: Arthur Freitas Ramos,
\href{https://orcid.org/0009-0003-3568-0325}{0009-0003-3568-0325};
David Barros Hulak,
\href{https://orcid.org/0009-0002-8056-1774}{0009-0002-8056-1774};
Ruy J. G. B. de Queiroz,
\href{https://orcid.org/0000-0003-1482-0977}{0000-0003-1482-0977}.}
\thanks{Copyright 2026 the authors. Licensed under
\href{https://creativecommons.org/licenses/by/4.0/}{Creative Commons Attribution 4.0 International (CC BY 4.0)}.}
\date{October 1, 2026}
\subjclass[2020]{20E05, 68Q45, 03B35}
\keywords{Stallings folding, free groups, finite inverse automata, subgroup membership, Lean 4, Mathlib}
\begin{document}
\begin{abstract}
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.
\end{abstract}
\maketitle
\enlargethispage{2pt}
\raggedbottom

\section{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
\cite{Stallings1983}. Kapovich and Myasnikov give a later combinatorial
and computational treatment \cite{KapovichMyasnikov2002}. 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
\emph{stallings-folding} at commit
\nolinkurl{117dde0a8415d3da1787e15ad22a6223a744432d}
\cite{StallingsArtifact}. This is the commit recorded by
\href{https://palomar-registry.org/entry?id=PALOMAR-2026-09-23-000004\&version=1}{PALOMAR-2026-09-23-000004, version 1}
\cite{PalomarRecord}. The public record selects
\decl{Stallings.folded_recognizer_exists} and the closed statement definition
\decl{Stallings.completeStatement}. The construction and intermediate
correctness results are in the implementation modules; the final interface
is in \source{Solution.lean}{\texttt{Solution.lean}}.

\subsection{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=F(a,b)$ is denoted by $\ev{w}$. If $w=x_1\cdots x_k$, its inverse word
is $\bar x_k\cdots\bar x_1$. In Lean these data are
\decl{Fin 2} $\times$ \decl{Bool}, lists of these pairs, and
\decl{FreeGroup (Fin 2)}; the Boolean value \texttt{true} denotes the
positive orientation. The definitions \decl{letterInv}, \decl{wordInv},
and \decl{wordEval} implement inversion and evaluation.

For a finite list $S=(s_0,\ldots,s_{m-1})$ of words, set
\begin{equation}\label{eq:H}
 H_S=\left\langle\ev{s_i}\mid 0\leq i<m\right\rangle\leq\F.
\end{equation}
The source defines \decl{generatorSubgroup S} using \decl{Subgroup.closure}
of the range of evaluation on \decl{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.

\begin{theorem}[Registered finite-recognizer statement]\label{thm:registered}
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\A\to V\cup\{\bot\}$ such that
\begin{equation}\label{eq:inverse}
 \delta(v,x)=w\quad\Longrightarrow\quad\delta(w,\bar x)=v
\end{equation}
and, for every $g\in\F$,
\begin{equation}\label{eq:accept}
 \run_\delta(o,\operatorname{red}(g))=o
 \quad\Longleftrightarrow\quad g\in H_S.
\end{equation}
Here $\operatorname{red}(g)$ is the canonical reduced word for $g$ and
traversal fails if a required transition is absent.
\end{theorem}

In the registered definition, $V$ has a \decl{Fintype} instance,
$\delta$ returns \decl{Option V}, and traversal is written directly with
\decl{List.foldl} and \decl{Option.bind}. The canonical word is
\decl{FreeGroup.toWord g}. A successful return is \decl{some base};
\decl{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 \decl{foldWords S}.

\section{Inverse automata and canonical-word traversal}

\subsection{The subgroup represented by an automaton}
The structure \decl{InverseAutomaton V} consists of a basepoint, a partial
transition map, and the inverse-edge law~\eqref{eq:inverse}. 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 \decl{InverseAutomaton.run} recurses over a word, propagating
failure through \decl{Option.bind}. The inductive predicate
\decl{InverseAutomaton.Walk} records the corresponding path. The theorem
\decl{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
\[
 L(G)=\{\ev{w}\mid w\text{ labels a walk from }o\text{ to }o\}.
\]
Empty walks, concatenation, and reversal prove that $L(G)$ is a subgroup.
This is the carrier of \decl{InverseAutomaton.loopSubgroup}; no additional
subgroup closure is needed in this definition.

\subsection{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
\emph{deleting} an inverse pair from a successful traversal preserves its
endpoint.

\begin{lemma}[Successful traversal survives reduction]\label{lem:reduce}
If $\run_G(v,w)=z$ and $w'$ is obtained from $w$ by free reduction, then
$\run_G(v,w')=z$.
\end{lemma}
\begin{proof}
For one cancellation write $w=p\,x\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.
\end{proof}

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

\begin{proposition}[Canonical-word recognition]\label{prop:canonical}
For every inverse automaton $G$ and $g\in\F$, traversal of
$\operatorname{red}(g)$ returns to the basepoint if and only if $g\in L(G)$.
\end{proposition}
\begin{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~\ref{lem:reduce} 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.
\end{proof}

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

\section{A finite least-congruence folding construction}

\subsection{The input multigraph and admissible relations}
Before folding, the labelled graph can have several targets for a fixed
source and label. The structure \decl{InverseMultigraph V} represents
these targets by finite sets $E(v,x)$. Its inverse law is
\[
 u\in E(v,x)\quad\Longleftrightarrow\quad v\in E(u,\bar x).
\]
Throughout the folding module, $V$ has finite enumeration, decidable
equality, and a linear order. The order is used to choose representatives.

\begin{definition}[Fold congruence]
A relation $R$ on $V$ is a fold congruence if it is an equivalence relation
and satisfies
\begin{equation}\label{eq:congruence}
 v\,R\,w,\quad u\in E(v,x),\quad t\in E(w,x)
 \quad\Longrightarrow\quad u\,R\,t.
\end{equation}
\end{definition}

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 \decl{IsFoldCongruence}
uses a Boolean table $r:V\to V\to\texttt{Bool}$ and expresses reflexivity,
symmetry, transitivity, and~\eqref{eq:congruence} with finite quantifiers.
Its explicit decidability instance follows from the finite types involved.

Define the relation $R_*$ by
\begin{equation}\label{eq:intersection}
 v\,R_*\,w\quad\Longleftrightarrow\quad
 \text{every Boolean fold congruence relates }v\text{ and }w.
\end{equation}
This is \decl{foldRel}. The universal Boolean relation is a fold
congruence, so the family is nonempty. The lemmas \decl{foldRel.refl},
\decl{foldRel.symm}, \decl{foldRel.trans}, and \decl{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.

\subsection{Representatives and partial transitions}
Let $\rep(v)$ be the least vertex in the $R_*$ class of $v$. Reflexivity
ensures that this class is nonempty. The function \decl{foldRep} takes the
minimum of a filtered \decl{Finset.univ}. Its main properties are
\[
 \rep(v)\,R_*\,v,\qquad
 v\,R_*\,w\Longrightarrow\rep(v)=\rep(w),\qquad
 \rep(\rep(v))=\rep(v).
\]
They are proved by \decl{foldRep_rel}, \decl{foldRep_eq_of_rel}, and
\decl{foldRep_idem}.

For a class and a label, collect the original targets
\[
 T(v,x)=\{t\in V\mid\exists u,\ u\,R_*\,v\text{ and }t\in E(u,x)\}.
\]
This finite set is \decl{foldTargets G v x}. Any two of its elements are
$R_*$ equivalent, by~\eqref{eq:congruence}; this is
\decl{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 \decl{foldedNext} permits
outgoing transitions only when $v=\rep(v)$; other vertices have no outgoing
transitions. The basepoint becomes $\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 \decl{foldAutomaton} proves the inverse law for
these transitions using the original inverse edges and equality of target
representatives.

\subsection{Executability and termination}
The computation uses decidable predicates on finite types, finite filtering,
and finite minima. In particular, deciding~\eqref{eq:intersection}
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
\decl{cosetBool} in \source{Stallings/Folding.lean}{\texttt{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~\eqref{eq:intersection};
the folding code never computes \decl{cosetBool} or queries subgroup
membership. No complexity bound or performance benchmark is proved or
reported here.

\section{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.

\subsection{The orientation of the coset relation}
For a subgroup $H\leq\F$, write
\begin{equation}\label{eq:coset}
 g\sim_H h\quad\Longleftrightarrow\quad gh^{-1}\in H.
\end{equation}
Equivalently $Hg=Hh$. Formula~\eqref{eq:coset}, 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:
\begin{equation}\label{eq:right}
 g\sim_H h\quad\Longrightarrow\quad gx\sim_H hx.
\end{equation}
Indeed $(gx)(hx)^{-1}=gh^{-1}$. The source names this relation
\decl{CosetEquivalent} and proves the corresponding reflexivity, symmetry,
transitivity, and \decl{right_mul} lemmas.

\begin{definition}[Compatible potential]
A potential $p:V\to\F$ is compatible with a labelled multigraph modulo $H$
if each edge $v\xrightarrow{x}w$ satisfies
\begin{equation}\label{eq:potential}
 p(w)\sim_H p(v)\ev{x}.
\end{equation}
\end{definition}

This is \decl{HasCosetPotential}. Induction on walks gives
\[
 v\xrightarrow{w}z\quad\Longrightarrow\quad
 p(z)\sim_H p(v)\ev{w}.
\]
The same expression holds for successful folded traversal, as shown below.

\begin{lemma}[A fold respects compatible potentials]\label{lem:coset}
If $p$ is compatible modulo $H$, then
$v\,R_*\,w$ implies $p(v)\sim_H p(w)$.
\end{lemma}
\begin{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~\eqref{eq:right} give
\[
 p(u)\sim_H p(v)\ev{x}\sim_H p(w)\ev{x}\sim_H p(t).
\]
Thus $R_p$ is a fold congruence. Represent it as a Boolean relation using
classical decidability. Definition~\eqref{eq:intersection} places $R_*$
inside this relation, proving the assertion.
\end{proof}

The lemma is \decl{foldRel_cosetPotential}. Using it to move between a
vertex and its representative, \decl{foldedNext_cosetPotential} proves
that each folded transition satisfies~\eqref{eq:potential}. Induction on
words then gives \decl{run_cosetPotential}:
\begin{equation}\label{eq:runpotential}
 \run_{\mathrm{fold}(G)}(v,w)=t
 \quad\Longrightarrow\quad p(t)\sim_H p(v)\ev{w}.
\end{equation}

\subsection{Equality of the represented subgroups}
For an inverse multigraph $G$, the source defines its based-loop subgroup
as the \emph{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.

\begin{proposition}[Folding preserves the loop subgroup]\label{prop:fold}
Suppose that $G$ has a potential compatible modulo $H_G$ and $p(o)=1$.
Then $L(\mathrm{fold}(G))=H_G$.
\end{proposition}
\begin{proof}
Each original edge induces a folded transition between representatives,
by \decl{foldedNext_of_edge}. Induction gives \decl{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(\mathrm{fold}(G))$.

For the opposite inclusion, let a folded loop at $\rep(o)$ have label $w$.
Lemma~\ref{lem:coset} and $p(o)=1$ imply $p(\rep(o))\in H_G$.
Equation~\eqref{eq:runpotential} gives
\[
 p(\rep(o))\sim_{H_G}p(\rep(o))\ev{w}.
\]
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(\rep(o))\ev{w}\in H_G$. Multiplication by $p(\rep(o))^{-1}$ gives
$\ev{w}\in H_G$, as required.
\end{proof}

The proposition is \decl{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.

\section{The flower construction and end-to-end correctness}

\subsection{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
\begin{equation}\label{eq:flowerV}
 V_S=\{o\}\ \sqcup\ \bigl(\{0,\ldots,m-1\}\times\{0,\ldots,M\}\bigr),
\end{equation}
implemented by
\decl{FlowerVertex S}, whose definition is the option of that finite product.
The basepoint is \decl{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~\eqref{eq:flowerV} includes positions unused by these
loops. In particular the pair states with $k=0$ and $k\geq |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
\decl{flowerPos} treats the endpoints, \decl{flowerEdge} specifies the
two orientations, and \decl{flowerGraph} filters the finite vertex set to
obtain each target set. A lexicographic order with \decl{none} first
provides the linear order required for representatives.

\subsection{The prefix potential}
The potential at an internal position $(i,k)$ is the evaluated prefix
$\ev{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 \decl{flower_hasCosetPotential} for
\decl{flowerPotential}. The theorem \decl{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.

\begin{proposition}[The flower represents the input subgroup]\label{prop:flower}
The subgroup closure of the flower's based-loop labels is $H_S$.
\end{proposition}
\begin{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}\ev{w}$, or $\ev{w}^{-1}\in H_S$.
Taking inverses proves that its label is in $H_S$. Subgroup closure yields
the desired inclusion.
\end{proof}

This is \decl{flowerGraph_loopSubgroup_eq_generatorSubgroup}. Combining
it with Proposition~\ref{prop:fold} gives
\begin{equation}\label{eq:foldWords}
 L(\text{\decl{foldWords S}})=H_S,
\end{equation}
proved as \decl{foldWords_loopSubgroup_eq_generatorSubgroup}.
Proposition~\ref{prop:canonical} then establishes the executable theorem
\begin{equation}\label{eq:booltest}
 \text{\decl{foldedMembershipTest S g}}=\texttt{true}
 \quad\Longleftrightarrow\quad g\in H_S,
\end{equation}
namely \decl{foldedMembershipTest_eq_true_iff}.

Finally, \source{Solution.lean}{\texttt{Solution.lean}} witnesses
Theorem~\ref{thm:registered} with $V_S$, its finite enumeration, the
basepoint of \decl{foldWords S}, and its transition map. The private lemma
\decl{foldl_run_eq} connects the registered statement's list fold with the
implementation's recursive traversal. The inverse law and
\eqref{eq:foldWords} then discharge the two specification clauses.

\subsection{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
\[
\begin{array}{c|cccc}
 &a&a^{-1}&b&b^{-1}\\\hline
 o&q&q&\bot&q\\
 q&o&o&o&\bot
\end{array}
\]
and basepoint $o$. The full returned state type still has the unused
positions from~\eqref{eq:flowerV}.

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~\eqref{eq:accept} specifies
canonical-word traversal. The example is a direct mathematical reading of
the definitions, rather than a reported Lean evaluation or performance
measurement.

\section{The registered artifact and verification boundaries}

\subsection{The statement and proof modules}
The Mathlib-only \source{Challenge.lean}{\texttt{Challenge.lean}}
contains the selected closed specification and a deliberate theorem
placeholder. The actual proof is in
\source{Solution.lean}{\texttt{Solution.lean}}, which imports the
implementation. The project configures separate \texttt{Challenge} and
\texttt{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 \decl{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 \decl{cosetBool};
no \texttt{sorry}, \texttt{admit}, custom axiom declaration, or
\texttt{unsafe} declaration was found in the solution or implementation.
Such a scan is a limited source check, not a kernel replay.

\subsection{Historical mechanical verification}
The record pins Lean \texttt{4.33.0} and Mathlib commit
\nolinkurl{db584cd6d46c92f209a44c0f1c829460d327499d}.
It reports verification on September 23, 2026, through the
\href{https://github.com/PalomarRegistry/PalomarSubmission/actions/runs/35820140999}{recorded Palomar workflow run}
\cite{PalomarRecord}. The comparator configuration selects the theorem
and closed statement definition, enables NanoDa, and permits
\decl{propext}, \decl{Quot.sound}, and \decl{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.

\subsection{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
\emph{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.

\section{Conclusion}

The artifact gives a finite, executable witness to subgroup recognition
for every finite list of words in $\F$. 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.

\clearpage
\bibliographystyle{amsplain}
\bibliography{references}
\end{document}