empty_append
plain-language theorem explainer
The empty trace is a left identity for syntactic append: concatenating the empty trace on the left leaves any finite trace unchanged. Anyone building the monoid structure of distinction traces (units and associativity) cites this. The proof is induction on the second argument, matching the right-recursive definition of append.
Claim. For every finite trace $T$, $\mathrm{append}(\varepsilon, T) = T$, where $\varepsilon$ denotes the empty trace and append is the syntactic concatenation of traces.
background
In the Primitive Recognition Calculus, a finite trace is the inductive record of distinction acts: it is either empty or obtained by extending a prior trace by one distinction act (K2.4). Traces are the raw histories on which later recognition structure is built.
Append is the syntactic composition operation on traces. By definition it is right-recursive: appending the empty trace on the right returns the left argument unchanged, and appending an extension peels the right-hand constructor and re-extends after the recursive call. Because the recursion is on the second argument, the left-unit law is not definitional and must be proved.
This module develops the basic algebraic facts about that composition (units, associativity, one-step extension) before higher PRC structure is layered on.
proof idea
Induct on the second argument $T$.
- Base case $T = \varepsilon$: both sides are empty;
rflcloses. - Inductive case $T = \mathrm{extend}(U,a)$: unfold
appendon the right-hand constructor, apply the inductive hypothesis that $\mathrm{append}(\varepsilon,U)=U$, and simplify to obtain $\mathrm{extend}(U,a)$.
The argument is forced by the right-recursive shape of append; no external lemmas beyond the definition and the IH are required. Marked @[simp] so later rewrites discharge left-empty concatenations automatically.
why it matters
This is the left half of the unit laws for trace composition in the foundation layer of Primitive Recognition Calculus. Together with the right-unit sibling and the associativity theorem (R4 in the same module), it equips finite traces with a monoid structure under append.
That monoid is the syntactic backbone for composing distinction acts before any cost, strength, or field structure is imposed. Downstream work that rewrites composite histories, normalizes empty prefixes, or treats traces as free monoid words depends on these unit laws being simp-ready.
No parent theorems currently list this declaration as a direct dependency in the graph, so its immediate role is local algebraic hygiene inside the Basic module rather than a named forcing-chain step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.