==== TABLE OF CONTENTS ====
Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem//main.tex
Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem//sections/conclusion.tex
Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem//sections/encoding.tex
Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem//sections/homological.tex
Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem//sections/introduction.tex
Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem//sections/stage.tex
Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem//references.bib
===========================

==== BEGIN Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem//main.tex ====
\documentclass[11pt]{article}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{enumitem}
\usepackage{microtype}
\usepackage{needspace}
\usepackage{tikz-cd}
\usepackage[numbers,sort&compress]{natbib}
\usepackage{xurl}
\usepackage[colorlinks=true,linkcolor=blue,citecolor=blue,urlcolor=blue]{hyperref}
\hypersetup{pdftitle={Simple F-infinity overgroups of groups with decidable word problem},pdfauthor={OpenAI}}
\setlength{\emergencystretch}{2em}
\setlist{itemsep=3pt,topsep=6pt}
\numberwithin{equation}{section}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\newcommand{\Z}{\mathbb Z}
\newcommand{\F}{\mathbb F}
\newcommand{\N}{\mathbb N}
\newcommand{\Q}{\mathbb Q}
\newcommand{\E}{\mathrm E}
\newcommand{\St}{\mathrm{St}}
\newcommand{\Finfty}{F_\infty}
\newcommand{\FPinfty}{\mathrm{FP}_\infty}
\DeclareMathOperator{\im}{im}
\DeclareMathOperator{\id}{id}
\DeclareMathOperator{\GL}{GL}
\DeclareMathOperator{\diag}{diag}
\DeclareMathOperator{\Tor}{Tor}
\DeclareMathOperator{\Sym}{Sym}
\title{Simple \texorpdfstring{$F_\infty$}{F-infinity} overgroups of groups\\
with decidable word problem}
\author{OpenAI}
\date{September 23, 2026}
\begin{document}
\maketitle
\begin{abstract}
Every finitely generated group with decidable word problem embeds in a
simple group of type \(F_\infty\). This resolves the higher-finiteness
strengthening of the Boone--Higman conjecture.
\end{abstract}
\begingroup
\small
\tableofcontents
\endgroup
\clearpage
\input{sections/introduction}
\input{sections/homological}
\input{sections/encoding}
\input{sections/stage}
\input{sections/conclusion}
\bibliographystyle{plainnat}
\bibliography{references}
\end{document}
==== END Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem//main.tex ====

==== BEGIN Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem//sections/conclusion.tex ====
\section{The simple overgroup}\label{sec:simple}

The action constructed in Theorem~\ref{thm:action} provides the input for
the twisted Brin--Thompson construction.  We describe the group and then
apply the simplicity and finiteness theorems of Belk and Zaremsky.

Let $A$ act faithfully on a countably infinite set $S$, and put
$\mathcal C=\{0,1\}^{\N}$.  A \emph{brick} in $\mathcal C^S$ prescribes a
finite binary prefix $\alpha(s)$ in each coordinate $s$, with all but
finitely many prefixes empty.  Its chart
$h_\alpha:\mathcal C^S\to B_\alpha$ prefixes each coordinate by
$\alpha(s)$.  For $a\in A$, the coordinate permutation is
\[
 (\tau_a\xi)(s)=\xi(a^{-1}s).
\]
The \emph{twisted Brin--Thompson group} $SV_A$ consists of the
homeomorphisms represented by two finite brick partitions and a
bijection between their pieces, with each piece map of the form
\[
 h_\beta\tau_a h_\alpha^{-1}:B_\alpha\longrightarrow B_\beta.
\]
Common refinements define composition.  The one-piece maps $\tau_a$
embed $A$ because its action on $S$ is faithful.
This is the construction of \citet[Section~1]{BelkZaremsky2022}.

An action is \emph{oligomorphic} if it has finitely many orbits on
finite subsets of each fixed cardinality.  The transfer theorem below
combines \citet[Theorem~D, with $n=\infty$, and
Theorem~3.4]{BelkZaremsky2022}.

\begin{theorem}[Belk--Zaremsky]\label{thm:twisted-transfer}
Let \(A\) act faithfully and oligomorphically on a countably infinite
set \(S\). Suppose \(A\) and the setwise stabilizer of every finite
subset of \(S\) have type \(\Finfty\).
Then \(SV_A\) is a nontrivial simple group of type \(\Finfty\)
and contains \(A\) through its global coordinate action.
\end{theorem}

\begin{proof}[Proof of Theorem~\ref{thm:main}]
Fix the finitely generated group \(G\) and its word-problem decider.
Theorem~\ref{thm:action} supplies an embedding
\(G\hookrightarrow\Lambda\) and a faithful highly transitive action
of \(\Lambda\) on a countably infinite set \(S\). In particular the
action is oligomorphic: every set of distinct \(m\) points can be
sent to any other such set.

The same theorem gives type \(\Finfty\) for \(\Lambda\) and for each
pointwise stabilizer \(\Lambda_{(F)}\), where \(F\subset S\) is finite.
The setwise stabilizer \(\Lambda_{\{F\}}\) acts on \(F\); its kernel is
\(\Lambda_{(F)}\), and its image lies in the finite symmetric group
\(\Sym(F)\). Lemma~\ref{lem:finite-extension} therefore gives type
\(\Finfty\) for \(\Lambda_{\{F\}}\).
All hypotheses of Theorem~\ref{thm:twisted-transfer} hold. Taking
\(H=SV_\Lambda\), we obtain the required inclusions
\[
 G\hookrightarrow\Lambda\hookrightarrow H,
\]
with \(H\) nontrivial, simple, and of type \(\Finfty\).
\end{proof}

The same overgroup $H$ can be generated by two elements of finite order.
Indeed, type $\Finfty$ implies finite generation, and the additional
conclusion of \citet[Theorem~3.4]{BelkZaremsky2022} applies to the
twisted Brin--Thompson group $H=SV_\Lambda$ constructed above.
==== END Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem//sections/conclusion.tex ====

==== BEGIN Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem//sections/encoding.tex ====
\section{Encoding the diagrams and their actions}\label{sec:encoding}

The ring needed for the action theorem must encode an action built
from its own elementary group $\E_7(B)$ on $B^7$.  Starting with one
ring and encoding its action in a larger ring would not meet this
requirement: the acting group would still come from the original ring.
We construct one finitely presented ring $B$ that accommodates this
action, the two idempotent diagrams, and a centralizing binary corner.

We first describe the diagrams for an arbitrary acting pair, so the
required ring data can be stated precisely.  The construction then
uses finite codes for ring expressions and action data before their
equality algorithms have been proved to terminate.  A calculation
on a code word of length $n$ will call the prospective normalizer
only on words of strictly smaller length.  Induction on that length
will prove these algorithms total and justify the required ring data.

\subsection{Two enlargements of an acting pair}

Let a group $V$ act on a set $Z$, and let $\ell\in\{2,3\}$.  Use
the prefix algebra $D_\ell$ and finite collection $\mathcal P_\ell$
of Lemma~\ref{lem:idempotents}.  Define
\begin{equation}\label{eq:enlargement-map}
 j_E(g)=(1-E)\otimes1+E\otimes g
 \quad(g\in V,\ E\in\mathcal P_\ell)
\end{equation}
in $D_\ell\otimes_{\F_\ell}\F_\ell[V]$, and let
$\mathcal W_\ell(V)$ be the subgroup of units generated by these
elements.  It acts on
\[
 \mathcal Y_\ell(Z)=D_\ell^{(Z)},
\]
the set of finitely supported arrays with entries in $D_\ell$:
$d\otimes g$ multiplies coefficients on the left by $d$ and sends
index $z$ to $gz$.  Write $\mathbf e_z$ for the unit basis entry.

\begin{lemma}\label{lem:enlargement}
Each $j_E$ is a homomorphism.  The map $j_I$ is injective, and
together with $z\mapsto\mathbf e_z$ it embeds the acting pair.
For every indicated orthogonal sum $E+P$ in $\mathcal P_\ell$,
the images of $j_E$ and $j_P$ commute elementwise and
\[
 j_{E+P}(g)=j_E(g)j_P(g).
\]
If $gz=z$, then $j_E(g)\mathbf e_z=\mathbf e_z$ for every $E$.
\end{lemma}

\begin{proof}
Orthogonality of the two summands in
Equation~\eqref{eq:enlargement-map} gives
$j_E(g)j_E(h)=j_E(gh)$ and inverse $j_E(g^{-1})$.
If $EP=PE=0$, direct multiplication gives the claimed commuting
product.  Since $D_\ell$ is nonzero, the elements $1\otimes g$
for distinct $g$ are distinct group-basis elements.  The action
assertions follow from
\[
 j_E(g)\mathbf e_z=(1-E)\mathbf e_z+E\mathbf e_{gz}.
\]
\end{proof}

For a unital $\F_2$-algebra $B$, put $Q=\E_7(B)$ and $X=B^7$,
with the usual left action on columns.  Apply the enlargement twice:
\begin{equation}\label{eq:two-enlargements}
 (W_1,Y^{(1)})=\bigl(\mathcal W_2(Q),\mathcal Y_2(X)\bigr),
 \qquad
 (W,Y^{(2)})=\bigl(\mathcal W_3(W_1),\mathcal Y_3(Y^{(1)})\bigr).
\end{equation}
Write
\[
 \iota:Q\longrightarrow W,\qquad
 \iota_X:X\longrightarrow Y^{(2)},\qquad
 Y=W\iota_X(X)
\]
for the full-identity embeddings and the indicated invariant subset.
With superscripts indicating the enlargement layer, set
\begin{equation}\label{eq:two-diagrams}
 j_{2,E}=j_I^{(3)}\circ j_E^{(2)},\qquad
 j_{3,E}=j_E^{(3)}\circ j_I^{(2)}.
\end{equation}
Both full-identity maps are $\iota$.  Each family satisfies the
orthogonal identities, and
\begin{equation}\label{eq:diagram-fixed-points}
 qx=x\quad\Longrightarrow\quad
 j_{\ell,E}(q)\iota_X(x)=\iota_X(x).
\end{equation}
The characteristic-three algebra in the second enlargement is used
only to define an abstract group.  We will embed that group, not
its algebra, into the characteristic-two ring.

\begin{theorem}\label{thm:ring-data}
For every finitely generated group $G$ with decidable word problem,
there is a nonzero finitely presented unital $\F_2$-algebra $B$
with the following properties.
\begin{enumerate}[label=\textup{(\roman*)}]
\item There is an injective nonunital algebra endomorphism
  $\phi:B\to B$.  With $p=\phi(1)$ there are
  $s_0,s_1,d_0,d_1\in pBp$, centralizing $\phi(B)$, such that
  \begin{equation}\label{eq:ring-binary-pairs}
   d_i s_j=\delta_{ij}p,\qquad s_0d_0+s_1d_1=p.
  \end{equation}
\item Form $Q,X,W,Y,\iota,\iota_X$ and $j_{\ell,E}$ as above.
  There is a nonzero idempotent $e\in B$ such that $G$ and $W$
  embed in $(eBe)^\times$.  There are $S_y,T_y\in eBe$, for
  all $y\in Y$, with
  \begin{equation}\label{eq:ring-prefix-data}
   T_yS_z=\delta_{yz}e,\qquad
   wS_y=S_{wy},\qquad T_yw=T_{w^{-1}y}.
  \end{equation}
  Here $w$ denotes its corner-unit image.
\end{enumerate}
The two diagrams have common full-identity map $\iota$ and
satisfy Equation~\eqref{eq:diagram-fixed-points}.
\end{theorem}

The construction has four steps. We first recall the compiler and
binary-corner results that we use. We then describe a monoid encoding
a group action and give finite codes for the prospective ring and
action data. A length induction proves that the resulting
self-referential normalizer is total and consistent in contexts.
Finally, contracted monoid algebras turn the codes into the required
ring embeddings and corner relations.

\subsection{The bounded compiler and the auxiliary monoid}

We use the following established form of the finite compiler
\citep[Lemma~7.1, Bounded Compiler Lemma]{FoundationsCompanion}.
Its bounded contextual
conclusion is essential.

\begin{lemma}[Bounded compiler]\label{lem:compiler}
Fix a sufficiently large finite alphabet $\Sigma$ containing the
distinguished letters of the compiler.  From an index $\eta$ for
a partial function $f_\eta:\Sigma^*\rightharpoonup\Sigma^*$ one
can compute a finite monoid presentation $K_\eta$, with alphabet
$\mathcal A_\eta$ and zero letter $\Omega$, and an additive
nonnegative integral word grade
$\gamma:\mathcal A_\eta^*\to\Z_{\geq0}$. Letter grades are at
most two, and $\gamma(\Omega)=0$.

There is a partial algorithm
$N_\eta:\mathcal A_\eta^*\rightharpoonup\mathcal A_\eta^*$,
independent of any budget,
with the following property.  Suppose that, for some $m\geq0$,
\begin{align}
 &f_\eta(u)\text{ is defined and }|f_\eta(u)|\leq |u|
       &&(|u|\leq m),\label{eq:compiler-budget-total}\\
 &f_\eta(a f_\eta(u)b)=f_\eta(aub)
       &&(|aub|\leq m).\label{eq:compiler-budget-context}
\end{align}
Then $N_\eta$ terminates through grade $m$.  Each such input is
connected to its literal output by a defining-equation derivation
that never raises grade.  A contextual defining-equation step
preserves the output if both endpoints have grade at most $m$.
Consequently,
\begin{equation}\label{eq:compiler-context}
 N_\eta(u)=N_\eta(v)\ \Longrightarrow\
 N_\eta(aub)=N_\eta(avb)
 \quad\text{if }\gamma(aub),\gamma(avb)\leq m.
\end{equation}
Unconditionally, $N_\eta$ fixes the empty word and $\Omega$,
sends every word containing $\Omega$ to $\Omega$, and fixes a
specified literal word $\operatorname{raw}(u)$ for every
$u\in\Sigma^*$.  The raw words are mutually distinct and distinct
from the empty word and $\Omega$.  If the hypotheses hold at every
$m$, then $N_\eta$ decides equality in $K_\eta$ and
\begin{equation}\label{eq:compiler-raw-product}
 N_\eta\bigl(\operatorname{raw}(u)\operatorname{raw}(v)\bigr)
   =\operatorname{raw}\bigl(f_\eta(uv)\bigr).
