When two construction histories mean the same thing

A persistent graph records how it was built. An observer at its newest node may see only a small part of that record. This article asks which changes to the construction preserve what such an observer can learn, and how those changes can be composed.

Start with three nodes, each with one outgoing edge. Node 1 has label 1 and points to itself. Node 2 also has label 1 and points to node 1. Node 3 has label 0; when created, it copies node 2’s outgoing endpoint, so it points to node 1. Looking forward from the final root, an observer sees 0, then 1 forever.

Node 2 is unreachable from that final root. Nevertheless, its edge was consulted when node 3 was created. Erasing node 2’s label has no effect on the final graph. Changing its edge before replaying the construction may change where node 3 points. Unreachable information and information irrelevant to replay are therefore different notions.

That example motivates causal support: keep the labels and edges visible in the final graph, then also keep every earlier edge that was used to compute a kept edge. Repeat until all such dependencies have been included. Everything outside this support can be changed without affecting replay. The proof follows those dependencies in chronological order.

The article also distinguishes two ways for histories to agree. They may give the same observable graph at every intermediate time, or only at the final time. The first is stronger. A change that moves a useful record from an earlier node to a later node can preserve the final answer while changing what was visible midway through the construction.

For the stronger equivalence, two local moves suffice. An endpoint detour replaces one path description by another path reaching the same old node. An absorption gives a new node its own self-loop when it already presents the same recursive behavior as an older self-looping node. The proof shows that repeatedly applying these moves reaches one canonical history for each complete sequence of observations.

Final observation allows more freedom. Some labels become irrelevant; useful records can move between construction times. In the case of one outgoing edge and distance-one access, these movements admit a particularly concrete description. Place the essential records in increasing time order, with the final root fixed at the final time. A move shifts one record into a neighboring vacancy. The legal placements form an order-ideal lattice, whose commuting moves give a cube geometry.

This geometric description is a theorem about histories and their relationships. It does not automatically give an automaton a procedure for discovering equivalent histories or normalizing them while input arrives. The distinction matters to the later residual-access result: a compact semantic description and an inexpensive update procedure are separate achievements.

The final section returns to computation. It shows how bounded batches of logical records, including fresh cycles, can be represented by one scaffold node per input symbol. The same finite slot technique appears in the direct-palindrome construction. Its current Draft 5 direct theorem is conditional on the complete Section 11.1 sequence contract; the concrete implementation remains informal evidence with open source-contract obligations, and numerical radius/distance remain withdrawn. The follow-up unary coherence article goes further in another direction: it compares whole sequences of history transformations, rather than only their endpoints.

1 From a finite presentation to a history algebra

1.1 The machine and the question

Loff, Moreira, and Reis (LMR) introduced scaffolding automata as a machine model for parsing expression grammars [12]; Section 2 defines both. For now the picture suffices. At each input position the machine reads a fixed-radius neighborhood of the current top of a persistent graph, chooses a finite label, and appends one new node. Each new edge is missing, points to the fresh node itself, or follows a bounded path from the preceding top. LMR prove that a language has a PEG if and only if its reversal is decided by such a machine [12, Theorem 16].

The usual observation made of such a machine is acceptance: does the run end in an accepting state? This paper keeps more of the generated object visible. A run has a physical graph at every time; an observer standing at the top and following edges sees, at every time, a behavioral figure; and at the end there is a final figure. Those are different quotients of the same history, and the paper’s question is:

When two finite construction histories generate the same behavior, which local fold, unfold, routing, erasure, and feedback moves connect them?

The answer has two layers. For every fixed finite degree and observation distance, two graph-local rewrites give a terminating, confluent presentation of the histories that have the same behavioral figure after every prefix (Theorem 6.8). Equality of only the final figure is harder because it forgets intermediate behavior; we prove what we can (Section 7–8) and state exactly what remains open (Section 10).

1.2 In what sense this is an “algebra”

We call the system of histories, behavioral equivalences, and rewrites an algebra in the informal sense in which one speaks of “the algebra of regular expressions”: a collection of objects, operations on them (appending a row, rewriting a row), and equations between the results. Where a formal algebraic structure is meant, it is named and proved: the monoid of rows under concatenation (Section 3), the transformation monoid of port navigation and its $\mathcal R$-triviality (Corollary 4.2), and the rewriting system with its normal forms (Theorem 6.8). No claim is made that the calculus is an instance of any particular variety, category, or polygraph; whether it is, is an open comparison (Section 10).

