\documentclass[11pt]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{lmodern}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{booktabs,tabularx}
\usepackage{enumitem}
\usepackage{xcolor}
\usepackage{microtype}
\usepackage{fancyhdr}
\usepackage{hyperref}

\hypersetup{colorlinks=true,linkcolor=blue!55!black,citecolor=blue!55!black,
urlcolor=blue!55!black,pdftitle={A Coherent Cubical Algebra for Unary Scaffold Histories},
pdfauthor={Joshua Gay}}
\urlstyle{same}
\setlist{nosep}
\setlength{\parskip}{0.45em}
\setlength{\parindent}{0pt}
\pagestyle{fancy}
\fancyhf{}
\fancyhead[L]{Coherent cubical scaffold algebra}
\fancyhead[R]{Draft 1, review stage}
\fancyfoot[C]{\thepage}
\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{boundary}{\begin{quote}\small\textbf{Boundary.}\ }{\end{quote}}
\newenvironment{intuition}{\begin{quote}\small\textbf{Working picture.}\ }{\end{quote}}

\newcommand{\SELF}{\mathsf{SELF}}
\newcommand{\MISS}{\mathsf{MISSING}}
\newcommand{\eps}{\epsilon}
\newcommand{\RP}{\mathsf{RP}}
\newcommand{\Gcal}{\mathcal G}
\newcommand{\Rcal}{\mathcal R}

\title{\textbf{A Coherent Cubical Algebra\\for Unary Scaffold Histories}}
\author{Joshua Gay\\\small FPRD Lab, Insight Forge}
\date{Draft 1, 23 August 2026}

\begin{document}
\maketitle

\begin{abstract}
Scaffolding automata give parsing expression grammars a persistent graph
machine model.  Previous work developed an algebra of finite scaffold
histories and proved that, at degree one and observation distance one,
endpoint detours, literal self-loop absorption, causal garbage, and temporal
carrier slides connect exactly the histories with one final behavioral
figure.  It left a path-level question open: which relations generate all
equalities between different sequences of those moves?

We answer that question by separating geometry from physical presentation.
After collapsing strong and garbage variation, essential residual carriers
form a corrected fixed-top order-ideal lattice, and independent temporal
slides fill its CAT(0) cube complex.  Over that base, causal garbage fibres
are products.  Effective detours, absorptions, and slides never enlarge
descriptor support.  Label transport is strict except at three support
captures, each filled by garbage cancellation.  Every horizontal critical
branching is Peiffer, cubical, triangular, or one bounded
absorption--transport hexagon
\[
 A_yA_x = T_{yz}A_xA_yD_z,
\]
where $A_x$ is empty when the lower row already uses literal $\SELF$; the
apparent detour--transport cell is derived.  Horizontal moves already trivial
inside a garbage fibre have bounded collapse cells.  A direct coherent-Newman
induction modulo garbage then shows that this length-independent guarded
family presents every parallel elementary path in every fixed-length unary
distance-one final fibre.

``Guarded'' is essential.  Physical endpoint and replay-support certificates
range over histories.  We do not claim a finite context-closed polygraph,
finite derivation type, higher-degree coherence, or novelty for the general
CAT(0) and rewriting machinery.
\end{abstract}

\section{Why paths, rather than only accepted languages?}

A formal language is a set of words.  A recognizer is a process that reaches
that yes-or-no observation through internal states and actions.  Context-free
grammars are usually read generatively: a successful derivation witnesses
membership.  Parsing expression grammars (PEGs) are deterministic
recognizers: ordered choice and the recognition history decide which suffix
remains.  Loff, Moreira, and Reis introduced \emph{scaffolding automata} as a
persistent graph machine model for PEGs \cite{LMR2020}.  At every input letter
one bounded row is appended to a permanent scaffold; the new row can inspect
only a bounded neighborhood of the preceding top.

