PaperlayerView exact revision on arXiv

Source-linked AI summary

Width-Bounded Equational Derivations for Finite Graph Expressions

Antonios Kalampakas

arXiv:2609.08325v1cs.LO

TL;DR

Ordinary completeness guarantees equality paths but does not bound the intermediate interfaces they require. This paper proves bounded equational coherence by compiling equal narrow closed expressions to a common canonical representative. The resulting width bound is independent of graph size, while the paper also relates pattern width to familiar graph-width parameters.

  • Problem

    Ordinary completeness gives no bound on intermediate interfaces, leaving open whether equal narrow graph descriptions can be connected without interfaces that grow with graph size.

    Source: §1 · p. 1

  • Method

    The proof protects cores and uses local normalization and parse-aligned interpolation to compile each expression to a common encoding-canonical representative using the fixed equations.

    Source: §4.1 · p. 7, §4.2 · p. 7, §4.3 · p. 14

  • Results

    Equal closed expressions of pattern width at most k are connected by a derivation of computably bounded width independent of graph size.

    Source: §4.4 · p. 15, §7 · p. 18

  • Takeaways & Limitations

    The resulting parameter reflects familiar structural width while retaining information about the expression tree.

    Source: §7 · p. 18

    The computable bound is obtained by finite proof search rather than a useful closed formula; no derivation-length bound or efficiency claim is given.

    Source: §7 · p. 18

Abstract

from arXiv · show

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.

1. Introduction

The introduction asks whether equal narrow graph descriptions can be connected without large intermediate interfaces, since completeness alone gives no resource bound. It presents bounded equational coherence for the unrestricted finite-graphoid presentation and relates pattern width to graph structure.

1. Introduction

  • Earlier finite-graphoid completeness establishes graph-value equality but does not bound derivational space.Related bounded-treewidth presentations build fixed interface bounds into specialized syntax, whereas this work uses unrestricted syntax and asks for a uniform bound in endpoint width.Source: §1 · p. 1
  • Equal closed expressions of pattern width at most k can reach a graph-value-selected representative through width at most BΣ(k), independently of graph size.The derivation uses the structural magmoid laws and fifteen finite-graphoid schemes; the bound is computable for fixed k and finite Σ.Source: §1 · pp. 1–2
  • The proof protects live vertices, locally normalizes a bounded edge-partition tree, and compares trees by four-cell switches.The containment ∂(X ∩ Y) ⊆ ∂X ∪ ∂Y prevents interface accumulation.Source: §1 · p. 2
  • bw(F) ≤ patw(F) ≤ 4(tw(F) + 1) for graphs whose underlying simple graph has at least two edges.The introduction also reports layered linear clique widths between 2n − 3 and 2n, branching-term width at most n + 1, and verified patw values 4, 5, 6, 6, 6 for K3 through K7.Source: §1 · p. 2
  • Unlike monoidal width, pattern width belongs to a chosen raw expression tree, and the bound concerns peak width along an equality path.The introduction distinguishes this from small-term reachability, which bounds target size, and from normal-form approaches that do not bound paths between supplied expressions.Source: §1 · p. 2

2. Preliminaries: the axiomatization of graphs

The preliminaries set up a typed raw-term syntax and its graph semantics. Structural laws and finite-graphoid equations present equality of finite graph values, while the word problem is tied to graph isomorphism.

2. Preliminaries: the axiomatization of graphs

  • A magmoid has typed composition and parallel sum, with associativity, unit, and interchange laws generating the structural equations B.Modulo B, raw expressions form the free magmoid, and pattern width remains a property of a raw representative.Source: §2 · p. 2
  • Finite graph values are boundary-preserving isomorphism classes of labeled hypergraphs with ordered begin and end sequences.Composition glues end to begin positionally, while sum takes disjoint union and concatenates interfaces.Source: §2 · p. 3
  • The fifteen finite-graphoid schemes, together with B, make graph-value equality equivalent to derivability.The quotient magmoid is isomorphic to the magmoid of finite hypergraphs; the schemes are equations between fixed raw terms.Source: §2 · pp. 3–4
  • Under the stated expanded-arity encoding and default alphabet, the word problem is polynomial-time many-one equivalent to graph isomorphism.The word problem rejects expressions of different ranks and otherwise asks whether they are equivalent under B and the finite-graphoid equations.Source: §2 · p. 4