1.3 What is new here, and what is inherited

The paper leans on three established theories and does not rename them. Bisimulation (two states are equivalent when every observation and every successor behavior matches) and the quotient of a system by it are standard objects of coalgebra [15, §2, §5–6]; the familiar instance is the minimal deterministic automaton obtained from the residuals (derivatives) of a language [3, 13]. Bottom-up merging of equivalent states and incremental minimization of acyclic deterministic automata are established [5, §2]. Cyclic term graphs, their unwinding into infinite trees, copying, hidden nodes, and confluence have a substantial theory [2]. Section 11 lists what is inherited from each.

The target here is the intersection of four restrictions that none of those theories imposes together:

1. one immutable layer is appended per input symbol;

2. every old address is read from the preceding top within one fixed radius;

3. a strong move must preserve the figure after every prefix; and

4. soundness must survive every common future continuation.

The resulting local rules live in the generated scaffold graph. They need not be bounded contiguous substring rules in the linear word of rows.

1.4 The viewpoint

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, and Section 11 states plainly what was checked and by whom. In this paper the viewpoint has a concrete form, Figure 1: changing an observation may merge histories without changing the rows that generated them; changing a presentation may alter the physical history while preserving every behavioral figure. The algebra begins by keeping both phenomena explicit.

1.5 How to read this paper

Section 2 supplies the background: words and languages, context-free grammars and PEGs, LMR’s scaffolding automaton with a drawn example, and the step from automata to arbitrary construction histories, which is where this paper’s objects begin. Section 3 defines histories, unfoldings, figures, and the two equivalences, with one worked history that recurs throughout. Sections 4–6 develop the strong-trace calculus: the chain theorem, guarded folds, and the two rewrites with their normal form. Sections 7–8 treat final observation. Section 9 gives the feedback application. Sections 10–11 state open problems, what is inherited, and how the work was produced. Every proof states its strategy first; every example says what generalizes.

2 Background

2.1 Words and languages

An alphabet is a finite set of letters; a word is a finite sequence of letters, $\epsilon$ is the empty word, and $\Sigma^*$ is the set of all words over $\Sigma$. A language is a set of words. The reversal of $w=c_1\cdots c_n$ is $w^R=c_n\cdots c_1$. A monoid is a set with an associative operation and an identity; $\Sigma^*$ under concatenation, with identity $\epsilon$, is the free monoid on $\Sigma$: every word is a unique sequence of letters.

2.2 Context-free grammars and parsing expression grammars

A context-free grammar has terminal symbols, non-terminal symbols, a start symbol, and rewriting rules $A\to\varphi$ with one non-terminal on the left [4, pp. 120–122]; it generates the words obtainable from the start symbol by repeatedly replacing a non-terminal by a right-hand side. For instance $S\to0S0\mid1S1\mid\epsilon$ generates the even-length binary palindromes $\mathsf{EPAL}_2=\{ww^R\}$. The reading is existential: a word is in the language if some derivation produces it.

A parsing expression grammar (PEG) [7, §3] uses similar rule shapes with an operational meaning. Expressions are built from letters, non-terminals, $\varepsilon$, and $\mathsf{FAIL}$ by sequence $e_1e_2$, ordered choice $e_1/e_2$, and the predicates $!e$ and $\&e$; each non-terminal $A$ has one rule $A\leftarrow R(A)$. Recognition $\operatorname{Rec}_G(e,x)$ reads $x$ from the left and either fails or succeeds consuming a prefix: a letter consumes itself; a sequence runs its parts in order; ordered choice runs $e_1$ and commits to it if it succeeds, trying $e_2$ only if $e_1$ fails; $!e$ succeeds (consuming nothing) exactly when $e$ fails [12, Definition 3, Algorithm 1]. The procedure is deterministic. A grammar is total if recognition never loops, and the language of a total grammar is $L(G)=\{x:\operatorname{Rec}_G(S,x)=x\}$, the words on which the start symbol succeeds consuming the whole input (“complete match”); $\mathsf{PEG}$ is the class of such languages [12, Definition 4]. Order is semantic: with $S\leftarrow a/ab$, the input $ab$ is not recognized, because the choice commits to $a$ and leaves $b$ unconsumed [7, p. 7]. PEGs recognize some non-context-free languages, such as $\{a^nb^nc^n\}$ [12, p. 3], while LMR conjectured that the context-free language $\mathsf{EPAL}_2$ has no PEG [12, Conjecture 7]; the comparison of the two classes is not syntactic and goes through the machine model below.

