substitute
plain-language theorem explainer
If a predicate on endpoints respects object-level sameness at a fixed trace, then sameness licenses substitution: whenever a and b are same at that trace and P holds of a, P holds of b. Anyone building PRC contexts, cost uniqueness, or ledger equalities cites this as the congruence rule. The proof is a one-line application of the RespectsSame hypothesis.
Claim. Let $J$ be an admissible trace judgment and $T$ a finite trace. Let $P$ be a predicate on endpoints that respects $J$-sameness at $T$. If $J$ judges endpoints $a$ and $b$ the same at $T$ and $P(a)$ holds, then $P(b)$ holds.
background
Primitive Recognition Calculus treats recognition as a finite trace of distinction acts. An endpoint is one side of a primitive distinction. A trace is either empty or obtained by extending a prior trace by one distinction act.
A trace judgment $J$ packages object-level sameness and witnessed difference at each trace, with sameness required to be reflexive, symmetric, and transitive (the R5 package). The predicate interface RespectsSame says $P$ is a congruence for that sameness relation at a fixed trace: $J.same, T, a, b$ and $P(a)$ imply $P(b)$.
This module sits in the foundation layer that axiomatizes SameT/DiffT before cost uniqueness and ledger constructions. The doc-comment tags the result as K2.10 and R7: substitution for contexts that respect SameT.
proof idea
Term-mode one-liner. The hypothesis hP : RespectsSame J T P is definitionally the implication
$\forall{a,b},; J.same, T, a, b \to P, a \to P, b$.
Applying hP to the given sameness witness and to ha : P a yields P b. No further lemmas are needed.
why it matters
Substitution is the congruence rule that lets later constructions treat SameT as equality-in-context. Downstream uses include bit-cost normalization on the recognition axis (J_bit_normalized), reduction of bilinear consistency families to d'Alembert form, the $\delta$-act ladder that recovers the calibration invariant $c^2$ in native cost uniqueness, flat log-potentials on the simplicial ledger, and several gravity/particle-sector bridges that rewrite equal endpoints under cost or mass predicates.
In the forcing chain this is pre-physics scaffolding: it does not force $J$, $\varphi$, the eight-tick octave, or $D=3$, but it is the equality hygiene those later steps assume when they rewrite along recognition traces. Without it, SameT would be a bare relation rather than a substitutive judgment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.