Shared cores support ordinary three-literal clauses

5 October 2026. A bounded-arity extension of the shared-core native construction.

Think of a constraint formula as many small local pieces that communicate through a few shared variables. Once the shared variables are fixed, each remaining piece can be solved independently. The difficulty here is operational: the input does not identify this core or provide a decomposition, yet a scaffolding automaton must discover a valid choice while the clauses arrive and must answer at the final symbol.

The result is positive for every fixed finite constraint language of bounded arity. If deleting some bounded set of variables leaves bounded components whose names have bounded local scale differences, a native recognizer can check that structure and satisfiability together. In particular, this includes ordinary signed 3CNF under the same condition. Clause order, literal order, late pins and the names of core variables remain unrestricted.

For example, in C(+u,+v,+c);, suppose u and v remain peripheral while c becomes a core variable. The constraint on the peripheral pair can be stored as a relation conditional on the value of c before its name has been read.

The crucial deadline is the last peripheral name in a clause, which need not be its last name. At that point all residual pieces affected by the clause fit one serviced name window. Later names may belong to the core, with arbitrarily different lengths. Their values can already appear as formal coordinates in the conditional clause table; their identities are validated when they arrive.

This extends the earlier binary construction rather than characterizing all tractable SAT presentations. It still requires one globally bounded core. A formula with arbitrarily many separate local hubs, such as a growing family of disjoint stars, remains outside the theorem and supplies the next structural test.

Statement and ordinary encoding

Fix a nonempty finite domain $D$, a finite relational language $\Gamma$ of maximum arity $r\ge1$, and integers $k\ge0,m\ge1,s\ge0$. A record for an arity-$a$ relation is R(w1,...,wa);, with a fixed alphabet tag for each relation and nonempty binary variable names. Leading zeros are significant. Repeated variables and repeated records are allowed. Nullary relations, if present, are handled directly in finite control.

Each record adds a clique on its distinct variables to the loopless primal graph $G$, including when its relation is full. Put $\lambda(w)=\lfloor\log_2|w|\rfloor$. Define $L$ to consist of exactly the well-formed satisfiable streams for which some set $C$ satisfies

$$|C|\le k,\qquad |H|\le m,\qquad \max_{w\in H}\lambda(w)-\min_{w\in H}\lambda(w)\le s \quad(H\text{ a component of }G-C).$$

Written theorem. Both $L$ and its string reversal have deterministic native scaffolding-automaton recognizers, and consequently both have PEGs.

3CNF corollary. Take ordinary signed clauses C(+u,-v,+w); with zero to three literals, using the same literal binary names and delimiters. Accept exactly the satisfiable formulas satisfying the displayed structural condition. Both orientations have native recognizers and PEGs. Signs and literal order are unrestricted; C(); is an unsatisfiable empty clause. A tautological clause still contributes the clique on its distinct syntactically occurring variables. This convention is explicit and requires no preprocessing.

The finite possibilities for arity and sign pattern can be simulated in parallel from the clause start and checked against the actual signs and terminator. They supply the finite relation tags needed by the general construction without inserting symbols, padding or a preprocessing pass. A sign mismatch discards its simulation. Thus this is recognition of the stated ordinary encoding, not a claim transferred through an uncharged normal-form conversion.

All parameters are fixed before input length $N$. Each automaton has finite initialization, fixed degree, labels and observation radius. Every name bit and delimiter is charged. There are no supplied cores, decompositions, favorable orders, remote handles, old-cell writes, address tests or end-of-input cleanup.

The inherited implementation and the larger local factor

The binary shared-core proof supplies the promotion identity and bounded-history strategy. Its component-local bucket implementation supplies a specific storage interface: while a name in class $j$ arrives, its logically current payload is obtained and old pending writes in $[\max(0,j-s),j+s]$ are serviced. At its delimiter a fixed number of replacements targeting that window can be published. Every subsequent name starts from the newly committed directory. Snapshot readers retain their pending overlays; outside-window work is preserved. This is the proved FIFO/capsule implementation, not a free dictionary oracle.