3. Pattern width

Pattern width measures the largest input-output interface of any subterm in a chosen raw expression. The section relates this tree-sensitive measure to constructions and describes a finite saturation procedure for testing width bounds.

3. Pattern width

  • patw(t) is the maximum a + b over subterm occurrences of rank (a, b), including leaves and t itself.For a graph F, patw(F) is minimized over expressions denoting F; this minimum is finite by surjectivity of evaluation.Source: §3 · p. 4
  • Layered linear expressions use fixed-bracketing parallel blocks composed in a left comb, unlike unrestricted branching expressions.The definition preserves the raw parenthesization when width is computed and minimized.Source: §3 · p. 4
  • Copy and merge make pattern width tree-like: paths have width at most 2, while out-stars and directed cycles have width at most 4.Disjoint union width is at most the maximum component width, and patw(Kn) = Θ(n).Source: §3 · p. 5
  • A closed subterm's internal vertices remain distinct in the whole value, with all incident edges inherited from that subterm.The surrounding context can identify boundary nodes, but not nodes internal to the subterm.Source: §3 · p. 5
  • Saturation states record placed edges, finalized vertices, live boundary labels, and ordered boundary words capped at total length W.Transitions combine states by sum or composition, enforce disjointness and boundary guards, and finalize a label after its last live class vanishes once incident edges are placed.Source: §3 · p. 5
  • Finite saturation terminates and accepts exactly when a target has an expression of width at most W.For undirected targets, both orientations of each edge are seeded; the vertexless target is accepted directly as e0.Source: §3 · p. 5

4. Bounded normal forms and bounded coherence

This section develops width-sensitive normalization for closed graph expressions of bounded pattern width, using protected cores, finite local routing schemes, and parse-aligned compilation. It constructs encoding-canonical representatives and shows that equal expressions can be connected with computable bounds on intermediate widths, using bounded tree and four-cell interpolation.

4.1. Derivation width and boundary control.

  • Global backfold normalization can require a rank-sum-2m subexpression, so width control instead uses holes that prevent collecting all graph letters into one parallel layer.Derivation width is the maximum pattern width among all raw expressions in the derivation.Source: §4.1 · pp. 6–7

4.2. Protected cores and local normalization.

  • Discrete normalization terminates at a unique record, preserves graph-bearing rank-zero holes, and renders six-slot windows of load k with load at most 12(k + 1).Each rendered local step uses at most four aggregate holes once.Source: §4.2 · p. 9
  • For any valid q-local datum, instantiated endpoints have width at most max{w, 4q + 4}, without inspecting or duplicating carriers.Here w bounds substituted holes, exposed scalars, and opaque carriers; same-type replacement preserves ancestor ranks.Source: §4.2 · p. 9
  • Compatible discrete contexts with the same protected data are connected within a computable width bound, without changing or duplicating any core.Compatibility requires the same ordered linear opaque holes and protected partition, outer interface, and number of discrete-only closed components.Source: §4.2 · p. 9
  • Every expression of pattern width at most k reaches a frame of computable width fΣ(k), with a reduced core of width at most 4k + 4.The frame restores the ordered boundary, including repetitions, while preserving every edge occurrence.Source: §4.2 · p. 10

