Proof. The transaction operations leave all colors and checker fields in place. Palette operations preserve the multiset of colors. During a check for \(x\), every passed cell has color different from \(x\): this is the condition for a forward step, and swaps within a passed run preserve it. A swap cannot cross from the passed region to the head or idle region because their checker fields differ. In particular, if every color occurs, a head seeking \(x\) cannot reach the last cell with a different color after having passed all earlier cells. Distinctness also prevents an equal-color adjacency.

For the converse, checker syntax in a complete palette either gives an idle palette or gives a single head after a passed prefix. If a passed cell has the sought color the whole word is zero. Otherwise every backward checker step is allowed. Move the head back to the first palette cell and apply the inverse creation rule using \(C(q_h)\). This does not require a transaction head to be in any specified place. With both tracks idle, all palette letters have identical non-color fields. Repeated colors can be brought adjacent by swaps, and a missing color can be sought from the first cell to the last, where the final test gives zero. A nonzero palette therefore has exactly one copy of each color, which can be sorted by adjacent transpositions. ◻

Proof. Structural tags never change, so structural syntax is preserved. For the transaction syntax it suffices to check the interfaces of each kind of move.

If an idle \(C(1)\) occurs in a syntactically admissible complete configuration, its predecessor, if present, has an external right interface. The predecessor may be idle, a completed full region’s last letter, or a boundary cursor stopped at the preceding stop. Its successor \(C(2)\) is idle: a new locked region cannot start at an internal core position. Creating a boundary cursor therefore preserves the external interface on each side. This remains true when the preceding boundary cursor intends to acquire more blocks. It has not acquired this block, and its next acquisition is blocked until the new cursor releases it.

In an acquisition, the old cursor becomes a left marker and its idle successor becomes the new cursor. Its untouched predecessor previously permitted a left marker or a head with these same metadata, and still does. The new cursor has an external right interface, as the old idle cell did. If its untouched successor is inside that block, the successor is idle, since a locked region cannot start there; if it is a block start, it may also start a new region, which is an allowed external joint. The known-last restriction prevents acquisition from creating the prohibited last left marker. The inverse release has the same interface checks in reverse. At \(C(1)\) inverse creation is possible only for a boundary cursor with no acquired successor, so it too preserves the outside interfaces.

In a full movement \(F,R\leftrightarrow L,F\), the exterior predecessor permits respectively \(F\) or \(L\), and the exterior successor permits respectively \(R\) or \(F\). Their internal metadata are unchanged. A move cannot introduce a right marker at first or a left marker at last because the old head must have the indicated neighbor inside its region. Endpoint phase changes do not change these interfaces. The boundary-to-full change is at the last position, where both heads have an external right interface and the same left-interface requirement. Changing the committed side at success changes no interface at all.

For the checker track, head creation occurs at its first position with an idle next checker cell, if present. A forward step changes \(H_x,I\) to \(A_x,H_x\) and has the prescribed predecessor and successor in the checker grammar. Its inverse has the same property. Palette swaps preserve both marker tracks, since their non-color fields must coincide. The main moves leave checker fields and colors in place; checker moves leave main fields and payload in place. In particular a main head may cross a checker head without any additional interface change.

Finally any acquired part of a block includes its \(C(1)\), or is a continuation of a region that acquired that \(C(1)\) earlier. Creation is allowed only at an idle \(C(1)\), and acquisition takes only idle cells. Since the only idle suffix of a partially acquired block is strictly after its cursor, no other transaction can start in that suffix or enter it from the left. This proves the ownership claim and completes the induction over replacements. ◻

Proof. The tour edges are invertible. Starting at \(A_j\) with zero registers, the reading tour reaches its gate with exactly the three bits from the clause’s addresses, and the undo tour restores zero registers. A false gate breaks the path before its after-gate state. Backtracking cannot circumvent this break: the only changes of clause index are the specified edges from \(Z_j\) to \(A_{j+1}\), the only acquisition interface is \(A_1\), and the only extra success edge changes a side bit which the schedule does not read. Thus success is reached exactly when all clauses are true, and no format, nonblank-register, or false-after-gate zero is reached. After a side change, the same clauses still read the same fixed slots, independently of the selected side, so all verification moves can be reversed. ◻

Proof. Fix the payload of the region. Each tour edge is a bijection on register tuples: it is either the identity or XOR by a specified tuple of the fixed payload bits. The legs and turns give a prescribed finite path. From any interior tour position, reversing that path reaches the endpoint preceding the tour, regardless of the initial register tuple. The endpoints exist because this is a complete region.

For a reading tour this returns to its \(A_j\) endpoint, where a nonzero register tuple is zero by declaration. For an undo tour it returns to \(G_j^{\rm gate}\). If the gate predicate there is false, the word is zero. Otherwise cross the gate backward and reverse the reading tour, again reaching \(A_j\) or zero. The same argument starts directly from either gate phase. In particular a false before-gate value is not a trap: it can reverse its reading tour.

From \(A_j\) with \(j>1\), reverse the edge from \(Z_{j-1}\) and apply the same argument to the preceding clause. A success state first reverses to \(Z_m\); its registers must already be zero, or it is a declared zero. Thus the clause index decreases until \(A_1\) is reached, or a specified violation occurs. No argument assumes that an earlier clause has actually been checked. The reverse gate test and the required blank-register endpoints supply precisely the checks needed for arbitrary starting states.

At \(A_1\) reverse the boundary-to-full change. Inverse acquisition then moves the boundary cursor back through its acquired prefix, returning committed data to the idle cells; finally inverse creation removes it. None of these moves reads a cell outside the acquired interval. The same release argument applies immediately to a region already carrying a boundary cursor. ◻

Proof. For an elementary replacement on \(l\) letters, acquire the \(l\) canonical blocks with the source data in the committed slot, the target data in the other slot, and an accepting computation certificate in the first core. All required acquisitions exist. The verifier checks every clause, reaches success, changes the committed side, and follows inverse verification and release moves to leave the target blocks. Their palettes and checker tracks have not changed. The same procedure for an elementary zero declaration uses its accepting certificate and reaches the success zero. No cell outside those blocks is needed.

For the converse, consider any sequence from a concatenation of canonical blocks. By Lemmas 6 and 5, all structural and marker syntax remains valid and all palettes retain exactly one of each color. At any time read a represented higher-level word as follows. An idle core cell contributes its idle data bit. An acquired core cell contributes the data bit in the side selected on its region’s unique head. The ownership assertion in Lemma 6 makes this unambiguous. Acquisition and release preserve the represented word, even when they choose new uncommitted data or certificate bits after a partial release. Palette operations do not affect it.

While a head is full, every slot and certificate bit of its region is fixed. Interleavings with another transaction cannot change this payload, by ownership; palette operations cannot change an addressed bit. Lemma 7 therefore applies throughout the transaction. If it reaches replacement success, its certificate establishes a genuine elementary rule on the currently represented letters. Changing the selected side changes the represented word by precisely that rule, and subsequent backtracking remains valid. A reached zero-task success likewise establishes an elementary zero on the currently represented word. No format, nonblank-register, or false-after-gate zero can be reached by verification started from acquisition.

These statements induct over the arbitrary sequence of replacements. All represented words are replacement-equivalent to the starting word. If that word is nonzero, a simulated zero success is impossible; all other zero declarations have already been excluded by the invariants. This proves nonzero preservation. Complete initial blocks keep all transaction regions complete; an absent neighbor can only prevent a requested acquisition, never supply a new transition. ◻

Proof. There is no transaction start strictly inside a palette. Its transaction track has at most one head and otherwise consists of constant-metadata wings, with a possible idle suffix after a boundary cursor. The checker track likewise has at most one head and constant passed and idle runs. The common refinement of these two ordered partitions, after removing their at most two head positions, has at most 16 homogeneous non-head intervals. This deliberately loose absolute bound also covers fragments with one or both ends missing. No payload is present on palette cells, and their relative block number is constant within an acquired part, so these intervals have identical fields except for color.

If a color repeats inside such an interval, adjacent transpositions bring its two occurrences together, producing an equal-color zero. Hence each interval in a nonzero word has at most \(q_h\) cells. The asserted palette bound follows. A whole block, or either of its fragments, therefore has length at most \(17q_h+3\).

At successive core beginnings an acquired region’s relative number strictly increases until at most \(k\), unless a new transaction or idle block begins; the latter creates a cut. There is no other possible continuation, by the internal and external interface tests. Thus an interval with no cut contains at most \(k\) intervening blocks, apart from its two end fragments. For example \[B_h=(k+2)(17q_h+3)\] bounds every such interval. This argument uses available pair tests and the unary known-endpoint exclusions, not tests for missing word neighbors. ◻