2.3 Scaffolding automata

The reversal is not an artifact: the automaton commits letter by letter from the left, and LMR’s grammar re-enacts its run from the other end. This paper uses the theorem only in the labelled example of Section 9; none of its own results depends on it.

2.4 From automata to histories

Everything from Section 3 to Section 8 concerns the graphs that scaffolding automata can build, not any particular automaton. A run of an automaton on an input word writes down, at each step, one row: the label chosen and the $d$ descriptors chosen. Conversely, any sequence of rows is a legal construction (an invalid port word simply yields a missing edge), whether or not some finite control would produce it. We therefore study all finite row sequences, called histories, and ask about their behavior as seen by an observer at the top. The finite control, the input word, the distance bound on what the control may read, and acceptance play no role until Section 9. In particular the rewrites of Sections 6–8 are mathematical operations on histories; we do not claim that an automaton could perform them while running (Section 6.3 says this once more where it matters).

3 Histories, unfoldings, and observations

3.1 The finite row alphabet

Fix a degree $d\geq1$, a distance $k\geq0$, and a finite working alphabet $\Gamma$. Write $[d]=\{0,\ldots,d-1\}$ for the port alphabet and $$\Delta_{d,k} = \{\mathsf{MISSING},\mathsf{SELF}\}\cup[d]^{\leq k}$$ for the set of descriptors.

The set of histories is the free monoid $\mathsf{Row}_{d,k,\Gamma}^{*}$ as syntax. Appending a row is a total operation on evaluated histories because invalid paths have the defined missing outcome.

3.2 Port-word behavior

For a rooted evaluated scaffold $(S,t)$, following a port word from $t$ either reaches a node or runs into a missing port. Adjoin a value $\bot_{\mathrm e}$ for the latter. The behavioral unfolding of $(S,t)$ is the function $$\mathcal U_{S,t}:[d]^{*}\longrightarrow \Gamma\cup\{\mathsf{UNLABELLED},\bot_{\mathrm e}\}$$ that sends a valid word to the label of its endpoint (with $\mathsf{UNLABELLED}$ for the base) and an invalid word to $\bot_{\mathrm e}$. The unlabelled base is therefore observable and is not a missing edge. The unfolding is everything an observer at $t$ can learn by following ports and reading labels; it is what LMR’s transition function sees, restricted to words of length at most $k$.

Two rooted scaffolds are behaviorally equivalent, written $(S,t)\simeq(T,u)$, when their unfoldings agree. For a history $H$ of length $n$, let $$\operatorname{Fig}_j(H)=M(\mathcal U_{S_j,j})$$ denote the canonical minimal figure of its length-$j$ prefix, defined in Section 3.4. The strong trace and final observation are $$\operatorname{Tr}(H)=(\operatorname{Fig}_1(H),\ldots,\operatorname{Fig}_n(H)), \qquad \pi(H)=\operatorname{Fig}_n(H).$$

Strong equivalence implies final equivalence. The converse fails because a later row may make an earlier difference unreachable or behaviorally irrelevant.

3.3 Full abstraction

The first theorem says that the unfolding is the right notion of behavior: it is determined by finite observations, it is exactly bisimilarity, it is preserved by every common future, and any difference is eventually visible.

Here a bisimulation between two rooted scaffolds is a relation on nodes that relates the roots and, whenever it relates $x$ to $y$, requires that $x$ and $y$ have the same label and that for every port either both are missing or the targets are again related; two roots are bisimilar if some bisimulation relates them. “Unary” means that the continuation uses only one port of each new node; “distance two” means its descriptors have length at most $2$ (whatever the distance of the original scaffolds). “Distinguished” means: there is a single sequence of rows which, appended to either scaffold, produces tops whose depth-$2$ neighbourhoods differ, so that a finite control reading those neighbourhoods can accept one and reject the other.

3.4 Why coalgebra, and what a figure is

