Finding the middle without being told where it is

The string 0110 is an even palindrome: its second half reverses its first. So are 00, 1001, and the empty string. A grammar can describe all such words by repeatedly wrapping the same symbol around a shorter palindrome. Recognizing the words while input arrives is a different task. Before the input ends, the recognizer is never told which position will be the middle.

A stack solves a related problem with a marked middle. Read the first half onto the stack, then compare incoming symbols with popped symbols after the marker. Removing the marker removes the moment at which that algorithm knows to switch roles. Keeping all plausible centers or walking back along many suffix links can take more work than one input step allows.

This article develops a direct persistent-graph construction. Its state describes the longest even-palindromic suffix of the input so far and the context to its left. A 10 September 2026 source-level audit now supplies an explicit fixed-layout resource certificate. A whole-client symbolic normalization theorem now closes the source-to-plan gap isolated by the end-to-end audit. The remaining weakest premise is the manual old-address certificate. Here is a short trace:

At each step the complete prefix is an even palindrome exactly when the remaining prefix is empty. The mathematical challenge is to update this description with uniformly bounded local work, including at steps where the longest suffix changes dramatically.

The construction stores receipts: pointers to records whose correctness has already been established. A receipt is more than a length or an endpoint. It identifies the particular palindrome record needed by a future transition. A persistent sequence of these receipts can be shared by several contexts. The key recurrence proves that the shared cells carry the same receipts, even when the surrounding palindrome contexts differ. Equality of the underlying strings alone would not justify reusing the pointers.

There is a second challenge. A newly created palindrome record points to its new receipt sequence, and the last receipt in that sequence points back to the record. Both objects belong to the same input step. Ordinary sequential allocation cannot make both pointers point to already allocated objects.

The article resolves that issue by packing a fixed-size batch of logical records into one physical scaffold node. A finite slot number says which logical record is meant. An edge between two records in the same batch becomes a physical self-loop together with a slot tag. The physical graph obeys the scaffold rules even when the decoded batch contains a cycle. This compiler is proved separately from the palindrome recurrence, so its role can be inspected directly.

To keep the receipt-sequence operations bounded in the worst case, the construction starts from Kaplan–Tarjan’s purely functional catenable-sequence result. Section 11 separates that stated worst-case theorem from the stronger FPRD requirements: finite branching and allocation, bounded old-address access, and opacity of the complete stored cell. A later length-free source variant, constructor proof, allocation and exposure audits, fixed client layout, and max-plus composition now supply that stronger interface in an explicit abstract source-record model. This is not a literal OCaml runtime theorem or a correspondence proof with the separate Rocq implementation.

The persistent-stacks article takes a different route through classical real-time palindrome machines. Here the point is to expose how the palindrome information itself can be maintained in a scaffold. The running trace, the failed simpler representations, the receipt recurrence, and the batch compiler explain successive parts of that construction.

I Why this proof looks different

1 The question and the direct route

Guiding question.  Can a device that adds only one bounded-local graph node per input letter recognize a language whose obvious description compares two unbounded halves?

1.1 The language and the conjecture

Write \(w^R\) for the word \(w\) read backwards and \(\mathsf{EPAL}_2\) for the set of binary words of the form \(ww^R\): the even-length palindromes \(\epsilon\), \(00\), \(11\), \(0110\), \(1001\), \(001100\), and so on. As a generative object the language is as simple as they come: three rewriting rules produce it (Section 2.2). Loff, Moreira, and Reis (hereafter LMR) studied how much computational power the recognition-based grammars called parsing expression grammars have, and found both surprising positive examples and a natural negative conjecture [7, Conjecture 7, p. 10]:

The language of even-length palindromes has no PEG, i.e. \(P=\{ww^r\mid w\in\{0,1\}^*\}\notin\mathsf{PEG}\).

The intuition behind the conjecture is that a PEG cannot “find the middle” of its input. The conjecture is false. An earlier paper of this project [5] refuted it by compiling strict real-time multitape Turing machines into LMR’s scaffolding automata and invoking the classical theorem that palindromes are recognizable in real time by such a machine [9, 4]. That route proves membership but explains nothing about what a scaffold must remember to compare two halves.

1.2 What this paper does

This paper develops a second, direct route. The reader needs no Turing machine and no palindrome theorem: only words, finite graphs, and one inherited data structure. A later source-level certificate makes the data-structure interface explicit. Theorem 11.3 closes the source-to-plan gap isolated by the end-to-end audit. Figure 1 shows the two routes.

The lower route produces two separable results.

• The direct application. The receipt construction gives a finite scaffolding automaton for \(\mathsf{EPAL}_2\) and then an ordinary PEG by LMR’s theorem. The source-resource constants belong to the abstract immutable-record model; their old-address proof remains manual rather than machine checked.

• The reusable tool. Any one-step update that reads a bounded amount of old persistent structure and creates a bounded finite graph of fresh records—even a graph with cycles among the fresh records—can be performed by one scaffold node (Theorem 10.2). The palindrome construction is exactly what forces the cyclic case.

1.3 How to read this paper

Section 2 defines everything the argument uses: words, context-free grammars, PEGs, scaffolding automata, persistence, and the mutable palindrome index that the scaffold cannot have. A reader who knows these objects may skim it, but should read Definition 2.6 and Theorem 2.7, whose exact form matters. Section 3 fixes three layers of description that the proof keeps separate. Section 4 follows one input word by hand. Part II proves the combinatorics of the longest even-palindromic suffix and turns it into operations on persistent ropes. Part III defines the compiler, proves it, and assembles the automaton. Part IV says what was proved, what is inherited, and what remains open.

Proofs state their strategy before their details. Every example says which of its features generalize. The compiler, conditional staging theorem, whole-client normalization theorem, and direct application are stated in this paper. Its external inputs are LMR’s Theorem 16 (sufficient direction) and Kaplan–Tarjan’s Theorem 5.1; the stronger finite-record interface used here is supplied by the later source-level certificate, not attributed to Kaplan–Tarjan.

2 Background: words, grammars, parsing expression grammars, and scaffolds

2.1 Words, languages, palindromes

An alphabet \(\Sigma\) is a finite set of letters; in this paper \(\Sigma=\{0,1\}\) unless stated otherwise. A word is a finite sequence of letters, \(\epsilon\) is the empty word, \(\Sigma^*\) is the set of all words, and \(|w|\) is the length of \(w\). Juxtaposition \(uv\) is concatenation. A language is any subset of \(\Sigma^*\). The reversal of \(w=c_1c_2\cdots c_n\) is \(w^R=c_n\cdots c_2c_1\); reversal of a language is \(L^R=\{w^R:w\in L\}\).

A word \(u\) is a suffix of \(w\) if \(w=xu\) for some \(x\), and a proper suffix if moreover \(u\ne w\); prefixes are defined symmetrically. The empty word is a proper suffix of every nonempty word. A palindrome is a word \(w\) with \(w=w^R\); an even palindrome is a palindrome of even length, equivalently a word of the form \(ww^R\). The empty word is an even palindrome. Thus \[\mathsf{EPAL}_2=\{ww^R:w\in\{0,1\}^*\}=\{\text{even palindromes over }\{0,1\}\},\] and \(\mathsf{EPAL}_2^R=\mathsf{EPAL}_2\) because reversing \(ww^R\) gives \(ww^R\) again.

