Unary constraints separate scaffolds from online tapes

4 October 2026. A written theorem and primary-literature comparison.

Unary SAT only asks whether the restrictions on each individual variable are consistent. There are no clauses coupling different variables. Nevertheless, its ordinary binary-name encoding exposes a substantial difference between scaffolding automata and online Turing machines.

For example, record one Boolean value for each of the names 00, 01, 10 and 11. A final T(10); asks whether the previously recorded value for 10 was true. With longer names, the same short query can select any one of a much larger collection of independently stored values. The logical operation is simple; reaching the selected information is the issue.

The exact distinction

Let $D$ be a fixed nonempty finite domain and $\Gamma$ a fixed finite family of unary relations on $D$. Give every relation a single tag in the fixed input alphabet. A formula is a sequence of records R(w);, where $w$ is a nonempty literal binary word. Repetitions and prefix-related names are allowed. Malformed strings reject and the empty conjunction accepts. Let $L_\Gamma$ be its satisfiability language and put

$$\Gamma_+=\{R\in\Gamma:R\ne\varnothing\},\qquad I=\bigcap_{R\in\Gamma_+}R,$$

with the empty-family intersection defined as $D$.

Theorem. Both $L_\Gamma$ and its string reversal have native deterministic scaffold recognizers. Moreover:

• If $I\ne\varnothing$, both languages are regular.
• If $I=\varnothing$, neither language belongs to $\mathrm{Online}(t(N))$ for any $t(N)=o(N/\log^2 N)$.

Here the second resource is the maximum number of ordinary Turing steps allowed per arriving input symbol, including the decision deadline. It is not a total-time lower bound. The machine is deterministic, has a fixed finite number of ordinary tapes and reads its input only forward. Unbounded computation after input ends is excluded. In particular, the second case cannot be recognized by a real-time multitape Turing machine.

For Boolean pins $\Gamma=\{\{0\},\{1\}\}$, the second case applies. Thus unary Boolean SAT is a concrete SAT example of the established separation between native scaffolds and real-time tapes. This does not separate two SAT families inside the scaffold class: all the unary families here belong to that class.

Native recognition in both orientations

The forward recognizer is the FIFO capsule-trie construction. Its dictionary stores each name’s allowed subset of $D$. Each name bit performs bounded local work, and the terminal update intersects that subset with the record’s relation. The explicit-tip invariant permits immediate commitment without reconstructing the ancestor path.

For the reversed language, a record has the form ;)v(R, where $v$ is the reversal of the original name. Start a new dictionary traversal at ;, check ), and process the nonempty bits of $v$ exactly as before. At ( retain the current subtree and path. At the final relation tag, expose the terminal once, intersect its allowed set, and commit the explicit node and capsule. The same transition sets the complete-record acceptance state. The relation is needed only at this last update, so its late arrival causes no extra work.

Reversal bijectively renames variables and reverses the record order. Neither change affects unary satisfiability. The parser and update therefore recognize the exact reversed language, including malformed-input rejection. This is a specific construction, not an assertion that scaffolds are closed under arbitrary reversal.

The original conservative certificate still suffices: one header root, record arity at most6, at most32 fresh source records per symbol and old-access radius16. The reviewed compiler gives fixed native degree at most193, inspection distance at most17 and $N+1$ physical nodes. All source work and allocated history, including discarded versions, are $O(N)$; pointer serialization is $O(N\log(N+2))$ bits. There is no preparation or deferred final work. By the scaffold-to-PEG reversal theorem, both orientations also have PEGs, applying that theorem separately to their two recognizers.

Proof of the tape distinction

If $I$ contains $a$, assigning $a$ to every variable satisfies every nonempty relation. A formula is then satisfiable exactly when it is well formed and contains no empty-relation tag. A finite automaton can check this, in either orientation.

Suppose instead that $I$ is empty. Choose an inclusion-minimal subfamily $R_1,\ldots,R_k$ of nonempty relations with empty intersection. Then $k\ge2$, and the intersection of $R_1,\ldots,R_{k-1}$ is nonempty.

At a name $w$, define two blocks of exactly $k-1$ records:

$$A(w)=R_1(w);\cdots R_{k-1}(w);,\qquad B(w)=R_k(w);\cdots R_k(w);.$$

Both blocks are individually satisfiable. Appending $R_k(w);$ makes $A(w)$ inconsistent and leaves $B(w)$ consistent.

Fix $d\ge1$. Enumerate all $2^d$ names of length $d$ in a fixed order. For every subset $S$ of those names, form a prefix $y_S$ using $B(w)$ when $w\in S$ and $A(w)$ otherwise. Every prefix is consistent, and every prefix has exactly

$$\ell_d=(k-1)(d+4)2^d$$

symbols. The suffix $z_x=R_k(x);$ has $m_d=d+4$ symbols, and

$$y_Sz_x\in L_\Gamma\quad\Longleftrightarrow\quad x\in S.$$

Consequently these prefixes have at least $2^{2^d}$ distinct acceptance behaviours under suffixes of length $m_d$.

The classical suffix-equivalence bound, stated and proved as Theorem25 of Loff, Moreira and Reis, gives at most $2^{C m t(\ell+m)}$ such behaviours for an online machine, with a constant $C$ depending on that machine. Applying it here gives

$$2^d\le C(d+4)t(N_d),\qquad N_d=(d+4)((k-1)2^d+1).$$

Since $\log N_d=\Theta(d)$, this forces $t(N_d)=\Omega(N_d/\log^2N_d)$ along these lengths, and excludes every globally little-oh delay bound in the theorem. The prefixes all have the same length, so knowing the total input length does not distinguish them.

For the reversed language, reverse each record separately in the constructed prefix and suffix. Reversing the resulting whole string changes only the order of these unary constraints. The same consistency test and lengths therefore prove the same lower bound.

All input size is counted: there are $b=2^d$ variables and $N_d=\Theta(b\log b)$ actual symbols. The number of distinguishable prefixes is $2^b$, rather than an assertion that one input encodes that many bits. The result concerns the late-query access budget; it gives no unrestricted SAT running-time or P-versus-NP conclusion.

What the literature establishes about the contribution

The comparison supports a specific assessment: this is a specialized native realization and a SAT application of established techniques. It supplies a useful explicit language witness and a simpler sufficient container interface, rather than a new general functional-dictionary bound or a new general separation method.

The FIFO-only implementation is a modest proof simplification of the functional path-container approach: it avoids needing the stronger catenable-deque interface for this application. The inspected sources support this attribution and scope. They do not justify presenting the underlying path-context idea or online lower-bound technique as our invention. The written proofs and their machine interfaces were independently audited; no proof-assistant verification is claimed.

The strategic consequence is that low logical complexity does not make serial name access trivial, yet this access problem already has a native solution. Equality SAT adds the distinct obligation of keeping component restrictions current under merges. That remains the next decisive native-recognition test. Further work should use the completed dictionary and this machine comparison as controls, rather than optimize their constants or reprove the classical separation.