\end{equation}
The presentation is computed without evaluating $f_\eta$.
Apart from finite computations, $N_\eta$ calls $f_\eta$ only on
inputs of length at most the grade of its own input.
\end{lemma}

Fix also the monoid $\mathcal D$ of partial maps of $\Q$ generated
by the full affine maps
\[
 u(x)=x/2,\qquad v(x)=(x+1)/2,
\]
their inverses, and the partial identities on
$[0,\infty)\cap\Q$ and $[1,\infty)\cap\Q$.
Composition applies the right factor first.  An element has
computable data $(a,b,r)$, denoting $x\mapsto ax+b$ on
$[r,\infty)\cap\Q$, with $a=2^j$ for $j\in\Z$, dyadic $b,r$,
and $r=-\infty$ for full domain.  These data multiply by
\begin{equation}\label{eq:partial-affine-data}
 (a,b,r)(c,d,s)
   =\bigl(ac,ad+b,\max\{s,(r-d)/c\}\bigr).
\end{equation}
Every domain is infinite, so equality is equality of these data.
This gives an unconditional decision algorithm.

We will use the precise conclusion of the Binary Tail Corner Lemma
\citep[Lemma~6.4]{FoundationsCompanion} for this same monoid:
\begin{equation}\label{eq:external-binary-corner}
 \begin{gathered}
 0\ne q=q^2\in\F_2[\mathcal D],\qquad
 s'_i,d'_i\in q\F_2[\mathcal D]q,\\
 d'_is'_j=\delta_{ij}q,\qquad
 s'_0d'_0+s'_1d'_1=q.
 \end{gathered}
\end{equation}
Its $q$ is the difference of the two tail identities, split
using the affine maps $u$ and $v$.

\subsection{A monoid for an action}

For an acting pair $V\curvearrowright Z$, define $M(V,Z)$ with
absorbing zero, generators $V$ and $\mathsf s_z,\mathsf t_z$
for $z\in Z$, and relations consisting of group multiplication,
zero absorption, and
\begin{equation}\label{eq:action-monoid-relations}
 \mathsf t_y\mathsf s_z=\delta_{yz},\qquad
 g\mathsf s_z=\mathsf s_{gz},\qquad
 \mathsf t_zg=\mathsf t_{g^{-1}z}.
\end{equation}
Here $\delta_{yz}$ denotes the monoid identity or zero.

\begin{lemma}\label{lem:action-monoid-normal-form}
Every nonzero element of $M(V,Z)$ has a unique normal form
\[
 \mathsf s_{z_1}\cdots\mathsf s_{z_a}\,g\,
 \mathsf t_{w_1}\cdots\mathsf t_{w_b},
 \qquad a,b\geq0,
\]
omitting an identity group label.  In particular, $V$ embeds
as a group of units.
\end{lemma}

\begin{proof}
Multiply adjacent group labels, erase identity labels, and
orient Equation~\eqref{eq:action-monoid-relations} to the right.
Each rule shortens the word.  Overlapping group products agree
by associativity; overlaps of two group labels with a prefix
or deletion agree by the action law.  The remaining nonzero
overlap is $\mathsf t_y g\mathsf s_z$.  Its two reductions
agree because $y=gz$ if and only if $g^{-1}y=z$.
Identity and zero overlaps join immediately.  The system is
therefore terminating and locally confluent, hence confluent.
Its irreducibles are exactly the stated words.
\end{proof}

\subsection{Syntax and costs before totality}

For a field $k$ and a monoid $M$ with absorbing zero, write $k_0[M]$ for its
\emph{contracted monoid algebra}: its basis consists of the nonzero
elements of $M$, and a monoid product equal to zero is interpreted
as algebra zero.

Fix provisionally an arbitrary index $\eta$ and its compiler
presentation.  Polynomial expressions over $\F_2$ are finite
sums of monoid words in the presentation letters.  Their
\emph{cost} is the maximum grade of a monomial, with cost zero
for the zero expression.  A column expression has the maximum
cost of its seven entries.  These are syntactic expressions:
we do not assume global equality in the prospective contracted
algebra $(\F_2)_0[K_\eta]$.

Use three families of generating symbols.
\begin{enumerate}[label=\textup{(\alph*)}]
\item A finite symmetric generating alphabet for $G$, evaluated
  using its word decider.  These symbols have cost zero.
\item The presentation alphabet $\mathcal A_\eta$ and a fixed
  finite generating alphabet for $\mathcal D$.  Their prospective
  values lie in the zero-product monoid
  \begin{equation}\label{eq:zero-product-monoid}
   T_\eta=\bigl((K_\eta\setminus\{\Omega\})\times\mathcal D\bigr)
          \sqcup\{0\}.
  \end{equation}
  Nonzero pairs multiply coordinatewise, with a product having
  first coordinate $\Omega$ replaced by zero.  Presentation
  letters have their compiler grades as costs; the other
  symbols have cost zero.
\item Root symbols $I+b\mathbf e_{ij}$, for $1\leq i\ne j\leq7$,
  where $\mathbf e_{ij}$ is the matrix unit and $b$ is an arbitrary
  polynomial expression, and their formal inverses.
  Carry each root through $j_F^{(3)}j_E^{(2)}$, with
  $E\in\mathcal P_2$ and $F\in\mathcal P_3$.
  Also use $\mathsf s_x,\mathsf t_x$ for every column expression
  $x$, indexed by its twice embedded basis entry, and a zero
  symbol.  Costs are those of the root entry or column;
  zero has cost zero.  The prospective evaluation is in $M(W,Y)$.
\end{enumerate}
These alphabets are effectively enumerable from $\eta$ without
running $N_\eta$.  Distinct syntactic descriptions may have the
same eventual value.  The third alphabet generates $M(W,Y)$
once the prospective objects exist: roots generate $Q$, each
$j_E$ is a homomorphism, and translating the supplied column
symbols gives those indexed by all of $Y=W\iota_X(X)$.

Encode these symbols by distinct computably decodable words in
a fixed finite alphabet $\Sigma$, reserving a letter $\zeta$ for
zero. The families use disjoint alphabets, and none uses $\zeta$.
Within each family, fix a start marker and a different end marker.
Every code in that family begins and ends with these markers,
neither of which occurs internally.  Binary syntax descriptions with unary
padding allow us to require
\begin{equation}\label{eq:code-cost}
 |\operatorname{code}(a)|\geq10\operatorname{cost}(a)+2.
\end{equation}
Fix a total order on $\Sigma$. The \emph{shortlex} order compares
words first by length and then lexicographically.
Code membership and enumeration of all code concatenations
through any specified length require no call to $N_\eta$.
The cost of a sequence of symbols is the sum of their costs.

\subsection{Calculations in a bounded system}

The code normalizer will compare expressions and replace them by
shorter codes for the same value.  A shorter code can have greater
symbolic cost.  We therefore need equality to survive substitution
whenever each resulting expression separately fits the available
budget.  The following lemma establishes that property without
assuming that the prospective ring or groups have global equality
algorithms.

\begin{lemma}\label{lem:bounded-action-calculus}
Suppose the hypotheses of Lemma~\ref{lem:compiler} hold through
length $3d$, where $d\geq0$. Within any one of the three families,
evaluation of any symbol sequence of
cost at most $d$, and equality comparison of two such sequences
(each separately of cost at most $d$), terminate using compiler
calls of grade at most $3d$. Tested equality respects
replacing a subword in a product whenever both whole symbol
sequences have cost at most $d$.  Tests agree at different
valid budgets.
\end{lemma}

\begin{proof}
Put $m=3d$.  We first construct bounded algebra, group, and action
operations.  We then normalize words in the action monoid and prove
that equal normal forms can be substituted even when their original
representatives have different costs.

\paragraph{Bounded algebra and action operations.}
For $0\leq b\leq m$, form the classes represented
by words of grade at most $b$, where equality is literal
equality of $N_\eta$ outputs.  These sets are nested, since
equality does not depend on the budget.  Products are defined
when the summed grades fit $m$.  By
Equation~\eqref{eq:compiler-context}, changing representatives
preserves a product whenever both resulting grades fit.
The nonincreasing normalization derivation puts the output
in the ball of the summed grade.  Associativity follows by
concatenating three representatives within their total budget.
The empty and zero classes are distinct, and zero absorbs.

A class has a minimum represented grade by well-ordering.
We use this minimum only in proofs, never as an algorithmic
search.  Finite $\F_2$-linear combinations of nonzero classes
give nested algebra balls.  Addition takes the maximum input
bound, multiplication the sum.  Equality is comparison of
basis coefficients after collecting equal $N_\eta$ outputs.
Distribution and collection preserve products by bounded
contextual compatibility.

For a word in elementary root matrices of cost at most $b$,
store both its forward matrix and the matrix of its formal
inverse word.  Their entries belong to the algebra ball of
level $b$.  Compare both components.  Operations are
\begin{equation}\label{eq:bounded-matrix-pairs}
 (A,A^-)(C,C^-)=(AC,C^-A^-),\qquad
 (A,A^-)^{-1}=(A^-,A).
\end{equation}
They respect equality whenever the summed levels fit $m$.
This avoids assuming uniqueness of inverses outside the
available budget.  A word and its formal inverse cancel
when their total cost fits, by successively cancelling
adjacent root factors; intermediate calculations stay in
that total bound.  Forward matrices act on columns, with
group bound $b$ and column bound $c$ giving bound $b+c$.

This construction propagates through an enlargement.
Expand a group word into a finite array of $D_\ell$-coefficients
indexed by preceding-level group labels; separately expand
the formal inverse.  For a word of cost at most $b$, all
indices in both arrays have level at most $b$.  Compare
arrays after collecting equal indices and performing the
unconditional arithmetic in $D_\ell$.  Multiplication
convolves arrays and adds bounds, reversing the order in
the inverse component as in
Equation~\eqref{eq:bounded-matrix-pairs}.

The corresponding set ball of level $c$ consists of finite
arrays with preceding-level set indices of level at most
$c$.  An acting array of level $b$ gives an output of level
$b+c$, by multiplying coefficients and acting on indices.
Expanding a full triple product gives identical arrays in
either association if the total input bound is at most $m$.
The same expansion proves the action law.  The maps $j_E$
and the basis-entry maps propagate generators and points
without increasing cost.  Formal inverse cancellation
follows from $E^2=E$ and the preceding inverse identities.
Repeating this argument gives both enlargement levels.
Their level inclusions are injective because equality is
literal equality of recursively collected arrays.

We have now defined products, inverses, and actions at both
enlargement levels whenever the total input costs fit $m$.
All identities used to define these operations have been checked
within that budget.  The algorithm retains the original words and
polynomials, multiplies by concatenation and finite expansion, and
uses $N_\eta$ for comparison and collection.  Thus these are finite
calculations in truncated systems; no complete group is assumed,
and no minimum-cost representative is sought.

\paragraph{Normal forms for the action monoid.}
Apply the reductions of
Lemma~\ref{lem:action-monoid-normal-form} to the third
family.  Every reduction consumes disjoint input data,
so the output labels have representations of jointly
bounded total cost no greater than the input cost.
Associativity and the action law resolve their usual
overlaps.  For the exceptional overlap
$\mathsf t_y w\mathsf s_z$, let the costs of $y,w,z$
be $c,b,e$, with $b+c+e\leq d$.  The equivalence
\begin{equation}\label{eq:bounded-inverse-action}
 y=wz\quad\Longleftrightarrow\quad w^{-1}y=z
\end{equation}
uses at most $2b+e$ or $2b+c$ when acting back by the
inverse or forward element.  Both are at most $2d$,
hence within $m$.  For example, equality $y=wz$
allows the action on either representative, and
$w^{-1}(wz)=z$ by the bounded inverse identity.
The converse is the same calculation.  Identity
and zero overlaps join immediately.  Thus the
terminating reductions are confluent on inputs
of total cost at most $d$, and their normal forms
are computed by the finite operations just described.

\paragraph{Substitution with unequal costs.}
It remains to prove the contextual assertion.  The difficulty is
that tested-equal subwords may have different costs, so one cannot
charge both representatives to a single calculation.
Give each group or point label its minimum represented cost in the
truncated system.  At every group level, take this minimum only over
genuine words in that level's generators, stored together with their
formal inverses.  Point labels may instead use ambient array
representatives.

Consider abstract labeled words whose total minimum cost is at most
$d$.  Each reduction above does not increase that total: the resulting
labels have representatives whose joint cost is no larger than that
of the labels consumed.  The same overlap calculations therefore
prove confluence on these abstract words.  In particular, the
inverse-action overlap still fits $2d\leq m$.

By the equality test just constructed, two tested-equal subwords
have the same normal form.  If it is zero, both contextual products
reduce to zero.  Otherwise it is a list $R$ of prefix labels, group
label, and deletion labels.  Its total minimum
cost is at most the original cost of either subword, since each
reduction supplied jointly bounded representatives for its output.
Put the subwords in fixed left and right contexts, with each whole
word separately of cost at most $d$.  Normalize the middle first.
Both routes reach the identical abstract word with middle $R$, and
this word fits the budget on each route.  Its unique normal form is
therefore the answer on both sides.  No step adds the costs of the
old and new equal representatives.

Minimum-cost point representatives may be ambient
array expressions rather than short orbit words.
That is sufficient: $R$ is a semantic proof device,
and the algorithm never needs to find a code for
it or decide membership in an orbit.

The second family has contextual compatibility
directly from Equation~\eqref{eq:compiler-context}
and the affine data; the first has it from its
group law and word decider.  Finally all the
comparisons use outputs of the same algorithm
$N_\eta$, not a budget-dependent normalizer.
The recursive array comparisons inherit that
independence, proving compatibility of budgets.
\end{proof}

\subsection{The self-referential normalizer}

The bounded calculations are now available conditionally.
We next construct the word normalizer whose consistency is the
condition they require. Its call bounds will make this apparent
circularity into an induction on word length.

For $\eta$ and a word $w\in\Sigma^*$ of length $n$,
define a partial procedure $F(\eta,w)$ as follows.
Include $a\zeta\to\zeta$ and $\zeta a\to\zeta$ for
every $a\in\Sigma$.  For every nonempty concatenation
$c$ of whole codes from one family with $|c|\leq n$,
evaluate its prospective product.  If the value is
zero, include $c\to\zeta$.  Otherwise search all
same-family code concatenations of length at most
$|c|$, also allowing the empty word for identity,
and choose the least tested-equal one in shortlex.
Include the replacement unless unchanged.  The
starting word is itself a candidate, so the search
is finite whenever its tests terminate.