Proof. The interval begins at \(C(1)\) and ends at \(S\), because the next cut is another \(C(1)\). If its first block is idle, there can be no locked start inside that block, and the next block would give a cut. The interval is then just one idle block. Otherwise its first nonidle letter has relative block number 1 and is \(L\), a boundary cursor, or a full head; it cannot be \(R\) by (6).

Starting with a left marker, follow its internal successors. The chain cannot stop at an external interface, cross the next cut, or end at the known last position, where a left marker is forbidden. It must therefore reach a head inside the interval. A boundary cursor ends the acquired prefix; its remaining current block is idle, and any later block would begin a new interval. A full head forces a right wing as far as its known last position. The interfaces admit no second head on that wing. This proves that a nonidle interval contains exactly one transaction and at most \(k\) blocks, including the final block if acquisition stopped partway through it.

Every palette here is complete. First remove all its checker heads using Lemma 5, or obtain a zero. Apply Lemma 8 to the transaction head and release the acquired cells, or again obtain a zero. The interval is a factor of a nonzero word, so any sequence producing zero in the interval would produce zero in that word and is impossible. All these operations are thus successful replacements. Their support is inside the interval: checker removal stays in the palette and its preceding core cell, and release uses only the acquired prefix. Unlike the clean-start argument, this step does not require the initial control state to have been reached by acquisition.

The interval is now idle on both tracks. In each palette a missing or repeated color would give zero by Lemma 5. Each palette has exactly \(q_h\) cells and can be sorted. The remaining idle core data specify one bit string of length \(cDh\) per block. These are letters of the upstairs bit-string alphabet, including its unused formats when considered before imposing its unary zero relations. The resulting word is exactly \(E_h(u)\) for the corresponding string \(u\) of between one and \(k\) letters. ◻

Proof. The map \(\mathcal A_m\) is multilinear. If \(X_i=X_j\) with \(i\ne j\), pair a permutation \(\sigma\) with \((i\ j)\circ\sigma\). The two products are equal, and the pairing has no fixed point. Their sum is zero in characteristic two. Hence \(\mathcal A_m\) is alternating, meaning that it vanishes whenever two arguments agree. Expand its arguments in a basis of the \(d^2\)-dimensional vector space \(M_d(K)\). If \(m>d^2\), each term in the multilinear expansion has a repeated basis argument and is therefore zero. This proves the result without any division by \(m!\). ◻

Proof. Fix such a test and choose \(n\) above the long-word threshold in Proposition 4. In its length-\(n\) sum discard the sequences whose concatenated word is zero. We partition the remaining sequences into permutation orbits and prove that each orbit contributes zero.

For each remaining sequence let \(w\) be its concatenated word. Erase only the color field from each letter of \(w\), retaining its position and all other fields. Among the maximal eligible runs, choose the first one having length at least \(q_j/100\). This choice exists by Proposition 4 and depends only on the color-erased word. Every eligible run in a nonzero word has distinct colors: if two colors agreed, adjacent transpositions within that run could bring them together and give a declared zero substring. This also explains why color distinctness need not enter the rule selecting the run.

Mark the chunk boundaries of the sequence. Its packet is the consecutive list of all complete chunks contained in the chosen run. Keep all other chunks fixed, including any chunk crossing an endpoint of the run. There are at most two crossing chunks. If the run has length \(r\) and the packet contains \(m\) chunks, then \[r\leq mb+2b,\qquad m\geq r/b-2>d^2.\] Here the last inequality follows from Equation (15). In particular the packet is nonempty.

Permute these \(m\) whole chunks arbitrarily. They may have unequal lengths, but their total length is fixed. Thus the packet occupies the same letter interval after every permutation, and every letter in that interval retains the common non-color tuple. The color-erased word is unchanged at every position. Consequently the chosen maximal run is unchanged. The exterior chunks, including the endpoint-crossing chunks, are unchanged as well, so the complete chunks in this run are again exactly the packet just permuted. Its internal chunk boundaries may move; its endpoints and the rule selecting it do not.

All words obtained in this way have the same algebra image: arbitrary permutations of their letters within the run are products of the allowed adjacent transpositions. If any permuted word were zero, their common image would be zero and the starting word would also be zero. Thus the discarded zero sequences cannot remove any member of a nonzero orbit, and every permuted sequence is still among the summands under consideration. Conversely applying the same procedure to any of them produces the same set of sequences. These sets are therefore a partition into orbits.

The labels of the packet chunks are pairwise distinct. Indeed each begins with a different color, since their first letters occupy distinct positions of the distinct-color run. Hence the chunk identifiers in the packet are also pairwise distinct, even if the original list admitted several identifiers with a common label. All \(m!\) permutations give different sequences of identifiers; the orbit is a free permutation orbit. This assertion concerns sequences, not their concatenated words. Distinct segmentations of a word remain separate summands and belong to their respective orbits.

Choose one orbit and write its fixed exterior matrix products as \(U,V\), the packet weights as \(X_1,\ldots,X_m\), and its common algebra image as \(a\in A_j(K)\). Its entire contribution is \[U\left(\sum_{\sigma\in S_m} X_{\sigma(1)}\cdots X_{\sigma(m)}\right)V\otimes a.\] The weights \(X_i\) themselves need not be distinct. The displayed middle sum vanishes by Lemma 13. There are only finitely many sequences of total length \(n\), so summing the zero orbit contributions proves the desired vanishing. ◻

Proof. Let \(M\) be a letter test at level \(j\). By Proposition 4, there are integers \(B,N_0\) such that every nonzero word of length at least \(N_0\) has the stated cut decomposition, with initial and final pieces of length at most \(B\). Increase \(B\) to at least one. A cut is recognized solely from the letter immediately after it; there is no additional cut after the last letter of the word.

Take the token list \(\mathcal T\) to be a set of distinct literal words. For each \(t\in\mathcal T\) fix once and for all an upper word \(u_t\) with \[ 1\leq |u_t|\leq k,\qquad |t|=L_j|u_t|,\qquad [t]_j=E_j([u_t]_{j+1}). \tag{16}\] If a token has more than one possible upper normal form, choose one; it is the literal token, not its normal form, that indexes this list. Every token begins with a cut letter and contains no further cut letter.

Let \(\mathcal P\) be the finite set of words of length at most \(B\) containing no cut letter, including the empty word. Let \(\mathcal S\) be the finite set of words of lengths \(1\) through \(B\) whose first letter is a cut letter and whose remaining letters are not. Consider concatenations \[ p\,t_1\cdots t_r\,s, \qquad p\in\mathcal P,\quad s\in\mathcal S,\quad t_i\in\mathcal T. \tag{17}\] They have a unique such representation: the prefix ends at the first cut, the suffix begins at the last cut, and the intervening cut intervals are exactly \(t_1,\ldots,t_r\). This also proves uniqueness when \(r=0\). For sufficiently large length every nonzero word has this representation. Some concatenations in Equation (17) may be zero, and some zero words may have no representation; in either case their contribution to Equation (13) is zero. Thus summing all concatenations in Equation (17) neither loses nor duplicates any nonzero contribution.

Use \(\mathcal T\) as the chunk identifiers at level \(j+1\), with label \(u_t\) and weight \(M(t)\). Denote the resulting length-\(m\) sum by \(C_m\). For every sufficiently large \(n\) we have the exact identity \[ S_{j,n}(M)= \sum_{\substack{p\in\mathcal P,\ s\in\mathcal S\\ m=(n-|p|-|s|)/L_j\in\mathbb Z_{\geq0}}} \bigl(M(p)\otimes[p]_j\bigr) (\mathrm{id}\otimes E_j)(C_m) \bigl(M(s)\otimes[s]_j\bigr). \tag{18}\] Indeed the length equation follows from Equation (16); multiplicativity of \(M\) preserves the matrix order, and the token equalities give the algebra factor. No nonzero-preservation or injectivity assertion about \(E_j\) is required for this identity. In particular, an upper concatenation whose encoded product vanishes causes no difficulty.

By hypothesis \(C_m=0\) for \(m\geq N_1\), for some \(N_1\). Since \(|p|+|s|\leq2B\), every integer \(m\) occurring in Equation (18) is at least \(N_1\) once \(n\geq2B+L_jN_1\). Taking \(n\) also large enough for that identity proves the lemma. ◻

Proof. First combine all identifiers with the same label \(v\) into one weight \[W(v)=\sum_{\gamma:\,v_\gamma=v}W_\gamma.\] Distributivity shows that this leaves every chunk sum unchanged, including the contributions from repeated occurrences of such a label. Zero weights can be retained or removed. If there are no labels, take every letter matrix to be the zero \(d\) by \(d\) matrix; this gives the assertion, including length zero. Hence suppose the label set is \(\mathcal V\ne\varnothing\).

