Proof. Start with \(\mathbb F_2\). In a finite field \(K\) of characteristic two, the additive map \(x\mapsto x^2+x\) has kernel \(\{0,1\}\), since \(x^2+x=x(x+1)\). Its image therefore contains exactly half of \(K\). Enumerate \(a\in K\), and, for each candidate, enumerate \(x\in K\) to test whether \(a=x^2+x\). An \(a\) outside the image exists. The polynomial \(X^2+X+a\) has no root in \(K\), hence is irreducible, and \[K[X]/(X^2+X+a)\] is a field: the Euclidean algorithm gives an inverse modulo this polynomial for every nonzero residue of degree less than two. Its elements are pairs of elements of \(K\) and its cardinality is \(|K|^2\).

Repeat until the cardinality first exceeds \(\Delta\). The final cardinality is at most \(\max(2,\Delta^2)\), and its binary vector representation has \(m=O(\log T)\) bits. The selected coefficients at all levels together use \(O(m)\) bits, since their representation lengths form a geometric sequence. Arithmetic can be implemented recursively on the pairs, reducing products using the defining quadratics. A direct recursive implementation uses at most a polynomial in \(m\) space; its recursion depth is \(O(\log m)\). Enumeration uses an \(m\)-bit counter. Alternatively, once multiplication is available, inversion can be implemented simply by enumerating all elements until their product with the given nonzero element is \(1\). The searches for the extension coefficients have the same space bound. No time bound is required. ◻

Proof. For \(u\in\{0,1\}^d\) and \(z\in\mathbb F^{d+1}\), set \[ B_u(z)=\prod_{\ell=1}^d \begin{cases} z_\ell,&u_\ell=1,\\ z_*-z_\ell,&u_\ell=0. \end{cases} \tag{1}\] At \(z=\overline v\), this is \(1\) for \(u=v\) and \(0\) otherwise. Thus \[ \widetilde f(z^{(1)},\ldots,z^{(a)}) =\sum_{u^{(1)},\ldots,u^{(a)}\in\{0,1\}^d} f(u^{(1)},\ldots,u^{(a)}) \prod_{j=1}^a B_{u^{(j)}}(z^{(j)}) \tag{2}\] has the stated agreement and homogeneity. The zero polynomial is allowed as a homogeneous polynomial of the indicated degree. For a word output, apply the formula to each of its \(d\) bit coordinates and to its extra coordinate, whose Boolean value is \(1\).

To evaluate one coordinate, enumerate the \(a\) Boolean assignments, compute the corresponding Boolean function value, and compute the basis products and running sum using field scalars. The assignments occupy \(ad=O(d)\) bits; the local Boolean computation occupies \(O(d\operatorname{polylog}T)\) bits. All inputs are the supplied vectors, read without modification, and immutable parameters. This routine makes no calls to evaluate any word. Its entire temporary storage can be discarded when its scalar result has been obtained. ◻

Proof. The polynomials \[\prod_{u\in S_L\setminus\{s\}}\frac{X-u}{s-u}\] interpolate the values at \(S_L\). Subtracting the resulting interpolant from \(p\) gives a polynomial of degree at most \(L\) with \(L+1\) distinct roots, so the difference is zero. Taking the coefficient of \(X^L\) proves (3). For each monomial of total degree \(L\), the coefficient of \(X^L\) after substituting \(a+Xv\) is the same monomial in \(v\). Summing proves (4). Enumeration of the first \(L+1\) field elements and a running product compute each weight using only field scalars and counters. All denominators are nonzero. This proof uses neither factorials nor derivatives, and applies in characteristic two even when \(L\) exceeds the characteristic. ◻

Proof. Use the field from Lemma 2 for the supplied degree bound \(\Delta\). Each register occupies \(O(d\log T)\) bits. We prove the contract by induction in the acyclic dependency graph, simultaneously for all scalars, targets, and initial register assignments. At every recursive call, the scalar request and the word identifier are ordinary saved data; neither is encoded by a register whose contents the call can change.

