The coefficient ring and the translation module

Put \[R=B\otimes_k B^{\mathrm{op}}, \qquad (a\otimes b^{\mathrm{op}})\cdot m=amb\quad(m\in B).\] Thus \(r=\sum_\nu a_\nu\otimes b_\nu^{\mathrm{op}}\) acts on \(B\) by the operation \(m\mapsto\sum_\nu a_\nu m b_\nu\). The opposite multiplication in the second factor makes composition of these operations agree with multiplication in \(R\), so \(B\) is a left \(R\)-module. The ring \(R\) is finitely presented as a unital associative ring: take a finite algebra presentation of \(B\), a second copy with products reversed, the relations commuting every generator of the first copy with every generator of the second, and \(2\cdot1=0\). The universal property of the tensor product identifies the resulting ring with \(R\). The module \(B\) is generated by \(1_B\); we next show that the relations on this module generator also have a finite description.

For a unital ring \(R\) and \(n\geq3\), the Steinberg group \(\operatorname{St}_n(R)\) has generators \(x_{ab}(r)\), where \(1\leq a\ne b\leq n\) and \(r\in R\), with relations \[\begin{align*} x_{ab}(r)x_{ab}(s)&=x_{ab}(r+s),\tag{3}\\ [x_{ab}(r),x_{bc}(s)]&=x_{ac}(rs) &&(a,b,c\text{ distinct}),\tag{4}\\ [x_{ab}(r),x_{cd}(s)]&=1 &&(a\ne d,\ b\ne c). \tag{5}\end{align*}\] Let \(e_{ab}\) denote the matrix unit. The map \(x_{ab}(r)\mapsto I+r e_{ab}\) gives a surjection \[\pi_n:\operatorname{St}_n(R)\longrightarrow\operatorname{E}_n(R),\] where \(\operatorname{E}_n(R)\) is the subgroup of \(\mathrm{GL}_n(R)\) generated by these elementary matrices. Krstić and McCool prove that \(\operatorname{St}_n(R)\) is finitely presented whenever \(R\) is a finitely presented unital associative ring and \(n\geq4\) (Krstić and McCool 1999, Theorem 3). Their theorem permits noncommutative rings, and applies to the ring constructed above.

A finite relative presentation

The next lemma supplies the additional relations needed for the translations. Finite presentation of the module and of the linear group alone would not establish its conclusion; we prove the semidirect-product presentation explicitly.

The transition endomorphism

Write \(\operatorname{St}=\operatorname{St}_6(R)\), \(\operatorname{E}=\operatorname{E}_6(R)\), and \(\pi=\pi_6:\operatorname{St}\to\operatorname{E}\). Recall the injective algebra map \(\phi:B\to B\) from Theorem 4, and set \(\psi=\phi\otimes\phi^{\mathrm{op}}:R\to R\). This map is injective because tensoring vector spaces over \(k\) preserves injections. Both maps may be nonunital.

We have obtained a finite presentation and compatible transition maps. The map \(\Theta\) need not be injective: the remaining obstruction lies in the kernel of \(\pi\). The next section proves that \(\theta\) annihilates this entire kernel.

Conjugation with an unused index

The use of an index outside the support of a root word is the classical Steinberg centrality argument; see (Weibel 2013, proof of Theorem III.5.2.1). We record its row-and-column form to justify the corner conjugations inside the Steinberg group. The kernel-annihilation theorem also uses the corner comparisons and four-corner splitting proved below.

Interchanging and splitting corners

For a unit \(a\in R^\times\), define \[w_{ij}(a)=x_{ij}(a)x_{ji}(-a^{-1})x_{ij}(a),\qquad h_{ij}(a)=w_{ij}(a)w_{ij}(-1).\] Direct multiplication gives \[ \begin{aligned} \pi(w_{ij}(a))\big|_{\{i,j\}} &=\begin{pmatrix}0&a\\-a^{-1}&0\end{pmatrix},\\ \pi(h_{ij}(a))\big|_{\{i,j\}} &=\begin{pmatrix}a&0\\0&a^{-1}\end{pmatrix}; \end{aligned} \tag{20}\] both matrices are the identity on the other indices.

We can now finish the kernel calculation. The preceding lemmas allow us to compare corner images as group elements, and to split an image over an orthogonal sum without a residual central factor.

For \(R=B\otimes_k B^{\mathrm{op}}\) and \(\psi=\phi\otimes\phi^{\mathrm{op}}\), the elements \(P,U_i,V_i\) constructed in Section 2 satisfy the support and commutation hypotheses and the pair identities (1). Theorem 10 therefore applies to the Steinberg transition of Section 3: it annihilates the matrix kernel in one step.

The mapping torus and its linear part

We first record explicitly why a mapping torus has the needed description even when its defining endomorphism is not injective.

Apply Lemma 15 to \((\Gamma_0,\Theta)\) and denote the resulting finitely presented group by \(\Gamma\). Put \[M_\infty=\varinjlim((B,+),\phi),\qquad E_\infty=\varinjlim(\operatorname{E}_6(R),F), \qquad F(g)=I+\psi^{(6)}(g-I).\] The transition \(F\) is the injective homomorphism of Lemma 9; recall the matrix map \(\pi:\operatorname{St}_6(R)\to\operatorname{E}_6(R)\).