4.3. Parse-aligned compilation.

  • A closed expression of pattern width at most k yields an edge-partition tree whose boundary widths are at most k.This is a combinatorial extraction from the pruned and suppressed parse tree, not permission to delete discrete parse pieces from the raw expression.Source: §4.3 · p. 11
  • In parse-aligned routing, each vertex router is connected, and it traverses a tree edge exactly when that vertex lies on the corresponding atom boundary.Folding and pruning produces the scalar-scheduled canonical routing, including the isolated-vertex suffix.Source: §4.3 · p. 11
  • When skeleton cuts and atom rank sums are at most k, folds and prunes reach each minimal spanning subtree within load 12(k + 1), and finite local schemes are effectively enumerable.A vertex with no incidence flags is represented by a tagged zero-leg block; the parse compiler uses M12(k+1).Source: §4.3 · p. 11
  • The recursive compiler preserves the graph value, edge occurrences, incident vertices, and boundary order, and its renderer conversion introduces no positive-rank bank.The compiler invariant also identifies end vertices exactly with vertices on the relevant subgraph boundary.Source: §4.3 · p. 12
  • Every closed expression of pattern width at most k can be compiled into a parse-aligned tree realization with a computable width bound cΣ(k).The parse-aligned compilation reassembles the original endpoint without enlarging that bound.Source: §4.3 · p. 13

4.4. Tree interpolation and canonical normal forms.

  • Quadrant interpolation transforms one edge-partition tree into another using clusters from either tree or their intersections, with every intermediate boundary at most p + q.The interpolation uses four-cell switches and avoids taking all intersections at once, which need not form a laminar family.Source: §4.4 · p. 14, §4.3 · p. 14
  • For each finite alphabet Σ, row and column forms of any r-bounded four-cell assembly are connected by derivations within a computable width bound dΣ(r).The proof reduces the cases to an effective finite set of load at most 12(r + 1).Source: §4.4 · p. 14
  • The normal form is the least raw serialization among bounded-width compiled presentations, depends only on the graph isomorphism class, k, and fixed syntax, and has width at most 4k + 4.It preserves labels, directions, multiplicities, loops, and isolated vertices.Source: §4.4 · p. 15
  • Equal closed expressions of pattern width at most k admit an equational derivation whose intermediate width is bounded by a computable function of k and Σ.Both expressions derive to the same bounded normal form, and the derivation from one can be reversed.Source: §4.4 · p. 15

5. Calibration with graph width

For graphs with at least two underlying simple edges, pattern width is at least branchwidth, and a supplied width-k tree decomposition yields an expression of width at most 4(k + 1). The section also distinguishes support width and gives a path-decomposition compiler.

Calibration with graph width

  • A three-way vertex partition construction gives middle sets of size at most ⌈2n/3⌉.The construction grafts three edge decompositions supported on pairwise unions of the vertex classes.Source: §5 · p. 16
  • For graphs with at least two underlying simple edges, bw(F) ≤ patw(F); a supplied width-k tree decomposition yields a closed expression of width at most 4(k + 1).At a join, the compiled pieces share only the join-bag vertices, and the join uses 2(k + 1) wires.Source: §5 · p. 16
  • The parse-tree lower bound retains one occurrence per simple edge and bounds each resulting middle set by the subterm interface rank sum.The resulting tree is a branch decomposition, giving bw(val(t)) ≤ patw(t).Source: §5 · p. 16
  • A path decomposition avoids join shuffles: bag gadgets are composed in path order using a fixed left-comb parenthesization.The section identifies this construction as a path-decomposition compiler.Source: §5 · p. 17
  • For support width, max{bw(F), 2} ≤ patw*(F) ≤ patw(F), with sharpness examples reported.Support width counts distinct final boundary vertices.Source: §5 · p. 17

6. Linear and unrestricted constructions

The section relates linear-fragment width to linear width and gives bounds and verified values for cliques. It also distinguishes layered linear expressions from branching expressions on complete binary trees.

6. Linear and unrestricted constructions

  • Pattern width is at most 8 on complete binary trees, while layered linear width is unbounded there.The proof sketch connects unbounded layered width to unbounded pathwidth.Source: §6 · p. 17
  • For graphs with an edge, the linear-fragment bounds relate patwlin to linear width: 2 lw(F) − 1 below and 2 lw(F) + 4 above.Refining a layered term to an edge order enlarges its boundary by at most a factor of three.Source: §6 · p. 17
  • 2n − 3 ≤ patwlin(Kn) ≤ 2n, while patw(Kn) ≤ n + 1 for n ≥ 3.For K3 through K7, the pattern-width values are (4, 5, 6, 6, 6).Source: §6 · p. 17
  • Lane-spiral expressions for 5 ≤ n ≤ 24 have directed values in Ori(Kn) and width exactly n + 1.The reproducibility package checks clique witnesses and canonical representative sets for K3 through K7.Source: §6 · p. 17

