Small components with comparable name lengths admit native recognition

5 October 2026. Written construction with an independent proof audit; an extension of persistent-trie and real-time scheduling methods.

Consider equality pairs followed by late pins:

E(00,11);E(01,10);T(00);F(11);

The final pin contradicts the first pair. A recognizer must know that by the final semicolon. For unbounded names, discovering the partner only after lookup and then replaying its spelling cannot in general fit the remaining fixed punctuation. But completing every physical update before the next record is stronger than recognition requires.

The construction below retains the latest changes in a small explicit list. While the next name arrives, it both installs those changes and compares the arriving name against the list. The answer is current even if the underlying dictionary was temporarily behind.

This yields a positive theorem for arbitrarily many small constraint components. The essential additional hypothesis is explicit: all variable names in a word have lengths within a fixed ratio. Equal-width binary identifiers are the simplest case. The recognizer checks both restrictions itself. No encoding translation from unrestricted names is asserted.

Exact statement

Fix a nonempty finite domain $D$, a finite language $\Gamma$ of unary and binary relations on $D$, and integers $k,C\ge1$. Let $L_{D,\Gamma,k,C}$ consist of ordinary record strings satisfying all three conditions:

1. The constraints are jointly satisfiable.
2. Every connected component of the loopless primal graph has at most $k$ variables.
3. Among all occurring nonempty binary-word names, the maximum length is at most $C$ times the minimum length.

Written theorem. Both $L_{D,\Gamma,k,C}$ and its string reversal have deterministic native scaffolding-automaton recognizers and PEGs.

A unary record is U(w);; a binary record is B(u,v);. Each relation has a fixed alphabet tag. Leading zeros matter, repeated and prefix-related names are allowed, and every literal symbol counts toward input length $N$. Each distinct-name binary record contributes an undirected primal edge even if its relation is full. Repeated edges are allowed; a same-name record applies its diagonal unary restriction. Malformed words reject. The empty conjunction is accepted, with the length condition vacuous.

The automaton is fixed for $D,\Gamma,k,C$, independently of $N$ and the number $b$ of variables. Components, their membership lists and identifiers are not supplied. Constraints and pins may arrive in arbitrary order, including pins before the first edge. Initialization is fixed; all storage is immutable, all observations have fixed radius, and all allocation per symbol is bounded. Acceptance is ready at the final input symbol, without an end-of-input transition.

There can be arbitrarily many components. In particular, the theorem includes unboundedly many equality pairs with late pins. Such graphs have unbounded total vertex-cover number, so this case is not covered by the earlier bounded-cover construction. Conversely, that construction permits large stars and unrestricted name lengths. Neither statement subsumes the other.

The bounded list of pending changes

Use the existing persistent FIFO and capsule-trie construction. A dictionary write to a known spelling of length $h$ takes at most $a(h+1)$ bounded local operations for one fixed constant $a$: traverse the spelling from a persistent FIFO, retain the path frames, and commit the replacement through a capsule. Each operation has bounded old access and allocation. The terminal replacement does not walk back up the path.

The dictionary may store a fixed amount of finite data together with a fixed number of opaque pointers. For this extension, each node and path frame copies those pointer fields just as it copies the off-path subtree pointer. view still opens exactly one logical node; no payload is recursively normalized and no pointer identity is tested. A fixed-size component header can therefore contain at most $k$ immutable spelling-FIFO references. All such headers and queue operations are charged.

At a complete-record boundary retain:

• a dictionary root $T$ that is correct before the latest record’s changes;
• a list $P$ of at most $k$ distinct spelling/replacement pairs that makes $T$ logically current;
• the already computed consistency bit.

No dictionary reads occur between records. During the first name of the next record, run three processes in parallel:

1. Look up the arriving name in the unchanged snapshot $T$.
2. Compare that name, bit by bit, with every spelling in $P$.
3. Starting from $T$, perform the writes in $P$ sequentially in a separate worker, producing $T'$.

At the name delimiter, a matching entry of $P$ overrides the snapshot payload. Otherwise the snapshot payload is current. The comparisons include exact termination, so a proper prefix never matches. The worker’s partially updated roots are never queried.

