Comparing two ways to rearrange a history

Suppose two legal sequences of changes turn one construction history into another. Knowing that they reach the same endpoint is useful. A stronger question asks whether we can explain their agreement by a small collection of local identities between sequences of changes. That is the meaning of coherence in this article.

The simplest identity swaps two independent moves. If one change affects an irrelevant label in row 2 and another affects an irrelevant label in row 5, their order does not matter. The two paths form a square. Three successive choices for one irrelevant label form a triangle: going through an intermediate value agrees with changing directly to the final value. Such identities explain all changes confined to a fixed set of irrelevant coordinates.

The complication is that relevance can change. Moving a record to a new construction time can make a previously irrelevant label visible. A valid identity must respect the guards under which each move is legal. Dropping those guards produces an easier algebra about different objects.

We work in the unary scaffold model: every node has one outgoing edge, and a construction step can copy the old top or its immediate endpoint, create a self-loop, or leave the edge missing. Even this small model distinguishes physical nodes, the behaviors they present, and the times at which useful behaviors are carried.

The timing geometry has a small example. Take a history of length five with three essential carriers and an ordinary terminal. The final carrier is fixed at time five. The first two may occupy any increasing pair of times in $\{1,2,3,4\}$:

$$(1,2,5),\ (1,3,5),\ (1,4,5),\ (2,3,5),\ (2,4,5),\ (3,4,5).$$

Subtract the carrier’s position in the tuple: $(t_1-1,t_2-2)$. The resulting pairs are the weakly increasing pairs between zero and two, representing the order ideals of a two-by-two rectangle. From $(1,3,5)$, moving the first carrier right and moving the second carrier right are independent. Either order reaches $(2,4,5)$ through legal placements. This is one of the squares in the carrier cube.

The article’s main work concerns the physical presentations lying over that timing geometry. Most pairs of moves commute or form a triangle. One interaction between absorption and temporal transport requires a larger identity: a bounded hexagon. Its two paths end at exactly the same physical descriptor triple. Section 6 writes both paths out, including the case where a lower row must first be made literally self-looping.

The proof then has two responsibilities. It must show that the directed simplifications terminate at one normal class, and it must classify every way two available steps can initially disagree. With those local cases in hand, induction replaces the first disagreement between longer paths and continues below the original reduction measure.

The conclusion is a fixed list of guarded kinds of identity, valid at every finite history length. The number of particular instances grows with the history, and their guards refer to endpoints and causal support. This is why the result does not claim a finite context-free list of rewriting rules with no side conditions. The definitions, local calculations, and induction below specify exactly which stronger comparison of paths has been established.

1 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 scaffolding automata as a persistent graph machine model for PEGs [5]. 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 Persistent scaffold computation develops these layers and four elementary moves [3]. 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.

Working picture.  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.

2 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 $$\mathsf{MISSING},\qquad \mathsf{SELF},\qquad \epsilon,\qquad 0.$$ If $e(i)$ is its physical endpoint, then $\mathsf{MISSING}$ is absent, $\mathsf{SELF}$ is $i$, $\epsilon$ 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 causal support. Changing any unsupported label or descriptor is a garbage move $G$.

Literal physical self-looping matters. A row may present a recursive behavior while pointing to a different old carrier; changing it directly to $\mathsf{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.

3 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$.

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 [1, Definition 2.3 and Theorem 2.5]. A rectangle has no inconsistent pairs.

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.

4 Rewriting modulo causal garbage

Let $\mathcal G$ be the symmetric relation of single-coordinate garbage changes. Support stability makes every $\mathcal G$-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 $$\mathsf{MISSING}<\mathsf{SELF}<\epsilon<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$.

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

5 Support transport

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

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.

6 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,\epsilon)$, 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 $\mathsf{SELF}$, and the empty path otherwise.

If $D_y$ is coinitial with the same slide, equality of the $0$ and $\epsilon$ endpoints forces $x$ itself to be literal $\mathsf{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.

7 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 $\epsilon,0,\epsilon$ and $0,\epsilon,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.

8 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 [2], proved here directly because our guards are not assumed to be a conventional context-closed polygraph.

Boundary.  This is a finite list of guarded schema 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 [4]. The bounded hexagon controls the observed A/T index, but no finite derivation type claim is made.

9 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 8.1; the causal arguments do.

A separate AI-assisted audit 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 audit recorded “gap closed.” This records the earlier checking process; the argument is the collapse lemma and the proof above.

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, $\mathsf{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.

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.