7. Conclusion

The conclusion presents bounded normal forms as a local resource statement: equal narrow graph expressions can be connected without interfaces whose size depends on the graph. It also states qualitative limits and situates the parameter relative to structural graph width and expression trees.

7. Conclusion

  • The bounded-normal-form theorem gives a local resource statement for equal narrow graph expressions, and protected cores with intersection interpolation explain the locality mechanism.Calibration and clique results show that the parameter reflects familiar structural width while retaining information about the expression tree.Source: §7 · p. 18
  • The bound BΣ is obtained by finite proof search without a useful closed formula; no derivation-length bound or efficient normal-form selection is claimed.Extensions to open values, the support-width/pattern-width gap, and the asymptotic value of patw(Kn) remain open.Source: §7 · p. 18

Supplementary proofs

Notation and conventions.

  • The syntax uses raw rank-(p, q) expressions over XΣ, built from alphabet letters, units, composition, and parallel sum.XΣ consists of Σ and the five discrete generators.Source: Notation and conventions · p. 19
  • Pattern width is the maximum a + b over subterm occurrences of rank (a, b); classical graph-width parameters apply to the underlying simple graph.For directed multigraphs, that graph is formed by forgetting directions, deleting loops, and merging parallel edges while retaining vertices.Source: Notation and conventions · p. 19

S1. Expanded calibration audit with branchwidth and treewidth

This section calibrates pattern width against branchwidth and treewidth, then gives constructive decomposition-based compilers. It also sharpens the linear-fragment result and identifies an open support-width question and the computational archive’s scope.

Tree-decomposition compiler

  • A width-k tree decomposition yields in polynomial time an expression for F of width at most 4(k + 1).The construction assigns edge occurrences to bags and builds expressions along the decomposition; loops, parallel edges, and opposite directed edges are handled separately.Source: S1. Expanded calibration audit with… · pp. 21–22

Path decompositions

  • For one-orientation-per-edge representations of simple graphs, a path decomposition gives patwlin(F) ≤ 4(pw(F) + 1) and a layered linear expression.The path construction has no join shuffle, which is the source of the factor 4 in the general tree-decomposition audit.Source: S1. Expanded calibration audit with… · pp. 21, 23

Calibration with treewidth

Normal forms from tree decompositions

  • Compiler outputs from different width-t tree decompositions, with the same orientation and labeling, connect through the same selected normal form within BΣ(k).The compiler output has exact value F and pattern width at most k = 4(t + 1).Source: S1. Expanded calibration audit with… · p. 23

Computational archive

  • The computational archive checks clique witnesses and the lane-spiral family, but does not independently implement either decomposition compiler.The tree- and path-decomposition bounds are established by symbolic width audits.Source: S1. Expanded calibration audit with… · p. 24

Support-width calibration

  • Sharp support calibration remains open: max{bw(F), 2} is a lower bound, while patw*(P3) and patw*(2K2) equal 2 despite branchwidths 1 and 0.The paper asks whether this lower bound is exact for every graph with at least two edges, or what the optimal gap is.Source: S1. Expanded calibration audit with… · p. 24

S2. The linear fragment: exact calibration and the clique lower bound

This section calibrates width for the linear fragment against linear-width and proves a clique lower bound. It contrasts unbounded optimal linear width with a tree-shaped construction of width 8, establishing an infinite separation between the linear and general fragments.

S2.2. The clique lower bound.

S2.1. Stages, references, and pieces.

  • In a linear expression, every started but incomplete vertex retains a cut reference, and the layer capacity bound limits edges placed to c_(j-1) - P_j.Here P_j counts vertices referenced at the previous cut that remain incomplete at stage j.Source: S2.1. Stages, references, and pieces · pp. 25–26