Proof. If there are no writable tapes, a direct capped simulation stores the finite-control state, elapsed time, terminal flags, and the fixed number of read-only head displacements. Unit movement keeps every query within the cap radius, so the controller and accessor use \(\operatorname{polylog}T\) work bits. Hence assume the writable-tape count \(m\) is positive, and let \(b=\lceil\sqrt T\rceil\). On each writable tape, use the represented blocks of Lemma 6: they contain the real symbols within distance \(T\) of that tape’s origin and a fixed filler outside. All block words below refer to this represented computation. The confinement argument applies to every head of every accepted candidate controller. From elapsed time \(\tau\) and displacement at most \(\tau\), after \(s\le T-\tau\) further unit steps its displacement is at most \(\tau+s\le T\). Thus a joint visit never reads or writes an exterior writable cell, and all read-only queries satisfy the access condition. Invalid or terminal controllers make no underlying tape query. The represented and real capped controller trajectories therefore agree.

Apply a common trial offset to all tapes. The sum of crossing counts, averaged over offsets, is at most \(mT/b\). End a joint visit when any writable head crosses, or on halt/timeout. Some offset therefore needs at most \(R=\lceil1+mT/b\rceil\) visits. A joint visit reads and updates only its \(m\) selected blocks and is computable in \(O((mb+1)\operatorname{polylog}T)\) space on those explicit blocks, including public-symbol access.

For each offset, enumerate a complete list of \(R+1\) raw fixed-width controller strings, including the prescribed initial one. Hold this list in one global \(O(R\log(T+2))\)-bit buffer. For a candidate list \(z_0,\ldots,z_R\), let \(Q_{t,h}\) denote the block word produced after visit \(t\) for the block on tape \(h\) selected by the incoming controller \(z_{t-1}\). Its incoming block is the output \(Q_{s,h}\) from the last earlier visit \(s<t\) selecting that same tape/block, or the initial block if none exists. Each \(Q_{t,h}\), and each gate computing or checking the outgoing controller, depends on at most \(m\) incoming block words and the prescribed controller \(z_{t-1}\). The last-update index is found by scanning the retained list. All dependencies decrease visit number, so their depth is \(O(R)\), even for malformed lists.

Use the same total parsing convention as in Lemma 6, with a designated valid block on each tape for an invalid controller. Each transition check compares its deterministic raw outgoing controller bit for bit with the proposed string \(z_t\). Apply the ordinary-rule evaluator with word width \(O(b)\), fixed fan-in and path weight \(O(R)\). Evaluate the transition checks one at a time. Induction from the initial controller proves that a passing list is exactly the actual capped computation: the last-update rule supplies each true incoming block, and the next check forces the true outgoing controller. Require a terminal last controller; disregard insufficient offsets. A completed actual list exists for a good offset, with stationary padding after termination.

The controller list is stored once, not copied into recursive frames. Evaluator storage and that buffer together occupy \(\widetilde O(b+R)=\widetilde O(\sqrt T)\). Only the maximum storage over offset/list trials is needed. ◻