Collapsing a scaffold computation to its accepted language forgets several
different objects:
\[
 \text{row word}\longrightarrow\text{physical history}
 \longrightarrow\text{strong trace}
 \longrightarrow\text{final figure}\longrightarrow\text{acceptance}.
\]
The physical history remembers node identity and construction time.  Its
strong trace remembers the behavioral figure after every prefix.  The final
figure forgets all earlier observations.  Acceptance forgets almost
everything else.

The companion paper \emph{Persistent scaffold computation} develops these
layers and four elementary moves \cite{GayScaffold2026}.  It proves one
right-packed object normal form for every unary distance-one final fibre.  It
also proves path coherence inside each garbage fibre and, after collapsing
whole strong/garbage chambers, in the carrier-slide quotient.  It explicitly
does not present all mixed physical derivations.  The present paper begins at
that boundary.

\begin{intuition}
The object is fibred.  Carrier placements form the base geometry.  Different
physical spellings of one placement form a vertical fibre.  Temporal slides
transport presentation data between adjacent fibres.  Higher cells say when
two vertical or horizontal operations can be interchanged.
\end{intuition}

\section{The unary history calculus}

Fix a nonempty finite label alphabet, history length $n$, scaffold degree one,
and observation distance one.  There is one distinguished unlabelled base at
time $0$.  Row $i$ has a label and one descriptor from
\[
 \MISS,\qquad \SELF,\qquad \eps,\qquad 0.
\]
If $e(i)$ is its physical endpoint, then $\MISS$ is absent, $\SELF$ is $i$,
$\eps$ is $i-1$, and $0$ copies $e(i-1)$.  The final live chain starts at $n$
and iterates $e$ until missing or a self-loop.  Minimizing equal residual
behaviors gives the final behavioral figure.

The labels of final-live rows are supported.  Every descriptor on that chain
is supported; if a supported descriptor is $0$, the descriptor immediately
below it is supported recursively.  This is the least replay-closed
\emph{causal support}.  Changing any unsupported label or descriptor is a
garbage move $G$.

\begin{definition}[Horizontal moves]
An endpoint detour $D$ replaces a descriptor by the least spelling with the
same physical endpoint.  A literal absorption $A$ applies when a fresh row
points to an old physical node $q$ with $e(q)=q$ and presents the same
recursive residual; it replaces that old pointer by fresh $\SELF$.  A
temporal slide $T$ exchanges
\[
  (\eps,0)\longleftrightarrow(0,\eps)
\]
on two consecutive rows when the two candidate carrier labels agree.
\end{definition}

Literal physical self-looping matters.  A row may present a recursive
behavior while pointing to a different old carrier; changing it directly to
$\SELF$ is not then a primitive absorption.  An early computational model in
this project made exactly that error.  All statements below use the literal
guard.

Each move preserves the final behavioral figure.  Detours and absorptions
also preserve every prefix figure; temporal slides may change intermediate
figures.  We study the undirected elementary path groupoid generated by
$D,A,T,G$, while orienting selected horizontal edges only to prove
termination.

\section{The CAT(0) carrier base}

Reduce the final live chain behaviorally and omit the arbitrary physical
carrier of a terminal recursive residual.  Let
$t_1<\cdots<t_m$ be the construction times of the remaining essential
carriers.  The final root is carried at the final time, so $t_m=n$.

\begin{proposition}[Corrected carrier rectangles]\label{prop:rectangles}
For an ordinary missing or base terminal and $m\ge1$, carrier placements are
the ideals of $[m-1]\times[n-m]$.  For a recursive terminal, $m=0$ is a
singleton; for $m\ge1$, placements are the ideals of
$[m-1]\times[n-m-1]$.
\end{proposition}

\begin{proof}
In the ordinary case
\[
 1\le t_1<\cdots<t_{m-1}<t_m=n.
\]
Put $\lambda_i=t_i-i$.  Then
$0\le\lambda_1\le\cdots\le\lambda_{m-1}\le n-m$, and the $\lambda_i$ are
the row lengths of an ideal in the displayed rectangle.  The inverse is
$t_i=\lambda_i+i$ with $t_m=n$.