The states are the empty word \(\epsilon\) and all nonempty proper prefixes of labels in \(\mathcal V\). For each state \(p\) and letter \(a\in\Sigma\) put an identity-weighted transition \[p\xrightarrow{\ a,\,1_d\ }pa\] whenever \(pa\) is a proper prefix of some label. Put a closing transition \[p\xrightarrow{\ a,\,W(pa)\ }\epsilon\] whenever \(pa\in\mathcal V\). Both kinds of transition are allowed when \(pa\) is both a label and a proper prefix. We add the weights of any transitions with identical initial state, final state, and letter.

If the number of states is \(e\), define \(B(a)\in M_{ed}(K)\) by taking its \((p,q)\) block to be the sum of the weights of transitions from \(p\) to \(q\) with letter \(a\). The \((\epsilon,\epsilon)\) block of \(B(a_1)\cdots B(a_n)\) is the sum of the weights of all paths reading \(a_1\cdots a_n\) and beginning and ending at \(\epsilon\). The visits to \(\epsilon\) mark exactly the closures of chunks. A path between two consecutive visits reads one label \(v\), contributes identity weights until its last step, and then contributes \(W(v)\). Paths therefore correspond bijectively to segmentations into labels, with exactly the ordered matrix products required in Equation (14). Taking the \((\epsilon,\epsilon)\) block after summing the words with their algebra images proves the asserted identity.

Every state is a word of length less than \(b\), so \[e\leq\sum_{i=0}^{b-1}s^i\leq b s^{b-1}\leq C_b s^b.\] Padding the matrices by zero blocks, if needed, realizes any larger specified dimension without changing positive-length sums in the original block. This proves the dimension claim. ◻

Proof. Fix the field and a starting letter-test dimension \(d\). For \(j\geq1\) define integer dimension bounds \[ d_j=d\prod_{i=1}^{j-1}\bigl(C_k|\Sigma_i|^k\bigr). \tag{20}\] The empty product gives \(d_1=d\). Lemma 15 reduces dimension-\(d\) letter tests at level zero to dimension-\(d_1\) chunk tests at level one. At a level \(i\geq1\), Lemma 16 turns a dimension-\(d_i\) chunk test into a letter test of dimension at most \(d_{i+1}=C_k|\Sigma_i|^kd_i\) at that same level. Padding to dimension \(d_{i+1}\) and applying Lemma 15 reduces its vanishing to that of a dimension-\(d_{i+1}\) chunk test at level \(i+1\).

We show that these reductions can be stopped after finitely many levels. Using \(|\Sigma_i|\leq2^{ch_i}\) and the geometric sum for \(h_i\), we obtain \[\begin{align*} \log_2(d_j^2) &\leq 2\log_2 d+2(j-1)\log_2 C_k +2kc\sum_{i=1}^{j-1}h_i \\ &=2\log_2 d+2(j-1)\log_2 C_k +\frac{2kc}{D-1}(h_j-h_1). \tag{21}\end{align*}\] By Equation (12), the number \(\delta=1-2kc/(D-1)\) is strictly positive. Since \(h_j=h_0D^j\), it follows from Equation (21) that \[h_j-\log_2(d_j^2)\longrightarrow+\infty.\] In particular there is a finite \(J\geq1\) such that \[2^{h_J}>400k d_J^2\geq100k(d_J^2+3),\] where the second inequality uses \(d_J\geq1\). Direct cancellation, Lemma 14, therefore applies to all dimension-\(d_J\) chunk tests of label bound \(k\) at level \(J\).

Work backwards through the finitely many reductions. If all dimension-\(d_{i+1}\) chunk tests at level \(i+1\) eventually vanish, then all dimension-\(d_{i+1}\) letter tests at level \(i\) eventually vanish by Lemma 15. Lemma 16 then gives eventual vanishing for all dimension-\(d_i\) chunk tests at level \(i\). Descending to level one and using Lemma 15 once more proves the letter-test assertion at level zero.

For precision, no common length threshold for all tests is being postulated. The stopping level \(J\) above depends only on the starting dimension and the fixed hierarchy. Each application of the reductions uses a finite test and, in the cut reduction, finitely many bounded end pieces. A threshold for the particular resulting test is pulled back through finitely many length dilations and additions of bounded end lengths. The conclusion has the order of quantifiers \[\text{for every fixed test, there is }N \text{ such that every length }n\geq N\text{ has zero sum}.\] It does not require one \(N\) for all dimensions.

Finally, a level-zero chunk test of dimension \(d\) with any label bound \(b\) is a block of a level-zero letter test of finite dimension at most \(C_b|\Sigma_0|^bd\), by Lemma 16. The already proved letter-test assertion applies to that test and proves the final claim. ◻

Proof. Take \(R=A_0(\mathbb F_2)\), using only the level-zero alphabet and the level-zero relations. The alphabet is finite, and there are only finitely many words of length at most \(k\) on it. The chosen replacement rules and zero rules thus give an ordinary finite algebra presentation \[R=\mathbb F_2\langle\Sigma_0\rangle/\mathcal J_0,\] where \(\mathcal J_0\) is the two-sided ideal generated by \(u-v\) for the listed replacements \(u\leftrightarrow v\) and by \(w\) for the listed zero words \(w\). No relation from a higher level is added to this ideal. All defining polynomials are homogeneous of positive degree, so word length gives the displayed grading, the empty word spans \(R_0=\mathbb F_2\), and the positive-degree part \(I\) is a two-sided ideal.

For every \(j\geq1\), choose a nonzero letter \(a_j\) at level \(j\). The word \[w_j=E_0E_1\cdots E_{j-1}(a_j)\] is nonzero by repeated use of the nonzero-preservation clause of Proposition 4. Its length is \(L_0L_1\cdots L_{j-1}\), which tends strictly to infinity because each \(L_i>1\). The nonzero classes \([w_j]_0\) lie in distinct homogeneous degrees and are therefore linearly independent. Consequently \(R\) is infinite-dimensional over \(\mathbb F_2\), and in particular is an infinite set.

Fix \(\ell\geq1\) and \(T\in M_\ell(I)\). Express its entries as finite linear combinations of nonempty word images and collect matrix coefficients to write \[ T=\sum_{\gamma\in\mathcal C} A_\gamma\otimes[v_\gamma]_0, \qquad A_\gamma\in M_\ell(\mathbb F_2),\qquad |v_\gamma|\geq1. \tag{22}\] If this list is empty then \(T=0\) and there is nothing to prove. Otherwise let \(b=\max_\gamma|v_\gamma|\). Introduce a central indeterminate \(z\) and apply Proposition 17 over the field \(K=\mathbb F_2(z)\) to the chunks \(v_\gamma\) with weights \(zA_\gamma\). Its length-\(n\) sum is the image of the polynomial \[ P_n(z)= \sum_{\substack{r\geq0,\ \gamma_1,\ldots,\gamma_r\in\mathcal C\\ \sum_i|v_{\gamma_i}|=n}} z^r A_{\gamma_1}\cdots A_{\gamma_r} \otimes[v_{\gamma_1}\cdots v_{\gamma_r}]_0 \ \in M_\ell(R)[z]. \tag{23}\] For fixed \(n\) this is a finite polynomial: nonempty chunks imply \(r\leq n\) for every positive-length term. The proposition supplies \(N\) such that the image of \(P_n(z)\) in \(M_\ell(K\otimes_{\mathbb F_2}R)\) is zero whenever \(n\geq N\).

The map \[M_\ell(R)[z]\longrightarrow M_\ell(\mathbb F_2(z)\otimes_{\mathbb F_2}R)\] is injective. For example, choose an \(\mathbb F_2\)-basis of \(R\) and expand the finitely many coefficients of a polynomial in that basis; its image is zero exactly when every resulting scalar polynomial is zero in \(\mathbb F_2(z)\), hence in \(\mathbb F_2[z]\). Thus \(P_n(z)\) itself is zero for all \(n\geq N\), and each of its coefficients can legitimately be extracted in the original matrix algebra.

For an integer \(a\geq1\), expansion of Equation (22) and grouping its sequences by total word length gives the finite identity \[ T^a=\sum_{n=a}^{ab}[z^a]P_n(z). \tag{24}\] The lower bound \(a\) uses that every factor has a nonempty label; the upper bound \(ab\) uses the fixed maximum label length. If \(a\geq N\), every polynomial on the right of Equation (24) is zero. Hence \(T^a=0\). Since \(\ell\) and \(T\) were arbitrary, every \(M_\ell(I)\) is nil, as asserted. ◻