S2.3. Elementary chains and linear-width.

  • For simple graphs F with at least one edge, elementary-chain width lies between 2 lw(F) - 1 and 2 lw(F) + 4, while every linear expression satisfies lw(F) <= 3 patw(t).The factor-two calibration applies to elementary chains, not unrestricted expressions.Source: S2.3. Elementary chains and linear-width · pp. 28, 30

S2.4. Separation of the fragments.

S3. Unrestricted clique bounds and certified values

The lane-spiral construction gives unrestricted clique pattern width at most n + 1, while machine-checked certificates establish exact values for K3 through K7. The results also separate linear from branching expressions on cliques and leave the asymptotic clique value open.

Certified clique values

  • Machine-verified upper witnesses and inductive-invariant lower certificates establish the unrestricted pattern widths of K3 through K7.The K7 witness has width 6, seven vertices, and all 21 unordered edges exactly once.Source: S3. Unrestricted clique bounds and… · p. 31

Unrestricted clique bounds

  • patw(Kn) ≤ n + 1 for n ≥ 3, via a uniform lane-spiral family of raw expressions.The construction schedules clique edges using bounded composite blocks and distributes live references between descending and ascending lanes.Source: S3. Unrestricted clique bounds and… · pp. 31–32

Lane-spiral construction

  • The lane-spiral recursion places each path edge at vertex birth and schedules every chord once, while preserving an ordered wire layout.Its width audit bounds every subterm by n + 1; the construction has width exactly n + 1 for 5 ≤ n ≤ 24.Source: S3. Unrestricted clique bounds and… · pp. 32–34

Support-width comparison

  • The unrestricted support-width lower bound patw*(Kn) ≥ ⌈2n/3⌉ contrasts with the pattern-width upper bound n + 1.Thus the elementary-chain doubling estimate does not extend to unrestricted expressions.Source: S3. Unrestricted clique bounds and… · pp. 31, 34

Linear versus unrestricted expressions

  • On cliques, the linear fragment exceeds the unrestricted fragment by at least n − 4, so their width gap grows without bound.The comparison uses the linear lower bound 2n − 3 and the unrestricted upper bound n + 1.Source: S3. Unrestricted clique bounds and… · pp. 31, 34

Certified clique values

  • The certified equality patw(K7) = 6 refutes both candidate laws patw(Kn) = n + 1 and patw(Kn) = bw(Kn) + 2 within the tested range.Determining the asymptotic clique value remains open.Source: S3. Unrestricted clique bounds and… · p. 34

S4. Explicit local normal-form schemes

This section develops finite local rewrite schemes and deterministic rendering procedures for normalizing graph-expression windows, contexts, and compiler derivations to prescribed canonical endpoints. It establishes their validity and coverage, audits arities and intermediate interface widths, and preserves protected ports, routing order, and scalar factors.

S4.1. Naturality and the padding audit.

  • For patw(u) ≤ n, structural induction bounds N(u)'s width by effective xΣ(n), since child derivations run sequentially rather than accumulating with syntax depth.The construction uses finite maxima for base exchanges and structural transports; padded contexts expose at most two child interfaces and two one-wire routing blocks.Source: S4.1. Naturality and the padding audit · p. 35
  • Rank-preserving substitution of formal boxes by terms uh yields an effective width estimate and does not change ancestor ranks.Each substituted (A15) step is replaced by N(uh), while the other derivation steps remain contextual instances of the same law.Source: S4.1. Naturality and the padding audit · pp. 35–36

S4.2. Names, frames, and edge-free terms.

  • The canonical reduced named core retains one ordered output per boundary-equality block, and its direct frame is the fixed raw representative.The name and the core followed by Repβ have boundary-preserving isomorphic values; the coarser final-equality partition and live classes select routers but authorize no merge.Source: S4.2. Names, frames, and edge-free terms · p. 37
  • An edge-free term is equivalent to Can(βd, cd), determined by its boundary-equality partition and count of vertices without boundary occurrences.Normalizing maximal edge-free subtrees first records each isolated vertex as one z factor before pruning.Source: S4.2. Names, frames, and edge-free terms · p. 37