At a recursive bottom, the omitted physical loop carrier must occur below the
first retained finite carrier, so time $1$ is unavailable.  Put
$\lambda_i=t_i-i-1$ to obtain the second rectangle.  Conversely, the unique
relay $\eps,0,\ldots,0$ realizes every listed placement; unused coordinates
are garbage.  Strong and garbage moves preserve the essential tuple, and all
histories with one tuple lie in one chamber \cite{GayScaffold2026}.
\end{proof}

A slide changes one $\lambda_i$ by one while preserving weak increase.  It is
exactly the addition or removal of one maximal ideal box.  Ardila, Owen, and
Sullivant construct from any poset with inconsistent pairs a rooted CAT(0)
cube complex whose vertices are consistent ideals and whose cubes remove
subsets of maximal elements \cite[Definition~2.3 and Theorem~2.5]{AOS2012}.
A rectangle has no inconsistent pairs.

\begin{theorem}[Carrier cube]\label{thm:carrier-cube}
Filling every Boolean family of independent temporal slides gives the rooted
CAT(0) order-ideal cube of Proposition~\ref{prop:rectangles}.  For a rectangle
with $r$ rows and $c$ columns it 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.
\end{theorem}

\begin{proof}
There is one hyperplane per box and one cube per antichain of currently
removable maximal boxes.  The maximum antichain in a rectangle has size
$\min(r,c)$.  Any edge path must cross every box in the symmetric difference
of its endpoint ideals; removing and adding those boxes in legal order attains
that bound.  The median ideal is
$(I\cap J)\cup(J\cap K)\cup(K\cap I)$, whose row lengths are the
coordinatewise medians.
\end{proof}

This theorem is recalled from the corrected Draft 3 of the companion paper.
Its role here is structural: pure temporal schedules already have cubical
coherence.  The unresolved work lies in lifting that geometry through the
physical presentation fibres.

\section{Rewriting modulo causal garbage}

Let $\Gcal$ be the symmetric relation of single-coordinate garbage changes.
Support stability makes every $\Gcal$-class a finite Cartesian product.
Same-coordinate triangles compose successive values; different-coordinate
squares commute them.  These cells make each garbage fibre coherent.

On garbage classes orient effective $D,A,T$ edges by
\[
 \mu(H)=(g(H),w(H)),
\]
where $g$ is total displacement of the behaviorally reduced essential tuple
from its right-packed tuple, and $w$ is the supported descriptor word in the
order
\[
 \MISS<\SELF<\eps<0.
\]
$D$ and $A$ preserve the reduced tuple and lower $w$.  An essential $T$ lowers
$g$; an inessential $T$ is oriented toward smaller $w$.  Thus every effective
horizontal edge strictly decreases $\mu$.

\begin{lemma}[Unique quotient normal class]\label{lem:normal}
Every final fibre has one irreducible garbage class, the right-packed class
$\RP_n(F)$.  Hence oriented effective horizontal rewriting terminates and is
object-confluent modulo garbage.
\end{lemma}

\begin{proof}
Finiteness and strict decrease give termination.  If $g>0$, choose the highest
carrier gap.  The unique-relay lemma exposes a supported
$\eps,0,\ldots,0$ bridge.  Its first hidden relay label is unsupported and can
be prepared inside the same garbage class; the adjacent essential slide then
reduces $g$.

At gap zero, a nonleast supported endpoint exposes $D$, a supported repeated
literal recursive residual exposes $A$, and an inessential adjacent inversion
exposes $T$.  When none applies, the terminal is forced to be the canonical
missing, recursive, or base bottom described in the companion proof.  This is
exactly $\RP_n(F)$, and it has no effective outgoing edge.  Every noncanonical
class therefore has a reduction and the canonical class is the unique normal
class.  Termination plus uniqueness yields confluence.
\end{proof}

Some legal horizontal edges are already identities in $\Gcal$.  They must not
simply disappear from a theorem about physical paths.

