A fringe simulation for catenable concatenation

30 September 2026. Written compositional proof for the scalar-free hand-written catenable source, with a finite free-monoid and source-alignment audit. This note proves exact abstract-sequence behavior for empty, push, inject, and concat, conditional only on the stated buffer interface. It does not yet prove pop or the internal non-catenable deque that supplies that interface.

Contents

1. Model and quantifiers

Fix an arbitrary payload set $A$ . The semantic theorem below does not need $A$ to be finite; the later bounded-record compilation does. Consider every well-typed finite runtime value generated by the constructor families in lib/cadeque_core.ml, including values retained on different persistent branches.

For each element type $X$ , assume a purely functional buffer implementation with a contents map

$\beta_X:B(X)\longrightarrow X^* .$

The required buffer contract is exact sequence behavior for empty, push, inject, pop, eject, their fixed two-element composites, single, pair, and the two classifiers has7p and has7s. For example,

$\beta(\mathsf{push}(x,p))=x\beta(p),\qquad \beta(\mathsf{inject}(p,x))=\beta(p)x,$

and has7s either returns all elements in a vector of length at most six or splits a word of length at least seven into its prefix and last two elements. The front version is symmetric. Run 20 proves that the four integer tests in the hand-written source can be replaced by persistent structural probes without changing these classifications.

This contract is independently checkable. It is a finite list of equations for the named buffer operations; it does not assume catenable concatenation.

2. One mutually recursive fringe

The efficient OCaml uses type nesting where the Rocq development uses an explicit natural-number level. Make that correspondence explicit. Put $E_0=A$ , and let $E_{n+1}$ be the type of stored values over $E_n$ . Define

$\mu_0(x)=[x],\qquad \mu_{n+1}(\mathsf{Small}(p))=\widehat\mu_n(p),$

$\mu_{n+1}(\mathsf{Big}(p,c,s)) =\widehat\mu_n(p)\,C_{n+1}(c)\,\widehat\mu_n(s), \tag{1}$

where $\widehat\mu$ maps a buffer elementwise and concatenates the results. The remaining constructor families have the following accumulator semantics:

$\begin{array}{ll} N(\mathsf{Only\_end}(p),u)&=\widehat\mu(p),\\ N(\mathsf{Only}(_,p,s),u)&=\widehat\mu(p)u\widehat\mu(s),\\ N(\mathsf{Left}(_,p,(y,z)),u)&=\widehat\mu(p)u\mu(y)\mu(z),\\ N(\mathsf{Right}(_,(x,y),s),u)&=\mu(x)\mu(y)u\widehat\mu(s). \end{array} \tag{2}$

$\begin{array}{ll} H(\mathsf{Hole},u)&=u,\\ H(\mathsf{Single\_child}(h,b),u)&=N(h,H(b,u)),\\ H(\mathsf{Pair\_yellow}(h,b,r),u)&=N(h,H(b,u)C(r)),\\ H(\mathsf{Pair\_orange}(h,l,b),u)&=N(h,C(l)H(b,u)),\\ Q(\mathsf{Packet}(b,t),u)&=H(b,N(t,u)),\\ C(\mathsf{Empty})&=\epsilon,\\ C(\mathsf{Single}(_,q,r))&=Q(q,C(r)),\\ C(\mathsf{Pair}(l,r))&=C(l)C(r). \end{array} \tag{3}$

The fringe of Triple(_,h,c) is $N(h,C(c))$ , and the fringe of T c or S c is $C(c)$ . Equations (1)-(3) are exactly the model functions in theory/Cadeque/Models.v, after replacing Rocq’s Ground x at level zero by the OCaml payload $x$ . They are definitions, not an appeal to the correctness theorem.

These definitions are well founded on finite constructor values. Colors, phantom arities, and regularity witnesses constrain which cases are well-typed but contribute no payload symbols.

3. Local helper contracts

The following contracts hold for the modified OCaml source, assuming the buffer equations above.

single_chain, push_ne_chain, and inject_ne_chain respectively produce fringe $\mu(x)$ , prepend $\mu(x)$ , and append $\mu(x)$ .
triple_of_chain and chain_of_triple preserve fringe.
left_of_only and right_of_only preserve fringe whether they return a short vector or a triple.
stored_of_right(sl,tr) returns $(d,(y,z))$ with $\mu(d)\mu(y)\mu(z)=\widehat\mu(sl)T(tr)$ . The left version is symmetric.
left_of_pair(tl,tr) and right_of_pair(tl,tr) both have fringe $T(tl)T(tr)$ .
make_left(c) and make_right(c) return either a vector or a triple whose fringe is $C(c)$ .

Here is the only apparently nonlocal case. Suppose Only(_,p,s),child is converted to a left triple. Write $\widehat\mu(s)=S'yz$ . The source appends Small s' to the child and stores $y,z$ at the node boundary. Its new fringe is

