Earlier embeddings and the higher-finiteness obstacle

Thompson-type groups have long supplied simple groups with strong finiteness properties. Brown established type \(F_\infty\) for the Thompson–Higman families (Brown 1987, sec. 4). More recently, Belk and Zaremsky constructed a single simple group of type \(F_\infty\) containing all finitely generated right-angled Artin groups (Belk and Zaremsky 2022, Corollary E); 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 \(F_\infty\) containing every countable abelian group (Belk et al. 2024, Theorems 4.4–4.6). 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 (Belk, Bleak, et al. 2026, Theorem A and Corollary D). Belk, Fournier-Facio, Hyde and Zaremsky proved it for \(\operatorname{Aut}(F_n)\) and mapping class groups of orientable punctured surfaces of finite type (Belk, Fournier-Facio, et al. 2026, Theorem A and Corollary B). Here \(F_n\) denotes the free group of rank \(n\). These conclusions do not by themselves give simple overgroups of type \(F_\infty\). Higher finiteness requires control of additional relations among relations in every dimension.

Our final step uses the twisted Brin–Thompson construction of Belk and Zaremsky (2022). Its input is a faithful action of a group \(\Lambda\) on a countably infinite set \(S\). The action must be 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 \(F_\infty\), their theorem gives a simple group \(SV_\Lambda\) of type \(F_\infty\) 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 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 \(F_\infty\) 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 \(F_\infty\) (Fournier-Facio et al. 2026, Theorem 1.1). 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.

Constructing the action and proving finiteness

