A bounded shared core can coordinate arbitrarily many constraint pieces

5 October 2026. Written native construction extending the bounded-cover and bounded-component methods.

Take arbitrarily many triangles with one shared vertex. The shared vertex can link the behavior of every triangle, so the whole graph has an unbounded component and an unbounded minimum vertex cover. Yet deleting that one vertex leaves disjoint pairs. Once its value is fixed, those pairs can be solved independently.

This familiar decomposition also supports strict native recognition. The core need not be supplied or identified early. A recognizer can discover it as constraints arrive, retain the relevant alternatives, and answer after the last symbol. The naming condition is local: names within each remaining piece must occupy a bounded range of doubling length classes. Core names, and the relative scales of unrelated pieces, are unrestricted.

The construction combines two earlier positive results. Its main additional step is handling a core variable discovered at the second endpoint of a record, when the earlier endpoint may have an arbitrarily different name length. A temporary core coordinate lets the recognizer prepare the first side before that discovery and validate it afterward.

Contents

Exact statement

For a nonempty binary name ww, put λ(w)=⌊log⁡2∣w∣⌋\lambda(w)=\lfloor\log_2|w|\rfloor. Fix a nonempty finite domain DD, a finite language Γ\Gamma of unary and binary relations, and constants k≥0k\ge0, m≥1m\ge1, s≥0s\ge0.

Let LD,Γ,k,m,sL_{D,\Gamma,k,m,s} contain exactly the well-formed, satisfiable record strings whose loopless primal graph GG has a vertex set CC satisfying

∣C∣≤k,∣H∣≤m,max⁡w∈Hλ(w)−min⁡w∈Hλ(w)≤sfor every component H of G−C.|C|\le k,\qquad |H|\le m,\qquad \max_{w\in H}\lambda(w)-\min_{w\in H}\lambda(w)\le s \quad\text{for every component }H\text{ of }G-C.

The core CC is existentially quantified; it is not part of the input.

Written theorem. Both LD,Γ,k,m,sL_{D,\Gamma,k,m,s} and its string reversal have deterministic native scaffolding-automaton recognizers. Consequently both have PEGs.

Records are U(w); and B(u,v);, with one fixed alphabet tag per relation and nonempty literal binary names. Leading zeros matter. Records and pins may occur in any order. A distinct-name binary record adds a primal edge even when its relation is full. A repeated-name record applies the diagonal unary restriction and adds no loop. Repeated edges and prefix-related names are allowed. Invalid or incomplete syntax rejects; the empty conjunction accepts.

One fixed automaton handles all input lengths for each fixed parameter tuple. Its initialization, finite labels, degree and observation radius are fixed. Every actual name bit and delimiter is charged to encoded length NN. There are no supplied handles, decompositions, favorable order, padding, preprocessing, old-node writes, address operations or end-of-input computation.

At k=0k=0 this gives the component-local name-scale theorem. At m=1m=1 the name condition is automatic and the structural condition is exactly a vertex cover of size at most kk, recovering the bounded-cover theorem. The shared-triangle example has k=1,m=2k=1,m=2. Its apex can have any name length, while each peripheral pair satisfies the displayed span condition. Arbitrarily many triangles give unbounded cover number because their peripheral edges form a matching.

The local storage interface

We use the proved FIFO capsule dictionary and the length-class buckets from the component-local construction. These are written implementation dependencies, not abstract constant-time dictionary oracles.

The bucket method provides the following exact interface. During a literal name ww in class jj, it obtains its logically current terminal payload and services all pending writes in the fixed bucket window [max⁡(0,j−s),j+s][\max(0,j-s),j+s]. At the name delimiter one may publish a bounded list of replacements to spellings within that window. The bucket representation is immediately logically current; physical installation may remain pending. A subsequent name starts from that committed directory. Its snapshot reader and pending-target comparators return current values even during installation.

The bound on the number of replacements may be any fixed constant: enlarge the fixed worker rate accordingly. Payloads may contain a fixed amount of finite data and a fixed number of opaque spelling-FIFO pointers. Servicing changes no logical value. The directory is committed through its current capsule path; an earlier saved path is never restored over later changes.

In that proof, a class-jj name supplies at least 2j2^j symbols, while every pending target in its window has length below 2j+s+12^{j+s+1}. Fixed-rate installation therefore suffices. Ahead readers replay the growing prefix at speed two, so the appropriate bucket is ready even though the class was not given in advance. Initialization at length one, class comparison by unary stacks, all temporary history and abandoned lookahead are already charged there.

