Unary SAT has a native scaffold recognizer

4 October 2026. Written construction, independently audited. The prior-work comparison and online-tape separation position this as a specialized native realization of established functional-trie techniques.

The positive SAT result

A scaffolding automaton can recognize consistency of arbitrary records T(w); and F(w);, where each variable name $w$ is a nonempty binary word. Names may repeat, occur in any order, or be prefixes of other names. The recognizer answers at ordinary input end. It needs no supplied variable handles, padding, preprocessing, mutation or final cleanup.

For example, T(0);F(01);T(01); becomes inconsistent only at the final record. The variables 0 and 01 are distinct. The construction must update one name without losing the other, and it must notice the conflict before any further input arrives.

Written recognition theorem. Fix a finite domain $D$ and a finite language $\Gamma$ of unary relations on $D$. Under ordinary records with literal binary-word variable names, $\mathrm{SAT}_{\mathrm{enc}}(\Gamma)$ belongs to native deterministic scaffolding recognition. One fixed automaton, depending on $D$ and $\Gamma$, handles every input length.

The Boolean pin language is the case $D=\{0,1\}$ and $\Gamma=\{\{1\},\{0\}\}$. The theorem supplies the positive side of our pins-versus-equality control. Equality SAT remains unresolved. The construction explains a concrete mechanism: independent restrictions at named variables can be maintained through serial name access without restoring a whole trie path after each update. It does not yet implement relations coupling two variables.

Contract and dependencies

Give each fixed unary relation a fixed tag. A record is R(w);; tags, parentheses and semicolons belong to a finite alphabet, and $w\in\{0,1\}^{+}$. Leading zeros matter. Every actual symbol counts toward encoded length $N$, including repeated name bits. Malformed input is rejected, and the empty conjunction is accepted. If $b$ is the number of distinct variables, $b\le N$.

The target is the native deterministic model: fixed finite control and labels, fixed degree and local inspection distance, fixed initialization at the unlabelled base, and one immutable new scaffold node per input symbol. Transitions inspect bounded labelled unfoldings. They have no physical pointer-equality or numeric-address tests, external oracle, memoization or extra end-of-input transition.

The proof uses the existing written counter-free strict persistent FIFO theorem and the reviewed simultaneous-record compiler. The FIFO construction adapts classical Hood–Melville scheduling. Its corrected resource bounds are arity6, old-access radius6 and at most12 fresh records per queue operation. These are written proof bounds, not conclusions inferred from finite tests. The compiler preserves one source transition per input symbol under its explicit virtual-initialization and observation hypotheses.

The formerly used deque premise is unnecessary for this construction. We need only a fully persistent FIFO with enqueue, legal dequeue, front and empty observations. No concatenation or access to the rear is used.

Opaque frames in the strict queue

The saved FIFO theorem states finite scalar payloads. Here each payload is instead an opaque pointer to a fixed-arity immutable frame. This extension requires justification.

In every FIFO transition, the payload of an exposed list cell is merely copied to another list cell. The scheduler never branches on it, compares it, follows it or changes it. Tokens and balance certificates use list tails, not payload values. Consequently the same induction preserves FIFO order over arbitrary opaque payload references. Replacing a finite scalar by one pointer makes a list cell have two pointer fields, still within the arity6 bound. It adds no record to a list-copy step. Each copied payload target is one field from an already exposed cell; use conservative old-access radius7 for the extension and retain the fresh-record bound12.

Payload frames are allocated and counted by the caller. Their fields target bounded old addresses or declared same-batch slots. They are internal references, not input-supplied ready handles. No test depends on their physical identity.

A trie with unfinished paths

A logical subtree has one of three finite record types:

• Blank, meaning every name below it still allows all of $D$;
• Node(M,left,right), where $M\subseteq D$ is the allowed set at that prefix;
• Capsule(Q,tip), where $Q$ is a nonempty FIFO of frames and tip is an explicit Node.

A frame is Frame(M,a,other), with finite label $M$, bit $a\in\{0,1\}$ and one subtree pointer. It describes a node with allowed set $M$, whose $a$-child continues the path and whose other child is other. Write $C_f(t)$ for this one-node context around a subtree $t$. The meaning of a capsule with queue contents $f_1,\ldots,f_k$ is

$$\llbracket\mathrm{Capsule}(Q,t)\rrbracket =C_{f_1}\bigl(C_{f_2}(\cdots C_{f_k}(t)\cdots)\bigr).$$

This is a semantic definition, not an instruction to traverse or fold the queue. Off-path subtrees may themselves be capsules. Crucially, a capsule’s tip is always explicit, so opening its end never requires recursively opening another capsule.

Exposing one logical node

The routine view returns the allowed set and two children of a logical subtree.

For Blank, it returns $D$ and two Blank children. For an explicit node, it reads the three fields. For a capsule, it reads the front frame and performs one legal FIFO dequeue. Its continuing child is tip if the resulting FIFO is empty, and a new capsule around the remaining FIFO and the same tip otherwise. The other child and allowed set come from the front frame.

This routine exposes exactly one logical node. It never calls view on either child or on the tip. Thus a path represented by many frames, or an off-path child represented by an older capsule, causes no unbounded work in one view.