The reader who knows finite automata has met the idea of this subsection already. A language $L$ has, for each word $p$, a residual (or derivative) $p^{-1}L=\{w:pw\in L\}$; the language is regular exactly when it has finitely many residuals, and those residuals are the states of its minimal deterministic automaton [3, Def. 3.1, Thm. 4.3], [13]. Two states of any automaton are equivalent when they accept the same words, and merging equivalent states gives the minimal automaton. Coalgebra is the general form of this idea: a system is described by what can be observed at a state (here, a label) and which states are reached next (here, the port targets); two states are bisimilar when every observation and every successor behavior matches; the quotient by bisimilarity is the smallest system with the same behavior [15, §2, §5–6]. We use only this much of the theory, in the deterministic labelled-graph instance, and we prove the facts we need directly.

For a valid port word $p$, write $\mathcal U_p(w)=\mathcal U(pw)$ for the residual unfolding at $p$: what an observer sees after first walking along $p$. Let $\mathcal R(\mathcal U)$ be the finite set of distinct valid residual unfoldings. A map $f$ from the nodes of one rooted labelled port graph to those of another is a functional bisimulation if it sends root to root, preserves labels, and for every node $x$ and port $i$ either both $x$ and $f(x)$ lack port $i$ or $f(x.i)=f(x).i$. Two rooted labelled port graphs are isomorphic if there is a bijective functional bisimulation between them.

4 Chronological order and navigation

Write $x\preceq y$ when $x$ is reachable from $y$ by following ports, including $x=y$; since edges point to older nodes or to the node itself, $x\preceq y$ implies that $x$ was created no later than $y$, so later nodes sit above earlier ones. A finite port graph is weakly acyclic when its only directed cycles are self-loops. Its rooted component is a reachability chain when $\preceq$ is a total order there.

Part (2) is worth a pause: it says that, from the top, any two reachable nodes are comparable, one reachable from the other. The reason is that a new node can only point into the previous top’s reachable set, which is a chain by induction.

A transformation $f$ of a finite totally ordered set is regressive if $xf\le x$ for every $x$ (we write the action on the right). In a monoid $M$, Green’s relation $\mathcal R$ is defined by $s\,\mathcal R\,t$ iff $sM^1=tM^1$, i.e. $s=tu$ and $t=sv$ for some $u,v\in M^1$; $M$ is $\mathcal R$-trivial when every $\mathcal R$-class is a singleton [14, Ch. V §1, p. 99; Ch. X §1.3].

Boundary.  This is the algebra of historical port navigation inside one figure. It says nothing about the streamed input language, and nothing about the finite control’s routing of roots, which is a separate finite interface.

5 Static guarded folding

5.1 Rewriting vocabulary

A rewriting system on a set is a binary relation $\to$ (“one step”). An object is irreducible, or a normal form, if no step applies to it. The system is terminating if there is no infinite sequence of steps, and confluent if whenever an object rewrites (in zero or more steps) to two objects, those two rewrite to a common object. A terminating confluent system gives every object exactly one normal form, and two objects are related by the equivalence generated by $\to$ exactly when they have the same normal form; this is the Church–Rosser property. We use these words in exactly this sense.

5.2 Guarded folds

Let $G$ be a finite deterministic labelled partial port graph and let $E$ be a bisimulation equivalence already imposed on it (an equivalence relation that is a bisimulation). Work in the quotient $G/E$, whose states are the classes and whose ports are well defined because $E$ is a bisimulation.

The last case is the guarded recursive clause. It permits self-reference at either member of the pair but no larger unresolved cycle.

This theorem contains the usual bottom-up acyclic merge [5, §2] as a special case. The extra local case is a self-recursive pair. Static normalization alone, however, may remove a physical state and therefore does not yet define a time-respecting rewrite of construction histories: the next section asks which rewrites of the rows realize it.

6 The causal presentation calculus

6.1 Strong equivalence and semantic sewing

A semantic step replacement changes one row over a fixed preceding prefix when the two possible fresh roots are behaviorally equivalent.

So there is no semantic obstruction: strongly equivalent histories are always connected by row replacements. The real problem is locality: the side condition “the two fresh roots are behaviorally equivalent” is a global statement about unfoldings, and we want a fixed family of moves each of which is justified by looking at a bounded piece of the scaffold.

6.2 One-state extensions

