prcFormalSystem_exprReflexive

In the Primitive Recognition Calculus, a finite trace is either empty or obtained by adjoining one distinction act. Trace extension is the natural "is-a-prefix-of / can-be-extended-to" order on traces; the Basic module records that this order is reflexive (R4): every trace extends itself via the empty continuation.

A formal system packages tokens, expressions, a distinction relation on tokens, and an expression-extension relation. PRC itself is the minimal such package: tokens are endpoints, expressions are finite traces, distinction is inequality of endpoints, and expression extension is trace extension.

ExprReflexive is the mild structural hypothesis that every expression extends itself. It holds for any "derivable-from", inclusion, or prefix-style order. The surrounding module uses it to run the $\delta$ distinction dichotomy on concrete foundations.

Term-mode proof. Unfold reflexivity of the expression order on PRCFormalSystem: the claim is that every expression (i.e. every Trace) is related to itself by Trace.Extends. Discharge each instance by the Basic lemma that trace extension is reflexive, which builds the witness as the empty continuation with a trivial equality.

This discharges the reflexivity hypothesis for the named PRC foundation, so the $\delta$4 headline applies to it: distinction is not optional except for the fully degenerate case. The parent results in this module (distinction_not_optional, distinction_dichotomy, and the named-foundations non-degeneracy corollaries) all take expression-order reflexivity as input; without this instance, PRC could not be fed into that chain.

In the broader Recognition framework this is foundation-layer hygiene rather than a forcing-chain step (T5--T8). It confirms that the minimal calculus of distinction acts already sits inside the class of foundations to which the dichotomy applies, so degeneracy is the only escape from realizing $\delta$.