A stable branch keeps an ordered core of size $t\le k$, its spelling FIFOs, and the exact extendibility relation $Q\subseteq D^t$. Each residual component has at most $m$ member spellings, a coordinate for the addressed member, finite class offsets, raw primal adjacency, and its conditional constraint factors.

For higher arity, store an array of relation tables indexed by ordered tuples of core/member coordinates of length at most $r$. Repeated factors on a tuple are intersected. This array is finite for fixed $D,\Gamma,k,m,r$; repeated coordinates implement repeated variable names. Raw adjacency remains separate. Core-only factors can be absorbed into $Q$.

Write the conjunction of a component’s raw factors as $P_H(a,x_H)$. Every constraint’s noncore variables lie in a single residual component, since its primal support is a clique. After promoting $S\subseteq H$, every factor’s remaining variables again lie in a single component of $H-S$. This clique fact is what makes conditional splitting exact for higher-arity factors. An arbitrary hypergraph presentation with only some co-occurrence edges would not justify it.

Promotion introduces values $z_S$ as new core coordinates and intersects the cylindrical extension of $Q$ with

$$\exists x_{H\setminus S}\;P_H(a,z_S,x_{H\setminus S}).$$

Keep the factors conditional on those coordinates before splitting. The displayed condition implies the old existential condition for $H$, so the old contribution already in $Q$ need not be removed. Other original components had no constraint sharing a noncore member of $H$; their new slots are unconstrained. Their payloads need no rewrite.

The finite semantic branching rule

Consider one record relative to the core at its start. Its noncore endpoints meet distinct original components $H_1,\ldots,H_h$, with $h\le r$. Unseen variables are fresh singleton components. Their union $U$ has at most $rm$ members. The new record joins these components into one if any remain; core endpoints are absent from the residual graph.

If this unpromoted union is legal, retain only the continuation with no promotions. Otherwise enumerate nonempty subsets $S\subseteq U$ fitting the remaining core budget. Promote $S$, add the record, and retain exactly the continuations with legal final residual components.

For any final witnessing core $C^*$, a branch with $C\subseteq C^*$ can select $(C^*\setminus C)\cap U$ at an illegal union. It is nonempty, and the resulting pieces are contained in final components of $G-C^*$. Both bounds are hereditary under taking such pieces. This proves completeness of discovery, including late discovery.

With $B=2^{rm}$, give a branch with $t$ core vertices weight $B^{k-t}$. A legal record has one child. An illegal record has at most $B$ children, each using at least one new slot, so total weight cannot increase. There are at most $B^k$ stable histories. The implementation below preserves one child per selected subset; speculative coordinate permutations are not allowed to create extra stable histories.

A record plan and first encounters

At record start simulate a fixed finite collection of plans. A plan predicts:

• the number $\ell\le k-t$ of new core vertices;
• for each endpoint, either an old core coordinate, one of the $\ell$ new coordinates, or a peripheral role;
• equivalently, the position $p$ of the last peripheral endpoint, or that no such endpoint exists.

All $\ell$ new coordinates are initially formal variables without spellings. They are not extra input or advice: every prediction is checked, and all parallel simulations have fixed total width. The finite arity/relation hypotheses for ordinary signed syntax are included here.

During every name, compare its actual bits and exact termination with old core names and all member spellings in previously encountered original components. At most $k+rm$ comparisons are needed. These identify repeats and original-component membership without pointer identity. Save each new original component’s full raw header and first-encounter name-class counter. Never reconstruct an original header from a later split or merged payload.

On the first encounter with an original component $H$:

1. Choose its entire subset $S_H$ of members to promote, including members that are not endpoints of this record.
2. Assign them the next unused new slots, in the stored member order. Original components receive blocks of slots in first-encounter order. This is a canonical assignment, not an arbitrary permutation.
3. Bind those slots to the member spellings already present in the header; intersect $Q$ with the conditional projection of the original $P_H$.
4. Split $H-S_H$ using raw adjacency. Publish all surviving pieces, at most $m$ member replacements, in this first encounter’s serviced window.

A later endpoint in original $H$ uses this saved choice and header; it cannot make a second promotion choice. If the name is new, its singleton header and spelling have just been constructed during that name. Every endpoint prediction is checked against its actual role after the first-encounter choice. At record end all $\ell$ slots must be bound and no extra selection is allowed.

For a fixed final subset $S$, these rules uniquely determine $\ell$, the slot order, the endpoint roles and $p$. On a legal original union, discard every plan with $\ell>0$. On an illegal one, require $\ell>0$. Thus temporary speculation does not invalidate the stable-history bound.

Publish the clause at its last peripheral endpoint

Before position $p$, the new record’s factor has not yet been imposed. Already encountered original components have been conditionally split and published. Keep their raw headers and selections in a bounded record workspace. They describe every split piece needed later even if a terminal payload has changed.

At position $p$, perform that endpoint’s first-encounter promotion, if needed, before processing the record. All peripheral endpoints are now known. Identify their residual pieces from the saved original headers and selections, with duplicates removed by finite component/member coordinates. Every such piece contains a peripheral endpoint of this record.

Let $M$ be their union. The new primal clique joins precisely these pieces into one component. Reject the plan if $|M|>m$ or its class span exceeds $s$. Otherwise multiply their conditional raw factors and the new relation, with each core endpoint replaced by its predicted coordinate. Some new coordinates may still lack spellings. Intersect $Q$ with the resulting existential condition on $M$ and publish its new header at every member.

All members of $M$ lie in the window serviced by the endpoint at $p$, because $M$ contains that endpoint and has span at most $s$. Pieces split off earlier and not meeting a peripheral endpoint do not acquire the new factor. They keep their earlier published payloads.

If there is no peripheral endpoint, the new relation is core-only and is imposed directly on $Q$ at the record terminator, after the names have been validated. No component publication is then required for that relation.

Names after the last peripheral endpoint

Every later endpoint must validate as old or newly selected core. It may nevertheless be the first encounter with another original component $J$: the arriving endpoint is selected from $J$, while its other members may remain peripheral. At its delimiter condition the whole original $P_J$, bind the appropriate slots, split and publish $J-S_J$ in its own window. No member of those residual pieces is an endpoint of this record, or the earlier prediction of $p$ was false and the plan is discarded.

This later binding is semantically exact. Before it, $Q$ contains the original existential condition $\exists x_J P_J$ and may contain the new clause as a condition on a formal coordinate $z$. Binding selected members of $J$ intersects with

$$\exists x_{J\setminus S_J}\;P_J(a,z_{S_J},x_{J\setminus S_J}).$$

That condition implies the old existential one and correlates precisely the selected values with the already imposed clause. It neither forgets their values nor identifies them with a second copy. Distinct original components are independent conditional on the old core. If $J$ had already been encountered, its entire selection and bindings were done then, so this operation is not repeated from a post-merge header.

This also explains why a final core endpoint of very short name length causes no debt: the earlier merged peripheral component was already published at $p$.

Every write and every class comparison is charged

At an ordinary first encounter, only that old component’s surviving members are written, at most $m$. At $p$, combine this list with the merged-piece replacements before publishing; the newer merged payload wins for overlapping targets. There are at most $(r+1)m$ targets, all in the serviced window. A fixed enlargement of batch capacity and worker rate suffices. A later first encounter writes only its own old component. Pending work outside the current window is retained; the current directory is committed, never a saved earlier path.