\begin{lemma}[Garbage-trivial collapse]\label{lem:collapse}
If a legal $D$ or $A$ edge is trivial modulo garbage, it equals one descriptor
garbage edge.  If a legal $T$ edge is trivial modulo garbage, it equals a
two-descriptor garbage path; the two orders agree by the garbage square.
\end{lemma}

\begin{proof}
Equal garbage normal forms have equal causal support.  $D/A$ change one
descriptor and $T$ changes two.  Any changed supported value would survive
normalization, so every changed coordinate is unsupported.  Replay invariance
keeps support fixed after the first of the two $T$ garbage changes.
\end{proof}

\section{Support transport}

The next question is whether a garbage change commutes with a horizontal
move.  Descriptors and labels behave differently.

\begin{lemma}[Descriptor-support monotonicity]\label{lem:descriptor}
For every effective oriented horizontal move $R$,
\[
 \operatorname{DescSupp}(RH)\subseteq\operatorname{DescSupp}(H).
\]
Every coinitial horizontal/garbage-descriptor branching is therefore a strict
naturality square modulo garbage.
\end{lemma}

\begin{proof}
A detour replaces an indirect $0$ name by a direct least name of the same
endpoint, deleting replay dependencies.  An absorption replaces a replay into
an old self-loop by fresh $\SELF$, again terminating dependencies.  A slide
exchanges the roles ``live carrier'' and ``certified replay dependency'' among
the same three local descriptor cells; it introduces no descriptor outside
the source closure.

An unsupported descriptor cannot influence any endpoint or guard read by an
effective move.  The same residual therefore remains available after changing
it, and monotonicity leaves the changed cell unsupported at the target.  The
two target histories differ by one garbage edge.
\end{proof}

Horizontal motion can promote a label from garbage to visible support.  There
are exactly three possibilities.  Absorption replaces an old self-loop
carrier by its fresh presentation, so only the fresh row label can be
captured.  A temporal slide substitutes one of two equal-labeled adjacent
carriers, so the gaining label is either the first slide row or its
predecessor, depending on direction.

\begin{proposition}[Support captures]\label{prop:captures}
The only mixed branches without a strict horizontal residual are
\[
 A/GL(0),\qquad T/GL(0),\qquad T/GL(-1).
\]
They require no new generator: the garbage-first path returns along the
inverse garbage edge and then takes the original reduction, so
$G;G^{-1};R=R$ by vertical cancellation.
\end{proposition}

\section{The absorption--transport hexagon}

The non-Peiffer horizontal interaction occurs on three consecutive rows
$x,y,z$.  Suppose the descriptors at $y,z$ are $(0,\eps)$, the labels of
$x,y$ agree, literal $A_y$ is available, and $T_{yz}$ is oriented from this
source.  Let $A_x$ be absorption at $x$ when $x$ is not already $\SELF$, and
the empty path otherwise.

\begin{theorem}[A/T hexagon]\label{thm:hexagon}
The following paths have exactly the same raw physical endpoint:
\[
 A_y;A_x = T_{yz};A_x;A_y;D_z.
\]
No garbage quotient is used in this equation.
\end{theorem}

\begin{proof}
Let $q=e(x)$ be the endpoint named by $y$'s $0$.  The literal $A_y$ guard says
that $q$ is an old physical self-loop and that $y$ presents its recursive
residual.  The temporal label guard makes $x$ present that residual as well.
Thus, if $x$ is not already $\SELF$, one literal $A_x$ is available; no long
prefix normalization is needed.

Write $p$ for $x$'s old descriptor.  The left path gives
\[
 (p,0,\eps)\xrightarrow{A_y}(p,\SELF,\eps)
 \xrightarrow{A_x}(\SELF,\SELF,\eps).
\]
The right path gives
\[
 (p,0,\eps)\xrightarrow{T}(p,\eps,0)
 \xrightarrow{A_x}(\SELF,\eps,0)
 \xrightarrow{A_y}(\SELF,\SELF,0)
 \xrightarrow{D_z}(\SELF,\SELF,\eps).
\]
At the last step, $0$ follows the now-self-looping row $y$, while $\eps$ names
$y$ directly.  They have the same physical endpoint.
\end{proof}

