Stored-element word richness and the remaining shape obligation

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.

1. The actual source contract

This note follows the stored-element definition at commit 503c5d3ff7f9a20bad1cd7a8f8d7abf4e635d3a0 of VerifiedCatenableDeque. The authors are Jules Viennot, Arthur Wendling, Armael Gueneau and Francois Pottier; their implementation develops Kaplan and Tarjan’s construction. The inspected sources, not a perfect-block replacement, specify:

• Ground(a): E_0.
• Small(s): E_(n+1), where s is a sized deque of 3+q entries of E_n.
• Big(p,c,s): E_(n+1), with prefix/suffix of 3+qp and 3+qs entries of E_n, and a chain c at level n+1.
• Empty is a chain at any level, kind and permitted color indices, with empty arity. Its flattened word is empty.

These statements come from theory/Cadeque/Types.v, constructors Ground, Small, Big and Empty. theory/Cadeque/Models.v gives the flattening equations: Ground yields one letter; Small flattens its buffer; Big concatenates prefix, child chain and suffix. No label test is part of these types.

We import only the buffer representation laws from theory/Deque/Deque.v: empty represents [], push prepends an entry while increasing the size index by one, and correct_deque_cmseq identifies mapped flattening with concatenation of entry meanings. Repeated push therefore represents any finite list of entries. This is an existence construction, not a claim that an arbitrarily large buffer is built in bounded time. The source contains proof-carrying definitions for these laws. We inspected their statements and pinned the files; we did not rerun the Rocq development.

2. Every sufficiently long word is available at a positive level

Let Sigma be a finite alphabet and interpret Ground payloads as its letters. Write W_n for the set of flattened words of all valid E_n values.

Proposition. For every n>=1, every Sigma-word of length at least 3^n belongs to W_n. Such a witness can use only Ground and Small stored elements.

Proof. For n=1, store the word’s N>=3 letters as Ground entries in a buffer and wrap it in Small. For n>1, split a word of length N>=3^n into three consecutive parts of lengths 3^(n-1), 3^(n-1), and N-2*3^(n-1). Each part has length at least 3^(n-1). By induction each is the flattening of an E_(n-1) value. Put those three entries in a buffer and apply Small. The imported buffer laws and Small’s flattening equation give exactly the requested word. QED.

This is a sufficient richness statement, not an assertion that the source forces length exactly 3^n, nor a complete characterization of all source shape constraints. Witness construction may be large; it occurs only in the proof of existence of admitted inputs, outside any one-call resource budget. A fixed initial alphabet of Ground records suffices; repeated equal letters may share records. No history-dependent initialization is assumed.

For n>=1 and a fixed buffer occupancy k, every word of length at least k3^n can likewise be split into k E_n entries. Thus even fixing Small’s occupancy does not remove richness above level one. At level zero, entries are individual letters and fixed occupancy instead fixes length. For a Big case whose child is permitted to be Empty and whose prefix/suffix each have three E_n entries, every word of length at least 63^n is realizable when n>=1. These controls respect their stated branch restrictions; they do not establish richness for every nonempty-chain or color-constrained frontier.

3. Separation and finite semantic selection

Assume Sigma contains distinct letters a,b. Fix m independent opaque roots Xi:E_(ni), with each ni>=1, and admit all tuples of those types. Levels may be equal or different. Aliasing is allowed but not required or observable. There must be no additional content relation or forced sharing between these roots. The observation is the decoded word under a specified operation, not an arbitrary future graph context.

Corollary (finite separation at fixed levels). For every finite set F of distinct formal words over Sigma and X1,…,Xm, one admitted tuple simultaneously distinguishes all members of F.

Proof. Let L>=1 bound their formal lengths. Choose Ni>=max(3^ni,L+m+3). The preceding prescribed-length lemma substitutes Xi=b a^(L+i+1) b^(Ni-L-i-2), using i=1,…,m. Each code has length Ni, so the proposition realizes it inside E_(ni). Long a-runs identify i; known code lengths identify boundaries. Hence the same decoding separates F. Independent values can be built separately; possible aliases in other inputs do not remove these legal witnesses. QED.