Let $Q$ be a behaviorally reduced old live figure (the reachable part of the old scaffold, assumed to have no two bisimilar nodes). It is convenient to describe a new row not by descriptors but by what its ports reach: a new row has the guarded one-variable form $$R=(a;t_0,\ldots,t_{d-1}), \qquad t_i\in Q\cup\{X,\bot_{\mathrm e}\},$$ where $X$ denotes the fresh root itself. We say the fresh root presents a behavior, namely its unfolding; it presents an old residual $q\in Q$ if its unfolding equals that of $q$.

6.3 The two primitive strong moves

Fix the total order $$\mathsf{MISSING}<\mathsf{SELF}<p \qquad(p\in[d]^{\leq k})$$ on descriptors, where port words are ordered by length and then lexicographically (so $\epsilon$ is the least port word), and order rows with the same label by comparing descriptor tuples position by position.

The simultaneous recursive part of $U$ is absorption $A$; its remaining changes are endpoint detours. The guard is physical and bounded: it names $q$ within the observed scaffold and inspects its fixed port tuple.

These are mathematical graph-local rewrites with explicit endpoint-equality certificates. The calculus does not assert that an LMR automaton can discover or execute a normalizing move from finite control, nor that the move occupies a bounded contiguous interval in the chronological row word.

6.4 SELF-eager prefixes

Call a canonical history SELF-eager when it uses $\mathsf{SELF}$ at every available self-loop coordinate and least names elsewhere; by the order fixed above, this is the same as being the least row at every step.

7 Final observation and replay support

Final equivalence forgets intermediate figures. A row that is unreachable in the final rooted graph can nevertheless have been queried while a later descriptor was evaluated: in the worked history $E$, node $2$ is not reachable from node $3$, but node $3$’s descriptor $0$ was evaluated by reading node $2$’s port. Ordinary graph garbage (unreachable nodes) is therefore too small a notion of “irrelevant data”; the right notion follows the evaluation.

We call the descriptor $\delta_{t,i}$ written in row $t$ a port cell and the label $a_t$ a label cell; these are the syntactic coordinates of a history. Evaluating a port cell that holds a port word $p$ from the old top queries the port cells of the nodes it passes through, including the one at which an invalid path fails.

The last sentence is a statement about sequences of garbage moves, of the kind Remark 6.9 calls path-level: form the graph whose vertices are the histories of the fibre and whose edges are single-coordinate changes, glue in a two-dimensional face for every triangle and every square named in the theorem, and the claim is that every closed loop of moves can be contracted across those faces—any two ways of making the same garbage change are related by the displayed elementary identities.

7.1 A noncommuting boundary

Let $S$ denote strong normalization (Theorem 6.8) and let $J$ (“junking”) choose least values outside causal support. Both preserve the final figure, but in general $$S\circ J\ne J\circ S.$$ An absorption can move a repeated residual to a newer physical carrier. Junking first may erase the label needed to perform that absorption; absorbing first makes the older carrier garbage. Thus the two normalizers can reach distinct common fixed points with one final figure already in the unary distance-one three-row fragment.

Concretely, take the worked history $E=(1;\mathsf{SELF})(1;\epsilon)(0;0)$.

Both final roots are labelled $0$ and point to a $1$-labelled self-loop, but $E_{SJ}$ and $E_{JS}$ are distinct and irreducible under both normalizers.

Boundary.  Object-level confluence for strong traces plus cubical coherence inside each garbage fibre does not present their join. The missing operation changes which chronological node carries a final residual and therefore changes the support boundary itself.

8 Two calibrated sewing theorems

This section does not assert a complete final-equivalence calculus at arbitrary degree and distance. It proves one local two-row theorem and one global unary theorem. Their different hypotheses show where the remaining problem lies. “Sewing” is used literally: given two histories with the same final figure, we want a sequence of local moves that stitches one into the other while every move preserves the final figure.

8.1 Unexposed acyclic two-row factorizations

Fix a behaviorally reduced old prefix with top $q$, append one node $r$ (the router), then one more node $z$ (the consumer). The router’s ports are its slots. A consumer port whose descriptor is a nonempty port word is a path demand; its first letter $i$ is its selector, naming router slot $i$. Assume no consumer port points to $r$ by the empty descriptor. Whenever a consumer word begins with router slot $i$, assume that slot contains an old-prefix path $\alpha_i$, not $\mathsf{SELF}$ or missing. Thus a consumer word $i\beta$ reaches $$q_{\alpha_i\beta},$$ the node reached from $q$ by the composite word $\alpha_i\beta$. Call such a block unexposed (the consumer does not point at the router itself) and acyclic (the used slots point into the past). Because every consumer port points into the old prefix, the router $r$ is unreachable from $z$ and hence from every later top: no later row can see or query $r$. Consequently $r$’s label and its unused slots are outside causal support, while a slot used by some consumer demand is queried and supported.