This interface is used at both endpoint delimiters. That is essential: the first endpoint’s window may be unavailable when a much shorter second name finishes.

What a stable branch means

A branch keeps an ordered core C=(c1,…,ct)C=(c_1,\ldots,c_t), t≤kt\le k, and a finite table Q⊆DtQ\subseteq D^t of exactly the core assignments extendible to a solution of all processed constraints.

Core names are stored as at most kk immutable spelling FIFOs. Every arriving name is compared against them bit by bit, including exact termination. No comparison of pointer identities is used. A core terminal’s old peripheral payload can be ignored permanently; the explicit comparisons identify the role even if that payload was never erased.

Every component HH of G−CG-C has at most mm members. Its replicated payload stores:

  • its ordered member spellings and the addressed member’s coordinate;
  • raw primal adjacency, separately from relation values;
  • unary masks, intersections of internal binary constraints, and oriented binary restrictions between each member and each core coordinate;
  • member length-class offsets relative to the addressed member.

All masks, adjacency and relation arrays are finite. Spelling references are the only unbounded data in this bounded header. Unused core slots have full relation and remain full until that slot is introduced locally. Raw adjacency must be retained: an edge labelled by the full relation is still an edge, and future promotion may split a component.

Let PH(a,xH)P_H(a,x_H) be the conjunction of these raw factors, conditional on core assignment aa. The formula factors into core-only constraints and the PHP_H. The table QQ already includes every existential component condition ∃xH PH(a,xH)\exists x_H\,P_H(a,x_H).

A restriction within HH replaces its factors by stronger ones and updates

Q←Q∩{a:∃xH PHnew(a,xH)}.Q\leftarrow Q\cap\{a:\exists x_H\,P_H^{\rm new}(a,x_H)\}.

No old factor needs removing because the new condition implies the old one. A legal merge uses the product of the two local factors intersected with the new edge relation, then makes the same update. Core-only constraints restrict QQ directly. These operations are finite table maps.

Promotion without losing correlations

Choose a subset SS of one old peripheral component HH and make its members new core coordinates zSz_S. Set

Q′(a,zS)=Q(a)∧[∃xH∖S  PH(a,zS,xH∖S)].Q'(a,z_S)=Q(a)\land \bigl[\exists x_{H\setminus S}\;P_H(a,z_S,x_{H\setminus S})\bigr].

This is the exact extendibility table for the enlarged core. The new condition implies the old existential condition for HH that was already in QQ.

Use raw adjacency to split H−SH-S. For each new piece, retain its internal factors and turn its old edges to SS into incidences to the new core coordinates. Factors wholly on the enlarged core are included in Q′Q'. Other old components acquire unconstrained new coordinates and need no rewrite: before promotion they had no edge to any member of HH.

It is crucial to condition before splitting. In the equality path u=x=vu=x=v, promoting xx leaves the factors u=zu=z and v=zv=z. Forgetting xx and retaining separate unconditional marginals would lose their correlation and incorrectly permit opposite late pins on uu and vv.

All surviving members of H−SH-S were in the old bounded-span component. Its at most mm replacements fit the window serviced by any queried member of HH. Even promotion of a member whose name is not the queried endpoint is therefore local. Its spelling was already present in the bounded header.

When discovery needs a new branch

Unary records, core incidences and edges within one peripheral component cannot violate the component size or span bounds. A possible violation occurs only when an edge joins two distinct peripheral components H,JH,J. Before that edge both are legal, and their union has at most 2m2m vertices.

If the union remains legal, retain the unique continuation with no promotions. If it is illegal, consider every nonempty subset S⊆H∪JS\subseteq H\cup J that fits the remaining core budget. Promote SS and retain the continuation only if every new peripheral piece is legal. This description is a finite semantic branching rule. The next section implements it without waiting for both names before doing all the work.

For completeness, fix a core C∗C^* witnessing the final input’s structural condition. Follow a branch with C⊆C∗C\subseteq C^*. At an illegal merge, deleting S=(C∗∖C)∩(H∪J)S=(C^*\setminus C)\cap(H\cup J) leaves pieces contained in final components of G−C∗G-C^*. Thus every piece obeys both bounds. This SS is nonempty, or the illegal union would survive in the final graph. Selecting it preserves containment and never exceeds kk.

The number of histories is bounded independently of input length. Put B=22mB=2^{2m} and give a stable branch with tt core vertices weight Bk−tB^{k-t}. A violating merge has at most BB surviving children, each spending at least one core slot. Their total weight is no greater than the parent’s. Valid records have one continuation per branch, and discarded branches reduce weight. Starting from one empty-core branch gives at most BkB^k stable branches. Keeping optional promotion branches on valid records would break this argument; the construction explicitly discards them.

