endpointClass_eq_of_same
plain-language theorem explainer
Under a fixed SameT judgment on a finite trace, related endpoints determine one and the same class in the endpoint quotient. Anyone defining or transporting maps out of that quotient cites this equality. The proof is a one-line application of quotient soundness to the SameT hypothesis.
Claim. Fix a trace judgment $J$ and a finite trace $T$. If endpoints $a$ and $b$ satisfy $J$'s SameT relation on $T$, then the quotient class of $a$ equals the quotient class of $b$ in the endpoint setoid induced by $J$ and $T$.
background
In the Primitive Recognition Calculus, an endpoint is one side of the primitive distinction (K2.3). A finite trace is built from the empty trace by successive distinction acts (K2.4). A TraceJudgment supplies, among other data, a SameT relation on endpoints relative to a given trace: the judgment that two endpoints are identified after that trace.
The module quotients endpoints by the setoid generated from that SameT relation. The class map sends an endpoint $a$ to its equivalence class under the setoid. This is the standard Lean quotient construction (Quot.mk on the SameT setoid), so equal classes are exactly the content of quotient soundness.
Upstream, the same pattern appears in the integers-from-logic construction, where Quotient.sound turns an additive witness into equality of integer classes. Here the witness is the SameT hypothesis rather than an integer equation.
proof idea
One-line term proof: apply Quot.sound to the given SameT hypothesis. By definition the class map is Quot.mk for the SameT setoid, so soundness yields equality of the two classes. No further rewriting or case analysis is required.
why it matters
This is K4.4 in the Primitive Recognition Calculus development: SameT endpoints determine the same quotient class. It is the soundness half of the endpoint quotient, the dual of the class-map definition. Sibling declarations (endpointClassLift, endpointClassLift_mk) use it to recurse SameT-respecting maps through the quotient, so maps out of endpoint classes are well-defined precisely when they respect SameT.
In the broader Recognition foundation, the quotient packages the primitive distinction into a coarser object on which later structure (exp/log field, Hamiltonian emergence on the finite register) can act without tracking redundant endpoint labels. No downstream theorem currently depends on this lemma in the graph, but it is the necessary glue for any K4.4-style lift.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.