RespectsSame
plain-language theorem explainer
A predicate on endpoints is said to respect object-level sameness at a fixed trace when it is invariant under that sameness relation. Anyone proving substitution or congruence lemmas for the primitive recognition calculus cites this. The body is a one-line universal property: same endpoints transfer the predicate.
Claim. Fix an admissible trace judgment $J$, a finite trace $T$, and a predicate $P$ on endpoints. $P$ respects sameness of $J$ at $T$ when, for all endpoints $a,b$, if $J$ judges $a$ the same as $b$ at $T$ and $P(a)$ holds, then $P(b)$ holds.
background
In the primitive recognition calculus, an endpoint is one side of a primitive distinction. A finite trace is built from the empty trace by successive distinction acts. An admissible trace judgment surface packages object-level sameness and witnessed difference at each trace, together with the reflexivity, symmetry, and transitivity obligations on sameness (R5).
Sameness is therefore an equivalence relation on endpoints at each fixed trace. Predicates used as contexts in substitution must be well-defined on those equivalence classes: if two endpoints are judged the same, the predicate cannot distinguish them.
The local module develops Same/Diff judgment structure (K2.6–K2.8) and the substitution rule that depends on this invariance condition.
proof idea
Definitional unfolding only. The predicate is the Prop $\forall,a,b,; J.\mathrm{same},T,a,b \to P(a) \to P(b)$. No lemmas are applied; downstream theorems simply apply a hypothesis of this type.
why it matters
This is the side condition for K2.10 / R7 substitution. The immediate consumer is substitute, which states that if a context respects sameness at $T$, then sameness of endpoints transfers the context from one endpoint to the other. Without an explicit respects-sameness gate, substitution would be unsound for arbitrary predicates.
In the broader Recognition foundation, this keeps object-level equality on the trace judgment surface congruent with propositional contexts, so later forcing and composition steps can treat SameT as a genuine equivalence usable inside proofs rather than a bare relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.