Three final-only moves are useful.

1. A routing crossing injectively reassigns used router slots and changes each first selector to follow the reassignment.

2. A cut slide moves one letter between $\alpha_i$ and $\beta$ when both bounded descriptors remain legal.

3. A dedicated relation exchange changes $(\alpha,\beta)$ to $(\alpha',\beta')$ in a slot selected by exactly one consumer port, under the guard $q_{\alpha\beta}=q_{\alpha'\beta'}$.

The first two refactor a fixed composite word. The third uses a relation in the pointed old navigation action and is the move that crosses between different words with one old endpoint.

Here “the same final old residual behavior” means that the nodes reached in the old prefix by corresponding demands have equal unfoldings, and “continuation-aware” records that a routing crossing rewrites the consumer’s selectors together with the router’s slots; in the present setting no later row can reach the router, so the common suffix is literally unchanged.

8.2 The unary whole space

Now set $d=k=1$. Every descriptor is one of $$\mathsf{MISSING},\qquad \mathsf{SELF},\qquad\epsilon,\qquad 0.$$ Each state of the final figure is represented by at least one physical node; a node whose residual is a state of the final figure and which is reachable from the final top is a carrier of that state. After absorbing repeated live presentations of a terminal recursive residual (a self-looping final state carried by several consecutive nodes each pointing to the previous one), the final live figure is a reduced chain, and each of its states has exactly one carrier. Rows between two consecutive carriers that are not themselves carriers are relay rows: they are not final-reachable, but their port cells pass the lower carrier upward to the next one.

A temporal carrier slide exchanges the adjacent descriptor patterns $$(\epsilon,0)\quad\longleftrightarrow\quad(0,\epsilon)$$ at rows $(t,t+1)$, provided rows $t-1$ and $t$ carry the same label. The endpoint calculation is literal. On the left, row $t$ points to row $t-1$ and row $t+1$ reaches row $t-1$ through row $t$’s port, so row $t-1$ carries the residual and row $t$ is a relay. On the right, row $t$ points to row $t-1$’s target and row $t+1$ points to row $t$; since rows $t-1$ and $t$ have the same label and now the same target, row $t$ carries the residual that row $t-1$ carried, and row $t-1$ has become garbage. The final figure is unchanged although the intermediate figure and the support carrier have changed.

“Right-packed” means that the carriers of the final chain occupy the latest possible consecutive rows, and everything below them is in a canonical form.

8.3 A path-level quotient

In the unary theorem, call two histories of one final fibre chamber-equivalent if they are connected by strong and garbage moves alone; a chamber is a class. The remaining coordinates of a chamber are the creation times $t_1<\cdots<t_m$ of the essential residual carriers, omitting the arbitrary physical carrier of a terminal $\mathsf{SELF}$ residual. Temporal slides move one carrier into one adjacent vacant time. The set of increasing carrier tuples is smaller than the unrestricted set of $m$-subsets of $\{1,\ldots,n\}$: the final root is always carried by the final node, so $t_m=n$. If the reduced chain has an ordinary missing or base terminal, put $r=m-1$ and $c=n-m$. Then $$1\le t_1<\cdots<t_{m-1}<t_m=n, \qquad \lambda_i=t_i-i,$$ and $0\le\lambda_1\le\cdots\le\lambda_r\le c$. These row lengths are the order ideals of the rectangle poset $[r]\times[c]$. If the terminal is recursive, its arbitrary physical $\mathsf{SELF}$ carrier is omitted. The pure recursive case $m=0$ is a singleton; for $m\ge1$, time $1$ is reserved below the first retained finite carrier, so $r=m-1$, $c=n-m-1$, and $\lambda_i=t_i-i-1$. This gives the order ideals of $[m-1]\times[n-m-1]$.