S4.3. The six rendered window kinds.

  • Leaf frames use explicit named cores or exact canonical routers, while binary windows cover two graph-bearing children and cases with one or both children edge-free.The edge-free cases use typed routing data and rank-zero suffix holes, with output-only blocks allowed.Source: S4.3. The six rendered window kinds · pp. 38–39
  • When both children are edge-free, composition-state steps extract isolated-vertex scalars incrementally, while graph-bearing rank-zero cores remain opaque and are never replaced by z.After combining child suffixes, the completed suffix is treated as one opaque term rather than exposing its full scalar list.Source: S4.3. The six rendered window kinds · p. 39
  • Fold and prune windows preserve complementary holes and outer order while handling nullary cases; prune removes a terminal strand and uses scalar counts in {0, 1, 2}.A scalar increment is included exactly when removing the terminal block would otherwise delete a component with no protected or outer port.Source: S4.3. The six rendered window kinds · pp. 39–40
  • The four-cell switch stages shared vertex blocks through row and column routers, then restores prescribed outer order while closing other blocks and appending the same scalar tag.Every occupied formal hole, including a graph-bearing rank-zero hole, occurs once at each endpoint.Source: S4.3. The six rendered window kinds · pp. 40–41
  • One- and two-scalar moves reorder rank-zero factors into a fixed right-associated suffix while exposing at most two scalar holes per move.The displayed scalar interchange s1 ◦ s2 ↔ s1 □ s2 is derived directly from interchange and rank-zero unit laws.Source: S4.3. The six rendered window kinds · p. 41
  • Child scalar suffixes move across composition by explicit interchange and unit steps, then successive scalar moves place factors in the fixed target order.The displayed composition window keeps only the child suffixes or an adjacent factor and opaque remainder visible.Source: S4.3. The six rendered window kinds · p. 42
  • The global state tracks processed components and edges, the active local-window address, carrier and port order, and the suffix cursor and pending scalar.The suffix is read from the fixed parse tree and recomputed after each raw update.Source: S4.3. The six rendered window kinds · pp. 42–43
  • Every displayed carrier has interface load at most k0 = max{r, w}, although its substituted raw term may widen and is bounded separately.Carriers are unchanged addressed subterms or aggregates from one interface; same-type replacement preserves their interface bound.Source: S4.3. The six rendered window kinds · p. 44
  • Local records and raw endpoints are determined from consecutive states, with their partitions fixed by the state updates rather than chosen independently.The record’s ordered carrier lists and placement injections are retained at both endpoints.Source: S4.3. The six rendered window kinds · p. 45
  • A port-free emitted component is represented by an external scalar z before restore or suffix, rather than hidden inside the final composition.The extraction uses interchange and structural-unit equations; the special emit records the component while displaying z externally.Source: S4.3. The six rendered window kinds · pp. 45–46
  • Router normalization proceeds through split, expose, fuse, and emit phases, updating ordered positions and equivalence classes as each incidence is processed.The phase rules transport partitions through stable permutations, join or quotient spider classes, and emit a canonical block for a completed component.Source: S4.3. The six rendered window kinds · p. 46
  • Suffix cleanup reassociates z at entry, moves it past each neighboring carrier, then each scalar factor, decreasing cursor coordinates until the prescribed suffix is reached.The procedure uses fixed local pairs and creates no state for a zero-cursor administrative completion.Source: S4.3. The six rendered window kinds · pp. 47–48
  • Each reachable state denotes a fully expanded raw term with literal carrier occurrences, and successor exposure links actual syntax trees rather than merely equal graph values.The run's terminal term is exactly N(K).Source: S4.3. The six rendered window kinds · pp. 49–51
  • The deterministic run terminates at exactly N(K), retaining surviving partition classes and representing each class absent from EK by one external z.Stable restore orders the outer banks, and terminal exposure restores the prescribed parenthesization.Source: S4.3. The six rendered window kinds · p. 50
  • For fixed (r, w), every local transition has bounded interface load, and its phase, types, placements, partitions, orders, scalar roles, and raw endpoints range over a finite set.The bound applies to the local record, although the number of global tasks may depend on the syntax.Source: S4.3. The six rendered window kinds · pp. 51–52
  • Injective charging of renderer occurrences yields |By| ≤ T + 1, |Bx| ≤ T + 1, and |BxB| ≤ 2T + 1.The base word AA′P(Ix)P(Iy)B has length at most T.Source: S4.3. The six rendered window kinds · p. 51
  • Each of the six templates preserves boundary graph values and each formal hole’s ordered incidence list; order-straightening is a separate W2 subfamily, not a seventh window kind.Source: S4.3. The six rendered window kinds · p. 52
  • Fold and prune pairs preserve protected and outer partitions and scalar counts, while a removed isolated component contributes z; four-cell moves preserve ordered incidences and retain rank-zero holes.A full fold uses merge associativity, with unit and permutation equations for nullary cases; pruning uses unit or counit.Source: S4.3. The six rendered window kinds · pp. 52–53