Reduce $w$ using a fixed deterministic choice of
rule and occurrence.  Every nontrivial rule decreases
shortlex.  A zero-valued code has length at least
two, so replacement by $\zeta$ also shortens.
Thus the reduction terminates once its finite
table of tests is available.  This is uniformly
partial computable, including computation of the
compiler presentation from its parameter $\eta$.

Effective parameterization gives a total computable
index transformation $\tau(\eta)$ for $F(\eta,-)$.
Kleene's Recursion Theorem supplies an index such that
\begin{equation}\label{eq:encoding-fixed-point}
 f_\eta(w)=F(\eta,w)
\end{equation}
as partial functions \citep[\S~2, p.~153]{Kleene38}.
Explicitly, if $U$ is universal evaluation, let
$d(a)$ be an effectively obtained index for
$w\mapsto U(U(a,a),w)$.  Choose $b$ computing
the total index-valued function $a\mapsto\tau(d(a))$.
Then $\eta=d(b)$ satisfies
\[
 U(\eta,w)=U(U(b,b),w)
          =U(\tau(d(b)),w)=F(\eta,w).
\]
No termination of $F(\eta,-)$ is assumed here.
Fix this $\eta$.

\begin{lemma}\label{lem:encoding-bootstrap}
The function $f_\eta$ is total and length-nonincreasing.
Its rule tables are stable on bounded-length words and
confluent on those words.  In particular,
\begin{equation}\label{eq:encoding-context-law}
 f_\eta(a f_\eta(u)b)=f_\eta(aub)
 \qquad(a,u,b\in\Sigma^*).
\end{equation}
\end{lemma}

\begin{proof}
Induct simultaneously on the input length $n$.
For $n=0$ there are no tests or reductions and
the empty word is unchanged.  For $n>0$, put
$d=\lfloor n/10\rfloor$.  Every code string in
a table entry or representative search has cost
at most $d$ by Equation~\eqref{eq:code-cost}.
Since
\begin{equation}\label{eq:strict-encoding-dependency}
 3\lfloor n/10\rfloor<n,
\end{equation}
the induction hypothesis supplies the compiler
hypotheses through length $3d$.  All tests
terminate by Lemma~\ref{lem:bounded-action-calculus}.
Only finitely many code strings have length at
most $n$, even though the symbol alphabet is
countable and can contain infinitely many
zero-cost symbols.  The finite table and its
shortlex-decreasing reduction therefore terminate.

A rule on a fixed code string is determined by
the same tests and the same search bound at
every larger length.  Thus rules with left
side of length at most $k$ are unchanged once
length $k$ is reached; longer rules cannot
act on a word of length at most $k$.

For local confluence in the length-$n$ ball,
disjoint occurrences commute, even when a
replacement is empty.  Every branch from a
word containing $\zeta$ retains it and can
be absorbed to $\zeta$, since code strings
avoid that letter.  Two overlapping code
rules have aligned code boundaries and
belong to the same family, by the delimiter
conditions.  Their union is a whole code
concatenation of length at most $n$.

Either replacement preserves its tested class
by Lemma~\ref{lem:bounded-action-calculus}.
A shorter code representative may have higher
symbolic cost.  We do not assert otherwise:
the old and new unions each separately have
length at most $n$, hence cost at most $d$.
This is the two-endpoint hypothesis of that lemma.

For a zero-class union, a branch either
introduces $\zeta$ and absorbs, or leaves
a zero-class code string with a whole-word
zero rule.  It cannot leave the empty
string, since zero and identity are distinct.
For a nonzero-class union, let $c_*$ be
its least representative within the original
search bound.  A branch gives a same-class
string $c_b$ of no greater length.  This was
an original candidate, so $c_*\leq c_b$
in shortlex, in particular $|c_*|\leq|c_b|$.
Thus $c_*$ is still the least candidate in
the branch's smaller search bound.  Each
branch reaches it by its whole-word rule,
unless already there.  This covers an empty
$c_*$ and containment overlaps as well.

The joining steps occur inside the old
union before any newly adjacent outside
letters are used.  Erasing identity codes
can therefore expose further redexes but
creates no missing local peak.  In particular,
different-family adjacencies after an erasure
do not create an overlapping initial peak.

Termination and local confluence give
confluence by Newman's Lemma \citep{Newman42}.
Its well-founded proof applies within the
ball: proper descendants have unique normal
forms, and a common descendant of two first
steps equates their normal forms.

For $|aub|\leq n$, normalize $u$ inside
its context first.  Stability puts all
these rules in the length-$n$ table;
length never increases.  Confluence proves
$f_\eta(a f_\eta(u)b)=f_\eta(aub)$.
The compiler hypotheses now hold through
length $n$, completing the induction.
\end{proof}

\subsection{The monoids and the ring}

The length induction has supplied a total normalizer consistent in
every context.  We now obtain the two algebra embeddings used to
construct $B$ and its self-map.  One comes directly from the code
families.  For the other, the compiler's raw words preserve monoid
multiplication but send the absorbing zero to a nonzero algebra
basis element.  Subtracting that basis element will give an embedding
of the contracted monoid algebra.

Let $L$ be the monoid on $\Sigma$ with equations
the union of the rule tables.  Every word is
related to its computed normal form.  Conversely,
a contextual defining equation preserves that
form: choose a length bound containing the
equation and both endpoints, and use stability
and confluence.  Thus equality in $L$ is exactly
equality of literal $f_\eta$ outputs.  Its
identity and absorbing zero are the distinct
irreducibles $\varepsilon$ and $\zeta$.

Lemma~\ref{lem:compiler} now applies at every
grade, giving an equality algorithm for
$K=K_\eta$ with distinct identity and zero.
Set
\[
 k=\F_2,\qquad B=k_0[K],\qquad A_*=k_0[L].
\]
The previously prospective $Q,X,W,Y$
now exist, and the bounded calculations
are their genuine evaluations.  Paired
forward/inverse equality agrees with
ordinary group equality, since the
formal inverse is now a genuine inverse.

\begin{lemma}\label{lem:encoding-embeddings}
The code families embed $G$, $T_\eta$, and
$M(W,Y)$ unitally into $L$, preserving
zeros in the last two cases.  There are
injective algebra maps
\begin{equation}\label{eq:encoding-algebra-maps}
 \kappa:B\otimes_k k[\mathcal D]\longrightarrow A_*,
 \qquad i:A_*\longrightarrow B,
\end{equation}
where $\kappa$ is unital and $i$ has a
nonzero proper support identity $e=i(1)$.
\end{lemma}

\begin{proof}
In one family, a least shortlex code
representative of a nonzero value is
irreducible.  An internal code reduction
would preserve its value and lower
shortlex, while zero and other-family
rules cannot occur inside it.  Every other
representative reduces to it by its
whole-word rule.  Zero values reduce
to $\zeta$.  Hence values remain distinct.
Codes concatenate and the empty identity
representative is allowed, giving unital
multiplicative embeddings.  The embedded
groups are units, using also
Lemma~\ref{lem:action-monoid-normal-form}.

For $h\in L$ with normal word $\overline h$, put
\[
 c(h)=[\operatorname{raw}(\overline h)]\in K.
\]
Distinct normal words give distinct
literal raw $N_\eta$ outputs, hence
distinct elements of $K$ avoiding
$1_K$ and $\Omega$.
Equation~\eqref{eq:compiler-raw-product}
gives $c(h)c(h')=c(hh')$.
The identity and zero need not be
preserved: $c(1_L)\ne1_K$ and
$c(\zeta)\ne\Omega$.  They are identity
and absorbing zero only within $c(L)$.

For a nonzero basis element $h$ of $A_*$, set
\begin{equation}\label{eq:raw-difference-embedding}
 i(h)=c(h)-c(\zeta).