Let the arriving name have length $\ell$. If the checked length condition still holds, every pending target has length at most $C\ell$. The entire worker needs at most

$$ak(C\ell+1)\le ak(C+1)\ell$$

local operations, after increasing $a$ to cover bounded setup and switching costs. Running this fixed number of worker operations per input bit completes $T'$ by the delimiter. The simultaneous snapshot lookup and at most $k$ equality comparisons also cost only a fixed amount per bit.

After that delimiter, use $T'$ for any second name in the record. Do not begin writing the current record’s changes yet. Once that record has been analyzed, its at most $k$ replacements become the next list $P$. This avoids merging a new write with a traversal made against an older root.

If input ends immediately after the record, nothing must be flushed: the consistency bit already reflects its logical effect. The pending list is part of the representation, not deferred decision work. Incomplete syntax rejects. If a name is too short for the worker’s guarantee, the length checker rejects that word independently, so no unfinished worker is used to decide a valid input.

Checking the length condition as names arrive

The length bound is not advice or a supplied header. Keep immutable unary stacks representing the smallest and largest previous name lengths, $m$ and $M$. Build a unary stack for each new name while reading its bits.

During a new name of length $\ell$, use independent cursors to check

$$\ell\le Cm,\qquad M\le C\ell.$$

For the first comparison, a finite phase counter spends one of the $m$ stack cells per $C$ arriving bits; another bit after all $Cm$ positions have been spent rejects. For the second, pop up to $C$ cells from the stack for $M$ per arriving bit and require emptiness at the delimiter. Separate one-pop-per-bit cursors compare $\ell$ with $m$ and $M$ to select the new minimum and maximum roots. The newly built length stack is available at that delimiter. All counters other than the unary stacks have fixed finite range.

The first name initializes both roots. Assuming the preceding lengths obeyed $M\le Cm$, the two displayed comparisons are exactly what is required for the new minimum and maximum to obey the same condition. Thus every name is checked without an end scan, arithmetic on addresses, or an input-sized integer register. Any violation persists under extension and can latch rejection.

Component tables

For a current component with ordered list of names

$$W=(w_1,\ldots,w_t),\qquad t\le k,$$

retain its exact feasible relation $R\subseteq D^t$. At each member’s dictionary terminal store the same $W,R$ and that member’s coordinate $j$. Since $D$ and $k$ are fixed, $t,R,j$ are finite data. The list $W$ is represented by at most $k$ immutable FIFO references. An unseen name is a singleton component with relation $D$; its spelling FIFO is built while its first occurrence arrives.

The invariant is that different component lists are disjoint, cover all variables already mentioned, and their feasible relations describe all assignments satisfying the processed constraints. The logical dictionary, including its pending replacements, contains the same current table at every member of a component. A permanent rejection bit records an empty feasible relation or an exceeded component bound.

Unary records

If U(w); addresses coordinate $j$, replace the component relation by

$$R'=\{z\in R:z_j\in U\}.$$

Compute whether $R'$ is empty now. Produce one replacement per component member, using the existing list $W$ and its respective coordinate. There are at most $k$ replacements.

Binary records within one component

After reading the first endpoint, its full component list $W$ is available. While the second endpoint arrives, compare it in parallel with every spelling in $W$. If it equals $w_j$ and the first endpoint was coordinate $i$, set

$$R'=\{z\in R:(z_i,z_j)\in B\}.$$

This covers repeated edges and $i=j$ self-loops. In particular, a repeated-name record does not increase component size. The comparison works for a newly seen first name too, since its spelling has just been collected. Publish the replacement table to all members through the pending list, and decide emptiness immediately.

Binary records joining two components

If the second endpoint matches no name in the first component’s complete list, its component is disjoint by the invariant. Its current payload is obtained from $T'$. Suppose its table is $(V,S)$, with size $s$, and its endpoint coordinate is $j$. If $t+s>k$, reject: adding this edge makes the checked graph restriction false. Otherwise use the concatenated ordered list $(W,V)$ and relation

