extends_refl
plain-language theorem explainer
Every finite recognition trace extends itself under the suffix-extension relation. Citation target for anyone building a reflexive expression order on PRC traces, or inducting on orbit-position traces. Proof is a one-line existential: the empty suffix witnesses reflexivity via the append-empty identity.
Claim. For every finite recognition trace $T$, the extension relation holds of the pair $(T,T)$: there exists a suffix trace $V$ such that appending $V$ to $T$ recovers $T$.
background
In the Primitive Recognition Calculus, a finite trace is the inductive type of empty history or a prior trace extended by one distinction act. Concatenation of traces is the associative append operation, with empty as two-sided unit.
Extension is the induced prefix order: $U$ extends $T$ when some suffix $V$ satisfies $\mathrm{append}(T,V)=U$. This is the K2.5 relation used to compare recognition histories. Reflexivity is the first structural law (R4) for that order; the companion R4 item is transitivity.
The local module develops the bare calculus of distinction acts, sides, endpoints, and traces before cost or dichotomy results are layered on.
proof idea
Term proof. Instantiate the existential in the definition of extension by the empty trace. The resulting equality $\mathrm{append}(T,\emptyset)=T$ is definitional (or the already-proved empty-right-unit law), discharged by rfl. No induction and no case split on $T$.
why it matters
Supplies the reflexivity half of the expression order on PRC traces. Downstream, prcFormalSystem_exprReflexive is literally fun T => extends_refl T, which is the hypothesis needed for the δ4 headline: distinction is not optional except for the fully degenerate foundation that distinguishes nothing.
Also closes the zero case of orbitPositionTrace_add_extends_left in native-cost uniqueness: adding the zero offset leaves the orbit-position trace unchanged, so extension holds by reflexivity. That lemma feeds the uniqueness argument for the native cost along recognition orbits.
Within the foundation layer this is pure order scaffolding for the forcing chain's recognition calculus, not yet a physics constant claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.