\end{equation}
Since $c(h)c(\zeta)=c(\zeta)c(h)=c(\zeta)$
and $c(\zeta)^2=c(\zeta)$,
\[
 (c(h)-c(\zeta))(c(h')-c(\zeta))
     =c(hh')-c(\zeta).
\]
If $hh'=\zeta$, this is zero as required.
Distinct $c(h)$ are distinct nonzero
basis vectors of $B$.  The vectors in
Equation~\eqref{eq:raw-difference-embedding}
are therefore linearly independent,
proving injectivity.  The support identity
\[
 e=c(1_L)-c(\zeta),\qquad e^2=e,
\]
is nonzero and is not $1_B$, since neither
of its basis vectors is $1_K$.

Finally nonzero basis pairs identify
$B\otimes_k k[\mathcal D]$ with
$k_0[T_\eta]$.  The code embedding
of $T_\eta$ extends linearly to
the required unital injection $\kappa$.
\end{proof}

\begin{lemma}\label{lem:encoding-finite-presentation}
The algebra $B$ is nonzero and finitely
presented as a unital associative
$\F_2$-algebra, and as a unital ring.
\end{lemma}

\begin{proof}
Take the finite generators of $K$ in
the free unital associative $\F_2$-algebra.
Replace its defining equations $u=v$
by binomials $u-v=0$, and impose
$\Omega=0$.  Before the last relation,
the binomial ideal is exactly the span
of differences of words in the same
monoid congruence class.  Indeed
contextual equation steps lie in the
ideal and telescope along a derivation;
conversely the linear map sending words
to monoid classes annihilates all
binomials.  The quotient has basis $K$.
Killing its absorbing zero class removes
exactly that basis element and gives
$k_0[K]$.  Identity survives since
$1_K\ne\Omega$.  Adding $2\cdot1=0$
gives a presentation as a unital ring.
\end{proof}

\begin{proof}[Proof of Theorem~\ref{thm:ring-data}]
The ring properties follow from
Lemma~\ref{lem:encoding-finite-presentation}.
The code embeddings put $G$ and $W$
in $A_*^\times$.  Transporting them
through $i$ puts them in $(eBe)^\times$.
Transport the prefix and deletion
symbols to $S_y,T_y\in eBe$.
Their monoid relations become exactly
Equation~\eqref{eq:ring-prefix-data},
with identity mapped to $e$ and zero
mapped to algebra zero.

Use Equation~\eqref{eq:external-binary-corner}
and define
\begin{equation}\label{eq:encoding-phi}
 \phi(b)=i\kappa(b\otimes q),\qquad
 s_i=i\kappa(1\otimes s'_i),\qquad
 d_i=i\kappa(1\otimes d'_i).
\end{equation}
The first map is multiplicative because
$q^2=q$ and injective because $q\ne0$,
the tensor product is over a field,
and $i,\kappa$ are injective.  With
$p=\phi(1)$, the binary identities
give $s_i,d_i\in pBp$ and
Equation~\eqref{eq:ring-binary-pairs}.
Moreover
\[
 (b\otimes q)(1\otimes s'_i)
   =b\otimes s'_i
   =(1\otimes s'_i)(b\otimes q),
\]
and the same holds for $d'_i$.
Thus these elements centralize $\phi(B)$.
Since $p\in eBe$ and $e\ne1_B$,
we have $p\ne1_B$, so $\phi$ is
nonunital.  The diagram assertions
follow from Lemma~\ref{lem:enlargement}
and Equations~\eqref{eq:two-diagrams}
and~\eqref{eq:diagram-fixed-points}.
\end{proof}
==== END Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem//sections/encoding.tex ====

==== BEGIN Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem//sections/homological.tex ====
\section{A homological device for ascending tori}
\label{sec:homological}

An ascending torus will have type $\Finfty$ for two distinct reasons.
Factoring its defining endomorphism through a finitely presented group
provides finite presentation.  Two finite systems of commuting
splittings then give the higher-dimensional finiteness: one system
annihilates the relevant homology classes by $2$, and the other
annihilates the same classes by $3$.  The factorization also starts
this second argument, by placing the image of the endomorphism in
a finitely generated subgroup.

We first construct the finite systems of idempotents that index the
splittings.  The resulting criterion is Theorem~\ref{thm:torus}.
Its proof must control a finite set of simplex types uniformly over
all cycles; it will impose no bound on chain lengths or coefficients.

\subsection{Two finite systems of idempotents}

For $\ell\in\{2,3\}$, let $D_\ell$ be the unital $\F_\ell$-algebra
of operators generated by $l_0,l_1,r_0,r_1$ on the free vector space
with basis $\{0,1\}^{\N}$.  The operator $l_i$ prefixes $i$, whereas
$r_i$ deletes an initial $i$ and sends every other basis vector to zero.
Thus
\begin{equation}\label{eq:binary-prefix-relations}
 r_i l_j=\delta_{ij}1,
 \qquad l_0r_0+l_1r_1=1.
\end{equation}
For a finite binary word $v$, write $l_v$ for prefixing $v$, write $r_v$
for deleting $v$, and put $E_v=l_vr_v$.

Every product of these operators is zero or a prefix replacement
$l_vr_w$.  Equality of finite linear combinations of prefix replacements
is decidable.  Indeed, choose $m$ at least as large as every domain
prefix length and expand each term by
\[
 l_vr_w=\sum_{|a|=m-|w|}l_{va}r_{wa}.
\]
Collect terms with the same domain prefix and the same output prefix.
For a fixed domain prefix, distinct output prefixes give distinct
outputs on an input whose remaining tail is not eventually periodic.
To see this, equality of two such outputs with different prefixes
would make the shorter prefix a prefix of the longer and would force
the remaining tail to be periodic.  The collected coefficients therefore
all vanish if and only if the operator vanishes.  This is a finite test
over $\F_\ell$.

Put
\[
 A=E_{00},\quad B'=E_{01},\quad C'=E_1,
 \qquad A_0=E_{000},\quad A_1=E_{001}.
\]
For each of the three prefix-free lists
\[
 (00,01,1),\qquad (000,01,1),\qquad (001,01,1),
\]
the operators $l_vr_w$ form matrix units for a copy of
$M_3(\F_\ell)$ in $D_\ell$.  Only the first of these copies has
identity $1$.  Let $\mathcal P_\ell$ be the union of their sets of
idempotents, together with $I=1$.  This is a finite, explicitly
specified set.  In the following statement, orthogonal means
$EP=PE=0$.

\begin{lemma}\label{lem:idempotents}
Let $T$ be an abelian group, and suppose that elements $z_E\in T$,
indexed by $E\in\mathcal P_\ell$, satisfy
\begin{equation}\label{eq:idempotent-additivity}
 z_{E+P}=z_E+z_P
\end{equation}
whenever $E,P,E+P\in\mathcal P_\ell$ and $E,P$ are orthogonal.
Then $\ell z_I=0$.
\end{lemma}

\begin{proof}
Within a rank-three matrix algebra, we will show that the
$\ell$-multiples attached to its diagonal units agree.  The overlapping
corners then identify these multiples for $A,A_0,A_1,B',C'$,
and the split $A=A_0+A_1$ forces their common value to vanish.

First work in any one of the three matrix algebras.  For a column
vector $u$ and a row covector $\lambda$ with $\lambda u=1$, write
$x(u,\lambda)=z_{u\lambda}$.  Fix $v\ne0$ in $\ker\lambda$.
We claim that
\[
 x(u+v,\lambda)-x(u,\lambda)
\]
is independent of the choice of $u$ with $\lambda u=1$.

Suppose first that $u'-u$ and $v$ are linearly independent.  The vectors
$u,u'-u,v$ then form a basis, so there is a covector $\mu$ with
\[
 \mu u=\mu u'=0,\qquad \mu v=1.
\]
The identity
\[
 u\lambda+v\mu=(u+v)\lambda+v(\mu-\lambda)
\]
expresses the same rank-two idempotent in two ways as a sum of
orthogonal rank-one idempotents.  Applying
\eqref{eq:idempotent-additivity} gives
\begin{equation}\label{eq:rank-one-difference}
 x(u+v,\lambda)-x(u,\lambda)
   =x(v,\mu)-x(v,\mu-\lambda).
\end{equation}
The same calculation for $u'$ gives the same difference.  If instead
$u'-u$ belongs to the span of $v$, choose
$w\in\ker\lambda\setminus\langle v\rangle$ and set $u''=u+w$.
Both $u''-u$ and $u''-u'$ are independent of $v$, so comparison through
$u''$ proves the claim.  This argument also applies over $\F_2$.

Apply the claim successively at $u,u+v,\ldots,u+(\ell-1)v$.
The resulting differences are equal, and their sum is zero.  Hence
\[
 \ell x(u+v,\lambda)=\ell x(u,\lambda).
\]
Transposing the argument shows that the $\ell$-multiple is also
unchanged when the covector is varied with the vector fixed and its
value still equal to one.  For two different basis vectors $e_i,e_j$,
take $\lambda=e_i^*+e_j^*$.  Change the covector at $e_i$, change the
vector from $e_i$ to $e_j$, and then change the covector at $e_j$.
It follows that the $\ell$-multiples of all three diagonal units agree.

The overlaps among our three matrix algebras now give
\[
 \ell z_A=\ell z_{B'}=\ell z_{C'}
            =\ell z_{A_0}=\ell z_{A_1}.
\]
Call their common value $q$.  Since $A=A_0+A_1$, relation
\eqref{eq:idempotent-additivity} gives $q=2q$, and therefore $q=0$.
Finally, $I=(A+B')+C'$, with $A+B'$ an idempotent in the first matrix
algebra.  Two applications of the same relation yield
$\ell z_I=0$.
\end{proof}

\subsection{The ascending-torus theorem}

For a group $U$ and an endomorphism $f:U\to U$, write
\[
 T(U,f)=\langle U,t\mid t^{-1}ut=f(u)\ (u\in U)\rangle.
\]
Here the notation includes all relations already holding in $U$.

\Needspace{18\baselineskip}
\begin{theorem}\label{thm:torus}
Let $f:U\to U$ be an injective endomorphism.  Assume the following.
\begin{enumerate}[label=\textup{(\roman*)}]
\item There are a finitely presented group $P$ and homomorphisms
      $a:U\to P$, $b:P\to U$ with $f=ba$.
\item For each $\ell\in\{2,3\}$ there are homomorphisms
      $h_E:U\to U$, indexed by $E\in\mathcal P_\ell$, such that
      $h_I=f$.  Whenever $E,P',E+P'\in\mathcal P_\ell$ and
      $EP'=P'E=0$, the subgroups $h_E(U)$ and $h_{P'}(U)$ commute
      elementwise, and
      \[
       h_{E+P'}(u)=h_E(u)h_{P'}(u)\qquad(u\in U).
      \]
\end{enumerate}
Then $T(U,f)$ is of type $\Finfty$.
\end{theorem}

We first establish finite presentation.  A product-module criterion
then reduces the remaining assertion to a precise homology-vanishing
statement.  Uniformly controlled fillings will supply that vanishing
through the homology sequence of the ascending torus.

\begin{lemma}\label{lem:torus-presentation}
Under assumption \textup{(i)} of Theorem~\ref{thm:torus}, the group
$T(U,f)$ is finitely presented.  This assertion does not require $f$
to be injective.
\end{lemma}

\begin{proof}
Set $g=ab:P\to P$, and let $s$ be the stable letter of $T(P,g)$.
There is a homomorphism
\[
 T(U,f)\longrightarrow T(P,g),\qquad u\longmapsto a(u),\quad
 t\longmapsto s.
\]
An inverse sends $p\in P$ to $t b(p)t^{-1}$ and sends $s$ to $t$.
The defining conjugation relations verify that these are homomorphisms;
their composites are the identity because
$t f(u)t^{-1}=u$ and $s g(p)s^{-1}=p$.
This is the algebraic interleaving of the two direct systems.  No
injectivity of $g$ is needed.  Finally, a finite presentation of $P$,
together with $s$ and its conjugation relations on a finite generating
set of $P$, is a finite presentation of $T(P,g)$.
\end{proof}

\subsection{A product-module criterion}

The product-module test below is a form of the Bieri--Eckmann
finiteness criterion \citep[Proposition~1.2]{BieriEckmann1974}.
For the cellular passage from homological to geometric finiteness,
see also Brown \citep[Section~3]{Brown1975}.  We give the argument for
the now finitely presented group $J=T(U,f)$: vanishing with products
of regular modules will yield finite skeleta of a classifying space.

All group homology below has integral coefficients, and coefficient
modules are right modules.  For a group $J$ and a set $\mathcal I$, the
notation $(\Z J)^{\mathcal I}$ means the direct product, not the
direct sum, with its coordinatewise right action.

\begin{lemma}\label{lem:product-criterion}
Suppose that $J$ is finitely presented and that
\[
 H_n\bigl(J,(\Z J)^{\mathcal I}\bigr)=0
 \qquad(n\ge2)
\]
for every set $\mathcal I$.  Then $J$ is of type $\Finfty$.
\end{lemma}

\begin{proof}
Start with a finite presentation complex and its simply connected
universal cover.  Inductively, suppose we have a connected CW complex
with fundamental group $J$, finite $n$-skeleton, and
$(n-1)$-connected universal cover, where $n\ge2$.  Its universal-cover
$n$-skeleton will be denoted by $Z$.  Attach cells of dimensions at
least $n+1$, without a finiteness requirement, to obtain a contractible
free $J$-complex $\widetilde Z$.  This can be done successively by
killing homotopy groups.  Its augmented cellular chain complex is a
free resolution over $R=\Z J$, and its modules $C_i$ are finitely
generated for $i\le n$.

Let $\mathcal I$ be the set of all cellular $n$-cycles in $Z$, and put
$M=R^{\mathcal I}$.  For every finite-rank free left $R$-module $C$,
the coordinate map gives an isomorphism
\begin{equation}\label{eq:finite-rank-product-tensor}
 M\otimes_R C\ \longrightarrow\ C^{\mathcal I},
 \qquad (m_i)_{i\in\mathcal I}\otimes c
             \longmapsto (m_i c)_{i\in\mathcal I}.
\end{equation}
Using this in degrees $n$ and $n-1$, the family whose coordinate
indexed by a cycle $z$ is $z$ itself defines a cycle in
$M\otimes_R C_n$.  By hypothesis, it is the boundary of some
$y\in M\otimes_R C_{n+1}$.

Choose an $R$-basis for $C_{n+1}$.  Although that basis can be infinite,
the tensor $y$ uses only finitely many of its elements,
say $c_1,\ldots,c_s$.  Taking coordinates of its boundary equation
shows that every $n$-cycle is an $R$-linear combination of
$\partial c_1,\ldots,\partial c_s$.  Thus the $R$-module of
$n$-cycles in $Z$ is finitely generated.  This argument does not assume
that $C_{n+1}$ has finite rank.

Since $Z$ is $(n-1)$-connected, the natural Hurewicz isomorphism
\citep[Theorem~4.37]{Hatcher2002} identifies
$\pi_n(Z)$ with $H_n(Z;\Z)$.  There are no $(n+1)$-cells in $Z$,
so the latter group is precisely its group of cellular $n$-cycles.
Choose spheres representing the finite list of module generators and
attach their $J$-translates.  Downstairs, this attaches finitely many
$(n+1)$-cells; upstairs, it produces an $n$-connected universal cover.
Induction gives a complex with finitely many cells in each dimension
whose universal cover is weakly contractible.  That cover is a CW
complex, so it is contractible by Whitehead's theorem
\citep[Theorem~4.5]{Hatcher2002}.  The resulting complex is the required
$K(J,1)$.
\end{proof}

For $J=T(U,f)$, finite presentation is already available.  It therefore
remains to prove
\[
 H_n\bigl(J,(\Z J)^{\mathcal I}\bigr)=0
 \qquad(n\ge2)
\]
for every set $\mathcal I$.  A tensor chain with these coefficients
may have arbitrarily large supports in its separate coordinates.
The next argument retains the finite set of simplex types shared by
all coordinates; this is the control needed to fill such chains.

\subsection{Uniformly bounded simplex types}

Let $\mathcal E(U)$ be the simplicial set whose $q$-simplices are
tuples $(u_0,\ldots,u_q)$ of elements of $U$.  Faces delete entries
and degeneracies repeat entries.  Its normalized integral chain
complex is denoted by $C_*(U)$.  Thus tuples with consecutive equal
entries are zero, and the boundary is the alternating sum of faces.
The augmentation sends each vertex to $1$.  Simultaneous left
translation gives a free $U$-action. Its augmented chain complex is
contractible as a complex of abelian groups: prepending the identity
gives a contraction.
Consequently its augmented chain complex is a free resolution of the
trivial left $\Z U$-module.

For a finite symmetric set $A\subseteq U$ containing $1$, let
$\mathcal E_A(U)$ consist of the tuples satisfying
\[
 u_i^{-1}u_j\in A\qquad\text{for all }i,j,
\]
and write $C_*^A(U)$ for its normalized chains.  This is a simplicial
subset.  We call $A$ a \emph{bound}.  A chain operator is controlled
on a given input bound if all its output chains lie in $C_*^{A'}(U)$
for some finite output bound $A'$ in each of the degrees under
consideration.  There is no restriction on the number of terms in an
individual output chain.

For each fixed degree $q$, $C_q^A(U)$ has only finitely many basis
elements up to left translation: translate the first vertex to $1$,
after which every other vertex belongs to $A$.  We refer to these
orbits as simplex types.  Every homomorphism of groups sends a finite
bound to a finite bound.  Unions of finitely many bounds may always
be replaced by one finite symmetric bound containing $1$.

Coning at $1$ fills every reduced cycle in the full complex $C_*(U)$.
It does not, however, preserve a common finite bound: on a simplex
with vertex $u$, it introduces the difference $u$ itself.  This becomes
an obstruction when the same bound must work for all translates and all cycles of
$C_*^A(U)$.  We instead construct fillings after an iterate of $f$,
using bounds independent of the individual cycle.

The first step is a controlled additivity calculation in integral
chain complexes.  Its partial homotopy need not be $U$-equivariant.
Later we assemble these ordinary fillings into fillings with product
coefficients.  We will not tensor the chosen homotopy over $\Z U$.

\begin{lemma}\label{lem:controlled-additivity}
Fix $n\ge1$ and a bound $A$.  Suppose that a power $f^k$ induces a
chain map
$F:C_*^A(U)\to C_*(U)$ admitting a controlled chain homotopy to the
constant map at $1$ through degrees less than $n$.  Let
$h_1,h_2:U\to U$ have elementwise commuting images, and put
$h(u)=h_1(u)h_2(u)$.  There is a finite bound $B$ such that every
$n$-cycle $z\in C_n^A(U)$ satisfies
\[
 [(h f^k)_*z]=[(h_1f^k)_*z]+[(h_2f^k)_*z]
       \quad\text{in }H_n(C_*^B(U)).
\]
The same output bound may be chosen for any fixed finite collection
of such pairs of maps.
\end{lemma}

\begin{proof}
Let $H_q$ be the given homotopy operators for $0\le q<n$, and set
$H_q=0$ in all other nonnegative degrees.  The chain map
\[
 F'=F-\partial H-H\partial
\]
is constant at the identity in degree zero and zero in degrees
$1,\ldots,n-1$.  Since $H_n=0$, it satisfies $F'z=Fz$ for every
$n$-cycle $z$.  Choose a common bound for $F$, $F'$, and the finitely
many operators $H_q$ used here.

The diagonal argument below eliminates mixed product terms using
lower-degree vanishing.  The same mechanism appears in the
diagonal-and-K\"unneth induction for mitotic groups
\citep[Proposition~4.1]{BDH1980}.  Here we need an integral chain
calculation retaining a common finite bound.  We use the classical
Alexander--Whitney and shuffle comparison of product and tensor
chain complexes \citep{EilenbergZilber1953}, recording the formulas
and their support control.
Define the diagonal tensor-chain map by
\begin{equation}\label{eq:aw-diagonal}
 D(u_0,\ldots,u_q)
  =\sum_{i=0}^q
       (u_0,\ldots,u_i)\otimes(u_i,\ldots,u_q).
\end{equation}
The tensor differential has the convention
$\partial(c\otimes d)=\partial c\otimes d+
(-1)^{\deg c}c\otimes\partial d$.
The terms at the two sides of each interior cut cancel, showing that
$D$ is a chain map.  Formula~\eqref{eq:aw-diagonal} descends to
normalized chains.

The shuffle map $S$ sends a tensor
$(u_0,\ldots,u_p)\otimes(v_0,\ldots,v_q)$ to the signed sum of
the chains in $U\times U$ obtained by following all monotone lattice
paths from $(0,0)$ to $(p,q)$ and replacing a lattice point $(i,j)$
by $(u_i,v_j)$.  Its sign is $(-1)^N$, where $N$ counts pairs in which
a vertical step precedes a horizontal step.  Deleting a corner of a
path cancels with the path traversing that corner in the other order;
the remaining faces are exactly the tensor differential.  Hence $S$
is a chain map, also on normalized chains.  Both $D$ and $S$ preserve
the bound in each coordinate.

Let $\Delta$ be the chain map induced by $u\mapsto(u,u)$.
There is a controlled chain homotopy between $\Delta$ and $SD$.
Here is a direct construction.  For a basis simplex $c$ with vertex
set $V$, both maps are supported on the full tuple complex on
$V\times V$.  Construct a homotopy $R$ inductively on degree.  In
degree zero the two maps agree, so take $R_0=0$.  Having defined it
on faces, the chain
\[
 \Delta c-SDc-R\partial c
\]
is a cycle supported on that same tuple complex.  It bounds there by
prepending the vertex $(u_0,u_0)$, where $u_0$ is the first vertex of
$c$.  Choose this cone for $R(c)$ and extend on the normalized basis.
Every coordinate vertex used is a vertex of $c$, so $R$ preserves
the bound in both coordinates.  This proves the needed homotopy
without any assumption about chain lengths.

Write $f^k\times f^k:U\times U\to U\times U$ for the product
homomorphism.  On the input complex,
\[
 \Delta F=(f^k\times f^k)_*\Delta
 \simeq (f^k\times f^k)_*SD=S(F\otimes F)D.
\]
The homotopy is $(f^k\times f^k)_*R$ from the preceding construction;
the last equality is naturality of the shuffle.  Thus it is controlled
on the input bound.  Next, the usual signed tensor operator
\[
 H\otimes F+F'\otimes H
\]
is a homotopy between $F\otimes F$ and $F'\otimes F'$.
In the second summand the value on $c\otimes d$ includes the sign
$(-1)^{\deg c}$.  Indeed its homotopy boundary is
\[
 (F-F')\otimes F+F'\otimes(F-F')
       =F\otimes F-F'\otimes F'.
\]
All chains involved have finite bounds separately in the two
coordinates, because this calculation uses only the already
controlled operators.

For an $n$-cycle $z$, applying $F'\otimes F'$ to $Dz$ leaves only
bidegrees $(0,n)$ and $(n,0)$.  The result is
\[
 (1)\otimes F'z+F'z\otimes(1)
     =(1)\otimes Fz+Fz\otimes(1).
\]
Shuffling a vertex against a chain merely holds that coordinate
fixed.  Finally apply the homomorphism
\[
 U\times U\longrightarrow U,
 \qquad (u,v)\longmapsto h_1(u)h_2(v).
\]
It is a homomorphism because the two images commute elementwise.
For coordinate bounds $B_1,B_2$, a difference in its image belongs
to the finite set $h_1(B_1)h_2(B_2)$.  Thus all preceding homotopies
remain controlled after this map.  Their two surviving terms give
the asserted identity.  Taking a union of output bounds proves the
last assertion.
\end{proof}

\begin{proposition}\label{prop:uniform-fillings}
Under the assumptions of Theorem~\ref{thm:torus}, for every finite
bound $A$ and every $n\ge0$ there are an integer $k\ge0$ and a finite
bound $B$ such that $f^k$ sends every reduced integral $n$-cycle of
$C_*^A(U)$ to a boundary in $C_*^B(U)$.
\end{proposition}

\begin{proof}
The word ``reduced'' matters only in degree zero.  The subgroup
$b(P)$ is finitely generated and contains $f(U)$.  Choose a finite
symmetric generating set for $b(P)$.  Every vertex $f(u)$ can be
joined to $1$ by a finite edge path whose differences belong to that
set.  Consequently every reduced zero-cycle is filled after applying
$f$, with a bound independent of the cycle.  This proves the base
case.  Notice that the paths need not have uniformly bounded lengths.

Suppose that the proposition is known in degrees less than $n$,
where $n\ge1$.  We first obtain the controlled partial homotopy
required by Lemma~\ref{lem:controlled-additivity}.  Begin with the
map induced by $f$ and choose the vertex paths just described for
its degree-zero homotopy to the constant map.  Suppose more generally
that a power of $f$ and its homotopy have been constructed through
degree $q-1$, with $1\le q<n$.  For every normalized $q$-simplex $c$, the
missing boundary equation for its homotopy value has right side
\[
 F(c)-H(\partial c),
\]
where $F$ is the current chain map.  For $q\ge1$ this is a cycle:
apply the already established homotopy equation to $\partial c$.
All these cycles, for all basis simplices $c$, have a common finite
bound.  The inductive assertion in degree $q$ supplies one further
power of $f$ that sends all of them to boundaries at a common bound.
Apply that power also to the previously constructed map and homotopy,
then choose a finite filling for each of these boundary equations.
Extending on the normalized basis defines $H_q$ with the required
control.  For $n=1$ only the initial vertex homotopy is needed.

After finitely many such steps, the map induced by some power $f^k$
has a controlled chain homotopy to the constant map through degrees
less than $n$.
The homotopy is not asserted to be $U$-equivariant.  The same exponent
works on all basis simplices because at each step the induction
assertion applies to every cycle in one bounded complex.

Apply Lemma~\ref{lem:controlled-additivity} to every orthogonal
relation in both finite idempotent systems, enlarging the output
bound once to cover all of them.  For a fixed $n$-cycle $z$, set
\[
 z_E=[(h_Ef^k)_*z]
\]
in the homology of this single bounded output complex.  These classes
satisfy all relations of Lemma~\ref{lem:idempotents}.  The identity
class is the same in both systems, namely
\[
 z_I=[(f^{k+1})_*z].
\]
It is annihilated by both $2$ and $3$, and hence is zero.  The bound
and exponent were chosen before $z$, so the conclusion is uniform
over all cycles of the input bound.  This completes the induction.
\end{proof}

\subsection{Products of regular modules and the HNN sequence}

We now complete the proof of Theorem~\ref{thm:torus}.  Put
$J=T(U,f)$.  Since $f$ is injective, the direct limit of the system
$U\xrightarrow f U\xrightarrow f\cdots$ is an increasing union of
copies of $U$.  Its stage shift is an automorphism, and adjoining
that automorphism gives $J$.  Explicitly, its $i$th copy maps into
$J$ by $u\mapsto t^iut^{-i}$; these maps give the inverse to the
direct-limit description.  In particular $U$ embeds in $J$, and
every element of $J$ has the form $t^p u t^{-q}$ with $p,q\ge0$.

There is a $J$-tree with vertices the left cosets $jU$ and one edge
indexed by $jU$ from $jU$ to $jtU$.  The second endpoint is independent
of the representative because $ut=tf(u)$.  Every vertex has one
outgoing edge, and its height increases by one.  The normal form just
given shows that every forward ray eventually meets the ray from
$U$.  Thus the graph is connected.  An undirected cycle would have a
vertex of least height with two outgoing edges, which is impossible.
It is therefore a tree, with one vertex orbit and one edge orbit,
both having stabilizer $U$.

For any right $\Z J$-module $M$, the tree gives the long exact
homology sequence containing
\begin{equation}\label{eq:ascending-hnn-homology}
 \begin{split}
 H_n(U,M)&\xrightarrow{\,1-F\,}H_n(U,M)
       \longrightarrow H_n(J,M)\\
       &\longrightarrow H_{n-1}(U,M)
          \xrightarrow{\,1-F\,}H_{n-1}(U,M).
 \end{split}
\end{equation}
We specify the chain map and a construction of this sequence.
Induce the homogeneous resolution to obtain
$P_* =\Z J\otimes_{\Z U}C_*(U)$.  On it, the second endpoint map is
\[
 j\otimes c\longmapsto jt\otimes f_*(c).
\]
It is well defined, again because $ut=tf(u)$.  The mapping cone of
the difference of the two endpoint maps resolves $\Z$: first taking
homology of the induced resolutions recovers the augmented cellular
chains of the tree, which are exact.  Tensoring that cone with $M$
gives \eqref{eq:ascending-hnn-homology}.  In the resulting complex
$M\otimes_{\Z U}C_*(U)$, its map $F$ is
\begin{equation}\label{eq:coefficient-shift}
 F(m\otimes c)=mt\otimes f_*(c).
\end{equation}

Take now $M=(\Z J)^{\mathcal I}$ for an arbitrary set $\mathcal I$.
We claim that $F$ is locally nilpotent on $H_i(U,M)$ for every $i>0$.
To interpret chains, let $\mathcal S_q(A)$ be the finite set of
normalized $q$-simplex types with bound $A$.  The freeness of these
types gives
\begin{equation}\label{eq:bounded-product-chains}
 \begin{split}
 M\otimes_{\Z U}C_q^A(U)
 &\cong\bigoplus_{s\in\mathcal S_q(A)} M\\
 &\cong\prod_{\alpha\in\mathcal I}
       \left(\bigoplus_{s\in\mathcal S_q(A)}\Z J\right).
 \end{split}
\end{equation}
The second isomorphism uses finiteness of $\mathcal S_q(A)$.

Every tensor chain involves finitely many simplex types, so lies in
such a bounded complex.  In each coordinate $\alpha$, expand its
$\Z J$ coefficients.  The result is a finite ordinary chain in
tuples contained in left cosets $jU$, with all within-coset differences
in one bound $A$ independent of $\alpha$.  Conversely, any family of
such chains, finite in each coordinate and sharing one bound, defines
a tensor chain by \eqref{eq:bounded-product-chains}.  The number of
terms and the coefficient supports may vary without bound as
$\alpha$ varies.

Let a positive-degree tensor cycle represent a class in $H_i(U,M)$.
In each coordinate its chain splits into finitely many coset chains,
and each is a cycle, because the boundary preserves the coset.
Choose an origin $j$ for each coset.  Formula~\eqref{eq:coefficient-shift}
shows that $F^k$ changes that origin to $jt^k$ and applies $f^k$ to
the relative vertices in $U$.  Proposition~\ref{prop:uniform-fillings}
provides one exponent $k$ and one output bound for all these cycles.
Choose a finite filling in each coordinate and each of its finitely
many cosets.  Their sum remains finite in that coordinate.  Even if
several input cosets have the same output coset, their fillings may
simply be added.  All coordinates still use one common finite set of
output simplex types, so their family is a tensor chain by
\eqref{eq:bounded-product-chains}.  It bounds $F^k$ of the original
cycle.  This proves local nilpotence.

For a locally nilpotent endomorphism, $1-F$ is invertible: its inverse
on any element is the finite geometric sum $1+F+F^2+\cdots$ evaluated
on that element.  The sequence~\eqref{eq:ascending-hnn-homology}
therefore gives
\[
 H_n\bigl(J,(\Z J)^{\mathcal I}\bigr)=0
       \qquad(n\ge2).
\]
No claim about local nilpotence on $H_0$ is needed.  By
Lemma~\ref{lem:torus-presentation}, $J$ is finitely presented.
Lemma~\ref{lem:product-criterion} now proves that it is of type
$\Finfty$, completing the proof of Theorem~\ref{thm:torus}.

\subsection{Finite extensions}

The final passage from pointwise to setwise stabilizers will use the
following closure property.  Its proof reuses the product-module
argument above.

\begin{lemma}\label{lem:finite-extension}
If \(K\) is a normal subgroup of finite index in \(L\) and \(K\) has
type \(\Finfty\), then \(L\) has type \(\Finfty\).
\end{lemma}

\begin{proof}
First \(L\) is finitely presented. Indeed, choose a finite presentation
of \(K\) and representatives of the finite quotient \(L/K\). Add the
representatives as generators, their conjugation relations on the
generators of \(K\), and their multiplication relations modulo \(K\).
These finitely many relations reduce every word to a word in \(K\)
followed by one representative, and give a presentation of \(L\).

Put \(R=\Z L\) and \(A=\Z K\).
The finite-type classifying space for \(K\) gives a free \(A\)-resolution
of \(\Z\) that is finitely generated in each degree. Therefore, for
every index set \(I\),
\[
 H_j\left(K,\prod_I A\right)=0\qquad(j>0):
\]
tensoring that resolution with \(\prod_I A\) gives the product of its
underlying integral chain complexes. Products of exact sequences of
abelian groups are exact.

We construct a degreewise finitely generated free \(R\)-resolution of
\(\Z\). Start with the finite generating set of \(L\), which makes the
augmentation ideal finitely generated. Suppose a partial finite free
resolution has been constructed through degree \(n\geq1\), exact
below that degree. Its restriction to \(A\) is still finite free,
because \([L:K]\) is finite. Complete it arbitrarily to a free
\(R\)-resolution and restrict to \(A\). Index a product of copies of
\(A\) by all cycles in degree \(n\). As in
Lemma~\ref{lem:product-criterion}, this family is one tensor cycle, and
the preceding vanishing supplies a boundary using only finitely many
basis elements \(c_1,\ldots,c_s\) of the next \(A\)-chain module.
For each cycle \(z\), its coordinate equation is
\(z=\sum_{i=1}^s a_i(z)\partial c_i\), with \(a_i(z)\in A\).
Thus these boundaries generate the cycle module over \(A\), hence
also over \(R\); no Noetherian hypothesis is used. This
extends the partial resolution by a finite free \(R\)-module.
Induction completes the construction.

For any product \(\prod_I R\), tensoring this degreewise finite
resolution commutes with the product, so
\(H_j(L,\prod_I R)=0\) for \(j>0\).
The finite presentation already proved and
Lemma~\ref{lem:product-criterion} now give type \(\Finfty\).
\end{proof}

==== END Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem//sections/homological.tex ====

==== BEGIN Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem//sections/introduction.tex ====
\section{Introduction}\label{sec:introduction}

The word problem asks whether a word in a fixed finite generating set
and its inverses represents the identity. A finitely generated group has
\emph{decidable word problem} if an algorithm answers this question for
every word. Embedding theorems connect this algorithmic condition with
the algebraic structure of an overgroup. Higman's embedding theorem
characterizes the finitely generated subgroups of finitely presented
groups as the recursively presented groups: those admitting a
recursively enumerable set of defining relations \citep{Higman1961}.
Boone and Higman obtained the finer characterization
\citep[Theorem~I]{BH74}: a finitely generated group has decidable word
problem if and only if it embeds in a simple group which in turn embeds
in a finitely presented group. They asked whether the simple overgroup
itself can always be finitely presented \citep[p.~43]{BH74}.
This is the Boone--Higman conjecture. Thompson subsequently showed that
the intermediate simple group can be chosen finitely generated with
decidable word problem \citep{Tho80}.

We consider the strengthening that asks for finiteness in every
homotopical dimension. A group \(H\) has \emph{type \(F_n\)} if it admits a
classifying space \(K(H,1)\) with finite \(n\)-skeleton, and has
\emph{type \(\Finfty\)} if it admits such a space with finitely many
cells in each dimension. Here a classifying space is a connected CW
complex with fundamental group \(H\) and contractible universal cover.
Type \(F_1\) is finite generation and type \(F_2\) is finite
presentation. The question of a simple overgroup of type \(\Finfty\)
appears in
the discussion following Question~5.6 of \citet{BBMZsurvey};
Question~5.6 itself asks about overgroups of type \(\Finfty\) for
arbitrary finitely presented groups.

\begin{theorem}\label{thm:main}
Every finitely generated group \(G\) with decidable word problem admits
an injective homomorphism into a nontrivial simple group \(H\) of type
\(\Finfty\).
\end{theorem}

The input need not be finitely presented, and its word-problem
algorithm may have arbitrary running time. The classifying space of
\(H\) may have infinitely many dimensions; type \(\Finfty\) imposes
neither torsion-freeness nor finite cohomological dimension.
The theorem answers the higher-finiteness question positively and in
particular implies the Boone--Higman conjecture.

The classical converse gives an algebraic characterization here as
well \citep{BH74}. A nontrivial finitely presented simple group has
decidable word
problem: in parallel, enumerate consequences of its defining relations
and consequences after adding the input word as a relation. A trivial
input word is detected by the first search; a nontrivial one normally
generates the simple group, so the second search eventually proves all
generators trivial. These outcomes are exclusive because the original
group is nontrivial. Restricting this algorithm along an embedding
solves the word problem in any finitely generated subgroup. Thus the
groups in Theorem~\ref{thm:main} are exactly the finitely generated
subgroups of simple groups of type \(\Finfty\).

\subsection{Earlier embeddings and the higher-finiteness obstacle}

Thompson-type groups have long supplied simple groups with strong
finiteness properties. Brown established type \(\Finfty\) for the
Thompson--Higman families \citep[Section~4]{Brown1987}.
More recently, Belk and Zaremsky constructed a single simple group of
type \(\Finfty\) containing all finitely generated right-angled Artin
groups \citep[Corollary~E]{BelkZaremsky2022}; these are the groups
presented by generators indexed by the vertices of a finite graph,
with commutation relations for its edges. Belk, Hyde and Matucci
constructed a simple group of type \(\Finfty\) containing every
countable abelian group \citep[Theorems~4.4--4.6]{BHMgerms}.
Such results give substantial classes of examples without a general
construction from a word-problem algorithm.

Other recent advances concern the finite-presentation conclusion of
the Boone--Higman conjecture. Belk, Bleak, Matucci and Zaremsky proved
it for hyperbolic groups and contracting self-similar groups
\citep[Theorem~A and Corollary~D]{BBMZhyperbolic}.
Belk, Fournier-Facio, Hyde and Zaremsky proved it for
\(\operatorname{Aut}(F_n)\) and mapping class groups of orientable
punctured surfaces of finite type
\citep[Theorem~A and Corollary~B]{BFFHZ}.
Here \(F_n\) denotes the free group of rank \(n\).
These conclusions do not by themselves give simple overgroups of type
\(\Finfty\). Higher finiteness requires control of additional
relations among relations in every dimension.

Our final step uses the twisted Brin--Thompson construction of
\citet{BelkZaremsky2022}. Its input is a faithful action of a group
\(\Lambda\) on a countably infinite set \(S\). The action must be
\emph{oligomorphic}, meaning that it has finitely many orbits on finite
subsets of each fixed cardinality. If \(\Lambda\) and all its finite-set
stabilizers have type \(\Finfty\), their theorem gives a simple group
\(SV_\Lambda\) of type \(\Finfty\) containing \(\Lambda\).
Consequently the problem is to embed \(G\) in a group equipped with
such an action, including the finiteness properties of its stabilizers.
We construct a \emph{highly transitive} action: any two ordered tuples
of distinct points of the same finite length lie in the same orbit.
This supplies the orbit condition. We prove type \(\Finfty\) for the
pointwise stabilizers; the corresponding setwise stabilizers are
finite extensions and inherit the property.

The stabilizer requirement is a genuine restriction on the choice of
acting group. Fournier-Facio, Kropholler, Lyman and Zaremsky prove that
an oligomorphic action on an infinite set of a group of finite virtual
cohomological dimension, or of a countable group linear over a field,
always has a finite-set stabilizer which is not of type \(\Finfty\)
\citep[Theorem~1.1]{FFKLZstabilizers}.
The construction below therefore builds the overgroup and its
stabilizers together; it does not ask the original group to possess
an action with these properties.

\subsection{Constructing the action and proving finiteness}

The action begins with a finitely presented ring \(B\), the elementary
matrix group \(Q=\E_7(B)\), and its action on the column set \(X=B^7\).
Here \(\E_r(B)\) is generated by the off-diagonal elementary matrices.
We construct compatible injections
\[
 \delta:Q\longrightarrow Q,\qquad \sigma:X\longrightarrow X.
\]
At each new stage, matrices can permute any finite collection of the
compressed columns \(\sigma(X)\). The direct limits of these two
systems, with the stage shift adjoined to the group, give the action
\(\Lambda\curvearrowright S\). This makes high transitivity a local
matrix calculation. The same construction embeds \(G\) into \(Q\).

The ring has to encode more than the given group. Its units must also
encode prescribed enlargements of the action of \(\E_7(B)\) on
\(B^7\), so the objects being encoded already involve the ring being
constructed. We resolve this self-reference by a length induction.
A finite compiler from the companion article
\emph{Finite algebraic envelopes and the Boone--Higman conjecture}
\citep{FoundationsCompanion} gives equality calculations at each finite
bound when its stated hypotheses hold. The encoding ensures that every recursive call uses
a strictly smaller bound. Kleene's recursion theorem first supplies the
program, and the length induction then proves its totality and
compatibility with multiplication. The companion also supplies a
binary corner construction and a Steinberg-kernel annihilation theorem;
their exact statements appear where they are used.

Finiteness is supplied by a separate ascending-torus criterion.
For an injective endomorphism \(f:U\to U\), write
\[
 T(U,f)=\langle U,t\mid t^{-1}ut=f(u)\ \text{for }u\in U\rangle.
\]
A factorization of \(f\) through a finitely presented group gives a
finite presentation of \(T(U,f)\). To obtain higher finiteness, we use
two finite systems of homomorphisms whose images commute in specified
pairs. Their product identities come from orthogonal idempotents over
\(\F_2\) and \(\F_3\). After lower-dimensional terms have been killed,
commuting products act additively on homology. The two systems then
force the same class to be annihilated by both \(2\) and \(3\).

The essential point is uniformity. We use simplices whose vertices are
elements of \(U\), and regard two simplices as having the same type
when they differ by a simultaneous left translation. One iterate and
one finite set of output types work for every cycle using a given
finite set of input types. Chain lengths and coefficients may be
arbitrarily large. This control allows fillings with coefficients in
products of copies of the group ring, and the Bieri--Eckmann finiteness
method then gives finite skeleta in every dimension. The result is
Theorem~\ref{thm:torus}.

The acting group and each finite-point stabilizer are themselves
ascending tori to which this same criterion applies. For stabilizers,
the defining endomorphism factors through a finitely presented
Steinberg group. The second factor sends the \emph{entire} Steinberg
group into the stabilizer, not merely the image of the first factor.
The commuting diagrams preserve the fixed points as well. These two
properties establish type \(\Finfty\) for all stabilizers and complete
the input to the twisted Brin--Thompson theorem.

\subsection{Organization and conventions}

Section~\ref{sec:homological} proves the ascending-torus criterion.
Section~\ref{sec:encoding} constructs the ring and the encoded actions.
Section~\ref{sec:stage} constructs \(\Lambda\curvearrowright S\) and
proves the stabilizer theorem. Section~\ref{sec:simple} applies the
twisted Brin--Thompson theorem and proves Theorem~\ref{thm:main}.

All rings used for matrices are unital and associative. Ring embeddings
and endomorphisms need not preserve the identity when this is expressly
stated. All homology is integral. Group actions are on the left;
coefficient modules for group homology are right modules.
==== END Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem//sections/introduction.tex ====

==== BEGIN Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem//sections/stage.tex ====
\section{A highly transitive action with finite-type stabilizers}
\label{sec:stage}

We strengthen the embedding problem to a statement about an action and
all its finite-point stabilizers.

\begin{theorem}\label{thm:action}
For every finitely generated group $G$ with decidable word problem,
there is a group $\Lambda$ containing $G$ and acting faithfully on a
countably infinite set $S$ such that:
\begin{enumerate}[label=\textup{(\roman*)}]
 \item the action is transitive on ordered tuples of distinct points
 of every finite length;
 \item $\Lambda$ and every pointwise stabilizer of a finite tuple
 are of type $\Finfty$.
\end{enumerate}
\end{theorem}

The action will be obtained by iterating an embedding of a group and its
set of columns.  Finite permutations become available after one
transition, giving high transitivity in the limit.  We then identify each
finite-point stabilizer as an ascending torus and verify the two
hypotheses of Theorem~\ref{thm:torus}: commuting splittings and a
factorization through a finitely presented group.

\subsection{Ring data and compressed diagonal matrices}

Apply Theorem~\ref{thm:ring-data} to the given finitely generated group
$G$ with decidable word problem.  Throughout this section, retain its
ring $B$, injective additive multiplicative map $\phi$, idempotent
$p=\phi(1)$, and centralizing binary pairs $s_i,d_i\in pBp$:
\begin{equation}\label{eq:stage-binary}
 d_i s_j=\delta_{ij}p,
 \qquad s_0d_0+s_1d_1=p.
\end{equation}
In particular, $\phi$ need not preserve the identity.  Also retain the
nonzero corner $eBe$, its embedded groups $G$ and $W$, and its elements
$S_y,T_y$ for $y\in Y$.  Write
\[
 Q=\E_7(B),\qquad X=B^7,
\]
and let
$\iota:Q\hookrightarrow W$ and $\iota_X:X\hookrightarrow Y$
be the equivariant embeddings of Theorem~\ref{thm:ring-data}.
For $x\in X$ we abbreviate
$S_{\iota_X(x)}$ and $T_{\iota_X(x)}$ to $S_x$ and $T_x$.

The first use of the binary corner is to turn a unit of $B$ into an
elementary matrix supported in one coordinate.  This will let us encode
both the action of $W$ and finite permutations of its indexed prefixes
inside $Q$.

For a unit $v\in B^\times$, denote by $D_j(v)$ the diagonal matrix
with entry $v$ in position $j$ and identity entries elsewhere; its size
will always be specified by the surrounding group.  Write
$e_{ij}(b)=I+b\mathbf e_{ij}$ for an elementary matrix, where
$\mathbf e_{ij}$ is a matrix unit.

\begin{lemma}\label{lem:diagonal}
For every $r\ge2$ and $v\in B^\times$,
\[
 D_1\bigl(1+\phi(v-1)\bigr)\in\E_r(B).
\]
\end{lemma}

\begin{proof}
Let $\operatorname{GE}_r(B)$ be the subgroup of $\GL_r(B)$ generated
by elementary matrices and invertible diagonal matrices.  Conjugation
by a diagonal matrix preserves the elementary subgroup, so
$\E_r(B)$ is normal in $\operatorname{GE}_r(B)$.  The quotient is
abelian, even though $B$ need not be commutative.  Indeed, in a
two-coordinate block,
\[
 w(v):=e_{12}(v)e_{21}(-v^{-1})e_{12}(v)
   =\begin{pmatrix}0&v\\-v^{-1}&0\end{pmatrix},
 \qquad
 w(v)w(-1)=\begin{pmatrix}v&0\\0&v^{-1}\end{pmatrix}.
\]
Thus $D_i(v)$ and $D_j(v)$ have the same class modulo $\E_r(B)$.
Classes of one-place diagonals commute because they can be represented
in distinct positions.  These classes generate the quotient.

Set
\[
 E_i=s_i d_i\quad(i=0,1),
 \qquad
 E_{00}=s_0s_0d_0d_0,
 \qquad
 E_{01}=s_0s_1d_1d_0.
\]
The binary relations give orthogonal decompositions
\begin{equation}\label{eq:stage-four-corners}
 p=E_0+E_1,
 \qquad E_0=E_{00}+E_{01}.
\end{equation}
All these idempotents commute with $\phi(B)$.

Each of $E_0,E_{00},E_{01}$ is orthogonal to and equivalent to $E_1$,
with implementing elements that commute with $\phi(B)$.  Here are
explicit implementing elements.  Put
\[
 s_{00}=s_0s_0,\quad d_{00}=d_0d_0,
 \qquad
 s_{01}=s_0s_1,\quad d_{01}=d_1d_0.
\]
For $v\in\{0,00,01\}$, define
$a_v=s_1d_v$ and $b_v=s_vd_1$.  Then
\[
 a_vb_v=E_1,\qquad b_va_v=E_v,
 \qquad
 \tau_v=1-E_v-E_1+a_v+b_v
\]
satisfies $\tau_v^2=1$ and $\tau_vE_v\tau_v^{-1}=E_1$.
It also commutes with $\phi(B)$.

Fix a unit $u\in B^\times$.  For any of these idempotents $E$,
the element $1+\phi(u-1)E$ is a unit, with inverse
$1+\phi(u^{-1}-1)E$.  Conjugating by $\tau_v$ shows that the
one-place diagonals belonging to $E_v$ and $E_1$ have equal classes
in the abelian quotient $\operatorname{GE}_r(B)/\E_r(B)$.
Let $c$ be the common class for $E_0,E_1,E_{00},E_{01}$.
The second orthogonal split in
Equation~\eqref{eq:stage-four-corners} gives $c=c^2$, hence $c=1$.
The first split then shows that
$D_1(1+\phi(u-1)p)$ is elementary.  Since
$\phi(u-1)p=\phi(u-1)$, this is the asserted matrix.
\end{proof}

\subsection{The transition of acting pairs}

The corner embedding of $W$ defines an injective homomorphism
\[
 \rho:W\hookrightarrow B^\times,
 \qquad \rho(w)=1-e+w.
\]
Indeed, its inverse-unit formula is
$\rho(w)^{-1}=1-e+w^{-1}$, and multiplication is the multiplication
in $eBe$ together with the identity on $1-e$.
Write $\phi^2=\phi\circ\phi$ and define
\begin{align}
 \mu(w)&=D_1\bigl(1+\phi^2(\rho(w)-1)\bigr)
        \in Q,\label{eq:stage-mu}\\
 \beta(y)&=\bigl(\phi^2(S_y),0,\ldots,0\bigr)^{\mathsf T}
        \in X.\label{eq:stage-beta}
\end{align}
Membership of $\mu(w)$ in $Q$ follows from
Lemma~\ref{lem:diagonal}, applied twice.  Expanding a product shows
that $v\mapsto1+\phi(v-1)$ is a homomorphism on units, and it is
injective because $\phi$ is injective.  Together with the injectivity
of $\rho$, this proves that $\mu$ is an injective homomorphism.

The prefix relations show that $\beta$ is injective.  If $y\ne z$
and $S_y=S_z$, multiplication by $T_y$ would give $e=0$;
injectivity of $\phi^2$ preserves the resulting distinction.
They also give equivariance, since
\begin{align*}
 \bigl(1+\phi^2(w-e)\bigr)\phi^2(S_y)
  &=\phi^2(S_y)+\phi^2\bigl((w-e)S_y\bigr)\\
  &=\phi^2(wS_y)
   =\phi^2(S_{wy}).
\end{align*}
We thus obtain an injective transition of acting pairs
\begin{equation}\label{eq:stage-transition}
 \delta=\mu\iota:Q\hookrightarrow Q,
 \qquad
 \sigma=\beta\iota_X:X\hookrightarrow X.
\end{equation}
The same compressed-diagonal construction, applied to the corner
copy of $G$, gives an embedding $G\hookrightarrow Q$.

\begin{lemma}\label{lem:stage-permutations}
Every permutation of $\sigma(X)$ with finite support is induced
on that set by an element of $Q$.
\end{lemma}

\begin{proof}
Let $F\subseteq X$ be finite, and let $\eta$ be a permutation of
$F$.  Put
\[
 v=1-\sum_{x\in F}S_xT_x
      +\sum_{x\in F}S_{\eta(x)}T_x.
\]
The elements $S_xT_x$ are pairwise orthogonal idempotents.  The
relations $T_xS_y=\delta_{xy}e$ show directly that $v$ is a unit,
with inverse obtained by replacing $\eta$ by $\eta^{-1}$.
Moreover,
\[
 vS_x=S_{\eta(x)}\quad(x\in F),
 \qquad vS_x=S_x\quad(x\in X\setminus F).
\]
The matrix $D_1(1+\phi^2(v-1))$ lies in $Q$ by
Lemma~\ref{lem:diagonal}, and acts on $\sigma(X)$ as required.
\end{proof}

\subsection{The limit group and its action}

Let
\[
 N=\varinjlim(Q,\delta),
 \qquad S=\varinjlim(X,\sigma).
\]
Write $q_i$ for the element of $N$ represented by $q\in Q$ at
stage $i$, and $[x,i]$ for a point of $S$ represented by $x\in X$.
Thus
\[
 q_i=\delta(q)_{i+1},
 \qquad [x,i]=[\sigma(x),i+1].
\]
The maps in both direct systems are injective.  Hence their stages
may be identified with increasing subgroups $Q_i\le N$ and
increasing subsets $X_i\subseteq S$.
Equivariance in Equation~\eqref{eq:stage-transition} defines an
action of $N$ on $S$: for $k\ge i,j$,
\begin{equation}\label{eq:stage-limit-action}
 q_i[x,j]=
 \bigl[\delta^{k-i}(q)\sigma^{k-j}(x),k\bigr].
\end{equation}
Passing to a larger common stage leaves this expression unchanged.

The shift $\tau(q_i)=q_{i+1}$ is an automorphism of $N$, with
inverse $\tau^{-1}(q_i)=\delta(q)_i$.  Similarly the bijection
\[
 t[x,i]=[x,i+1]
\]
of $S$ has inverse $[x,i]\mapsto[\sigma(x),i]$.
Equation~\eqref{eq:stage-limit-action} implies that this bijection
conjugates the action of $n\in N$ to that of $\tau(n)$.
It therefore extends the action to
\[
 \Lambda=N\rtimes_{\tau}\langle t\rangle.
\]
Identifying $Q$ with $Q_0$, its defining relation is
\begin{equation}\label{eq:stage-torus}
 t^{-1}qt=\delta(q)\qquad(q\in Q).
\end{equation}
In particular, $\Lambda$ is the ascending torus of $\delta$.
For completeness, the inverse map from the direct-limit description
to the group with this presentation sends $q_i$ to $t^iqt^{-i}$.
Equation~\eqref{eq:stage-torus} makes this well defined and gives
the two inverse homomorphisms.

\begin{lemma}\label{lem:stage-faithful-transitive}
The set $S$ is countably infinite.  The action of $\Lambda$ on $S$
is faithful and transitive on ordered tuples of distinct points
of every finite length.
\end{lemma}

\begin{proof}
The finitely generated ring $B$ is countable, so $X$ and $S$ are
countable.  The ring is infinite: iterating the binary relations
in Equation~\eqref{eq:stage-binary} produces, for every $m$, a
family of $2^m$ pairwise orthogonal nonzero idempotents in $pBp$.
They are nonzero because the corresponding deletion-prefix products
are $p\ne0$.  Thus $X$, and consequently $S$, is infinite.

The action of $N$ is faithful.  Indeed, a nonidentity element of
$N$ is represented by a nonidentity matrix in some stage $Q_i$.
Such a matrix moves one of the standard basis columns in that stage,
and injectivity of the point maps preserves the distinction in $S$.

Every element of $N$ preserves $X_j$ setwise for all sufficiently
large $j$: its action at any such stage is by an invertible matrix.
In contrast, $tX_j=X_{j+1}$, and every stage inclusion is strict.
To see strictness, note that $\sigma(X)$ has zero coordinates
outside position 1, whereas the column with identity in position 2
does not.  Thus, for $k\ne0$ and sufficiently large $j$,
$t^kX_j=X_{j+k}\ne X_j$.  No nonzero power of $t$ acts as an
element of $N$.  If an element $nt^k\in\Lambda$ acts trivially,
this observation forces $k=0$, and faithfulness for $N$ then forces
$n=1$.

Given two ordered tuples of distinct points of the same finite
length, place them in a common stage $X_i$.  Their images in the
next stage lie in $\sigma(X)$.  The prescribed bijection between
their entries extends to a finitely supported permutation of
$\sigma(X)$.
Lemma~\ref{lem:stage-permutations} supplies the required element
of $Q_{i+1}$.  This proves the asserted transitivity.
\end{proof}

\subsection{Pointwise stabilizers as ascending tori}

Fix a nonnegative integer $m$.  By
Lemma~\ref{lem:stage-faithful-transitive}, it suffices to prove the
finiteness assertion for one ordered tuple $z=(z_1,\ldots,z_m)$
of distinct points with every $z_j\in\sigma(X)\subseteq X$.
When $m=0$ the tuple is empty and its stabilizer is all of
$\Lambda$.  Since both $z$ and $\sigma(z)$ have entries in
$\sigma(X)$, Lemma~\ref{lem:stage-permutations} gives $a\in Q$
such that
\begin{equation}\label{eq:stage-align}
 a\sigma(z)=z.
\end{equation}
For the empty tuple, take $a=1$.
Put
\[
 U=Q_{(z)},\qquad t'=ta^{-1}.
\]
The subscript denotes pointwise stabilization.  In our convention
for the limit action,
\[
 t'[z,0]=[a^{-1}z,1]=[\sigma(z),1]=[z,0],
\]
so $t'$ fixes the tuple.  Furthermore,
\begin{equation}\label{eq:stage-stabilizer-map}
 (t')^{-1}qt'=a\delta(q)a^{-1},
 \qquad
 f:U\longrightarrow U,
 \quad f(u)=a\delta(u)a^{-1}.
\end{equation}
The codomain in this formula follows either from the fact that $t'$
fixes the tuple or directly from equivariance and
Equation~\eqref{eq:stage-align}.  The map $f$ is injective.

\begin{lemma}\label{lem:stage-stabilizer-torus}
The pointwise stabilizer $\Lambda_{([z,0])}$ is the ascending torus
of $U$ under $f$.
\end{lemma}

\begin{proof}
The height homomorphism $\Lambda\to\Z$ sends $Q$ to zero and
$t'$ to one.  Its kernel is $N$.  For every $i\ge0$ there is
$b_i\in Q$ such that $(t')^i=t^i b_i$: this follows inductively
from $qt=t\delta(q)$.  Hence
\[
 (t')^iQ(t')^{-i}=t^iQt^{-i}=Q_i,
 \qquad N=\bigcup_{i\ge0}(t')^iQ(t')^{-i}.
\]
Since $t'$ fixes the tuple,
\[
 N\cap\Lambda_{([z,0])}
   =\bigcup_{i\ge0}(t')^iU(t')^{-i}.
\]
An element of the full stabilizer of height $k$, multiplied by
$(t')^{-k}$, belongs to this height-zero subgroup.  Thus the full
stabilizer is its semidirect product with $\langle t'\rangle$.
The conjugation formula in
Equation~\eqref{eq:stage-stabilizer-map} identifies this group
with the ascending torus of $f$.
\end{proof}

The two diagram systems required by Theorem~\ref{thm:torus}
also restrict to $U$.  Let
$j_{\ell,E}:Q\to W$ be the maps of
Theorem~\ref{thm:ring-data}, for $\ell=2,3$ and
$E\in\mathcal P_\ell$, with common full-identity map $\iota$.
Define
\begin{equation}\label{eq:stage-stabilizer-diagrams}
 h_{\ell,E}:U\longrightarrow U,
 \qquad
 h_{\ell,E}(u)=a\mu(j_{\ell,E}(u))a^{-1}.
\end{equation}
These maps do have their entire images in $U$.  If $u$ fixes $z_j$,
the fixed-point property of the enlargement says that
$j_{\ell,E}(u)$ fixes $\iota_X(z_j)$.  Equivariance of $\beta$
then says that $\mu(j_{\ell,E}(u))$ fixes $\sigma(z_j)$;
conjugation by $a$ gives the claim.  The maps are homomorphisms,
$h_{\ell,I}=f$, and they preserve each orthogonal-sum identity
and each required elementwise commutation relation, since $\mu$
and conjugation by $a$ are homomorphisms.

We have now identified the stabilizer as an ascending torus and supplied
its commuting splittings.  The remaining hypothesis of
Theorem~\ref{thm:torus} is a factorization of $f$ through a finitely
presented group.  We will use $\St_6(B)$ as that group.  A six-coordinate
elementary block inside $Q=\E_7(B)$ fixes every vector supported in the
first coordinate, so its entire image fixes $\sigma(z)$.  Two steps are
needed: lift the compressed units homomorphically to $\St_6(B)$, then
move their nonidentity part from coordinate 1 into that block without
moving the marked columns.

\subsection{A homomorphic Steinberg lift}

For a unital ring $R$, the Steinberg group $\St_6(R)$ has generators
$x_{ij}(a)$ for $i\ne j$ and $a\in R$, with the relations
\begin{align*}
 x_{ij}(a)x_{ij}(b)&=x_{ij}(a+b),\\
 [x_{ij}(a),x_{jk}(b)]&=x_{ik}(ab)
       &&\text{if }i,j,k\text{ are distinct},\\
 [x_{ij}(a),x_{kl}(b)]&=1
       &&\text{if }i\ne l\text{ and }j\ne k.
\end{align*}
We use the convention $[u,v]=uvu^{-1}v^{-1}$.
The map sending $x_{ij}(a)$ to $e_{ij}(a)$ is a surjection
$\pi:\St_6(R)\twoheadrightarrow\E_6(R)$.

We need the following precise form of the kernel-annihilation theorem
from \citet[Theorem~4.1]
{FoundationsCompanion}.

\begin{theorem}[Kernel annihilation]\label{thm:stage-kernel}
Let $R$ be a unital associative ring and let $\psi:R\to R$ be an
additive multiplicative map.  Put $P=\psi(1)$.  Suppose that
$U_0,U_1,V_0,V_1\in PRP$ commute with $\psi(R)$ and satisfy
\[
 V_iU_j=\delta_{ij}P,
 \qquad U_0V_0+U_1V_1=P.
\]
Then the homomorphism
\[
 \theta:\St_6(R)\longrightarrow\St_6(R),
 \qquad x_{ij}(a)\longmapsto x_{ij}(\psi(a)),
\]
annihilates the kernel of $\pi$.
\end{theorem}

The theorem permits nonunital $\psi$ and noncommutative $R$.
For such a coefficient map the matrix of the image of a root word
with matrix $g$ is
\begin{equation}\label{eq:stage-nonunital-matrix}
 I+\psi^{(6)}(g-I),
\end{equation}
where $\psi^{(6)}$ means entrywise application.  This follows first
on elementary matrices and then on products from
$gh-I=(g-I)+(h-I)+(g-I)(h-I)$.

\begin{lemma}\label{lem:steinberg-lift}
There is a homomorphism
$L:B^\times\to\St_6(B)$ such that
\begin{equation}\label{eq:stage-lift}
 \pi L(v)=D_1\bigl(1+\phi^2(v-1)\bigr).
\end{equation}
Moreover, $\St_6(B)$ is finitely presented.
\end{lemma}

\begin{proof}
Apply Theorem~\ref{thm:stage-kernel} with
\[
 R=B,\quad \psi=\phi,\quad P=p,
 \quad U_i=s_i,\quad V_i=d_i.
\]
Its hypotheses are precisely the support, commutation, and binary
relations in Theorem~\ref{thm:ring-data}.
Consequently its coefficient map factors as a homomorphism
\[
 \lambda:\E_6(B)\longrightarrow\St_6(B),
 \qquad \lambda(\pi(s))=\theta(s).
\]
The definition is independent of the choice of $s$ because $\theta$
kills $\ker\pi$.  By
Equation~\eqref{eq:stage-nonunital-matrix},
\[
 \pi\lambda(g)=I+\phi^{(6)}(g-I).
\]

The homomorphism on units used to define $\mu$, together with
Lemma~\ref{lem:diagonal}, supplies a homomorphism
\[
 A:B^\times\longrightarrow\E_6(B),
 \qquad A(v)=D_1\bigl(1+\phi(v-1)\bigr).
\]
Take $L=\lambda A$.  The displayed formula for $\pi\lambda$ gives
Equation~\eqref{eq:stage-lift}.

Finally, Lemma~\ref{lem:encoding-finite-presentation} proves that $B$
is finitely presented as a unital associative ring: to its finite
$\F_2$-algebra presentation one adds $2\cdot1=0$ over $\Z$.
Theorem~3 of
\citet{KrsticMcCool1999} states that $\St_n(R)$ is finitely
presented for every finitely presented unital associative ring $R$
and every $n\ge4$.  It allows noncommutative rings and applies with
$R=B$ and $n=6$.
\end{proof}

\subsection{Factoring the stabilizer endomorphism}

The tuple $\sigma(z)$ is supported in coordinate 1, as is the
nonidentity part of $\delta(U)$.  An ordinary exchange of coordinates
1 and 2 would move the tuple.  Instead we exchange only the idempotent
part on which those nonidentity increments are supported; this part
annihilates the marked columns.  The resulting factorization sends the
whole intermediate Steinberg group into $U$.

\begin{lemma}\label{lem:stage-stabilizer-factor}
The endomorphism $f$ in
Equation~\eqref{eq:stage-stabilizer-map} factors through
$\St_6(B)$ by homomorphisms
\[
 U\xrightarrow{\alpha}\St_6(B)\xrightarrow{b}U.
\]
\end{lemma}

\begin{proof}
For the fixed tuple $z$, put
\begin{equation}\label{eq:stage-d}
 q_j=\phi^2(S_{z_j}T_{z_j}),
 \qquad d=1-\sum_{j=1}^m q_j,
 \qquad c=1-d.
\end{equation}
The prefix relations make the $q_j$ pairwise orthogonal
idempotents, so $d$ is an idempotent.  It depends only on $z$.

For $u\in U$, write $w=\iota(u)$ and
\[
 r=\phi^2(\rho(w)-1)=\phi^2(w-e),
 \qquad v'=1+r.
\]
Then $\delta(u)=D_1(v')$.  The element $w$ fixes each index
$\iota_X(z_j)$, so both prefix equations give
\[
 (w-e)S_{z_j}=0,
 \qquad T_{z_j}(w-e)=0.
\]
Consequently $rq_j=q_jr=0$ and
\begin{equation}\label{eq:stage-support}
 dr=rd=r.
\end{equation}
Also, using $T_{z_i}S_{z_j}=\delta_{ij}e$,
\begin{equation}\label{eq:stage-fixed-columns}
 d\phi^2(S_{z_j})
  =\phi^2(S_{z_j})
       -\sum_{i=1}^m\phi^2(S_{z_i}T_{z_i}S_{z_j})=0.
\end{equation}
These identities use only additivity and multiplicativity of $\phi$;
no identity-preservation assumption is needed.

In coordinates 1 and 2 of $B^7$, let
\[
 E=e_{12}(d)e_{21}(-d)e_{12}(d)
   =\begin{pmatrix}c&d\\-d&c\end{pmatrix},
 \qquad
 E^{-1}=\begin{pmatrix}c&-d\\d&c\end{pmatrix},
\]
with identity entries on all other coordinates.  This is an element
of $Q$.  Equation~\eqref{eq:stage-fixed-columns} shows that both
$E$ and $E^{-1}$ fix every column $\sigma(z_j)$.  Direct
multiplication, using Equation~\eqref{eq:stage-support}, gives
\begin{equation}\label{eq:stage-exchange}
 E D_1(v')E^{-1}=D_2(v').
\end{equation}
In particular, the signed exchange leaves no sign or inversion on
the moved unit.

Let $L$ be the homomorphism of Lemma~\ref{lem:steinberg-lift},
and define
\begin{equation}\label{eq:stage-alpha}
 \alpha(u)=L(\rho(\iota(u))).
\end{equation}
By Equation~\eqref{eq:stage-lift}, its matrix projection, placed
in coordinates 2 through 7, is $D_2(v')$.  In particular, the
argument of $L$ here is the original unit $\rho(w)$; the two
applications of $\phi$ are already included in the defining
property of $L$.

For every $s\in\St_6(B)$, define
\begin{equation}\label{eq:stage-b}
 b(s)=aE^{-1}\diag(1,\pi(s))Ea^{-1}.
\end{equation}
This is a homomorphism to $Q$, because embedding the elementary
six-coordinate block in coordinates 2 through 7 gives an elementary
seven-coordinate matrix.  Its entire image lies in $U$: the
matrix $\diag(1,\pi(s))$ fixes every first-coordinate vector
$\sigma(z_j)$, the matrices $E^{\pm1}$ do so as well, and
$a\sigma(z)=z$.  Finally,
\[
 b(\alpha(u))
   =aE^{-1}D_2(v')Ea^{-1}
   =aD_1(v')a^{-1}
   =f(u).
\]
This proves the factorization.  For $m=0$, the sums in
Equation~\eqref{eq:stage-d} are empty and $d=1$; all the same
formulas apply.

The codomains can be seen in the commutative diagram
\[
\begin{tikzcd}[column sep=large,row sep=large]
 U \arrow[r,"\alpha"] \arrow[d,"f"']
   & \St_6(B) \arrow[d,"{\diag(1,\pi(-))}"] \\
 U
   & Q_{(\sigma(z))} \arrow[l,"c_{aE^{-1}}"']
\end{tikzcd}
\]
where $c_g$ denotes conjugation by $g$. The lower right group is
the entire pointwise stabilizer of $\sigma(z)$ in $Q$.
The right arrow lands there because it leaves the first coordinate
unchanged; the lower arrow lands in $U$ because $E$ fixes
$\sigma(z)$ and $a\sigma(z)=z$.
\end{proof}

\begin{proof}[Proof of Theorem~\ref{thm:action}]
The embedding $G\hookrightarrow Q\hookrightarrow\Lambda$ was
constructed above, and
Lemma~\ref{lem:stage-faithful-transitive} proves the assertions
about the action.  For a tuple $z$ chosen as above,
Lemma~\ref{lem:stage-stabilizer-torus} identifies its pointwise
stabilizer with the ascending torus of the injective endomorphism
$f:U\to U$.  The diagrams in
Equation~\eqref{eq:stage-stabilizer-diagrams} satisfy the two
orthogonal-splitting hypotheses of Theorem~\ref{thm:torus}.
Lemma~\ref{lem:stage-stabilizer-factor}, together with finite
presentation in Lemma~\ref{lem:steinberg-lift}, supplies its other
hypothesis.  Thus this stabilizer has type $\Finfty$.
High transitivity conjugates every tuple of distinct points to one
of this form.  Repeated entries do not change a pointwise
stabilizer, and the empty tuple gives $\Lambda$ itself.  This
proves all the claims.
\end{proof}
==== END Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem//sections/stage.tex ====

==== BEGIN Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem//references.bib ====
@article{BH74,
  author = {Boone, William W. and Higman, Graham},
  title = {An algebraic characterization of groups with soluble word problem},
  journal = {Journal of the Australian Mathematical Society},
  volume = {18},
  number = {1},
  year = {1974},
  pages = {41--53},
  doi = {10.1017/S1446788700019108}
}

@misc{BBMZsurvey,
  author = {Belk, James and Bleak, Collin and Matucci, Francesco and
            Zaremsky, Matthew C. B.},
  title = {Progress around the {Boone--Higman} conjecture},
  year = {2025},
  eprint = {2306.16356},
  archivePrefix = {arXiv},
  primaryClass = {math.GR},
  note = {Version 3, 22 May 2025},
  url = {https://arxiv.org/abs/2306.16356v3}
}

@misc{FoundationsCompanion,
  author = {{OpenAI}},
  title = {{Finite algebraic envelopes and the Boone--Higman conjecture}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Finite-algebraic-envelopes-and-the-Boone-Higman-conjecture-September-23-2026/paper.pdf}{OAI:Finite-algebraic-envelopes-and-the-Boone-Higman-conjecture-September-23-2026}},
  year = {2026}
}

@article{BelkZaremsky2022,
  author = {Belk, James and Zaremsky, Matthew C. B.},
  title = {Twisted {Brin--Thompson} groups},
  journal = {Geometry \& Topology},
  volume = {26},
  number = {3},
  year = {2022},
  pages = {1189--1223},
  doi = {10.2140/gt.2022.26.1189},
  url = {https://eprints.gla.ac.uk/280398/1/280398.pdf}
}

@article{KrsticMcCool1999,
  author = {Krsti{\'c}, Sava and McCool, James},
  title = {Presenting {$\mathrm{GL}_n(k\langle T\rangle)$}},
  journal = {Journal of Pure and Applied Algebra},
  volume = {141},
  number = {2},
  year = {1999},
  pages = {175--183},
  doi = {10.1016/S0022-4049(98)00022-X}
}

@article{Kleene38,
  author = {Kleene, S. C.},
  title = {On notation for ordinal numbers},
  journal = {The Journal of Symbolic Logic},
  volume = {3},
  number = {4},
  year = {1938},
  pages = {150--155},
  doi = {10.2307/2267778}
}

@article{Newman42,
  author = {Newman, M. H. A.},
  title = {On theories with a combinatorial definition of "equivalence"},
  journal = {Annals of Mathematics},
  series = {2},
  volume = {43},
  number = {2},
  year = {1942},
  pages = {223--243},
  doi = {10.2307/1968867}
}

@article{BieriEckmann1974,
  author = {Bieri, Robert and Eckmann, Beno},
  title = {Finiteness properties of duality groups},
  journal = {Commentarii Mathematici Helvetici},
  volume = {49},
  year = {1974},
  pages = {74--83},
  doi = {10.1007/BF02566720}
}

@article{Brown1975,
  author = {Brown, Kenneth S.},
  title = {Homological criteria for finiteness},
  journal = {Commentarii Mathematici Helvetici},
  volume = {50},
  year = {1975},
  pages = {129--135},
  doi = {10.1007/BF02565740}
}

@article{EilenbergZilber1953,
  author = {Eilenberg, Samuel and Zilber, J. A.},
  title = {On products of complexes},
  journal = {American Journal of Mathematics},
  volume = {75},
  number = {1},
  year = {1953},
  pages = {200--204},
  doi = {10.2307/2372629}
}

@book{Hatcher2002,
  author = {Hatcher, Allen},
  title = {Algebraic Topology},
  publisher = {Cambridge University Press},
  year = {2002},
  note = {Author's corrected electronic version},
  url = {https://pi.math.cornell.edu/~hatcher/AT/ATpage.html}
}

@incollection{Tho80,
  author = {Thompson, Richard J.},
  title = {Embeddings into finitely generated simple groups which preserve the word problem},
  booktitle = {Word Problems II},
  editor = {Adian, S. I. and Boone, W. W. and Higman, G.},
  series = {Studies in Logic and the Foundations of Mathematics},
  volume = {95}, publisher = {North-Holland}, year = {1980}, pages = {401--441},
  doi = {10.1016/S0049-237X(08)71348-X}
}

@article{BBMZhyperbolic,
  author = {Belk, James and Bleak, Collin and Matucci, Francesco and Zaremsky, Matthew C. B.},
  title = {Hyperbolic groups satisfy the {Boone--Higman} conjecture},
  journal = {Duke Mathematical Journal},
  volume = {175}, number = {9}, year = {2026}, pages = {1519--1592},
  doi = {10.1215/00127094-2025-0055},
  url = {https://arxiv.org/abs/2309.06224v3}
}

@misc{BFFHZ,
  author = {Belk, James and Fournier-Facio, Francesco and Hyde, James and Zaremsky, Matthew C. B.},
  title = {{Boone--Higman} embeddings of {$\mathrm{Aut}(F_n)$} and mapping class groups of punctured surfaces},
  year = {2026}, eprint = {2503.21882}, archivePrefix = {arXiv}, primaryClass = {math.GR},
  note = {Version 3, 17 September 2026. To appear in Proceedings of the London Mathematical Society},
  url = {https://arxiv.org/abs/2503.21882v3}
}

@article{Higman1961,
  author = {Higman, Graham},
  title = {Subgroups of finitely presented groups},
  journal = {Proceedings of the Royal Society of London. Series A},
  volume = {262}, number = {1311}, year = {1961}, pages = {455--475},
  doi = {10.1098/rspa.1961.0132}
}

@article{Brown1987,
  author = {Brown, Kenneth S.},
  title = {Finiteness properties of groups},
  journal = {Journal of Pure and Applied Algebra},
  volume = {44}, number = {1--3}, year = {1987}, pages = {45--75},
  doi = {10.1016/0022-4049(87)90015-6}
}

@misc{BHMgerms,
  author = {Belk, James and Hyde, James and Matucci, Francesco},
  title = {Finite germ extensions},
  year = {2024}, eprint = {2407.03149}, archivePrefix = {arXiv},
  primaryClass = {math.GR}, note = {Version 1, 3 July 2024},
  url = {https://arxiv.org/abs/2407.03149v1}
}

@misc{FFKLZstabilizers,
  author = {Fournier-Facio, Francesco and Kropholler, Peter H. and
            Lyman, Robert Alonzo and Zaremsky, Matthew C. B.},
  title = {Finiteness properties of stabilisers of oligomorphic actions},
  year = {2026}, eprint = {2506.02319}, archivePrefix = {arXiv},
  primaryClass = {math.GR}, note = {Version 2, 27 February 2026},
  url = {https://arxiv.org/abs/2506.02319v2}
}

@article{BDH1980,
  author = {Baumslag, Gilbert and Dyer, Eldon and Heller, Alex},
  title = {The topology of discrete groups},
  journal = {Journal of Pure and Applied Algebra},
  volume = {16}, year = {1980}, pages = {1--47},
  doi = {10.1016/0022-4049(80)90040-7}
}
==== END Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem//references.bib ====