S4.4. Finite enumeration, coverage, and the arity audit.

  • Finite enumeration tests rendered endpoint pairs by boundary-preserving isomorphism, and completeness [10, Cor. 3] supplies an effective derivation for each retained pair.The finite test preserves labels, ordered hole incidences, outer interfaces, and port-free component counts; substitution then converts proofs to the original alphabet.Source: S4.4. Finite enumeration, coverage,… · p. 54
  • Finite enumeration makes P(q), C(q), and K(q) computable, yielding a computable bound on rendered local endpoints.The functions bound fixed permutation words, canonical routers, and endpoints of local state records, respectively.Source: S4.4. Finite enumeration, coverage,… · p. 54
  • The retained families cover parse alignment, routing normalization, and four-cell switching, including absent cells and occupied rank-zero graph-bearing holes.Routing fold and prune steps reduce duplicate or terminal strands; switching preserves the final partition, survivor order, and scalar tag.Source: S4.4. Finite enumeration, coverage,… · pp. 54, 57
  • Normalization terminates because each outer transition strictly decreases a fixed lexicographically ordered measure of unfinished nodes, tasks, phases, inversions, and scalar-order defects.Individual equation steps inside a retained derivation need not decrease that measure.Source: S4.4. Finite enumeration, coverage,… · p. 56
  • Rendered endpoint width is at most max{w, 4q + 4} for leaf frames, binary routers, folds, prunes, and four-cell switches; scalar moves use max{w, 2}.The scalar suffix-entry and carrier-crossing rows instead give max{w, 2k}.Source: S4.4. Finite enumeration, coverage,… · p. 58
  • Every required parse, fold, prune, or scalar datum is 12(k + 1)-local, while every required four-cell datum is 12(r + 1)-local.These bounds assume the stated incident-bank, atom, carrier, and four-cell staging-load conditions.Source: S4.4. Finite enumeration, coverage,… · pp. 57–58

S4.5. Recursive normalization and exact routing endpoints.

  • Matching contexts with the same ordered holes, labeled cores, port partition, outer interface, and port-free component count normalize to one endpoint via a derivation bounded by computable aΣ(r, w).The contexts have width at most w, with at most r protected core and ordered outer ports; no step duplicates, deletes, or identifies protected ports inside a hole.Source: S4.5. Recursive normalization and… · pp. 58–59
  • Bounded frame straightening equates a named core with its canonical frame representative using width bounded by a computable function of p + q and w.The passage gives a coarse bound charging bends, repetition, naming, and restoration positions.Source: S4.5. Recursive normalization and… · p. 60
  • The routing invariant makes each vertex’s routing multigraph connected, and fold-and-prune steps produce exactly Rsc(G, S, ρ), including its prescribed bank orders and scalar factors.For each closed compiler datum, an effective raw derivation connects Rsc(G, T, ρ) and R(G, T, ρ); its scalar and padded rank-zero steps add no pattern-width load.Source: S4.5. Recursive normalization and… · p. 60
  • Recursive quadrant interpolation preserves inherited plane orders, with every local change represented by a four-cell renderer that also covers two-cell and three-cell cases.The common outer router restores the prescribed boundary order, so a switch does not change the order visible to an ancestor.Source: S4.5. Recursive normalization and… · p. 62
  • Ordered carrier exposure uses associativity to make disjoint interval subwords literal, left-to-right subterms without increasing pattern width.The exposed occurrences have pairwise prefix-incomparable syntax-tree addresses, and reversing the derivation restores the original parenthesization.Source: S4.5. Recursive normalization and… · pp. 62–63