Class comparisons use the inherited unary counters, copied as cursors and advanced during each later name. There are at most $r$ saved origins. For the original union’s span test, a pair of origin classes differing by more than $s$ already proves illegality, since those origins belong to the union. Otherwise their finite member offsets give the exact span.

For the final merged piece, an old component’s saved origin might itself be promoted and absent from that piece. Its class can differ from the current endpoint’s class by as much as $2s$, even when the merged piece is legal: at most $s$ to one of its surviving endpoints, then at most $s$ to the current endpoint. Compare with threshold $2s$, shift the saved finite offsets, and test the actual retained members’ span exactly. Rejecting at threshold $s$ here would be incorrect. Deleted side pieces inherit legality and need no global class comparison. These are fixed lookahead and finite-table operations, not arithmetic on unbounded numeric addresses.

Correctness and resources

At a stable boundary the raw component factors, core table and logical dictionary have the same invariant as in the binary proof. Within a record, conditioned original factors replace their older projections by stronger conditions. At $p$, the product for the merged piece and the new record replaces the separate projections by a stronger condition. Later bindings add the exact conditional projections of previously untouched components. This yields precisely the conjunction with the new constraint, conditioned on the final selected core.

The raw clique graph ensures every surviving factor is assigned to one residual piece or to the core. First-encounter headers prevent accidental reconditioning from a transient merged table. The finite record validation ensures all formal coordinates correspond to actual selected names and every retained plan realizes exactly one semantic child. Soundness and the witness-following argument therefore prove the stated language equality.

Acceptance is nonempty $Q$ in some stable branch at a complete-record boundary. Invalid or incomplete syntax rejects. Empty conjunctions accept; an empty clause makes $Q$ empty. Contradictions, including arbitrarily late pins, are resolved immediately in finite tables. Deferred physical installation never defers the answer.

For reversed input, hypothesize the finite relation/arity at record start, process reversed endpoint order with the correspondingly permuted relation, and validate the final tag. In signed syntax the sign follows rather than precedes the reversed name; its finite hypothesis is checked on arrival. Reverse each spelling consistently. Identity and name lengths are preserved. The same first-encounter and last-peripheral schedule works in this reading order, giving a direct second recognizer. Apply the scaffold/PEG correspondence separately to both recognizers.

There are at most $B^k$ stable histories, a fixed number of record plans per history, at most $r$ saved original headers, and at most $k+rm$ parallel spelling comparisons per plan. Tables have fixed finite size. Each symbol performs a bounded number of already proved FIFO, trie, unary-stack and finite-header operations. Opaque pointers are copied from exposed fields; no guard tests their identity. Initialization is a fixed finite pointer-closed graph.

The reviewed simultaneous-record compiler applies. The native run has $N+1$ physical nodes. All source work and allocated history, including dead plans, are $O_{D,\Gamma,r,k,m,s}(N)$ records, with $O_{D,\Gamma,r,k,m,s}(N\log(N+2))$ explicit pointer bits. No formal verification is claimed.

Significance and the next structural test

The result puts ordinary three-literal clauses directly inside the positive construction. The restriction concerns how interactions remain organized after deleting a small core; it does not reduce clauses to binary syntax or require a supplied decomposition. Arbitrarily many peripheral pieces can constrain the same core values while each is maintained locally.

The offline decomposition and conditional enumeration are classical. The preceding proof’s primary comparison credits vertex integrity and fracture-backdoor methods. This extension adds a native scheduling argument for multi-endpoint constraints: first-encounter whole-component selection, canonical formal coordinates, and publication at the last peripheral endpoint. It is an extension of the existing construction, not a new offline tractability criterion.

The next substantial question is whether arbitrarily many local cores can replace one globally bounded core. Disjoint stars are the first test: each has a one-vertex separator, but a growing family need not have a globally bounded deletion set leaving bounded pieces. The present finite global $Q$ does not solve that problem. Independently, the prefix-clause construction still raises the different question of removing its common literal-order requirement.