sameSetoid
plain-language theorem explainer
At a fixed finite trace, object-level endpoint equality (SameT) is packaged as a Lean setoid on endpoints. Anyone building endpoint trace-classes or quotienting by recognition-sameness cites this. The body just installs the reflexivity, symmetry, and transitivity witnesses already required of an admissible trace judgment.
Claim. Given an admissible trace judgment $J$ and a finite trace $T$, the object-level equality relation $\mathrm{Same}_T$ on endpoints forms a setoid: its underlying relation is $J$'s $\mathrm{Same}$ at $T$, and the equivalence laws are exactly $J$'s reflexivity, symmetry, and transitivity proofs for that relation.
background
In the primitive recognition calculus, an endpoint is one side of the primitive distinction (K2.3). A finite trace is built inductively: empty, or extended by one distinction act (K2.4). Equality and difference of endpoints are not absolute; they are judged relative to a trace.
An admissible trace judgment (K2.6–K2.8) supplies two families of propositions: $\mathrm{Same}_T(a,b)$ (object-level equality at trace $T$) and a witnessed-difference predicate. Admissibility includes the equivalence laws for $\mathrm{Same}_T$: reflexivity, symmetry, and transitivity at every trace (R5 and companions).
This module turns that relational data into Lean’s Setoid/Quot infrastructure so endpoints can be identified precisely when $\mathrm{Same}_T$ holds.
proof idea
Definitional packaging, not a derived theorem. The setoid relation is set to $J.\mathrm{same},T$. The iseqv record is filled pointwise from the judgment’s own witnesses: reflexivity via same_refl_proof, and symmetry/transitivity by introducing the endpoints and hypotheses then applying same_symm_proof and same_trans_proof at $T$. No extra algebra is performed.
why it matters
This is the K2.11 bridge from the SameT judgment surface to quotient types. Downstream, EndpointClass is defined as the quotient of endpoints by this setoid, and endpointClassOf is the canonical class map via Quot.mk. Those classes are the objects on which later recognition calculus reasons about “the same endpoint up to the trace,” rather than raw sides of the distinction.
In the broader foundation stack, endpoint classes sit under the primitive recognition calculus that feeds the forcing chain and the recognition composition law; without a setoid, SameT remains a bare Prop and cannot support class-level constructions used later in the quotient module (e.g. class equality from SameT, and lifts off the quotient).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.