$$R'=\{(x,y)\in R\times S:(x_i,y_j)\in B\}.$$

This is a finite table operation. It is valid even for full or empty $B$ and for pins that preceded the edge. Generate $t+s\le k$ replacements with their new coordinates. No old component member is traversed to discover its name; all spellings were stored in the two bounded headers. Traversing those spellings to install the replacements is precisely the worker’s charged task during the next name.

The relation formulas prove the invariant inductively. An empty table gives a contradiction that later conjuncts cannot remove. Component size is also monotone under added primal edges. At each complete-record boundary, acceptance is exactly well-formedness, the two checked restrictions, and nonemptiness of every component table.

Native realization and resources

The implementation has a fixed number of rooted cursors: snapshot and worker tries, one worker path FIFO, at most $k$ pending spelling comparators, at most $k$ current-component comparators, bounded component headers, spelling builders and the length-check stacks. The worker’s program state is finite. Each scheduled step uses the existing strict queue and one-node trie operations; it can pause after any step.

Unrolling the fixed number of steps assigned to one input symbol gives constants $q,A,r$ depending only on $D,\Gamma,k,C$: fixed record arity, bounded fresh records, and bounded old-address radius. Guards inspect finite labels and empty-stack/queue markers. New references target exposed old fields or declared same-batch records. No guard compares pointers, reads an address, or assumes mutable memoization. The initial empty dictionaries, FIFOs, stacks and parser state form a fixed finite virtual graph.

These are the hypotheses of the reviewed bounded-batch native compiler. It yields one physical scaffold node per input symbol, plus the base. All source work and retained auxiliary history, including unfinished final writes, cost $O_{D,\Gamma,k,C}(N)$ records; explicit pointer serialization costs $O_{D,\Gamma,k,C}(N\log(N+2))$ bits. There is no independent preprocessing phase. The number of distinct variables satisfies $b\le N$.

The reversed input orientation

A reversed unary record has the form ;)w^R(U; a reversed binary record has the form ;)v^R,u^R(B. The parser reads one or two names and validates the relation tag and its arity at the end. It retains the component tables and endpoint coordinates until that tag arrives; their total size is fixed. A binary tag then applies its transposed relation because the endpoints were encountered in reverse order. Unary tags apply their ordinary restriction. The pending batch is created at this final tag, where the answer is already ready.

Internally treat the reversed spellings as variable names. Reversal is a bijection on literal words and preserves their lengths. Reversing the record sequence does not change the final conjunction, graph components or length condition. Every graph-size, inconsistency or length violation remains permanent under further records, so early rejection is sound in this order too. The same pending-write budget applies during the next record’s first name. Malformed reversed syntax rejects.

This constructs a native recognizer for the reversed language directly. Applying the established scaffold/PEG correspondence separately to the two orientations gives PEGs for both. No closure under reversal is assumed.

What this resolves, and what it does not

The fixed-pair difficulty has a positive answer under the checked name-length condition, even with arbitrary edge and pin order. The method also handles all fixed-size components. Its structural point is that the latest component changes fit into a bounded list, which remains directly searchable while older dictionary writes finish. A physically current dictionary is unnecessary; a logically current answer is sufficient.

This does not settle star forests with arbitrarily large components or unrestricted equality SAT. A star update can affect unboundedly many terminal copies, and wildly different name lengths invalidate the displayed worker budget. Neither is proved necessary for recognition: they are the limits of this construction. In particular, failure of this schedule for unrestricted names is not a language lower bound.

The method extends classical real-time scheduling rather than introducing that method. Okasaki’s Purely Functional Data Structures, thesis §5.2, printed page51 explains incremental rebuilding, coexisting working/rebuilding versions, and buffering changes before switching versions. Here the additional argument is the bounded pending-name comparison, its exact serial-input budget, and its combination with checked small-component SAT under the native model. The component-table operations are elementary finite-domain constraint elimination. This is a specialized native construction, not a claim to a new general persistence theorem.

The next decisive question is whether a different pending-update representation can remove the name-length restriction without losing the final-symbol deadline, and whether unbounded stars can avoid copying their entire component state.