Equality SAT: two names, one current value

5 October 2026. Primary-proof review and construction assessment.

Can ordinary equality constraints on disjoint pairs be recognized by a native scaffolding automaton when paired variable names have arbitrarily different lengths? The existing component-local construction handles bounded name-scale span inside each component. Removing that condition remains the target.

The review identifies two separate obligations: discovering the required answer before the name ends, and ensuring that this answer belongs to the current state. Classical weighted search, string comparison and functional persistence address important parts of these obligations, but their guarantees do not compose automatically.

Exact test

Use the existing finite-alphabet record encoding: nonempty literal binary names, equality records and Boolean pins, with explicit delimiters. Initially restrict attention to a charged matching prefix followed by arbitrary pins. This promise isolates the access problem; a full language theorem must also check matching structure and handle the required record order. Invalid input must be rejected.

One deterministic automaton must work at every input length, with fixed degree, radius and finite labels. Initialization is fixed. Name routing, observations of old storage, metadata and allocation are charged to actual encoded length N. There are no supplied handles, free preparation, padding or end-of-input cleanup. Old nodes remain immutable. A short endpoint may be pinned immediately before its arbitrarily long mate, or conversely, with unrelated pairs interleaved.

What the primary proofs supply

Bent, Sleator and Tarjan, Biased Search Trees, §3 and Appendix B, supply weighted-depth bounds and distinguish local amortized operations from globally biased worst-case operations. Their rank-difference accounting telescopes along join/split paths. Insertion also depends on neighboring weights; the linear construction assumes sorted leaves. These are comparison-tree results, not serial-name recognition guarantees.

For our proposed short-owner scheme, assigning a distinct h-bit owner weight 2^(-2h) gives total weight at most one and classical depth O(h). This remains a useful escape from an unweighted Patricia-path argument. It does not establish when those search decisions become available during a longer mate’s arrival.

Amir and coauthors, Managing Unbounded-Length Keys in Comparison-Driven Data Structures with Applications to On-Line Indexing, §§2–3, give a transformation with external-string cost O(T(n)+|y|). Figure 1 and Lemma 1 telescope increases of a best matched prefix; stored-key LCP settles other comparisons. The scan frontier can advance monotonically. Their LCP structure uses range minima, packed representations and RAM table access. Insertion requires a neighbor and adjacent LCP information. The suffix specialization in §5 assumes registered tails and does not directly cover arbitrary names.

Demaine, Langerman and Price, Confluently Persistent Tries for Efficient Version Control, §2, maintain a fixed number of designated fingers using a small connecting structure and deque tendons. This is useful for retaining the first endpoint while reaching the second. The separate balanced variant in §3 has logarithmic modification costs. Neither theorem provides constant-time conversion of an arbitrary historical finger into the corresponding position in the latest version.

The deque dependency leads to Kaplan and Tarjan, Purely Functional, Real-Time Deques with Catenation, §§6.1–6.2. Their strict functional proof uses finite color invariants and compressed preferred paths. Internal removals avoid recursive repair; Lemmas 6.1–6.4 establish the invariants behind Theorem 6.1’s worst-case bound. This supports the classical dependency. Extracting an exact native implementation remains a separate obligation, and granting it would still leave the paired-value problem below.

A search can finish scanning before it finishes deciding

Here is a direct test of sequential comparison search. Take a balanced binary search tree with root r = 0^L10. Its left subtree contains many keys 0^L0z and the key q = 0^L1 as its maximum; its right subtree contains equally many keys 0^L11z. Choose distinct suffixes and balanced subtree shapes so q has logarithmic depth.

On external input q, the root comparison waits for the delimiter. It then enters the left subtree and follows a logarithmic rightmost path. Those comparisons need no additional query characters, but still form dependent decisions after the delimiter. Thus a linear aggregate character-and-comparison budget does not establish a constant final-symbol deadline.

This is a counterexample to the literal sequential schedule, not to every representation or to every biased-tree implementation. Speculation or prepared termination answers could avoid it. It suggests a constructive invariant: after each prefix p, keep the answer required if the next symbol ends the name. A recognizer must also handle prefixes that are not registered names.

There is no inherent requirement to reread an old query character in Figure 1. When a new stored key differs earlier than the best matched prefix, the comparison sign can be inherited from the stored best friend. The native obligation is therefore an accessible stored-key LCP/order certificate, rather than an unavoidable second scan of the query.

A historical endpoint is not its current value

During registration, a fixed set of current fingers could hold the root and both endpoints, conditional on a suitable native implementation. After many pairs have been registered, retaining all those past finger configurations does not keep all pairs current. Updating a pin through one endpoint creates a new representation; the old configuration still describes the old version.

The decisive hostile sequence is small: update pair B, update pair A using a saved context, then query B through its mate. Publishing A must preserve B’s update. A subtree copied as a value is not a live alias that follows future changes. Even perfect string lookup and a constant-time deque do not establish this property.

The next construction should therefore test grouped publication of current pair masks. It must explain how literal-name arrival reaches the current mask while unrelated updates survive. It need not physically refresh every old copy; the existing pending-write construction already demonstrates that current answers can coexist with stale storage.

Consequence for the investigation

The shortest weighted route, monotone string scan and functional finger are useful classical ingredients with identified provenance. This review adds a concrete deadline stress test and an interface synthesis; it establishes no new native SAT inclusion or exclusion.

The next tests are: grouped updates for a charged fixed matching; termination answers during literal-name arrival; composition of those two invariants under alternating pair updates; and restoration of matching validation and unrestricted record order. A failed presentation must be checked against weighted routes, grouped caches and speculative lookup before suggesting an obstruction to all native automata.