Adding state preserves the dynamics of a star
5 October 2026. An exact semantic construction and the remaining native recognition test.
Can scaffolding automata recognize satisfiable constraints on arbitrarily many independent stars? The shared-core theorem allows one globally bounded set of coordinating variables. Independent stars would allow unboundedly many local coordinators, each with arbitrarily many leaves. That native extension remains open.
There is a useful exact result on the representation side. Moving the represented center to a leaf can destroy conditional independence. Adding the original center’s value to that leaf repairs the problem: a domain suffices, preserves all original named observations, and supports repeated changes of center without further growth. We give the correspondence, its update laws and a matching minimum for this representation shape. The construction is a specialization of classical lossless joins and hidden-variable representations.
Contents
The language and deadline under consideration
Fix a nonempty finite domain and a finite collection of unary and binary relations, including singleton pins. Use ordinary records U(w); and R(u,v);, with one alphabet tag for each relation and nonempty binary names. Leading zeros distinguish names. Names, records and endpoints may occur in any order; repeated records and self-loops are allowed. A self-loop imposes the corresponding diagonal unary condition. Each binary record on distinct names adds its edge to the raw primal graph, even if the relation is full.
The candidate language consists of the well-formed, satisfiable streams whose raw graph is a star forest, with a fixed per-component bound on the range of
Isolated vertices and single edges count as stars. No centers, component labels or ready handles are supplied. Malformed or structurally invalid inputs are rejected. For Boolean SAT take ; all unary and binary Boolean relations form one fixed finite choice of alphabet. The semantic examples below use equality and the full binary relation from that choice.
All encoded symbols count. Without whitespace,
The target is one deterministic native automaton for each fixed parameter choice. Starting from the unlabelled base, each symbol adds one node. Control, labels, degree and observation radius are fixed. New edges follow bounded port paths from the previous top, are missing, or point to the new node itself; observations are labeled unfoldings. Acceptance is the final finite-control state. No preprocessing, supplied annotation, pointer-identity test, old-cell mutation, padding or end-of-input cleanup is available. The semantic construction below does not itself supply such an automaton or a PEG consequence.
What the quotient must remember
Fix a named star with original hub and leaves . Every original name remains available to later pins. Two constraint systems are indistinguishable by all future SAT tests exactly when they have the same full relation of assignments on these names. Equality is sufficient because later constraints are conjoined with that relation. It is necessary because singleton pins can select any tuple in the symmetric difference. This applies the existing boundary-equivalence lemma to the entire accessible interface; the leaves are not sealed private variables.
Let be that solution relation. Define
Rows outside are canonically empty. For a nonempty relation every displayed row is nonempty, and
Thus the feasible hub values and their conditional leaf rows determine the relation exactly; projections recover them. The empty relation is one bottom state on the fixed interface. Keeping only loses information: equality and disequality on two Boolean names have the same feasible hub values but different answers to later pins.
The checked graph restriction needs additional information. On the same three named variables, take one full edge with isolated , or two full edges . Include the full unary record in both streams so all three names occur. Their solution relations agree. Appending the full edge produces a star in the first case and a triangle in the second. Choose equal-length names so the scale condition agrees as well. A sufficient state therefore retains the raw structural roles and membership information, name-scale extrema and the semantic relation. Moving the semantic center does not move the syntactic graph hub.
Exactly when an ordinary change of center works
Choose a leaf . For a possible value of , put
Criterion. The same relation factors as a star centered at , without enlarging , if and only if for every and every other leaf , the sets are identical as ranges over .
To prove this, fix . The remaining relation is
Its unary projection on is , and its projection on is the union of the displayed rows. Their product equals the relation precisely when each row equals that union. This proves both directions, including empty fibers.
For example, let and leave unrestricted, with a full edge . Conditioning on still leaves and correlated. Treating them as independent leaves would invent assignments with . Conversely, in a Boolean equality/disequality star a leaf’s value determines the hub value, so the criterion holds.
The condition is not stable under all original updates. An initially unconstrained star can be centered anywhere. Strengthening to equality destroys the alternative factorization around another leaf . An equivalence that works at one instant need not preserve the subsequent dynamics.
A decorated center repairs the failure
Replace the represented pivot by a center with value
Its feasible values are . The original hub becomes a leaf forced to equal . Every other leaf permits exactly . The original name is observed through the second projection of .
Every original solution has exactly one lifted solution: pair its and values at , leaving all other values unchanged. Conversely, read the second coordinate as and forget the duplicated first coordinate. The forced constraint makes these maps inverse. In the Boolean counterexample there are four center values; for both and equal , while .
The correspondence preserves the original updates:
| Original operation | Operation in the lifted representation |
|---|---|
| Pin | Restrict the first coordinate of |
| Pin | Restrict the second coordinate of |
| Pin another leaf | Restrict its conditional row |
| Strengthen | Restrict the allowed pairs at |
| Strengthen , | Restrict using the first coordinate of |
| Attach a fresh leaf at | Add its row indexed by the first coordinate |
For each operation, lifting after imposing the original constraint gives exactly the relation obtained by imposing its translation after lifting. This is an isomorphism of the corresponding semantic update systems, with the stated observation maps. It concerns updates supported on the original star; a new leaf-to-leaf edge still requires the original graph-validity test.
Repeated pivots keep the same latent hub coordinate. To move from to another leaf , exchange for . The old pivot returns to its leaf row. The domain remains , however many pivots occur. Removing the latent coordinate would restore the correlation failure above.
The added information can be necessary
Write . For with free , any exact star representation centered solely at a decorated requires at least effective center values, provided is a fixed function of the center value and are independent branches conditioned on that value.
With equality tag E and full-relation tag T, the concrete witness E(00,01);T(00,10); has and three accessible variables, .
Indeed, one center value permits a nonempty product . To stay inside equality this product must be the singleton . The same center value also fixes one , so it covers only one of the required pairs . The argument permits multiple extensions per original assignment. Independent auxiliary variables inside the two branches do not help, since projecting them still leaves a product. A second shared separator or a retained edge changes the representation shape and escapes the bound.
The lift attains this minimum. It is an elementary minimum for a specified semantic representation, not a lower bound against native automata.
Where the native construction still stops
Physically normalizing every leaf row after a hub value disappears could require unboundedly many writes. Instead keep raw rows and one authoritative mask
A pin or edge strengthening at changes only , then intersects with its new support. If the current row and current mask are accessible, these are finite table operations for fixed . This annotation avoids a semantic need to broadcast every normalization.
It does not yet provide current access through ordinary names. A leaf storing an old copy of can become stale after a distant leaf or hub update. A pointer to an immutable hub record identifies an old version. If the hub spelling is learned only at the leaf’s delimiter, a second name search begins too late for immediate termination. Comparable name lengths bound its total work but do not supply symbols after the deadline.
Loss certificates also leave this obligation. At most hub values disappear per star, and a contradiction has a witness using at most leaves and source atoms. These elementary finite-domain bounds do not tell an addressed leaf which losses have already occurred elsewhere. A pending event installer cannot postpone the answer when that event removes the last feasible hub value.
For a star with named vertices the fully accessible interface has variables, not one. The logical raw-row representation uses finite table fields, plus names, structural metadata and routing. That is not a bound on an implemented scaffold’s historical storage. Any native construction must charge preparation and all retained versions, obtain its observations through fixed-radius labeled unfoldings, allocate only the permitted per-symbol storage, and output one deterministic acceptance bit on time. Neither the lift nor the small contradiction witness proves those obligations. No communication simulation or all-representations obstruction is asserted here.
Late discovery has a bounded semantic repair: a one-edge component has two possible hubs; on valid star inputs, the next distinct nonloop edge incident to that component settles the choice while the old component has only two vertices. Once a vertex has degree at least two, it is the unique hub. The unresolved step is maintaining arbitrarily many such hubs and their current masks under interleaved updates.
Literature comparison, evidence and next test
Fagin’s 1977 lossless-join theorem, Section 2, Theorem 1 and its multiblock extension, characterizes reconstruction from projections by the ability to mix tuples sharing a separator value. Formula (1) and the change-of-center criterion instantiate that classical condition. They are applications of the established relational method.
Dechter’s 1990 hidden-variable paper, Section 2, explicitly represents a relation by a hidden star center indexing full solution tuples; Section 5 composes independently lifted subrelations. Here the existing star factorization lets us retain only the hub/pivot pair, giving a fixed domain rather than one growing with the number of solutions. The lift and its minimum are concrete specializations of that method. Its semantic representation theorem does not supply a native input schedule.
Freuder’s 1982 backtrack-free theorem, Theorem 1 and Section 4, explains why sufficient consistency and a suitable width-one variable order make tree constraints tractable. That order is an order of choosing solution values after consistency requirements hold, not an arbitrary serial order of incoming records. Its proof therefore supports the semantic control without discharging the current-mask deadline.
The proofs above were independently audited. A reproducible finite check examines all 784 normalized Boolean profiles with three leaves: 2,352 pivot/lift checks and 18,816 pin-commutation checks pass, including the update that destroys ordinary re-centering. These are finite semantic experiments, not formal verification or timing tests of a native recognizer.
Next decisive tests. The precise test for the star approach is a current-answer construction using the raw rows and latent hub coordinate: after interleaved leaf losses, a final pin must combine its row with that hub’s latest mask before the record ends. It must also obtain current structural information without supplied handles. Repeating an ordinary re-centering objection or a stale-copy example cannot settle it. This investigation found no such schedule, so the next fresh construction target is the independent ordinary signed-clause route with checked nested supports and arbitrary literal order. The existing prefix-order theorem remains intact, and the decorated-star route remains available when a concrete current-access mechanism can be tested.