IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Quotient
Defines the setoid induced by the SameT relation at a fixed trace, and the resulting quotient of endpoint classes. Recognition calculus constructions that need to treat same-difference endpoints as identical cite this layer. The module is definitional: setoid, class type, canonical map, and the lift of functions constant on SameT-classes.
claimAt a fixed trace, the relation $\mathrm{SameT}$ is a setoid on endpoints. Write $[e]$ for the equivalence class of an endpoint $e$ (an endpoint class). Functions constant on $\mathrm{SameT}$-pairs descend uniquely to the quotient of endpoint classes.
background
Primitive Recognition Calculus works with traces and endpoints before any continuum limit. The upstream SameDiff layer supplies the relation SameT: two endpoints are identified when they realize the same difference structure relative to a fixed trace. That relation is the raw material for quotienting.
This module packages SameT as a Lean setoid sameSetoid, introduces the type EndpointClass of equivalence classes, and the canonical map endpointClassOf sending an endpoint to its class. Equality of classes is characterized by endpointClass_eq_of_same: two classes coincide exactly when representatives are SameT-related.
The lift endpointClassLift (with computation rule endpointClassLift_mk) is the universal property of the quotient: any map out of endpoints that is constant on SameT-pairs factors uniquely through endpoint classes. Downstream Kernel imports this quotient so kernel-level identities can be stated on classes rather than on raw endpoints.
proof idea
Definition module, not a theorem chain. It declares the setoid from SameT, the quotient type of endpoint classes, the class-of map, the characterization of class equality by SameT, and the standard quotient lift with its computation on representatives. Any nontrivial obligations are discharged by the setoid and quotient API from Mathlib together with SameDiff facts about SameT.
why it matters in Recognition Science
K2.11 in the foundation numbering: the setoid induced by SameT at a fixed trace. Without this quotient, later calculus would have to carry SameT-invariance hypotheses on every map. Kernel imports the module and works on endpoint classes, so identities and operators there are well-defined on the quotient rather than on representatives. In the broader Recognition stack this is bookkeeping infrastructure under the forcing chain, not a T5–T8 landmark itself; it keeps the primitive calculus coherent before cost, $\phi$, and dimension forcing appear.
scope and limits
- Does not prove that SameT is an equivalence relation beyond packaging it as a setoid.
- Does not define cost, J, or any Recognition Composition Law identity.
- Does not force $\phi$, eight-tick structure, or spatial dimension $D=3$.
- Does not construct the Kernel; only supplies the quotient Kernel imports.
- Does not identify endpoint classes across different traces.