Proof. Let \(F=\mathbb F_2\langle\Sigma_0\rangle\) be the free unital algebra used in Theorem 18, and let \(F_+\) be its subalgebra spanned by the nonempty words. This is the free nonunital associative algebra on the finite alphabet \(\Sigma_0\). Let \(S\subset F_+\) be the finite set of defining polynomials: the listed \(u-v\) and the listed zero words \(w\). Write \((S)_+\) for the two-sided ideal of the nonunital algebra \(F_+\) generated by \(S\). Both \((S)_+\) and the unital ideal \(\mathcal J_0=(S)_F\) are the linear span of the products \(usv\), with \(s\in S\) and with each word context \(u,v\) allowed to be empty. Indeed, closure under multiplication by \(F_+\) gives the nonempty contexts, while the generators themselves and one-sided products give the empty contexts. Since every \(s\) has positive degree, these products lie in \(F_+\). Hence \(\mathcal J_0=(S)_+\subset F_+\), and restriction of the quotient map gives \[I\cong F_+/(S)_+.\] This is a finite presentation in the nonunital category. The splitting \(F=\mathbb F_2\oplus F_+\) descends to \(R=\mathbb F_2\oplus I\) with the usual unitization multiplication.

Theorem 18 and this direct sum show that \(I\) is infinite-dimensional. Taking matrix size one in that theorem shows that \(I\) is nil. If \(i^N=0\), then in its unitization \[(1-i)^{-1}=\sum_{j=0}^{N-1}i^j.\] Thus every element of \(I\) is quasi-regular, so \(I\) is Jacobson radical. If \(I^m=0\) for some \(m\), every word in the finite generating alphabet of length at least \(m\) would vanish. The images of the finitely many words of lengths \(1,\ldots,m-1\) would then span \(I\), contradicting its infinite dimension. Therefore \(I^m\ne0\) for every \(m\geq1\).

The finite presentation and infinite dimension of \(R\) are already part of Theorem 18. For \(r=a1+i\) choose \(N=N(i)\) with \(i^N=0\). Then \((r-a1)^N=i^N=0\), which proves that \(r\) is algebraic over \(\mathbb F_2\). This applies to every element of \(R\). ◻

Proof. Let \(H_1=\langle A,Z\rangle\) and \(H_2=\langle X,B\rangle\). Every generator of \(H_1\) commutes with every generator of \(H_2\) by the assumptions, so these two subgroups centralize one another. Conjugation of \([X,Z]=1\) by \(Y\), together with \[YXY^{-1}=A^{-1}X, \qquad YZY^{-1}=BZ,\] gives \([A^{-1}X,BZ]=1\). Since \(B\) and \(Z\) commute, and since the factors from \(H_1\) commute with those from \(H_2\), expansion of this commutator gives \[1=[A^{-1}X,ZB]=[A^{-1},Z][X,B].\] Set \(C=[A^{-1},Z]\) and \(D=[X,B]\). Then \(C=D^{-1}\) belongs to both \(H_1\) and \(H_2\). An element in their intersection centralizes each subgroup, so \(C\) commutes with \(A,Z,X,B\). Finally, direct expansion gives \[[A,Z]^{-1}=A[A^{-1},Z]A^{-1}=ACA^{-1}=C=D^{-1}.\] This proves both assertions. ◻

Proof of Theorem 21. First omit Equation (30), and denote the resulting finitely presented group by \(P_0\). We will prove \(P_0\cong\mathop{\mathrm{St}}_n(T)\), and then impose the algebra relators.

Proof. For each \(i\neq j\), choose \(h\notin\{i,j\}\). Every defining generator of the Steinberg group is a commutator: \[x_{ij}(a)=[x_{ih}(a),x_{hj}(1)].\] Hence the commutator subgroup contains all the generators, proving perfectness. Its quotient \(\mathop{\mathrm{E}}_n(R)\) is perfect as well. For a fixed root position \((i,j)\), the matrices \(e_{ij}(a)\) for distinct \(a\in R\) are distinct, as is seen in their \((i,j)\) entries. Thus an infinite \(R\) gives an infinite \(\mathop{\mathrm{E}}_n(R)\), and the surjection (25) then gives an infinite \(\mathop{\mathrm{St}}_n(R)\). ◻

Proof. An invertible matrix remains invertible under reduction. Conversely, let \(A\in M_n(R)\) have invertible reduction \(\overline A\) over \(\mathbb F_2\). Regard \(B=\overline A^{-1}\) as a matrix over the specified copy of \(\mathbb F_2\) in \(R\); it is already invertible over \(R\). Then \(AB=I_n+U\) with \(U\in M_n(I)\). Choose \(m\geq1\) such that \(U^m=0\). In characteristic two, \[(I_n+U)^{-1}=I_n+U+\cdots+U^{m-1}.\] Thus \(AB\), and hence \(A\), is invertible.

Now take \(A\in\mathop{\mathrm{GL}}_n(R)\). The finite group \(\mathop{\mathrm{GL}}_n(\mathbb F_2)\) contains its reduction, so \(\overline A\) has some finite order \(d\geq1\). Consequently \(A^d=I_n+V\) with \(V\in M_n(I)\). Choose \(m\geq1\) with \(V^m=0\), and choose \(e\geq0\) with \(2^e\geq m\). Successive squaring in characteristic two gives \[A^{d2^e}=(I_n+V)^{2^e}=I_n+V^{2^e}=I_n.\] This proves the periodicity assertions without requiring a common nilpotence index or a common bound on element orders. ◻

Proof. The invertibility assertion is Lemma 24. To complete a tuple of columns, complete their reductions to a basis over \(\mathbb F_2\) and lift the additional columns; the resulting matrix is invertible by that assertion.

In particular, an element of \(R\) with nonzero reduction is a unit. An invertible matrix has such an entry in its first column. Interchange rows to put that entry in position \((1,1)\), and denote it by \(u\). Left multiplication by elementary matrices with parameters \(-a_{i1}u^{-1}\) clears the remaining entries of the first column. Right multiplication by elementary matrices with parameters \(-u^{-1}a_{1j}\) then clears the remaining entries of the first row. The resulting complementary block is invertible by reduction. Induction reduces the matrix to a diagonal matrix of units. The order of the products used here is valid in a noncommutative ring. Finally, a row interchange is elementary because, in characteristic two, its two by two block is \[e_{12}(1)e_{21}(1)e_{12}(1)= \begin{pmatrix}0&1\\1&0\end{pmatrix}.\] This proves the generation assertion. ◻

Proof. We first work with a finite labeled collection of nonzero vectors spanning a vector space of dimension \(n\) over \(\mathbb F_2\). Its independence complex has one vertex for every label; parallel vectors with different labels are not identified. We prove the homology assertion by induction on \(n\). For \(n=1\), the asserted vanishing is just nonemptiness.

Choose a basis from the collection. Its independence complex is a simplex. Adjoin the remaining labeled vectors one at a time. When a vector \(v\) is adjoined, its link in the preceding complex is the independence complex of the preceding vectors projected to the quotient by \(\mathbb F_2v\), with zero projections discarded. The projected collection spans a space of dimension \(n-1\), and its labels are retained. By induction its reduced homology vanishes through degree \(n-3\). Adjoining \(v\) attaches the cone on this link. The relative simplicial chains are its augmented link chains shifted by one. The long exact sequence of this pair therefore preserves vanishing of reduced homology through degree \(n-2\).

For \(n\geq3\) each of these links is connected, by the homology assertion in rank \(n-1\). Attaching a cone on a connected subcomplex to a simply connected complex preserves simple connectivity: a path through the new cone may be replaced, with the same endpoints, by a path in its link, and the replacement is homotopic relative to the endpoints in the cone. Starting with the basis simplex proves the finite assertion on fundamental groups as well.

Any finite set of vertices of \(X_n\) can be augmented by columns whose reductions form a basis. The independence complex on that finite set is one of the finite complexes just considered. Every simplicial cycle and every edge loop uses finitely many vertices, so the finite results give the corresponding assertions for \(X_n\). ◻

Proof. Let \(H'_n\) be the presented group and let \(\pi:H'_n\to H_n\) be its natural surjection, which is surjective by Lemma 25. We prove injectivity by induction on \(n\). For \(n=5\), every true relation is included, so there is nothing to prove. Suppose that \(n>5\) and the result is known in rank \(n-1\).