Scheduling a binary record

The relation tag is known before the forward record’s names. All hypotheses below are deterministic parallel simulations in a fixed number of header slots, not nondeterministic guesses.

If the first endpoint uu is already in the core, the second name’s comparisons identify either a core coordinate or a peripheral component. At its delimiter the new relation changes QQ, or changes that component’s incidence to uu and publishes its bounded replacements in the second window. No discovery branch is needed.

Suppose instead uu belongs to peripheral component HH.

An existing core as the second endpoint

For each current core coordinate ii, start a temporary plan. At the first delimiter, impose the new incidence between uu and cic_i, update QQ, and publish the replacements for HH in the first window. Read the second name from the newly committed directory and retain this plan exactly when the name is cic_i.

Only one such plan can validate. This is the same bounded endpoint speculation used by the cover construction, now applied to a small component instead of a single leaf.

Two endpoints outside the old core

Start plans indexed by a subset SH⊆HS_H\subseteq H and a Boolean flag VV. The subset names members of HH to promote at the first delimiter. The flag predicts whether the second endpoint itself will be promoted. Do not exceed the remaining budget. Keep the unmodified old header of HH for final validation.

At the first delimiter:

  1. Promote SHS_H by the displayed lemma and split H−SHH-S_H.
  2. If V=1V=1, reserve one additional core coordinate zz for the as-yet-unread second endpoint. For now zz is a fresh formal variable. If uu remains peripheral, put the relation B(u,z)B(u,z) into its component’s new incidence slot and impose that component’s new existential condition on QQ. If uu was promoted, impose B(u,z)B(u,z) directly on QQ.
  3. Publish all changed surviving members of HH, at most mm, in the first serviced window and commit that directory. The reserved slot has no spelling comparator until it is bound.

Read the second name from this directory. Compare it in parallel against all original core names and all original member spellings of HH.

If it equals a member of the old core, discard these plans. If it belongs to original HH, discard every promotion or reserved-coordinate plan. The sole SH=∅,V=0S_H=\varnothing,V=0 plan handles the ordinary within-component edge, including a self-loop, with the exact local table update. Its writes fit the second window.

Otherwise the second endpoint vv lies in a different original component JJ. Its current header is unchanged semantically by the first-side promotions: there was no prior residual edge between HH and JJ. Using the saved original HH and this JJ, check whether the original unpromoted merge was legal.

  • If legal, retain only SH=∅,V=0S_H=\varnothing,V=0 with no second-side promotions, and do the ordinary merge.
  • If illegal, try every second-side subset SJ⊆JS_J\subseteq J, requiring v∈SJv\in S_J exactly when V=1V=1. Keep only nonempty combined selections, total core size at most kk, and legal resulting residual pieces.

When V=1V=1, bind the reserved coordinate to the actual vv; it is not allocated a second coordinate. Other members of SJS_J receive fresh slots. If their values are qq, the additional table condition is

∃xJ∖SJ  PJ(a,v=z,q,xJ∖SJ).\exists x_{J\setminus S_J}\;P_J(a,v=z,q,x_{J\setminus S_J}).

Before binding, QQ represented the old formula with vv still existential in JJ, together with the new relation to the fresh formal zz. The displayed condition implies the old existential factor for JJ and identifies precisely the selected values. Thus intersection gives the exact new table. No old existential condition needs retracting. The disjoint-original-component test is essential to this argument.

When V=0V=0, promote SJS_J excluding vv in the usual way, then process the new edge. If uu was promoted, it is a core incidence on the piece containing vv. Otherwise it joins the pieces containing uu and vv. In the latter case, check the final merged size and span and retain the plan only when both are legal.

Why every final write has a serviced window

There are three cases after second-side selection:

Endpoints after selection First-side work Work at the second delimiter
vv is selected Its incidence was prepared using reserved zz Split/update members of JJ only
vv remains peripheral and uu is selected Promotion and split of HH already committed Split/update members of JJ only
Both remain peripheral Pieces split off from uu already committed Update the legal merged piece and other pieces of JJ

All members of JJ lie in the second endpoint’s original serviced window. In the third case the accepted merged piece has span at most ss and contains vv, so all its first-side members also lie in that window. No other first-side piece changes at this point. Additional new core slots have no earlier incidence to those separate pieces.

