Finite Monoid Computations and a Uniform Generalized Star-Height Bound

Proof. Consider a word accepted by the right side of (2.1). Its membership in D^* fixes its actual episode parsing. In a factorization through the nontrivial branch, the initial W-factor is a sequence of D'-episodes. Prefix-code uniqueness makes these actual initial episodes. The adjacent P,Q factors now begin at a true boundary; condition (i), applied to the remaining word in D^*, makes them exactly the next episode and gives its indexed update. The next W-factor consumes actual skipped episodes. Inducting through the finite number of starred factors proves the claimed whole update. The W_{x,y} branch handles words without an explicit split.

Conversely, for a genuine episode sequence, split every episode outside D' using (ii) and collect consecutive skipped episodes into W-factors. The deterministic computation supplies the intervening state indices. If every episode is skipped, use W_{x,y}. This also handles \epsilon.

For the height statement, D^* has height at most two. The starred middle factor has height at most 1+\max\{1,H\}. All remaining operations and factors fit the asserted maximum.□

Proof. The composite of v\mapsto vA+b followed by v\mapsto vC+d is v\mapsto vAC+bC+d. Therefore the linear part of the composed update g_w is g_w(v)-g_w(0), with the desired product of linear parts. If R_{x,z} are its graph tests, then

is exactly the test for linear output y on input x. Both tests concern the same word and hence the same map.□

Proof. Suppose h<j are eligible. The prefix conditions for j determine every actual interval through z_h, and the suffix condition for h determines the product from z_h to C. Hence

This uses multiplication, without cancellation.

If T=T_*, every eligible pair fits \beta=0. If T\ne T_*, at most one block is eligible; choose its forced shift y_j-x_jT, or zero if none is eligible. These rules define \beta on every trial. For a perfect prediction, the block for (x,xT) is eligible for each x.□

Proof. We first specify finitely many cyclic coordinates and construct the sets and roster values in their product. At the end we identify this product with a single cyclic group. Put

Here K_{\mathrm{cl}} is fixed once and for all.

Partitions and coordinate layout. Choose a assignments of \Lambda to a left side and a right side, allowing either side to be empty, so that, whenever

some partition puts \alpha on the left, \beta on the right, and \gamma,\delta on the same side. We allow \gamma=\delta. To prove existence, independently assign each tag to a side with probability 1/2. The required assignment is feasible: if \{\gamma,\delta\} contains \alpha, put both on the left; if it contains \beta, put both on the right; and if it contains neither, put both on the left. The excluded equality in Equation (3.2) ensures that these prescriptions never force \alpha and \beta onto the same side. Specifying sides for at most four distinct tags has probability at least 1/16. There are at most m^4 constraints. With a independent partitions, the expected number that all partitions miss is at most

The number missed is a nonnegative integer, so some choice misses none. We give each of these a partitions one coordinate, called a first coordinate.