When a palindrome \(P\) occurs as a suffix of a word \(S=CP\), the letter of \(C\) immediately to the left of that occurrence will matter constantly; we say the occurrence is preceded by that letter. The empty suffix of a nonempty word is preceded by the word’s last letter; the empty suffix of \(\epsilon\) is preceded by no letter.

2.2 Context-free grammars: the generative reading

A context-free grammar consists of a finite set of terminal symbols (our alphabet), a disjoint finite set of non-terminal symbols, a start non-terminal, and finitely many rewriting rules \(A\to\varphi\) in which \(A\) is one non-terminal and \(\varphi\) is a word over terminals and non-terminals [1, pp. 120–122]. A derivation starts from the start symbol and repeatedly replaces one occurrence of a non-terminal by the right-hand side of one of its rules, in any order, until only terminals remain. The language generated by the grammar is the set of terminal words obtained by some derivation.

2.3 Parsing expression grammars: the recognition reading

Parsing expression grammars, introduced by Ford [3, §3], use rule shapes that look like context-free rules but give them an operational meaning. We follow the formalization of LMR [7, Definitions 1–4], which is the one their theorem is stated for.

The meaning of an expression is a recognition procedure \(\operatorname{Rec}_G(e,x)\) that reads an input word \(x\) from the left and either fails or succeeds consuming a prefix \(x'\) of \(x\) [7, Definition 3 and Algorithm 1]:

• \(\varepsilon\) succeeds consuming nothing; \(\mathsf{FAIL}\) fails; the terminal \(a\) succeeds consuming \(a\) if \(x\) begins with \(a\), and fails otherwise.

• Sequence \(e_1e_2\): run \(e_1\) on \(x\); if it succeeds consuming \(y_1\), run \(e_2\) on the remainder; succeed consuming \(y_1y_2\) if both succeed, otherwise fail.

• Ordered choice \(e_1/e_2\): run \(e_1\); if it succeeds, that is the answer; only if it fails is \(e_2\) run on the same input.

• Predicates: \(!e\) succeeds consuming nothing if \(e\) fails, and fails if \(e\) succeeds; \(\&e\) succeeds consuming nothing if \(e\) succeeds.

• A non-terminal \(A\) runs \(R(A)\).

The procedure is deterministic: at every point exactly one thing happens. It may loop forever (for example \(A\leftarrow A\)); a grammar is total if it never does. Following LMR, a total grammar recognizes the language \[L(G)=\{x\in\Sigma^*:\operatorname{Rec}_G(S,x)=x\},\] the words on which the start expression succeeds consuming the whole input, and \(\mathsf{PEG}\) is the class of languages recognized by total PEGs [7, Definition 4]. We call this complete-match recognition; it is the ordinary notion, not a variant.

2.4 Why comparing the two classes is not a syntactic matter

Example 2.1 shows \(\mathsf{EPAL}_2\) is context-free by three rules. One cannot read those rules as a PEG and hope: the choice \(S\leftarrow 0S0/1S1/\varepsilon\) commits to \(0S0\) whenever the input begins with \(0\), and then must find the matching closing \(0\) at a position it has no way to locate—a PEG consumes left to right and cannot “count to the middle”. That is the content of LMR’s conjecture. Conversely, PEGs recognize languages, such as \(\{a^nb^nc^n\}\) [7, p. 3], that no context-free grammar generates. Neither class contains the other by any syntactic argument; the comparison must go through a machine model. LMR supplied that model.

2.5 Scaffolding automata

LMR’s machine builds a permanent graph. We give their definition [7, Definitions 10–15, pp. 14–16] in words first, then precisely, then with a picture.

In words: the machine reads one input letter at a time. Its memory is a growing directed graph whose nodes are numbered \(0,1,2,\ldots\) in the order of creation; node \(0\) is an unlabelled base, and every later node carries a label from a finite working alphabet and a fixed number \(d\) of ports (outgoing edges), each pointing to an older node, to the node itself, or to nothing. Old nodes are never changed. At each letter the machine looks only at the nodes within a fixed distance \(k\) of the most recently created node (the top), following ports; based on what it sees, on the letter, and on its finite control state, it creates one new node, chooses its label, and chooses where its ports point—necessarily among the nodes it just looked at, or the new node itself. After the last letter it accepts or rejects by its control state.

Three points deserve emphasis. The descriptor \(\epsilon\) (the empty port word) names the old top itself. The descriptor \(\mathsf{SELF}\) lets a new node point to itself; it is part of LMR’s model, not an extension. And the machine cannot test whether two observed nodes are the same node: it sees a tree.

2.6 The exact correspondence with PEGs, and why reversal appears

We use only the second sentence (the “sufficient direction”, whose proof in LMR begins on p. 23). The reversal is not an accident of notation. A scaffolding automaton consumes the input left to right and commits at each letter; LMR’s grammar for the reverse language re-enacts the automaton’s run from the grammar’s point of view, which reads the other way. For a language equal to its own reversal, such as \(\mathsf{EPAL}_2\), the distinction disappears, and this is exactly why Corollary 12.3 mentions reversal invariance. The paper does not use the other direction of the theorem and makes no statement about the class \(\mathsf{SA}\) as a whole.

2.7 Persistent data structures

A data structure is ephemeral if an update destroys the old version, and persistent if every old version remains available after updates; it is fully persistent if old versions can also be updated [2, §1]. The scaffold of Definition 2.5 is persistent by construction: nothing is ever overwritten. The data structures of this paper are persistent in the strongest sense, which Kaplan and Tarjan call purely functional: built only from the three LISP primitives \(\mathsf{cons}\) (make a pair), \(\mathsf{car}\) and \(\mathsf{cdr}\) (read its two components), with no mutation and no memoization [6, p. 578, footnote 1].

The key consequence is structural sharing. If a list is represented as a chain of pairs, then \(\mathsf{cons}(x,\ell)\) creates one new pair pointing at the old chain \(\ell\); the old list and the new list share everything but that pair, and neither can tell (Figure 3). A structure that needs to “copy” an unbounded old part can instead point to it.

A steque (stack-ended queue) is a sequence supporting push (add at the front), pop (remove the front element), and inject (add at the rear); a catenable steque also supports concatenating two steques [6, pp. 578–579]. A data structure is real-time when every operation takes worst-case constant time—a constant number of primitive steps regardless of the sequence’s length [6, p. 579]. (The reader should keep this data-structure sense of “real-time” apart from the machine sense used in the earlier transfer paper, where a real-time Turing machine is one that performs a bounded number of steps per input letter.) Section 11 quotes the theorem of Kaplan and Tarjan that supplies a purely functional real-time catenable steque.

2.8 The mutable palindrome index, and why a scaffold cannot have it

Algorithms that maintain all palindromes of a growing word use a palindromic tree (the eertree of Rubinchik and Shur [8, §2.2]): one node per distinct palindrome, a suffix link from each node to its longest proper palindromic suffix, and, added whenever it is first discovered, an edge labelled \(c\) from the node of \(P\) to the node of \(cPc\). Discovering that edge means walking suffix links from the current node until a node is found whose occurrence is preceded by \(c\); the walk can be long, but its cost is amortized and the edge is then stored at the old node, so it is never needed again.

A scaffold can do neither thing. It cannot walk an unbounded chain within one step (it sees distance \(k\)), and it cannot add an edge to an old node. The present paper shows what must be stored instead: not a pointer from a palindrome type to a type, but a pointer carried by each occurrence to the particular historical record that the next step will need. Section 7 records, with small counterexamples, why each cheaper idea fails.

3 A reader’s map

3.1 The viewpoint behind the paper

This paper builds directly on LMR’s framework. Their scaffolding automata turn the history generated by a finite transition table into an explicit persistent graph, and their correspondence turns acceptance of that graph process into a PEG language. Our question is therefore not only whether \(\mathsf{EPAL}_2\) has some PEG, but which internal recognition dynamic makes palindrome comparison visible to that correspondence.

Finitely Presented Recognition Dynamics, abbreviated FPRD, is the research viewpoint used in this work: a finite grammar or machine description is treated as a presentation that generates an internal recognition dynamic, and the accepted language is treated as one observation of that dynamic. FPRD Lab is the AI-assisted research project in which the present arguments were developed; nothing in this paper requires trust in that project, its tools, or its records, and Section 14 states plainly what was checked by whom. The viewpoint has one concrete role in the proofs: we keep the word-level recurrence (what is true of the input), the record-level representation (what a persistent program stores), and the scaffold-level encoding (what the machine physically appends) as three separate layers, and we prove each implication between them rather than identifying them.

3.2 Three representations of one state

The distinction between type and occurrence is especially important. The word \(0110\), for example, is one palindrome type. During an online run it may occur at many positions and under different surrounding contexts. A conventional mutable index attaches transitions to the shared type. An immutable scaffold cannot retroactively add a pointer to an old record, so it transports receipts associated with the occurrence that made a transition available. One consequence should be said at once, because it resolves an apparent tension later: the content stored in a record (its suffix link, its bridge letter, its ropes) is a function of the palindrome type alone—the receipt traces of Section 8 are defined from words—so any record of the right type would do semantically; what depends on the occurrence is only which physical record is reachable within the machine’s fixed distance.

Definitions are given at the first point where they carry proof weight, and Appendix A collects the notation. In diagrams a solid arrow is a logical pointer or implication; a dashed arrow is a decoded or represented relationship rather than an additional heap edge.

4 A running palindrome trace

Before introducing the record machinery, we follow one word. For every input prefix \(S\), let \(P=P(S)\) be its longest even-palindromic suffix (it exists, since \(\epsilon\) is one), write \(S=CP\), and let \(\ell=C^R\). The pair \((P,\ell)\) determines acceptance: \(\ell=\epsilon\) exactly when the entire prefix is an even palindrome. It also contains enough word-level information to determine the next pair.

Table 1 gives the complete trace for \(00011001\). The empty word is displayed as \(\epsilon\). “External” means that the new letter matches the first letter of the stored context, so it wraps the entire current palindrome. “Internal” means that the full \(P\) cannot be wrapped, but a proper even-palindromic suffix of \(P\) can. “Reset” means that no even suffix at all—not even the empty one—can be wrapped, so the new longest even suffix is empty. Recall that the empty suffix of a nonempty word counts as preceded by the word’s last letter; that is why row 3 is an internal update and not a reset.

Two rows are worth pausing over. After the second letter the word is \(00\), so \(P=00\) and the context is empty: the recognizer would accept at that point. The next \(0\) cannot externally wrap \(00\), because there is no letter to its left. Nevertheless the empty proper suffix can be internally wrapped, giving the new longest even suffix \(00\) at the last two positions and context \(0\). At the final row, the current \(P=001100\) is preceded by \(0\), not by the arriving \(1\). The proper suffix \(00\) is preceded inside \(P\) by \(1\), so it is wrapped to \(1001\); the remainder of the old palindrome is transferred into the context. That apparent nonlocal jump is the update that the receipt machinery must make bounded-local.

The case sequence \[\text{reset, external, internal, reset, external, external, external, internal}\] will reappear when we interpret the general recurrence. This word will be followed through every layer of the paper: its row 8 becomes the rope update of Example 8.10 and the scaffold batch of Example 12.1. What generalizes from it is the three-way case split and the use of the empty suffix; what is incidental is the particular word.

II Persistent palindrome state

5 The occurrence-context recurrence

Guiding question.  What is the smallest exact word state from which one new letter determines the next longest even-palindromic suffix?

Maintaining a longest suffix is reminiscent of a failure-link automaton (a string-matching automaton whose “failure” transitions fall back to the longest matching proper suffix): when the current candidate cannot be extended, one tries a proper suffix. The difference here is that we cannot follow an unbounded chain during one input step. We therefore separate the combinatorial recurrence from the later question of how its selected transition is exposed by one bounded pointer. This section proves the recurrence with ordinary words only.

5.1 Definitions

Let \(S\) be the input prefix read so far. Let \(P(S)\) be its longest even-palindromic suffix and write \[S=CP,\qquad \ell=C^R.\] The word \(\ell\) is the left-context stack of the current occurrence; its first letter lies immediately to the left of \(P\).

The pair \((D_a(P),\omega_a(P))\) should be read as a factored transition. Its first coordinate is the longest proper suffix of \(P\) that the arriving \(a\) can wrap. Its second coordinate is exactly the material displaced from the palindrome into the reversed context when that transition is taken. It is important that \(D_a(P)\) is selected by an occurrence of \(a\) immediately before the suffix, not merely by equality of palindrome types.

5.2 The three-case update

In Table 1, rows 2, 5, 6, and 7 are external matches; rows 3 and 8 are internal-direct updates; rows 1 and 4 are resets. The final equivalence in the theorem explains why row 2 is accepting and the final row is not. The theorem also shows why keeping only the length of \(P\) would be insufficient: the internal case must identify a particular suffix and the chunk that precedes it.

5.3 The transition table has fixed width

This recursion is the first sign of persistent self-similarity. For the one letter \(b\) immediately before the suffix link, the desired transition is available at the current record. Every other alphabet coordinate is inherited from the suffix-link record and receives the same intervening block. Because the alphabet is fixed, the entire transition table has fixed width. The remaining difficulty is not the number of coordinates; it is transporting the correct historical record and the potentially long intervening word without walking through either one.

6 Typed mirror receipts

Theorem 5.4 reduces online recognition to catenating type-indexed chunks. It does not yet say how a fresh occurrence obtains its suffix-link record without a search. The needed object is a typed receipt.

A palindrome type is a word such as \(001100\). A palindrome occurrence is that word at a specified interval of the input history. The distinction is inexpensive in the mutable palindromic tree of Section 2.8: a dictionary may map a type and a letter to another type whenever the transition is discovered. An append-only scaffold has no such global update. The record available at the current top must already carry a bounded route to the historical occurrence that will certify its next suffix link.

The word “typed” in typed receipt does not mean a programming-language type annotation. It means that the receipt identifies a record of exactly the palindrome type required by the proof. A raw time coordinate says where some relevant substring ended; a typed receipt says which immutable record at that history node represents the required suffix-link occurrence.

Working picture.  Reflect the proper suffix of the new palindrome across its center. Its mirror copy finishes before the newly appended last letter, so it is wholly old. The online construction has already created a record when that palindrome first appeared. The receipt transports a pointer to that record rather than asking the next transition to rediscover it.

What this does and does not say.  The theorem says that the required record exists in the old history. It does not yet say which old field holds a pointer to it; that is Theorem 8.9(iv): in the external case it is the receipt stored in the first cell of the live context rope, and in the internal case it is the header of the old rope entry selected by the letter. Nor does the theorem say that the pointer reaches the birth record; any record of the right type serves (Section 3).

The word “typed” is essential. A raw endpoint does not identify the needed record at bounded depth. Proposition 6.2 makes this precise for the following endpoint-only discipline: store, instead of a typed pointer, the time at which the mirror copy of the required palindrome ends, and recover the record by starting from the longest even-palindromic suffix of the prefix ending there and following suffix links downward.

What this does and does not say.  This is a representation-specific escape theorem, not a language or scaffold lower bound. It says that the positive construction must transport the typed record pointer itself. What generalizes: any discipline that recovers a record by descending a suffix-link chain from an endpoint is unbounded. What is incidental: the particular family \(0^{2m}1100\).

7 Why simpler representations fail

The receipt construction was not guessed in its final form. Several natural representations preserve enough extensional information to describe the next palindrome but do not expose the needed immutable pointer within a bounded number of old-field traversals. Recording these failures serves two purposes. It explains why the positive representation carries apparently redundant occurrence data, and it keeps the propositions in their proper scope. None of them is a lower bound for PEGs, scaffolding automata, or palindrome recognition in general.

7.1 Why an immutable type table is not enough

If one record is created at the first birth of each palindrome type, it is tempting to copy a fixed-alphabet transition table from the suffix-link record, as the mutable palindromic tree would do: an entry for letter \(a\) pointing to the record of the target type \(aD_a(P)a\). The target of a later transition, however, need not exist when the source type is born.

The forced design decision is modest but decisive: transitions must be transported by occurrence-indexed receipts, or by some representation of equal strength. A canonical type node remains useful for explaining suffix relations, but it is not by itself a closed immutable update interface. The reader may ask why the per-letter entries that the final construction does store (Section 12) escape this proposition. They do because they point to the record of the selected suffix \(D_a(P)\), which exists when \(P\) is born (it is a suffix of \(P\)), and not to the record of the target \(aD_a(P)a\), which may not.

7.2 Why raw persistent words are not enough

A persistent rope can share the letters of a context perfectly. Receipts, however, depend on the palindrome around which those letters are interpreted.

This proposition does not forbid structural sharing of the underlying word. It says that the positive object must be an anchored receipt path, and that later reuse must justify why the receipt shadow survives a legal change of physical anchor. Lemma 8.3 supplies exactly that justification.

7.3 Why bounded bridge chasing is not enough

One might defer the missing transition and repeatedly follow the suffix link, testing the bridge letter at each record. The following family makes the number of failed tests arbitrary.

The proposition refutes bounded bridge chasing for this representation. It does not refute recursively stored direct transitions: the final construction materializes the same recursion persistently, so the transition selected in a later step is already at bounded depth.

These eliminations narrow the task to a positive one: define an anchored path whose cells carry typed receipts, and prove that the parts shared after an online update retain the same receipt trace even when their concrete palindrome anchors change. That is the purpose of receipt ropes.

8 Receipt ropes and shadow transport

Guiding question.  How can a persistent sequence share an arbitrarily long old tail when the palindrome at the tail’s central anchor has changed?

8.1 What a receipt rope represents

Consider the current state \((P,\ell)\) with \(\ell=c_1c_2\cdots c_k\). If the next input letters happen to be \(c_1,c_2,\ldots\) in that order, the external case of Theorem 5.4 fires each time: the palindrome becomes \(c_1Pc_1\), then \(c_2c_1Pc_1c_2\), and so on, while the context loses one letter each time. Each of those future palindromes will need its suffix link at the moment it becomes current (Theorem 6.1), and each is determined by \(P\) and a prefix of \(\ell\). A receipt rope stores the context as a sequence of cells, one per context letter, where cell \(i\) carries both the letter \(c_i\) and the typed receipt for the palindrome obtained after \(i\) external matches. Popping a cell (an external match) then exposes, in the next cell, exactly the receipt the new current palindrome needs. The rope is not merely a word with annotations: it is a walk through palindrome occurrences, anchored at \(P\).

The record at the front is a header: the receipt of the anchor itself. If a pop makes the first wrapped palindrome current, its suffix-link receipt is promoted to the new header. This promotion is what an ordinary list of letters lacks.

8.2 Definitions

The header is the receipt required if the anchor becomes current; taking a tail promotes the first cell’s receipt to the new header. Anchored paths obey the literal catenation law \[\Pi(A,uv)=\Pi(A,u)\cdot\Pi(\operatorname{wrap}_u(A),v).\] The catenation law carries an important guard: the second path is anchored at the result of wrapping \(A\) by \(u\). Two identical raw words do not therefore represent interchangeable receipt ropes at arbitrary anchors. Proposition 7.2 is the one-letter instance of this fact.

8.3 The bridge-shadow identity

The physical palindrome states in a retained context tail can change after a prepend or reset. The next lemma shows that the typed receipt trace does not. Its two anchors \(H\) and \(P\) are different words; the claim is that wrapping them through the same context produces the same sequence of suffix links.

(The statement allows \(P=\epsilon\): then \(H=Rb\) is any nonempty even palindrome with \(\lambda(H)=\epsilon\), and the hypothesis on \(w^RP=w^R\) says \(w^R\) has no nonempty even-palindromic suffix.)

Working picture.  The anchors \(H\) and \(P=\lambda(H)\) begin with the same suffix-link choice as soon as the first context letter is not the bridge \(b\). If their receipt traces first diverged later, the unequal bridge exposed at that first divergence could be reflected through the context already consumed. The reflection would form an even-palindromic suffix strictly longer than \(P\) in \(w^RP\), contradicting the hypothesis that \(P\) is longest. The proof below adds indices and a strict length bound to this picture.

The length inequality in (2) is not bookkeeping decoration. It ensures that the bridge inspected at the next step lies inside the suffix shared by both physical anchors. The parity subcase is the only point at which equality could occur; resolving it by constructing the forbidden longer suffix is what makes the shadow statement global rather than merely a one-cell observation.

8.4 Direct and reset ropes, and the mirror-prefix lemma

For nonempty \(Y\) with suffix link \(L\), bridge \(b\), and bridge block \(B\), write \[Y=RbL=LbB.\] When \(D_c(Y)\) is defined, define the direct headered rope \[\Omega_c(Y)= \widehat\Pi\bigl(cD_c(Y)c,\omega_c(Y)\bigr).\] When it is undefined, define the reset rope \[Z_c(Y)=\widehat\Pi(\epsilon,cY).\] The direct rope is the context rope that the internal case of Theorem 5.4 will need: it is anchored at the palindrome \(cD_c(Y)c\) that the letter \(c\) creates, and its cells carry the receipts for the displaced chunk \(\omega_c(Y)\) that becomes the front of the new context. The reset rope is the analogue when nothing can be wrapped: anchored at \(\epsilon\), its cells carry the receipts for the whole failed candidate \(cY\).

The last cell of such a rope has a receipt that can be named explicitly. This fact is used three times below (in Theorems 8.7 and 8.9), so we state it once.

8.5 The receipt-rope recurrence

In words, every off-bridge direct rope and every reset rope consists of three pieces already visible at bounded depth: the corresponding rope at the suffix link \(L\), one bridge cell, and the body of the single bridge-matching rope at \(Y\). The bridge-shadow identity is what makes the third piece literally shareable; without it the equation would describe only equal raw words and would not be a persistent pointer construction. Note that the third piece is shared between two ropes whose anchors differ: in \(\Omega_c(Y)\) the cells after the bridge cell are anchored at \(b\,(ZcL)\,b\), in \(\Omega_b(Y)\) at \(bLb\).

8.6 Full receipt closure

The adjective “abstract” marks a clean interface boundary. The theorem has already eliminated suffix-link search, mutation, global interning, and random access to the old input. It assumes only a persistent sequence supporting a fixed collection of operations in worst-case bounded structural work. The next part supplies that sequence and explains how its fresh structural records are represented by the scaffold. Which old fields hold the receipts named below is fixed by the record layout of Section 12.

III Turning bounded records into a scaffold

9 The cyclic allocation obstacle

Guiding question.  If every rope operation performs only bounded work, why can we not simply allocate its fresh immutable records in topological order?

9.1 Records, fields, and batches

From here on a record is a finite tuple with a finite tag, a finite payload (such as a letter), and a fixed number \(q\) of pointer fields, each of which is missing or points to a record. A persistent program holds a fixed number \(s\) of roots (pointers kept in finite control) and, at each step, reads old records by following fields from the roots and creates a finite batch of fresh records. The fresh batch is a finite labelled directed graph: its vertices are the fresh records (slots \(0,\ldots,A-1\) for some bound \(A\)), and each field of each slot is missing, points to an old record, or points to a slot.

In ordinary functional programming a fresh record can only point to records that already exist when its constructor runs, so the fresh batch of one step is acyclic and can be allocated in topological order: first the records with no fresh targets, then those pointing only to them, and so on. Three small batches show what a cycle would mean. A self-loop has one slot \(x\) with field \(f(x)=x\). A forward reference has two slots \(x,y\), created in that order, with \(f(x)=y\). A mutual cycle has \(f(x)=y\) and \(g(y)=x\). All three are perfectly good finite labelled adjacency tables; none can be produced by allocating one constructor at a time, because the first constructor would have to store a pointer to a record that does not exist yet.

9.2 The cycle the palindrome construction forces

The obstruction is already visible in equation (2) of the closure proof. A fresh palindrome occurrence record \(P\) stores the root of its bridge rope \(\Omega_b(P)\). The final fresh cell of that rope stores the typed receipt \(P\). Thus \[P\longrightarrow\Omega_b(P) \longrightarrow\text{terminal receipt }P.\] Both edges are semantic requirements of the same input transition. Neither endpoint can be replaced by an old record, and neither ordering of the two fresh objects makes all pointers backward. Example 8.10 exhibits the cycle concretely: the record for \(1001\) and the cell \((1,1001)\) are both created at row 8 and point at each other.

This is not a request for a recursively defined infinite object. After the input letter and bounded old observation are fixed, there are finitely many fresh slots and a finite adjacency table saying which slot each field targets. The graph may contain a cycle, exactly as an ordinary finite directed graph may. Decoding the graph means recovering that adjacency table; it does not mean recursively unfolding the cycle into a tree.

A previously considered source interface allowed a fresh field to name only an old object or an earlier fresh slot. That interface silently excludes Figure 9; proving closure inside it would prove a theorem about the wrong program. The repair is to permit arbitrary references within one uniformly bounded fresh batch and then show that this stronger source step still compiles to the target model. The palindrome batch is larger than the three toy batches but no different in kind.

10 Bounded simultaneous record transducers

We now define the source machine precisely and compile it into the scaffold model of Definition 2.6. This section is independent of palindromes: a reader may regard its input as an arbitrary bounded persistent-record update.

10.1 The source model

An old address is a root together with a sequence of at most \(r\) field names; it is dereferenced by starting at the root and following the named fields. “Simultaneous” constrains dependencies rather than prescribing a physical allocation primitive. The plan may depend on finite control and bounded old structure, but it may not branch on a fresh record as though that record had already been evaluated. The adjacency table is output data of the transition. The initial roots may be missing or point into a fixed finite, immutable, pointer-closed initial record graph. The compiled decoder stores that graph and its initial roots as finite table data; those virtual records are present from time zero and are never charged to a fresh batch.

10.2 Tuple packing

The scaffold appends one node per letter; the transducer creates up to \(A\) records per letter. Tuple packing resolves the tension: the one physical node \(v_t\) appended at time \(t\) represents the entire batch born at time \(t\), and a finite slot number \(i<A\) says which logical record is meant. A logical pointer is decoded as a pair \((v_t,i)\). The physical node’s label records, for each of its ports, the slot number of the record that port’s target stands for; old logical field traversal therefore alternates between a physical port and the finite slot tag read at the node that owns the port. A fresh pointer uses \(\mathsf{SELF}\) to return to \(v_t\) and carries the desired fresh slot in the new label. The physical graph remains a legal scaffold; “record” is an interpretation placed on its ports and label.

For the three sample batches of Section 9, the compiler emits one physical node in every case. A self-loop is \(\mathsf{SELF}\) tagged by its own slot; a forward reference is \(\mathsf{SELF}\) tagged by the later slot; and the two edges of a mutual cycle are two \(\mathsf{SELF}\) ports with opposite slot tags. This explicit check is useful because it isolates the sole new semantic feature from all palindrome and steque details.

11 Opaque-atom staging

Guiding question.  How does a worst-case constant-time functional sequence operation become a bounded fresh-record plan, and where may the cyclic payload be tied in?

The receipt proof has reduced the online step to a constant number of catenable-sequence primitives. We now justify that these primitives expose a bounded record plan without pretending that an ordinary immutable functional value can tie the cycle in (2).

11.1 Why an ordinary list is not enough

An ordinary persistent singly linked list provides constant-time head, tail, and insertion at the front, but not catenation or insertion at the rear. A naive catenation must copy one operand or defer work in a thunk (a suspended computation stored in place of its result); copying is unbounded in the current step, while an unevaluated thunk merely moves that unbounded work to an unspecified later step. Memoization—caching a computed result inside the structure—is a side effect and is excluded from the strict model below. Receipt closure needs the following stronger abstract interface.

11.2 The inherited theorem and its model

Kaplan and Tarjan supply regular catenable-steque operations with worst-case constant cost in their strict purely functional model. That theorem is an important source premise, but it does not by itself exhibit the stronger finite-record interface used below. In particular, the published theorem does not state a typed finite decision tree, a uniform allocation bound, or base-element opacity. Those are separate bridge obligations.

Here “regular” is the invariant of Kaplan and Tarjan’s representation (§5.1 of their paper) that each operation is proved to restore; the reader may treat it as “in the normal form the operations expect”. For their paper, Kaplan and Tarjan define “purely functional” to mean built only from \(\mathsf{car}\), \(\mathsf{cons}\), and \(\mathsf{cdr}\)—pair construction and the two projections—with memoization explicitly excluded [6, p. 578, footnote 1]. This strict model is stronger for our purpose than a bare unit-cost RAM claim.

One scoping remark is essential for the next theorem. The steque representation is recursive: a steque of elements of type \(A\) contains buffers and a child steque whose elements are pairs over \(A\), and so on [6, §5.1, pp. 588–589]. The operations inspect those pairs and buffers freely; they are the structure’s own constructors. The described operations appear to move base elements without inspecting them, but Theorem 5.1 does not state an opacity theorem. In our application the steque base element is the whole fixed-shape cell whose receipt field may contain the symbolic fresh owner. Establishing that the intended implementation never inspects, compares, hashes, identity-tests, or traverses such cells remains part of the bridge audit.

The theorem separates two notions that are easy to conflate. The steque allocates an acyclic structural skeleton; this follows from ordinary strict functional evaluation, because a fresh constructor can point only to old or earlier structural constructors. Some fields of that skeleton are payload positions. The sequence implementation neither follows nor compares them. Replacing a symbolic payload atom by the simultaneously fresh owner pointer may therefore make the combined semantic graph cyclic without changing any branch or allocation in the steque calculation.

Equivalently, opaque-atom staging is a substitution lemma. Run the structural program with a variable \(x\) in each fresh cell position. The old structure determines a finite graph expression \(G(x)\). The simultaneous batch substitutes a fresh cell slot for \(x\), makes its receipt field target the owner slot, and places the fixed result roots in that owner. No recursive evaluation of \(G\) is performed after substitution. Figure 9 depicts precisely this boundary.

Source-model applicability certificate. The length-free four-operation variant inspected at the paper-pinned source commit is a finite, nonrecursive, base-element-opaque case program. Separate branch audits prove its list semantics, assertion safety, bounded source allocation, old-input reads, and old-pointer exposure. The fixed client layout below composes those local certificates. This closes the earlier finite-resource omission in the stated abstract immutable source-record model, not in a literal OCaml runtime or machine-address model.

Why sequential address bounds compose. Give every intermediate pointer the largest old-root address length it may denote. A selector adds its field cost. If an operation reads to depth \(d\) from one input and exposes an old pointer to depth \(e\), a later dependent read has level \(L+d\) and the output has level at most \(L+e\). Dependent edges add and independent paths take their maximum. Induction over the finite client dependency graph gives the global radius. This max-plus argument is per labelled input lineage and does not require an alias oracle.

The hypotheses are essential. Identity tests can distinguish heaps with equal labelled unfoldings; inspecting a fresh receipt cell can make a branch depend on the owner cycle; local read bounds without output exposure do not control a later dependent call; an unbounded walk has no finite transition table; and an escaping temporary must be counted as a persistent record. The theorem claims none of those cases.

Application certificate. In the direct-palindrome client, the live-front and source cells returned from old sequence roots are old exact-token cells, so their letter and receipt reads are ordinary charged old observations. The external acceptance uncons reads the structural tail returned by the first uncons; later catenations also consume earlier structural results. The symbolic evaluator partially evaluates exactly those fresh structural constructors. Neither of the two fresh cells nor the fresh owner is inspected. The existing max-plus certificate already includes every dependent path. Conditional on its manual local read and exposure premises, Theorem 11.3 preserves \(s=2\), \(A=8838\), \(q=7\), and \(R=1534\).

Theorems 11.2 and 11.3 now connect the explicit source program to Definition 10.1. Appendix D still records why the separate Rocq implementation does not verify the inspected OCaml source. The `55/766` old-read ceilings remain manual source proofs and the weakest quantitative premise; this is not a literal runtime or external-validation claim.

12 A direct palindrome scaffold

Guiding question.  Do the word recurrence, receipt closure, catenable sequence, and simultaneous compiler now meet with uniform constants in one machine?

12.1 The record layout

We assemble the construction. The persistent program keeps \(s=2\) roots: the current occurrence record and the live context rope. Finite control remembers whether the current palindrome is empty and the acceptance bit determined by whether the live rope has empty body.

An occurrence record for a nonempty palindrome \(P\) has the following fields.

1. A suffix-link field: a typed pointer to a record of type \(\lambda(P)\), or the empty record \(\bot\) if \(\lambda(P)=\epsilon\).

2. A bridge payload: the letter \(b_P\).

3. For each letter \(c\in\{0,1\}\), a table entry, which is either direct—a tag, a typed pointer to a record of type \(D_c(P)\) (the transition receipt), and the rope root of \(\Omega_c(P)\)—or reset—a tag and the rope root of \(Z_c(P)\).

The empty record \(\bot\) has no suffix link and no bridge, and its two entries are the reset ropes \(Z_c(\epsilon)=\widehat\Pi(\epsilon,c)=(\bot;(c,\epsilon))\); it belongs to the fixed virtual initial graph and is decoded from time zero. A rope value is a header receipt together with a steque root whose elements are cells \((c,\text{receipt})\).

For the explicit source-resource certificate, this logical layout has three physical record shapes. An occurrence owner has seven direct pointer fields: suffix; transition, header, and body for entry \(0\); and transition, header, and body for entry \(1\). Its bridge and two direct/reset tags are finite payloads; a reset tag guards a missing transition pointer. A live-rope record has header and body fields. A cell record has a finite letter and one receipt pointer, and its pointer is the opaque element stored by the sequence. Table entries and their rope pairs are therefore flattened into the owner rather than separately boxed. The two roots remain the owner and live-rope records.

The transition receipts materialize the chunk recursion of Lemma 5.6 persistently: for the bridge letter the transition receipt is the suffix link (\(D_b(P)=\lambda(P)\)), and for the other letter it is copied from the corresponding entry of the suffix-link record (\(D_c(P)=D_c(\lambda(P))\)), one old pointer read at creation time. This is what Proposition 7.3 demanded: the selector that a later step needs is already at depth one, not at the end of a chain.

12.2 One step

On input \(a\), inspect the live rope’s first cell and the \(a\)-entry of the current record. The old live-rope header is not read. Theorem 5.4 selects the case: external if the first cell’s letter is \(a\); internal if the \(a\)-entry is direct; reset otherwise. Then:

In the two nonreset cases the fresh record is filled by Theorem 8.9: bridge \(b\) and bridge rope from the source rope by one pop and one inject (equation (2)); transition receipt for \(b\) equal to the suffix link; for the other letter \(c\), transition receipt copied from the \(c\)-entry of the suffix-link record and rope built by Theorem 8.7 with two catenations. Theorem 11.2 stages each opaque sequence operation, and Theorem 11.3 symbolically composes the complete eight/eight/two client into one old-dependent simultaneous plan. Theorem 10.2 appends that batch as the one scaffold node required for the arriving letter. Acceptance is the finite empty-body test on the live rope (Theorem 5.4).

12.3 Uniform constants

All constructors, letters, table coordinates, and slot tags range over finite sets. In the explicit abstract source-record model, the local sequence certificates and complete eight/eight/two client schedules give \(A_*=8838\) charged fresh records and old-address radius \(R_*=1534\). The external branch controls both maxima; its radius is the live-body selector, the first pop’s tail exposure, and the acceptance pop: \(1+767+766=1534\). Internal has radius at most \(881\), and reset at most \(768\). The reset value corrects 767 by counting the client’s inspection of the opaque cell returned from the old live body.

Every retained sequence record has at most five pointer fields, while the flattened owner has seven, so \(q=7\) in this model. Bounded temporary vectors, result packages, GADT witnesses, and transition-local products are compiled into finite control rather than retained as records. Theorem 11.3 justifies that erasure and eliminates observations of intermediate fresh structural values by symbolic partial evaluation. Literal OCaml evaluation can allocate an eight-pointer temporary tuple, so this is not a runtime-heap claim. Conditional on the manual local read and exposure bounds, the two current roots and Theorem 10.2 give the deliberately nonminimal degree bound \(2+8838\cdot7=61868\) and distance bound \(1535\). The earlier formulas \(A=6K+4\) and \(r=6K+8\) remain withdrawn.

12.4 The run invariant and the theorem

After reading a prefix \(S=CP\):

1. the decoded occurrence root names a record for the current occurrence of the longest even-palindromic suffix \(P\) (the empty record if \(P=\epsilon\));

2. the decoded live-rope root denotes \(\widehat\Pi(P,C^R)\);

3. every table entry in every reachable occurrence record has the word and receipt semantics of Section 8 (its rope is \(\Omega_c\) or \(Z_c\) of its record’s type, and its transition receipt, when present, names a record of type \(D_c\) of that type); and

4. finite control marks acceptance exactly when the live rope has empty body.

The empty initial prefix satisfies the invariant using the distinguished empty record and empty rope. One application of the word recurrence chooses the right abstract update; receipt closure proves the new decoded objects have the required semantics; opaque staging and the compiler prove that the single new physical node decodes to those objects. This is the induction performed in the final theorem.

Scope and assurance. The earlier real-time transfer proof already established the membership conclusion and refuted LMR’s Conjecture 7. The contribution here is a different direct internal explanation. Its local `55/766` address proof remains manual, and the reviews share model dependencies; no external specialist validation, literal OCaml runtime theorem, or OCaml–Rocq correspondence is claimed.

IV Result, meaning, and evidence

13 What the direct route contributes

The corollary settles no membership question that was still open: the earlier transfer paper [5] already proved \(\mathsf{EPAL}_2\in\mathsf{PEG}\). The contribution is a different direct factorization of that fact. It exposes the recognition state as a persistent palindrome algorithm and isolates interfaces that can be reused or challenged independently. The source-level data-structure interface and the whole-client symbolic normalization are explicit; the quantitative address certificate remains the weakest manual premise.

First, the palindrome side replaces global mutable type transitions with typed occurrence receipts. The longest-suffix recurrence is represented by headered ropes whose shared tails retain a provably invariant receipt shadow. The endpoint, type-birth, anchor-dependence, and bridge-chasing families explain why each extra coordinate is present. This is a more informative outcome than merely knowing that some real-time machine exists: it identifies the exact historical information a direct immutable recognizer carries.

Second, the compiler side shows that a bounded persistent update need not be topologically ordered within one time step. A fixed finite cyclic adjacency table is no harder for a scaffold node to encode than an acyclic one, because all logical fresh records occupy slots of that node and \(\mathsf{SELF}\) supplies the common physical target. Opaque-atom staging gives a disciplined way to use this fact with ordinary strict functional data structures: compute their acyclic skeleton first, and tie any semantic payload cycle only in the final simultaneous batch.

These results motivate questions about other online algorithms, simultaneous-batch normal forms, and receipt replacements for mutable canonical indexes. Here we prove a compiler theorem, a bounded-client normalization theorem, and one direct palindrome application; we do not classify PEGs, scaffolding automata, persistent algorithms, or palindromic data structures.

13.1 Comparison of the two proof routes

The transfer route and the direct receipt route should be viewed as complementary explanations. Both are proofs of the same membership statement. Their internal palindrome arguments and source machines differ, while both ultimately use the Loff–Moreira–Reis scaffold-to-PEG direction.

Agreement at the final statement is useful assurance, but the routes are not independent proofs of every intermediate lemma: both eventually use the Loff–Moreira–Reis scaffold-to-PEG direction. Their internal palindrome arguments and scaffold source models are different. A defect in the direct receipt construction would not retract the earlier membership result; it would invalidate the claimed persistent explanation and compiler application.

13.2 Why the negative representation results matter

The four escape families are small mathematical results with deliberately narrow conclusions. Their value is diagnostic. Each converts an intuitive but underspecified implementation proposal into an exact doctrine and then exhibits an unbounded parameter that doctrine fails to expose. The residue of the failure becomes the next positive invariant: endpoint escape motivates typed pointers; future type transitions motivate occurrence receipts; anchor dependence motivates anchored ropes; bridge escape motivates recursively materialized direct ropes and their transition receipts. The final coordinate system is not asserted to be canonical. It is the first one in this chain for which every semantic update, persistent operation, and scaffold address closes with an explicit uniform bound.

14 Assurance, provenance, and the viewpoint

14.1 What kind of evidence supports what

The theorems of this paper have ordinary written mathematical proofs. The public package also contains executable checks; they answer different questions, and none of them changes the mathematical status of a theorem.

The public package contains five independent Python programs. They check the three-case context recurrence, typed mirror receipts, receipt-rope closure, simultaneous cyclic batch decoding, and the modern catenable-interface calibration, on exhaustive domains of words up to a fixed length and on random longer instances (counts are recorded in the package’s audit/RUN-OUTPUT.txt). The programs use exact finite words and pointer graphs. They corroborate the displayed identities and protect against regression, but bounded computation is not the proof of a universal theorem. The checks are intentionally divided at the same seams as the proof: a word checker has no implementation of scaffolds; the compiler checker generates bounded record heaps and cyclic batches without palindrome semantics; the source-interface checker inspects a pinned catenable implementation without assuming the receipt equations. This separation is not complete logical independence, but it reduces the chance that one shared encoding mistake makes every check agree.

Three boundaries should remain visible.

1. The conclusion \(\mathsf{EPAL}_2\in\mathsf{PEG}\) was already proved by the earlier real-time transfer route [5]. This paper contributes a direct persistent-record route whose source-resource interface and whole-client normalization are explicit. The local old-address ceilings remain manual source proofs.

2. Endpoint-only, type-birth-only, and bounded bridge-chasing failures are representation-specific. They are not lower bounds against all scaffolding automata.

3. External specialist review and a broader novelty search remain open. The manuscript contains complete arguments for the compiler and conditional staging lemma, plus a later source-level resource certificate; it does not yet claim that the independently audited pieces constitute a complete audit of the assembled direct route. Validity, novelty, and review status remain separate, and no novelty claim is made here.

14.2 Provenance and AI assistance

The arguments were developed in FPRD Lab, an AI-assisted research project. The mathematics is the author’s responsibility; AI systems drafted and checked text and code under the author’s direction, and an adversarial pass by such a system found, before publication, that an earlier version of the source model excluded the very cycle its own receipt equation creates (Section 9); the present simultaneous model is the repair. The primary sources [7, 6] were read in full and the exact statements used are quoted with page numbers; copies and extracted text are held locally and are not part of the public repository. No proof assistant is used for this paper; an existing Lean development of the project independently reconstructs LMR’s sufficient direction, but the paper cites the published theorem and does not rely on that reconstruction.

14.3 The viewpoint, stated more fully

The viewpoint of Section 3 can be stated as a discipline with four layers, each implication between which is a theorem obligation:

1. Semantic algebra: exact recognition behaviors and their constructors, quotiented only by exact behavior equality.

2. Observational completion: finite interfaces—for example, agreement on all inputs through a bounded length—and their quotient maps.

3. Presentation-generated dynamics: a distinguished initial state and named actions extracted from, or supplied by, one finite presentation.

4. Coordinate realization: an injective state encoding, coordinates for every named action, and a uniform readout recovering recognition behavior from coordinates and input.

In this paper the exact word recurrence and receipt equations supply the semantic behavior; bounded old-record and scaffold unfoldings are the finite interfaces; input letters generate the persistent occurrence dynamic; and the tuple-packed compiler supplies both an injective scaffold encoding and its uniform decoder. Acceptance is the final observation that the reversed context is empty. The transfer route of [5] studies a different presentation-generated dynamic with the same language observation; the two routes therefore complement one another even though both end at \(\mathsf{EPAL}_2\in\mathsf{PEG}\). Changing the observation may merge states without changing the presentation; changing the presentation may change internal actions without changing the accepted language. Both phenomena are kept visible rather than quotiented away at the start. This failure-to-invariant progression (Section 7) is where the viewpoint affected the proof most visibly: instead of treating a convenient representation as the recognition dynamic, the investigation repeatedly projected the same word semantics into competing persistent coordinates and asked which observations remain bounded.

A Notation

Table 3 collects the symbols whose meanings cross more than one proof layer. A symbol naming a word is not silently identified with the record that represents an occurrence of that word.

B Fixed allocation inventory

The proof needs uniform finiteness, not optimized constants. Nevertheless an explicit inventory prevents the phrase “constant number of operations” from hiding an input-dependent loop.

The following historical six-call list counted only constructive rope updates. A later literal client audit found that it omitted branch observations and one second uncons in external acceptance. The corrected complete schedules are eight calls in each nonreset branch and two in the reset branch.

1. one pop to expose the body of the source direct or reset rope;

2. one inject to add the terminal receipt carrying the fresh owner;

3. one singleton construction for the new bridge cell;

4. two catenations for the off-bridge direct or reset table entry; and

5. one pop or catenation for the new live context.

The fixed physical layout uses one seven-pointer occurrence owner, one two-pointer live-rope wrapper, and one-pointer receipt cells. Binary table entries are flattened into the owner. The source sequence stores opaque pointers to cells rather than inline cell fields. The nonempty reset ropes are ordinary dynamic sequence values; only the distinguished empty owner’s reset ropes are virtual.

In the explicit abstract source-record model, the three branches have allocation/radius pairs \((8838,1534)\), \((6798,881)\), and \((2941,768)\). Thus \(A_*=8838\), \(R_*=1534\), and \(q=7\). Theorem 10.2 gives degree at most \(61868\) and distance at most \(1535\) for this abstract source program. The reset radius is 768, not 767: the returned cell lies within the sequence exposure bound and the fresh live wrapper adds one field edge. These are deliberately loose source-model bounds, not measurements of an OCaml runtime. The former \(6K+4\) and \(6K+8\) formulas are not retained.

C Claim and reproducibility map

The publication package separates mathematical statements from the mechanisms used to challenge them, and records each theorem under an identifier in the project’s claim ledger. FPRD-D36 is Definition 10.1. FPRD-T125 is the receipt package comprising Theorems 5.4, 6.1, 8.7, and 8.9, with Lemmas 8.3 and 8.5. FPRD-T126 is Theorem 10.2. FPRD-T127 comprises Theorems 11.2 and 11.3. FPRD-T128 is Theorem 12.2 and Corollary 12.3. These identifiers are bookkeeping; they carry no mathematical weight.

The five public checkers correspond respectively to occurrence-context words, mirror receipts, receipt closure and shadow reuse, simultaneous record compilation, and the catenable-sequence interface. Their canonical output is stored with the paper so that a rerun can be compared byte for byte. The package verifier rebuilds the PDF, checks its reader-facing anchors and size guardrails, reruns the focused mathematical audits, and checks the central claim/publication registries.

Primary papers and external source checkouts are intentionally not copied into the public repository. The source audit records titles, versions, links, local checksums, and exactly which theorem or source property is used. A successful checker run is evidence about the tested finite instances or pinned source; it does not change the mathematical status of a theorem, certify novelty, or substitute for specialist review.

D Modern source calibration

Viennot, Wendling, Guéneau, and Pottier give a later OCaml implementation and a separate Rocq implementation of Kaplan–Tarjan catenable deques [10]. Their paper clearly separates the evidence: the OCaml code is tested but not verified; the Rocq code has machine-checked functional correctness; there is no formal correspondence between the two; and the Rocq extraction does not establish the same constant-time bound because runtime indices are retained.

Kaplan–Tarjan’s Theorem 11.1 supplies the abstract worst-case sequence result, not the stronger finite-record interface. The modern source is a hostile implementation calibration. At the pinned commit recorded in the package’s source audit, its operational core is strict and nonrecursive. The length-free variant replaces unbounded cached-length observations by fixed persistent end probes and matches the outer empty constructor rather than using polymorphic structural equality. A constructor proof establishes its list semantics through the sealed four-operation facade, and separate audits enumerate source allocations, old reads, and output exposure. The client certificate then composes those bounds through an explicit record layout. This is still a source-level argument rather than verification of the OCaml runtime or a correspondence proof with the Rocq development.

This separation matters because “functionally verified” and “satisfies the bounded-record cost interface” are different obligations. The Rocq development supplies the former for its own implementation but not the required constant-time extraction; the OCaml implementation supplies executable nonrecursive code but lacks a proved correspondence to the Rocq development. The original theorem plus the conditional staging lemma do not silently supply their conjunction.

Acknowledgment of inherited work

Kaplan–Tarjan catenable steques and the Loff–Moreira–Reis scaffold/PEG correspondence are inherited mathematical results. The Viennot et al. implementations are external work used for calibration. This paper contributes the occurrence-context formulation, typed receipt system, representation escape audits, simultaneous cyclic source model, tuple-packed compiler, opaque-atom staging bridge, direct composition, and the adversarial correction that exposed the same-step cycle before publication. Detailed attribution is recorded in the accompanying package files.