For a finite poset $P$, Ardila, Owen, and Sullivant construct a cube complex $X(P)$ whose vertices are order ideals and whose cubes remove arbitrary subsets of the maximal elements of one ideal; their general poset-with- inconsistent-pairs theorem makes $X(P)$ a rooted CAT(0) cube complex [1, Definition 2.3 and Theorem 2.5].

Boundary.  Proposition 8.5 is path-level coherence only after collapsing each strong/garbage chamber. Theorem 7.5 gives path coherence inside a garbage fibre. A finite elementary presentation of all mixed strong, garbage, and temporal derivations is not proved here.

9 Feedback, receipts, and a repaired allocation model

The preceding calculus was developed intrinsically. A direct palindrome construction supplies a deliberately hostile application because it forces a fresh feedback edge. Everything proved in this section is proved here; the palindrome construction itself is described only as far as the reader needs to see the knot, and its theorems are not assumed (Section 9.4).

9.1 The receipt knot

Consider a recognizer for $\mathsf{EPAL}_2=\{ww^R\}$ that keeps, for the input read so far, its longest even-palindromic suffix and a persistent sequence (“rope”) describing the letters to the left of that suffix. Whenever the recognizer discovers a new palindrome, it creates a fresh record for that occurrence; and because old records can never be modified, it must store in the fresh record everything a later step may need, including a fresh rope. The companion paper [9] argues that the last cell of that fresh rope must hold a typed receipt—a pointer—to the fresh record itself, so that when that cell is later reached the recognizer can find the record without a search. Thus the same input step contains the logical cycle $$\text{fresh record}\longrightarrow\text{fresh rope}\longrightarrow \text{terminal cell}\longrightarrow\text{fresh record}.$$

An earlier internal version of the allocation model (numbered PC-83 in the project’s records) allowed a fresh field to name only an already constructed fresh slot, and its finite checker imposed the same topological order. Figure 5 is therefore a genuine proof defect in that version: the claimed source transition was outside its own model. The rest of this section is the repair, stated for arbitrary bounded record programs.

9.2 Bounded simultaneous record transducers

The last clause permits self, forward, and mutual fresh references. The batch is a finite labelled graph specified all at once. Three small batches show what is allowed: a self-loop (one slot pointing to itself), a forward reference (slot $0$ pointing to slot $1$), and a mutual cycle (slots $0$ and $1$ pointing to each other).

9.3 Staging a strict persistent sequence

The compiler solves the target representation problem but not the source evaluation problem. A cycle is safe only if the program can choose its allocation skeleton without following the fresh feedback edge. A data structure is persistent when old versions survive updates [6, §1], and purely functional in Kaplan and Tarjan’s strict sense when built only from the LISP primitives $\mathsf{car}$, $\mathsf{cons}$, $\mathsf{cdr}$ (pair construction and projection), with memoization excluded [11, p. 578, footnote 1].

Kaplan and Tarjan’s Theorem 5.1 gives worst-case constant-time push, pop, inject, and catenation for regular catenable steques in their strict purely functional model [11, p. 592]. It does not itself state the stronger conjunction needed by Theorem 9.4: a concrete finite constructor program, base-element opacity, a uniform fresh-allocation bound, and a uniform old-address-depth bound. Those are separate applicability obligations, not consequences silently imported from the asymptotic theorem.

9.4 The conditional application

What this does and does not say.  Proposition 9.5 repairs the allocation seam in general. It does not assert that any particular program satisfies its hypotheses; that is a separate proof obligation for each application.

10 Open boundaries

The proved general object is strong-trace equivalence. The broader program begins where final observation forgets that trace.

1. Unrestricted final presentation. Determine whether a finite graph-local move family presents final behavioral equivalence at all fixed degrees and distances. In plain terms: is there, for every $d,k$, a finite list of local rewrites connecting any two histories with the same final figure? Dedicated relation exchange may be a primitive or may be derivable by refactoring older rows.

2. Elementary higher coherence. The strong normalizer gives one object normal form, garbage fibres are cubical, and unary carrier chambers form distributive lattices. A finite set of cells presenting all mixed derivations—elementary identities between sequences of moves of all three kinds—is open.

3. Support handoff. A temporal slide can transfer one visible label obligation across a causal cut. Classify its interactions (critical pairs) with detours and absorption.

4. Navigation monoids. Characterize which finitely generated submonoids of the regressive chain monoid occur at fixed degree, distance, and uniform finite control.

