Width-Bounded Equational Derivations for Finite Graph Expressions
TL;DR
It is proved that equal closed expressions of pattern width at most $k$ are joined by a derivation in which every step applies an equation in either direction and every intermediate width is at most a computable $B_\Sigma(k)$, independently of graph size.
Abstract
Completeness of an equational presentation guarantees an equality path but need not control the resources used along it. For finite graph expressions we measure derivational space by the largest input-output interface of an intermediate raw term. For every finite doubly ranked edge alphabet $\Sigma$, we prove that equal closed expressions of pattern width at most $k$ are joined by a derivation in which every step applies an equation in either direction and every intermediate width is at most a computable $B_\Sigma(k)$, independently of graph size. The derivation uses only the structural magmoid laws and the fifteen finite-graphoid schemes. The construction compiles each expression through protected cores and finite routing windows to an encoding-canonical representative $\operatorname{NF}_k$ of width at most $4k+4$. We call this property bounded equational coherence. We also prove $\operatorname{bw}(F)\le\operatorname{patw}(F)\le4(\operatorname{tw}(F)+1)$ whenever the underlying simple graph has at least two edges, separate layered linear from branching expressions on cliques, and provide machine-checkable witnesses and finite invariants for the first five nontrivial clique values.