Also choose b partitions into Type 1 and Type 2 that separate every two distinct tags. For example, label the tags by distinct binary strings of length b, and use the bit at each position. When m=1, b=0 and there are no such partitions. Give each Type partition a batch of coordinates as follows. List every ordered list of K_{\mathrm{cl}} directed pairs (p,p') of distinct roster labels whose underlying unordered edges are distinct and form a forest. A forest here is a finite simple graph with no cycles. Give each such list one dedicated coordinate in the batch, and add spare coordinates if needed to make the batch size positive and odd. All these lists form a finite set. This defines a finite coordinate set \mathcal C before choosing any prime orders.

Choose pairwise distinct primes N_c, c\in\mathcal C, satisfying

This is possible recursively: the product of all primes at most any given finite bound, plus one, has a prime divisor exceeding that bound. At each step include the previously chosen primes in the bound. Write

For x\in\mathbb Z/N_c\mathbb Z, identify x/N_c with its point on \mathbb T=\mathbb R/\mathbb Z. On this circle write \|z\|_{\mathbb T}=\min_{j\in\mathbb Z}|z-j| and \operatorname{dist}_{\mathbb T}(z,A) =\min_{a'\in A}\|z-a'\|_{\mathbb T} for a nonempty finite set A.

The first coordinates. In the coordinate for a left/right partition, impose the requirements

Any nonzero total is a sum for a diagonal pair: put the total in the required nonzero summand and put zero in the other. At total zero, however, no edge between two tags on the same side is possible, since it would have exactly one nonzero summand.

Suppose an off-diagonal edge \alpha\to\beta occurs at a total \ell\in G. For any (\gamma,\delta) satisfying Equation (3.2), choose its separating partition. The edge \alpha\to\beta forces total zero in that coordinate, because its two summands are both required to be zero. The competing edge \gamma\to\delta is impossible there because its tags are on the same side. Thus the only other edge that could coexist with \alpha\to\beta is \beta\to\alpha. This argument also excludes every diagonal edge, because the constraints explicitly include \gamma=\delta.

Type 1 batches: all sums and separated differences. Put

For a tag of Type 1 in a batch, require in every coordinate c of that batch

The sums of the two center sets contain every sixth of the circle:

Every target z\in\mathbb T is therefore within 1/12 of some center sum a'+d'. Choose a signed adjustment \theta, with |\theta|\le1/12, such that z=a'+d'+\theta on the circle. The continuous summands a'+\theta/2 and d'+\theta/2 are each within 1/24 of their respective centers. If z is a point of the N_c-grid, round the first summand to the nearest grid point and define the second to be z minus the rounded first. Both summands then lie on the grid and each changes by circular distance at most 1/(2N_c). Since N_c>24,

Thus the Type 1 sumset is the entire batch group, with the choices made independently in its coordinates.

The two center sets have circular distance at least 1/6 from each other. Consequently, every Type 1 difference i-j satisfies

Type 2 batches: majority sums and differences. Suppose a batch has 2s+1 coordinates. Call a coordinate value small if its circular distance from zero is at most 1/100. For a tag of Type 2, both I_\alpha and J_\alpha require a strict majority, that is, at least s+1, of the batch coordinates to be small. There are no restrictions on the other coordinates.

Their sumset contains every target vector z with at least one small coordinate. Indeed, at one such coordinate set the first summand equal to z and the second to zero, making both small. Partition the other 2s coordinates into two sets of size s. On the first set make the first summand zero, and on the second set make the second summand zero; in each coordinate determine the remaining summand by the target. Both vectors have at least s+1 small coordinates. Conversely, the sets of small coordinates of two vectors satisfying the majority condition must intersect. Every Type 2 difference therefore satisfies

This argument also covers a one-coordinate batch, with s=0.

The exclusive graph alternative. Define each I_\alpha\subseteq G and J_\alpha\subseteq G by imposing all its first-coordinate and batch requirements. These requirements concern disjoint coordinate blocks. We already know that an off-diagonal edge can coexist only with its reversal. If both \alpha\to\beta and \beta\to\alpha occurred, there would be elements i_\alpha\in I_\alpha, j_\alpha\in J_\alpha, i_\beta\in I_\beta, and j_\beta\in J_\beta with

Choose a Type partition separating \alpha and \beta. In its batch the common difference would satisfy the bounds in both Equation (3.4) and Equation (3.5), which is impossible because 2/100<1/24. This proves the alternative in (ii) in G.

Let W\subseteq G be the union of the following obstructions:

1. (a)

   a first coordinate of the total is zero;

2. (b)

   in some Type batch, none of the total’s coordinates is small.

If \ell\notin W, every diagonal pair has a decomposition of \ell in every first coordinate and every batch, by the sumset arguments above. Combining these decompositions gives \ell\in I_\alpha+J_\alpha for every \alpha. The exclusive graph alternative then implies that the graph is the full diagonal. This proves (iii). No converse assertion about W is needed.

We have now established the graph alternative and the availability of all diagonal pairs outside W. It remains to choose the roster residues so that every translate produces few ordered pairs in W. The first coordinates and the Type batches require different counting arguments.

Roster values in the first coordinates. Enumerate \mathcal R=\{p_0,\ldots,p_{r-1}\}. In every first coordinate assign

The nonzero ordered integer differences are all distinct. For a positive difference with j>i, the factorization

determines i as the exponent of the largest power of two dividing the difference, and then determines j. The sign distinguishes the reverse ordering. For r\ge2, all signed differences lie between -(2^{r-1}-1) and 2^{r-1}-1; by Equation (3.3), their range has length less than N_c. Thus they remain distinct modulo N_c. For any fixed u\in G, at most one ordered pair p\ne p' can satisfy

This also holds when r\le1, since there are no such pairs.

Roster values in a dedicated coordinate. Consider a coordinate c dedicated to a list with directed pairs

Choose d_j\in\mathbb Z/N_c\mathbb Z by rounding j/K_{\mathrm{cl}} to the nearest point of the N_c-grid, so that

Prescribe (v_{\pi'_j})_c-(v_{\pi_j})_c=d_j. To realize these prescriptions, root each tree component and assign its root value zero. On traversing an edge to a previously unassigned vertex, add d_j if traversing from \pi_j to \pi'_j, and subtract d_j if traversing in the opposite direction. The absence of cycles means that each new vertex is assigned once, with no consistency condition left to check. Give isolated roster labels value zero. Spare coordinates can have arbitrary roster values, for example all zero. Distinct roster labels may receive the same value in a batch coordinate; only the prescribed edge differences will be used.

For every u_c\in\mathbb Z/N_c\mathbb Z, one of the equally spaced points j/K_{\mathrm{cl}} is within 1/(2K_{\mathrm{cl}}) of -u_c/N_c. For that edge,

using K_{\mathrm{cl}}=400 and N_c>400. Thus every translate makes at least one edge of this dedicated forest small in this coordinate.

The bound for one batch. Fix u\in G and a batch, and let S be the set of ordered pairs p\ne p' for which u+v_{p'}-v_p has no small coordinate in that batch. Suppose that |S|>4K_{\mathrm{cl}}^2. Forget directions and identify the two orientations of each unordered edge to obtain a simple graph on the nonisolated roster labels. This graph contains a forest with K_{\mathrm{cl}} edges. To see this, take a spanning forest, obtained by growing a tree in each connected component until all its vertices are reached. If its edge count f were less than K_{\mathrm{cl}}, then, writing v for its number of vertices and t for its number of components, we would have

Here each component has at least two vertices because isolated vertices were removed. But then |S|\le v(v-1)<4K_{\mathrm{cl}}^2, a contradiction.

Choose K_{\mathrm{cl}} forest edges, choose for each an orientation belonging to S, and order the resulting directed pairs. The batch already has a coordinate dedicated to this list. By Equation (3.6), one of its pairs has a small translated difference in that coordinate, contradicting membership in S. Consequently every batch contributes at most 4K_{\mathrm{cl}}^2 ordered pairs to the obstruction. The forest may depend on u; every possible directed list was allocated a coordinate in advance. If no such forest can be formed from the roster, the spanning-forest count alone gives the required bound, and the spare coordinates do not affect it.

Combining the estimates and the cyclic coordinates. Taking a union over the a first coordinates and b batches gives

Since \log 2>1/2,

It follows that the last bound is at most

Only the number of partitions enters this estimate. The number of coordinates within a batch, and the eventual modulus, may depend on the entire roster.

Finally put n=\prod_{c\in\mathcal C}N_c. The residue map

is an isomorphism of additive groups. For an explicit proof of surjectivity, n/N_c is nonzero modulo the prime N_c, so some multiple e_c of it is 1 modulo N_c; the same e_c is zero in all other coordinates. A prescribed tuple (x_c) is therefore the image of \sum_c x_ce_c. The kernel consists of integers divisible by every N_c, hence by their product, proving injectivity. Transport I_\alpha,J_\alpha,W, and all v_p through this isomorphism. All sum, difference, and translation statements are preserved, and every prime factor of n satisfies (i).

For m=1 the first-coordinate construction still uses the positive number a of coordinates, while no Type batches are needed. The separation constraints are vacuous, and the diagonal is available whenever all first totals are nonzero. Thus this case uses the same proof, without an empty product of moduli. Empty and singleton rosters have no ordered distinct pairs and were also included above. This completes the proof.□

Proof. List as v_1,\ldots,v_N all length-K words having no period below d. Start with no markers. At stage j, mark every occurrence of v_j whose start is at distance at least d from all markers installed at earlier stages. Two occurrences installed at this same stage cannot be less than d apart. Indeed a word in the list has K\ge d, since otherwise K itself would be a period below d. Starts at positive distance a<d\le K would therefore overlap and give v_j period a, a contradiction. Separation is preserved at every stage.

For locality, take r_0=K and r_j=K+j(d-1). If earlier decisions have radius r_{j-1}, deciding the stage-j rule at x requires its length-K block and the earlier decisions at x-(d-1),\ldots,x+(d-1). These are all determined in [x-r_j,x+r_j). The union with earlier markers is determined there too. Thus r=r_N suffices. The construction commutes with every integer translation.

If the block at z equals some v_j, at stage j its start is either marked or blocked by an earlier marker at distance less than d. That marker remains installed. Absence of a marker in [z-d,z+d] therefore excludes every word on the list and proves the last assertion. Locality proves extension independence.□

Proof. The integer ab is a period of both two-sided words. Given any position, translate it by a multiple of ab into the interval of agreement. Both letters are preserved by this translation, proving the first assertion.

For (i), any two blocks overlap in at least K-w>d^2 letters, more than the product of their two short periods. Their periodic extensions therefore agree. This also shows that choosing a different short period for any one block gives the same extension. Fixing one block now gives a common extension for them all. Their union is the interval from the least start to the greatest start plus K, since w<K; every letter there belongs to a block and has the asserted value.

For (ii), each indicated start x has [x-d,x+d]\subseteq[z-H,z+H], so Lemma 4.1 gives a period below d for its length-K block. Consecutive blocks overlap in K-1 letters, at least the product of their periods. The first assertion, applied successively, identifies all their extensions. The common extension retains, for example, the short period of the first block.□

Proof. If a first-marker result changes, a marker belongs to the symmetric difference of the two search intervals. Such a marker is within distance h of z-L or of z+L. As z ranges over I, each of these enlarged endpoint ranges has diameter D+2h<d and hence contains at most one marker. For a fixed marker and a fixed endpoint, the condition of being within distance h permits at most 2h+1 integer centers. Summing over the two endpoints proves (i). We only use the implication from a changed result to a crossing; an entering marker need not change the minimum.

For (ii), assign to a center z its first marker m strictly after z+L. It satisfies z+L<m\le z+L+h. Suppose distinct serving markers m<m' are assigned to centers z,z'. Since m' is the first marker after z'+L, we have m\le z'+L. The marker-free interval about z' then forces m\le z'-L-1. Combining this with m\ge z+L+1 gives z'-z\ge2L+2, contrary to the diameter hypothesis. Thus at most one marker serves the centers under consideration. For that fixed m,

which allows at most h integer centers. Finally, distinct ordered differences make the indexing map (p,p')\mapsto z_0+p-p' injective.□

Proof. Let e,f\in E, with e a prefix of f. Their starts and sampling origins coincide. All end-marker inspections used by e are internal to e, so the two words obtain the same value of \eta(t). A present marker immediately fixes the same anchor. If it is absent, the same seed fixes the same repetition. The first mismatch seen in e is present in f, and all earlier letters inspected for continuation coincide; hence their first mismatches coincide too. In either case |e|=q+B_{\rm tail}=|f|, proving the prefix-code assertion. The same argument, and locality of all bounded searches, prove the final claim.□

Proof. All bounded tests in the two factors inspect the same ambient letters. By locality they obtain the same results, including for false candidate origins. If the common value of \eta is a marker position, it is also \eta(t)=q, so the exact end requirement gives b=q+B_{\rm tail}.

Suppose instead that every value is \bot. The seed starts x_\tau=z_\bullet(\tau) have diameter at most w_E. By Equation (4.1) and Lemma 4.2, all seeds have one common two-sided extension \pi. The word agrees with \pi throughout their union

Thus the true first mismatch q, which occurs after the true seed, cannot lie inside any later seed. It follows that q\ge x_{\max}+K_\bullet. There is no mismatch between the end of any seed and q: before x_{\max}+K_\bullet this follows from the seed union, and afterwards it follows from the true first-mismatch rule. Hence every candidate seed has exactly the same first subsequent mismatch q.

For completeness this argument also excludes incorrectly truncated or extended proposed suffixes. Put q'=b-B_{\rm tail}. If q'<q, the proposed mismatch letter at q' is present in both factors and contradicts the continuation just proved. If q'>q, the proposed continuation reaches the visible mismatch at q and fails there. A suffix lacking any required bounded inspection or its claimed mismatch letter cannot pass the requirements in the first place. Therefore q'=q and b=b_0.

Finally, stability and t\in\mathcal T imply equality of \eta on \mathcal T. The same seed-union argument shows that the actual suffix satisfies the exact end rule for every reference.□

Proof. The bounded predicates have the same values on their common letters, so the passing true candidate cannot disappear in the proposed suffix. Uniqueness therefore identifies it. Apply Lemma 4.6 with the singleton reference set \{t\}; its equality condition is automatic.□

Proof. Take an arbitrary accepted prefix/suffix pair at a genuine episode boundary. The end guard gives exact consumption and the common total \ell. If \mathcal G_1(\ell) is diagonal, the tags match. The actual t then appears among (5.6). The prefix establishes all earlier boundaries and the suffix establishes all later boundaries, so \mathcal A(t) holds. Their joint checks give an ideally eligible pair of the actual current trial. Lemma 2.5, together with the ideal computations before and after that trial, gives F_{1,e}(x)=y.

If tags differ, the clock graph consists of that unique off-diagonal edge. The input and output checks fix x=X(\alpha), y=Y(\beta), so (5.5) fits the transfer. The calculations performed under possibly false roles introduce no competing input or output. These cases prove soundness for every independent pair of witnesses.

For e\in S_1 and input x, select a perfect trial and its block for the vector actually arriving there and its trial output. Choose the tag X=x, Y=F_{1,e}(x). Since \ell\notin W_1, this diagonal tag pair is available at some first residue. Its n_1 consecutive cut choices realize every such residue. Every role-origin differs from the true one by less than R_1, so future-boundary stability makes all suffix comparisons pass. End stability makes the independent guard pass. All required data are present, giving the desired split.□

Proof. Again the independent guard gives exact consumption and total \ell. For matching tags, their product, residue and context are actual. Since k=z_\lambda(t)+a, 0\le a<R_2, the prefix absence interval and (5.10) cover the full actual search [z_\lambda(t)-H,z_\lambda(t)+H]. Thus this boundary is absent and \neg\mathcal A(t) is proved by the successful split. The suffix has consequently evaluated \widehat F_{1,e} correctly. In the diagonal second-clock case its output is F_{2,e}(x). Mismatched tags fit the unique input/output pair in (5.9). This proves soundness without assuming correctness of unmatched context.

For availability, let e\in S_2, with the indicated center z. The marker property gives short-period K_\circ-blocks at all starts from z-H+d_\circ through z+H-d_\circ. Lemma 4.2 makes these one periodic run of some period d<d_\circ. The second inequality of (5.11) places all needed contexts and at least |M| whole periods immediately before z within this run.

For any c\in M, two of c^0,\ldots,c^{|M|} agree. Multiplying onward gives an eventual period at most |M|, starting before |M|, and that period divides N_M. In particular

Consider cuts

They have 0\le k_a-z<R_2, identical 2r_\circ-letter contexts, and a fixed residue modulo n_1. Take the period word in phase at z, with product c=T_{z,z+d}, and put A=T_{s,z-|M|d}. Then

Thus the prefix-product field m is fixed. Although the suffix product can vary with a, it always satisfies mT_{k_a,q+B_{\rm tail}}=T_e; the recovered first-clock total is likewise always q-t. For input x, one correct tag in (5.8), with X=x and Y=x\widehat F_{1,e}, is therefore valid at all these cuts. The prime-factor requirement gives \gcd(dN_Mn_1,n_2)=1. The cuts realize every residue modulo n_2, so one realizes this diagonal tag pair since \ell\notin W_2. Both absence tests lie in the markerless interval from (5.12): their rightmost endpoint is less than z+H+2R_2, and their leftmost positions are covered by the same margin. The stable end guard passes. This gives a split for every input.□

Proof. Suppose A_4 fails. If \mathcal A(t) holds and both A_0,A_1 fail, all conditions of S_1 hold. If \mathcal A(t) fails, choose a missing boundary. Failure of A_2,A_3 gives a good second-clock total and an empty window extended by 2R_2 at that boundary, hence S_2 unless the episode was already in S_1. Thus an episode in neither designation has a witness.□

Proof. For i=0, all main boundaries and trials are after a_0. Their marker decisions and actual interval products are suffix data, and both clock graphs depend on fixed q-t. Replace each required T_{s,z} by mT_{a_0,z}. The explicit rules of Section 5 then compute F_1, its homogeneous lift, and F_2 for every m, agreeing with F_2 at the actual prefix product. This gives \Phi_0.

For i<4, put a=a_{i+1} and b=a_i. Every stage-i measurement and trial lies after a. A hypothetical product m assigns mT_{a,u} to the measurement at u, selecting a leaf h(m) in the full tree. Let C_\nu be the stage-i trial ends, and compute their ideal shifts \beta_\nu(h(m)) from that leaf’s predictions and the actual interval products. For every x\in U_{i+1}, set

The first term transports the input to b; each summand transports one trial shift from its insertion point to b. Each shift is added once to the whole vector, and the terminal map is then applied linearly. The result is affine in x.

Every basis value encountered by H_i has a defined image because \Phi_i is total on M. Hence this formula is defined even for an infeasible hypothetical m or an arbitrary sum of basis vectors. At m=T_{s,a}, it is exactly g_{i+1,e}. A hypothetical m changes the work evolution and selected history; it changes neither the actual suffix interval products nor t,q. This proves the next table property.

For fixed word data, the letter actions and terminal map are linear and all inserted shifts are independent of the input. Removing the shifts therefore gives the linear part \rho(T_{s,a_i})H_i, proving (6.6). All schedules and basis sets are finite functions of the already specified state sizes and M; formula complexity changes none of them.□

Proof. For an actual cut p, the candidate p'=p is the true t; the others are t+p-p'.

For i<4, the explicit equality/end guard and h_i<w_E give the true q, independently of any decoded metadata. The true complete episode contains every bounded control, and the proposed suffix must contain those same controls. Thus even a prematurely or excessively long proposed suffix sees the same control values. The later guard eliminates every later witness at the true origin. Since \Gamma_i\subseteq\Gamma_i+\Delta_i, this holds for either guard. The entry promise forces the true current witness to pass. Uniqueness therefore selects precisely the actual p, and the shared anchor already gives exact consumption.

For i=4, the entry promise itself makes the true candidate pass the q-free test. Internal visibility of all controls prevents any choice of proposed length or two-sided extension from hiding it. Uniqueness first recovers the true time; applying its end rule then forces exact consumption. This argument uses no anchor to prove the uniqueness assertion.

For availability of the primary guard, a candidate differs from t by an element of \Delta_i, and (6.8) excludes every corresponding later \Gamma_i-translate. For the secondary guard, (6.9) excludes the further \Delta_i-expanded tests at every candidate. When i<4, both full conditions include absence of A_4(t), since all expansion sets contain zero. This is stability for every shift of magnitude at most w_E, so the equality/end guard is available.

The true candidate now passes at each stencil cut. If actual offset p is ambiguous, some p'\ne p satisfies the condition counted in (6.3). Choosing one such p' for each ambiguous p injects ambiguous offsets into the counted pairs. At most C_i offsets are lost in the whole stencil, so more than C_i copies of each kind leave a decodable copy of that kind.□

Proof. Let \mathcal B be the set of all leaf histories whose prediction differs from the actual tuple on every trial. If R distinct leaves belonged to \mathcal B, their allocated common trial would assign all R possible tuples across those leaves. One assignment equals that trial’s actual tuple, a contradiction. Thus |\mathcal B|<R.

At a true-path node with measurement u, a wrong proposed value d chooses a different branch. Continue at any later measurement u' using dT_{u,u'}. This selects a well-defined leaf in the off-path subtree, whether or not the whole history is feasible. Departures at two different nodes of the true path lie in disjoint subtrees, so their leaves differ. Selecting one wrong surviving value at each ambiguous node injects those nodes into \mathcal B, proving the bound.□

Proof. The secondary split first gives graph tests for g_{i+1} on (D_i')^*. The primary split uses these as skips and gives its graph tests on D_i^*. Both splits act on U_{i+1} with the same deterministic affine update g_{i+1}. By Lemma 2.3 these determine the product of its episode linear parts. Equation (6.6) shows that starting from [v,1_M], this product ends at [g_{i,w}(v),1_M]. Thus finite basis-state queries recover the required graph tests for g_i.

The domain promise and empty terminal domain follow from the definitions of the full sets, and the next total table follows from Lemma 6.1. Starting with identity graph tests on the empty D_5 domain, the five stages consequently produce graph tests for g_0=F_2 on D_0^*.□

Proof. Write \kappa_i for the number of cut kinds at stage i, and use \mu_i copies of each kind, so that N_i=\kappa_i\mu_i. We will choose the finite objects in the following order and verify each estimate as its inputs become fixed.

1. 1.

   Fix the spaces U_i, full trees, aligned trial identities, and prediction assignments. These determine the numbers \kappa_i before any clock or position is chosen.

2. 2.

   Choose the stage-0 copy count \mu_0 and its abstract roster. This fixes the main-trial identities and predictions, the first tag count m_1, and \mathcal Z. Choose the first clock and R_1, retaining its prescribed roster residues but leaving the integer stage-0 positions open.

3. 3.

   Choose the stage-1 count and numerical stencil. Then choose the inner marker separation d_\circ, block length K_\circ, and inspection radius r_\circ.

4. 4.

   Fix the second tag alphabet, choose the stage-2 count, and construct the second clock and numerical stencil. Then fix the periodic-window width R_2.

5. 5.

   Choose the stage-3 count and numerical stencil. Then choose the inner search halfwidth H and a common main-trial template large enough for all the prescribed inspections.

6. 6.

   Place the stage-0 stencil with its reserved residues and with differences separated by more than this template length. Place the main trials; this determines the outer cut sets.

7. 7.

   Choose the end-stability radius w_E, then the stage-4 count and numerical stencil, and finally the end marker parameters d_\bullet,K_\bullet,r_\bullet.

8. 8.

   Translate the aligned arrangements into reverse stage order. Choose L_0, then o_\bullet, then B_{\rm tail} to put every bounded inspection inside the true episode.

At steps 3–5 the stage-0 positions, and hence the numerical sets \Gamma_1,\Gamma_2,\Gamma_3, are not yet fixed. Their cardinalities are already bounded in terms of the chosen roster sizes. The clock and marker estimates are uniform in the translated origin and in the nominal search centers, so these cardinality bounds suffice until the actual positions are selected. The only copy count that enters its own obstruction bound is \mu_0; its logarithmic dependence will be resolved explicitly below.

Finite kinds before numerical parameters

Put m=|M|. The sets

are fixed now; in particular |U_{i+1}|=2^{m|U_i|}. At stage i, set

Use the full rooted m-ary tree with b_i measurements along each root-to-leaf path. It has

These formulas also apply when m=1. For integers a,r\ge0, write (a)_r=a(a-1)\cdots(a-r+1) when r\le a, and (a)_r=0 when r>a. Allocate one aligned trial for each ordered list of K_i^{\rm al} distinct leaves, and one spare trial. There are \tau_i=1+(\ell_i)_{K_i^{\rm al}} trials. On a listed trial, assign the K_i^{\rm al} possible product tuples bijectively to its listed leaves; assign arbitrary tuples to all other leaves. The spare trial has arbitrary predictions. Thus every history, including every infeasible history, has a prediction on every trial, as required in Lemmas 6.1 and 6.3.

There is one measurement kind for each node and payload in U_{i+1}, and one trial kind for each trial, block, and leaf. Hence the number of kinds introduced above is

None of these sets or counts involves a clock, a marker radius, a main-trial identity, or a numerical position. In the terminal map [v,a]\mapsto[\Phi_i(a)(v),1_M], the argument set U_i\times M and the output basis set are already fixed. A later, more complicated formula for the total table \Phi_i therefore does not introduce new kinds or enlarge the spaces. The formulas in Lemma 6.1 evaluate every hypothetical product; they do not add a prefix-feasibility field to a kind.

We fix an ordering of these kinds and their eventual copies compatible with the following finite event order. First order the tree nodes topologically, so that each ancestor precedes its descendants. Place all copies for a node before that node’s measurement, and place that measurement before the copies for every subsequent node. After all measurements, place the aligned trials in order, with their blocks in order and all copies for a block between its neighboring boundaries. Checkpoints and trial starts and ends are interposed in the indicated order. The extra ordering between unrelated nodes is harmless. In particular, every measurement copy sees its ancestor measurements before the cut and its own and descendant measurements after the cut; every aligned trial follows the entire tree.

Separated differences with prescribed residues

We shall repeatedly use the following elementary construction. Given a finite ordered roster, a modulus n\ge1, an assigned residue for every roster slot, and an integer S\ge1, there are increasing integer positions for the slots with those residues such that all nonzero ordered differences are distinct and are separated from each other and from zero by more than S. Any fixed finite number of interposed events can also be accommodated in each prescribed gap.

Here is a direct induction. Suppose the already chosen positions are x_1<\cdots<x_a, with all their positive differences separated by more than S, and each positive difference greater than S. Their largest positive difference is D=x_a-x_1, taking D=0 when a=1. Choose x_{a+1} in its prescribed residue class so large that

and also so that the gap has room for every event to be inserted there. The new positive differences all exceed D+S. The difference of two of them is an old point gap, and is greater than S. They are consequently separated from one another and from all old differences. Their negatives have the same property, and the positive and negative differences are separated through zero. The first gap can be chosen greater than S, initiating the induction. Arbitrarily large representatives of every residue class exist, so no residue restricts this choice. Events are then placed at distinct integer positions inside the reserved gaps. Extra room before the first and after the last cut accommodates any exterior trial boundaries.

We shall choose each stencil together with its interposed events in this way. Denote its diameter by h_i. A subsequent translation of the entire stage changes none of its differences or internal chronology. In particular, if before translation its residues are v_p, then afterwards they are v_p+c for one constant c; all differences v_{p'}-v_p used by the clock remain unchanged.

For every such stencil, |\Delta_i|\le N_i^2 and |\Delta_i+\Delta_i|\le N_i^4. The cardinality of a sumset is at most the product of the cardinalities of its summands, whence

All these sets contain zero. The second formula is a bound on the absolute values of their elements, not a bound by the same number on their diameters.

Stage 0: the number of copies and the first clock

Put J=|V|^2 and K=m^{J+1}. Initially regard \mathcal P_0 as an indexed roster, without numerical positions. With N_0=\kappa_0\mu_0, it has Q=N_0(N_0-1) ordered pairs of distinct slots. For every ordered list of K distinct such pairs, allocate a group of K main trials, whose predictions exhaust M^{J+1}. Include one spare main trial. Thus the number of main trials is

The full first tag alphabet consists of trial, block, and two vectors in V. Consequently

No position or clock modulus occurs in this count.

For completeness, the simultaneous requirement \mu_0>K+c_{\rm cl}\log(2m_1) has the following explicit solution. Define constants, independently of \mu_0, by

Choose an integer

For \mu_0\ge1, Equation (7.8) gives

We used \log x\le\sqrt x for x\ge1, which follows, for example, by minimizing \sqrt x-\log x; its minimum is 2-\log4>0. This proves the desired strict inequality without a fixed-point assumption about the clock size.

Fix this roster, tag alphabet, prediction schedule, and \mathcal Z. Apply Lemma 3.1 with this roster and prime threshold 1, obtaining n_1,W_1 and roster residues. Set R_1=n_1. Reserve the prescribed residues for the stage-0 positions. Their actual integer values will be chosen only after the common main-trial template length is known.

Stage 1 and the inner marker system

Choose \mu_1=\lfloor C_1\rfloor+1, with C_1 as in Equation (7.2); all its inputs are now fixed. Construct the stage-1 stencil and event order with separated differences, using modulus 1, and record h_1. Choose integers

and obtain the inner marker rule from Lemma 4.1, with an integer inspection radius r_\circ\ge K_\circ.

To prove the stage-1 count, fix \gamma\in\Gamma_1 and a boundary label \lambda. As the nonzero difference \delta=p-p' varies, the center t+\gamma+o_\lambda+\delta lies in an interval of diameter 2h_1. If the first-marker search changes under some shift of absolute value at most R_1, a marker lies within R_1 of one of the two original search endpoints. For either endpoint, the swept interval has diameter 2h_1+2R_1<d_\circ, so contains at most one marker. Such a marker accounts for at most 2R_1+1 integer values of \delta. This is also the endpoint-crossing estimate of Lemma 4.3; it does not depend on the as yet unchosen halfwidth H. Distinct nonzero differences identify distinct ordered pairs. Summing over the two endpoints, \gamma, and \lambda gives

The choice of nominal boundary positions will not affect this count.

Stage 2 and the second clock

The full second tag alphabet is now fixed. Its fields have sizes |\mathcal Z|, |U_0|, |U_0|, m, n_1, and |\Sigma|^{2r_\circ}, respectively. We take the whole Cartesian product, including tags that no particular word realizes. Therefore

Neither the second modulus nor the cut index in a periodic window is a field. Choose \mu_2=\lfloor C_2\rfloor+1, and apply Lemma 3.1 to the resulting stage-2 roster, with threshold \max\{n_1,N_M,d_\circ\}, where N_M=m!. This gives n_2,W_2 and the stage-2 roster residues. Construct its numerical stencil with these residues and separated differences, and record h_2. Set

For a fixed \gamma\in\Gamma_2, the stage-2 predicate on an ordered pair is exactly

Here q-t-\gamma is fixed while the pair varies. The roster bound therefore gives at most c_{\rm cl}\log(2m_2) pairs for this \gamma. Equation (7.7) proves the bound C_2. The clock estimate is uniform in the translate q-t-\gamma; only |\Gamma_2|, not its eventual numerical values, enters this bound.

Every prime factor of n_2 exceeds n_1,N_M,d_\circ. For each 1\le d<d_\circ, it follows that

Thus the cuts with displacements a dN_Mn_1, 0\le a<n_2, run through every second-clock residue. Each displacement is less than R_2, as required by Lemma 5.2.

Stage 3 and the inner search halfwidth

Choose \mu_3=\lfloor C_3\rfloor+1, construct the stage-3 stencil with separated differences, and record h_3. Choose an integer

Fix \gamma\in\Gamma_3 and \lambda. The relevant centers lie in an interval of diameter 2h_3. Apply Lemma 4.3(ii) with D=2h_3, L=H, and h=2R_2. Equation (7.13) gives D<2L+2. At most 2R_2 centers have the required empty search and right-margin marker. Distinct ordered differences identify distinct ordered pairs, and a union bound gives

This argument is independent of the nominal positions of the boundaries. Equation (7.13) also implies the separate periodic-window requirement

Indeed, subtracting the right side from the left and using Equation (7.13) leaves a positive quantity. Together with K_\circ>3d_\circ^2, this supplies both the overlapping short-period blocks and all the context and stabilized-power margins used in Lemma 5.2.

At this point the first three numerical stencils, both clocks, the inner marker radius, and the periodic-window width have all been fixed. The only postponed early choice is the numerical stage-0 stencil. We can now place it with gaps exceeding the complete main-trial template while preserving the first-clock residues chosen earlier.

The main template and the postponed stage-0 positions

Choose an even integer

The common template is the interval of length T. Boundary i, 0\le i\le J+1, has center (i+1)G relative to its start; block j, 1\le j\le J, begins at jG+G/2 and has the R_1 consecutive cut positions prescribed in Section 5. All boundary inspection windows, and all periodic-window cuts and their inspection neighborhoods, fit strictly inside the template. For a block cut, its preceding boundary’s entire inspection window lies to the left, and the next boundary’s entire inspection window lies to the right. The same holds for the future searches under every origin k-c_{\nu,j}-a, 0\le a<R_1: relative to k the nearest future center is G/2-a, which exceeds H+r_\circ. The nearest preceding center for the actual prefix is -G/2-a, whose whole inspection window precedes the cut. Earlier and later trial windows have still larger separations. The periodic suffix’s absence test uses starts from k-r_\circ onward, so a marker inspection needs no letter earlier than k-2r_\circ. This is exactly the context length included in its tag.

We may now choose the numerical positions of the stage-0 roster, with its previously prescribed first-clock residues. Use the separated-difference induction with spacing S=T, reserving all aligned events in their required order. Record h_0. For each allocated group, let \delta_a=p_a-p'_a, 1\le a\le K, be the differences of its listed pairs. Give its trial a the template start

relative to t, retaining the prediction already assigned to that abstract trial. The differences are distinct and separated by more than T, so the templates within a group are disjoint. Bases for distinct groups can be chosen explicitly. Put the spare trial at offset T, enumerate the groups by g=1,\ldots,(Q)_K, and take

Every group lies between offsets T+g(2h_0+2T) and T+g(2h_0+2T)+2h_0+T. These intervals are positive, mutually separated, and disjoint from the spare template. Sort all trials by physical position for the processing rules. Sorting changes neither their identities nor their assigned predictions. It now determines all o_\lambda,c_{\nu,j},\mathcal H_1,\mathcal H_2.

It remains to justify C_0. Its first-clock part contributes at most c_{\rm cl}\log(2m_1), since

and the first-clock roster differences have been preserved. Suppose that the prediction-failure part held for K distinct ordered pairs. Take their ordered list and its allocated group. At origin t+\delta_a, the indicated trial has physical template start

All these K trials therefore have identical physical boundary search centers. The predicate under consideration includes \mathcal A(t+\delta_a), so all their boundaries exist. Locality and translation equivariance of the marker rule give the same actual boundary positions, hence the same actual tuple of J+1 interval products, for all K trials. Their predictions exhaust all possible tuples; one must be perfect. This contradicts the assumed absence of any perfectly predicted main trial at its origin. There are thus at most K-1 prediction-failure pairs, and the total is strictly less than C_0. If the roster has fewer than K ordered pairs, that last assertion already follows from its size. The internal visibility needed for this argument, including all translated templates, is established below.

Stage 4 and the end marker system

Choose an integer

In particular h_i<w_E for i<4. Choose \mu_4=\lfloor C_4\rfloor+1, construct its stencil with separated differences, and record h_4. Choose integers

and obtain its marker rule and radius r_\bullet\ge K_\bullet. These choices imply

so Lemma 4.6 applies to each required set of unexpanded candidate origins. For fixed \gamma\in\Gamma_4, apply the same endpoint argument as at stage 1, with center range of diameter 2h_4, stability radius w_E, and marker separation d_\bullet. Each endpoint sweep has diameter 2h_4+2w_E<d_\bullet, and the number of bad nonzero differences is at most 2(2w_E+1). Hence

This count is independent of the end search’s eventual lag.

All five ambiguity bounds are now proved, and each stencil has more copies per kind than its bound. It remains to put the finite arrangements inside words. This last step must cover every false-origin inspection, not only the windows used by a correctly chosen split.

Final placement and visibility under every hypothesis

Translate the five complete aligned arrangements, including all interposed events, into disjoint integer intervals strictly after s, in order 4,3,2,1,0. End stage i’s interval at a_i, after all its events and before the next interval begins. Write A_{\rm buf} for a positive upper bound on all their offsets from s. These translations do not change any h_i,N_i, \Delta_i,\Gamma_i, or clock difference. Every stage-i measurement, trial, and endpoint is after a_{i+1}, for i<4. This is the chronological hypothesis for the recursion of the total suffix tables in Lemma 6.1.

We give explicit finite envelopes, so that the remaining choices do not hide a dependence on an episode length. Let

Every origin displacement that must be tested, before the extra stability shifts in A_1 and A_4, has absolute value less than D. To check this assertion exhaustively, an outer end guard uses differences in \mathcal H_j-\mathcal H_j. At an actual main cut, even a suffix with an unrelated trial/block role uses a candidate k-c_{\nu,j}-a whose displacement from t is in \mathcal H_1-\mathcal H_1. Aligned candidates have displacements in \Delta_i. Current-witness and primary later-witness tests use \Delta_i+\Gamma_i; the secondary later-witness tests use \Delta_i+\Gamma_i+\Delta_i. Designations and the next-domain promises use subsets of these same expansions, or \Gamma_{i+1}=\Gamma_i+\Delta_i+\Delta_i. Equation (7.7) bounds all their absolute values by 2\sum_{j\le i}h_j. The swept intervals used in the count proofs satisfy the same bounds even when the displacement ranges over every integer in [-h_i,h_i]. The additional shifts of A_1 have magnitude at most R_1, and those of A_4 at most w_E; we include them in the respective inspection envelopes below.

Let A_{\rm main}\ge1 be an integer exceeding the absolute values of all main-template endpoints, all o_\lambda, and all elements of \mathcal H_1\cup\mathcal H_2. Set

All bounded inner-marker, boundary, main-trial, and periodic-window data at every origin just listed lie strictly between t-B_\circ and t+B_\circ. This includes inspection neighborhoods of radius r_\circ, the right-margin overhang 2R_2, the preceding periodic contexts, the short-period blocks, and the whole swept ranges used in the estimates. Equation (7.13) gives H>r_\circ, so the term H+r_\circ also covers the 2r_\circ-letter context. Actual marker-selected interval endpoints differ from their centers by at most H, so products within these bounded trials have endpoints in the same envelope. Choose

Consequently this entire envelope follows every aligned buffer. It is available in every aligned suffix as far as its left endpoint is concerned, including before time has been decoded. Its right endpoint will be put before every possible true anchor next.

For the end controls put

Every bounded end-marker inspection and seed block required under any candidate origin or witness translate lies strictly between z_\bullet(t)-B_\bullet and z_\bullet(t)+B_\bullet. Indeed the origin contributes at most D, a stability test at most w_E, a searched marker start at most d_\bullet, and its inspection at most r_\bullet; a seed extends by at most K_\bullet. We have used a sum of these bounds to cover all cases at once. Choose

The entire bounded end envelope now follows the inner envelope and all actual cuts. Even an end-rule origin among the stated hypotheses has its marker anchor, or the beginning of its possible first-break scan, after the earlier activities, since B_\bullet>D+d_\bullet. For the true episode, its anchor always satisfies q\ge z_\bullet(t)-d_\bullet. Therefore

Every bounded control is thus strictly internal to the true episode, even when its anchor is the earliest possible marker. In the markerless case the actual first break may occur arbitrarily later; this only increases the available length. Its mismatching letter is visible because B_{\rm tail}>1. In the notation of Equation (4.2), take I_-=-B_\circ,I_+=B_\circ,E_-=-B_\bullet,E_+=B_\bullet and use A_{\rm buf} for its last buffer endpoint. Equations 7.20 and 7.22 then imply each of those margin inequalities directly.

In particular, the stage-4 controls do not presuppose knowing the end. At k=s+p, all their inspected letters have displacement from z_\bullet(t) at most

A sufficient padding inequality just for these controls is

which follows from Equations 7.18, 7.21, and 7.22. It contains no occurrence of the unbounded break position q.

We spell out the consequences for arbitrary prefix/suffix pairings. Every proposed suffix must have all of its specified bounded controls on its reading side; an unavailable candidate is a reason to reject the suffix, not a reason to remove that candidate. At a cut of a true complete episode, a shorter proposed suffix either fails this availability test or reads exactly the true letters in all those windows. A longer one reads the same letters there, because all the windows precede the true first episode’s end. Locality of both marker rules therefore fixes the same control values in either case. This applies to every candidate, including the true candidate, independently of the proposed suffix length. For i<4, the candidate-origin diameter is h_i<w_E; for the outer guards it is at most the diameter of the appropriate \mathcal H_j. The equal-search and seed-overlap argument of Lemma 4.6 hence supplies the true anchor before any anchor-dependent witness is used. At stage 4 the witness is q-free: the true candidate cannot disappear from the uniqueness test, because its entire inspected neighborhood is already internal by Equation (7.23). Unique decoding therefore precedes the exact end test at that decoded origin, just as required by Lemma 6.2.

Finally, the side of every noncontrol computation is determined by the event order. Prefixes read earlier measurements, earlier trial boundaries, and the indicated prefix products. Suffixes at aligned trial cuts read the later boundaries, the later trials, and the terminal table at a_i. At a measurement copy they read its measurement and every descendant measurement after the cut, using ancestor values only as verified metadata. The reverse stage order puts every earlier-stage event needed by a terminal table after the current buffer. The main-template inequalities already put all main prefix and suffix boundary searches on their specified sides, including all suffix role hypotheses. The periodic suffix uses only its stated 2r_\circ letters of supplied left context. After correct decoding, all required suffix computations thus have their prescribed access. For an arbitrary standalone suffix with false metadata, a needed unavailable position or ill-ordered interval is rejected; its evaluation never calls for an unspecified prefix factor. Products that extend to the true or proposed end have that end as an endpoint, and the total formulas \Phi_i use the supplied hypothetical product for their omitted prefix.

These observations also give the finite-endpoint property used in Section 8. In any single test, all local inspections and all interval endpoints other than its exact end range over fixed finite sets of offsets from the beginning of that test; bounded offsets from its exact end are allowed as well. There is only the one first-break scan belonging to its selected reference or decoded end-rule origin. Witness translations and hypothetical table evaluations keep that scan’s q fixed and introduce no additional search for a break. This assertion holds for false suffix metadata as well as for successful pairings.

Later translations preserve every earlier count and residue difference. The final three lengths change no schedule diameter, clock, state set, or number of copies. Every marker count now applies to complete words because its full inspection windows are internal, including those at false origins. Thus the ambiguity bounds, chronological requirements, and end margins in the proposition all hold.□

Proof. There are integers N\ge0,d\ge1 such that membership in S above N depends only on the residue modulo d. For each accepted residue choose its least representative r\ge N. Its tail is expressed by ab^r(b^d)^*c; use singleton words for the finitely many accepted exponents below N. A fixed word means its concatenation of letters, and an empty factor means 1. Each expression has height at most one, and finite union preserves this bound.

For the last assertion, enlarge the finite endpoint sets to include every position that any branch might inspect. A fixed start offset eventually lies in a fixed initial segment of the repeated word; a fixed end offset lies in a fixed final segment. Their letters stabilize because the varying middle contains whole copies of the same b. Availability and ordering of any two endpoints also eventually stabilize.

An interval between two start offsets, or between two end offsets, has eventually constant letters. An interval stretching from a start offset to an end offset has, for all sufficiently large j, a product of the form

for fixed A,C\in M and integer j_0. This follows by removing the fixed initial and final partial copies of b. The reverse ordering is eventually invalid and is handled as such. Powers of an element of a finite monoid are ultimately periodic, by repetition of two powers followed by right multiplication. Length residues are periodic.

There are finitely many queried data values. Take a common threshold and a common multiple of all their periods. The entire data array is then periodic, so any fixed finite function of it is periodic. Branching or finite table recursion still computes such a function. This proves the assertion.□

Proof. Every P_x has length in a fixed finite set of cut offsets. Hence it is a finite language, whatever finite test decides its members.

For an exact-end language, take finite cases for the origin at which its end rule is applied. Relative to the argument start, this origin has a fixed offset in each case. If its end marker is present, the anchor lies in a bounded search window and the argument has bounded length. There are only finitely many such words.

In the markerless case, a length-K_\bullet block at a fixed offset determines a short-period repetition. The word agrees with it from the seed end until its first mismatch q, and the argument ends at q+B_{\rm tail}. Take finite cases for the prefix through the seed, the period word in the phase immediately after the seed, the partial period just before q, and the B_{\rm tail}-letter tail beginning with the mismatch. The resulting words have shape ab^jc, with b\ne\epsilon. The finite case specifies continuation, the first mismatch, and the required tail. Additional bounded inspections extending past the seed remain finite tests on the template; the finitely many small exponents cause no difficulty.

For E, the origin is t=s+L_0. For an outer Q, the guard selects one fixed reference from k-\mathcal H_r. At an aligned stage below 4, it selects a reference among (6.10); at stage 4 it first selects the decoded candidate. There are finitely many choices in each case. A standalone Q’s own end condition gives the template, without presuming that its reference is the true origin of any episode. In every such case its indicated q is the argument end minus B_{\rm tail}.

It remains to check that the other conditions fit Lemma 8.1. Their possible endpoints have a finite inventory:

1. (a)

   nominal main boundaries, their fixed search windows and inspection neighborhoods, and actual markers chosen inside those windows;

2. (b)

   fixed tree measurements, aligned checkpoints, trial endpoints and buffer ends;

3. (c)

   all candidate origins, all required \Delta_i,\Gamma_i translates, and all bounded end-marker searches at them;

4. (d)

   the exact argument end, q, and bounded offsets from them.

All start-side positions range over a fixed finite set, even when a branch selects which one is used. Marker-selected positions have finitely many possibilities because their searches are bounded. The only distant anchor is the already selected q. Translated witnesses keep it fixed and do not run new first-break scans.

Prefix products passed as tags or as hypothetical table inputs are finite indices in M. For a suffix’s own candidate copy, a_i has positive offset from its cut because every copy of stage i lies before a_i. All buffer ends and schedules invoked recursively by \Phi_i are later still. Thus table recursion never introduces a missing arbitrary prefix word. It only multiplies the supplied M-value through actual intervals on the reading side. Every schedule has finitely many measurements and trials, irrespective of word length.

The table formulas in Lemma 6.1 use these interval products, finite clock graphs, bounded marker values, and finite vector operations. They run no sequence graph test and do not redefine q. If any position required on the reading side is unavailable or an interval is ill-ordered, the suffix rejects. These availability and order conditions are themselves among the eventually stable data in Lemma 8.1. A false tag or infeasible hypothetical product is consequently included in the same compilation argument.

The full-set conditions add only stability over a fixed finite range, fixed-clock membership, actual-history choices, and equalities of finitely many trial products. The residual domains are finite Boolean combinations of these conditions on E; their definitions use no split-success oracle. On each template every component condition is therefore ultimately periodic. Lemma 8.1 gives height at most one. All metadata choices are finite unions, and every Boolean operation is implemented over the same alphabet by union and complement.□

Proof. By Proposition 8.2, (8.1) has height at most one. Fix a length threshold large enough to contain all bounded end-decision windows and to exceed every marker-present episode length. Words shorter than this threshold form a finite language.

A longer word in F cannot be in the marker-present case, since the corresponding bounded complete episode would be its prefix. Thus its markerless seed fixes a periodic continuation. If the first mismatch is q and at least B_{\rm tail} letters remain beginning there, the prefix ending at q+B_{\rm tail} is an episode, a contradiction. That prefix contains every bounded decision window by the padding conditions, so the argument does not use letters beyond the proposed complete prefix.

Accordingly the word either has no mismatch yet, or has fewer than B_{\rm tail} letters from its first mismatch through its end. Take finite cases for its bounded prefix/seed, period word, partial-period remainder, and bounded final tail. These give finitely many templates ab^jc, covering all sufficiently long F-words. On each template T_f=m is ultimately periodic in j. Intersect the resulting height-one product language with F; this gives the exact required test, including the bounded cases.

Finally, remove a complete episode prefix whenever one exists. Episode lengths are positive, so the process terminates on a finite word. The remainder has no episode prefix and belongs to F. Thus every word factors as an E^*-word followed by an F-word.□

Proof of Theorem 1.1. Fix the DFA transition monoid and choose its faithful representation on basis vectors indexed by M. Proposition 7.1 supplies all finite constructions and their hypotheses.

Start with identity graph tests on the empty residual domain D_5, of height zero. Apply Lemma 6.4 backward for i=4,3,2,1,0. The same-update requirement makes the secondary tests valid skips for the primary tests, and Boolean recovery gives the preceding computation on each domain. We obtain graph tests for F_2 on D_0^*.

Lemma 5.2 now gives graph tests for F_2 on (E\setminus S_1)^*. By Lemma 2.3, their linear parts give the products of the homogeneous lifts of F_1. Querying homogeneous inputs (v,1) gives F_1 on these skipped sequences. Lemma 5.1 then gives F_1 on E^*. One further Boolean linear-part recovery gives the original monoid action on E^*.

By Proposition 8.2 and Lemma 2.2, each split changes a skip bound H to at most \max\{2,H+1\}. There are exactly twelve split applications along the recursion:

The stars within the component languages are included in this recurrence. All recoveries and restrictions to particular finite states are Boolean operations and add no nesting.

Let L_m be the height-at-most-thirteen test that an E^*-word has product m, obtained by querying the identity basis vector. Let F_n be the height-at-most-one product test from Lemma 8.3. If A\subseteq M is the set of transformations taking the DFA’s initial state to an accepting state, the DFA language is

Every input has the required E^*F factorization, and every accepted factorization has actual total product mn. Concatenation and finite union preserve the bound thirteen. Every expression is over \Sigma, and no bound depends on the size of \Sigma, M, or the DFA. This proves the theorem.□