append_assoc

In the Primitive Recognition Calculus, a finite trace is the inductive history of distinction acts: either empty, or an existing trace extended by one act. Concatenation is defined by recursion on the right argument: appending the empty trace leaves the left trace unchanged; appending an extension peels the last act and re-extends the recursive join.

This is pure syntax for composing recognition histories before any cost, strength, or dynamics is imposed. The same module introduces the extension relation: $U$ extends $T$ when some suffix $V$ satisfies $\mathrm{append}(T,V)=U$. Associativity of append is the algebraic fact that makes that relation a preorder once reflexivity is in hand.

Upstream, the only local ingredient is the recursive definition of append itself; the other import edges are ambient RS units and operators not used in the equality.

Induct on the rightmost trace $V$. If $V$ is empty, both sides reduce to $\mathrm{append}(T,U)$ by the empty clause of append, so reflexivity closes the goal. If $V$ is an extension of a shorter trace by one distinction act, unfold append on both sides; the inductive hypothesis rewrites the inner join, and simplification finishes the equality. No external lemmas beyond the definition of append are required.

This is the R4 associativity step for traces. Downstream it is the rewrite that closes transitivity of extension: if $U$ is $T$ plus suffix $A$ and $V$ is $U$ plus suffix $B$, then $V$ is $T$ plus $\mathrm{append}(A,B)$, and associativity identifies the nested joins. Without it the extension preorder would not be available as a clean partial order on recognition histories.

In the broader foundation stack this keeps multi-step distinction sequences coherent before cost functionals, eight-tick structure, or Hamiltonian emergence are layered on. It is bookkeeping rather than a forcing-chain landmark, but every later argument that treats traces as composable paths relies on it.