Proof. Spoiler always selects zero valuations in the homogeneous graph. They are legal in every block. Whenever two pebbled distinct blocks share readouts, their selected zero valuations are adjacent, so their answers must agree on every shared readout.

We may regard a finite query as ending immediately after discards, by the removal closure of winning positions from Section 2.

Fix a type \(t\) and an allowed full address. Its site ring consists of the \(r\) site blocks using the address labels at consecutive boundaries, as illustrated in Figure 1(b). The sum of their answered horizontal readouts is a value \(h_t\in\mathbb{F}_2^{d_t}\). To cross a link at a matched address, replace these site blocks by their corresponding square blocks, one row at a time: place the square while retaining its old site, and then discard the site. This uses at most \(r+1\) pairs and preserves each old horizontal readout on the \(t\) side. When all \(r\) squares are pebbled, their vertical readouts agree at adjacent boundaries. Summing (4) in the affine graph gives (3) for the sums on the two sides. Now replace the squares, in the same manner, by the site ring at \(u\). Its sum is preserved from the \(u\) side of the squares. Repeating along the subdivided path transmits the original affine comparison. The same procedure works in reverse.

Fix a winning strategy. Let \(Q_{P,\mathbf a}\) consist of all sums attainable on the real site ring \((P,\mathbf a)\) in plays consistent with that strategy, with zeros selected on the homogeneous side and all other pairs discarded. These sets are nonempty: Spoiler can always query any such ring from the empty position. Starting with any attainable endpoint sum and transmitting across an individual edge produces an attainable sum at its other endpoint with the same affine image. Transmitting in both directions proves both inclusions in (2). ◻

Proof. The support is connected and uses at most \(r+1\) distinct links, since each square contributes one link. Every subdivided wire has \(4(r+1)+1\) links. Reaching two real types, or closing a cycle in the support, would require traversing an entire wire. This also applies to a subdivided original loop or to a cycle arising from parallel schemas. Internal types are private to their wires, giving the remaining claims. ◻

Proof. For any closed walk, the parity of its horizontal traversals is the same in each row. Indeed, at each boundary the total incidence parity is zero, while vertical traversals contribute twice at that boundary. Odd seam parity therefore requires an odd number of traversals in every row and hence at least one block in every row.

With exactly \(r\) blocks, there is one per row, and the witnessing walk meets them all. All horizontal edges of the block in a given row have the same pair of aligned labels. At boundary \(i\), apply parity conservation separately at each aligned label, combining all types. Vertical edges preserve that label. Since both incident rows have odd traversal parity, their specified labels at boundary \(i\) must agree. These labels give the full address.

Two size-\(r\) subcollections of \(U\) share at least \(r-1\) blocks in distinct rows. They therefore overlap, and lie in one component. They can differ only in the remaining row. Every boundary has an incident common row when \(r\geq3\), so the recovered addresses agree in every coordinate. ◻

Proof. If \(V=U\) there is nothing to prove. Assume \(V\subsetneq U\), so \(|V|\leq r\). If a component of \(\Gamma_V\) wraps, Lemma 11 requires at least \(r\) blocks. It therefore uses all \(r\) blocks of \(V\), and there is at most one such component.

Admissible shifts on a retained wrapping component. Let \(D\) be a wrapping component of \(\Gamma_V\), contained in a component \(C\) of \(\Gamma_U\). Compare all recovered addresses in the alignment of \(C\)’s support. The size-\(r\) witness in \(D\) is also in \(C\), so Lemma 11 gives the same address for \(D\) and for the \(Q\) condition on \(C\). We claim that restricting admissible shift families from \(C\) to \(D\) gives exactly all admissible shift families on \(D\).

• If both supports contain a real type, it is the same type with the same \(Q\) restriction. Its real vector determines every arm scalar in either support. Every allowed old vector therefore extends by assigning the newly present arm scalars.

• If \(C\) contains no real type, both supports lie in the same wire interior. They are parameterized by the same common scalar with the same \(Q\) restriction, so restriction is exact.

