append
plain-language theorem explainer
Syntactic concatenation of two finite recognition traces: the distinction acts of the first, then those of the second. Anyone building the monoid of traces, the Extends relation, or ledger past-addressability cites this. Defined by structural recursion on the second argument (empty is a right unit; extend peels one act and recurses).
Claim. Given finite traces $T$ and $U$ (each empty or built by successive distinction acts), $\mathrm{append}(T,U)$ is the trace whose acts are those of $T$ followed by those of $U$. Equivalently: $\mathrm{append}(T,\varepsilon)=T$ and $\mathrm{append}(T, U{::}a)=\mathrm{append}(T,U){::}a$.
background
In the Primitive Recognition Calculus, a finite trace is the inductive type of K2.4: either empty, or obtained by extending a prior trace by one distinction act. Distinction acts are the atomic recognition steps; traces are finite histories of such steps.
Append is the pure syntactic composition of two such histories. It does not interpret acts physically; it only glues sequences. The local module builds the basic algebra of traces (units, associativity, the Extends prefix relation) before any dynamics or cost is imposed.
Upstream, Trace is the carrier; the various U and T names in the dependency graph are unrelated constants (RS units, evolution operators, field towers) that share identifiers but are not used in this definition's body.
proof idea
Not a theorem: a recursive definition on the second argument. Base case: appending the empty trace returns the first trace unchanged. Inductive case: if the second trace is an extension by act $a$, recurse on the prefix and re-extend by $a$. The two simp lemmas append_empty and append_extend are definitional equalities from these clauses.
why it matters
This is the composition law that makes traces a monoid and underwrites K2.5 Extends ($U$ extends $T$ iff some suffix $V$ satisfies $\mathrm{append}(T,V)=U$). Downstream it feeds append_assoc (R4), the unit laws, extends_trans, length comparisons under extension, and ledger past-addressability (past_addressable_at), where committed history is read as a stable prefix under further commits. In the Recognition framework it is the syntactic backbone for ordered recognition histories before J-cost, the eight-tick octave, or continuum limits enter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.