5. Functional sharing versus branching. Separate ordinary immutable record DAGs from unrestricted scaffold navigation first at the dynamic or observational level, before seeking a language separation.

6. Comparator theorem. Construct the precise structure-preserving translation, if one exists, from the guarded causal presentation calculus to an established cyclic term-graph rewriting system [2] or to the categorical presentation of term graphs [8]. Novelty should be judged only after that comparison.

11 Assurance, provenance, and nonclaims

The theorem proofs in this paper are ordinary written mathematical proofs. Executable enumeration is used separately to find counterexamples and corroborate finite instances. No proof assistant is used as a stronger label for the mathematics here.

The public package includes a theorem inventory, proof audit, source audit, finite audit code, and exact output. The finite audits enumerate bounded histories (for instance all unary distance-one histories up to a fixed length), search for split fibres, and check the displayed normalizers; their counts are recorded in the package. They corroborate; they are not the proofs.

What is inherited.

Coalgebraic minimization and functional bisimulation [15]; ordinary acyclic-state merging [5]; general cyclic term-graph fold/unfold and confluence [2]; the scaffold model and its PEG correspondence [12]; strict real-time catenable steques [11]. No unrestricted final-equivalence or finite higher-coherence theorem is claimed; the palindrome example is not a theorem of this paper; and at this review stage no novelty claim is made.

What the viewpoint contributed.

The separation in Figure 1 repeatedly changed the mathematical target: treating physical endpoint equality and behavioral equality as different observations produced the unfolding quotient and exposed pure aliases as presentation data; retaining every prefix figure produced a right-stable strong congruence and the detour/unroll normal form; forgetting prefixes only afterward exposed temporal carrier motion and causal support as final-observation coordinates; treating a receipt as a typed coordinate rather than a semantic existence assertion exposed the same-step allocation cycle; and moving from topological allocation to a simultaneous coordinate realization turned that apparent impossibility into ordinary $\mathsf{SELF}$ feedback with finite slot state. Each arrow of $$\text{presentation} \;\longrightarrow\; \text{exact dynamics} \;\longrightarrow\; \text{observation} \;\longrightarrow\; \text{change of representation}$$ is a theorem obligation. In particular, a universal graph embedding is not automatically a bounded coordinate realization, and final language equality does not imply equality of causal histories.

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 found the allocation defect of Section 9 in an internal draft before publication. Load-bearing external statements are cited with locators and source scope. A later source audit found that the Kaplan–Tarjan theorem had been asked to carry an unstated implementation bridge; the correction above keeps that bridge open rather than attributing it to the source. This paper and the companion paper [9] were developed contemporaneously; neither treats the other as established, and every theorem of this paper is proved from its own text and the cited literature.

12 Conclusion

Persistent scaffold computation has an intrinsic algebra before one asks which language a machine recognizes. Its generated behavioral figures are ordered residual systems. Guarded static folds collapse equivalent presentations; chronological detours and one $\mathsf{SELF}$-unroll lift that collapse to a convergent presentation of full strong traces. Final observation then reveals a second layer—causal support, garbage cubes, temporal carriers, and cross-cut sewing—whose unrestricted presentation remains open.

The receipt knot explains why this distinction matters computationally. The semantic record exists, but a topologically ordered presentation cannot build it. In a simultaneous scaffold coordinate system the same cycle is a finite batch of $\mathsf{SELF}$ edges with slot tags. That change of representation repairs the generic same-step allocation seam. The companion uses that compiler only under its complete Section 11.1 sequence contract; the implementation evidence leaves that premise open. More importantly, the generic construction exhibits the general principle: complexity can move between semantic structure, presentation dynamics, and observation without disappearing.

A Move and preservation table

B The central implication map

$$\begin{array}{c} \text{LMR row semantics}\\[2pt] \Downarrow\\ \text{future-context full abstraction}\\[2pt] \Downarrow\\ \text{minimal reachability-chain figures}\\[2pt] \Downarrow\\ \text{guarded static fold completeness}\\[2pt] \Downarrow\\ \text{one-state extension dichotomy}\\[2pt] \Downarrow\\ \text{convergent strong-trace presentation}\\[6pt] \searrow\hspace{26mm}\swarrow\\[-2pt] \text{causal-support sewing}\hspace{12mm} \text{simultaneous SELF feedback} \end{array}$$