• If only \(C\) contains a real type, \(D\) lies inside one arm of a wire \(e\) with ordered real endpoints \(P,R\). Write its internal address as \(\mathbf a\in A_e\). The internal coordinates use the first endpoint’s system. Since every \(a_i\in A_{e,i}\), the permutation extending \(\sigma_{e,i}\) sends \(a_i\) to the actual matched label \(\sigma_{e,i}(a_i)\), and its inverse returns that label to \(a_i\). All other matches along the wire are identities. Thus the recovered address is \(\mathbf a\) at the first endpoint \(P\) and \(\boldsymbol\sigma_e(\mathbf a)\) at the second endpoint \(R\). Equation (5) gives \[\phi_{e,0}(Q_{P,\mathbf a}) =Q_{t,\mathbf a} =\phi_{e,1}(Q_{R,\boldsymbol\sigma_e(\mathbf a)}).\] Using the equality for the endpoint reached by \(C\), every admissible old scalar has an admissible real preimage, and every admissible real vector restricts to an admissible old scalar. After choosing the real preimage, assign the scalars on the other arms from that vector. These remain separate endpoint statements when \(P=R\).

These cases are exhaustive, since a real type in \(D\) also belongs to \(C\).

Restriction of readouts. Take a member of \(\mathcal H_U\) and one representation by shifts and potentials. Restrict both to each component \(D\) of \(\Gamma_V\). The link equations remain valid. If \(D\) wraps, the shift fact just proved preserves its \(Q\) condition; if \(D\) does not wrap, it has no such condition. Formulas (6) and (7) then give the same readouts on \(V\). Hence \(\mathcal H_U|_V\subseteq\mathcal H_V\).

Extension of retained readouts. Fix \(a_V\in\mathcal H_V\) and choose one representation, writing \(h_t^D\) for its shifts on an old component \(D\) and \(M_v\) for its corner potentials. On each new component \(C\) choose admissible shifts \(\widehat h_t^C\). If \(C\) contains the wrapping old component, choose these shifts to agree with \(h_t^D\) throughout that old support; the shift fact makes this possible. Since a wrapping old component uses all \(r\) blocks of \(V\), no new real shift must lift two independently prescribed old arm scalars.

The new shifts already agree on a wrapping \(D\). On each nonwrapping \(D\) we now adjust the representing potentials so that the new shifts produce the original readouts of \(a_V\). Mark each horizontal edge in row \(i\) with \(\delta_i\) and each vertical edge with zero. Every closed walk in \(D\) has mark sum zero. Summing marks along paths from a root therefore defines bits \(s_v\) such that \(s_v+s_w\) is the mark of every edge \(vw\).

