\documentclass[11pt]{article}

\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{lmodern}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{booktabs,tabularx,array}
\usepackage{enumitem}
\usepackage{xcolor}
\usepackage{microtype}
\usepackage{fancyhdr}
\usepackage{graphicx}
\usepackage{tikz}
\usetikzlibrary{arrows.meta,positioning,fit,calc,decorations.pathreplacing}
\usepackage{hyperref}

\hypersetup{
  colorlinks=true,
  linkcolor=blue!55!black,
  citecolor=blue!55!black,
  urlcolor=blue!55!black,
  pdftitle={Persistent Scaffold Computation: Causal Presentations, Sewing, and Feedback},
  pdfauthor={Joshua Gay}
}
\urlstyle{same}
\setlist{nosep}
\setlength{\parskip}{0.45em}
\setlength{\parindent}{0pt}

\pagestyle{fancy}
\fancyhf{}
\fancyhead[L]{Persistent scaffold computation}
\fancyhead[R]{Draft 3, review stage}
\fancyfoot[C]{\thepage}
\renewcommand{\headrulewidth}{0.3pt}
\setlength{\headheight}{14pt}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{example}[theorem]{Example}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\newenvironment{intuition}
  {\begin{quote}\small\textbf{Working picture.}\ }{\end{quote}}
\newenvironment{boundary}
  {\begin{quote}\small\textbf{Boundary.}\ }{\end{quote}}
\newenvironment{scope}
  {\begin{quote}\small\textbf{What this does and does not say.}\ }{\end{quote}}

\newcommand{\SELF}{\mathsf{SELF}}
\newcommand{\MISS}{\mathsf{MISSING}}
\newcommand{\Fig}{\operatorname{Fig}}
\newcommand{\Tr}{\operatorname{Tr}}
\newcommand{\NF}{\operatorname{NF}}
\newcommand{\SA}{\mathsf{SA}}
\newcommand{\PEG}{\mathsf{PEG}}
\newcommand{\EPAL}{\mathsf{EPAL}_2}
\newcommand{\Rtriv}{\mathcal R}
\newcommand{\eps}{\epsilon}
\newcommand{\Ucal}{\mathcal U}
\newcommand{\Gcal}{\mathcal G}
\newcommand{\ports}{[d]}
\newcommand{\Rec}{\operatorname{Rec}}
\newcommand{\FAIL}{\mathsf{FAIL}}
\newcommand{\missing}{\varnothing}

\tikzset{
  box/.style={draw=black!65, rounded corners=2pt, align=center,
    inner sep=5pt, fill=black!3, font=\small},
  emphbox/.style={box, draw=black, fill=black!8},
  snode/.style={draw=black!80, circle, minimum size=7mm, inner sep=1pt,
    fill=white, font=\small},
  flow/.style={-{Latex[length=2mm]}, semithick, draw=black!75},
  dashedflow/.style={flow, dashed},
  every picture/.style={line cap=round, line join=round}
}

\title{\textbf{Persistent Scaffold Computation:\\
Causal Presentations, Sewing, and Feedback}}
\author{Joshua Gay\\\small FPRD Lab, Insight Forge}
\date{Draft 3, 23 August 2026}

\begin{document}
\maketitle

\begin{abstract}
Scaffolding automata were introduced by Loff, Moreira, and Reis to
characterize the languages of parsing expression grammars: a scaffolding
automaton reads its input once and, at every letter, appends one new node of
bounded degree to a permanent graph, choosing the new node's edges among the
nodes within a fixed distance of the previous one.  Their language-theoretic
power is known.  This paper studies the graphs themselves: what a
construction history builds, what an observer standing at the newest node can
learn by following edges, when two different histories are indistinguishable
to such an observer, and---the main question---which \emph{local} rewrites of
a history connect it to every history that is indistinguishable from it.

We separate four things that are easy to conflate: the physical history
(which nodes exist and which edges they carry), its \emph{behavioral figure}
at each moment (the smallest graph with the same observations), the
\emph{strong trace} (the sequence of all those figures), and the \emph{final
figure} alone.  For fixed degree and distance we prove that the reachable
part of a history is always totally ordered by reachability; that on such
graphs a simple pairwise \emph{guarded fold} rule computes the behavioral
figure; and, as the main theorem, that two rewrites---renaming an edge by a
shorter path to the same node, and replacing a pointer to an old self-looping
node by the new node's own self-reference---form a terminating and confluent
presentation of strong-trace equivalence, with a linear bound on the number
of rewrites.  Equality of final figures only is a harder problem, because a
later node can make an earlier difference invisible; we define the
\emph{causal support} that a final figure actually depends on, prove that the
remaining data are freely variable, and prove two exact results in restricted
settings (a two-row theorem relative to a fixed past, and a complete theorem
for degree one and distance one).  We say precisely what is not proved.

Finally we use the calculus on a demanding application: a direct
even-palindrome recognizer needs a fresh record to own a fresh sequence whose
last cell points back to that record, a same-step cycle that no ordinary
allocation discipline can build.  We prove that every bounded one-step update
with an arbitrary finite graph of fresh records compiles into a scaffolding
automaton, and explain why the cycle is harmless.  Palindromes are a stress
test of the calculus, not its subject.  The paper is self-contained: it
defines grammars, PEGs, scaffolding automata, bisimulation, and every rewrite
it uses, and it makes no novelty claim for the established coalgebraic,
automata-minimization, or term-graph ideas it builds on.
\end{abstract}

\tableofcontents

\section{From a finite presentation to a history algebra}
\label{sec:intro}

\subsection{The machine and the question}

Loff, Moreira, and Reis (LMR) introduced scaffolding automata as a machine
model for parsing expression grammars \cite{LMR2020}; Section~\ref{sec:background}
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 \cite[Theorem~16]{LMR2020}.

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 \emph{behavioral figure};
and at the end there is a \emph{final figure}.  Those are different
quotients of the same history, and the paper's question is:

\begin{quote}
\emph{When two finite construction histories generate the same behavior,
which local fold, unfold, routing, erasure, and feedback moves connect
them?}
\end{quote}

\begin{figure}[ht]
\centering
\begin{tikzpicture}[node distance=10mm and 13mm]
  \node[box] (rows) {finite row\\presentation};
  \node[box, right=of rows] (hist) {chronological\\physical history};
  \node[emphbox, right=of hist] (trace) {strong trace\\of figures};
  \node[box, right=of trace] (final) {final\\figure};
  \node[box, right=of final] (lang) {accept/reject\\observation};
  \draw[flow] (rows) -- node[above,font=\tiny]{evaluate} (hist);
  \draw[flow] (hist) -- node[above,font=\tiny]{quotient} (trace);
  \draw[flow] (trace) -- node[above,font=\tiny]{forget} (final);
  \draw[flow] (final) -- node[above,font=\tiny]{readout} (lang);
\end{tikzpicture}
\caption{The observation ladder.  A \emph{row} is one construction step
written down (Definition~\ref{def:row}); a \emph{history} is a sequence of
rows; its \emph{physical history} is the graph it builds; the \emph{figure}
at a time is the smallest graph an observer at the top cannot distinguish
from the real one; the \emph{strong trace} keeps every figure and the
\emph{final figure} only the last.  Every arrow can identify presentations.
No reverse implication is automatic.}
\label{fig:ladder}
\end{figure}

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~\ref{thm:causal-nf}).  Equality of only the final figure is harder
because it forgets intermediate behavior; we prove what we can
(Section~\ref{sec:final}--\ref{sec:sewing}) and state exactly what remains
open (Section~\ref{sec:open}).

\subsection{In what sense this is an ``algebra''}

We call the system of histories, behavioral equivalences, and rewrites an
\emph{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~\ref{sec:histories}), the transformation
monoid of port navigation and its $\Rtriv$-triviality
(Corollary~\ref{cor:rtrivial}), and the rewriting system with its normal
forms (Theorem~\ref{thm:causal-nf}).  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~\ref{sec:open}).

\subsection{What is new here, and what is inherited}