There are at most 2m2m final targets in the window. Enlarge the pending-batch capacity and worker rate to this fixed bound. Any first-side pending writes in that window have already been serviced while the second name arrived; first-side writes outside it remain intact. Commit using the second name’s current directory, never the first name’s saved path.

The original and final span tests use the existing unary class counters. If ∣ju−jv∣>s|j_u-j_v|>s, the original union is certainly illegal. Otherwise shifting the old finite offsets permits an exact finite maximum-minus-minimum test. A final residual merge retaining both endpoints must again have ∣ju−jv∣≤s|j_u-j_v|\le s; its bounded offsets can then be tested and rebased. Pieces produced by deletion inherit legality from their old component. A selected endpoint never imposes a spurious name-length restriction on the other endpoint.

Each combined subset has exactly one SH,SJ,VS_H,S_J,V description, with fixed coordinate order within each old header. Thus this schedule realizes the semantic branching rule and its history bound. Temporary plans add only a fixed factor for old-core predictions, subsets and the one flag.

Correctness, deadline and both orientations

The promotion identity, conditional raw factors and exact merge/restriction maps prove the semantic invariant. Every surviving stable branch supplies a genuine core and legal residual components. Its QQ is exactly the set of extendible core assignments. Conversely the branch following any final witness C∗C^* survives every structural test; a satisfying assignment makes its QQ nonempty. Hence the input is accepted exactly when at least one surviving branch has nonempty QQ and the finite parser is at a complete-record boundary.

Empty tables can be discarded. Unary pins on a core coordinate restrict QQ immediately; pins on a residual member update its bounded local table. Neither causes a scan of the other pieces. Syntax, repeated names, full-relation edges and late input end are handled by the cases already stated.

For reversal, a record has form ;)rev(v),rev(u)(B or ;)rev(w)(U. At its beginning run the finitely many tag/arity hypotheses. Apply the same procedure to the reversed name spellings, using the transposed binary relation. Validate the actual tag at the record’s final symbol and discard incorrect hypotheses. The unique correct tag survives; the extra temporary width is fixed. Name reversal preserves identity and lengths, and reversing the order of conjuncts preserves the final property. This constructs a second recognizer directly, without assuming reversal closure. The scaffold/PEG correspondence then supplies PEGs for both orientations.

All tables and plan choices have fixed finite size. Each input symbol advances a fixed number of FIFO, dictionary, spelling comparison and unary-stack operations in each of a fixed number of branches. At delimiters there are fixed finite table maps and bounded header copies. Guards read labels, bits and queue/stack termination; no guard tests an address or pointer identity. Initialization is a fixed finite pointer-closed graph.

The reviewed simultaneous-record compiler therefore applies with constants depending only on D,Γ,k,m,sD,\Gamma,k,m,s. The native run has N+1N+1 physical nodes. All logical work and allocated history, including dead plans and pending writes, are OD,Γ,k,m,s(N)O_{D,\Gamma,k,m,s}(N) bounded records, or OD,Γ,k,m,s(Nlog⁡(N+2))O_{D,\Gamma,k,m,s}(N\log(N+2)) explicit pointer bits. Storage installation may be unfinished at input end; the answer is already computed and requires no flush.

What the result adds

The structural idea is classical. Vertex integrity minimizes the sum of core size and largest residual component size; see Gima and coauthors, introduction. The separate bounds k,mk,m used here describe the same core-and-small-pieces geometry, with an additional name-span restriction.

Dvorak, Eiben, Ganian, Knop and Ordyniak, IJCAI2017, Sections3-4 study fracture backdoors for integer linear programs. Their detection argument branches on vertices of a small connected obstruction. Our finite semantic branching uses that established principle. The domain, constraint problem and strict serial machine model differ; their offline parameterized bounds are not imported as native recognition bounds.

The contribution here is an extension of the earlier native constructions: late core discovery, conditional splitting, bounded deterministic histories, and the reserved-coordinate schedule together make that decomposition usable by the last symbol. The local name-scale hypothesis remains explicit. The proof is written and independently audited, not mechanically verified.

The theorem unifies the previous cover and component positives and permits one small shared core to coordinate an unbounded collection of interacting pieces. A separate prefix-clause construction gives a different route with unbounded clause width and no fixed core bound.

The immediate extension to test is ordinary three-literal clauses. In particular, a selected core variable might be the last of three endpoints, after two peripheral names have already been read. A corresponding multi-endpoint publication argument would give the same structural positive directly for 3SAT; the binary proof does not establish it. A further structural question is whether arbitrarily many local cores, or recursively decomposable pieces, can replace the one globally bounded core while retaining the deadline and correlation invariants.