Cheap witnesses and uniform residual construction

Working research note, 30 September 2026.

Understand when future computational behavior admits a representation maintained by finite rules with bounded local access and bounded allocation, and what structural obstructions prevent such a representation.

1. The hypothesis being tested

The broad working hypothesis is that useful subclasses of persistent representations admit independently checkable conditions for keeping future states locally constructible. The immediate proposed implication is sharper: if every input has some cheap construction for its next state, does one bounded local rule work on every input? This note proves that implication for independent opaque word pieces and a fixed concatenation specification, and disproves its unrestricted extension to a correlated rope interface.

These are one-operation results about decoded words. A theorem for arbitrary operation sequences still needs an invariant preserved by each operation. Neither result characterizes every representation of a language.

2. An independently specified word interface

Fix a finite alphabet Sigma containing distinct letters a,b, m named input roots X1,…,Xm, and a natural allocation budget K. Records are immutable acyclic E, letter, and binary Cat records, with their usual word semantics. The fixed initial graph contains E and one record for each letter, independently of the input lengths. Each Xi is an opaque root supplied to a call. It may represent any finite word, independently of the other Xi; sharing is allowed. No descent into an Xi is available to this interface. The available old roots are precisely the Xi and the fixed constants. A call may make at most K fresh Cat records, using old roots or earlier fresh records, and return one root. All old records and versions are preserved. Empty words are legal.

Specify the required output by a finite formal word Q in (Sigma union {X1,…,Xm})*. This is supplied independently of a program. For example Q=X1 a X2 asks for those pieces in that order, and Q=X1 X1 asks for a duplicate of the first piece. A root exposed by a prior structural view may serve as Xi; establishing that view is a separate obligation.

A template is a finite acyclic binary construction with at most K fresh Cat records and one chosen return root. Unfolding it gives a formal word P over the same symbols, with E interpreted as empty. There are finitely many templates: topologically order new nodes and choose each child’s index from the finite list of old and earlier new roots. Discarded nodes count; allowing them does not expand the output possibilities beyond this enumeration. Every unfolded P has at most 2^K symbols, since each available leaf has formal length at most one. This bounds formal length, not decoded word length.

The pointwise premise permits an omniscient choice of template for each assignment of words to the Xi. It assumes no effective selector. The uniform conclusion will use one template, with no observation of the Xi at all.

3. Finite separation by a single substitution

Lemma. For any finite collection F of formal words over Sigma and the Xi, there is a substitution of ordinary Sigma-words for Xi that distinguishes every pair of distinct members of F while fixing the letters of Sigma.

Proof. Let L be at least the formal length of every member of F. Substitute Xi by b a^(L+i+1) b, with i starting at one. In an evaluated word, every maximal run of a of length greater than L comes from exactly one Xi. Literal constant runs have length at most L; the b at either end of each code prevents merging with adjacent a-runs. The long run’s length identifies i. Recover Xi by removing its long run and the immediately neighboring b on each side, and replacing that block by Xi. These blocks are disjoint even for adjacent variables, whose codes have two b’s between the long runs. All remaining letters are the original constants. This decoding recovers the formal word uniquely. QED.

The substitution is proof evidence, not preprocessing required at runtime. It is not asserted to be injective on every formal word of unbounded length. For fixed F it is explicitly calculable.

4. A fixed-budget characterization

Theorem. In the interface of Section 2, the following are equivalent:

1. For every tuple of finite input words, some template using at most K fresh records returns the required value Q on that tuple.
2. One template using at most K fresh records has unfolded formal word Q.
3. One uniform rule using at most K fresh records returns Q correctly on every tuple, without descending into any input root.

Proof. List the finite templates and their unfolded formal words Pj. Apply the lemma to F={Q} union {Pj}. By (1), at the separating substitution some Pj evaluates to the same word as Q. Injectivity on F implies Pj=Q as formal words, proving (2). Execute this fixed template to get (3). Finally (3) supplies the witness in (1). QED.

This is an exact characterization of the stated one-call interface, including its budget K. It gives a finite decision and synthesis procedure: enumerate templates, unfold, and compare with Q. No oracle for correctness on infinitely many inputs is assumed by this check. The independent-input hypothesis is checked from how the interface is specified: it explicitly admits every tuple, rather than an invariant correlating their contents. A claimed use inside a richer data structure must prove that abstraction appropriate.

The constructed rule uses at most K allocations, no input descent, two child ports per new record, and a finite number of pointer assignments depending only on K and m. It preserves old graphs and decoded output; it does not preserve input graph shape. The least K passing the finite test is the exact worst-case allocation threshold for this particular interface, not for all implementations of the abstract operation. The search terminates for some K because Q itself can be built by sequential concatenation.