The action begins with a finitely presented ring \(B\), the elementary matrix group \(Q=\mathrm E_7(B)\), and its action on the column set \(X=B^7\). Here \(\mathrm 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 \(\mathrm 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 Finite algebraic envelopes and the Boone–Higman conjecture (OpenAI 2026) 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 \(\mathbb F_2\) and \(\mathbb 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 3.

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 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 \(F_\infty\) for all stabilizers and complete the input to the twisted Brin–Thompson theorem.

Organization and conventions

Section 2 proves the ascending-torus criterion. Section 3 constructs the ring and the encoded actions. Section 4 constructs \(\Lambda\curvearrowright S\) and proves the stabilizer theorem. Section 5 applies the twisted Brin–Thompson theorem and proves Theorem 1.

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.

Two finite systems of idempotents

For \(\ell\in\{2,3\}\), let \(D_\ell\) be the unital \(\mathbb F_\ell\)-algebra of operators generated by \(l_0,l_1,r_0,r_1\) on the free vector space with basis \(\{0,1\}^{\mathbb N}\). The operator \(l_i\) prefixes \(i\), whereas \(r_i\) deletes an initial \(i\) and sends every other basis vector to zero. Thus \[ r_i l_j=\delta_{ij}1, \qquad l_0r_0+l_1r_1=1. \tag{1}\] 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 \(\mathbb 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(\mathbb 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\).

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\).

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.

A product-module criterion

The product-module test below is a form of the Bieri–Eckmann finiteness criterion (Bieri and Eckmann 1974, Proposition 1.2). For the cellular passage from homological to geometric finiteness, see also Brown (Brown 1975, sec. 3). 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 \((\mathbb ZJ)^{\mathcal I}\) means the direct product, not the direct sum, with its coordinatewise right action.

For \(J=T(U,f)\), finite presentation is already available. It therefore remains to prove \[H_n\bigl(J,(\mathbb ZJ)^{\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.

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 \(\mathbb ZU\)-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 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 \(\mathbb ZU\).

Products of regular modules and the HNN sequence

We now complete the proof of Theorem 3. 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 \(\mathbb ZJ\)-module \(M\), the tree gives the long exact homology sequence containing \[ \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} \tag{6}\] We specify the chain map and a construction of this sequence. Induce the homogeneous resolution to obtain \(P_* =\mathbb ZJ\otimes_{\mathbb ZU}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 \(\mathbb 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 (6). In the resulting complex \(M\otimes_{\mathbb ZU}C_*(U)\), its map \(F\) is \[ F(m\otimes c)=mt\otimes f_*(c). \tag{7}\]

Take now \(M=(\mathbb ZJ)^{\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{split} M\otimes_{\mathbb ZU}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)}\mathbb ZJ\right). \end{split} \tag{8}\] 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 \(\mathbb ZJ\) 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 (8). 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 (7) shows that \(F^k\) changes that origin to \(jt^k\) and applies \(f^k\) to the relative vertices in \(U\). Proposition 7 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 (8). 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 (6) therefore gives \[H_n\bigl(J,(\mathbb ZJ)^{\mathcal I}\bigr)=0 \qquad(n\ge2).\] No claim about local nilpotence on \(H_0\) is needed. By Lemma 4, \(J\) is finitely presented. Lemma 5 now proves that it is of type \(F_\infty\), completing the proof of Theorem 3.

Finite extensions

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

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 2. Define \[ j_E(g)=(1-E)\otimes1+E\otimes g \quad(g\in V,\ E\in\mathcal P_\ell) \tag{9}\] in \(D_\ell\otimes_{\mathbb F_\ell}\mathbb 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.

For a unital \(\mathbb F_2\)-algebra \(B\), put \(Q=\mathrm E_7(B)\) and \(X=B^7\), with the usual left action on columns. Apply the enlargement twice: \[ (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). \tag{10}\] 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 \[ j_{2,E}=j_I^{(3)}\circ j_E^{(2)},\qquad j_{3,E}=j_E^{(3)}\circ j_I^{(2)}. \tag{11}\] Both full-identity maps are \(\iota\). Each family satisfies the orthogonal identities, and \[ qx=x\quad\Longrightarrow\quad j_{\ell,E}(q)\iota_X(x)=\iota_X(x). \tag{12}\] 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.

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.

The bounded compiler and the auxiliary monoid

We use the following established form of the finite compiler (OpenAI 2026, Lemma 7.1, Bounded Compiler Lemma). Its bounded contextual conclusion is essential.

Fix also the monoid \(\mathcal D\) of partial maps of \(\mathbb 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\mathbb Q\) and \([1,\infty)\cap\mathbb Q\). Composition applies the right factor first. An element has computable data \((a,b,r)\), denoting \(x\mapsto ax+b\) on \([r,\infty)\cap\mathbb Q\), with \(a=2^j\) for \(j\in\mathbb Z\), dyadic \(b,r\), and \(r=-\infty\) for full domain. These data multiply by \[ (a,b,r)(c,d,s) =\bigl(ac,ad+b,\max\{s,(r-d)/c\}\bigr). \tag{19}\] 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 (OpenAI 2026, Lemma 6.4) for this same monoid: \[ \begin{gathered} 0\ne q=q^2\in\mathbb F_2[\mathcal D],\qquad s'_i,d'_i\in q\mathbb F_2[\mathcal D]q,\\ d'_is'_j=\delta_{ij}q,\qquad s'_0d'_0+s'_1d'_1=q. \end{gathered} \tag{20}\] Its \(q\) is the difference of the two tail identities, split using the affine maps \(u\) and \(v\).

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 \[ \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}. \tag{21}\] Here \(\delta_{yz}\) denotes the monoid identity or zero.

Syntax and costs before totality

For a field \(k\) and a monoid \(M\) with absorbing zero, write \(k_0[M]\) for its 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 \(\mathbb F_2\) are finite sums of monoid words in the presentation letters. Their 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 \((\mathbb F_2)_0[K_\eta]\).

Use three families of generating symbols.

1. A finite symmetric generating alphabet for \(G\), evaluated using its word decider. These symbols have cost zero.

2. The presentation alphabet \(\mathcal A_\eta\) and a fixed finite generating alphabet for \(\mathcal D\). Their prospective values lie in the zero-product monoid \[ T_\eta=\bigl((K_\eta\setminus\{\Omega\})\times\mathcal D\bigr) \sqcup\{0\}. \tag{22}\] 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.

3. 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)\).

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 \[ |\operatorname{code}(a)|\geq10\operatorname{cost}(a)+2. \tag{23}\] Fix a total order on \(\Sigma\). The 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.

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.

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 \[ f_\eta(w)=F(\eta,w) \tag{26}\] as partial functions (Kleene 1938, sec. 2, p. 153). 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\).

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 11 now applies at every grade, giving an equality algorithm for \(K=K_\eta\) with distinct identity and zero. Set \[k=\mathbb 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.

Ring data and compressed diagonal matrices

Apply Theorem 10 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\): \[ d_i s_j=\delta_{ij}p, \qquad s_0d_0+s_1d_1=p. \tag{32}\] 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=\mathrm 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 10. 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.

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,\tag{34}\\ \beta(y)&=\bigl(\phi^2(S_y),0,\ldots,0\bigr)^{\mathsf T} \in X. \tag{35}\end{align*}\] Membership of \(\mu(w)\) in \(Q\) follows from Lemma 18, 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 \[ \delta=\mu\iota:Q\hookrightarrow Q, \qquad \sigma=\beta\iota_X:X\hookrightarrow X. \tag{36}\] The same compressed-diagonal construction, applied to the corner copy of \(G\), gives an embedding \(G\hookrightarrow Q\).

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 (36) defines an action of \(N\) on \(S\): for \(k\ge i,j\), \[ q_i[x,j]= \bigl[\delta^{k-i}(q)\sigma^{k-j}(x),k\bigr]. \tag{37}\] 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 (37) 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 \[ t^{-1}qt=\delta(q)\qquad(q\in Q). \tag{38}\] 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 (38) makes this well defined and gives the two inverse homomorphisms.

Pointwise stabilizers as ascending tori

Fix a nonnegative integer \(m\). By Lemma 20, 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 19 gives \(a\in Q\) such that \[ a\sigma(z)=z. \tag{39}\] 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, \[ (t')^{-1}qt'=a\delta(q)a^{-1}, \qquad f:U\longrightarrow U, \quad f(u)=a\delta(u)a^{-1}. \tag{40}\] The codomain in this formula follows either from the fact that \(t'\) fixes the tuple or directly from equivariance and Equation (39). The map \(f\) is injective.

The two diagram systems required by Theorem 3 also restrict to \(U\). Let \(j_{\ell,E}:Q\to W\) be the maps of Theorem 10, for \(\ell=2,3\) and \(E\in\mathcal P_\ell\), with common full-identity map \(\iota\). Define \[ h_{\ell,E}:U\longrightarrow U, \qquad h_{\ell,E}(u)=a\mu(j_{\ell,E}(u))a^{-1}. \tag{41}\] 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 3 is a factorization of \(f\) through a finitely presented group. We will use \(\mathrm{St}_6(B)\) as that group. A six-coordinate elementary block inside \(Q=\mathrm 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 \(\mathrm{St}_6(B)\), then move their nonidentity part from coordinate 1 into that block without moving the marked columns.

A homomorphic Steinberg lift

For a unital ring \(R\), the Steinberg group \(\mathrm{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:\mathrm{St}_6(R)\twoheadrightarrow\mathrm E_6(R)\).

We need the following precise form of the kernel-annihilation theorem from OpenAI (2026, Theorem 4.1).

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 \[ I+\psi^{(6)}(g-I), \tag{42}\] 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)\).

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\).