If $D_y$ is coinitial with the same slide, equality of the $0$ and $\eps$
endpoints forces $x$ itself to be literal $\SELF$.  Then
$D_yA_y=T_{yz}A_yD_z$.  The ordinary D/A triangle identifies $D_yA_y$ with
direct $A_y$, so D/T is a pasting of D/A with the SELF-eager hexagon and is not
an independent cell.

\section{Complete local classification}

Two detours commute because they preserve physical endpoints.  A lower
absorption acts on every affected later $0$ replay by the uniform substitution
of its old self-loop carrier by the fresh equal-behavior carrier.  Uniform
substitution preserves endpoint equalities and transports other literal
absorption guards.  Hence strong/strong peaks are Peiffer squares or the
same-row D/A triangle.

For T/T, two essential reductions remove incomparable maximal boxes in the
carrier cube and commute.  The only overlapping raw descriptor words are
$\eps,0,\eps$ and $0,\eps,0$.  If the repeated residual is recursive, both
swaps are inessential and exactly one direction lowers descriptor order.  If
it is nonrecursive, the swaps move essential carriers oppositely and exactly
one lowers carrier gap.  Thus no overlapping oriented T/T peak exists.

A slide transports suffix endpoints by one uniform substitution between its
adjacent equal-behavior carriers.  Strong guards away from the first slide
coordinate therefore commute.  The apparent exception is an upper
absorption whose old physical self-loop would be replaced by a non-self-looping
equal-behavior row.  If that upper absorption is effective, the lower
recursive block is behaviorally inessential; the threatened slide direction
then increases descriptor order and is not oriented.  The reverse orientation
preserves the literal guard.  At the first slide coordinate, the only cases
are the A/T hexagon and derived D/T diagram above.

\begin{theorem}[Local cell classification]\label{thm:local}
Every coinitial effective horizontal pair is aspherical, Peiffer/cubical,
D/A triangular, A/T hexagonal, or D/T derived.  Every horizontal/garbage pair
is a strict naturality square or one of the three cancellation captures.
Every garbage-trivial horizontal edge has a collapse cell from
Lemma~\ref{lem:collapse}.
\end{theorem}

\section{Uniform guarded coherence}

We use a direct finite-graph version of coherent Newman induction modulo
relations.  Let $E$ be a symmetric relation with a coherent path
presentation, and let $R$ terminate on $E$-classes with one normal class.  If
every R/R and R/E local branch has a chosen confluence cell modulo $E$, then
those cells present every parallel path.  Indeed, canonicalize vertical
subpaths and induct on the quotient reduction measure and remaining
horizontal length.  Replace the first disagreement by its local cell; every
horizontal tail lies below the source class.  An E-capture may use an inverse
vertical edge, but it needs no recursive horizontal induction.  This is the
proof architecture of coherent confluence modulo \cite{DupontMalbos2022},
proved here directly because our guards are not assumed to be a conventional
context-closed polygraph.

\begin{theorem}[Uniform guarded path presentation]\label{thm:main}
Fix a finite alphabet and history length in degree one and distance one.  In
each final behavioral fibre, all parallel paths generated by endpoint
detours, literal absorptions, causal-garbage changes, and temporal slides are
presented by the following length-independent guarded cell families:
\begin{enumerate}
\item garbage same-coordinate triangles and different-coordinate squares;
\item collapse cells for garbage-trivial D/A/T edges;
\item strong Peiffer squares and the same-row D/A triangle;
\item carrier-cube and inessential temporal Peiffer squares;
\item strict mixed naturality squares; and
\item the bounded A/T hexagon.
\end{enumerate}
The three support captures use vertical cancellation, and D/T is derived.
\end{theorem}

\begin{proof}
Lemma~\ref{lem:normal} supplies quotient termination and one normal class.
Garbage fibres have their product cells.  Lemma~\ref{lem:collapse} eliminates
horizontal edges already vertical.  Theorem~\ref{thm:local} supplies every
remaining local R/R and R/E cell.  Apply the direct coherent-Newman induction
modulo garbage.
\end{proof}