Examples: Q=X1 has threshold zero; Q=X1X1 has threshold one, using sharing; Q=X1X2X1 has threshold two. The last lower bound follows because a one-node template has formal length at most two. For a unary alphabet, target X1X1X2X2 can be realized with two new records by first forming X1X2 and then doubling it: letter counts agree on every assignment. But no two-node template unfolds to formal X1X1X2X2. To achieve formal length four with two nodes, the second must double the first, producing a repetition of a two-symbol block. Three nodes suffice for X1X1X2X2 itself. Thus the exact syntactic characterization requires the two-letter hypothesis. Another failure mode is a correlated domain X1=X2: returning X2 is always correct for target X1 there, although their formal words differ. These controls delimit the lemma, not a claim of impossibility on such domains.

5. Cheap candidates can still be impossible to select locally

Here is a different interface in the same positive rope language, now with letters a,b,c. Fixed initialization consists of E,A,B,C. Put D_s=Cat(A,S) for s in {b,c}, where S is B or C, and define P_0^s=D_s and P_(n+1)^s=Cat(E,P_ns). A supplied input heap contains these records and has named roots (P_n^s,E,A,B,C). Every P has cached head tag a; E and the letter records have their correct cached tags. The required pop answer is head a and a root whose decoded word is s. Both candidate roots B and C are already named and available.

Calls begin in the same control state. They may inspect the complete rooted radius-r view, including labels, cached tags and equality of pointers reached by paths of length at most r. They may use only reached old roots and the fixed constants as old children of fresh records. Addresses, allocation numbers, heap size, inverse edges and the input’s construction history are not observations. At depth r, outgoing edges are unobserved. Fresh graphs may use arbitrary sharing but only the positive E/letter/Cat interpretation. A fixed K bounds new records. Correctness is required for every supplied heap in this family, not only states reached by a chosen history-sensitive controller. The loader constructs the finite input graph from the same fixed constants; its work is outside the one-call resource bound.

Proposition. Every supplied heap has a correct zero-allocation witness, but no fixed r,K deterministic rule realizes pop on all these inputs.

Proof. Pointwise, return B when s=b and C when s=c. Fix r,K and choose n>r. The radius-r views of the two inputs are isomorphic, respecting all named roots, labels, cached tags and observed aliasing. The D_s node lies below the observed boundary. Thus the rule chooses the same construction template on both inputs, with corresponding old pointers.

Every reached old P node contains a. A correct residual, either b or c, cannot use such a node anywhere in its returned expression, because positive concatenation cannot erase its a. Once all these roots are excluded, the same template uses only identical constants in the two heaps and therefore has the same decoded output. It cannot equal b on one input and c on the other. Contradiction. Extra allocation, within any fixed K, cannot repair the missing choice. QED.

This proof covers constructing a fresh answer as well as choosing B or C. It would be incomplete to argue only that the candidate pointers differ: a common old pointer can denote different words in two completions. Positivity is what excludes every such hidden-dependent root from a correct output here.

A visible selector bit repairs this family with zero allocation. It can be maintained while building the wrappers; a controller remembering the initial choice also repairs it. Unbounded descent can find D_s. These are positive controls and explain why the proposition is not a lower bound for all persistent implementations or all reachable-state invariants. The proposed unrestricted pointwise-to-local implication is false in the stated model.

6. What is established, and what remains open

The positive theorem and negative proposition have written unbounded proofs. The accompanying checker enumerates small formal constructions, checks the separating substitution on its finite list, and compares finite paired rope views. It does not verify the proofs in a proof assistant, quantify over all budgets or radii, or establish a compiler refinement.

Uniformization is an established subject: Filiot, Jecker, Loding and Winter, On Equivalence and Uniformisation Problems for Finite Transducers (ICALP 2016, Sections 1-2), distinguish admissible input/output relations from sequentially implementable choices. Their general setting has undecidability and restricted decidability results. We import no decidability theorem from that model into ours. The finite-template enumeration and marker coding here are elementary ingredients; novelty of this particular combination is unestablished. The additional work is the allocation-explicit opaque-piece characterization and a positive-rope counterexample that excludes synthesized answers as well as candidate selection.

The next question is to extend independent pieces to a useful, explicitly specified correlated interface. Candidate invariant: a bounded structural view exposes a word decomposition, and a finite certificate records enough relations among its pieces to make template validity decidable and preserved by updates. No theorem or formal conjecture claiming this for all invariants is asserted. The decisive next test is one concrete correlated class and a proof of preservation, not another general renaming of uniform selection.

These results concern word semantics under the named operations. They make no claim of graph identity, arbitrary future scaffold-context equivalence, a language separation, or general PEG pumping. Any use of the scaffold compiler still requires its full hypotheses and fixed virtual initialization. Transfer of a recognized scaffold language L to a PEG still yields the reverse of L.