Uniform construction with shared block levels

Working research note, 1 October 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.

The question

The opaque-piece theorem used independently arbitrary words. Recursive representations often correlate their lengths. We test a specific hypothesis: for perfect ternary blocks of a common unknown level, does pointwise bounded construction still imply one rule that never reads that level? The answer is yes in the following constructor model. The result does not yet supply a recursive head-removal algorithm or a theorem for the full catenable deque.

1. Prescribed-length separation

Fix an alphabet Sigma containing distinct a,b. Let F be a finite set of formal words in Sigma and variables X1,…,Xm, with every formal length <=L. Take L>=1 and m>=1. For any prescribed integers Ni>=L+m+3, substitute

Xi = b a^(L+i+1) b^(Ni-L-i-2),       1<=i<=m.       (1)

Each code has exactly Ni letters, and its trailing b exponent is at least one.

Lemma. Substitution (1) is injective on F, while fixing all literal letters.

Proof. Every maximal a-run longer than L is the interior of exactly one variable code. Literal a-runs have length at most L, and each code is guarded by b on both sides. The long run’s length identifies i. Its starting position minus one identifies the start of the code; its prescribed length Ni identifies the end. These intervals are disjoint, including for adjacent variable codes. Replacing each interval by Xi leaves exactly the original literal letters. Thus the evaluated word determines its formal source in F. QED.

This works for equal Ni=N, and for Ni=3^(ell+ci) with fixed nonnegative ci once ell is large enough. Length correlation alone therefore does not prevent a common separating assignment. Restrictions on the contents could prevent it; the lemma requires every tuple with those prescribed lengths to be allowed. The codes are proof witnesses, not runtime encodings or initialization.

2. An explicit indexed constructor model

Fix nonnegative offsets c1,…,cm and d1,…,dp, finite p>=1, and budget K. Types B_n are finite immutable perfect ternary blocks:

letter_c : B_0
G : B_n x B_n x B_n -> B_(n+1).

Flattening concatenates the three child words in order. A B_n word has length 3^n, and every Sigma-word of that length has such a representation. Sharing is allowed, so these are DAGs whose unfoldings have the specified shape. The fixed initial graph consists of one record per letter of Sigma.

A call is supplied opaque roots Xi:B_(ell+ci), for any ell>=0 and every independent choice of their contents at those lengths. Loading the supplied inputs is outside this one-call bound; it must not be confused with a theorem about reachable histories. No access inside Xi, no equality test, no runtime index, and no inspection of ell is allowed. There is one observation branch. Specify each desired output by a formal word Qj and the type B_(ell+dj). The declaration is independent of an implementation.

A candidate allocates <=K fresh G records in acyclic order and returns p roots from the inputs, constants or fresh records. Every allocated record counts, including unused nodes. Each G must have equal child levels. A pointwise witness may depend omnisciently on ell and all input contents, but must meet the actual types at that ell. A uniform rule is one fixed candidate valid at every ell. These definitions do not give the witness an unbounded construction primitive or a semantic equality oracle.

3. Removing accidental small-level typings

Lemma. A candidate with <=K fresh G nodes that is well typed, including all its output requirements, at one ell>K is well typed at every ell>=0.

Proof. A subconstruction using only fixed letters has rank at most K. A subconstruction containing an input root, whenever well typed, has rank ell+u for a nonnegative integer u. At ell>K a fixed-only child cannot have the same rank as an input-dependent child. Thus no G in a valid candidate mixes these two classes. Within the input-dependent class, equalities between ranks are equalities between offsets u, independent of ell. Within the fixed class they are constant equalities. An output of required rank ell+dj cannot be fixed-only at ell>K. Its required equality is again an offset identity. The same assignments therefore type every node and output for all ell>=0. QED.

This lemma uses the exact rank rules above. Negative offsets, additional constructors, arbitrary indexed inequalities and new observations need separate analysis. If the initial graph contained fixed blocks up to height H, the same argument would use ell>H+K instead.

4. Exact fixed-budget uniformization

Theorem. In Section 2’s model the following are equivalent:

1. For every ell>=0 and every admitted input tuple there exists a correctly typed <=K candidate with output words Q1,…,Qp.
2. There exists a <=K candidate whose types are valid for every ell and whose unfolded formal outputs are exactly Q1,…,Qp.
3. One rank-blind uniform rule of this candidate form works on all admitted inputs and levels, preserving old records and versions.

