endpointClassOf
plain-language theorem explainer
Maps an endpoint to its equivalence class under the SameT relation at a fixed trace. Anyone working with quotiented endpoints in the primitive recognition calculus cites this constructor. The body is a one-line Quot.mk against the SameT setoid.
Claim. Given a trace judgment $J$, a finite trace $T$, and an endpoint $a$ (a side of the primitive distinction), return the class $[a]$ in the quotient of endpoints by the SameT relation of $J$ at $T$.
background
In the primitive recognition calculus, an endpoint is a side of the primitive distinction $\delta$ (left or right). A trace is a finite word of distinction acts, built from empty by successive extension. A trace judgment $J$ supplies a SameT relation on endpoints at each fixed trace: two endpoints are related when $J$ judges them the same after $T$.
The setoid sameSetoid J T is exactly that relation, with reflexivity and symmetry taken from the judgment's proofs. The type of endpoint trace-classes is the quotient of endpoints by this setoid (K2.11). This definition is the canonical map from a concrete endpoint into that quotient.
proof idea
Pure constructor: apply Lean's Quot.mk to the SameT setoid at $(J,T)$ and the given endpoint $a$. No lemmas, no tactics.
why it matters
This is the introduction map for endpoint classes under SameT (K2.11). Downstream, endpointClass_eq_of_same (K4.4) uses it to show that SameT-related endpoints determine the same class via Quot.sound. The lift lemma endpointClassLift_mk uses it as the unit of the quotient elimination principle. The first-pass kernel certificate (K7/A2) depends on this quotient surface being inhabited and well-formed. In the Recognition stack this is scaffolding for treating endpoints up to judgmental sameness before any physics-facing forcing (T5–T8) is applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.