Processing the input

Keep a committed trie root, a current subtree, and a new path FIFO. A fixed header stores these three references; relation and parser states are finite control.

At the start of a record, set current to the committed root and the path FIFO to empty. For each name bit $a$:

1. Obtain $(M,t_0,t_1)=\mathrm{view}(\mathrm{current})$.
2. Enqueue Frame(M,a,t_(1-a)) into the new path FIFO.
3. Set current to $t_a$.

When ) arrives, expose the current node once. Intersect its allowed set with the relation specified by the record, retain its two children, and allocate an explicit node containing the result. The new committed root is a capsule containing the accumulated path FIFO and that explicit node. There is no restoration walk. An empty intersection latches a contradiction flag.

The parser requires at least one name bit and the final ;. It accepts only at a complete-record boundary with no contradiction or syntax error. Hence a final complete record is already settled when its semicolon arrives; an incomplete record rejects. No extra input symbol is requested.

The invariant that proves correctness

While a name is being read, the path FIFO contains the ancestor frames for exactly its already-read prefix, in root-to-leaf order. Each frame retains the old allowed set and the off-path subtree. The current subtree denotes the remainder at that prefix. Therefore

$$\text{committed trie}=\operatorname{fold}(\text{path FIFO},\mathrm{current}).$$

A name-bit transition exposes one node, records its context, and descends. It preserves this equality by the definition of view. At ), replace only the current node’s allowed set, preserving its children. Folding the same ancestor contexts around the explicit replacement gives precisely the point update at the full name. The capsule stores that result immediately, restoring its explicit-tip invariant.

This induction covers arbitrary record order. If a name ends inside a previously stored path, the replacement retains the unconsumed path as a child, so proper-prefix names are safe. If a name extends an old terminal, its ancestor frame retains that terminal’s restriction. Repeating a name exposes old frames one at a time and intersects the same terminal set. An off-path capsule is entered only during a later name-bit transition; it is not recursively normalized now.

Each variable’s stored allowed set is thus exactly the intersection of all unary constraints seen for it. Unary constraints are satisfiable together precisely when every such intersection is nonempty. Since intersections only shrink, the permanent contradiction flag gives exact satisfiability at every complete-record boundary.

Native compilation and all charged resources

Here is a conservative bounded-record certificate. It is deliberately loose; the constants are not a research objective.

All record types have at most6 pointer fields. Take a single header root, batch limit $A=32$ and old-address radius $r=16$. The queue pointer is at most two fields behind that root. Its extended radius7, frame/off-child fields and bounded empty-result observations fit within this conservative radius. Each view is performed once per transition; there is no repeated nested opening. Every guard inspects finite tags along these bounded paths. Fresh records may reference other declared slots in that same batch.

Blank, the empty FIFO, idle status and header initialization form one fixed finite pointer-closed virtual graph. No part of it depends on the input. The compiler hypotheses therefore hold with

$$s=1,\qquad q=6,\qquad A=32,\qquad r=16.$$

The reviewed compiler yields a native automaton of degree at most193 and distance at most17, with exactly $N+1$ physical nodes including its base. These are existence bounds for one fixed automaton, not claims of optimality. All source auxiliary history is $O(N)$ records and all transition work is $O(N)$, including old queue versions, discarded wrappers and abandoned malformed partial records. A literal binary pointer serialization uses $O(N\log(N+2))$ bits. There is no separate preprocessing or deferred logical update: queue scheduling already guarantees an immediately available front on every valid version.

What this changes in the SAT investigation

This establishes the unary-family positive control by a written native construction. The proof has been independently audited, including payload extension, prefix and repeated names, initialization, local access, allocation and EOF. It has not been formally verified. The queue and compiler dependencies have their own documented verification scopes. The subsequent primary comparison identifies functional path-deque tries as close prior art: the contribution here is the FIFO-only simplification, explicit-tip invariant and native resource proof. The linked follow-up derives a common-value criterion separating regular unary languages from unary languages requiring substantial online Turing-machine delay.

Binary name routing itself can now be handled in the native model for independent terminal restrictions. The unresolved equality problem requires coherently updating restrictions across whole components. A current record found by this trie is not automatically a current component representative, and repeated parent-name searches still face the failed approaches in the equality construction assessment.

There is also a sharper conditional consequence. Boolean pins and pins-plus-equality have the same positive-arity idempotent polymorphisms. Therefore the portfolio’s hypothetical assertion that polymorphism sets determine native recognition would now imply equality-SAT recognition from this proved pin result. A native nonrecognition theorem for equality would refute that invariance assertion. We have neither such outcome nor a separation, and membership for 2SAT, Horn or affine SAT is not inferred.

The next decisive test is to use this completed serial dictionary as the name layer of an equality-specific component representation, and prove that current component pin information is ready by the delimiter. Any such proof must account for merging and history coherence in addition to trie access. The independent-variable case should not be reopened as a deque problem.

A scaffold recognizer for this language also gives a PEG for its reversal by the existing scaffold-to-PEG theorem. No reversal is used in the native recognition construction itself.