S4.6. A two-edge path.

  • For a two-edge path with rank-(1, 1) labels, the construction has boundary load one and edge-arity load two, giving the stated coarse bound 4r + 4 = 12.The router merges the two representatives and closes the result without exposing all four edge incidences at once; relative spider straightening sends alternative discrete stagings to the same router.Source: S4.6. A two-edge path · p. 63

S5. Encoding details for the equational word problem

The section gives a polynomial-time, isomorphism-invariant encoding of finite simple graphs as closed expressions. Graph isomorphism is preserved by the encoding and, by finite-graphoid completeness, corresponds to equivalence in the raw syntax.

S5. Encoding details for the equational word problem

  • Replacing each undirected edge by both directed arcs preserves graph isomorphism and retains isolated vertices.The construction makes no orientation choice dependent on a vertex ordering.Source: S5. Encoding details for the… · p. 64
  • Each arc gadget adds one arc while returning all vertex wires to their original positions.The construction lists the 2m arcs of D(G), composes their gadgets with persistent vertex wires, then closes the wires; the closed value is D(G).Source: S5. Encoding details for the… · p. 64
  • The construction uses adjacent transpositions to route selected vertex wires, with each padded routing word and its inverse of size O(n^2).The padded edge gadget has size O(n), and the resulting expression is computable in polynomial time.Source: S5. Encoding details for the… · p. 64
  • G ∼= H exactly when val(pG) ∼= val(pH), and finite-graphoid completeness gives the corresponding equivalence in raw syntax.The map from a finite simple undirected graph to a closed expression is computable in polynomial time.Source: S5. Encoding details for the… · pp. 63–64

S6. Expanded finite-saturation audit and certificate semantics

The audit defines finite state systems for bounded-width expressions in directed and underlying-simple target modes, then proves that saturation and symmetry-reduced certificates characterize width bounds. Its certificate checker verifies finite closure conditions and excludes the accepting state.

S6.1. Raw states and legality.

  • A raw state records placed edge occurrences, finalized vertices, live-piece labels, and ordered begin and end boundaries, subject to legality and a rank-sum cap.The realization invariant requires exact endpoint incidences; in underlying-simple mode, each edge occurrence may use either orientation.Source: S6.1. Raw states and legality · p. 65

S6.2. Successor operations.

  • Sum and composition successors combine realizations while preserving endpoint incidences; composition finalizes a vertex only when its live class is unique and all incident edges are placed.The internal-node condition prevents a finalized vertex from later being merged with a distinct live piece of the same target label.Source: S6.2. Successor operations · pp. 66–67
  • Finite saturation contains the accepting state exactly when the target has pattern width at most W, in either directed or underlying-simple mode.In underlying-simple mode, an accepting reconstruction realizes the target graph under some orientation; a vertexless target is handled separately by e0.Source: S6.2. Successor operations · p. 67

S6.3. Symmetry quotient and static certificates.

  • Symmetry-reduced certificates prove patw(F) > W by including all seed orbits, checking successor closure, and excluding the accepting orbit.For underlying-simple targets, both oriented seeds per edge make the conclusion apply to every orientation; the standalone checker verifies the certificate without importing the search engine.Source: S6.3. Symmetry quotient and static… · p. 69

Declarations

  • The audit’s reproducibility package archives code, witnesses, certificates, manifests, logs, replay scripts, and licenses.The package is version 1.1.0 on Zenodo.Source: Declarations · p. 70
Loading 2609.08325v1…