$\widehat\mu(p)C(child)\widehat\mu(s')\mu(y)\mu(z),$

which is the old fringe. Every other clause is the same kind of reassociation in the free monoid $A^*$ . The pair cases use contract 4 once. No commutativity, cancellation, or length argument is used.

Proof of the contracts

Proceed by structural induction following the source case tree. Buffer calls are replaced by their contract equations. Equations (2)-(3) reduce the triple_of_chain and chain_of_triple clauses definitionally. In the short cases, has7p or has7s supplies the complete vector. In the long cases, the returned split supplies exactly the two symbols moved across the node boundary.

For stored_of_right, write the right triple as $abCS$ and split $S=S'yz$ . The returned stored value and pair flatten to $slabCS'yz=sl\,T(tr)$ . The left equation is its mirror. Substituting these identities into the two clauses of each pair helper proves contract 5. make_left and make_right then follow from the three chain constructors. $\square$

The companion Rocq file theory/Cadeque/Core.v states these same contracts as dependent result types. Its executable clauses and the hand-written OCaml clauses have the same constructors and helper calls on this path. This is useful corroboration, but the proof above is independent: it uses the explicit fringe equations and the OCaml case tree rather than importing the Rocq concat_correct theorem without an erasure map.

4. Public-operation theorem

Initialization is T Empty. Old runtime values are immutable and remain valid. All outputs below are well-typed regular catenable values by the GADT result types.

Theorem 1 (fringe correctness through concatenation). For every payload set $A$ , every two well-typed regular source values $d_1,d_2$ , and every payload $x$ , the modified hand-written source satisfies

$\begin{aligned} F(\mathsf{empty})&=\epsilon,\\ F(\mathsf{push}(x,d_1))&=[x]F(d_1),\\ F(\mathsf{inject}(d_1,x))&=F(d_1)[x],\\ F(\mathsf{concat}(d_1,d_2))&=F(d_1)F(d_2). \end{aligned} \tag{4}$

The quantifier includes every branch from every retained older version.

Proof

The first three equations follow from the empty-chain case and helper contract 1. For concatenation, apply contract 6.

If the left call returns a vector $v$ , its fringe is $F(d_1)$ . vector_fold_right push v d2 therefore has fringe $F(d_1)F(d_2)$ .
If the left call succeeds and the right call returns a vector $v$ , that vector has fringe $F(d_2)$ . vector_fold_left inject d1 v again has the required fringe.
If both calls return triples, chain_of_triple preserves their fringes, and the Pair constructor concatenates them by (3).

The vector constructors have fixed maximum length six, so the fold argument is a finite case split rather than an induction over an unbounded list. $\square$

This is exact language-level sequence semantics for the listed operations, not merely agreement on one parity observation. It still does not preserve a particular stored graph, pointer identity, or behavior under arbitrary future scaffold contexts.

5. What remains and the decisive restriction

Theorem 1 closes the catenable layer above a buffer contract. It does not make the filtering controller unconditional, because the required fourth public operation is pop. The first unproved source boundary is now precise:

$\mathsf{pop\_green}(c)=(x,s) \Longrightarrow C(c)=[x]F(s),\qquad C(\mathsf{ensure\_green}(s))=F(s). \tag{5}$

The pop_green and ensure_green paths enter the full red-node repair cascade and, through every buffer operation, the hand-written Deque_core. The current fringe handles all catenable constructor families, but it treats each buffer by its abstract contents. It therefore cannot prove (5) until the non-catenable runtime constructors receive their own model and repair invariant.

That missing strengthening is not another length or allocation problem. It is a semantic certificate for the restricted non-catenable presentation: deque_cmseq must be defined for Ending, Chain, packets, and decomposition results, and every reachable repair helper must preserve it. The verified Rocq development already supplies the target equations; the new work would be an explicit source relation or an independently checked finite algebraic certificate.

After the three-run narrowed allowance, continuing to transcribe helper clauses would be poor leverage. The useful principle exposed by this audit is to separate two certificates:

a locality certificate, showing finite branching, bounded probes, and bounded allocation; and
a fringe certificate, assigning free-monoid meanings to constructors and proving every transition equation.

The next target should formalize a restricted class of finite acyclic persistent algebraic programs for which those two certificates are sufficient and mechanically checkable. The scalar-free catenable source is then a stress-test, not the definition of the theory. Equation (5) is the first remaining instance.

This is a redirect within the same question, not a negative result about all catenable sequences or all persistent filtering representations.

6. Resources, verification, and contribution boundary

Combining Theorem 1 with the Run 20 source certificate gives the same conservative construction bounds for these operations:

$q_C\leq8,\qquad r_C<2^{100000},\qquad A_C<2^{100000}.$

These are bounds for one presentation, not optima. For a finite payload alphabet the reviewed simultaneous-record compiler can encode each finite transition plan, preserving the listed word semantics on the same operation traces. It does not promise graph isomorphism.

The companion checker normalizes the local equations in a free monoid and audits the pinned source hashes, helper names, and Rocq contract statements. It checks negative controls that reverse a short vector and place a moved pair on the wrong side. This finite/static audit does not prove Theorem 1, the buffer contract, equation (5), or the source-to-record compiler.

Viennot, Wendling, Gueneau, and Pottier’s constructor design, model functions, and Rocq helper theorems are imported. The additional argument is the explicit level-erasure/fringe relation for the hand-written concat path, its compositional proof after threshold erasure, and the separation of locality from fringe certificates. Novelty is unestablished.

Primary source: