endpointClassLift

In the primitive recognition calculus, an endpoint is one side of the primitive distinction (left or right). A finite trace is built by successive distinction acts from the empty trace. A trace judgment $J$ packages object-level SameT and DiffT predicates on endpoints at each trace, with SameT required to be reflexive (and, via the ambient setoid, an equivalence).

EndpointClass $J,T$ is the quotient of endpoints by the setoid generated by $J.\mathrm{same},T$. The doc labels this K2.11: “Endpoint trace-classes under SameT.” Maps out of that quotient are exactly the maps on endpoints that are constant on SameT-pairs at $T$.

This module sits in Foundation.PrimitiveRecognitionCalculus.Quotient and imports the SameDiff judgment surface. The local goal is the standard quotient API (class of an endpoint, equality of classes from SameT, and recursion/lift for respecting maps).

One-line wrapper around Quot.lift. The function $f$ is passed as the representative map; the proof obligation that $a\sim b$ implies $f,a=f,b$ is discharged by applying the supplied hypothesis hf to the setoid relation witness. No further algebraic work.

This is K4.4 in the PRC quotient layer: the recursion principle for SameT-respecting maps on endpoint classes. Downstream, endpointClassLift_mk records the computation rule that lifting and then evaluating on the class of $a$ recovers $f,a$ (the standard Quot.lift beta law).

Without this lift, later constructions that assign invariants, costs, or field values to endpoints could not pass to the quotient and would remain sensitive to SameT-redundant representatives. In the broader Recognition stack, endpoint classes are the first place where “same under the current trace” becomes a type, so every subsequent SameT-invariant quantity on the distinction calculus factors through this definition. It does not itself invoke the forcing chain (T5–T8) or the RCL; it is pure foundational bookkeeping for the PRC quotient.