EndpointClass
plain-language theorem explainer
Endpoint classes are the quotient of endpoints by SameT at a fixed finite trace, relative to an admissible judgment surface. Anyone building SameT-respecting maps or the first-pass PRC kernel certificate cites this type. The body is a one-line definition: the Lean quotient by the induced setoid.
Claim. Fix an admissible trace judgment $J$ and a finite trace $T$. The type of endpoint classes at $T$ is the quotient of endpoints by the equivalence relation $\mathrm{Same}_T$ of $J$.
background
In the Primitive Recognition Calculus, a finite trace is built inductively: empty, or extended by one distinction act (K2.4). An admissible trace judgment surface $J$ packages object-level Same and Diff predicates on endpoints at each trace, with Same required to be reflexive (and, via the setoid, an equivalence).
At fixed $J$ and $T$, sameSetoid is the setoid whose relation is $J$'s Same at $T$, with reflexivity, symmetry, and transitivity taken from the judgment axioms. Endpoint classes are the corresponding quotient type: two endpoints determine the same class exactly when Same holds at that trace.
This sits in the Quotient module of PRC foundation work (K2.11), upstream of quotient recursion and the kernel certificate chain.
proof idea
Pure definition: the type is Quot applied to the setoid induced by Same at the given judgment and trace. No proof obligations beyond those already discharged when the setoid was built.
why it matters
K2.11 introduces the stable objects on which SameT-invariant reasoning runs. Downstream, endpointClassOf embeds an endpoint into its class, and endpointClassLift (K4.4) lifts any SameT-respecting map on endpoints to a well-defined map on classes (quotient recursion).
The first-pass PRC kernel certificate bundles existence of judgment surfaces and trace logic; endpoint classes are the concrete type that makes "stable finite-trace predicates" mean quotient-level identity rather than raw endpoint equality. Without this quotient, later stages cannot treat SameT as equality of recognition endpoints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.