The paper leans on three established theories and does not rename them.
\emph{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 \cite[\S2, \S5--6]{Rutten2000}; the familiar
instance is the minimal deterministic automaton obtained from the residuals
(derivatives) of a language \cite{Brzozowski1964,Nerode1958}.  Bottom-up
merging of equivalent states and incremental minimization of acyclic
deterministic automata are established \cite[\S2]{DaciukEtAl2000}.  Cyclic
term graphs, their unwinding into infinite trees, copying, hidden nodes, and
confluence have a substantial theory \cite{AriolaKlop1996}.  Section~\ref{sec:assurance}
lists what is inherited from each.

The target here is the intersection of four restrictions that none of those
theories imposes together:
\begin{enumerate}
  \item one immutable layer is appended per input symbol;
  \item every old address is read from the preceding top within one fixed
        radius;
  \item a \emph{strong} move must preserve the figure after every prefix; and
  \item soundness must survive every common future continuation.
\end{enumerate}
The resulting local rules live in the generated scaffold graph.  They need not
be bounded contiguous substring rules in the linear word of rows.

\subsection{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 \emph{presentation} that generates an internal recognition
\emph{dynamic}, and the accepted language is treated as one
\emph{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~\ref{sec:assurance} states
plainly what was checked and by whom.  In this paper the viewpoint has a
concrete form, Figure~\ref{fig:ladder}: 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.

\subsection{How to read this paper}

Section~\ref{sec:background} 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 \emph{arbitrary} construction
histories, which is where this paper's objects begin.
Section~\ref{sec:histories} defines histories, unfoldings, figures, and the
two equivalences, with one worked history that recurs throughout.
Sections~\ref{sec:chain}--\ref{sec:calculus} develop the strong-trace
calculus: the chain theorem, guarded folds, and the two rewrites with their
normal form.  Sections~\ref{sec:final}--\ref{sec:sewing} treat final
observation.  Section~\ref{sec:feedback} gives the feedback application.
Sections~\ref{sec:open}--\ref{sec:assurance} state open problems, what is
inherited, and how the work was produced.  Every proof states its strategy
first; every example says what generalizes.

\section{Background}
\label{sec:background}

\subsection{Words and languages}

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

\subsection{Context-free grammars and parsing expression grammars}

A \emph{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 \cite[pp.~120--122]{ChomskySchutzenberger1963}; it \emph{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\eps$
generates the even-length binary palindromes $\EPAL=\{ww^R\}$.  The reading
is existential: a word is in the language if \emph{some} derivation produces
it.

A \emph{parsing expression grammar} (PEG) \cite[\S3]{Ford2004} uses similar
rule shapes with an operational meaning.  Expressions are built from
letters, non-terminals, $\varepsilon$, and $\FAIL$ by sequence $e_1e_2$,
\emph{ordered choice} $e_1/e_2$, and the predicates $!e$ and $\&e$; each
non-terminal $A$ has one rule $A\leftarrow R(A)$.  Recognition
$\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 \emph{commits to it if it succeeds}, trying
$e_2$ only if $e_1$ fails; $!e$ succeeds (consuming nothing) exactly when $e$
fails \cite[Definition~3, Algorithm~1]{LMR2020}.  The procedure is
deterministic.  A grammar is \emph{total} if recognition never loops, and
the language of a total grammar is
$L(G)=\{x:\Rec_G(S,x)=x\}$, the words on which the start symbol succeeds
consuming the \emph{whole} input (``complete match''); $\PEG$ is the class
of such languages \cite[Definition~4]{LMR2020}.  Order is semantic: with
$S\leftarrow a/ab$, the input $ab$ is not recognized, because the choice
commits to $a$ and leaves $b$ unconsumed \cite[p.~7]{Ford2004}.  PEGs
recognize some non-context-free languages, such as $\{a^nb^nc^n\}$
\cite[p.~3]{LMR2020}, while LMR conjectured that the context-free language
$\EPAL$ has no PEG \cite[Conjecture~7]{LMR2020}; the comparison of the two
classes is not syntactic and goes through the machine model below.

\subsection{Scaffolding automata}
\label{sec:scaffold}

\begin{definition}[scaffold {\cite[Definitions~10--11]{LMR2020}}]
\label{def:scaffold}
Let $d\ge1$ and let $\Gamma$ be a finite alphabet.  A $(d,\Gamma)$-scaffold
with top $t$ has nodes $0,1,\ldots,t$; a label $L(v)\in\Gamma\cup\{\missing\}$
for each node, with $L(0)=\missing$ (the \emph{base} is unlabelled); and for
each node $v$ and each \emph{port} $i\in\ports=\{0,\ldots,d-1\}$ a target
$e_v(i)\in\{0,\ldots,v\}\cup\{\missing\}$: every edge points to an older node
or to the node itself, or is missing.  A \emph{port word} $p\in\ports^*$ is
followed from a node by taking port $p_1$, then port $p_2$ of the node
reached, and so on; it is \emph{valid} from $v$ if no missing port is met.
The $k$-\emph{neighbourhood} $N_k(v)$ is the labelled tree of depth $k$
obtained by unfolding ports from $v$; it records labels and missing ports,
not node numbers.
\end{definition}

\begin{definition}[scaffolding automaton {\cite[Definitions~12--15]{LMR2020}}]
\label{def:automaton}
A scaffolding automaton $A=\langle\Sigma,d,\Gamma,k,Q,\delta,q_0,F\rangle$
has an input alphabet, a degree $d$, a working alphabet $\Gamma$, a
\emph{distance} $k\ge0$, a finite control $(Q,q_0,F)$, and a transition
function $\delta:Q\times\Sigma\times N_k(d,\Gamma)\to
Q\times\Gamma\times(\ports^{\le k}\cup\{\SELF,\missing\})^d$.  Reading a
letter in state $q$ with top $t$, it computes
$(q',\gamma,p_0,\ldots,p_{d-1})=\delta(q,\sigma,N_k(t))$ and appends node
$t+1$ with label $\gamma$ and ports: the endpoint of $p_i$ followed from $t$
if $p_i$ is a valid port word; missing if $p_i=\missing$ or invalid; the new
node $t+1$ itself if $p_i=\SELF$.  It accepts a word if the state after the
last letter is in $F$.
\end{definition}

\begin{figure}[ht]
\centering
\begin{tikzpicture}[node distance=14mm]
  \node[snode, fill=black!8] (n0) {$0$};
  \node[snode, right=of n0] (n1) {$1{:}a$};
  \node[snode, right=of n1] (n2) {$2{:}b$};
  \node[snode, right=of n2] (n3) {$3{:}a$};
  \draw[flow] (n1) -- node[above,font=\scriptsize]{$0$} (n0);
  \draw[flow] (n2) -- node[above,font=\scriptsize]{$0$} (n1);
  \draw[flow, bend left=35] (n2) to node[below,font=\scriptsize]{$1$} (n0);
  \draw[flow, bend right=35] (n3) to node[above,font=\scriptsize]{$1$} (n1);
  \draw[flow] (n3) to[out=60,in=0,looseness=6] node[right,font=\scriptsize]{$0$} (n3);
\end{tikzpicture}
\caption{A scaffold of degree $2$ after three steps, built by the rows
$(a;\eps,\MISS)$, $(b;\eps,0)$, $(a;\SELF,0)$ in the notation of
Definition~\ref{def:row}: node $1$ points to the base; node $2$ points to
node $1$ (the old top, descriptor $\eps$) and, via port word $0$ from node
$1$, to the base; node $3$ points to itself and, via port word $0$ from
node $2$, to node $1$.  An observer at node $3$ who follows ports sees
labels $a$, then $a$ again forever along port $0$; it cannot see that the
node is the same each time.}
\label{fig:scaffold-example}
\end{figure}

\begin{theorem}[Loff--Moreira--Reis {\cite[Theorem~16, p.~21]{LMR2020}}]
\label{thm:lmr}
A language $L$ is in $\PEG$ if and only if $L^R$ is decided by some
scaffolding automaton.
\end{theorem}

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~\ref{sec:feedback};
none of its own results depends on it.

\subsection{From automata to histories}
\label{sec:automata-to-histories}

Everything from Section~\ref{sec:histories} to Section~\ref{sec:sewing}
concerns the \emph{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 \emph{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
\emph{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 \emph{read}, and acceptance play no role until
Section~\ref{sec:feedback}.  In particular the rewrites of
Sections~\ref{sec:calculus}--\ref{sec:sewing} are mathematical operations on
histories; we do not claim that an automaton could perform them while
running (Section~\ref{sec:moves} says this once more where it matters).

\section{Histories, unfoldings, and observations}
\label{sec:histories}

\subsection{The finite row alphabet}

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

\begin{definition}[row, history]
\label{def:row}
A \emph{row} is an element of $\mathsf{Row}_{d,k,\Gamma}=\Gamma\times\Delta_{d,k}^{d}$:
one label and one descriptor per port.  A \emph{history} is a finite
sequence of rows.  The empty word $\eps\in\ports^{\leq k}$ is a valid
descriptor: it names the preceding top.
\end{definition}

\begin{definition}[Evaluation]
\label{def:evaluation}
A history
\[
  H=(a_t;\delta_{t,0},\ldots,\delta_{t,d-1})_{t=1}^{n}
\]
is evaluated from an unlabelled edgeless base node $0$.  At time $t$, append
node $t$ with label $a_t$.  Its port $i$ is missing if
$\delta_{t,i}=\MISS$, points to $t$ if $\delta_{t,i}=\SELF$, and otherwise
points to the endpoint obtained by following $\delta_{t,i}$ from node $t-1$ in
the old scaffold.  An invalid path gives a missing edge.  We write $S_j$ for
the scaffold after the first $j$ rows.
\end{definition}

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.

\begin{example}[a worked history]
\label{ex:worked}
Take $d=1$, $k=1$, $\Gamma=\{0,1\}$, so every descriptor is one of $\MISS$,
$\SELF$, $\eps$, $0$ (the only port word of length $1$).  The history
\[
  E=(1;\SELF)\;(1;\eps)\;(0;0)
\]
evaluates as follows (Figure~\ref{fig:worked}).  Row 1 creates node $1$ with
label $1$ and a self-loop.  Row 2 creates node $2$ with label $1$ pointing to
the old top, node $1$.  Row 3 creates node $3$ with label $0$ whose port
follows port word $0$ from node $2$: node $2$'s port leads to node $1$, so
node $3$ points to node $1$.  Node $2$ is not reachable from node $3$, yet
its port cell was \emph{consulted} when node $3$'s edge was evaluated; this
distinction drives Section~\ref{sec:final}.  What generalizes: every history
is evaluated this way, one row at a time, reading only the previous top's
surroundings.  What is incidental: the labels and the length.
\end{example}

\begin{figure}[ht]
\centering
\begin{tikzpicture}[node distance=14mm]
  \node[snode, fill=black!8] (n0) {$0$};
  \node[snode, right=of n0] (n1) {$1{:}1$};
  \node[snode, right=of n1] (n2) {$2{:}1$};
  \node[snode, right=of n2] (n3) {$3{:}0$};
  \draw[flow] (n1) to[out=60,in=120,looseness=6] (n1);
  \draw[flow] (n2) -- (n1);
  \draw[flow, bend left=35] (n3) to (n1);
\end{tikzpicture}
\caption{The worked history $E=(1;\SELF)(1;\eps)(0;0)$ evaluated.  From
node $3$ the observer sees label $0$, then $1$, then $1$ forever.}
\label{fig:worked}
\end{figure}

\subsection{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 \emph{behavioral unfolding} of
$(S,t)$ is the function
\[
  \Ucal_{S,t}:\ports^{*}\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 \emph{behaviorally equivalent}, written
$(S,t)\simeq(T,u)$, when their unfoldings agree.  For a history $H$ of
length $n$, let
\[
  \Fig_j(H)=M(\Ucal_{S_j,j})
\]
denote the canonical minimal figure of its length-$j$ prefix, defined in
Section~\ref{sec:figure}.  The \emph{strong trace} and \emph{final
observation} are
\[
  \Tr(H)=(\Fig_1(H),\ldots,\Fig_n(H)),
  \qquad
  \pi(H)=\Fig_n(H).
\]

\begin{definition}[Two congruences]
\label{def:congruences}
Equal-length histories are \emph{strongly equivalent}, $H\equiv_{\mathrm s}H'$,
when $\Tr(H)=\Tr(H')$.  They are \emph{finally equivalent},
$H\equiv_{\mathrm f}H'$, when $\pi(H)=\pi(H')$.
\end{definition}

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

\begin{example}
\label{ex:final-not-strong}
With $d=k=1$, the histories
\[
  (0;\MISS)\,(0;\MISS)\,(0;\MISS)
  \qquad\text{and}\qquad
  (1;0)\,(1;0)\,(0;0)
\]
have the same final figure---a single node labelled $0$ with a missing
port---because in the second history every descriptor $0$ follows a port
that is itself missing.  Their strong traces differ already at time $1$
  (labels $0$ versus $1$). Many histories share a final figure while their
strong traces differ; the displayed pair is the smallest fact used below.
\end{example}

\subsection{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.

\begin{theorem}[Future-context full abstraction]\label{thm:full-abstraction}
For rooted degree-$d$ scaffolds over one working alphabet:

\begin{enumerate}
  \item equal unfoldings, equality of every finite rooted neighborhood, and
        deterministic labelled bisimilarity are equivalent;
  \item unfolding equivalence is preserved by every common scaffold row and
        hence by every common continuation; and
  \item unequal unfoldings are distinguished after finitely many steps by a
        distance-two unary scaffold continuation.
\end{enumerate}
\end{theorem}

Here a \emph{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 \emph{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.

\begin{proof}
\emph{Strategy.}  (1) is a restatement; (2) is an induction on the query
word; (3) constructs a ``cursor'' that walks along a shortest distinguishing
port word, one letter per row.

The depth-$m$ neighborhood is exactly the restriction of the unfolding to
port words of length at most $m$, which proves the first equivalence.  The
relation ``same unfolding'' is a bisimulation, and conversely a bisimulation
forces equal unfoldings by induction on the word.

Suppose the old unfoldings agree and append the same row.  The observed
depth-$k$ neighborhoods agree.  For a query word starting at fresh port $i$,
a missing descriptor fails on both sides; a $\SELF$ descriptor returns to the
respective fresh root; and an old descriptor $p$ reduces the comparison to
$\Ucal_{S,t}(pw)=\Ucal_{T,u}(pw)$.  The fresh labels agree.  Induction on the
remaining query length proves equality of the new unfoldings.  Iterating proves
continuation stability.

For the converse, choose a shortest port word
$p_1\cdots p_m$ on which the unfoldings differ.  If $m=0$, the current labels
already differ.  Otherwise a unary tester stores a cursor in one port.  Its
first row points along $p_1$; at the next step the distance-two path through
the cursor and $p_2$ advances it; and so on.  All proper prefixes behave
identically by minimality.  The last neighborhood exposes the first label or
missing-edge difference, which finite control records in acceptance.
\end{proof}

\begin{corollary}\label{cor:right-congruence}
Both $\equiv_{\mathrm s}$ and $\equiv_{\mathrm f}$ are stable under a common
right suffix of rows.
\end{corollary}

\subsection{Why coalgebra, and what a figure is}
\label{sec:figure}

The reader who knows finite automata has met the idea of this subsection
already.  A language $L$ has, for each word $p$, a \emph{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 \cite[Def.~3.1, Thm.~4.3]{Brzozowski1964},
\cite{Nerode1958}.  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 \emph{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
\emph{bisimilar} when every observation and every successor behavior
matches; the quotient by bisimilarity is the smallest system with the same
behavior \cite[\S2, \S5--6]{Rutten2000}.  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 $\Ucal_p(w)=\Ucal(pw)$ for the
\emph{residual unfolding} at $p$: what an observer sees after first walking
along $p$.  Let $\mathcal R(\Ucal)$ 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 \emph{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 \emph{isomorphic} if there is a bijective functional
bisimulation between them.

\begin{theorem}[Minimal residual figure]\label{thm:minimal-figure}
Every finite rooted scaffold has a canonical finite behavioral figure
$M(\Ucal)$ whose states are $\mathcal R(\Ucal)$, whose root is
$\Ucal_{\eps}$, and whose port $i$ sends $\Ucal_p$ to $\Ucal_{pi}$ when
defined.  The physical reachable graph maps onto $M(\Ucal)$ by a surjective
functional bisimulation.  Two rooted scaffolds are behaviorally equivalent if
and only if their minimal figures are isomorphic.
\end{theorem}

\begin{proof}
Every residual is represented by a physical reachable node, so there are at
most as many residuals as nodes.  Residualization commutes with every port
($\Ucal_p=\Ucal_q$ implies $\Ucal_{pi}=\Ucal_{qi}$), which makes labels and
successors well defined and makes the node-to-residual map a functional
bisimulation.  Distinct residual functions have distinct unfoldings and cannot
be bisimilar.  The construction depends only on $\Ucal$, proving minimality
and uniqueness up to rooted labelled port-graph isomorphism.
\end{proof}

\begin{example}
For the worked history $E$ of Example~\ref{ex:worked}, the residuals from
node $3$ are: $\Ucal_\eps$ (label $0$, then $1$ forever) and
$\Ucal_0=\Ucal_{00}=\cdots$ (label $1$ forever).  The figure $\Fig_3(E)$ has
two states, a $0$-labelled root pointing to a $1$-labelled state with a
self-loop.  The physical node $2$ is not reachable and plays no part.
\end{example}

\begin{remark}
\label{rem:aliasing}
Physical aliasing is finer than behavior.  Two ports may point to one node in
one history and to two bisimilar nodes in another; their minimal figures still
agree.  Alias identity becomes observable only when a presentation explicitly
stores it in finite labels.
\end{remark}

\section{Chronological order and navigation}
\label{sec:chain}

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 \emph{above} earlier ones.  A finite port graph is \emph{weakly acyclic}
when its only directed cycles are self-loops.  Its rooted component is a
\emph{reachability chain} when $\preceq$ is a total order there.

\begin{theorem}[Generated-chain theorem]\label{thm:chain}
Let $S$ be a legally generated chronological scaffold with current top $t$.

\begin{enumerate}
  \item Its physical graph and its minimal figure are weakly acyclic.
  \item The nodes reachable from $t$, and the states of the minimal figure,
        are totally ordered by reachability.
  \item Conversely, every finite behaviorally reduced labelled rooted
        reachability-chain port graph, with an optional least unlabelled
        edgeless state, has an exact legal scaffold presentation at some finite
        distance.
\end{enumerate}
\end{theorem}

Part (2) is worth a pause: it says that, from the top, \emph{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.

\begin{proof}
A non-$\SELF$ edge of node $t$ reaches an older node, so creation time never
increases along a port path and can stay fixed only on a self-loop.  If the
behavioral quotient had a cycle through two classes, repeating a word around
the cycle from a physical representative would give an infinite path of
nonincreasing times.  It is eventually constant, so every later edge is one
physical self-loop and all classes on the alleged cycle coincide.

Let $R_j$ be the component reachable from the top after step $j$.  Every old
target of the new top is already in $R_{j-1}$, so
$R_j\setminus\{j\}\subseteq R_{j-1}$.  Induction makes $R_j$ a chain, and
quotienting preserves total comparability.

Conversely enumerate the desired states
$q_1\prec\cdots\prec q_m$.  When $q_j$ is appended, each strict successor is
some $q_i$ at or below $q_{j-1}$ and is therefore reached from $q_{j-1}$ by a
port word.  Use that word, $\SELF$ for self-loops, and missing for absent
edges.  A shortest simple word has length at most $j-2$, so one distance at
most $m-1$ realizes all rows.
\end{proof}

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

\begin{corollary}[Regressive navigation]\label{cor:rtrivial}
After adjoining a least missing sink to a generated minimal figure and
numbering its chain, every port acts regressively.  Its port-word transition
monoid is a submonoid of the full regressive transformation monoid and is
$\Rtriv$-trivial.
\end{corollary}

\begin{proof}
Each successor is at or below its source.  If transformations $f,g$ are
$\Rtriv$-related, write $f=gu$ and $g=fv$.  Pointwise regressiveness gives
$xf\leq xg$ and $xg\leq xf$ for every state $x$, hence $f=g$.
\end{proof}

\begin{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.
\end{boundary}

\section{Static guarded folding}
\label{sec:folding}

\subsection{Rewriting vocabulary}

A \emph{rewriting system} on a set is a binary relation $\to$ (``one
step'').  An object is \emph{irreducible}, or a \emph{normal form}, if no
step applies to it.  The system is \emph{terminating} if there is no
infinite sequence of steps, and \emph{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
\emph{Church--Rosser} property.  We use these words in exactly this sense.

\subsection{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.

\begin{definition}[Elementary guarded fold]
\label{def:fold}
Two distinct quotient states $x,y$ admit a guarded fold when their labels
agree and, at every port, the two successors are both missing, are the same
quotient state, or lie in $\{x,y\}$.  Equivalently, identifying $x$ and $y$
makes their one-step successor profiles equal.
\end{definition}

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

\begin{figure}[ht]
\centering
\begin{tikzpicture}[node distance=10mm and 18mm]
  \node[snode] (x) {$x{:}a$};
  \node[snode, right=of x] (y) {$y{:}a$};
  \node[snode, below right=8mm and 3mm of x] (z) {$z{:}b$};
  \draw[flow] (x) -- (z); \draw[flow] (y) -- (z);
  \draw[flow] (x) to[out=120,in=60,looseness=6] (x);
  \draw[flow] (y) -- (x);
  \node[below=3mm of z, font=\small, align=center] {foldable: port $0$ both to $z$,\\port $1$ within $\{x,y\}$};
  \node[snode, right=40mm of y] (u) {$u{:}a$};
  \node[snode, right=of u] (v) {$v{:}a$};
  \node[snode, below right=8mm and 3mm of u] (w) {$w{:}a$};
  \draw[flow] (u) -- (w); \draw[flow] (w) -- (v);
  \draw[flow] (v) to[out=120,in=60,looseness=6] (v);
  \node[below=3mm of w, font=\small, align=center] {$u,v$ bisimilar but not foldable:\\$u$'s successor $w\notin\{u,v\}$};
\end{tikzpicture}
\caption{Left: a guarded fold of $x$ and $y$ (degree $2$; port $0$ drawn
down, port $1$ drawn across).  Right (degree $1$): all three of $u,w,v$ are
bisimilar, but the pair $(u,v)$ fails the guard; the fold must proceed
through $(w,v)$ first, then $(u,[wv])$.}
\label{fig:fold}
\end{figure}

\begin{theorem}[Guarded folds generate bisimilarity]\label{thm:guarded-fold}
On every finite weakly acyclic deterministic labelled partial port graph,
the equivalence generated by elementary guarded folds is exactly the greatest
bisimulation equivalence.
\end{theorem}

\begin{proof}
\emph{Strategy.}  Soundness is immediate.  For completeness, find, in any
sound quotient that is not yet fully reduced, a bisimilar pair that satisfies
the guard: take a minimal unreduced class and look at its sinks.

Each fold is sound because corresponding successors become equal in the new
quotient.

Two facts keep the induction well posed.  First, the greatest bisimulation
quotient of a finite weakly acyclic graph is weakly acyclic: the argument of
Theorem~\ref{thm:chain}(1) applies verbatim with any topological numbering
in place of creation time.  Second, a guarded fold preserves weak
acyclicity: a new cycle through the folded class $[xy]$ would pass through a
state $z\notin\{x,y\}$ that is a successor of $x$ or $y$ and reaches $x$ or
$y$; since $x$ and $y$ have identical non-pair successors, $z$ is a successor
of both, so the old graph had a cycle $z\to\cdots\to y\to z$ of length at
least two, contradicting weak acyclicity.  Hence every sound quotient reached
by folds is weakly acyclic, and ``minimal in strict reachability'' below is
meaningful.

For completeness, suppose a sound quotient still has a nonsingleton greatest
bisimulation class.  Choose such a class $C$ minimal in strict reachability of
the behavioral quotient.  Every strict successor class below $C$ is already a
singleton.

The edges between distinct current states inside $C$ form a finite DAG.  If it
has two sinks $x,y$, an internal successor of either sink can only be its own
self-loop, while corresponding external successors are the same singleton;
therefore $x,y$ are guarded-foldable.  If it has one sink $x$, choose a
minimal state $y$ of $C\setminus\{x\}$.  Every strict internal successor of
$y$ is $x$, and every internal successor of $x$ is its self-loop.  External
successors are again equal, so $x,y$ are guarded-foldable.

Another sound fold is therefore available until the greatest bisimulation
quotient is reached.
\end{proof}

\begin{corollary}[Static normal form]\label{cor:static-nf}
Orient each guarded fold toward its quotient.  The system terminates and is
confluent up to rooted labelled port-graph isomorphism.  Its normal form is
the minimal residual figure.
\end{corollary}

\begin{proof}
Every fold reduces the state count.  An irreducible graph is behaviorally
reduced by Theorem~\ref{thm:guarded-fold}; every reduction preserves the
unfolding; and Theorem~\ref{thm:minimal-figure} gives one reduced figure up to
isomorphism.
\end{proof}

This theorem contains the usual bottom-up acyclic merge
\cite[\S2]{DaciukEtAl2000} 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
\emph{rows} realize it.

\section{The causal presentation calculus}
\label{sec:calculus}

\subsection{Strong equivalence and semantic sewing}

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

\begin{proposition}[Semantic causal sewing]\label{prop:semantic-sewing}
Two strongly equivalent length-$n$ histories are connected by at most $n$
semantic step replacements.
\end{proposition}

\begin{proof}
Align the rows from left to right.  Once the prefixes through $j-1$ are
literally equal, replaying the old $j$th row over that prefix preserves its
behavior by Theorem~\ref{thm:full-abstraction}; the target row has the same
$j$th figure by strong equivalence.  Replace it and continue.
\end{proof}

So there is no \emph{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.

\subsection{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 \emph{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
\emph{presents} a behavior, namely its unfolding; it presents an old
residual $q\in Q$ if its unfolding equals that of $q$.

\begin{lemma}[One-state extension dichotomy]\label{lem:extension}
Suppose two such fresh roots have the same behavior.

\begin{enumerate}
  \item If the behavior is not already a state of $Q$, their missing and
        $\SELF$ positions agree, and their old target agrees at every other
        port.
  \item If the behavior is an old state $q\in Q$, each row is a guarded
        unroll of $q$: it copies every missing and strict-successor port, while
        a self-loop of $q$ may target either $q$ or the fresh variable $X$.
\end{enumerate}
\end{lemma}

\begin{proof}
In the first case, a fresh $\SELF$ on one side and an old target $q$ on the
other would make the common fresh behavior equal to $q$, a contradiction.
Thus the $\SELF$ masks agree.  Corresponding old targets are bisimilar and are
therefore the same state of reduced $Q$; missing positions also agree.

In the second case, compare the fresh root with $q$.  A non-$\SELF$ target
must be the unique reduced successor of $q$.  A fresh $\SELF$ is possible
exactly where that successor is $q$ itself.  These conditions are also
sufficient: identity on $Q$ together with the fresh-root/$q$ pair is a
bisimulation.
\end{proof}

\subsection{The two primitive strong moves}
\label{sec:moves}

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

\begin{definition}[Endpoint detour $D$]
\label{def:detour}
Replace one old-top word by another bounded word with the same physical
endpoint.  All invalid words share the missing endpoint.  Orient the move
toward the least name of that endpoint.
\end{definition}

\begin{definition}[Literal guarded unroll $U$]
\label{def:unroll}
Let a fresh row point, at some port, to an old physical node $q$ that has a
self-loop at that port, and suppose the fresh root presents the residual of
$q$: its label equals $q$'s, and at every port its target is missing exactly
when $q$'s is, is the physical successor of $q$ where that successor is not
$q$, and is either $q$ or $\SELF$ where $q$ has a self-loop.  If at least one
such port points to the old $q$, replace all of them by $\SELF$ and choose
least endpoint names at the other ports.  Orient in that direction.
\end{definition}

The simultaneous recursive part of $U$ is \emph{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.

\begin{example}[the two moves on the worked history]
In $E=(1;\SELF)(1;\eps)(0;0)$, row 2 points to node $1$, which has a
self-loop and the same label, and node $2$'s unfolding equals node $1$'s;
so $U$ applies and rewrites row 2 to $(1;\SELF)$.  After that rewrite, row
3's descriptor $0$ is followed from the new node $2$, whose port is now a
self-loop, so the endpoint is node $2$; the least name for node $2$ from the
old top is $\eps$, and $D$ rewrites row 3 to $(0;\eps)$.  The result
$(1;\SELF)(1;\SELF)(0;\eps)$ has the same figure as $E$ at every time.  What
generalizes: an unroll can change the physical endpoints of later rows, and
detours then rename them.
\end{example}

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.

\subsection{SELF-eager prefixes}

Call a canonical history \emph{SELF-eager} when it uses $\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.

\begin{lemma}[Canonical history exists]\label{lem:canonical-exists}
Every realizable finite strong trace has a unique lexicographically least
history.  It is obtained from left to right by appending the least row that
realizes the next figure over the already chosen prefix.
\end{lemma}

\begin{proof}
Assume the canonical prefix through time $j-1$ has been chosen and take any
original realization of the full trace.  Its length-$(j-1)$ prefix has the same
rooted unfolding as the canonical prefix.  Replay the original $j$th row over
the canonical prefix.  Theorem~\ref{thm:full-abstraction} says that the new
root has the required $j$th figure, so the finite set of realizing rows is
nonempty and has a unique least element.  Induction constructs the history;
leastness at the first differing row proves uniqueness.
\end{proof}

\begin{lemma}[Reduced live prefixes]\label{lem:reduced-prefix}
Every root-reachable component at every prefix of a SELF-eager history is
behaviorally reduced.
\end{lemma}

\begin{proof}
Induct on prefix length.  If the fresh behavior is new, it adds one new
residual above a reduced old component.  If it repeats an old residual $q$,
Lemma~\ref{lem:extension} says that every strict successor lies below $q$ and
that only a self-loop coordinate can choose between old $q$ and fresh
$\SELF$.  SELF-eagerness chooses the fresh root.  It therefore reaches itself
and strict descendants but not the old physical $q$.  The fresh root replaces
$q$ as the unique live representative.
\end{proof}

\begin{theorem}[Convergent strong-trace presentation]\label{thm:causal-nf}
For fixed finite $d,k,\Gamma$, oriented endpoint detours and literal guarded
unrolls form a terminating confluent graph-local presentation of strong
equivalence.  Two histories have the same strong trace if and only if they
reduce to the same SELF-eager history.  A length-$n$ history normalizes in at
most $dn$ row moves when $U$ counts as one whole-row move.
\end{theorem}

\begin{proof}
\emph{Strategy.}  Soundness of each move; termination by a lexicographic
measure; then show that an irreducible history is the canonical one of
Lemma~\ref{lem:canonical-exists}, by induction from left to right.

Both moves are sound.  A detour preserves a physical endpoint.  For an
unroll, identity on the old prefix together with the fresh-root/$q$ pair is a
bisimulation.  Theorem~\ref{thm:full-abstraction} carries either replacement
through the unchanged suffix.

Lexicographically order the chronological descriptor word.  A detour
strictly decreases one path name.  An unroll replaces at least one old path by
smaller $\SELF$ and never increases an earlier descriptor.  Thus reduction
terminates.

Induct left to right through an irreducible history.  Its old prefix is already
SELF-eager and reduced by Lemma~\ref{lem:reduced-prefix}.  Compare the fresh
row with the least row supplied by Lemma~\ref{lem:canonical-exists} for the
same next figure.  If the residual is new,
Lemma~\ref{lem:extension} gives the same missing/$\SELF$ mask and the same old
residual targets.  Reducedness turns those targets into the same physical
nodes; any remaining difference is a detour redex.  If the residual repeats
old $q$, a path back to $q$ at a self-loop is an unroll redex, and a nonleast
path to any fixed strict successor is a detour redex.  Therefore an
irreducible row is exactly the SELF-eager least row.

Each strong-trace class has one irreducible history, so termination gives
confluence and completeness.
Normalizing from left to right, a new residual needs at most $d$ detours.  A
repeated residual needs at most $d$ detours or one whole-row unroll; because
$d\geq1$, the total is at most $dn$.
\end{proof}

\begin{remark}[What ``coherence'' means here]
\label{rem:coherence}
Theorem~\ref{thm:causal-nf} is object-level Church--Rosser coherence: equal
strong traces have one normal form, so any two reduction sequences from one
history end at the same place.  It does \emph{not} say that any two such
sequences are themselves related by a finite list of elementary identities
between sequences (``two-dimensional cells'').  We reserve the phrase
\emph{path-level coherence} for results that actually present those
relations between sequences of moves.
\end{remark}

\section{Final observation and replay support}
\label{sec:final}

Final equivalence forgets intermediate figures.  A row that is unreachable in
the final rooted graph can nevertheless have been \emph{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 \emph{port cell}
and the label $a_t$ a \emph{label cell}; these are the syntactic coordinates
of a history.  Evaluating a port cell that holds a port word $p$ from the old
top \emph{queries} the port cells of the nodes it passes through, including
the one at which an invalid path fails.

\begin{definition}[Causal endpoint support]
\label{def:support}
Let $R_H$ be the created nodes reachable from the final top.  Support every
label cell and every port cell of a node in $R_H$.  Whenever a supported port
cell was created by following an old-top path, support every older port cell
actually queried along that evaluation, including the cell at which an
invalid path fails.  Close backward to the least such set $C_H$.
\end{definition}

\begin{example}
For $E$: $R_E=\{3,1\}$; the supported label cells are those of rows $3$ and
$1$; the supported port cells are those of rows $3$ and $1$ and, because row
$3$'s descriptor $0$ queried node $2$'s port, also the port cell of row $2$.
Row $2$'s label is unsupported.
\end{example}

\begin{theorem}[Replay invariance]\label{thm:support}
Suppose an equal-length history $H'$ agrees with $H$ on the labels of $R_H$
and on every descriptor cell in $C_H$.  Then the final rooted concrete
scaffolds of $H$ and $H'$ are identical.  Moreover
$R_{H'}=R_H$ and $C_{H'}=C_H$.
\end{theorem}

\begin{proof}
Proceed chronologically through supported descriptor cells.  Every dependency
of a supported cell is an earlier supported cell, so induction makes its
evaluation traverse the same physical endpoints on both sides.  The outgoing
edges and labels of all final-reachable nodes are therefore identical, giving
the same rooted concrete scaffold and the same reachable set.  Recomputing the
least backward closure follows the same descriptor traces, hence gives the
same support.
\end{proof}

\begin{definition}[Garbage fibre]
\label{def:garbage}
$\Gcal(H)$ is the set of histories agreeing with $H$ on the data named in
Theorem~\ref{thm:support}.  A $G$-move changes any collection of the remaining
data.
\end{definition}

\begin{theorem}[Causal-garbage cube]\label{thm:garbage-cube}
Every garbage fibre is the Cartesian product of the finite value sets of its
unsupported label and descriptor coordinates.  Simultaneous $G$ factors into
single-coordinate changes.  Fill a triangle for three values of one
coordinate and a square for changes of two distinct coordinates.  The
resulting path two-complex is simply connected.
\end{theorem}

The last sentence is a statement about \emph{sequences} of garbage moves, of
the kind Remark~\ref{rem:coherence} 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.

\begin{proof}
Support stability in Theorem~\ref{thm:support} makes every unsupported
coordinate independent.  Order the coordinates.  Commuting squares move all
changes of the first coordinate to the front, then the second, and so on.
Same-coordinate triangles compose each block to the direct change between its
endpoint values.  Every path reduces to one coordinate-ordered path; a loop
reduces to the empty path.
\end{proof}

\subsection{A noncommuting boundary}
\label{sec:noncommuting}

Let $S$ denote strong normalization (Theorem~\ref{thm:causal-nf}) 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;\SELF)(1;\eps)(0;0)$.
\begin{center}\small
\begin{tabularx}{\textwidth}{@{}llllX@{}}
\toprule
 & row 1 & row 2 & row 3 & comment \\
\midrule
$E$ & $(1;\SELF)$ & $(1;\eps)$ & $(0;0)$ & node $3\to1$; node $2$ unreachable but queried \\
$S(E)$ & $(1;\SELF)$ & $(1;\SELF)$ & $(0;\eps)$ & row 2 absorbed; row 3 renamed to the new carrier \\
$J(S(E))=E_{SJ}$ & $(0;\MISS)$ & $(1;\SELF)$ & $(0;\eps)$ & row 1 now entirely garbage \\
$J(E)$ & $(1;\SELF)$ & $(0;\eps)$ & $(0;0)$ & row 2's label unsupported, set to $0$; its port cell kept \\
$S(J(E))=E_{JS}$ & $(1;\SELF)$ & $(0;\eps)$ & $(0;0)$ & already strong-normal: node $2$ no longer presents node $1$ \\
\bottomrule
\end{tabularx}
\end{center}
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.

\begin{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.
\end{boundary}

\section{Two calibrated sewing theorems}
\label{sec:sewing}

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.

\subsection{Unexposed acyclic two-row factorizations}

Fix a behaviorally reduced old prefix with top $q$, append one node $r$ (the
\emph{router}), then one more node $z$ (the \emph{consumer}).  The router's
ports are its \emph{slots}.  A consumer port whose descriptor is a nonempty
port word is a \emph{path demand}; its first letter $i$ is its
\emph{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
$\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 \emph{unexposed} (the consumer does not point at the router itself)
\emph{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 \emph{unused} slots are outside causal
support, while a slot used by some consumer demand is queried and supported.

Three final-only moves are useful.

\begin{enumerate}
  \item A \emph{routing crossing} injectively reassigns used router slots and
        changes each first selector to follow the reassignment.
  \item A \emph{cut slide} moves one letter between $\alpha_i$ and $\beta$
        when both bounded descriptors remain legal.
  \item A \emph{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'}$.
\end{enumerate}

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.

\begin{theorem}[Unexposed two-row sewing]\label{thm:two-row}
Fix $d$, $k\geq1$, and a behaviorally reduced old prefix.  Consider two
unexposed acyclic two-row extensions with the same consumer label, the same
valid nonmissing path-demanding consumer coordinates, and literal agreement as missing or
$\SELF$ on every other consumer coordinate.  If corresponding path demands
have the same final old residual behavior, the blocks are connected by
endpoint detours, causal-garbage moves, continuation-aware routing crossings,
and dedicated relation exchanges.  Every common suffix is preserved.
\end{theorem}

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.

\begin{proof}
\emph{Strategy.}  Make each demand own a private router slot, then change
the slots one at a time under the endpoint guard, then undo the private
splitting.

Reducedness makes equal old residual behaviors the same physical old state.
Canonicalize every missing consumer coordinate to literal missing by a
detour.

If several path demands use one first selector, fewer router slots than
demands are currently used.  Copy that router descriptor into an unsupported
slot by $G$ (legal, since unused slots are outside support) and retarget one
consumer word to the copy by a detour; its complete physical endpoint is
unchanged.  Iteration makes the used selectors injective.  Routing crossings
put both blocks into one fixed injective slot placement.

Now each demand has a dedicated slot.  Its current and target factorizations
reach the same old physical state.  One dedicated relation exchange changes
that pair without affecting another demand.  Process all demands, align the
unused cells and router label by $G$, and reverse the target-side
selector-splitting steps.  Every move preserves the consumer endpoint vector,
so the consumer-rooted concrete graph is identical and every common suffix
replays identically.
\end{proof}

\begin{remark}
\label{rem:relative}
Dedicated relation exchange has a bounded graph-local guard for fixed $d,k$,
but it is not a rowwise endpoint detour.  It explicitly cites equality between
two composite old paths across the router/consumer cut.  Whether it is
derivable by refactoring older rows is open.  Theorem~\ref{thm:two-row} is
therefore a presentation \emph{relative to the pointed endpoint congruence of
the old prefix}; it is not a finite relation list independent of that old
action.
\end{remark}

\subsection{The unary whole space}
\label{sec:unary}

Now set $d=k=1$.  Every descriptor is one of
\[
  \MISS,\qquad \SELF,\qquad\eps,\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 \emph{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 \emph{relay rows}: they are not
final-reachable, but their port cells pass the lower carrier upward to the
next one.

\begin{lemma}[Unique relay]\label{lem:relay}
If consecutive states $u>v$ of that final reduced chain are carried at
nonadjacent construction times, the supported descriptor segment between them
is, up to endpoint detours at a recursive bottom,
\[
  \eps\,0\,0\cdots0.
\]
\end{lemma}

\begin{proof}
The first row after the lower carrier selects that carrier by $\eps$.
Every later supported relay row, including the upper carrier's edge to the
lower residual, must use $0$ to pass the same endpoint upward; missing or
$\SELF$ would terminate the relay, while a later $\eps$ would make the
immediately preceding row final-reachable and insert another live residual
between $u$ and $v$.  If the endpoint is a self-loop residual, $\eps$ and $0$
can name the same old endpoint and one detour chooses the displayed form.
\end{proof}

A \emph{temporal carrier slide} exchanges the adjacent descriptor patterns
\[
  (\eps,0)\quad\longleftrightarrow\quad(0,\eps)
\]
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.

\begin{theorem}[Unary final presentation]\label{thm:unary-final}
Fix a length $n$, a nonempty finite working alphabet, degree one, and distance
one.  Two histories have the same final behavioral figure if and only if they
are connected by endpoint detours, absorption, causal-garbage changes, and
temporal carrier slides.  Every final fibre contains one literal right-packed
normal form determined by $n$ and the final figure.
\end{theorem}

``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.

\begin{proof}
\emph{Strategy.}  Soundness is known for each move.  For completeness, push
every carrier upward by slides until the carriers are consecutive at the top,
then canonicalize what is left below.

Soundness has been proved for each move.  For completeness, absorb every
final-live finite unroll of a recursive residual.  The remaining live chain is
behaviorally reduced.

Apply Lemma~\ref{lem:relay} between each two consecutive live residuals.
Prepare the first hidden relay label by a garbage move (the relay row's label
is unsupported).  An inverse temporal slide advances the lower carrier through
that relay time; if it is recursive, absorption restores the $\SELF$
presentation.  Each slide decreases the sum of gaps between consecutive
essential carriers.  Working from the final root downward terminates with the
whole reduced live chain in the latest possible consecutive rows.

Canonicalize endpoint spellings by detours.  Below the last essential carrier
there are three cases.  A missing terminal leaves only causal garbage; a
recursive terminal leaves a canonical $\SELF$ bottom block; and a terminal at
the distinguished base has the unique supported relay
$\eps0\cdots0$, with only its unused labels free.  Garbage moves choose the
least remaining data.  The result depends only on $n$ and the final figure,
and is the right-packed history $\mathsf{RP}_n(F)$.  Histories in one final
fibre both reach that form.
\end{proof}

\subsection{A path-level quotient}

In the unary theorem, call two histories of one final fibre
\emph{chamber-equivalent} if they are connected by strong and garbage moves
alone; a \emph{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 $\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 $\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
\cite[Definition~2.3 and Theorem~2.5]{ArdilaOwenSullivant2012}.

\begin{proposition}[Carrier-surgery CAT(0) geometry]\label{prop:carrier-lattice}
For a fixed unary distance-one final figure and history length, the temporal
slide graph on strong/garbage chambers is the undirected Hasse graph of the
order-ideal lattice of the rectangle above.  Filling every Boolean family of
independent slides gives the CAT(0) cube complex $X(P)$.  If the rectangle has
$r$ rows and $c$ columns, then the complex has $rc$ hyperplanes, dimension
$\min(r,c)$, edge distance
\[
  d(t,s)=\sum_{i=1}^{r}|t_i-s_i|,
\]
and coordinatewise-median carrier tuples.  In particular, its diamond-filled
two-skeleton is simply connected.
\end{proposition}

\begin{proof}
The unique-relay lemma shows that strong and garbage moves preserve the
essential tuple and that all histories with one tuple lie in one chamber.
The temporal endpoint calculation realizes exactly an adjacent move into a
vacancy, which is a cover relation in the componentwise order.  Conversely,
the unique-relay construction realizes every allowed cover.  In the
$\lambda$ coordinates a cover adds or removes one maximal rectangle box, so
the filled cubes are exactly those of $X(P)$ and the cited theorem gives
CAT(0).

There is one hyperplane per rectangle box.  A cube is an antichain of boxes,
whose maximum size in a rectangle is $\min(r,c)$.  Any path between two ideals
must cross each box in their symmetric difference, and removing the boxes of
the first difference in maximal order and adding the second in minimal order
meets that bound; symmetric-difference size is the displayed carrier
distance.  The median ideal is
\[
 (I\cap J)\cup(J\cap K)\cup(K\cap I),
\]
whose row lengths are the coordinatewise medians.

Orient its edges upward.  At a maximal-rank vertex of a loop, equal incident
edges cancel as a backtrack.  Otherwise the two downward moves remove distinct
maximal boxes and form a commuting lattice diamond.  Replacing the peak by the
other two sides strictly lowers the maximal-rank profile.  Iteration contracts
the loop.
\end{proof}

\begin{boundary}
Proposition~\ref{prop:carrier-lattice} is path-level coherence only after
collapsing each strong/garbage chamber.  Theorem~\ref{thm:garbage-cube} gives
path coherence inside a garbage fibre.  A finite elementary presentation of
all mixed strong, garbage, and temporal derivations is not proved here.
\end{boundary}

\section{Feedback, receipts, and a repaired allocation model}
\label{sec:feedback}

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~\ref{sec:conditional}).

\subsection{The receipt knot}

Consider a recognizer for $\EPAL=\{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 \emph{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 \cite{GayDirect2026} argues that the last
cell of that fresh rope must hold a \emph{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}.
\]

\begin{figure}[ht]
\centering
\begin{tikzpicture}[node distance=18mm and 22mm]
  \node[emphbox] (owner) {fresh record\\(owner)};
  \node[box, right=of owner] (rope) {fresh receipt\\rope};
  \node[box, below=of rope] (terminal) {terminal cell\\(pointer)};
  \draw[flow] (owner) -- node[above,font=\scriptsize]{owns} (rope);
  \draw[flow] (rope) -- node[right,font=\scriptsize]{tail} (terminal);
  \draw[flow] (terminal.west) to[bend left=25]
    node[below left,font=\scriptsize]{typed receipt} (owner.south);
\end{tikzpicture}
\caption{The same-step receipt knot.  A fresh allocator that can only
point to records that already exist cannot construct this finite strongly
connected component.}
\label{fig:receipt-knot}
\end{figure}

An earlier internal version of the allocation model (numbered PC-83 in the
project's records) allowed a fresh field to name only an \emph{already
constructed} fresh slot, and its finite checker imposed the same topological
order.  Figure~\ref{fig:receipt-knot} 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.

\subsection{Bounded simultaneous record transducers}

\begin{definition}[Simultaneous record batch]
\label{def:batch}
Fix constants $s$ (roots), $A$ (fresh slots), $q$ (pointer fields per slot),
and $r$ (old dereference radius), together with finite control, tag, and
payload alphabets.  A transition may inspect tags and payloads reached within
$r$ old logical field dereferences from its roots.  From that old observation
it chooses the next control and one finite batch of at most $A$ records.  Each
fresh field and next root targets missing, a bounded old address, or
\emph{any} active slot of the same batch.  No fresh slot is inspected while
the plan is selected, and control does not branch on physical pointer identity.
\end{definition}

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).

\begin{theorem}[Simultaneous-batch compiler]\label{thm:batch}
Every bounded simultaneous record transducer with parameters $(s,A,q,r)$ has
an exact letter-synchronous scaffolding-automaton implementation of degree
\[
  d=s+Aq
\]
and observation/update distance at most $r+1$.
\end{theorem}

\begin{proof}
\emph{Strategy.}  Pack the whole batch into one node, use ports for fields,
use $\SELF$ with a slot tag for every fresh target, and check that decoding
is exact.

One physical scaffold node represents the whole logical batch.  Its finite
label records the active mask; every active tag and payload; and, for every
root and field, the finite target-slot tag.

Ports $0,\ldots,s-1$ represent roots.  Port $s+iq+j$ represents field $j$ of
logical slot $i$.  A decoded pointer is a pair $(v,i)$ of a physical historical
node and a slot.  An old logical address beginning at root $u$ and following
fields $j_1,\ldots,j_m$, $m\leq r$, compiles to the physical word
\[
  u,\quad s+i_0q+j_1,\quad\ldots,\quad s+i_{m-1}q+j_m,
\]
where each next slot $i_h$ is read from the finite target tag at the preceding
edge.  The observed depth-$(r+1)$ neighborhood contains this information.

Use a missing descriptor for missing, the compiled word for an old target,
and physical $\SELF$ for every fresh target.  In the last case the new label
supplies the requested target slot.

Assume the old physical heap decodes correctly.  Induction along a logical old
address proves that its physical word reaches the same old pointer.  Missing
decodes immediately.  A fresh descriptor reaches the node currently being
appended and its tag selects exactly the requested fresh slot.  Applying these
three cases to every root and field makes the decoded new finite adjacency
table identical to the source batch, including all cycles.  This is equality
of finite labelled graphs; no recursive graph unfolding or fixed point is
needed.  Run induction gives exact simulation.  All alphabets and plan
branches are finite, proving the stated degree and distance bounds.
\end{proof}

\begin{remark}[Where the cycle lives]
\label{rem:cycle-lives}
There is no contradiction with Theorem~\ref{thm:chain}.  The physical scaffold
still has only backward edges and self-loops.  A logical record pointer is the
larger coordinate $(v,i)$, not the physical node $v$ alone.  Following a
physical $\SELF$ edge keeps $v$ fixed while its finite edge tag changes the
logical slot from $i$ to $i'$.  An arbitrary finite cycle in the decoded fresh
batch is therefore represented by one physical self-loop together with finite
slot dynamics.  The coordinate realization has moved cyclicity from physical
time into the finite decoder state.
\end{remark}

\subsection{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 \emph{persistent} when old versions survive updates
\cite[\S1]{DSST1989}, and \emph{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 \cite[p.~578, footnote~1]{KaplanTarjan1999}.

\begin{theorem}[Opaque-element staging]\label{thm:staging}
Let a strict purely functional sequence operation:

\begin{enumerate}
  \item use only finite constructor tests and a worst-case bounded number of
        fixed-arity constructor, projection, and pointer steps;
  \item treat elements of its base type as opaque atoms, with no equality,
        hashing, pattern match, identity test, or traversal through a base
        element, while permitting inspection of the representation's own
        pairs, buffers, and recursive child structures; and
  \item return a fixed finite tuple of roots and removed elements.
\end{enumerate}

For fixed old roots and symbolic new elements, its control branch and fresh
structural allocation graph are determined independently of the symbolic
values.  If one symbol denotes a fresh owner that stores a resulting sequence
root, the owner and structural graph form one bounded simultaneous batch and
compile by Theorem~\ref{thm:batch}.
\end{theorem}

\begin{proof}
Run the bounded operation with distinct symbols in place of new elements.
Induct over its bounded primitive steps.  A constructor test or projection
reads only an old structural record or an earlier fresh structural record.
Element opacity prevents the control path from following or branching on a
symbol.  A constructor step adds one fixed-arity structural record whose
fields are old pointers, earlier structural pointers, or symbolic elements.
Thus the branch and an acyclic bounded structural allocation graph are fixed
before element substitution.

Add the fresh owner slot and replace its symbol by a pointer to that slot.  The
substitution can create a cycle from the owner through the sequence structure
and back through an opaque element field, but it cannot change the selected
branch or work bound.  Theorem~\ref{thm:batch} represents every edge of the
resulting finite graph using old paths, missing, or $\SELF$ plus a slot tag.
\end{proof}

Kaplan and Tarjan's Theorem~5.1 gives worst-case constant-time push, pop,
inject, and catenation for regular catenable steques in exactly this strict
model \cite[p.~592]{KaplanTarjan1999}.  Elements at the base type are
parameters to those structural operations; the representation inspects its
own fixed pair and buffer constructors at recursive levels but never the
base element stored at a payload leaf.  Hence their theorem supplies the
source premise required by Theorem~\ref{thm:staging}, not merely an
asymptotic slogan.

\subsection{The conditional application}
\label{sec:conditional}

\begin{proposition}[Feedback programs compile]\label{prop:feedback}
Let a persistent program, at each input letter, start from a fixed number $s$
of roots and perform a fixed finite composition of
strict purely functional sequence operations satisfying the hypotheses of
Theorem~\ref{thm:staging} on opaque pointer elements. In addition it may create
a bounded number of fresh fixed-arity records whose layouts are determined by
the same old observation and whose fields target old records, resulting
sequence roots, or records in that fresh finite batch. At most one designated
fresh owner's pointer is stored as a base-type element of those sequences.
Suppose the complete
per-letter computation, including those sequence operations, follows old
logical fields only within some fixed dereference radius $r$.  Then the
program is a bounded simultaneous record transducer, and it has an exact
letter-synchronous implementation by a finite scaffolding automaton of degree
$s+Aq$ and distance at most $r+1$ for suitable finite $A,q$.
\end{proposition}

\begin{proof}
By Theorem~\ref{thm:staging}, each sequence operation, run with the fresh
owner's pointer replaced by a symbol, has a control branch and an acyclic
structural allocation graph determined by old structure alone; a fixed
finite composition of such operations therefore allocates a bounded acyclic
skeleton and reads a bounded number of old fields. Adding the bounded
fixed-arity records, including the designated owner when present, and
substituting that owner for its symbolic base element yields one finite batch
of bounded size. Its fields target only bounded old addresses, structural
sequence roots, or active fresh slots. This is a transition of
Definition~\ref{def:batch} with $A$ the total allocation bound and $q$ the
maximal record arity. Theorem~\ref{thm:batch} compiles it.
\end{proof}

\begin{example}[the direct even-palindrome recognizer]
\label{ex:palindrome}
The companion paper \cite{GayDirect2026} constructs a recognizer for $\EPAL$
whose per-letter update is a composition of at most six catenable-steque
operations (pop, inject, push, two catenations, and one pop or catenation)
on opaque typed receipts, with one fresh owner record per nonreset step whose
pointer is injected as the terminal element of a fresh rope. Its two table-rope
values and live-rope value are the bounded auxiliary fixed-arity records
allowed by Proposition~\ref{prop:feedback}; their fields contain finite tags,
old receipts, or resulting sequence roots. If that
construction is correct as claimed there, Proposition~\ref{prop:feedback}
applies to it, and Theorem~\ref{thm:lmr} (with the observation that $\EPAL$ is
its own reversal) then yields $\EPAL\in\PEG$ by a route that uses neither a
Turing machine nor the classical real-time palindrome theorem.  This paper
does not re-prove the companion paper's receipt recurrences or its
acceptance invariant, and $\EPAL\in\PEG$ is not a result of this paper: it is
a theorem of the earlier transfer paper \cite{GayStacks2026} and, by the
second route, of \cite{GayDirect2026}.  What the example establishes here is
narrower and entirely proved above: the same-step cycle that broke the
topologically ordered allocator is no obstacle for a scaffold.
\end{example}

\begin{scope}
Proposition~\ref{prop:feedback} 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.
\end{scope}

\section{Open boundaries}
\label{sec:open}

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

\begin{enumerate}
  \item \textbf{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.
  \item \textbf{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.
  \item \textbf{Support handoff.}  A temporal slide can transfer one visible
        label obligation across a causal cut.  Classify its interactions
        (critical pairs) with detours and absorption.
  \item \textbf{Navigation monoids.}  Characterize which finitely generated
        submonoids of the regressive chain monoid occur at fixed degree,
        distance, and uniform finite control.
  \item \textbf{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.
  \item \textbf{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
        \cite{AriolaKlop1996} or to the categorical presentation of term
        graphs \cite{FritzLiang2023}.  Novelty should be judged only after
        that comparison.
\end{enumerate}

\section{Assurance, provenance, and nonclaims}
\label{sec:assurance}

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.

\begin{center}
\begin{tabularx}{0.94\textwidth}{>{\bfseries}l X}
\toprule
Layer & What it establishes\\
\midrule
Written proof & the stated theorem for all objects satisfying its hypotheses\\
Finite audit & exact behavior over one explicitly bounded search domain\\
Source audit & the external theorem or model says what the paper attributes to it\\
Specialist review & an independent reader has attacked correctness and positioning\\
Novelty review & the contribution has been compared broadly enough to support priority language\\
\bottomrule
\end{tabularx}
\end{center}

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.

\paragraph{What is inherited.}  Coalgebraic minimization and functional
bisimulation \cite{Rutten2000}; ordinary acyclic-state merging
\cite{DaciukEtAl2000}; general cyclic term-graph fold/unfold and confluence
\cite{AriolaKlop1996}; the scaffold model and its PEG correspondence
\cite{LMR2020}; strict real-time catenable steques \cite{KaplanTarjan1999}.
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.

\paragraph{What the viewpoint contributed.}  The separation in
Figure~\ref{fig:ladder} 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 $\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.

\paragraph{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~\ref{sec:feedback} in an internal draft before publication.  The
primary sources cited were read in full and the exact statements used are
quoted with locators; copies and extracted text are held locally and are not
part of the public repository.  This paper and the companion paper
\cite{GayDirect2026} 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.

\section{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 $\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 $\SELF$ edges with slot tags.  That change of representation repairs
the allocation seam of the palindrome application, but more importantly it
exhibits the general principle: complexity can move between semantic
structure, presentation dynamics, and observation without disappearing.

\appendix

\section{Move and preservation table}

\begin{center}
\begin{tabularx}{\textwidth}{>{\bfseries}l X X}
\toprule
Move & Local action & Guaranteed preservation\\
\midrule
$D$ endpoint detour & rename one bounded word with the same physical endpoint & every prefix figure and every common suffix\\
$A$/$U$ absorption, unroll & replace an old recursive carrier by fresh $\SELF$ & every prefix figure and every common suffix\\
$G$ garbage change & change data outside one source-certified replay support & final rooted concrete scaffold\\
$T$ temporal slide & move a unary residual carrier across one adjacent time cut & final behavioral figure\\
$R$ routing crossing & reassign demanded router slots injectively and transport selectors & final concrete consumer endpoints\\
$E^{\mathrm{rel}}$ relation exchange & exchange two dedicated factorizations with one old endpoint & final concrete consumer endpoints\\
\bottomrule
\end{tabularx}
\end{center}

\section{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}
\]

\begin{thebibliography}{99}

\bibitem{ArdilaOwenSullivant2012}
Federico Ardila, Megan Owen, and Seth Sullivant.
\newblock Geodesics in CAT(0) cubical complexes.
\newblock \emph{Advances in Applied Mathematics}, 48(1):142--163, 2012.
\newblock \url{https://doi.org/10.1016/j.aam.2011.06.004}.

\bibitem{AriolaKlop1996}
Zena M. Ariola and Jan Willem Klop.
\newblock Equational term graph rewriting.
\newblock \emph{Fundamenta Informaticae}, 26(3--4):207--240, 1996.
\newblock \url{https://doi.org/10.3233/FI-1996-263401}.
\newblock Earlier version: CWI report CS-R9552, 1995 (the version inspected).

\bibitem{Brzozowski1964}
Janusz A. Brzozowski.
\newblock Derivatives of regular expressions.
\newblock \emph{Journal of the ACM}, 11(4):481--494, 1964.
\newblock \url{https://doi.org/10.1145/321239.321249}.

\bibitem{ChomskySchutzenberger1963}
Noam Chomsky and Marcel-Paul Sch\"utzenberger.
\newblock The algebraic theory of context-free languages.
\newblock In P.~Braffort and D.~Hirschberg, editors, \emph{Computer
Programming and Formal Systems}, pages 118--161. North-Holland, 1963.

\bibitem{DaciukEtAl2000}
Jan Daciuk, Stoyan Mihov, Bruce W. Watson, and Richard E. Watson.
\newblock Incremental construction of minimal acyclic finite-state automata.
\newblock \emph{Computational Linguistics}, 26(1):3--16, 2000.
\newblock \url{https://aclanthology.org/J00-1002/}.

\bibitem{DSST1989}
James R. Driscoll, Neil Sarnak, Daniel D. Sleator, and Robert E. Tarjan.
\newblock Making data structures persistent.
\newblock \emph{Journal of Computer and System Sciences}, 38(1):86--124, 1989.
\newblock \url{https://doi.org/10.1016/0022-0000(89)90034-2}.

\bibitem{Ford2004}
Bryan Ford.
\newblock Parsing expression grammars: A recognition-based syntactic
foundation.
\newblock In \emph{Proceedings of POPL 2004}, pages 111--122. ACM, 2004.
\newblock \url{https://doi.org/10.1145/964001.964011}.

\bibitem{FritzLiang2023}
Tobias Fritz and Wendong Liang.
\newblock Free gs-monoidal categories and free Markov categories.
\newblock \emph{Applied Categorical Structures}, 31(2):21, 2023.
\newblock \url{https://doi.org/10.1007/s10485-023-09717-0}.  arXiv:2204.02284.

\bibitem{GayDirect2026}
Joshua Gay.
\newblock Persistent receipts and simultaneous records: a direct scaffold for
even palindromes.
\newblock FPRD Lab review paper, Draft 2, 22 August 2026.
\newblock \url{https://gitlab.com/insight-forge/boxlab/fprd-lab/-/tree/main/publications/direct-palindrome-scaffolding}.

\bibitem{GayStacks2026}
Joshua Gay.
\newblock Real-time multitape languages transfer to parsing expression
grammars.
\newblock FPRD Lab review paper, released 5 August 2026.
\newblock \url{https://gitlab.com/insight-forge/boxlab/fprd-lab/-/tree/main/publications/persistent-stacks-scaffolding}.

\bibitem{KaplanTarjan1999}
Haim Kaplan and Robert E. Tarjan.
\newblock Purely functional, real-time deques with catenation.
\newblock \emph{Journal of the ACM}, 46(5):577--603, 1999.
\newblock \url{https://doi.org/10.1145/324133.324139}.

\bibitem{LMR2020}
Bruno Loff, Nelma Moreira, and Rog\'erio Reis.
\newblock The computational power of parsing expression grammars.
\newblock \emph{Journal of Computer and System Sciences}, 111:1--21, 2020.
\newblock \url{https://doi.org/10.1016/j.jcss.2020.01.001}.
\newblock Expanded preprint arXiv:1902.08272v2 (2020); definition and theorem
numbers in this paper follow the preprint.

\bibitem{Nerode1958}
Anil Nerode.
\newblock Linear automaton transformations.
\newblock \emph{Proceedings of the American Mathematical Society},
9(4):541--544, 1958.
\newblock \url{https://doi.org/10.1090/S0002-9939-1958-0135681-9}.

\bibitem{PinMPRI}
Jean-\'Eric Pin.
\newblock \emph{Mathematical Foundations of Automata Theory}.
\newblock Lecture notes, MPRI; author-hosted, version retrieved 22 August
2026.
\newblock \url{https://www.irif.fr/~jep/PDF/MPRI/MPRI.pdf}.

\bibitem{Rutten2000}
Jan J. M. M. Rutten.
\newblock Universal coalgebra: a theory of systems.
\newblock \emph{Theoretical Computer Science}, 249(1):3--80, 2000.
\newblock \url{https://doi.org/10.1016/S0304-3975(00)00056-6}.


\end{thebibliography}

\end{document}