A faithful action and two-transitivity

Set \(X=M_\infty^6\). The subgroup \(M_\infty^6\) acts on \(X\) by translations, and \(E_\infty\) acts by matrices after passing to a common stage, as in (24). Let \(t\) act by the forward stage shift. This shift intertwines the matrix actions, so these formulas define an action of \(\Gamma\) on \(X\).

Embedding the input group and finishing the proof

The last step is to put the original group into the elementary matrix part of \(\Gamma\). Here the commutator property of Lemma 3 is essential.

The monoid input

We first define the auxiliary monoid used in the construction. Let \(\mathcal P\) be the monoid 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 \(e_0,e_1\) on \([0,\infty)\cap\mathbb Q\) and \([1,\infty)\cap\mathbb Q\), respectively. Composition applies the right-hand factor first. The identity \(1_{\mathcal P}\) is the full identity map.

For a monoid \(K\) with zero \(\Omega\ne1_K\), write \[T=(K\setminus\{\Omega\})\times\mathcal P\ \sqcup\ \{0_T\}.\] The element \(0_T\) is absorbing. Nonzero pairs multiply coordinatewise, except that a product whose \(K\)-coordinate is \(\Omega\) is replaced by \(0_T\). Its identity is \((1_K,1_{\mathcal P})\).

The proof of Theorem 19 occupies Section 7, using the finite compiler proved in Appendix 8. In the construction, \(\zeta\) is the zero symbol and \(z\) is the class of a distinct separator letter \(\mathtt z\).

A simple algebra inside a finitely presented algebra

Throughout this section \(k=\mathbb F_2\). For any monoid \(D\) with zero \(0_D\ne1_D\), its contracted monoid algebra \(k_0[D]\) has \(k\)-basis \(D\setminus\{0_D\}\). Basis elements multiply as in \(D\), with a product equal to \(0_D\) interpreted as the zero vector. It is a unital algebra, with identity the basis element \(1_D\).

To prove Theorem 4 for a given group \(L\), apply Theorem 19 with \(\widehat G=L\) and set \[A_0=k_0[H],\qquad B=k_0[K].\] Both algebras are nonzero. We distinguish the monoid elements \(\zeta,\Omega\) from algebra zero, and distinguish \(c_{\zeta}\) from all three: it is a nonzero basis element of \(B\).

The monoid requirements now serve distinct purposes. The selectors in Theorem 19(iii) isolate one coefficient of a nonzero element of \(A_0\), forcing simplicity. The maps in (ii) and (iv) provide algebra embeddings in opposite directions, but treat zero differently: \(\kappa\) preserves it, whereas the linear extension of \(c\) requires a correction by \(c_{\zeta}\). Finally, the separator in (v) keeps the ordered pairs indexing a tensor basis distinct, which will supply the tensor detector.

Identify \(A=i(A_0)\subseteq B\). It is a simple algebra with its own identity \(e\), and Theorem 19(i) embeds \(L\) in \(A^\times\): a unit of \(H\) and its inverse give inverse basis elements in \(A_0\), which \(i\) sends to units relative to \(e\). We next construct an injective nonunital endomorphism of \(B\) whose image lies in \(A\).

Two equivalent subcorners

For a dyadic rational \(a\), let \(e_a\) denote the partial identity on \([a,\infty)\cap\mathbb Q\). These maps belong to \(\mathcal P\): \(u^{-1}v\) is translation by \(1\), its powers and conjugates by powers of \(u\) give all dyadic translations, and conjugating \(e_0\) by translation by \(a\) gives \(e_a\). In the monoid itself, \[ e_a e_b=e_{\max\{a,b\}},\qquad w e_a w^{-1}=e_{w(a)} \tag{27}\] for every available full increasing affine map \(w\). Thus these are equalities of basis elements in the abstract algebra \(k[\mathcal P]\).

We require a nonzero corner that decomposes into two orthogonal copies of itself. The identities in the next lemma have the rectangular-inverse form familiar from Leavitt’s module-type construction (Leavitt 1962, sec. 3), with the corner idempotent as identity. Here we realize them directly using the partial affine maps above.