Now supply a finite list of candidate pointer-construction plans. Each plan must already have an independently checked shape/type certificate for all admitted inputs, a fixed local view, and stated bounds <=K fresh records and radius r. It must preserve old records. Its decoded output tuple is obtained from finite constructor word equations, so every output has a formal-word normal form. The required tuple Q is specified in the same language. No candidate may invoke an unresolved primitive without retaining its contract as an explicit premise. For an opaque-root case r=0.

Theorem (semantic selection from certified plans). If every admitted input tuple has some correct candidate in this finite list, then one listed candidate has formal output tuple Q and is correct on every admitted tuple. Conversely such a candidate is a pointwise witness. Comparing formal words therefore decides semantic realizability within this list and retains that candidate’s stated resources and structural guarantees.

Proof. Include all candidate output coordinates and target coordinates in F and apply the corollary. A pointwise witness at its separating tuple must agree formally in every coordinate. Formal equality then gives semantic agreement on all inputs. Its independent type certificate supplies the shape conclusion; that conclusion does not follow from word separation. QED.

This does not assume semantic correctness of a plan, only its syntactically specified behavior and separately checked shape/resource obligations. It is complete for the supplied certified list, not a proof that the list contains every bounded pointer program. It gives no general type-inference algorithm. It concerns supplied states, not automatically every reachable invariant or every finite operation history. Iteration additionally requires coverage of successive views and preservation of the declared invariant from a fixed valid initialization. The earlier typed-list result supplies those obligations in its own model; this note does not supply them for the full deque.

4. Two precise failures of stronger transfers

Rank-stabilization proof does not transfer as stated. The perfect-block proof bounded the rank of every constant-only construction by the initial height plus its allocations. In the actual source, the same Empty chain has type at any level, and its sequence is always empty. Thus constant-only does not imply bounded level for all source sorts. This refutes that proof premise, not the possibility of a revised polymorphic type checker or a uniform rule. Any extension must track chain arity, colors, kind and polymorphic emptiness separately from the ranks of nonempty stored elements.

Content restrictions can destroy separation despite unlimited lengths. If the admitted domain requires X=Y, formal X and Y agree on every input, however long they are. Returning Y for target X is semantically valid there. Such a domain cannot be checked by literal formal equality in independent variables without first recording its equations. The source’s all-tuples type domain supplies independence; a particular runtime view may not. Empty-only frontiers similarly cannot be treated as long arbitrary words.

Removing the first E_n entry from a buffer and removing the first payload letter are still different operations. Richness proves neither cheap access to that payload nor preservation of the next local view. The construction of long marker witnesses must never be counted as a bounded runtime algorithm.

5. What the accumulated result does and does not give

There is now a reusable restricted principle: a finite menu of bounded plans can be selected by symbolic word comparison when the admitted input domain can simultaneously distinguish their expressions. The independent-word, explicit-cache, typed-list and shared-level results identify concrete domains where this works. The actual stored-element domain also has the needed word richness at positive levels.

The missing ingredient for a general persistent-realization theorem is a complete, independently checkable account of the structural plans and their closure under subsequent operations. Calling this a general characterization would be premature. The current result explains a semantic part of synthesis; it does not synthesize an adequate invariant or a representation.

On Equivalence and Uniformisation Problems for Finite Transducers is the established uniformization comparison; its theorems are not imported here. The stored constructors and buffer laws belong to the deque authors. The new argument here is the explicit realization of arbitrary long words inside those types and its consequence for finite semantic selection. The induction, marker method and finite search are elementary. Novelty remains unestablished; this is working mathematics with a written unbounded proof.

The checker records exact source hashes, tests the constructive Small-only model on finite words, tests finite separation and the two negative controls. It neither executes the Rocq implementation nor proves the unbounded claims. No machine-checked status is transferred from the authors’ development to this new argument.

The next practical test should be a finite indexed type checker that handles polymorphic Empty alongside nonempty stored elements, and certifies one closed recursive interface. Further marker variants alone will not close the identified gap. A successful result must state initialization, view coverage, every allocation, and how the residual remains admitted.

Nothing here separates languages, preserves physical graph identity, or excludes other pumping methods. Scaffold compilation retains native-observation and virtual-initialization obligations. Scaffold-to-PEG transfer reverses L.