append_empty
plain-language theorem explainer
Right-unit law for finite traces: appending the empty trace on the right leaves any trace unchanged. Cited by anyone building the monoid (or free-composition) structure on Primitive Recognition Calculus traces. Proof is pure definitional reflexivity from the first clause of append.
Claim. For every finite trace $T$, appending the empty trace on the right is a no-op: $\mathrm{append}(T,\varepsilon)=T$.
background
In the Primitive Recognition Calculus, a finite trace is the inductive type of empty history or a history extended by one distinction act (K2.4). Distinction acts are the atomic recognition steps; traces are their finite concatenations.
Append is the syntactic composition of two traces, defined by recursion on the right argument: the empty right factor returns the left factor unchanged, and an extended right factor pushes the extension outside a recursive append. That first clause is exactly the right-unit equation.
The local module builds the basic algebra of traces (step, append, extends) before strength and exp/log field material is layered on.
proof idea
One-line definitional proof. Unfolding append on a right-hand empty trace matches the first equation clause, so both sides are definitionally equal and rfl closes the goal. Marked @[simp] so the unit law fires automatically in later rewrites.
why it matters
Establishes the right unit for trace composition, a prerequisite for treating traces as a monoid under append (with the matching left-unit and associativity siblings in the same file). In the Recognition framework this is bookkeeping infrastructure for the Primitive Recognition Calculus: finite histories of distinction acts must compose with neutral empty history before one can talk about extension orders, strength, or forcing-chain material that sits above PRC. No downstream consumers are wired yet in the graph; the lemma is scaffolding for that monoid layer rather than a physics identity (not T5–T8, RCL, or mass-ladder).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.