Define \[j:B\longrightarrow A_0,\qquad j(b)=\rho(b\otimes q), \qquad \phi=i\circ j:B\longrightarrow B.\] These maps are nonunital algebra homomorphisms. The map \(j\) is multiplicative because \(q^2=q\), and it is injective because \(q\ne0\) and tensor products are over the field \(k\). Hence \(\phi\) is injective and \(\phi(B)\subseteq A\). Let \[p=\phi(1_B),\qquad s_l=i\rho(1_B\otimes s'_l),\qquad t_l=i\rho(1_B\otimes t'_l)\quad(l=0,1).\] The idempotent \(p\) belongs to \(A\), so \(p\ne1_B\). Applying the two algebra maps to Lemma 21 gives \[ s_l,t_l\in pBp,\qquad t_ls_j=\delta_{lj}p,\qquad s_0t_0+s_1t_1=p. \tag{28}\] These elements commute with \(\phi(B)\). Indeed, \[(b\otimes q)(1_B\otimes s'_l)=b\otimes s'_l =(1_B\otimes s'_l)(b\otimes q),\] and the identical calculation holds for \(t'_l\); now apply \(i\rho\). Thus the required self-embedding and binary pairs centralizing \(\phi(B)\) have been constructed. It remains to verify detection for the tensor action.

A separating tensor vector

As in Section 3, set \(R=B\otimes_k B^{\mathrm{op}}\), acting on \(B\) by \((a\otimes b^{\mathrm{op}})m=amb\), and define \[\psi=\phi\otimes\phi^{\mathrm{op}}.\] We need one vector on which \(\psi(r)\) acts nontrivially for every \(r\ne0\). The separator gives this simultaneously for all \(r\), by realizing distinct basis tensors as distinct monoid elements.

Let \(W=\rho(B\otimes_k k[\mathcal P])\subseteq A_0\), with basis \(\{\kappa(\tau):\tau\in T\setminus\{0_T\}\}\). Part (v) of Theorem 19 proves that the linear map \[D:W\otimes_k W^{\mathrm{op}}\longrightarrow A_0, \qquad D(x\otimes y^{\mathrm{op}})=xzy,\] is injective: it sends distinct basis tensors to distinct nonzero basis elements of \(A_0\). This includes tensors with an identity factor. Since \(j(B)\subseteq W\), the composite \[R\xrightarrow{\ j\otimes j^{\mathrm{op}}\ } W\otimes_k W^{\mathrm{op}} \xrightarrow{\ D\ } A_0 \xrightarrow{\ i\ } B\] is a sequence of injective linear maps. For \(r=\sum_{\nu}a_{\nu}\otimes b_{\nu}^{\mathrm{op}}\), its value is \[\begin{aligned} i\bigl(D((j\otimes j^{\mathrm{op}})(r))\bigr) &=\sum_{\nu}i(j(a_{\nu}))\,i(z)\,i(j(b_{\nu}))\\ &=\psi(r)\cdot i(z). \end{aligned}\] Thus \(b_*=i(z)\) satisfies \[ r\ne0\quad\Longrightarrow\quad\psi(r)\cdot b_*\ne0. \tag{29}\] The assertion concerns the action after \(\psi\); its proof uses the explicit separator vector.

The bounded compiler

Fix a finite alphabet \(\Sigma\) containing the disjoint triples \[(\mathtt b_T,\mathtt a_T,\mathtt c_T),\qquad (\mathtt b_G,\mathtt a_G,\mathtt c_G)\] and the six further letters \(\mathtt z,\mathtt d,\mathtt l,\mathtt r,\mathtt h,\zeta\). Fix a total order with \(\mathtt a_T<\mathtt c_T\) and \(\mathtt a_G<\mathtt c_G\). Words are ordered by shortlex: first by length and then lexicographically. We use an acceptable programming system for partial functions \(\Sigma^*\to\Sigma^*\), writing \(f_\eta\) for the function with index \(\eta\). In particular, universal evaluation and effective substitution of parameters are available; integers and tuples are represented by fixed computable word encodings.

The following finite construction is proved in Appendix 8. Its conditional statement is essential: the program index determines the presentation without running the program. The evaluator is also fixed independently of a length bound; its termination and compatibility with equations will be proved from the program’s behavior within that bound.

For clarity, (32) follows from the preceding derivation statement. Transplant the paths from \(u\) and \(v\) to their common output into \(x(-)y\). Neither contextual path leaves the budget, so one-step invariance identifies their outputs. A general machine encoding without this bounded conclusion would not suffice below. The raw singleton rule has a different role: it will distinguish the elements used for the injection \(H\to K\). Multiplication of two raw words, rather than evaluation of a singleton, will encode the product in \(H\) through (33).

Codes and finite rule tables

First consider any index \(\eta\). The auxiliary monoid \(\mathcal P\) has decidable equality by Lemma 18.

Let \(Y\) be the disjoint union of \(X_\eta\) and a fixed finite generating alphabet for \(\mathcal P\). For a \(Y\)-word \(v\), write \(v_K,v_{\mathcal P}\) for its projections, obtained by deleting the letters of the other alphabet. Its tested class is zero if \(N_\eta(v_K)=\Omega\); otherwise it is the pair consisting of \(N_\eta(v_K)\) and the value of \(v_{\mathcal P}\) in \(\mathcal P\). This is at present a partial test. For the second type of code, fix a finite monoid generating alphabet \(Z\) for \(\widehat G\), including the inverses of a finite group generating set, and test words by their values in \(\widehat G\). This second test is total by the hypothesis of Theorem 19.

Choose computably an integer \(D_0>M\) such that \(2^{D_0-1}\ge\max\{|Y|,|Z|\}\). Encode the letters of \(Y\), in their chosen order, by distinct words beginning with \(\mathtt b_T\) and followed by \(D_0-1\) letters from \(\{\mathtt a_T,\mathtt c_T\}\), in lexicographic order. Encode \(Z\) in the same way using the other triple. Write \(C(v)\) for concatenation of the appropriate codes and put \(C(\varepsilon)=\varepsilon\). The type of a nonempty code sequence is unambiguous. Codes preserve shortlex comparison and have length \(D_0\) per generator.

Enumerate all nonempty finite ordered tuples \[(w_1^{(j)},\ldots,w_{s_j}^{(j)})\qquad(j\ge1)\] of distinct \(\Sigma\)-words avoiding \(\zeta\); the empty word is allowed as a member. Choose integers \(N_j\) recursively so that \[ N_j>j,\qquad N_j>\max_i|w_i^{(j)}|,\qquad N_j>2N_h+2+\max_i|w_i^{(h)}|\quad(h<j). \tag{34}\] These inequalities concern all potential earlier envelopes, regardless of which rules will be selected. The increasing sequence \(N_j\) is computable without performing any tested-class evaluation.

We now define a partial procedure \(F(\eta,w)\). Put \(n=|w|\) and form the following finite rule table \(\mathcal R_n\).

1. Include \(\zeta a\to\zeta\) and \(a\zeta\to\zeta\) for every letter \(a\in\Sigma\). For each nonempty \(Y\)-word \(v\) with \(D_0|v|\le n\), test its class. If it is zero, include \(C(v)\to\zeta\). Otherwise find the shortlex least word \(v'\) of the same tested class among all words of length at most \(|v|\), including the empty word; include \(C(v)\to C(v')\) if \(v'\ne v\). Do the same for \(Z\)-words using equality in \(\widehat G\), with no zero case. Call these the static rules.

2. Process the tuples with \(N_j\le n\) in order. If every member of tuple \(j\) has no reducible occurrence under the static rules and previously selected rules, include \[ \mathtt d\mathtt l^{N_j}w_i^{(j)}\mathtt r^{N_j}\mathtt h \longrightarrow \begin{cases} \varepsilon,&i=1,\\ \zeta,&i>1. \end{cases} \tag{35}\] Some of these left sides may be longer than \(n\); they simply cannot act on the input.

3. Reduce \(w\) until no rule applies, using a fixed deterministic choice of occurrence and rule.

Whenever the tests terminate, the last step terminates: every rule decreases shortlex. In particular a nonempty code reduced to \(\zeta\) shortens, since \(D_0>2\). All other non-code rules shorten as well. Thus \(F\) is uniformly partial computable.

The fixed point and its length induction

Effective substitution of parameters gives a total computable index transformation \(\tau(\eta)\) for the function \(F(\eta,-)\). Kleene’s Recursion Theorem (Kleene 1938) supplies an index with \[ f_\eta(w)=F(\eta,w) \tag{36}\] as partial functions. Here is the short parameterization argument. Let \(U\) be universal evaluation and let \(d(a)\) be an effectively obtained index for the partial function \(w\mapsto U(U(a,a),w)\). Choose an index \(b\) computing the total function \(a\mapsto\tau(d(a))\). For \(\eta=d(b)\), \[U(\eta,w)=U(U(b,b),w)=U(\tau(d(b)),w)=F(\eta,w).\] Only now fix the presentation alphabet and code length belonging to this particular \(\eta\). There is no advance bound on the machine’s size or working space. Write \(f=f_\eta\) and \(K=K_\eta\).

The two monoids and their embeddings

Let \(H\) be the monoid on \(\Sigma\) whose equations are the union of all the rule tables. Every word is related to its computed normal form, which is irreducible for this union by stability. Conversely, a contextual use of any one equation preserves that form: choose a bound containing both endpoints and the equation, and apply stability and confluence from Lemma 23. Thus two words represent the same element of \(H\) if and only if their literal \(f\)-outputs agree. This proves decidability. The empty word and the single letter \(\zeta\) are distinct irreducibles; they represent the identity and the absorbing zero of \(H\).

The budget hypotheses now hold at every length, so Lemma 22 gives an equality test for \(K\). In particular its identity and zero are distinct. The tested product classes are now the actual elements of \[T=\bigl((K\setminus\{\Omega\})\times\mathcal P\bigr)\cup\{0_T\},\] with coordinatewise multiplication and every pair having first coordinate \(\Omega\) collapsed to zero. Here a letter of \(X_\eta\) acts in the first coordinate and a generator of \(\mathcal P\) in the second; the letter \(\Omega\) maps to \(0_T\). Thus \(Y\) generates \(T\).

For a nonzero element of \(T\), take its least shortlex \(Y\)-representative \(v\). The code \(C(v)\) is irreducible: a subcode rule would either force the element to be zero or produce a smaller representative; no selector or absorption side occurs in a pure code word. Every other representative reduces by its whole-word rule to this same code, and every zero-class code reduces to \(\zeta\). Consequently coding defines an injective zero-preserving monoid map \[\kappa:T\longrightarrow H.\] It is unital because the least representative of the identity is empty, and it is multiplicative because codes concatenate. The identical argument for \(Z\)-words embeds \(\widehat G\) unitally in \(H\). Its image consists of units, since the products of mutually inverse group words have the empty representative. This includes the trivial group and does not require a nonempty generating set.

Let \(z\in H\) be represented by the separator \(\mathtt z\). For least representatives \(v,v'\) of nonzero elements of \(T\), the words \[ C(v)\mathtt z C(v') \tag{39}\] are irreducible. No code crosses the separator; each code portion is already irreducible; and there are no selector markers or \(\zeta\). These literal words recover the ordered pair, including when one or both representatives are empty. They are nonzero because none equals \(\zeta\). This proves the separator assertion of Theorem 19.

Selectors and multiplication by raw words

Take any ordered tuple of distinct nonzero elements \(h_1,\ldots,h_s\) of \(H\), and let \(w_1,\ldots,w_s\) be their normal words. These words avoid \(\zeta\), since any word containing it reduces to the zero word. Their tuple occurs in the enumeration, say at stage \(j\). A word irreducible for the final rule set is irreducible for the static and selected rules present at stage \(j\). Hence this tuple passes its test. With \[L=\mathtt d\mathtt l^{N_j},\qquad R=\mathtt r^{N_j}\mathtt h\] as elements of \(H\), the selected equations give \(Lh_1R=1\) and \(Lh_iR=\zeta\) for \(i>1\). The argument includes a tuple containing the identity, whose normal representative is empty.

Finally define a multiplicative map in the opposite direction by \[c:H\longrightarrow K,\qquad c([w])=[\operatorname{raw}(f(w))].\] The normal-form characterization of \(H\) makes this well-defined. Every raw singleton is its own literal \(N_\eta\)-output. Distinct normal words therefore give distinct elements of \(K\), and none of these elements is its identity or its zero. For normal words \(u,v\), (33) gives \[c([u])c([v])=[\operatorname{raw}(f(uv))]=c([uv]).\] Thus \(c\) is injective and multiplicative, as required. It is not unital: even \(c(1)=[\operatorname{raw}(\varepsilon)]\) is distinct from \(1_K\). Also \(c(\zeta)\ne\Omega\); it is absorbing only within \(c(H)\). The finite presentation of \(K\) came from the compiler, while the finite alphabet and normal-form procedure give the claimed finite generation and decidability of \(H\). All conclusions of Theorem 19 are proved.

Cells, paths, and the validator

A cell consists of an immutable base in \(\Sigma\sqcup\{\mathsf C,\mathsf D,\mathsf W\}\) and a finite tag. Bases in \(\Sigma\) are called anchors. The other bases mark two cuts and a workspace cell. A tag has an anchor-read bit, a workspace-filled bit, a work symbol from the compiled machine’s finite tape alphabet, an output-reading bit, and an output mark in \(\Sigma\sqcup\{\mathrm{none}\}\). The clean tag has every bit unset, work symbol blank, and output mark none. All these fields may be included on every base; fields not used there are simply left unchanged. A bare cell base in a rule means the cell with its entire tag clean.

The presentation has a zero letter \(\Omega\) and the arrows of the quiver in Figure 2. There are arrows \(\alpha:O\to L\) and \(\omega:R\to O\), head arrows \(L\to R\), and two loop copies \(b_L,b_R\) of every tagged cell \(b\), at \(L,R\), respectively. There are no vertex-identity generators: the empty word is the global identity. Add the equations making \(\Omega\) absorbing and making every incompatible pair of arrows equal to \(\Omega\).

A nonempty path is cut at every \(\omega\alpha\) into sectors. Each contains at most one head, since returning from \(R\) to \(L\) requires such a cut. A headed sector has optional \(\alpha\), left loops, a head, right loops, and optional \(\omega\). Sectors without heads are allowed. Thus the same notation describes complete computations and words with missing boundaries.

Assign grade zero to \(\Omega\) and workspace cells, grade two to cut cells with base \(\mathsf C\), and grade one to all other generators. Tags do not affect grade. Extend grade additively to words, writing \(\gamma\). The maximum generator grade is therefore \(M=2\). Workspace can be added without increasing grade, although it increases literal word length.

Use raw and quota heads \(\mathsf Q,\mathsf P\), validator heads \(\mathsf I,\mathsf J,\mathsf J',\mathsf N,\mathsf V\), a disjoint set of machine heads, and a cleanup head \(\mathsf Z\). For an anchor word \(x\), the notation \(x_L\) or \(x_R\) means its sequence of clean cell copies. A sector is full raw if it has the form \[\operatorname{raw}(x)=\alpha\mathsf Q x_R\omega, \qquad x\in\Sigma^*.\] The word \(x\) is its payload. To combine two such sectors, first impose \[\begin{align*} \mathsf Q a_R&=a_L\mathsf Q &&(a\in\Sigma),\tag{40}\\ \mathsf Q\omega\alpha\mathsf Q&=\mathsf C_L\mathsf P\mathsf D_R, &\mathsf P\mathsf D_R&=\mathsf W_L\mathsf P\mathsf D_R, &\mathsf P\mathsf D_R&=\mathsf I\mathsf D_R. \tag{41}\end{align*}\] In the following validator equations, the arrows specify the forward direction used to analyze the machine; the defining relations are equations in both directions: \[\begin{align*} \mathsf W_L\mathsf I&\longrightarrow\mathsf I\mathsf W_R, &\mathsf C_L\mathsf I&\longrightarrow\mathsf J\mathsf C_R, &a_L\mathsf J&\longrightarrow\mathsf J a_R,\\ \alpha\mathsf J&\longrightarrow\alpha\mathsf J', &\mathsf J'a_R&\longrightarrow a_L\mathsf J', &\mathsf J'\mathsf C_R&\longrightarrow\mathsf C_L\mathsf N, \tag{42}\\ \mathsf N\mathsf W_R&\longrightarrow\mathsf W_L\mathsf N, &\mathsf N\mathsf D_R&\longrightarrow\mathsf D_L\mathsf V, &\mathsf V a_R&\longrightarrow a_L\mathsf V, &\mathsf V\omega&\longrightarrow q_{\rm start}\omega. \end{align*}\] The anchor rules range over \(a\in\Sigma\).

An entry has head \(\mathsf I\) immediately before clean \(\mathsf D_R\). The validator reaches \(q_{\rm start}\) from an entry only when that entry has the complete form \[ \alpha x_L\mathsf C_L\mathsf W_L^s\mathsf I\mathsf D_R y_R\omega, \qquad x,y\in\Sigma^*,\quad s\geq0. \tag{43}\] Indeed the first left sweep checks precisely the clean workspace up to \(\mathsf C\), and the next checks only clean anchors up to \(\alpha\). The rightward sweeps then check these anchors, the first cut, the workspace, the second cut, and only clean anchors up to \(\omega\). Thus both boundaries and every tag are checked. At the handoff all cells are on the left of the head.

These relations prepare a raw product for computation. Slide the first head across \(x\), merge the two adjacent heads, insert \(s\) workspace cells, and enter the validator. The simulation and cleanup defined below will complete the following passage whenever \(f_\eta(xy)\) is defined and has length at most \(|xy|\), provided \(s\) is sufficiently large: \[ \begin{aligned} \operatorname{raw}(x)\operatorname{raw}(y) &\ \rightsquigarrow\ \alpha x_L\mathsf C_L\mathsf W_L^s\mathsf I\mathsf D_R y_R\omega\\ &\ \rightsquigarrow\ \operatorname{raw}\bigl(f_\eta(xy)\bigr). \end{aligned} \tag{44}\] The first passage is the preparation just described; the second is validation, simulation on the workspace, and cleanup. The two anchor blocks retain the input \(xy\) and provide space for its output letters.

Successful computations alone do not control the presented monoid, because each equation can also be used in reverse. The validator and simulator will preserve the ordered cell bases and have finitely many tags and head states. Consequently their transitions on any fixed sector form a finite graph, even if the simulated program never halts. We will search its whole weak component—allowing transitions in either direction—to normalize arbitrary configurations. The component analysis will distinguish those that contain an entry from those that do not. Quota insertion is kept outside this finite graph.

A finite transition table for the computation

We specify the remaining machine equations explicitly through finite scan instructions. This makes the construction uniform in \(\eta\) while avoiding a separate list of rules for each tape symbol.

Every state has one designated reading side. A right-reading state has, for each tested tagged cell, at most one rule of either form \[ q b_R\longrightarrow b'_Lq' \quad\hbox{or}\quad q b_R\longrightarrow q'b'_R; \tag{45}\] a left-reading state uses the mirrored forms. These instructions cross the cell or stay in the same gap, respectively. The cells \(b,b'\) always have the same base. Boundary tests are stationary rules \(\alpha q\to\alpha q'\) or \(q\omega\to q'\omega\) on the designated side. A failed test has no rule. A finite cell predicate expands into the list of tagged cells satisfying it; complementary cases are disjoint. Finite registers are incorporated into the state set by a finite Cartesian product.

Here are the scan instructions used below, together with their complete expansion convention.

• To rewind, cross every cell on the left unchanged. At \(\alpha\), change state without moving and start the specified right-reading continuation. If \(\alpha\) is absent, the scan gets stuck at the left end of the word.

• To find the first cell satisfying a predicate, test cells on the right. At a failure cross unchanged and repeat. At a match use the specified stationary update and continuation. At \(\omega\), use the specified end continuation, or get stuck if failure was prescribed.

• To go to the right boundary, cross all right cells unchanged and use the specified stationary continuation at \(\omega\).

All invocations are expanded with distinct phase states, apart from explicit repetitions of a loop. In particular \(q_{\rm start}\) is fresh: its only incoming rule is the validator handoff, and its only outgoing rule is \(q_{\rm start}\omega\to q_{\rm rewind}\omega\), where \(q_{\rm rewind}\) starts the first rewind. No continuation returns to \(q_{\rm start}\) or to a validator state.

The following finite control program supplies all further internal machine equations.

1. Copy the input. Rewind, and find the first anchor whose read bit is unset. Set that bit, carry its base \(a\) in finite state, rewind, and find the first workspace cell whose filled bit is unset. Write \(a\) on its work track and set its filled bit. Failure to find that workspace cell is stuck. Rewind and repeat the anchor search.

   When the anchor search reaches \(\omega\), rewind and check that an unfilled workspace cell remains; otherwise get stuck. Rewind once more and locate the first workspace cell for simulation. On (43) this writes exactly \(xy\) in anchor order into the initial workspace cells, followed by a blank.

2. Run the given machine. The simulated head reads a workspace cell on its right. For each machine state and work symbol, expand its single transition using (45). A stationary move writes and stays. A right move writes and crosses the current cell, and the next simulation state requires another workspace cell on the right. A left move first writes without crossing, then enters a left-reading intermediate state. That state crosses an immediately left workspace cell unchanged, or stays if the immediately left base is \(\mathsf C\); any other case is stuck. It then returns to a right-reading simulation state. This implements the left-end convention. A halt is recognized only at a workspace cell in bounds.

3. Read the output. After halt, rewind and find the first workspace cell whose output-reading bit is unset. A blank work symbol ends the output. For a work symbol \(a\in\Sigma\), set that bit, carry \(a\) in finite state, rewind, and place output mark \(a\) on the first anchor whose output mark is none. Failure to find such an anchor is stuck. Rewind and repeat. An invalid output symbol, or exhaustion of the workspace without a blank, is stuck. When output ends, go to \(\omega\) and enter a fresh state \(q_{\rm ok}\), with no outgoing internal transition.

Each instruction uses only the finite predicates, finite registers, and updates just specified. Expanding all cases gives a finite list of equations computable from the machine table. Each state tests only its designated side and has disjoint cases. Consequently the internal forward transition relation has outdegree at most one on every sector, including sectors with missing boundaries and arbitrary tags. Every transition preserves the number and ordered bases of the cells.

On a passing entry, simulation success computes \(f_\eta(xy)\) genuinely. Conversely, if \(f_\eta(xy)\) is defined and has length at most \(|xy|\), then some finite quota \(s\) permits success: take more workspace cells than the input length, the largest tape index visited by the halting computation, and the output length. The extra cell supplies its blank delimiter. There are \(|xy|\) anchors for the output marks. This includes empty input: at least one workspace cell is supplied, and a length bound forces the output to be empty.

Add the exit equation \(q_{\rm ok}\omega\to\mathsf Z\omega\) and the following cleanup equations. An anchor cell \(b\) with output mark \(a\in\Sigma\) has \[ b_L\mathsf Z\longrightarrow\mathsf Z a_R. \tag{46}\] For every other tagged cell use \(b_L\mathsf Z\to\mathsf Z\), and add \(\alpha\mathsf Z\to\alpha\mathsf Q\). Cleanup is deterministic and never increases grade, even on dirty data. Applied to a successful passing entry, it leaves \[ \alpha\mathsf Q f_\eta(xy)_R\omega. \tag{47}\] The leftward sweep places successive output letters on its right in the correct order. All unused anchors and all nonanchor cells disappear.

Finite components on arbitrary sectors

We now analyze sectors with arbitrary tags and optional boundaries. For a validator or machine sector, form the graph of internal forward transitions, excluding entry from \(\mathsf P\) and exit to \(\mathsf Z\). We use its entire weak connected component. The ordered bases of its cells and its boundary flags are fixed. If there are \(k\) cells and \(h\) internal head states, with at most \(c\) tags per cell, there are at most \((k+1)h c^k\) possible configurations with these data. Its weak component can therefore be found by a finite search through elementary compiled steps. This search does not call \(f_\eta\) or wait for a computation to halt. In particular, the quota insertion rule is excluded: finite grade alone would not bound the number of grade-zero workspace cells.

The partial evaluator

The component lemma leaves a choice when both an entry and a successful terminal occur. Returning to the entry, removing its quota, and undoing the merge, then sliding the raw heads left, gives \(\operatorname{raw}(x)\operatorname{raw}(y)\); cleaning up the terminal gives \(\operatorname{raw}(f_\eta(xy))\). We give the entry priority, so that internal equations have identical preprocessing outputs. The final combination of consecutive raw sectors will identify the two routes in (44), using the contextual identity assumed in Lemma 22 when other raw sectors are adjacent.

This priority also applies to a failed or malformed entry; in that case quota removal need not produce two full raw sectors. Conversely, a successful component without an entry need not encode a genuine input computation. It can use its unique terminal cleanup directly. The following algorithm includes all these cases.

The algorithm \(N_\eta\) preserves the empty word. It sends every word containing \(\Omega\), and every nonpath, to \(\Omega\), using the zero relations. For a nonempty path, first preprocess its sectors as follows.

1. Leave sectors without heads unchanged. Move \(\mathsf Q\) to its leftmost reachable gap using (40), across clean anchors only.

2. If \(\mathsf P\) has clean \(\mathsf D_R\) immediately right, remove all immediately preceding clean \(\mathsf W_L\) by the quota equation. If clean \(\mathsf C_L\) is then immediately left, unmerge \(\mathsf C_L\mathsf P\mathsf D_R\) into \(\mathsf Q\omega\alpha\mathsf Q\) and normalize the two resulting raw heads as above. Otherwise keep the trimmed sector. A \(\mathsf P\) without immediately right clean \(\mathsf D_R\) is kept.

3. Run \(\mathsf Z\) cleanup until it is stuck or becomes \(\mathsf Q\); in the latter case normalize that raw head.

4. For any validator or machine head, find its finite internal weak component. If there is an entry, move to it along a weak path, revert to \(\mathsf P\), and use the preceding rule. If there is no entry but there is a sector ending in \(q_{\rm ok}\omega\), move there and use cleanup. If neither exists, use the least sector in the component in shortlex order.

Lemma 24 makes the choices in the last rule unambiguous. The ordering is fixed independently of any grade budget. All these operations preserve the original outer boundaries; only unmerge creates an interior \(\omega\alpha\) and splits a sector.

Replace each maximal run of \(t\geq2\) consecutive full raw sectors, with payloads \(u_1,\ldots,u_t\), by \[ \alpha\mathsf Q f_\eta(u_1\cdots u_t)_R\omega. \tag{48}\] A run of length one is left unchanged, without evaluating \(f_\eta\). This completes the definition of \(N_\eta\). Its only calls to that function are in (48).

Assume now the budget hypothesis of Lemma 22 at \(m\). Every preprocessing operation has a derivation that never raises grade. Internal component paths preserve every base and hence grade. Raw slides and entry reversal preserve grade. Quota cells have grade zero. Unmerge preserves grade because \[\gamma(\mathsf C_L\mathsf P\mathsf D_R)=2+1+1 =1+1+1+1=\gamma(\mathsf Q\omega\alpha\mathsf Q).\] Cleanup preserves or decreases it. Each argument in (48) has length at most the original total grade, since every anchor contributes one. Thus all required calls terminate for an input of grade at most \(m\).

The replacement of two full raw sectors is also derivable without raising grade. Move the first head right across its anchors, merge at \(\mathsf Q\omega\alpha\mathsf Q\), insert a sufficient grade-zero workspace quota, enter, simulate successfully, and clean up. The result is the raw word for \(f_\eta(u_1u_2)\). Repeating this operation gives (48), because the budget hypothesis implies \[f_\eta\bigl(f_\eta(u_1u_2)u_3\bigr) =f_\eta(u_1u_2u_3)\] and the analogous identities for longer runs. The successive arguments to \(f_\eta\) have length at most \(|u_1|+\cdots+|u_t|\), because \(f_\eta\) is length-nonincreasing. Each elementary derivation step preserves or decreases grade, including the insertion of grade-zero workspace. Thus every call and every intermediate word remains within its required budget. This proves termination and the asserted grade-nonincreasing normalization path.

Invariance under equations and contexts

We verify that one contextual equation step preserves \(N_\eta\) when both endpoints have grade at most \(m\). All nonzero equation sides are nonempty paths with the same initial and terminal vertices. This includes the deletion \(b_L\mathsf Z\to\mathsf Z\). A replacement therefore preserves whether the whole word is a path. Zero equations and nonpaths give \(\Omega\) on both sides, so it remains to compare paths, using their sectors in the whole contextualized word.

Raw slides have the same leftmost reachable gap. Quota changes have the same trimmed sector. Entry from \(\mathsf P\) has the same preprocessing on both sides, since the internal component gives priority to its entry, even if that entry is malformed and validation fails. Internal validator or machine equations leave the weak component unchanged. Cleanup equations give the same result by forward determinism, including the last step to \(\mathsf Q\). A merge is immediately undone by quota preprocessing before normalizing its two raw heads. This remains true when the two sectors have incomplete outer boundaries or dirty cells. In each case the preprocessed sector list is identical, so its subsequent raw-run replacements agree.

The only remaining equation is \(q_{\rm ok}\omega\to\mathsf Z\omega\). If its internal component has no entry, both sides use the same unique terminal cleanup. If it has an entry, Lemma 24 says that the entry is (43) and its computation returns \(f_\eta(xy)\). Entry-priority preprocessing on one side gives two full raw sectors for \(x,y\); cleanup on the other gives a single full raw sector for \(f_\eta(xy)\). With no full raw neighbors, the pair is replaced by exactly that singleton. Otherwise let \(a,b\) be the concatenations of the neighboring raw words on the left and right. The final runs have outputs \[f_\eta(axyb) \quad\hbox{and}\quad f_\eta\bigl(a f_\eta(xy)b\bigr),\] which agree by the budget hypothesis. The anchor count \(|axyb|\) on the entry side is at most the original grade, so this use is legitimate. Passing validation forces both \(\alpha\) and \(\omega\); an incomplete sector cannot occur in this exceptional comparison. This proves equation-step invariance in every context.

If \(N_\eta(u)=N_\eta(v)\) and both \(xuy,xvy\) have grade at most \(m\), transplant the nonincreasing normalization paths of \(u\) and \(v\) into \(x(-)y\). Additivity keeps every intermediate word within budget. Equation-step invariance identifies each input’s answer with the answer of its contextualized normal form. Those two middle strings are literally equal, proving bounded context compatibility. This argument does not require sector boundaries to survive the attachment of context.

If the hypotheses hold at every budget, every finite derivation is covered by some budget. Invariance then implies that equal monoid words have equal \(N_\eta\) answers. The converse follows from each word’s derivation to its answer. Thus \(N_\eta\) is an exact word-problem evaluator. Its definition always leaves each raw singleton \(\alpha\mathsf Q u_R\omega\) literal, distinct from \(\Omega\) and from the empty word; on two such sectors it gives the raw encoding of \(f_\eta(uv)\) whenever the relevant budget hypothesis holds. All parts of Lemma 22 follow.