append_extend

In the Primitive Recognition Calculus, the basic object-level move is a distinction act (denoted $\delta$ at the object level). A finite trace is the free inductive history built from those acts: either empty, or obtained by extending a prior trace by one more distinction act.

Append is the syntactic composition of two such histories. By definition it is recursive on the second argument: appending anything to the empty trace leaves it unchanged, and appending $T$ to an extended trace $\mathrm{extend}(U,a)$ is defined to be $\mathrm{extend}(\mathrm{append}(T,U),a)$. The present statement is exactly that second clause, packaged as a simp lemma so later rewrites can fire on composite traces without unfolding the definition by hand.

The local module builds the algebraic scaffolding (append, empty laws, associativity, the Extends relation) before any dynamics or cost is imposed.

One-line definitional proof. The right-hand side is literally the second pattern-matching clause in the definition of append, so both sides reduce to the same constructor term and rfl closes the goal. No lemmas are invoked.

This is the computational engine of trace composition in the foundation layer of Recognition Science. Without a simp-ready form of the recursive clause, later identities (empty laws, associativity of append, reflexivity of Extends) cannot rewrite cleanly. Those identities equip the free monoid of distinction histories that underwrites the primitive recognition calculus before the forcing chain (T0–T8), the J-cost, or the eight-tick octave is introduced.

No downstream theorem currently depends on this declaration in the graph, so its role is infrastructural: it keeps the syntactic monoid of traces definitionally coherent. It does not itself touch mass ladders, $\alpha$, or dimensional forcing.