Extends
plain-language theorem explainer
Trace extension is the prefix relation on finite recognition traces: U extends T when U is T followed by some (possibly empty) suffix. Anyone working the Primitive Recognition Calculus, formal-system embeddings, or cost uniqueness on independent decompositions cites it. The body is a one-line existential definition via syntactic append.
Claim. For finite traces $T$ and $U$, $T$ extends to $U$ when there exists a (possibly empty) suffix trace $V$ such that appending $V$ to $T$ yields $U$.
background
In the Primitive Recognition Calculus, a finite trace is the empty history or a history extended by one distinction act (a directed cut between the two primitive endpoints). Traces are the syntactic carriers of successive recognition steps.
Append is the inductive concatenation of two traces: appending the empty trace leaves the left factor unchanged; appending an extended right factor recurses and then adds the final distinction act. Extension is the induced prefix relation: $U$ is an extension of $T$ precisely when some suffix witnesses $T$ as an initial segment of $U$.
The local setting is the basic PRC module (K2.4–K2.5, R3–R4): traces, one-step extension, and the algebraic laws of append that make extension a preorder.
proof idea
Pure definition: the proposition is the existential $\exists V,,\mathrm{append}(T,V)=U$. No tactics or lemmas are invoked at the definition site. Downstream reflexivity takes the empty suffix; transitivity concatenates the two witnessing suffixes and uses associativity of append.
why it matters
Extension is the order skeleton of PRC histories. It feeds reflexivity and transitivity (R4), so extension is a preorder on traces, and it appears in length comparisons used by inevitability instances.
Formal-system structure and PRC embeddings require a preserved expression-extension relation; this definition is the native source of that relation. Cost-from-distinction uniqueness on independent decompositions also depends on it when configurations are built by successive distinction acts.
Within the broader forcing picture, traces record the discrete recognition steps whose eight-tick octave and $D=3$ geometry are forced later; extension is the minimal compositional glue holding those histories together.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.