Proof. Soundness of the expression. Consider a factorization accepted by the expression on the right of (2). The outer intersection puts the word in \(D^*\), so it has its true episode boundaries. A \(W\)-factor starting at such a boundary consumes a sequence of complete episodes: its factorization into members of \(D'\subseteq E\) agrees with the ambient factorization by the prefix-code property.

In the second term, pair each \(P\)-factor with the following \(Q\)-factor. Condition (i) says that this pair consumes exactly the next episode and has the indicated input and output states. Induction through the alternating \(W\)-factors and these pairs proves both the boundary alignment and the required composite update. This includes the case in which the central star contributes no factors, leaving one explicit split. The first term \(W_{x,y}\) is already correct.

Completeness and height. Conversely, take a word in \(D^*\) with the required update. Split each episode outside \(D'\) using condition (ii), and absorb each intervening sequence of \(D'\)-episodes into its graph language \(W\). This gives the second term, unless there are no explicit splits, in which case it gives \(W_{x,y}\). Thus the displayed language is exact.

For the height estimate, \(D^*\) has height at most two. The central star has height at most \(1+\max\{1,b\}\), and all other operations are finite unions, concatenations, or intersections. The stated bound follows. ◻

Proof. Applying \(v\mapsto vL+c\) and then \(v\mapsto vA+d\) gives \(v\mapsto vLA+cA+d\). Hence the composite on any word of \(D^*\) has the form \(v\mapsto vL+c\), where \(L\) is the product of the episode linear parts in reading order. Its output at zero is \(c\). The displayed intersection says that the two outputs are \(y+f\) and \(f\), which is equivalent to \(vL=y\). The union ranges over the finite set of possible \(f\). Only finite Boolean operations are used. ◻

Proof. We first bound the probability of failure for one state and tuple, then show that all these failures can be avoided simultaneously. The length \(l\) is chosen only after both estimates are available.

Write \(q_U=|U|\). If \(m=1\) or \(q_U=1\), take \(l=1\) and \(\beta=0\). We therefore assume \(m,q_U>1\). For an integer \(l\) to be chosen, choose the values of \(\beta\) independently and uniformly in \(U\) at all points of \(M^l\). For each \((v,\mathbf d)\), let \(\mathcal B_{v,\mathbf d}\) be the event that no coordinate line through \(\mathbf d\) has the asserted constancy.

Condition on \(\beta(\mathbf d)\). Constancy along a specified line then prescribes the values of \(\beta\) at its other \(m-1\) points, so has probability \(q_U^{1-m}\). Different coordinate lines through \(\mathbf d\) have disjoint sets of noncentral points. Their constancy events are therefore independent under this conditioning, and the conditional probability of failure does not depend on the center value. Consequently \[\Pr(\mathcal B_{v,\mathbf d}) =p_l:=(1-q_U^{1-m})^l.\]

An event \(\mathcal B_{v,\mathbf d}\) uses only the random values at points of Hamming distance at most one from \(\mathbf d\). It is thus independent of the joint family of events whose centers have distance greater than two from \(\mathbf d\). The number of potentially dependent events is at most \[q_U\left(1+l(m-1)+\binom l2(m-1)^2\right)-1 \ \le\ D_l:=q_U(1+lm+l^2m^2).\] This count includes all possible input vectors at each nearby center.

We use a local-lemma argument (Erdős and Lovász 1975, sec. 2, pp. 616–617), recalling the required finite probability estimate with its proof. Suppose a finite family of events has a dependency graph of maximum degree at most \(D\ge1\): each event is independent of the joint family of its nonneighbors. If every event has probability at most \(u(1-u)^D\), where \(0<u<1\), then their simultaneous nonoccurrence has positive probability.

For completeness, induct on the size of a conditioning set to show that its nonoccurrence has positive probability and that the conditional probability of any other event is at most \(u\). The assertion with an empty conditioning set follows from the probability bound. Positivity for a set of size \(k\) follows by removing one member and applying the conditional bound for size \(k-1\). To prove the conditional bound for an event \(A\) and a set \(S\) of size \(k\) not containing it, partition \(S\) into its neighbors \(S_1\) and nonneighbors \(S_0\). If \(S_1\) is empty, joint independence gives the unconditional bound. Otherwise, \[\Pr\left(A\,\middle|\,\bigcap_{B\in S}B^c\right) \le \frac{\Pr\left(A\,\middle|\,\bigcap_{B\in S_0}B^c\right)} {\Pr\left(\bigcap_{B\in S_1}B^c\,\middle|\, \bigcap_{B\in S_0}B^c\right)} \le \frac{\Pr(A)}{(1-u)^{|S_1|}} \le u.\] The denominator is bounded by revealing the members of \(S_1\) successively: every conditional set then has size at most \(k-1\), so the induction applies. The numerator uses joint independence from \(S_0\). This completes the induction and proves the estimate.

Apply the estimate with \(D=D_l\) and \(u=1/(2D_l)\). Bernoulli’s inequality gives \[u(1-u)^{D_l} =\frac1{2D_l}\left(1-\frac1{2D_l}\right)^{D_l} \ge\frac1{4D_l}.\] The quantity \(p_l\) decays exponentially in \(l\), whereas \(D_l\) grows quadratically. Choosing \(l\) large enough makes \(p_l\le1/(4D_l)\). There is therefore a choice of \(\beta\) for which no failure event occurs. Fix such a choice. ◻

Proof. List the finitely many length-\(K\) words having no positive period below \(d\). Process these words in a fixed order. When processing a word, mark all its starts that are not within distance less than \(d\) of a previously installed marker. Two starts added at this same step cannot be at distance \(a<d\): their overlap would make \(a\) a period of the listed word. Induction therefore proves separation of all markers.

Each step makes its decision from a length-\(K\) block and the decisions of earlier steps at offsets of magnitude less than \(d\). Induction over the finite list gives a finite inspection radius; enlarge it to at least \(K\). The construction commutes with translations. Finally, a listed word at \(z\) was either marked or prevented by a marker within distance less than \(d\). Thus marker absence on \([z-d,z+d]\) excludes every listed word at \(z\), as required. ◻

Proof. A block of period \(a\) extends by repeating its first \(a\) letters. Two two-sided words of respective periods \(a,b\) that agree on \(ab\) consecutive positions agree everywhere: both have period \(ab\). Here \(a,b<d\), so \(ab<d^2\). This proves both uniqueness and the assertion about overlapping blocks.

For the last assertion, every start in the inclusive interval \([z-H+d,z+H-d]\) has no marker within distance \(d\). Its length-\(K\) block therefore has a period below \(d\). Consecutive such blocks overlap sufficiently, so their extensions agree. Their union is the displayed interval, on which the extension agrees with the actual letters. ◻

Proof. The proof has three steps: the two boundaries stay in one class modulo \(dN\); the actual word contains enough periodic letters on both sides; and monoid-power periodicity then compares the ordered products.

A common boundary class. Consider one center \(z\). If its marker is present, usability leaves the boundary unchanged. If absent, the old and new periodic blocks have the same extension by Lemma 8: \(|h|\leq R_r<d_\circ\), and the blocks have length \(K_\circ>3d_\circ^2\). Thus the least period \(d\), smooth divisor \(\sigma\), and phase class \(x\bmod d\) are common.

If \(\sigma\leq S_r\), the displacement \(h\) is divisible by \(\sigma N\). Translation along the lattice gives \(y(z+h)=y(z)+h\), so the second residue in (16) is unchanged. Otherwise, usability says that no point of that lattice lies between any of the positions under consideration, so \(y(z+h)=y(z)\). In both cases the two boundaries belong to one class modulo \(dN\). Writing them in increasing order as \(b_-\leq b_+\), we have \[ b_+-b_-=kdN\quad(k\geq0). \tag{23}\]

Margins of actual periodic letters. By (17), both choices lie in \([z-R_r,z+R_r+Nd)\). Marker absence and Lemma 8 give a common run of actual letters containing \([z-H+d_\circ,z+H-d_\circ)\). The inequality (15) therefore implies that \[ [b_--md,\ b_++md) \subset [z-H+d_\circ,z+H-d_\circ) \tag{24}\] lies in that run. In particular both choices have the required periodic margins on their two sides.

Comparing products one endpoint at a time. Let \(c\in M\) be the product of one length-\(d\) period beginning in the phase of \(b_-\). For an incoming product from any fixed \(a\leq z-H\), comparison at \(b_--md\) gives the two factorizations \[T_{a,b_-}=A c^m,\qquad T_{a,b_+}=A c^{m+kN}.\] For an outgoing product to any fixed \(b\geq z+H\), comparison at \(b_++md\) gives \[T_{b_-,b}=c^{m+kN}C,\qquad T_{b_+,b}=c^m C.\] Here \(A\) and \(C\) are the products on the unchanged remaining portions. Equation (1) gives \(c^{m+kN}=c^m\). The equalities require neither cancellation nor reordering of factors.

The old and new boundary at each center lie within its unshifted window \([z_j-H,z_j+H]\), by the same estimates. Adjacent center windows are disjoint and separated by more than their required margins, since \(G>10H\). To compare an interval between successive boundaries, move its left endpoint while fixing its right endpoint, then move the right endpoint while fixing the new left endpoint. Each fixed opposite endpoint is outside the relevant window, so the local calculation applies. This proves (21). Its outgoing version at the last center proves (22). ◻

Proof. We count numerical difference tuples rather than choose digit pairs at every stage. Nonzero differences recover the slots; zero differences contribute only one value. This distinction prevents an unnecessary factor of \(P\) at each equal-digit coordinate.

Clock failures and recovery of the ordered pair. The clock part contributes at most \(C_{\rm cl}\), because \[q-(t+p-p')\equiv(q-t)+v_{p'}-v_p\pmod n.\] This is precisely the uniform translated-difference bound of Lemma 6. It remains to count pairs for which no scale is usable.

For an ordered pair of slots define its numerical digit differences \[D_r=f_r(x_r(p))-f_r(x_r(p')).\] The full tuple \((D_1,\ldots,D_R)\) determines a distinct ordered pair \(p\neq p'\). Indeed, it has at least \(k_0\) nonzero coordinates by (9). Each such coordinate determines both ordered digits by the uniqueness of the digit differences. These \(k_0\) evaluations determine each polynomial slot separately; unrevealed equal digits at zero coordinates therefore introduce no additional pairs.

Exceptional scales. For a pair with no usable scale, look at its origin \(t+p-p'\) and declare a coordinate \(r\) exceptional if \[ S_r<\sigma\leq S'_r \tag{27}\] at at least one absent center. At this fixed origin each center has one value of \(\sigma\), and the intervals \((S_r,S'_r]\) are disjoint. There are therefore at most \(Z\) exceptional coordinates. We may sum over all their possible sets, of which there are at most \(2^R\).

Descending count with all smaller digits still free. Fix such a set of exceptions. Count difference tuples in descending coordinate order. At an exceptional coordinate there are at most \(P^2\) possible differences. At a nonexceptional coordinate \(r\), fix the differences at all larger coordinates. For each center label \(j\), its possible positions are of the form \[ C_j+D_r+e,\qquad |e|\leq J_r,\qquad C_j=t+o_j+\sum_{b>r}D_b. \tag{28}\] The error includes the smaller-coordinate differences and \(\epsilon_p-\epsilon_{p'}\). This description fixes only the larger numerical differences; it does not assume that their underlying digit pairs have already been determined.

Since scale \(r\) fails to be usable, at some center label one of the following occurs:

1. A marker lies within \(R_r\) of one of the two search endpoints.

2. The search is absent at the center, \(\sigma>S'_r\), and a point of \(x+\sigma\mathbb Z\) lies within \(R_r\) of the center.

Indeed a change in the first marker of a translated search interval requires a marker to enter or leave through an endpoint. If the search does not change, failure of the second usability condition requires absence, \(\sigma>S_r\), and such a lattice point. Nonexceptionality then strengthens \(\sigma>S_r\) to \(\sigma>S'_r\).

For (a), the range swept by a given search endpoint, enlarged by \(R_r\), has diameter at most \[ 2(h'_r+J_r+R_r)<d_\circ. \tag{29}\] It contains at most one marker. A fixed marker can serve at most one nonzero value of \(D_r\): by (28), serving it restricts \(D_r\) to an interval of length \(2(J_r+R_r)\), whereas distinct nonzero digit differences are more widely separated. The two endpoints give at most two such values for each label.

For (b), all the centers under consideration for a fixed label lie in an interval of diameter at most \(2(h'_r+J_r)<d_\circ\). Among those centers whose searches are absent, their length-\(K_\circ\) blocks determine the same two-sided periodic extension, by Lemma 8: their start distance is less than \(d_\circ\), and \(K_\circ-d_\circ>d_\circ^2\). Only absent candidates enter this comparison. Present candidates between them are irrelevant, since overlap directly compares any two of the absent candidates’ seed blocks. Thus, even as \(D_r\), the lower digits, and the residue corrections vary, these absent candidates have one common least period, smooth divisor, phase, and lattice. This is where the long local blocks are needed in the descending count. If the common \(\sigma\) does not exceed \(S'_r\), none of these candidates can realize (b). Otherwise the enlarged center range has diameter less than \(\sigma\), by (11); it contains at most one point of the common lattice. That point accounts for at most one nonzero difference \(D_r\), by the same separation argument as for a marker.

Summing the budgets. There are \(Z\) center labels. Allowing also the single difference value zero, a nonexceptional coordinate therefore has at most \(3Z+1\) possibilities. It is not necessary to specify the equal digits when the difference is zero. Summing the descending count over exception sets bounds the number of full difference tuples by \[2^R P^{2Z}(3Z+1)^R.\] Since different ordered pairs give different tuples, this also bounds the number of pairs. Adding the clock contribution proves (26) with the constant in (8).

For a finite word, take any two-sided extension. Internal inspection windows give the same decisions, so the bound just proved applies unchanged. ◻

Proof. If the first marker in a moving search interval changes under a shift of magnitude at most \(w\), a marker must cross one of its endpoints. In particular, a marker lies within distance \(w\) of an original endpoint. Fix \(\gamma\in\Delta_0\) and fix one of the two endpoints. As \(p-p'\) ranges over \(\Delta_1\), the possible marker positions just described lie in an interval of diameter at most \(2h_1+2w<d_e\). This interval contains at most one end marker. For that marker, the required ordered difference \(p-p'\) lies in an interval of length \(2w\). The separation of the nonzero ordered differences gives at most one ordered pair with \(p\ne p'\). There are two endpoints and \(|\Delta_0|\) choices of \(\gamma\), proving the bound. With all windows available in a finite word, take any two-sided extension; none of the inspected marker decisions changes. ◻

Proof. Three finite envelopes. First translate the fixed buffer arrangements intact so that \[s<B_{1,0}<a_1<B_{0,0}<a_0\] with each buffer’s own boundaries and cut offsets in their prescribed order. Each difference \(B_{i,j}-s\) or \(a_i-s\) is a fixed offset. Set \[D=\operatorname{diam}\mathcal H+h_0+h_1+w+1.\] The main hypotheses differ from the true origin by at most \(\operatorname{diam}\mathcal H\). Aligned hypotheses differ by \(p-p'\), of magnitude at most \(h_i\); stage 1 adds \(\gamma\) of magnitude at most \(h_0\), and an \(A_1\) test adds at most \(w\). Thus \(D\) bounds all the end-system displacements that will be used.

Include in an inner envelope every inner search, inspection block, boundary, and main cut at origins displaced by at most \(D\), together with the additional shifts of magnitude at most \(\max_r R_r\) needed for usability. Every such position lies in \([t-C,t+C]\) for a finite constant \(C\ge D+1\) fixed before \(L\) is chosen. The marker radii and the bounded phase displacements used to define the \(B_j\) are included in \(C\). Choose \(L\) so that \(L-C>a_0-s\).

Likewise, include all end searches, their marker-inspection windows, and their seeds at displacements of magnitude at most \(D\). They lie in \([z_e(t)-C',z_e(t)+C']\) for a finite constant \(C'\) independent of \(o_e\); increase it so that \(C'>d_e+D\). Choose \(o_e\) so that \(o_e-C'>C\). Finally choose \[b_{\rm tail}>C'+d_e+1.\] Any anchor satisfies \(q\ge z_e(t)-d_e\). Therefore \(q+b_{\rm tail}>z_e(t)+C'+1\), proving that the true end is beyond the whole end envelope, and hence beyond both earlier envelopes.

Data on the required side of each cut. It remains to verify the sidedness of the computations. At a main cut \(k=t+c_j+\delta_r a\), the spacing of the main centers puts all inspections for boundaries through \(B_{j-1}\) before \(k\). For any guessed role \((j,r)\) in a suffix and any corresponding hypothesis \(t'=k-c_j-\delta_r a\), its first required center is \[z_j(t')=k+G/2-\delta_r a.\] Since \(0\le\delta_r a<R_r\) and \(G>10(H+r_\circ+\max_r R_r+1)\), its inspection windows, boundary, and all later main data lie after \(k\). This calculation holds independently of the role that produced the actual prefix cut.

For a buffer hypothesis \(p'\) of interval kind \(j\), the hypothetical start is \(s'=k-p'\). The first later boundary has offset \((B_{i,j}-s)-p'>0\) from \(k\), and all required preceding data lie on the prefix side when the hypothesis is true. The order \(1,0\) puts all stage-0 segment data after every stage-1 cut; hence the stage-1 suffix can form its later terminal table. All inner and end data are later still by the envelope choices. This proves every assertion. ◻

Proof. By Lemma 13, each decision window is internal before the prescribed endpoint. Its letters therefore remain unchanged under extension. A present-marker anchor is unchanged. In the absent case, the seed and its periodic extension are unchanged, and the first mismatch already seen remains the first mismatch. Thus any extension has the same prescribed endpoint. It can be a complete episode only if it ends there. ◻

Proof. Agreement of the actual anchors. An accepted argument contains every mandatory window, so all the candidate marker decisions agree with the corresponding decisions in the containing word. The true candidate therefore has its true value of \(\eta\). If the common value is a present marker, the reference’s anchor is immediately \(q\), and the exact-end test forces the claimed end.

Suppose instead that the common value is \(\bot\). Every candidate seed has a period less than \(d_e\). Their starts differ by at most \(w\), and \[K_e-w>d_e^2.\] Their seeds consequently determine the same two-sided periodic word by Lemma 8. The overlapping union of the seeds consists entirely of letters of this word. The true first mismatch is after the true seed. Every later candidate seed starts before the true seed ends, since its displacement is at most \(w<K_e\). The mismatch cannot precede the start of such a seed, and it cannot lie in any later candidate seed: that seed consists of actual letters of the same periodic word, whereas the mismatch letter differs from it. A candidate seed starting earlier also ends before the true seed ends. Thus the true first mismatch follows the entire seed union. It is therefore also the first mismatch after the reference seed.

Rejection of premature and excessive consumption. For a proposed suffix ending too soon, either a mandatory window is absent, or no earlier reference mismatch exists to certify its proposed endpoint. For a suffix extending too far, the actual first mismatch is still the first one, so its exact-end test still requires the original endpoint \(q+b_{\rm tail}\). Both cases are excluded.

Acceptance on a stable true episode. Finally, if \(A_1(t)\) is false, every candidate is within distance \(w\) of \(t\) and has the same \(\eta\) value. On the true suffix all windows are available by placement. The argument above shows that the reference exact-end rule supplies the true endpoint, so the guard accepts. ◻

Proof. Soundness for arbitrary independent tags. Suppose that a prefix of a word in \(E^*\) factors as \(P_x^{\rm main}Q_y^{\rm main}\). The prefix length is positive and its cut lies before the earliest possible first episode end, by Lemma 13. Hence there is a first episode \(e\). If the prefix chose \(k=t+h\) with \(h\in\mathcal H\), then the true origin \(t\) belongs to the suffix’s end-guard list. Its diameter is \(\operatorname{diam}\mathcal H<w\). Lemma 16 therefore forces the concatenation to end exactly at the end of \(e\), with its true anchor \(q\). This conclusion applies also to a proposed factor ending too early or extending into later episodes; it does not presume that the suffix has already identified the episode correctly.

Let \(\alpha\) and \(\lambda\) be the independently chosen prefix and suffix tags. The two residue tests give \((\alpha,\lambda)\in\mathcal E(q-t)\). If this edge set is contained in the diagonal, then \(\alpha=\lambda\). The true origin is consequently among the candidates for the selected role \((j,r)\) in the suffix test. At that candidate, the transmitted vector and preceding products are correct by the prefix checks, and the later products are correct by the suffix checks. Evaluating the constant function (33) at the actual \(d_j\) gives the true corrected vector at \(B_l\). Its transport to \(b\) proves \(g_{0,e}(x)=y\). If instead there is one off-diagonal edge, the prefix forces \(x=X(\alpha)\) and the suffix forces \(y=Y(\lambda)\). Formula (32) again gives \(g_{0,e}(x)=y\). Thus every accepted split is sound, regardless of which tags were guessed.

Completeness at one usable scale. Let \(e\in E\setminus D_0\) and fix \(x\in V\). Then \(q-t\pmod n\notin W\), some scale \(r\) is usable at \(t\), and \(A_1(t)\) fails. Put \(v=xT_{s,B_0}\). Lemma 4 chooses an interval \(j\) for which the corrected segment function is constant on the coordinate line through the true tuple \(\mathbf d\). Choose the tag with this \(j,r,v\), the true preceding products, and \[X=x,\qquad Y=g_{0,e}(x).\] The full diagonal is available outside \(W\). Since \(\gcd(\delta_r,n)=1\), the cuts \(t+c_j+\delta_r a\) for \(0\leq a<n\) realize every residue modulo \(n\). One therefore satisfies both clock tests for this tag.

The end guard succeeds because \(A_1(t)\) fails. Each candidate for the selected role differs from \(t\) by a multiple of \(\delta_r\) of magnitude at most \(R_r\). Lemma 10 leaves all its later interval products and its \(B_l\)-to-\(b\) product unchanged. Thus every candidate in the universal suffix check has the same constant function and the same final output as the true candidate. Notice that this uses only the later products: no claim about the vector at a shifted \(B_0\) is needed. The selected cut gives a split with output \(g_{0,e}(x)\). ◻

Proof. The initial total table is (35). Given any total table \(\Phi_i\), prescribing \(H_i\) on the basis defines a unique linear map. The maps \(\Phi_i(c)\) need not be linear as maps on \(U_i\): their values only select the images of basis vectors in the larger space. Formula (36) is therefore affine, with the linear part displayed in (37). Moreover, \[[v,1_M]\rho_i(T_{s,a_i})H_i =[v,T_{s,a_i}]H_i =[\Phi_i(T_{s,a_i})(v),1_M] =[g_{i,e}(v),1_M].\]

The lift has been constructed from a total table. We must still verify that the next suffix can compute such a table without the earlier prefix. This is the precise role of the reversed physical buffer order.

It remains to obtain the table \(\Phi_1\) needed to construct \(g_2\). The buffer order is \(1\) then \(0\), so \(a_1\) precedes all the segment data of buffer \(0\). Define, for every \(c\in M\) and \(z\in U_1\), \[ \Phi_1(c)(z)= \left(z\rho_0(cT_{a_1,a_0}) +\beta_0(\mathbf d_0)\rho_0(T_{B_{0,l_0},a_0})\right)H_0. \tag{38}\] The actual tuple \(\mathbf d_0\), the displayed suffix products, and the entire map \(H_0\) are available from the suffix after \(a_1\). Indeed, \(H_0\) is built from the total table \(\Phi_0\), whose values depend only on the later anchored schedule and suffix products; it does not require the true value of \(T_{s,a_0}\). More explicitly, with \(q,t,\mathbf d,A,C\) fixed by those later data, the suffix enumerates (35) for every \(c'\in M\) and \(v\in U_0\). Those values give every basis image of \(H_0\), including images indexed by infeasible prefix values. Thus (38) is a total table with the required dependence. Substitution of \(c=T_{s,a_1}\) yields (36) for \(g_1\). The preceding construction then gives \(H_1\) and \(g_2\). All these maps are defined from the complete episode independently of any split or skipped class. ◻

Proof. For a sequence \(e_1\cdots e_k\in D^*\), the linear part of the affine composite of \(g_{i+1,e_1},\ldots,g_{i+1,e_k}\) is \(L_{i+1,e_1}\cdots L_{i+1,e_k}\), in reading order. Equation (37) shows that the distinguished basis vectors return to distinguished basis vectors after every episode. By induction, this product sends \([v,1_M]\) to \[[g_{i,e_k}(\cdots g_{i,e_1}(v)\cdots),1_M].\] If \(R_{\xi,\zeta}\) are graph tests for the affine composite on \(U_{i+1}\), the graph test for sending \(v\in U_i\) to \(w\in U_i\) is therefore \[\bigcup_{f\in U_{i+1}} \left(R_{[v,1_M],[w,1_M]+f}\cap R_{0,f}\right),\] by Lemma 3. The zero in \(R_{0,f}\) is the zero vector of \(U_{i+1}\). This formula applies to the entire sequence, including the empty sequence, and proves the claim. ◻

Proof. Soundness: decode the true offset and force the true end. Consider an accepted concatenation \(P_x^{(i)}Q_y^{(i)}\) at the start of a word in \(D_i^*\). The positive prefix cut lies before every possible first episode end, so there is a first episode \(e\in D_i\). If the prefix chose \(p\), then its true origin occurs in the suffix list as \[t=s+L=k+L-p=\tau_p.\]

At stage \(0\), the end guard therefore forces exact consumption of this first episode and supplies its true \(q\). The suffix also requires \(A_1(t)\) to fail. Since \(e\in D_0\), this implies \(A_0(t,q)\). The true candidate \(p\) thus satisfies the decoding predicate, so uniqueness forces the decoded \(p'\) to equal \(p\).

At stage \(1\), membership of \(e\) in \(D_1\) directly implies that \(p\) satisfies the decoding predicate. Every window in that predicate is mandatory and, on the true episode, lies inside the episode. An accepted proposed suffix therefore sees the same bounded data even if its proposed end was too early or too late. Uniqueness first forces \(p'=p\); the exact end rule at this correctly decoded origin then forces exact consumption of \(e\).

In both stages the prefix and suffix have consequently used the same kind and the true buffer schedule. The prefix supplies the correct vector at \(B_{i,0}\) and the preceding interval products; the suffix supplies the correct later products. Line constancy then gives the true corrected vector at \(B_{i,l_i}\). Its subsequent work action and terminal map \(H_i\) give exactly (36), proving \(g_{i+1,e}(x)=y\).

Completeness: count all lost offsets of the needed kind. Fix \(e\in D_i\setminus D_{i+1}\) and \(x\in U_{i+1}\). Apply Lemma 4 to the true buffer tuple and the vector \[v=x\rho_i(T_{s,B_{i,0}}).\] It gives an interval \(j\) and thus one required kind \((j,v,d_1,\ldots,d_{j-1})\). Every offset of that kind passes the prefix checks. There are more than \(C_i\) such offsets.

At stage \(0\), the condition \(e\notin D_1\) makes \(A_1\) false at all \(t+\gamma\), \(\gamma\in\Delta_0\). For every cut \(p\), all candidate origins are of this form, so the absence checks and the stable end guard pass and give the true \(q\). Moreover \(A_0(t,q)\) holds, so the true candidate passes the current decoding predicate. If an offset \(p\) fails uniqueness, some \(p'\ne p\) satisfies \(A_0(t+p-p',q)\). By Proposition 11, at most \(C_0\) ordered pairs \((p,p')\) have this property. In particular at most \(C_0\) offsets \(p\) can fail uniqueness.

At stage \(1\), true membership in \(D_1\) supplies the true candidate for every cut. A failure of uniqueness gives an ordered pair \(p\ne p'\) with \[\text{there exists }\gamma\in\Delta_0 \text{ with }A_1(t+p-p'+\gamma).\] Lemma 12 bounds the number of these pairs, and hence the number of lost offsets, by \(C_1\).

In either stage, a copy of the required kind remains. At its correctly decoded origin all later data are available by placement, and the affine-line check gives the required output \(g_{i+1,e}(x)\). This proves completeness. ◻

Proof. On \(D_2^*=\{\epsilon\}\), the graph tests for \(g_2\) are \(\{\epsilon\}\) for equal input and output and empty otherwise. Apply Proposition 20 at stage \(1\) and Lemma 2 to obtain graph tests for \(g_2\) on \(D_1^*\). Lemma 19 converts these to graph tests for \(g_1\) on \(D_1^*\).

Use those tests as the skipped-class tests in the stage-\(0\) application of Proposition 20. The split lemma gives graph tests for \(g_1\) on \(D_0^*\), and Lemma 19 recovers graph tests for \(g_0\) on \(D_0^*\). These are the skipped-class tests required by Proposition 17, whose application yields graph tests for \(g_0\) on \(E^*\).

Finally, Lemma 3 recovers the product of the linear parts of the maps \(g_{0,e}\). By (32), these are the true \(T_e\) actions on \(V\). Applying their product to the basis vector indexed by \(1_M\) identifies the \(T\)-value of the whole episode sequence. Only the three stated split applications introduce stars through the split formula; all recovery operations are finite Boolean operations. Section 7 will establish the height bounds for the component languages and complete the count. ◻

Proof. Ultimately periodic data and explicit expressions. Fix a template. For sufficiently large \(h\), all the indicated availability and order relations stabilize. Letters at a bounded distance from the start or end also stabilize, since increasing \(h\) inserts a full copy of \(b\). A product between boundedly separated endpoints then stabilizes. A product spanning the growing middle has the form \[u\,T(b)^{h-j}\,v\] for fixed \(u,v\in M\) and a fixed integer \(j\), once \(h\) is sufficiently large. This follows by separating its fixed initial and terminal pieces from its complete copies of \(b\). Powers of an element of a finite monoid are ultimately periodic: if two powers coincide, multiplying by further powers gives the eventual period. Lengths modulo any fixed integer are periodic in \(h\). Thus the entire finite data array is ultimately periodic. A fixed finite computation from this array, including a universal or uniqueness check on a fixed finite list, remains ultimately periodic.

Let the resulting accepted exponents have period \(f>0\) after a threshold. They are a finite set together with finitely many progressions \(h_0+f\mathbb N\). Each progression contributes the expression \[a\,b^{h_0}\,(b^f)^*\,c,\] where the displayed fixed powers are finite words. These expressions have height one; the exceptional words have height zero. A finite union proves the first assertion, including a finite number of templates and finite exceptions.

The template cover for an independent exact-end test. For the final assertion, fix one possible end-rule origin relative to the argument start. The present-marker branch has a bounded anchor and therefore bounded total length. For the absent-marker branch, the seed is at a fixed offset and has fixed length. Make finite choices of all letters through the seed, of its short period and phase, and of the fixed-length tail beginning at the first mismatch. These choices fix a prefix \(a\) through the seed and a nonempty period word \(b\) beginning at the next position. If the mismatch occurs after \(h\) full copies of \(b\) and a partial copy of length \(r<|b|\), place that partial copy, the mismatching letter, and its remaining \(b_{\rm tail}-1\) letters in \(c\). There are finitely many such choices, and the mismatching letter is required to differ from the next periodic letter. They give exactly templates (39) for this continuation and end. The bounded marker and availability conditions can still be tested on the templates. Taking the finite union over possible end-rule origins proves the assertion. ◻

Proof. We first identify the single end rule that supplies each template cover, then verify that every remaining operation is a finite calculation from the allowed data. No part of this argument assumes that a standalone suffix has guessed the true episode origin.

All prefix cuts come from fixed finite sets of offsets, so the lengths of \(P_x\) words are bounded. Hence \(P_x\) is finite.

Every other language in the assertion has one exact-end rule on its entire argument. For \(E,D_0,D_1\) this is the true episode rule. A main or stage-0 suffix uses the reference rule in its end guard. A stage-1 suffix uses the rule at its uniquely decoded candidate. For a stage-1 suffix considered alone, first make a finite case distinction for the decoded offset \(p'\). The uniqueness predicate inspects all candidates’ bounded end-search windows and their finitely many \(\gamma\) translates; it contains no mismatch search. The case then has just the exact-end rule at \(k+L-p'\), whether or not that is a genuine episode origin. There are only finitely many reference or decoded offsets; we may take a finite union over them. Lemma 22 therefore supplies the finite template cover even for standalone suffixes with incorrect hypotheses.

We check that the remaining tests use only the finite data in that lemma. Marker searches and their stability checks inspect bounded windows at fixed nominal offsets. So do usability, the phase and lattice choices, and all additional candidate translates. Every selected main boundary lies within a fixed bounded neighborhood of its center. Buffer boundaries have fixed offsets. Consequently all partial products in the component computations have endpoints selected from finite sets of start offsets, except for the argument end itself.

The anchor supplied by the exact-end rule is the argument end minus \(b_{\rm tail}\). Thus the clock and \(A_0\) use only fixed-modulus differences between this end offset and their candidate origins. The predicates \(A_1\) and the stage-1 decoding predicate are wholly bounded. Equality, universal checks, and uniqueness over their finite candidate lists are finite calculations, with the mandatory availability convention retained for every candidate.

The affine-line checks range over finite vector spaces and the finite monoid \(M\). Their data consist of the specified states and actual partial products just described. The tables \(\Phi_i\) and \(H_i\) are computed by their explicit formulas using hypothetical elements of \(M\) and actual suffix products and schedule data. Their finite recursion does not invoke a graph test on an episode sequence. The total-table property permits every hypothetical monoid value, so no extra prefix existence test is being imposed.

Finally, no translated candidate makes a second unbounded continuation search. The guards compare bounded marker data and use just their one reference rule. Stage 1 makes bounded decoding checks before applying the one decoded rule. Accordingly all remaining acceptance conditions are fixed finite calculations from the template data. Applying Lemma 22 proves the bounds. Every resulting expression uses finite words in \(\Sigma^*\) and Boolean operations, concatenation, and stars over \(\Sigma\); no auxiliary tag has become an input letter. ◻

Proof. Product tests on the incomplete tail. Choose a fixed length threshold exceeding all the bounded decision windows at a first start and all possible first-episode lengths in the present-marker case. A longer word in \(F\) cannot have a present end marker: that would already give an episode prefix. Its marker-absent seed has a fixed short-period continuation. Either no mismatch has yet occurred, or its first mismatch is at a position \(q\) satisfying \[|u|-q<b_{\rm tail}\] when the word \(u\) starts at position zero. Otherwise the prefix ending at \(q+b_{\rm tail}\) is a complete episode. All the required bounded windows for that prefix are internal by Lemma 13, even when the mismatch itself is early.

In the no-mismatch case, finite choices of the bounded initial word, period, phase, and final partial period give templates \(a b^h c\). In the mismatch case, append one of the finitely many possible post-mismatch portions of length less than \(b_{\rm tail}\); these again give finitely many such templates. Words below the threshold form a finite language. On every template the test \(T(u)=d\) is an ultimately periodic monoid-product test, so Lemma 22 gives a height-one language with that value on the template cover. Intersecting with \(F\) gives exactly \(F\cap T^{-1}(d)\) and keeps the same bound.

Unique parsing. Repeatedly remove an episode prefix while one exists. Every episode is nonempty, so this procedure terminates, and the remaining word is in \(F\). Lemma 15 makes each removed prefix unique. Any alternative \(E^*F\) factorization must therefore remove the same successive episodes; it also cannot stop earlier while an episode prefix remains. This proves uniqueness. ◻

Proof of Theorem 1. The component bounds needed for the three applications of Lemma 2 are supplied by Proposition 23. If the skip graph tests have height at most \(b\), that lemma gives the new bound \[\max\{2,b+1\}.\] Indeed the episode-domain test \(D^*\) has height at most two, and the single star in the split formula lies over component and skip tests of height at most \(\max\{1,b\}\).

The stage-1 skipped class is \(D_2=\varnothing\), whose graph tests consist only of the empty-sequence tests and have height zero. In the order proved in Proposition 20 and Proposition 17, the bounds are therefore \[\underbrace{0}_{D_2^*} \ \longrightarrow\ \underbrace{2}_{\text{stage 1}} \ \longrightarrow\ \underbrace{3}_{\text{stage 0}} \ \longrightarrow\ \underbrace{4}_{\text{main split}}.\] The affine linear-part recoveries and distinguished-basis queries use only finite Boolean operations and do not raise these bounds. The linear part of the main episode update is the action of \(T_e\) on \(V\). Thus its recovered sequence tests determine \(T\) on \(E^*\), since the image of the identity basis vector identifies the monoid value.

Let \(A_d=E^*\cap T^{-1}(d)\) be the resulting height-at-most-four tests, and let \(F_d=F\cap T^{-1}(d)\) be the height-at-most-one tests from Lemma 24. For a language recognized by \(T\) with accepting subset \(S\subseteq M\), its expression is \[\bigcup_{\substack{d,f\in M\\df\in S}} A_d F_f.\] The factorization lemma and the morphism identity prove that this is exactly the desired language. Concatenation and finite union do not increase the maximum height, which is four. All expressions are over \(\Sigma\), proving the theorem. ◻