For a type \(t\) of this \(D\subseteq C\), put \(g_t=h_t^D+\widehat h_t^C\), the difference of its old and new shifts over \(\mathbb{F}_2\). Both shift families satisfy the same affine link equations, so \[L_{\ell,t}g_t=L_{\ell,u}g_u\] on every support link. Replace the old corner potentials of type \(t\) by \(M'_v=M_v+s_vg_t\). Including the change of shift, the change in a horizontal readout from (6) is \[(s_v+s_w)g_t+\delta_i g_t=0.\] For a vertical edge, \(s_v=s_w\), so the change in its readout from (7) is \[s_vL_{\ell,t}g_t+s_wL_{\ell,u}g_u=0.\] Thus every old readout is preserved.

Perform this adjustment independently on each nonwrapping component, and keep the old potentials on a wrapping component. Distinct old components have disjoint corner sets, even if their type supports share types or the new blocks merge them. Their potential assignments therefore do not conflict. Assign arbitrary potentials to new corners of \(\Gamma_U\). Together with the chosen admissible shifts, they represent a member of \(\mathcal H_U\) whose readouts on \(V\) are exactly \(a_V\). This proves the reverse inclusion.

This also covers a set \(U\) that first wraps at size \(r+1\). It has no size-\(r\) wrapping subcollection, and all its proper subsets are nonwrapping. Thus no retained shift must stay fixed, and the same potential adjustment preserves every retained readout. ◻

Proof. For the set \(U\) of blocks containing pebbled vertices, maintain offsets \((a_B)_{B\in U}\in\mathcal H_U\). A homogeneous vertex \(z\) in block \(B\) is matched to the affine vertex \(z+a_B\). On discarding pebbles, discard offsets only for blocks no longer occupied; the invariant is retained by Lemma 12.

Before placing a new pair there are at most \(r\) occupied blocks. For each unoccupied block \(B\), independently extend the retained offsets to a member of \(\mathcal H_{U\cup\{B\}}\), and use its offset \(a_B\). For occupied blocks keep the old offsets. On every block, translation by \(a_B\) is a bijection from its full homogeneous solution space onto its full affine solution coset. The union is therefore a bijection of the vertex sets. Only one new block is selected, so its chosen extension preserves the invariant. The family \(\mathcal H_{\{B\}}\) need not contain all affine valuations: any one legal offset already supplies the required block bijection.

Offsets on shared readouts agree. Adding the same offset to the readouts of two pebbled valuations preserves both their agreement and their disagreement, including when several readouts are shared. Thus adjacency and nonadjacency between distinct blocks are preserved. Within one block, injectivity of translation preserves equality and there are no edges. Multiple pebbles in a block cause no difficulty. These bijections therefore maintain a partial isomorphism forever. ◻

Proof. Associate a one-dimensional vector variable to each scalar gate. Its input and output direction are both the identity on \(\mathbb{F}_2\). Associate a vector \((x_1,x_2)\in\mathbb{F}_2^2\) to each AND gate: the input directions are the coordinate projections and the output direction is \(x_1+x_2\). The intended encoding is that truth forces the corresponding output image to be \(\{0\}\).

A seed is constrained by comparing its scalar direction with the constant form zero on a dummy variable. A test is constrained by comparing its scalar direction with the constant form one on a dummy variable. These are permitted affine forms, with zero linear part; the dummy variable itself can have any nonempty set of values.

For each connection \(c\) from a source output \(o_c\) to a destination port \(i_c\), introduce a private buffer variable \((z_c,z'_c)\in\mathbb{F}_2^2\) and three separate comparisons \[ o_c=z_c,\qquad o_c=z'_c,\qquad z_c+z'_c=i_c. \tag{9}\] Each equality means equality of the two scalar images of the corresponding nonempty sets. In particular, the first two comparisons are individual edges; they are not combined into a joint constraint.

Suppose first that an arc-consistency witness exists. If a source output has image \(\{0\}\), the first two comparisons in (9) force both buffer coordinates to have image \(\{0\}\). The nonempty buffer set is therefore \(\{(0,0)\}\), and the third comparison forces the destination port image to be \(\{0\}\). A true scalar gate has image \(\{0\}\) either because it is seeded or because it receives a true signal. A true AND gate has both coordinate images \(\{0\}\), hence also has output image \(\{0\}\). Induction over the circuit proves this assertion for every true gate. A true test would additionally require image \(\{1\}\), which is impossible.

Conversely, assume that every test is false. At an ordinary scalar gate take \(\{0\}\) if it is true and \(\mathbb{F}_2\) if it is false; at a test take \(\{1\}\). These rules are compatible because no test is true. At an AND gate take \[\bigl\{(x_1,x_2)\in\mathbb{F}_2^2: x_j=0\text{ for each true input port }j\bigr\}.\] These sets are nonempty. A true AND has output image \(\{0\}\); a false AND has a free coordinate, whose change toggles the sum, so its output image is \(\mathbb{F}_2\). Thus every false gate that is a source of a connection has full output image. Here terminality of the tests is essential: a false test has image \(\{1\}\), but is never a source.

For a connection with true source, the destination port is true, so take the buffer set \(\{(0,0)\}\). For a connection with false source, let \(D\) be the nonempty image already chosen for its destination port and take \[B_D=\{(z,z')\in\mathbb{F}_2^2:z+z'\in D\}.\] The three possible cases are

They verify all three comparisons. In particular, forcing a destination port to zero does not force a false source to zero: the buffer can use the diagonal set. All dummy comparisons also hold, proving the first assertion.

For the schematic assertion, give each connection schema its own buffer type, in the source address system. Restrict all three new schemas to the connection’s source product domain. The first two use identity address transmission, and the third uses the original componentwise partial bijection. Each allowed buffer address then participates only in the three comparisons for the intended individual connection. Unused buffer addresses are unrestricted. Seed and test comparisons use identity transmission to a dummy type on their stated product domains. Unions of domains are handled by separate schemas; repeated requests for the same constant are harmless. There is one new two-dimensional type and three schemas per connection schema, and only a bounded additional number for the constant comparisons. This proves the claimed preservation of the short description. ◻

Proof. The order bound and padding assertion are those of Theorem 8. Write \(N_0\) for the number of valuation vertices before adding marks, the hub, and padding; that proof gives \(N_0=O(m^2)\).

For the time bound, store each vertex by a descriptor. A valuation descriptor consists of its block identifiers, its at most two coordinate labels, and its bounded list of readout values. A mark descriptor records its owner’s identifier and its local mark number. The remaining vertex kinds are the hub and numbered padding vertices. Every descriptor has \(O(\log(n+1))\) bits, with a constant depending only on the fixed template and \(r\). All names of shared readouts can be included when a block is enumerated.

The coordinate tables can be scanned rather than randomly accessed. Enumerating \(O(m^2)\) blocks, looking up a bounded number of coordinate matches for each, and listing their valuations uses \(O(m^3(\log(m+1))^2)\) time. Count \(N_0\) in a first pass, then enumerate the valuation vertices and their mark lists using binary counters; finally append the padding list. This costs \(O(n(\log(n+1))^2)\) additional time. All arithmetic here concerns a bounded number of integers of \(O(\log(n+1))\) bits and can, for example, use the elementary quadratic digit algorithms. Since \(n\geq m^{20}\), the entire preparation costs \(O(n^2)\).

Now enumerate the ordered pairs of vertex identifiers. Even retrieving their descriptors by fresh scans of the whole list costs only \(O(n(\log(n+1))^2)\) per pair. Adjacency of two valuation vertices is decided by comparing their bounded lists of shared names and values. Adjacency involving marks, hub, or padding follows directly from the vertex kinds and owner identifiers. Writing all \(n^2\) entries therefore takes \[O\bigl(n^3(\log(n+1))^2\bigr)=O(n^4)\] time. The second graph is constructed in the same bound. No step enumerates a full address in \([m]^r\); the dependence on \(r\) occurs only in fixed loop counts and descriptor lengths. The optional \(O(m^3)\) table preprocessing also fits in \(O(n^4)\). ◻

Proof. Let \(\Sigma\) be the fixed alphabet consisting of ordinary tape symbols and tape symbols carrying a head state of \(M\). There is a fixed map \[F:\Sigma^3\longrightarrow\Sigma\] that updates the center cell of a valid machine configuration. Indeed, its next symbol and head information are determined by whether the old head is at the center or one of its immediate neighbors, together with the scanned symbol and state recorded there. A triple containing no head leaves its center symbol unchanged. Assign arbitrary values on triples that never occur in a configuration with one head. This defines \(F\) everywhere while giving the exact update on every valid configuration, including frozen halting configurations.

Use \(d\) base-\(m\) digits for time and \(q=r-d\) base-\(m\) digits for position. Write \[H=m^d,\qquad L=m^q,\] and regard positions modulo \(L\). Time ranges from \(0\) to \(H-1\) and is not cyclic. The total of \(r\) digits is the address of every gate type.

We first verify that this spatial ring gives the intended computation. For a prehalting transition at time \(\tau<T_0(m)\), let \(h\) be the head position. Then \(|h|\leq\tau\leq T_0(m)-1\). Only the centers \(h-1,h,h+1\) can change, and the triples that determine their next letters lie in \[[h-2,h+2]\subseteq[-T_0(m)-1,T_0(m)+1].\] Together with the initial input, these positions lie in the interval \[I=[-T_0(m)-1,m+T_0(m)]\cap\mathbb{Z}.\] It has \(2T_0(m)+m+2\) elements, fewer than \(L\) by (10). Reduction modulo \(L\) is therefore injective on \(I\). At every step before halting, the head reads and writes exactly the corresponding line cell, and the only changes occur at the old and new head locations. Induction on the step proves agreement of the ring computation and line computation through halting. Cells away from the head remain unchanged, so no additional head or change can arise elsewhere on the ring. The frozen state then preserves agreement through time \(H-1\).

For each \(f\in\Sigma\) introduce a scalar gate type \(S_f\). At time zero seed exactly the actual initial letter at each position. For every triple \((a,b,h)\in\Sigma^3\), introduce two AND types \(A_{a,b,h}\) and \(B_{a,b,h}\). At address \((\tau,j)\) the connections are \[\begin{align*} S_a(\tau-1,j-1)&\longrightarrow\text{port 1 of }A_{a,b,h}(\tau,j),\\ S_b(\tau-1,j)&\longrightarrow\text{port 2 of }A_{a,b,h}(\tau,j),\\ A_{a,b,h}(\tau,j)&\longrightarrow\text{port 1 of }B_{a,b,h}(\tau,j),\\ S_h(\tau-1,j+1)&\longrightarrow\text{port 2 of }B_{a,b,h}(\tau,j),\\ B_{a,b,h}(\tau,j)&\longrightarrow S_{F(a,b,h)}(\tau,j). \end{align*}\] Every connection whose source time is \(\tau-1\) is present only for \(\tau\neq0\); the two same-time connections are present at all addresses. All position arithmetic in this display is modulo \(L\).

This circuit is acyclic. Give \(A\) gates at time \(\tau\) rank \(3\tau\), \(B\) gates rank \(3\tau+1\), and scalar gates rank \(3\tau+2\). The same-time connections strictly increase rank, and every temporal connection comes from rank \(3\tau-1\) at time \(\tau-1\) to rank \(3\tau\) or \(3\tau+1\). At time zero all \(A\) gates are false, since neither port has a temporal input. All \(B\) gates are false as well, since their first port is false. Thus only the chosen letter seed is true at each position at time zero.

Suppose inductively that the true scalar gates at time \(\tau-1\) specify exactly one letter at each cell, namely its actual letter. At \((\tau,j)\), the first AND for a triple is true precisely when its first two letters are the actual left and center letters. The second AND is true precisely when the third letter is also the actual right letter. Exactly one triple then has a true \(B\) gate, and its output makes exactly \(S_{F(a,b,h)}(\tau,j)\) true. Induction proves that the scalar gates record the actual ring computation at all times.

Test every scalar instance \(S_f(H-1,j)\) for which \(f\) carries an accepting halted state. These tests are terminal: scalar gates only have connections to the next time, and no time follows \(H-1\). By (10) and the frozen-state convention, some test is true if and only if \(M\) accepts \(w\).

It remains to describe the circuit by a bounded list of product schemas. The same-time connections use the identity. In source coordinates, the three temporal kinds of connection have address maps \[ (t,j)\longmapsto(t+1,j+1),\qquad (t,j)\longmapsto(t+1,j),\qquad (t,j)\longmapsto(t+1,j-1), \tag{11}\] respectively. In all three, \(t=H-1\) is excluded.

Here is an explicit decomposition into product domains. Number the digits in each group from least to most significant. For nonmaximal time, let \(a\in\{1,\ldots,d\}\) be the first digit not equal to \(m-1\). Its case has domain \[\{m-1\}^{a-1}\times\{0,\ldots,m-2\}\times[m]^{d-a}.\] Apply the permutation \(x\mapsto x+1\pmod m\) to the first \(a\) digits and the identity to the others. Lower digits become zero, the \(a\)th digit increases without overflow, and higher digits remain unchanged; hence this is exactly addition of one. The \(d\) cases partition all nonmaximal times. There is no all-maximal time case, so they do not introduce time wraparound.

For cyclic position increment use the analogous \(q\) cases and the additional all-maximal case, on which every digit is incremented modulo \(m\). For cyclic decrement use the first nonzero digit: lower digits are zero, that digit is in \(\{1,\ldots,m-1\}\), and all later digits are arbitrary. Decrement the digits through that first nonzero digit modulo \(m\), leaving higher digits unchanged. Add the all-zero wrap case, on which every position digit is decremented modulo \(m\). These are exactly the usual carry and borrow identities, expressed using products and coordinate permutations. Because the time and position groups are disjoint, combining one time case with one position case still gives a product domain. Thus each shifted map in (11) uses at most \(d(q+1)\) schemas, and the unshifted one uses \(d\) schemas. Every coordinate map is a restriction of a permutation of \([m]\), as required.

The seed domains are equally short. All time digits are zero. Positions \(j<m\) have all but their least significant position digit zero. For each possible initial letter, its occurrences among these positions are a subset of that one remaining digit; the digit zero is assigned the letter carrying the initial head state. These subsets are determined by scanning \(w\). The blank positions \(j\geq m\) are the union of the \(q-1\) products obtained by requiring a specified higher position digit to be nonzero and leaving the other position digits arbitrary. Overlaps merely repeat the same blank seed. Finally, a test domain sets every time digit to \(m-1\) and leaves all position digits unrestricted.

There are \(|\Sigma|\) scalar types and \(2|\Sigma|^3\) AND types. The number of product schemas just described is bounded in terms of \(r\) and \(\Sigma\), independently of \(m\). Proposition 14 therefore produces a short consistency instance with bounded numbers of types and schemas and dimensions at most two. Its one-coordinate tables contain only a bounded number of subsets and permutations of \([m]\), so have \(O_{r,M}(m)\) entries. They can be produced by scanning \(w\), enumerating the labels, and applying the identity or cyclic increment/decrement maps. Even repeated input scans and elementary binary arithmetic give \(O_{r,M}(m^2(\log(m+1))^2)=O_{r,M}(m^3)\) time. This computation does not simulate \(M\) on \(w\).

By Proposition 14, the resulting instance has an arc-consistency witness exactly when no test is true, hence exactly when \(M\) does not accept \(w\). Theorem 8, with \(K=r+1\), turns existence of the sets into equivalence of the two simple uncolored graphs. This gives the asserted acceptance polarity and the stated \(\mathrm{WL}\) interpretation. Lemma 15 gives their common order \(N=O_{r,M}(m^6)\) and the construction time. For all sufficiently large \(m\), \(N\leq m^{20}\), so that lemma applies to every \(n\geq m^{20}\). On the particular interval \(m^{20}\leq n<(m+1)^{20}\), its \(O_{r,M}(n^4)\) bound is \(O_{r,M}(m^{80})\), an absolute-degree polynomial as claimed. ◻

Proof. For \(s\ge1\), Theorem 18 bounds the running time of \(M_s\) on length-\(m\) inputs by \(C'_s m^{20s}\), for a constant \(C'_s\). Put \(d=\lfloor r/3\rfloor\). For sufficiently large \(r\), \[20s\le\frac{r}{50}<d, \qquad 20s<r-d.\] Consequently, for all sufficiently large \(m\), uniformly over words of length \(m\), a running-time bound \(T_0(m)\) for \(M_s\) satisfies \[T_0(m)<m^d-1, \qquad 2T_0(m)+m+2<m^{r-d}.\] The computation construction of Theorem 16, the graph reduction of Theorem 8, and Lemma 4 therefore give graph pairs with the polarity in (15). Their common unpadded order is at most \(C_r m^6\). The constant includes the dependence on the fixed machine \(M_s\).

For all sufficiently large \(m\), this order is at most \(m^{20}\). The padding assertion in Theorem 8 reaches each prescribed order \(n\in I_m\) while preserving equivalence and the diameter bound. Lemma 15 gives the asserted explicit construction time. Choosing \(m_0(r)\) to satisfy these finitely many eventual conditions completes the proof. ◻

Proof. The procedure handles lengths below \(m_0(r)\) directly with \(M_s\). At larger lengths it generates and tests the padded instances one at a time, starting each simulation from the initial configuration of \(A\). Since \(A\) is correct, every completed answer has the polarity specified in (15). If all simulations reach their cutoffs, \(M_s\) supplies the answer. Thus the procedure always decides \(H_s\) correctly. Its finite program may hardwire \(r\), \(p\), and \(m_0(r)\).

We first implement the procedure on a fixed number of tapes. Let \(t=m^p\) be the cutoff for one trial. Constructing the input pair costs \(O_r(n^4)\) time. A multitape candidate can then be simulated directly on work tapes with a cutoff counter. For completeness, the following more generous bound also covers the RAM case: \[ O_{A,r}\bigl((n^3+t+2)^6\bigr) \tag{17}\] multitape steps suffice for one cutoff simulation, including initialization and counter maintenance.

To see this for the RAM, store a list of initialized or subsequently touched memory cells. If \(S\) denotes their maximum number during the trial, then \(S=O_A(n^2+t+1)\), since the input is explicit and each instruction accesses only boundedly many cells. Each address and stored value has \(O_A(\log(n+2))\) bits. An unlisted address represents an untouched cell in its default initial state. Full scans of the list suffice for reads and writes; the whole address space is never allocated. If \(t\) exceeds the number of available addresses, repeated accesses do not enlarge this list; the displayed estimate remains an upper bound.

Every fixed instruction can be evaluated by a fixed bit computation in \((\log(n+2))^{O_A(1)}\) time. Using full scans and even unnecessarily slow copies of the stored list, one simulated step costs at most \[O_A\bigl(S^2(\log(n+2))^{q_A}\bigr)\] for some fixed exponent \(q_A\). For every fixed \(q_A\), \((\log(n+2))^{q_A}\le n\) for all sufficiently large \(n\). The total for \(t\) simulated steps is consequently bounded by \[O_A(tS^2n) \;=\;O_A\bigl(t(n^2+t+1)^2n\bigr) \;=\;O_A\bigl((n^3+t+2)^4\bigr).\] Initializing the explicit input list costs at most \(O_A(n^3)\). The cutoff counter has \(O_p(\log(m+2))=O_p(\log(n+2))\) bits and adds at most \(O_p(t\log(n+2))\) time. These costs all fit in (17). Thus even an arbitrarily large but fixed word-operation exponent affects only the starting size and the multiplicative constant, not the absolute exponent in that bound.

There are \(O(m^{20})\) trials, and every \(n\in I_m\) is \(O(m^{20})\). Thus, for \(p\ge1\), the total multitape cost before fallback is at most \[\begin{align*} O_{A,r}\left( m^{20}\left[m^{80}+(m^{60}+m^p+2)^6\right] \right) &=O_{A,r}\bigl(m^{380+6p}\bigr). \end{align*}\] The counters enumerating the interval and the bookkeeping for trials fit in this bound. Applying the one-tape simulation of Lemma 17 gives \(O_{A,r}(m^{760+12p})\) time for this stage. The simulation is by online marked-track sweeps, so its quadratic bound applies to the prefix before fallback as well as to a complete computation. Increasing a fixed absolute constant \(D\) if necessary gives (16). The constants in the \(O_{A,r}\) notation may depend on \(A\) and \(r\), but \(D\) and the coefficient \(50\) do not. ◻

Proof of Theorem 1. The parameters in (13) satisfy, for all sufficiently large \(k\), \[ D+50p<s, \qquad 20c_0 k<p. \tag{18}\] Indeed \(p\le s/1000\), whereas \(p\ge r/10^6-1.001\), and \(r\) is either \(k\) or \(k-1\). The first inequality follows as \(s\) tends to infinity; the second follows from \(20c_0=2\cdot10^{-8}<10^{-6}\).

Fix such a \(k\). We prove the stronger promised version: assume that \(A\) is required to halt and decide correctly only on pairs of simple connected uncolored graphs of diameter at most two, and let \(T_A(n)\) be its maximum running time over pairs in this class with \(n\) vertices in each graph. Every trial of Lemma 21 belongs to this class by Lemma 20. Its construction and correctness proof therefore still give a fixed one-tape decider \(B\) for \(H_s\), without any assumption on the behavior of \(A\) outside the promised class.

The second strict gap in (18) implies that, for all sufficiently large \(m\) and every \(n\in I_m\), \[ n^{c_0 k} \le (m+1)^{20c_0 k} =m^{20c_0 k}(1+1/m)^{20c_0 k} \le m^p. \tag{19}\] Here \(k\) is fixed, and the positive exponent gap \(p-20c_0k\) absorbs the bounded factor \((1+1/m)^{20c_0k}\). This also accounts for the upper endpoint of \(I_m\).

Suppose some \(n\in I_m\) satisfies \[ T_A(n)<n^{c_0 k}. \tag{20}\] For every word \(w\) of length \(m\), its padded reduction instance at this same \(n\) is an input on which \(A\) completes within the cutoff \(m^p\). Consequently \(B\) returns before fallback on every word of length \(m\), whether it finishes on this trial or on an earlier one. Its worst-case time at that length is therefore \[O_{A,r}\bigl(m^{D+50p}\bigr)<m^s\] for all sufficiently large \(m\), by the first strict gap in (18).

This contradicts Theorem 18 applied to \(B\), which requires worst-case time greater than \(m^s\) at every sufficiently large length. Choose one threshold \(M=M(A,k)\) beyond all starting lengths used above, including the diagonal lower-bound threshold for \(B\) and the length needed to absorb the constant in (16). Then no \(m\ge M\) admits any \(n\in I_m\) satisfying (20).

The intervals \(I_m\) partition all integers at least \(M^{20}\). It follows that \[T_A(n)\ge n^{c_0 k} \qquad\text{for every integer }n\ge M^{20}.\] Taking \(c=c_0\) proves the claimed eventual lower bound. No monotonicity of \(T_A\) is assumed: trying the complete interval is what excludes isolated fast input sizes. The threshold may depend on the fixed algorithm and parameter, while the exponent constant is absolute. The unrestricted worst-case time is at least this restricted maximum, so the same lower bound also holds without a promise on the input graphs. ◻