same_trans
plain-language theorem explainer
SameT is transitive on endpoints at any fixed finite trace, for every admissible judgment surface. Anyone treating object-level equality in the primitive recognition calculus cites this. The proof is a one-line projection of the structure's built-in R5 transitivity witness.
Claim. Let $J$ be an admissible trace judgment surface, $T$ a finite trace, and $a,b,c$ endpoints. If $J$ asserts that $a$ is the same as $b$ at $T$ and that $b$ is the same as $c$ at $T$, then $J$ asserts that $a$ is the same as $c$ at $T$.
background
In the primitive recognition calculus, an endpoint is one side of a primitive distinction (left or right). A finite trace is built inductively: empty, or extended by one distinction act. A trace judgment surface packages two object-level relations at each trace: SameT (equality) and DiffT (witnessed difference), together with the R5 axioms that SameT is an equivalence relation at every trace.
The structure field same is the object-level equality predicate; its companion fields supply reflexivity, symmetry, and transitivity proofs. This module (K2.6–K2.8) isolates those properties so later consistency and substitution lemmas can treat SameT as a genuine equivalence without reopening the admissibility package.
Upstream, Endpoint and Trace come from the Basic layer of the calculus; the judgment surface itself is the local carrier of R5.
proof idea
One-line term wrapper. The goal is exactly the conclusion type of the structure field that every TraceJudgment must carry (the R5 transitivity witness). Apply that field to the given trace and the two SameT hypotheses; no further rewriting or case analysis.
why it matters
R5 demands that SameT be an equivalence at each trace. This declaration surfaces the transitivity half as a named theorem, matching the sibling reflexivity and symmetry extractions. Downstream siblings in the same module (consistency of a trace under a judgment surface, RespectsSame, and substitute) rely on having SameT behave like equality so DiffT exclusivity and replacement are well-typed.
In the broader Recognition stack this sits in Foundation, under the primitive recognition calculus that precedes cost, forcing, and the T0–T8 chain. It does not itself force phi, the eight-tick octave, or D = 3; it only hardens the equality fragment those later layers assume when they talk about identified endpoints along a trace. No used_by edges are recorded yet, so its immediate consumers are the in-module consistency and substitution results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.