Proof. Set \(a=5/2-\epsilon\) and \[\beta=\frac25\max\{1,a\} =\max\left\{\frac25,1-\frac{2\epsilon}{5}\right\}<1.\] On an input of length \(n\), compute \(n\) with a logarithmic-space counter and try doubling caps starting at \(T_0=\max\{2,n\}\), reusing space after each timeout and returning only on a halt. At every trial cap \(T\ge n\), rescanning supplies every symbol within the cap radius in \(O(\log(n+2)+\log(T+2))=O(\log(T+2))\) work bits. Thus the access condition holds for each capped call, even when \(a<1\). For a run of length \(t\), the final cap is at most \(2\max\{2,n,t\}\). Theorem 1 therefore gives, for any fixed machine with \(t(n)=O(s(n)^a)\), a uniform deterministic simulation whose work-space usage in bits satisfies \[\begin{align*} \text{space} &=O\!\left((n+t(n)+2)^{2/5}\log^C(n+t(n)+2)\right)\\ &=O\!\left(s(n)^\beta\log^{C'}(s(n)+2)\right). \end{align*}\] This includes the length counter. No value of \(s(n)\) or running-time bound is needed by the simulator.

Choose one \(q\) with \(\beta<q<1\). Every fixed logarithmic exponent and constant in this bound is absorbed by \(s(n)^q\), so \(\mathrm{TIME}_{1w,\mathrm{ro}}(s^a)\) is contained in \(\mathrm{DSPACE}(\lceil s^q\rceil)\). The deterministic space hierarchy, in its standard constant-factor form, separates \(\mathrm{DSPACE}(s)\) from \(\mathrm{DSPACE}(r)\) whenever the larger bound \(s\ge n\) is space-constructible and \(r=o(s)\); constructibility of \(r\) is not required (Ladner and Lynch 1976, Theorem 3.1). For this application, the passage from the cited exact-cell theorem to bit-space bounds can be seen directly. Choose \(q'\) with \(q<q'<1\). After a fixed normalization of the machine and constructor models, an exactly constructible cell bound \(S=\Theta(s)\) is available, and each fixed \(O(s^q)\)-bit decider uses \(O(s^q+\log(n+2))=o(S^{q'})\) cells. For each such decider, the bound \(\lceil S^{q'}\rceil\) therefore holds at all sufficiently large lengths; the finitely many exceptional inputs can be handled in finite control. Apply the exact-cell theorem with the smaller bound \(\lceil S^{q'}\rceil=o(S)\), which need not be constructible. Its separating machine uses \(O(S)=O(s)\) bits. This proves the required separation from \(\mathrm{DSPACE}(\lceil s^q\rceil)\). ◻

Proof. For membership in linear space, first reject any malformed tuple or transition table, and reject if \(|M|>k\). A universal simulation then stores the bounded work interval, head positions and state in \(O(k+|M|+\log(N+2))=O(N)\) bits, looking up transitions by rescanning the code. For fixed encoding constants \(K_0,K_1\), the number of bounded configurations is at most \[K_0(N+2)2^{|M|}(k+1)^3 3^k \le 2^{K_1(k+|M|+\log(N+2)+1)}.\] The factors account for the bounded input head, state code, work-interval and head markers, and the fixed three-symbol work alphabet. A conservative counter for this bound uses \(O(N)\) bits. Reject an attempted visit to a \((k+1)\)-st work cell, accept a halt within the bound, and otherwise reject when the clock is exhausted. In the last case a deterministic bounded configuration has repeated.

Fix \(A\in\mathrm{DSPACE}(n)\). Constant-factor space normalization gives a fixed decider \(M_A\) in the chosen format using at most \(cn+d\) work cells. Replace rejection by a stationary loop, leaving acceptance as a halt, to obtain \(M_A^+\). Choose \(k=c'n+d'\) large enough to bound this computation and satisfy \(k\ge |M_A^+|\), including small inputs. Put \(y(x)=\langle M_A^+,x,1^k\rangle\). Then \(x\in A\) if and only if \(y(x)\in H\), and \(|y(x)|=O(n+1)\). This is a logarithmic-space reduction of linear output length. More specifically, given a coordinate \(j\), counters compute the field boundaries and return a fixed-code, header or unary symbol, or rescan \(x\) for its indexed bit; outside the encoding they return the prescribed blank or endmarker. This uses \(O(\log(n+2)+\log(|j|+2))\) work bits and also computes \(|y(x)|\). The encoded string \(y(x)\) is independent of the simulation cap.

Suppose a fixed target-model machine decided \(H\) in \(O(N^a)\) time, where \(a=5/2-\epsilon\). Simulate it on the virtual input \(y(x)\) by Theorem 1, supplying the symbols of its prescribed initial writable and read-only tapes from \(y(x)\), or the fixed blank symbol, by the preceding procedure. Start doubling caps at \(\max\{2,|y(x)|\}\). Since \(|y(x)|\ge n\), symbol access uses \(O(\log(T+2))\) bits at every coordinate within distance \(T\) of the fixed head origins, for each trial cap \(T\). Thus every capped call satisfies the access condition. The last cap is \(O(n+1+(n+1)^a)\), giving \[O\!\left((n+1)^\beta\log^C(n+2)\right)=o(n), \qquad \beta=\frac25\max\{1,a\}<1.\] Choosing one \(q\in(\beta,1)\) as above would put every \(A\in\mathrm{DSPACE}(n)\) in \(\mathrm{DSPACE}(\lceil n^q\rceil)\), contrary to the space hierarchy. This uses the public-symbol interface of Theorem 1, not closure of one-tape time under logarithmic-space reductions. ◻