\begin{boundary}
This is a finite list of guarded schema \emph{types}; it is not a finite
context-closed polygraph.  Endpoint-equality and causal-support certificates
range over histories.  Guiraud and Malbos show why indexed critical
branchings make finite-derivation-type conclusions delicate in higher
dimensions \cite{GuiraudMalbos2009}.  The bounded hexagon controls the observed
A/T index, but no finite derivation type claim is made.
\end{boundary}

\section{Evidence, failure modes, and the larger program}

The promoted exact atlas checks complete domains with one label through
length eight, two labels through length five, and three labels through length
four: 147,448 histories.  It asserts quotient termination, one normal class,
descriptor-support monotonicity, the exact A/T and D/T critical signatures,
the exact three label captures, and the collapse classification.  A separate
raw-history checker verifies 12,914 A/T hexagons, including 4,116 with a
non-SELF-eager lower row.

A homology mutation is used only as a falsifier.  Removing the overlapping
D/T cell while retaining D/T Peiffer squares leaves zero residual first
homology.  Retaining only SELF-eager A/T instances also leaves zero.  Removing
A/T exposes 120 residual classes.  A seeded length-10/20/40 probe checks
67,848 additional coinitial pairs and finds no new non-Peiffer type.  None of
these finite results proves Theorem~\ref{thm:main}; the causal arguments do.

An independent reviewer reconstructed the proof and found one missing edge
class: legal horizontal moves already trivial modulo garbage.  The collapse
lemma was added, the quotient normal-form proof was expanded, and the same
reviewer returned ``gap closed.''  This is review evidence, not authorship or
specialist endorsement.

The fibred formulation suggests a higher-degree program.  Replace the unary
carrier chain by the dependency diagram of essential residual records.  Ask
whether legal time placements form a poset-with-inconsistent-pairs cube or a
different event geometry.  Put detours, folds/unfolds, receipts, $\SELF$, and
garbage in vertical fibres; treat sewing as transport; then classify the cells
where transport changes support or overlaps a vertical fold.  Failure of
CAT(0), unbounded indexed branchings, or proliferating support curvature would
be a precise obstruction rather than merely a failed language-level proof.

\section*{Assurance and contribution statement}

The ordinary mathematical arguments are the proof.  Executable checks are
independent falsifiers only to the extent stated in the public evidence
ledger.  No proof assistant is used as a stronger label.  AI systems assisted
with exploration, checking, adversarial review, and exposition; Joshua Gay is
responsible for the public claims and their disposition.

The FPRD contribution is the separation of presentation, dynamics, and
observation.  That separation exposed an exact CAT(0) base, causal fibres,
partial transport, and one curvature cell.  It also exposed and repaired the
overbroad absorption model, overcounted support generators, incorrect carrier
rectangle, and omitted garbage-trivial edges.

\begin{thebibliography}{99}
\bibitem{AOS2012}
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{DupontMalbos2022}
Benjamin Dupont and Philippe Malbos.
\newblock Coherent confluence modulo relations and double groupoids.
\newblock arXiv:1810.08184v3, 2021.
\newblock \url{https://arxiv.org/abs/1810.08184}.

\bibitem{GayScaffold2026}
Joshua Gay.
\newblock Persistent scaffold computation: causal presentations, sewing, and
feedback.
\newblock FPRD Lab review paper, Draft 3, 23 August 2026.
\newblock \url{https://gitlab.com/insight-forge/boxlab/fprd-lab/-/tree/main/publications/persistent-scaffold-causal-algebra}.

\bibitem{GuiraudMalbos2009}
Yves Guiraud and Philippe Malbos.
\newblock Higher-dimensional categories with finite derivation type.
\newblock arXiv:0810.1442v2, 2009.
\newblock \url{https://arxiv.org/abs/0810.1442}.

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

\end{document}