Proof. Enumerate all acyclic candidates and their output-root choices, initially ignoring types. The list is finite. Unfold every output as a formal word; its length is at most 3^K. Include all Qj and choose L bounding these lengths. Choose ell>K with 3^ell>=L+m+3. Lemma 1 supplies a simultaneous separating tuple with |Xi|=3^(ell+ci), realizable by the required blocks. By (1) one candidate works there. Lemma 2 promotes its actual typing to universal typing. Separation promotes agreement in every output coordinate to formal-word identity. This proves (2). Execute that same template to obtain (3); (3) immediately gives (1). QED.

This yields a terminating decision and synthesis procedure for a given K: enumerate the finite candidates, propagate rank expressions and compare formal words. Universal rank equality is coefficient/constant equality between integers and expressions ell+u. This is not a test that assumes the existence of a controller. It characterizes exactly the declared one-call candidates, not all pointer programs. No claim is made that some K must succeed for an arbitrary prescribed Q and output type. If one succeeds, the least such K is an allocation optimum only in this constructor and available-root interface. Resources are <=K fresh arity-three records, zero old-edge traversal, and a fixed number of root assignments. The only preservation guarantees are old heap immutability, output types, and decoded words, not graph identity.

Positive examples: three inputs of rank ell combine in one G to a block of rank ell+1; permuting them also takes one G. One input triples by G(X,X,X) with one fresh node, preserving all versions through repeated tripling from a fixed singleton. These bounds are exact for these examples since no old available root has the required output length at positive ell.

5. What this does not prove about head removal

A stored G(x,y,z):B_(ell+1) can be exposed in one structural step as three B_ell entries. The theorem applies to their independent contents: every triple is admitted. Removing the first entry leaves the pair (y,z), without new block allocation. A bounded buffer of two entries can hold it. It cannot be returned as one perfect block at any rank because 23^ell is not a power of three. Removing the first payload letter* is a different operation: for ell>0, that letter lies inside x and is not exposed by this one step.

This is the exact boundary in the comparison with the previously inspected indexed prefix repair. The source’s Small buffer can contain at least three entries, and Big contains additional buffers and a recursive chain. Its E_n values do not all have length 3^n. Therefore our theorem applies to the perfect three-entry fragment, not the full Small/Big representation. The earlier arbitrary-word certificate remains a sound sufficient proof method there; we have not shown its synthesis completeness. In particular no unproved pop_green or buffer contract has been discharged here.

There are useful negative controls:

• Length constraints alone do not imply closure under residuals: even the two-entry residual above leaves the perfect-block class.
• A fixed short level need not separate finite candidates. On binary singleton X, the opaque roots with words aX and ba pointwise cover target Xa at zero allocation: use aX when X=a and ba when X=b. Neither root works for both. This control is in the preceding concatenation/cache interface, not the ternary-only signature. It shows why the separation argument cannot use an arbitrary fixed level. A visible letter test repairs the selection problem.
• Over a unary alphabet, all words with equal lengths coincide. For example X1X2 and X2X1 cannot be separated. The two-letter premise is essential to the formal-word criterion, not to every possible semantic decision procedure.

6. Status and next decisive question

Uniformization is established theory; see Filiot, Jecker, Loding and Winter, On Equivalence and Uniformisation Problems for Finite Transducers. Their transducer results are not imported into this graph model. Marker coding, finite enumeration and symbolic rank checking are elementary ingredients. The added argument is prescribed-length separation combined with elimination of accidental low-level typings, yielding the exact constructor-model result. Novelty remains unestablished.

For the richer structure, credit Viennot, Wendling, Gueneau and Pottier’s Verified Purely Functional Catenable Real-Time Deques and its underlying Kaplan-Tarjan construction. The source comparison uses the already recorded indexed-prefix contract; this run does not reverify that implementation or claim that our perfect-block theorem covers it.

Written proofs cover unbounded levels and budgets. The checker tests finite marker injectivity, symbolic-vs-concrete typing on bounded candidates, and positive/negative examples. It is not proof-assistant verification.

Next resolve the actual variable-length stored-element domain: does every finite set of distinct frontier expressions admit a simultaneous separating assignment inside the exact Small/Big typing constraints, and does finite candidate typing stabilize at large levels? Either exhibit such assignments and a sound finite type test, or identify a counterexample to that inference. Do not replace the actual E_n domain by perfect blocks. Reassess the six-run window after this next test; another isolated coding lemma without progress on structural closure will not establish a general realization principle.

Observations concern specified output words and typed controller operations, not arbitrary future scaffold contexts or language equivalence. Any compiler application must retain native observations and fixed virtual initialization. A scaffold for L still transfers to a PEG for the reversed language.