endpointClassLift_mk
plain-language theorem explainer
Computation rule for the endpoint-class quotient: after lifting a map that respects trace-sameness, evaluating on the class of an endpoint recovers the original value. Anyone manipulating SameT-quotients in the Primitive Recognition Calculus cites this as the standard β-rule. The proof is pure definitional reflexivity from Quot.lift/Quot.mk.
Claim. Let $J$ be an admissible trace judgment, $T$ a finite trace, and $f$ a map from endpoints to a type $\alpha$ such that $J.same\,T\,a\,b$ implies $f(a)=f(b)$. Then the quotient lift of $f$ applied to the SameT-class of any endpoint $a$ equals $f(a)$.
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). An admissible trace judgment $J$ supplies object-level sameness and difference predicates on endpoints at each trace, with sameness required to be reflexive (K2.6–K2.8, R5).
The SameT relation at a fixed trace induces a setoid on endpoints. The class of an endpoint is the corresponding quotient element; the lift construction is the standard quotient recursion for maps constant on SameT-pairs (K4.4). This module packages that quotient interface so later PRC arguments can work with classes rather than raw endpoints.
proof idea
One-line definitional proof. The lift is defined as Quot.lift f with the supplied SameT-respecting hypothesis, and the class constructor is Quot.mk of the SameT setoid. The identity Quot.lift f h (Quot.mk r a) = f a holds by the reduction rule of the quotient, so rfl closes the goal. Marked @[simp] for automatic unfolding at use sites.
why it matters
Closes the basic computational interface for K4.4 (quotient recursion for SameT-respecting maps) in the Primitive Recognition Calculus foundation. Without this β-rule, any argument that defines a quantity on endpoint classes via a representative-wise map cannot reduce back to the concrete value. No downstream consumers are wired yet in the graph; the lemma is infrastructure for later PRC development that treats sameness-classes as the true objects of recognition. It sits upstream of any forcing-chain or physical identification work that needs well-defined maps out of the endpoint quotient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.