The stabilizer \(P\) of the column \(e_1\) in \(H_n\) consists of matrices \[\begin{pmatrix}1&b\\0&B\end{pmatrix}, \qquad B\in H_{n-1}.\] Its complementary copy of \(H_{n-1}\) lifts homomorphically to \(H'_n\) by the induction hypothesis. Its row subgroup, generated by \(e_{1j}(a)\) for \(j\ne1\), also lifts: its additive and commuting relations involve at most three coordinates. Conjugation of this row subgroup by each complementary elementary or diagonal generator is its matrix conjugation, again by relations on at most three coordinates. These relations give a homomorphic section \(P\to H'_n\) of \(\pi\) on \(P\). For example, writing a matrix of \(P\) uniquely as a row transvection times \(\operatorname{diag}(1,B)\) gives its lift using this semidirect product structure. Denote the image by \(P'\). The section is injective because its composite with \(\pi\) is the inclusion of \(P\).

Let \(s\in H'_n\) be the elementary word for the swap \((12)\). Its square is one by a two-coordinate relation. The groups \(P'\) and \(\langle s\rangle\) generate \(H'_n\). Indeed, conjugating the generators already in \(P'\) by \(s\) gives every first-column elementary generator and the first diagonal generator; these conjugation identities involve at most three coordinates.

Let \(Q\leq P\) fix both \(e_1\) and \(e_2\) pointwise. It is generated by the complementary elementary and diagonal generators on coordinates \(3,\ldots,n\) and the row generators \(e_{ij}(a)\) with \(i\in\{1,2\}\) and \(j\geq3\). Its image \(Q'\) under the section of \(P\) is generated by the same displayed generators in \(H'_n\). Conjugation by \(s\) fixes the complementary generators and exchanges the two row families, by small-coordinate relations. Hence \[sQ's^{-1}=Q'.\] At the first induction step \(n=6\), this argument uses only generators of the complementary \(H_4\) inside the already lifted \(P\); it does not require a presentation theorem in rank four.

We use \(X_n\) to identify the cosets of \(P'\). The map \[H'_n/P'\longrightarrow X_n^{(0)},\qquad hP'\longmapsto\pi(h)e_1\] is well defined. If \(w\) is adjacent to \(\pi(h)e_1\), frame completion provides \(p\in P\) with \(p e_2=\pi(h)^{-1}w\). From \(hP'\) transport along this oriented edge to \[h\widetilde p\,sP',\] where \(\widetilde p\) is the section of \(p\). The result is independent of \(p\): if \(p e_2=p'e_2\), then \(p'^{-1}p\in Q\), and \(s^{-1}Q's\subseteq P'\). It is also independent of the representative \(h\) of its coset, since replacing \(h\) by \(hr\), with \(r\in P'\), may be offset by replacing \(p\) by \(\pi(r)^{-1}p\). None of these assertions assumes global injectivity of \(\pi\).

Transport reverses along an edge: from the representative \(h\widetilde p s\), the reverse step can use \(p=1\), giving \(h\widetilde p s^2P'=hP'\). Transport around every triangle is also trivial. By translating its first vertex and then using one element of \(P\), frame completion reduces the triangle to \((e_1,e_2,e_3)\). Put \(t=(23)\in P'\), expressed as an elementary word. The three successive representatives can be taken to be \[s,\qquad sts,\qquad ststs=t.\] The final equality is a true relation on the first three coordinates, and \(t\in P'\). Thus the endpoint coset is the starting coset.

By Lemma 26, \(X_n\) is simply connected. Combinatorial edge paths with the same endpoints therefore differ by backtracks and triangle moves, after subdivisions of a null homotopy; both moves preserve transport. Starting at \(P'\), transport consequently assigns exactly one coset to every vertex. Every coset is reached, since \(P'\) and \(s\) generate \(H'_n\): multiplication on the right by an element of \(P'\) changes only a representative, and multiplication by \(s\) is one of the allowed edge steps. The displayed coset map is therefore a bijection.

If \(h\in\mathop{\mathrm{Ker}}\pi\), its coset maps to \(e_1\), so \(h\in P'\). The restriction of \(\pi\) to \(P'\) is injective. Hence \(h=1\), completing the induction. ◻

Proof. Assign to each elementary generator \(e_{ij}(a)\) of \(H_n\) conjugation by \(x_{ij}(a)\) on \(\mathop{\mathrm{St}}_n(R)\). Assign to a diagonal generator the automorphism \[x_{ij}(a)\longmapsto x_{ij}(u_i a u_j^{-1}),\] where all but one of the \(u_i\) are one. This preserves the Steinberg relations; in particular the adjacent-root product becomes \((u_i a u_j^{-1})(u_j b u_k^{-1})=u_i ab u_k^{-1}\).

We check that every true relation supported on a set \(S\) of at most five coordinates acts trivially. Choose \(t\notin S\). For parameters indexed by \(S\), the two groups \[U_t(v)=\prod_{i\in S}x_{it}(v_i),\qquad V_t(w)=\prod_{i\in S}x_{ti}(w_i)\] are additive abelian groups. Their maps to elementary matrices are injective, since their parameters occur in distinct matrix positions and no cross product occurs inside either strip.

The assigned action of \(e_{ab}(r)\), with \(a,b\in S\), sends \(v_a\) to \(v_a+r v_b\) in the first strip. In the second it sends \(w_b\) to \(w_b-w_a r\). To see the latter formula directly, use \[[x_{ta}(w_a),x_{ab}(r)]=x_{tb}(w_a r);\] the right side commutes with both factors, so reversing the commutator replaces its parameter by its negative. A diagonal \(d_a(u)\) sends \(v_a\) to \(u v_a\) and \(w_a\) to \(w_a u^{-1}\). Thus a word with matrix product \(M\) supported on \(S\) acts on these two strips by \[v\longmapsto Mv,\qquad w\longmapsto wM^{-1}.\] These formulas preserve the order of all noncommutative products. A true relation has \(M=I\), so fixes both strips pointwise. Repeating this calculation for each \(t\notin S\) fixes every root with exactly one index in \(S\). It also fixes every root supported outside \(S\). Finally, for \(i,j\in S\), \[x_{ij}(a)=[x_{it}(a),x_{tj}(1)],\] so it fixes the internal roots as well. Exactly one outside coordinate is needed for this argument.

Proposition 27 now gives a homomorphism \(H_n\to\operatorname{Aut}(\mathop{\mathrm{St}}_n(R))\). On the image of each Steinberg generator it is conjugation by that generator. Hence for every \(z\in\mathop{\mathrm{St}}_n(R)\), the action of its matrix image is conjugation by \(z\). If \(z\in J_n\), that matrix image is the identity. Therefore \(z\) commutes with every element of \(\mathop{\mathrm{St}}_n(R)\). ◻

Proof. Elementary generators normalize their own generated subgroup, and diagonal conjugation preserves each elementary root subgroup. Lemma 25 therefore proves normality.

In the presentation of Proposition 27, kill all elementary generators. Elementary swap words then become trivial, so the conjugation relation for a swap identifies \(d_i(u)\) with \(d_j(u)\) for every pair of positions. Diagonals in different positions commute. We may consequently use a single generator \(d(u)\) for each unit. Every remaining defining relation is obtained from a true matrix relation on at most five coordinates by deleting elementary generators and replacing each \(d_i(u)\) by \(d(u)\).

This list of relations is independent of \(n\geq5\). Indeed, whether a word supported on \(S\) is a true relation depends only on its matrix block on \(S\), and not on the other coordinates. Every such word can be relabeled onto at most five fixed coordinates, and all those relations already occur in rank five. Inclusion is the identity on the resulting unit generators and on their relations, proving the assertion. ◻

Proof. First let the quotient group \(L\) be finite. Choose normalized set-theoretic lifts and write their additive multiplication defect as \(f(g,h)\in\mathbb Q\). Associativity says \[f(g,h)+f(gh,t)=f(h,t)+f(g,ht).\] Define \(b(g)=|L|^{-1}\sum_{t\in L}f(g,t)\). Averaging this identity over \(t\) gives \[f(g,h)=b(g)+b(h)-b(gh).\] Changing the chosen lift of \(g\) by the central element \(-b(g)\) therefore makes it a homomorphic splitting. Two splittings differ by a homomorphism \(L\to\mathbb Q\), which must be zero.

If \(L\) is locally finite, apply the finite result to the inverse image of each finite subgroup. Uniqueness makes the splittings compatible under inclusion. Every finite set of elements of \(L\) lies in a finite subgroup, so these splittings glue to a unique homomorphic splitting on \(L\). ◻

Proof. Every upper unitriangular subgroup over \(R\), for any ordering of the coordinates, is locally finite. To see this, start with finitely many unitriangular matrices and collect their entries above the diagonal in a finite set \(S\). Entries of products and inverses are prime-field linear combinations of words in \(S\) of length at most \(n-1\). Indeed, every such product follows a strictly increasing sequence of coordinate indices; the inverse formula is the finite geometric series for a strictly triangular matrix and has the same property. There are finitely many words of these bounded lengths, and their \(\mathbb F_2\)-span is finite. Only finitely many matrices can consequently occur in the subgroup generated by the original matrices.

Let \[1\longrightarrow\mathbb Q\xrightarrow{\iota}X \longrightarrow\mathop{\mathrm{E}}_n(R)\longrightarrow1\] be a central extension. Lemma 30 gives a unique splitting on each unitriangular subgroup. Their root lifts agree whenever a root occurs in different orderings: the root group itself is locally finite and has a unique splitting. These root lifts satisfy every Steinberg relation. Addition is a relation in one root group. A consecutive-root commutator relation fits in a unitriangular group with its three indices in the path order. A commuting relation fits in a unitriangular group as well: the two directed edges specified by its root positions have no directed cycle, since the opposite-root case is excluded. Extend the resulting partial ordering to an ordering of all coordinates. In each case the relevant splitting is a homomorphism, so proves the relation among lifts. We have obtained a homomorphism \[f:\mathop{\mathrm{St}}_n(R)\longrightarrow X\] over \(\mathop{\mathrm{E}}_n(R)\). Its restriction to \(J_n\) lands in the prescribed central copy of \(\mathbb Q\) and defines \(\varphi:J_n\to\mathbb Q\). The map \(f\) is unique: two such maps differ pointwise by a homomorphism from the perfect group \(\mathop{\mathrm{St}}_n(R)\) to the central abelian group \(\mathbb Q\). Perfectness also follows directly from \(x_{ij}(a)=[x_{ik}(a),x_{kj}(1)]\).

Conversely, given \(\varphi\in\mathop{\mathrm{Hom}}(J_n,\mathbb Q)\), form \[X_\varphi= (\mathop{\mathrm{St}}_n(R)\times\mathbb Q)/ \{(j,-\varphi(j)):j\in J_n\}.\] The subgroup being divided out is central by Proposition 28. The map \(q\mapsto[(1,q)]\) is injective, and the induced map \(X_\varphi\to\mathop{\mathrm{E}}_n(R)\) is surjective with this central kernel. In fact \([(j,q)]=[(1,q+\varphi(j))]\) for \(j\in J_n\). Thus this is a central extension by the specified copy of \(\mathbb Q\). The map \(s\mapsto[(s,0)]\) gives its canonical root lifts, and its restriction to \(J_n\) recovers \(\varphi\).

Starting instead with the extension \(X\) and its map \(f\), the homomorphism \[\mathop{\mathrm{St}}_n(R)\times\mathbb Q\longrightarrow X,\qquad (s,q)\longmapsto f(s)\iota(q)\] is surjective: choose \(s\) with the same elementary image as any given element of \(X\), and account for the difference in the central kernel. Its kernel is exactly \(\{(j,-\varphi(j)):j\in J_n\}\). It therefore identifies \(X_\varphi\) with \(X\) as an extension. This proves the bijection. Restricting an extension to a smaller rank preserves its canonical root lifts, by their uniqueness. The bijection consequently commutes with rank restriction. ◻

Proof. First, taking \(N\)-coinvariants is exact over \(\mathbb Q\). Only preservation of injections needs proof. If \(U\subseteq V\) and \(u\in U\) becomes zero in \(V_N\), write \[u=\sum_i(n_i v_i-v_i).\] The subgroup \(B\) generated by the finitely many \(n_i\) is finite. The averaging operator \(e_B=|B|^{-1}\sum_{b\in B}b\) kills the right side, so \(e_Bu=0\). Hence \[u=u-e_Bu=|B|^{-1}\sum_{b\in B}(u-bu)\] is already zero in \(U_N\).

Take a free left \(\mathbb Q[K]\)-resolution \(L_\bullet\to M\). Coinvariants give an exact resolution \((L_\bullet)_N\to M_N\), free over \(\mathbb Q[K/N]\), because coinvariants of \(\mathbb Q[K]\) are \(\mathbb Q[K/N]\). Moreover, \[\mathbb Q\otimes_{\mathbb Q[K]}L_\bullet =\mathbb Q\otimes_{\mathbb Q[K/N]}(L_\bullet)_N.\] Computing homology by a resolution of the coefficient module gives the same answer as resolving the trivial right module: tensor the two resolutions together, and augment first in either direction. For each fixed index the other tensor factor is free, so the augmented rows or columns are exact. Finite elimination along the diagonals of this first-quadrant double complex identifies its total homology with both computations. This proves the assertion and its naturality. ◻

Proof. Complete a prescribed ordered frame to a matrix \(h\in H_m\), putting the prescribed columns in the last \(l\) positions. By Lemma 29, the complementary \(H_r\) represents every coset of \(\mathop{\mathrm{E}}_m(R)\) in \(H_m\), since \(r\geq9\). Multiplying \(h\) on the right by an appropriate complementary matrix therefore puts it in \(G\) without changing these columns. This proves transitivity.

In block form the unordered stabilizer in \(H_m\) consists of \[\begin{pmatrix}A&0\\B&P\end{pmatrix}, \qquad A\in H_r,\quad P\text{ a permutation matrix}.\] The permutation block is elementary in characteristic two, as is the strip that removes \(B\). The whole matrix belongs to \(\mathop{\mathrm{E}}_m(R)\) if and only if its block \(A\) does, by injectivity in Lemma 29. Thus projection onto \(A\) has image \(\mathop{\mathrm{E}}_r(R)\) and section \(A\mapsto\operatorname{diag}(A,I_l)\). Its kernel is the semidirect product of the additive group \(M_{l\times r}(R)\) with the finite symmetric group \(S_l\).

This kernel is locally finite. Given finitely many of its elements, take all permutation translates of their finitely many strips. Their span over \(\mathbb F_2\) is finite, and its semidirect product with \(S_l\) is a finite group containing the given elements.

The orientation character is the sign of \(P\). If \(l\geq2\), a transposition in \(N_l\) acts as \(-1\) on \(\mathbb Q_{\epsilon_l}\). Thus its coinvariants are zero: their defining relations include \(-a-a=-2a\). The characteristic of \(R\) does not change the rational orientation sign. Lemma 32 gives vanishing in every degree. If \(l=1\), the orientation module is trivial and the same Lemma identifies homology with that of \(\mathop{\mathrm{E}}_{m-1}(R)\). The projection induces this identification, and its complementary section induces the inverse. ◻

Proof. Put \(m=n+1\), \(G=\mathop{\mathrm{E}}_m(R)\), and let \(C_\bullet\) be the oriented simplicial chain complex of \(X_m\) over \(\mathbb Q\), with augmentation \(C_0\to\mathbb Q\). Fix a free right resolution \(P_\bullet\to\mathbb Q\) over \(\mathbb Q[G]\). Consider the first-quadrant double complex \[D_{p,q}=P_q\otimes_{\mathbb Q[G]}C_p,\] with horizontal differential induced by the simplicial boundary, vertical differential induced by the resolution, and total differential \(d=d_h+(-1)^p d_v\). Write \(T_\bullet\) for its total complex and \(A_\bullet=P_\bullet\otimes_{\mathbb Q[G]}\mathbb Q\).

The augmentation induces a chain map \(F:T_\bullet\to A_\bullet\). We verify explicitly that it induces an isomorphism in degree two. Adjoin column \(p=-1\) by setting \(C_{-1}=\mathbb Q\). The resulting total complex has the form \[K_j=T_j\oplus A_{j+1},\qquad d_K(t,a)=(d_Tt,F(t)-d_Aa).\] Every augmented horizontal row is exact at positions \(p=-1,0,1,2\), by Lemma 26 and the freeness of each \(P_q\). To kill a cycle of total degree \(j\leq2\) in \(K_\bullet\), choose its component of largest resolution degree \(q\). That component is horizontally closed, since no component of larger \(q\) contributes to its horizontal target. Its horizontal position is \(p=j-q\leq2\). Row exactness supplies a horizontal primitive in position \((p+1,q)\). Subtracting its total boundary removes the chosen component and introduces only smaller resolution degrees. Repeating this finite procedure kills the cycle. In particular \(H_1(K_\bullet)=H_2(K_\bullet)=0\). The long exact sequence of \[0\longrightarrow A_\bullet[-1] \longrightarrow K_\bullet\longrightarrow T_\bullet \longrightarrow0\] therefore shows that \(F_*:H_2(T_\bullet)\to H_2(A_\bullet)\) is an isomorphism. Here the connecting map is precisely the augmentation map \(F_*\).

For \(0\leq p\leq3\), Lemma 33 gives a single orbit of simplices, and the oriented chain module is \[C_p\cong\mathbb Q[G]\otimes_{\mathbb Q[K_{p+1}]}\mathbb Q_{\epsilon_{p+1}}.\] The stabilizer is that of the unordered simplex, with its orientation sign on the coefficient line. Tensoring with the right resolution identifies the vertical column with \(P_\bullet\otimes_{\mathbb Q[K_{p+1}]}\mathbb Q_{\epsilon_{p+1}}\). Restriction of \(P_\bullet\) to a subgroup is still an exact free resolution, so the vertical column homology is the stabilizer homology in Lemma 33. Consequently columns one, two, and three have zero homology in every degree. Column zero has homology \(H_q(\mathop{\mathrm{E}}_{m-1}(R);\mathbb Q)\).

Inclusion of column zero induces an isomorphism onto \(H_2(T_\bullet)\). For surjectivity, remove the component in position \((2,0)\) of a total two-cycle using the vanishing of vertical homology there. Subtracting the chosen total boundary leaves a cycle whose largest possible column is one. Remove its component in \((1,1)\) in the same way. The remaining cycle belongs to column zero. For injectivity, suppose a column-zero two-cycle bounds a total three-chain. Remove successively that chain’s components in \((3,0)\), \((2,1)\), and \((1,2)\) by subtracting total boundaries. At each step the component to remove is vertically closed, because the boundary is in column zero and all higher components have already been removed. The requisite vertical homology vanishes. The resulting bounding chain is in column zero, as required. Columns of index at least four cannot occur in these cycles or bounding chains. Equivalently, the only possible incoming differentials to bidegree \((0,2)\) have sources \((1,2)\), \((2,1)\), and \((3,0)\), all of which vanish.

For column zero choose the representative vertex \(e_m\). Under the chain identification above, its map through the augmentation is the map induced by inclusion of its stabilizer into \(G\). The complementary section from \(\mathop{\mathrm{E}}_{m-1}(R)\) is exactly \(A\mapsto\operatorname{diag}(A,1)\). Combining the two proved isomorphisms thus gives the asserted standard stabilization map. ◻

Proof. Proposition 34 and the bar-cochain identification above show that restriction gives a bijection on central extension classes by \(\mathbb Q\). By Lemma 31, this is precisely restriction on the displayed Hom groups. Restriction is a homomorphism of these Hom groups, so its bijectivity makes it an isomorphism. ◻

Proof. The image of \(a\) in \(A\otimes_{\mathbb Z}\mathbb Q\) is zero exactly when some positive integer kills \(a\): this is the defining equality criterion in localization at the nonzero integers. If that image is nonzero, extend it to a basis of the \(\mathbb Q\)-vector space \(A\otimes_{\mathbb Z}\mathbb Q\). The functional taking that basis vector to \(1\) and the other basis vectors to \(0\), composed with the natural map from \(A\), is a homomorphism detecting \(a\). ◻

Proof. It is abelian by Proposition 28. Suppose that \(\varphi:J_n(\mathbb F_2)\longrightarrow\mathbb Q\) is a homomorphism. Form the central extension \[H=\bigl(\mathop{\mathrm{St}}_n(\mathbb F_2)\times\mathbb Q\bigr) \big/\{(z,-\varphi(z)):z\in J_n(\mathbb F_2)\}.\] The copy of \(\mathbb Q\) injects into \(H\), and the quotient by that copy is \(\mathop{\mathrm{E}}_n(\mathbb F_2)\). This last group is finite. By Lemma 30, its central extension by \(\mathbb Q\) splits. Projection onto the resulting \(\mathbb Q\) factor, composed with \(\mathop{\mathrm{St}}_n(\mathbb F_2)\longrightarrow H\), is a homomorphism from a perfect group to an abelian group, and is therefore zero. On the kernel \(J_n(\mathbb F_2)\) it is \(\varphi\). Thus every such \(\varphi\) is zero, and Lemma 36 proves the claim. ◻

Proof. For a transposition interchanging \(a\) and \(b\), take \[p=x_{ab}(1)x_{ba}(1)x_{ab}(1).\] For a coordinate \(c\) outside \(\{a,b\}\), the two commuting roots \(x_{ac}(r)\) and \(x_{bc}(s)\) form an additive column strip. Conjugation by \(x_{ab}(1)\) adds the second entry to the first, by the consecutive Steinberg relation. The analogous statement holds for \(x_{ba}(1)\). The three indicated additions interchange the two entries in characteristic two. Thus conjugation by \(p\) interchanges \(x_{ac}(r)\) and \(x_{bc}(r)\). Applying the same relations to the incoming row strip interchanges \(x_{ca}(r)\) and \(x_{cb}(r)\). Roots with both indices outside \(\{a,b\}\) commute with all three factors of \(p\).

For the remaining roots, use an outside coordinate \(c\) and the identities \[x_{ab}(r)=[x_{ac}(r),x_{cb}(1)],\qquad x_{ba}(r)=[x_{bc}(r),x_{ca}(1)].\] The already established strip action interchanges these two roots as well. Decomposing a permutation into transpositions and composing their exact actions gives the result. ◻

Proof. The first two identities follow factor by factor from the root relations. In the third identity, the only nontrivial commutators are \[[x_{(i,s),(j,t)}(a_{st}),x_{(j,t),(k,v)}(b_{tv})] =x_{(i,s),(k,v)}(a_{st}b_{tv}).\] Every resulting root commutes with every root in either input block. The commutator therefore expands into the product of the displayed terms. Additivity at a fixed pair of coordinates gives the entries \(\sum_t a_{st}b_{tv}\) of \(AB\).

An elementary operation inside outer block \(i\) acts on the outgoing strip from \(i\) to \(j\) by left multiplication. This follows by the same commutator computation, with one of the two factors supported inside block \(i\). An operation inside block \(j\) acts by inverse right multiplication. There is no opposite-root case, since the other endpoint lies in a different outer block. Operations in any other block centralize the strip. These are group equalities in \(\mathop{\mathrm{St}}_{nN}(R)\).

Finally, Gaussian elimination over \(\mathbb F_2\) expresses \(P\) as a product of elementary matrices. All nonzero pivots equal \(1\), and a row interchange is the product of the three additions used in Lemma 38. Lift these elementary factors inside each outer block and apply the exact strip actions successively. This proves the last assertion. ◻

Proof. Call \(t-s\) the gap of the displayed root. Two positive-gap roots either commute or have a commutator root whose gap is the sum of their gaps. The two noncommuting possibilities are concatenation in either order. They cannot be opposite roots, since both gaps are positive. These statements follow directly from the Steinberg relations, using the inverse of a consecutive commutator for the reverse order.

For \(g\geq 1\), let \(U_g\) be generated by roots of gap at least \(g\); put \(U_N=1\). The preceding computation shows that \(U_g\) is normal in \(U\) and that interchanging two root factors changes the product only by factors of larger gap. It follows successively, for \(g=1,\ldots,N-1\), that any element of \(U\) can be written as an ordered product with one factor per pair of coordinates, in increasing gap, and with all coefficients at an identical pair added. To see this without an infinite collection process, first collect the finitely many gap-one positions modulo \(U_2\), then collect the residual element of \(U_2\) modulo \(U_3\), and continue until \(U_N=1\).

If the matrix of such a product is the identity, its entries of inner gap one are exactly the corresponding collected coefficients, so these vanish. Once all gaps below \(g\) have vanished, entries of gap \(g\) are likewise exactly their collected coefficients: a product of two remaining strictly upper entries has larger gap. Induction on \(g\) makes every coefficient zero. The original group element is therefore the identity.

A root with equal inner indices cannot be opposite to a positive-gap root. Its commutator with such a root is either trivial or again has that positive gap. Conjugating the generators of \(U\) therefore keeps them in \(U\), and the same argument applies to the inverse conjugation. ◻

Proof. For every polynomial entry \(a(t)\), the matrix \(a(T)\) is upper triangular and has diagonal entry \(a(\lambda)\) at each inner index. Split its block root into the commuting product of its diagonal terms and its strictly upper terms. By Lemma 40, the diagonal terms normalize \(U\), so all strictly upper terms in the whole word can be collected on the right. The diagonal terms at different inner indices commute. We obtain \[W_v(T)=\left(\prod_{s=1}^{N}\iota_s(v(\lambda))\right)z, \qquad z\in U.\] Both the word on the left and every \(v(\lambda)\) have identity matrix image. Hence the matrix image of \(z\) is the identity. Faithfulness of \(U\) gives \(z=1\). ◻

Proof. Write the \(h\)th block factor of \(W_v(C_N)\) as \(D_h F_h\), where \(D_h\) is the corresponding factor of \(W_v(S_N)\) and \(F_h\) is the product of its wrap entries. This splitting is exact by the commutativity of the roots in a single outer rectangle. Since \(d<N\), a term of degree \(b\) goes from inner row \(s\) to inner column \(s+b\), and wraps only when \(s+b>N\). Consequently every root in \(F_h\) has source inner index greater than \(N-\delta\) and target inner index at most \(\delta\).

For an integer \(r\geq 1\), consider the strip generated by roots whose source inner index is greater than \(N-r\delta\) and whose target inner index is at most \(r\delta\). As long as \(N>2r\delta\), these source and target sets are disjoint. All roots in the strip commute, and their matrix product is the identity plus the matrix of their entries. Additivity at a fixed coordinate pair shows that this strip injects into matrices.

Figure 2 displays the support condition on the inner indices; each band includes all outer indices.

We claim that conjugating an element of the strip of width \(r\delta\) by one truncated block factor \(D_h\), or by its inverse, keeps it in the strip of width \((r+1)\delta\), whenever \(r\leq m\). It is enough to check a strip root. Every constituent of \(D_h\) goes from an outer index \(i\) to a fixed different outer index \(j\), and has inner displacement between \(0\) and \(d\). All these constituents commute. A constituent initially commuting with the strip root can therefore be omitted when computing the conjugation: it also commutes with every conjugate of that root by the other constituents.

An interacting constituent can change the source endpoint only when its target is the old source; it then moves that endpoint left by at most \(d\). It can change the target endpoint only when its source is the old target; it then moves that endpoint right by at most \(d\). These assertions, including the coefficients in their prescribed multiplication order, are precisely the consecutive Steinberg relations and their reversed versions. No constituent can be opposite to a strip root: an edge from its low target to its high source would have displacement greater than \(d\), by the bound on \(N\). This exclusion also holds after one endpoint has moved. The source inner index minus the target inner index is then greater than \(N-(2r+1)\delta>\delta\), since \(r\leq m\) and \(N>2(m+1)\delta\). A constituent of displacement at most \(d\leq\delta\) therefore cannot be opposite to an intermediate root.

There is also no accumulation of many shifts at one endpoint during this single block factor. After a source change, that source has outer index \(i\), whereas every constituent has target outer index \(j\ne i\), so it cannot change the source again. After a target change, that target has outer index \(j\), whereas every constituent has source outer index \(i\), so it cannot change the target again. Both endpoints may change, but each changes at most once. Every root produced thus belongs to the strip of width \((r+1)\delta\). The argument applies to a product of strip roots and to inverse conjugation as well. In characteristic two, each block factor is in fact its own inverse.

Collecting all \(D_h\) to the left now gives \[W_v(C_N)=W_v(S_N)\,z,\] where \(z\) is a product of the wrap factors \(F_h\) conjugated by suffixes of the truncated factors. More explicitly, set \(D_{>h}=D_{h+1}\cdots D_m\) and \(D_{>m}=1\). The group identity \[\prod_{h=1}^m(D_hF_h) =(D_1\cdots D_m) \prod_{h=1}^m(D_{>h}^{-1}F_hD_{>h})\] keeps the last product in increasing order of \(h\). Thus no correction factor is used to conjugate another correction. Each suffix has at most \(m\) factors. The claim puts every resulting correction in the single strip \[\text{source inner index}>N-(m+1)\delta, \qquad \text{target inner index}\leq(m+1)\delta.\] Its endpoint sets are disjoint by our choice of \(N\). Both evaluated words have identity matrix image, so \(z\) also has identity matrix image. Faithfulness of this strip gives \(z=1\), as required. ◻

Proof. Choose a finite root word representing \(u\) and apply the grading homomorphism \(\gamma\) to its entries, obtaining the word \(u(t)\) from the opening of this section. Its matrix image is the identity, \(u(1)\) represents \(u\), and \(u(0)\) represents an element of \(J_n(\mathbb F_2)\) before the field is included into \(R\).

If the word is empty there is nothing to prove. Otherwise let \(m\) be its number of root factors and \(d\) the maximum degree of their entries. Choose a power of two \(N\) with \[N>2(m+1)\max\{1,d\},\] and set \(W=W_u(C_N)\in\mathop{\mathrm{St}}_{nN}(R)\).

Since \(C_N^N=I\) and \(N\) is a power of two, the binomial identity in characteristic two gives \((C_N-I)^N=0\). A nilpotent linear map has an upper triangular matrix with zero diagonal in a basis adapted to its successive kernels. Thus some \(P\in\mathop{\mathrm{GL}}_N(\mathbb F_2)\) makes \(P^{-1}C_NP\) upper triangular with all diagonal entries equal to \(1\). Lemma 39 gives an exact conjugation between the two evaluated root words. Both belong to \(J_{nN}(R)\), which is central by Proposition 28; that conjugation consequently fixes \(W\). Lemma 41 now yields \[W=\prod_{s=1}^{N}\iota_s(u).\] Each \(\iota_s(u)\) belongs to the central kernel at rank \(nN\). By Lemma 38, a permutation of coordinates conjugates any one of these coordinate images to any other. Centrality therefore makes them equal, and \[ W=\iota_1(u)^N. \tag{36}\]

On the other hand, Lemma 42 and then Lemma 41, now with diagonal value \(0\), give \[ W=W_u(S_N)=\prod_{s=1}^{N}\iota_s(u(0)). \tag{37}\] By Lemma 37, \(u(0)\) has finite order. Its coordinate images commute, so their product in (37) has finite order as well. It follows from (36) that \(\iota_1(u)\) has finite order: if \(W^a=1\), then \(\iota_1(u)^{Na}=1\).

Finally, a permutation of the \(nN\) coordinates carries the ordered coordinates \((1,1),\ldots,(n,1)\) to the first \(n\) usual coordinates. Lemma 38 identifies \(\iota_1(u)\) with a conjugate of the usual stabilized image of \(u\). Hence that stabilized image is torsion. This argument used only coordinate homomorphisms and never their injectivity. ◻

Proof. Fix \(u\in J_n(R)\) and a homomorphism \(\varphi:J_n(R)\longrightarrow\mathbb Q\). Proposition 43 provides a rank \(q\geq n\) at which the image of \(u\) has finite order. Successively applying Proposition 35 extends \(\varphi\) to a homomorphism \(J_q(R)\longrightarrow\mathbb Q\). This extension kills the torsion image of \(u\), so \(\varphi(u)=0\). The group \(J_n(R)\) is abelian by Proposition 28. Lemma 36 therefore makes \(u\) torsion. Again, no stabilization map was required to be injective. ◻

Proof of Theorem 1. Take the algebra \(R\) from Theorem 18 and put \(G=\mathop{\mathrm{St}}_{12}(R)\). Theorem 21 gives an ordinary finite presentation of \(G\). Its image \(\mathop{\mathrm{E}}_{12}(R)\) is infinite, because distinct entries in any one elementary matrix position give distinct matrices and \(R\) is infinite. Thus \(G\) is infinite.

By Lemma 24, the elementary matrix group \(\mathop{\mathrm{E}}_{12}(R)\) is periodic. For \(g\in G\), choose a positive integer \(a\) killing its elementary matrix image. Then \(g^a\in J_{12}(R)\), and Theorem 44 gives a positive integer \(b\) with \((g^a)^b=1\). Consequently every element of \(G\) has finite order. The group \(G\) is the required infinite, finitely presented periodic group. ◻

Proof of Corollary 2. Theorem 18 presents \(R\) as a unital associative \(\mathbb F_2\)-algebra on finitely many generators. Since \(\mathbb F_2\) is the prime field, those generators together with \(1\) generate \(R\) as a ring. Ershov and Jaikin-Zapirain prove that \(\mathop{\mathrm{St}}_n(S)\) has property \((T)\) for every finitely generated associative ring \(S\) with \(1\) and every \(n\geq3\) [5]. This applies directly to \(S=R\) and \(n=12\). Infinitude, finite presentation, and periodicity are those of Theorem 1.

Write \(G=\mathop{\mathrm{St}}_{12}(R)\). If \(G\) were amenable, normalized characteristic functions of Følner sets would give almost invariant unit vectors in the left regular representation on \(\ell^2(G)\). Property \((T)\) would then give a nonzero invariant vector. Such a vector is constant on \(G\), and a nonzero constant function on the infinite group \(G\) is not square-summable. Hence \(G\) is nonamenable. ◻